diff options
| author | Hannes Schulze <contact@haschu.me> | 2026-04-14 16:04:44 +0200 |
|---|---|---|
| committer | Hannes Schulze <contact@haschu.me> | 2026-04-15 13:22:40 +0200 |
| commit | a5ff8efe5b5e314e0aa759318e5fb194e066f612 (patch) | |
| tree | 4d13dd84ac4ced2360a51799f0e5c846bd733872 /Algebra | |
| parent | 43942e78f4b3ed4cfca3b508f06161d0983c545e (diff) | |
update lean
Diffstat (limited to 'Algebra')
| -rw-r--r-- | Algebra/Derivations.lean | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/Algebra/Derivations.lean b/Algebra/Derivations.lean index 717ffe1..b6e5cb5 100644 --- a/Algebra/Derivations.lean +++ b/Algebra/Derivations.lean @@ -118,11 +118,11 @@ lemma Derivable.of_eq Derivable T eq := by intro hderiv have heq : (eq.val.vars ⊢ t ≣ u) = eq := by - apply Subtype.eq; ext + apply Subtype.ext; ext · rfl · rfl - · rw [heq_eq_eq]; exact ht - · rw [heq_eq_eq]; exact hu + · exact heq_of_eq ht + · exact heq_of_eq hu rw [← heq]; exact hderiv lemma Derivable.equivariant_substitution @@ -180,7 +180,7 @@ lemma Derivable.equivariant {m : ℕ} {t u : TermAtDepth 𝔸 T.sig X m} : · rw [rename_eq] apply Derivable.trans (by apply Derivable.symm; apply equivariant_substitution; exact h_1) _ apply Derivable.trans _ (by apply equivariant_substitution; exact h_1) - rw [← MulAction.mul_smul, ← MulAction.mul_smul] + rw [← SemigroupAction.mul_smul, ← SemigroupAction.mul_smul] apply Derivable.ax · exact h · exact h_1 @@ -195,7 +195,7 @@ lemma Derivable.equivariant {m : ℕ} {t u : TermAtDepth 𝔸 T.sig X m} : exact h_1 x · intro x show Derivable T (X_1 ⊢ π • ts x ≣ ⸨π a, π b⸩ • π • us x) - rw [← MulAction.mul_smul, ← FPerm.mul_swap_eq_swap_mul, MulAction.mul_smul] + rw [← SemigroupAction.mul_smul, ← FPerm.mul_swap_eq_swap_mul, SemigroupAction.mul_smul] exact a_ih x instance DerivableEq.instEquivariant : Rel.Equivariant 𝔸 (DerivableEq T X n) := by |