simplify derive_char

katydid · Aug 29, 2024 · 1a97e16 · 1a97e16
1 parent 91dbeb7
commit 1a97e16
Showing 1 changed file with 10 additions and 19 deletions.
diff --git a/Sadol/Calculus.lean b/Sadol/Calculus.lean
@@ -227,31 +227,22 @@ def derive_char {α: Type u} {a: α} {c: α} {w: List α}:
   refine TEquiv.mk ?toFun ?invFun ?leftInv ?rightInv
   case toFun =>
     intro ⟨ D ⟩
-    cases D with
-    | refl =>
-      exact ⟨ trfl, trfl ⟩
+    cases D with | refl =>
+    exact ⟨ trfl, trfl ⟩
   case invFun =>
     intro ⟨ ⟨ S1 ⟩ , ⟨ S2 ⟩  ⟩
-    cases S1 with
-    | refl =>
-      cases S2 with
-      | refl =>
-        exact trfl
+    cases S1 with | refl =>
+    cases S2 with | refl =>
+    exact trfl
   case leftInv =>
-    simp
     intro ⟨ H ⟩
-    cases H with
-    | refl =>
-      exact trfl
+    cases H with | refl =>
+    exact trfl
   case rightInv =>
-    simp
     intro ⟨ ⟨ H1 ⟩, ⟨ H2 ⟩ ⟩
-    simp
-    cases H1 with
-    | refl =>
-      cases H2 with
-      | refl =>
-        exact trfl
+    cases H1 with | refl =>
+    cases H2 with | refl =>
+    exact trfl
 
 -- δ∪  : δ (P ∪ Q) a ≡ δ P a ∪ δ Q a
 -- δ∪ = refl