From a5ff8efe5b5e314e0aa759318e5fb194e066f612 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Tue, 14 Apr 2026 16:04:44 +0200 Subject: update lean --- Algebra/Derivations.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'Algebra/Derivations.lean') 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 -- cgit v1.3.1