From 175ac2c818553dd317f97a6cd64dd08a50db63d3 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sun, 31 Oct 2021 10:19:07 +0000
Subject: [PATCH] chore(algebra/group/defs): golf a proof (#10067)

Use `monoid.ext` to golf `div_inv_monoid.ext`.
---
 src/algebra/group/defs.lean | 27 ++++++++-------------------
 1 file changed, 8 insertions(+), 19 deletions(-)

diff --git a/src/algebra/group/defs.lean b/src/algebra/group/defs.lean
index cb260933aa832..dfdd4aece13af 100644
--- a/src/algebra/group/defs.lean
+++ b/src/algebra/group/defs.lean
@@ -610,31 +610,20 @@ lemma div_inv_monoid.ext {M : Type*} ⦃m₁ m₂ : div_inv_monoid M⦄ (h_mul :
   (h_inv : m₁.inv = m₂.inv) : m₁ = m₂ :=
 begin
   let iM : div_inv_monoid M := m₁,
+  have : @div_inv_monoid.to_monoid M m₁ = @div_inv_monoid.to_monoid M m₂, from monoid.ext h_mul,
   unfreezingI {
     cases m₁ with mul₁ _ one₁ one_mul₁ mul_one₁ npow₁ npow_zero₁ npow_succ₁ inv₁ div₁
       div_eq_mul_inv₁ zpow₁ zpow_zero'₁ zpow_succ'₁ zpow_neg'₁,
     cases m₂ with mul₂ _ one₂ one_mul₂ mul_one₂ npow₂ npow_zero₂ npow_succ₂ inv₂ div₂
       div_eq_mul_inv₂ zpow₂ zpow_zero'₂ zpow_succ'₂ zpow_neg'₂ },
-  change mul₁ = mul₂ at h_mul,
-  subst h_mul,
-  have h_one : one₁ = one₂,
-  { rw ←one_mul₂ one₁,
-    exact mul_one₁ one₂ },
-  subst h_one,
-  have h_npow : npow₁ = npow₂,
-  { ext n,
-    induction n with d hd,
-    { rw [npow_zero₁, npow_zero₂] },
-    { rw [npow_succ₁, npow_succ₂, hd] } },
-  subst h_npow,
-  change inv₁ = inv₂ at h_inv,
-  subst h_inv,
-  have h_div : div₁ = div₂,
+  dunfold div_inv_monoid.to_monoid at this, simp only at this,
+  obtain rfl : mul₁ = mul₂ := h_mul,
+  obtain rfl : one₁ = one₂, by injection this,
+  obtain rfl : npow₁ = npow₂, by injection this,
+  obtain rfl : inv₁ = inv₂ := h_inv,
+  obtain rfl : div₁ = div₂,
   { ext a b,
-    convert (rfl : a * b⁻¹ = a * b⁻¹),
-    { exact div_eq_mul_inv₁ a b },
-    { exact div_eq_mul_inv₂ a b } },
-  subst h_div,
+    exact (div_eq_mul_inv₁ a b).trans (div_eq_mul_inv₂ a b).symm },
   have h_zpow_aux : ∀ n g, zpow₁ (int.of_nat n) g = zpow₂ (int.of_nat n) g,
   { intros n g,
     induction n with n IH,