chore(algebra/group_with_zero): cleanup (#5762)

* remove `classical,` from proofs: we have `open_locale classical` anyway;
* add a lemma `a / (a * a) = a⁻¹`, use it to golf some proofs in other files.

src/algebra/group_with_zero/basic.lean

@@ -411,7 +411,6 @@ calc 1⁻¹ = 1 * 1⁻¹ : by rw [one_mul]
 
 @[simp] lemma inv_inv' (a : G₀) : a⁻¹⁻¹ = a :=
 begin
-  classical,
   by_cases h : a = 0, { simp [h] },
   calc a⁻¹⁻¹ = a * (a⁻¹ * a⁻¹⁻¹) : by simp [h]
          ... = a                 : by simp [inv_ne_zero h]
@@ -421,7 +420,6 @@ end
 (whether or not `a` is zero). -/
 @[simp] lemma mul_self_mul_inv (a : G₀) : a * a * a⁻¹ = a :=
 begin
-  classical,
   by_cases h : a = 0,
   { rw [h, inv_zero, mul_zero] },
   { rw [mul_assoc, mul_inv_cancel h, mul_one] }
@@ -431,7 +429,6 @@ end
 (whether or not `a` is zero). -/
 @[simp] lemma mul_inv_mul_self (a : G₀) : a * a⁻¹ * a = a :=
 begin
-  classical,
   by_cases h : a = 0,
   { rw [h, inv_zero, mul_zero] },
   { rw [mul_inv_cancel h, one_mul] }
@@ -441,7 +438,6 @@ end
 is zero). -/
 @[simp] lemma inv_mul_mul_self (a : G₀) : a⁻¹ * a * a = a :=
 begin
-  classical,
   by_cases h : a = 0,
   { rw [h, inv_zero, mul_zero] },
   { rw [inv_mul_cancel h, one_mul] }
@@ -525,7 +521,7 @@ units.exists_iff_ne_zero
 instance group_with_zero.no_zero_divisors : no_zero_divisors G₀ :=
 { eq_zero_or_eq_zero_of_mul_eq_zero := λ a b h,
     begin
-      classical, contrapose! h,
+      contrapose! h,
       exact ((units.mk0 a h.1) * (units.mk0 b h.2)).ne_zero
     end,
   .. (‹_› : group_with_zero G₀) }
@@ -540,7 +536,6 @@ instance group_with_zero.cancel_monoid_with_zero : cancel_monoid_with_zero G₀
 
 lemma mul_inv_rev' (x y : G₀) : (x * y)⁻¹ = y⁻¹ * x⁻¹ :=
 begin
-  classical,
   by_cases hx : x = 0, { simp [hx] },
   by_cases hy : y = 0, { simp [hy] },
   symmetry,
@@ -574,6 +569,10 @@ classical.by_cases (λ hb : b = 0, by simp [*]) (mul_div_cancel a)
 
 local attribute [simp] div_eq_mul_inv mul_comm mul_assoc mul_left_comm
 
