From 84e03cc730fef9e75e8599792f98e444a660059b Mon Sep 17 00:00:00 2001
From: Hannah Fechtner <hfechtne@andrew.cmu.edu>
Date: Wed, 30 Oct 2024 23:38:49 -0400
Subject: [PATCH] reorder to avoid implicit arguments

---
 Mathlib/GroupTheory/Congruence/Basic.lean | 78 +++++++++++------------
 1 file changed, 38 insertions(+), 40 deletions(-)

diff --git a/Mathlib/GroupTheory/Congruence/Basic.lean b/Mathlib/GroupTheory/Congruence/Basic.lean
index 0c9fddf70f563..0f770ce5bd992 100644
--- a/Mathlib/GroupTheory/Congruence/Basic.lean
+++ b/Mathlib/GroupTheory/Congruence/Basic.lean
@@ -89,46 +89,44 @@ theorem conGen_le_comap {M N : Type*} [Mul M] [Mul N] (f : M → N)
 theorem comap_conGen_of_Bijective {M N : Type*} [Mul M] [Mul N] (f : M → N)
     (hf : Function.Bijective f) (H : ∀ (x y : M), f (x * y) = f x * f y) (rel : N → N → Prop) :
     Con.comap f H (conGen rel) = conGen (fun x y ↦ rel (f x) (f y)) := by
-  ext a b
-  constructor
-  · intro h
-    simp only [Con.comap_rel] at h
-    have H : ∀ n1 n2, (conGen rel) n1 n2 → ∀ a b, f a = n1 → f b = n2 →
-        (conGen fun x y ↦ rel (f x) (f y)) a b := by
-      intro n1 n2 h
-      induction h with
-      | of x y h =>
-        intro _ _ fa fb
-        apply ConGen.Rel.of
-        rw [fa, fb]
-        exact h
-      | refl x =>
-        intro _ _ fc fd
-        rw [hf.1 (fc.trans fd.symm)]
-        exact ConGen.Rel.refl _
-      | symm _ h => exact fun a b fs fb ↦ ConGen.Rel.symm (h b a fb fs)
-      | trans _ _ ih ih1 =>
-        exact fun a b fa fb ↦ Exists.casesOn (hf.right _) fun c' hc' ↦
-        ConGen.Rel.trans (ih a c' fa hc') (ih1 c' b hc' fb)
-      | mul _ _ ih ih1 =>
-        rename_i w x y z _ _
-        intro a b fa fb
-        rcases Function.bijective_iff_has_inverse.mp hf with ⟨f', is_inv⟩
-        have Ha : a = f' w * f' y := by
-          rw [← is_inv.1 a, fa]
-          have H : f (f' (w * y)) = f (f' w * f' y) := by
-            rw [is_inv.2 (w * y), H, is_inv.2 w, is_inv.2 y]
-          exact hf.1 H
-        have Hb : b = f' x * f' z := by
-          rw [← is_inv.1 b, fb]
-          have H : f (f' (x * z)) = f (f' x * f' z) := by
-            rw [is_inv.2 (x * z), H, is_inv.2 x, is_inv.2 z]
-          exact hf.1 H
-        rw [Ha, Hb]
-        exact ConGen.Rel.mul (ih (f' w) (f' x) (is_inv.right w) (is_inv.right x))
-          (ih1 (f' y) (f' z) (is_inv.right y) (is_inv.right z))
-    exact H (f a) (f b) h a b (refl _) (refl _)
-  exact @conGen_le_comap _ _ _ _ f H rel a b
+  apply le_antisymm _ (conGen_le_comap f H rel)
+  intro a b h
+  simp only [Con.comap_rel] at h
+  have H : ∀ n1 n2, (conGen rel) n1 n2 → ∀ a b, f a = n1 → f b = n2 →
+      (conGen fun x y ↦ rel (f x) (f y)) a b := by
+    intro n1 n2 h
+    induction h with
+    | of x y h =>
+      intro _ _ fa fb
+      apply ConGen.Rel.of
+      rw [fa, fb]
+      exact h
+    | refl x =>
+      intro _ _ fc fd
+      rw [hf.1 (fc.trans fd.symm)]
+      exact ConGen.Rel.refl _
+    | symm _ h => exact fun a b fs fb ↦ ConGen.Rel.symm (h b a fb fs)
+    | trans _ _ ih ih1 =>
+      exact fun a b fa fb ↦ Exists.casesOn (hf.right _) fun c' hc' ↦
+      ConGen.Rel.trans (ih a c' fa hc') (ih1 c' b hc' fb)
+    | mul _ _ ih ih1 =>
+      rename_i w x y z _ _
+      intro a b fa fb
+      rcases Function.bijective_iff_has_inverse.mp hf with ⟨f', is_inv⟩
+      have Ha : a = f' w * f' y := by
+        rw [← is_inv.1 a, fa]
+        have H : f (f' (w * y)) = f (f' w * f' y) := by
+          rw [is_inv.2 (w * y), H, is_inv.2 w, is_inv.2 y]
+        exact hf.1 H
+      have Hb : b = f' x * f' z := by
+        rw [← is_inv.1 b, fb]
+        have H : f (f' (x * z)) = f (f' x * f' z) := by
+          rw [is_inv.2 (x * z), H, is_inv.2 x, is_inv.2 z]
+        exact hf.1 H
+      rw [Ha, Hb]
+      exact ConGen.Rel.mul (ih (f' w) (f' x) (is_inv.right w) (is_inv.right x))
+        (ih1 (f' y) (f' z) (is_inv.right y) (is_inv.right z))
+  exact H (f a) (f b) h a b (refl _) (refl _)
 
 end