chore(Algebra/Group): remove backward.privateInPublic

Author: wwylele

Mathlib/Algebra/Group/Defs.lean

@@ -1213,13 +1213,10 @@ variable [Group G] {a b : G}
 theorem inv_mul_cancel (a : G) : a⁻¹ * a = 1 :=
   Group.inv_mul_cancel a
 
-set_option backward.privateInPublic true in
 @[to_additive]
 private theorem inv_eq_of_mul (h : a * b = 1) : a⁻¹ = b :=
   left_inv_eq_right_inv (inv_mul_cancel a) h
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 @[to_additive (attr := simp)]
 theorem mul_inv_cancel (a : G) : a * a⁻¹ = 1 := by
   rw [← inv_mul_cancel a⁻¹, inv_eq_of_mul (inv_mul_cancel a)]
@@ -1251,14 +1248,13 @@ theorem inv_mul_cancel_right (a b : G) : a * b⁻¹ * b = a := by
 theorem div_mul_cancel (a b : G) : a / b * b = a := by
   rw [div_eq_mul_inv, inv_mul_cancel_right a b]
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 @[to_additive]
-instance (priority := 100) Group.toDivisionMonoid : DivisionMonoid G :=
-  { inv_inv := fun a ↦ inv_eq_of_mul (inv_mul_cancel a)
-    mul_inv_rev :=
-      fun a b ↦ inv_eq_of_mul <| by rw [mul_assoc, mul_inv_cancel_left, mul_inv_cancel]
-    inv_eq_of_mul := fun _ _ ↦ inv_eq_of_mul }
+instance (priority := 100) Group.toDivisionMonoid : DivisionMonoid G where
+  inv_inv a := by exact inv_eq_of_mul (inv_mul_cancel a)
+  mul_inv_rev a b := by
+    apply inv_eq_of_mul
+    rw [mul_assoc, mul_inv_cancel_left, mul_inv_cancel]
+  inv_eq_of_mul _ _ := by exact inv_eq_of_mul
 
 -- see Note [lower instance priority]
 @[to_additive]

Mathlib/Algebra/Group/Subsemigroup/Operations.lean

@@ -551,17 +551,14 @@ theorem coe_srange (f : M →ₙ* N) : (f.srange : Set N) = Set.range f :=
 theorem mem_srange {f : M →ₙ* N} {y : N} : y ∈ f.srange ↔ ∃ x, f x = y :=
   Iff.rfl
 
-set_option backward.privateInPublic true in
 @[to_additive]
 private theorem srange_mk_aux_mul {f : M → N} (hf : ∀ (x y : M), f (x * y) = f x * f y)
     {x y : N} (hx : x ∈ Set.range f) (hy : y ∈ Set.range f) :
     x * y ∈ Set.range f :=
   (srange ⟨f, hf⟩).mul_mem hx hy
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 @[to_additive (attr := simp)] theorem srange_mk (f : M → N) (hf) :
-    srange ⟨f, hf⟩ = ⟨Set.range f, srange_mk_aux_mul hf⟩ := rfl
+    srange ⟨f, hf⟩ = ⟨Set.range f, by exact srange_mk_aux_mul hf⟩ := rfl
 
 @[to_additive]
 theorem srange_eq_map (f : M →ₙ* N) : f.srange = (⊤ : Subsemigroup M).map f :=

Mathlib/Algebra/GroupWithZero/Basic.lean

@@ -353,28 +353,23 @@ theorem inv_mul_cancel_left₀ (h : a ≠ 0) (b : G₀) : a⁻¹ * (a * b) = b :
     _ = b := by simp [h]
 
 
-set_option backward.privateInPublic true in
 private theorem inv_eq_of_mul (h : a * b = 1) : a⁻¹ = b := by
   rw [← inv_mul_cancel_left₀ (left_ne_zero_of_mul_eq_one h) b, h, mul_one]
 
 -- See note [lower instance priority]
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
-instance (priority := 100) GroupWithZero.toDivisionMonoid : DivisionMonoid G₀ :=
-  { ‹GroupWithZero G₀› with
-    inv := Inv.inv,
-    inv_inv := fun a => by
-      by_cases h : a = 0
-      · simp [h]
-      · exact left_inv_eq_right_inv (inv_mul_cancel₀ <| inv_ne_zero h) (inv_mul_cancel₀ h)
-    mul_inv_rev := fun a b => by
-      by_cases ha : a = 0
-      · simp [ha]
-      by_cases hb : b = 0
-      · simp [hb]
-      apply inv_eq_of_mul
-      simp [mul_assoc, ha, hb],
-    inv_eq_of_mul := fun _ _ => inv_eq_of_mul }
+instance (priority := 100) GroupWithZero.toDivisionMonoid : DivisionMonoid G₀ where
+  inv_inv a := by
+    by_cases h : a = 0
+    · simp [h]
+    · exact left_inv_eq_right_inv (inv_mul_cancel₀ <| inv_ne_zero h) (inv_mul_cancel₀ h)
+  mul_inv_rev a b := by
+    by_cases ha : a = 0
+    · simp [ha]
+    by_cases hb : b = 0
+    · simp [hb]
+    apply inv_eq_of_mul
+    simp [mul_assoc, ha, hb]
+  inv_eq_of_mul _ _ := by exact inv_eq_of_mul
 
 -- see Note [lower instance priority]
 instance (priority := 10) : IsCancelMulZero G₀ where