+@[simp] lemma div_self_mul_self' (a : G₀) : a / (a * a) = a⁻¹ :=
+calc a / (a * a) = a⁻¹⁻¹ * a⁻¹ * a⁻¹ : by simp [mul_inv_rev']
+... = a⁻¹ : inv_mul_mul_self _
+
 lemma div_eq_mul_one_div (a b : G₀) : a / b = a * (1 / b) :=
 by simp
 
@@ -655,7 +654,6 @@ eq.symm $ div_eq_of_eq_mul hx h.symm
 
 lemma eq_of_div_eq_one (h : a / b = 1) : a = b :=
 begin
-  classical,
   by_cases hb : b = 0,
   { rw [hb, div_zero] at h,
     exact eq_of_zero_eq_one h a b },
@@ -860,7 +858,6 @@ semiconj_by.inv_symm_left_iff'.2 h
 
 lemma inv_right' (h : semiconj_by a x y) : semiconj_by a x⁻¹ y⁻¹ :=
 begin
-  classical,
   by_cases ha : a = 0,
   { simp only [ha, zero_left] },
   by_cases hx : x = 0,
@@ -922,7 +919,7 @@ lemma map_ne_zero : f a ≠ 0 ↔ a ≠ 0 :=
 ⟨λ hfa ha, hfa $ ha.symm ▸ f.map_zero, λ ha, ((is_unit.mk0 a ha).map f.to_monoid_hom).ne_zero⟩
 
 @[simp] lemma map_eq_zero : f a = 0 ↔ a = 0 :=
-by { classical, exact not_iff_not.1 f.map_ne_zero }
+not_iff_not.1 f.map_ne_zero
 
 end monoid_with_zero
 
@@ -933,7 +930,7 @@ variables (f : monoid_with_zero_hom G₀ G₀') (a b : G₀)
 /-- A monoid homomorphism between groups with zeros sending `0` to `0` sends `a⁻¹` to `(f a)⁻¹`. -/
 @[simp] lemma map_inv' : f a⁻¹ = (f a)⁻¹ :=
 begin
-  classical, by_cases h : a = 0, by simp [h],
+  by_cases h : a = 0, by simp [h],
   apply eq_inv_of_mul_left_eq_one,
   rw [← f.map_mul, inv_mul_cancel h, f.map_one]
 end

src/analysis/special_functions/pow.lean

@@ -775,8 +775,7 @@ begin
       congr,
       norm_num },
     rw [sub_eq_add_neg, rpow_add H, B, rpow_neg (le_of_lt H)],
-    field_simp [hx, ne_of_gt A],
-    ring }
+    field_simp }
 end
 
 lemma has_deriv_at.sqrt (hf : has_deriv_at f f' x) (hx : f x ≠ 0) :

src/data/complex/basic.lean

@@ -277,11 +277,7 @@ theorem inv_def (z : ℂ) : z⁻¹ = conj z * ((norm_sq z)⁻¹:ℝ) := rfl
 @[simp] lemma inv_im (z : ℂ) : (z⁻¹).im = -z.im / norm_sq z := by simp [inv_def, division_def]
 
 @[simp, norm_cast] lemma of_real_inv (r : ℝ) : ((r⁻¹ : ℝ) : ℂ) = r⁻¹ :=
-ext_iff.2 $ begin
-  simp,
-  by_cases r = 0, { simp [h] },
-  { rw [← div_div_eq_div_mul, div_self h, one_div] },
-end
+ext_iff.2 $ by simp
 
 protected lemma inv_zero : (0⁻¹ : ℂ) = 0 :=
 by rw [← of_real_zero, ← of_real_inv, inv_zero]

src/data/complex/is_R_or_C.lean

@@ -670,20 +670,7 @@ noncomputable instance real.is_R_or_C : is_R_or_C ℝ :=
   norm_sq_eq_def_ax := λ z, by simp only [pow_two, norm, ←abs_mul, abs_mul_self z, add_zero, mul_zero,
     add_monoid_hom.zero_apply, add_monoid_hom.id_apply],
   mul_im_I_ax := λ z, by simp only [mul_zero, add_monoid_hom.zero_apply],
-  inv_def_ax :=
-    begin
-      intro z,
-      unfold_coes,
-      have H : z ≠ 0 → 1 / z = z / (z * z) := λ h,
-        calc
-          1 / z = 1 * (1 / z)           : (one_mul (1 / z)).symm
-            ... = (z / z) * (1 / z)     : congr_arg (λ x, x * (1 / z)) (div_self h).symm
-            ... = z / (z * z)           : by field_simp,
-      rcases lt_trichotomy z 0 with hlt|heq|hgt,
-      { field_simp [norm, abs, max_eq_right_of_lt (show z < -z, by linarith), pow_two, mul_inv', ←H (ne_of_lt hlt)] },
-      { simp [heq] },
-      { field_simp [norm, abs, max_eq_left_of_lt (show -z < z, by linarith), pow_two, mul_inv', ←H (ne_of_gt hgt)] },
-    end,
+  inv_def_ax := λ z, by simp [pow_two, real.norm_eq_abs, abs_mul_abs_self, ← div_eq_mul_inv],
   div_I_ax := λ z, by simp only [div_zero, mul_zero, neg_zero]}
 
 noncomputable instance complex.is_R_or_C : is_R_or_C ℂ :=

src/data/zsqrtd/gaussian_int.lean

@@ -146,7 +146,7 @@ calc ((x / y : ℂ) - ((x / y : ℤ[i]) : ℂ)).norm_sq =
     ((x / y : ℂ).im - ((x / y : ℤ[i]) : ℂ).im) * I : ℂ).norm_sq :
       congr_arg _ $ by apply complex.ext; simp
   ... ≤ (1 / 2 + 1 / 2 * I).norm_sq :
-  have abs' (2 / (2 * 2) : ℝ) = 1 / 2, by rw _root_.abs_of_nonneg; norm_num,
+  have abs' (2⁻¹ : ℝ) = 2⁻¹, from _root_.abs_of_nonneg (by norm_num),
   norm_sq_le_norm_sq_of_re_le_of_im_le
     (by rw [to_complex_div_re]; simp [norm_sq, this];
       simpa using abs_sub_round (x / y : ℂ).re)