Simplify some uses of field_simp, to show the effect (more to come)

Archive/Imo/Imo2005Q3.lean

@@ -25,9 +25,6 @@ namespace Imo2005Q3
 
 theorem key_insight (x y z : ℝ) (hx : x > 0) (hy : y > 0) (hz : z > 0) (h : x * y * z ≥ 1) :
     (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) ≥ (x ^ 2 - y * z) / (x ^ 2 + y ^ 2 + z ^ 2) := by
-  -- have h₁ : x ^ 5 + y ^ 2 + z ^ 2 ≠ 0 := by positivity
-  -- have h₃ : x ^ 2 + y ^ 2 + z ^ 2 ≠ 0 := by positivity
-  -- have h₄ : x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2) ≠ 0 := by positivity
   have key :
     (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) -
         (x ^ 5 - x ^ 2 * 1) / (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)) =

Archive/Imo/Imo2008Q4.lean

@@ -48,10 +48,8 @@ theorem imo2008_q4 (f : ℝ → ℝ) (H₁ : ∀ x > 0, f x > 0) :
       rw [h w hw, h x hx, h (y ^ 2) (pow_pos hy 2), h (z ^ 2) (pow_pos hz 2)]
     · intro w x y z hw hx hy hz hprod
       rw [h w hw, h x hx, h (y ^ 2) (pow_pos hy 2), h (z ^ 2) (pow_pos hz 2)]
-      have hy2z2 : y ^ 2 + z ^ 2 ≠ 0 := ne_of_gt (add_pos (pow_pos hy 2) (pow_pos hz 2))
-      have hz2y2 : z ^ 2 + y ^ 2 ≠ 0 := ne_of_gt (add_pos (pow_pos hz 2) (pow_pos hy 2))
       have hp2 : w ^ 2 * x ^ 2 = y ^ 2 * z ^ 2 := by linear_combination (w * x + y * z) * hprod
-      field_simp [ne_of_gt hw, ne_of_gt hx, ne_of_gt hy, ne_of_gt hz, hy2z2, hz2y2, hp2]
+      field_simp [hp2]
       ring
   -- proof that the only solutions are f(x) = x or f(x) = 1/x
   intro H₂
@@ -66,7 +64,6 @@ theorem imo2008_q4 (f : ℝ → ℝ) (H₁ : ∀ x > 0, f x > 0) :
     have h1xss : 1 * x = sqrt x * sqrt x := by rw [one_mul, mul_self_sqrt (le_of_lt hx)]
     specialize H₂ 1 x (sqrt x) (sqrt x) zero_lt_one hx (sqrt_pos.mpr hx) (sqrt_pos.mpr hx) h1xss
     rw [h₁, one_pow 2, sq_sqrt (le_of_lt hx), ← two_mul (f x), ← two_mul x] at H₂
-    have hx_ne_0 : x ≠ 0 := ne_of_gt hx
     have hfx_ne_0 : f x ≠ 0 := by specialize H₁ x hx; exact ne_of_gt H₁
     field_simp at H₂ ⊢
     linear_combination 1 / 2 * H₂
@@ -82,12 +79,12 @@ theorem imo2008_q4 (f : ℝ → ℝ) (H₁ : ∀ x > 0, f x > 0) :
   specialize H₂ a b (sqrt (a * b)) (sqrt (a * b)) ha hb (sqrt_pos.mpr hab) (sqrt_pos.mpr hab) habss
   rw [sq_sqrt (le_of_lt hab), ← two_mul (f (a * b)), ← two_mul (a * b)] at H₂
   rw [hfa₂, hfb₂] at H₂
-  have h2ab_ne_0 : 2 * (a * b) ≠ 0 := mul_ne_zero two_ne_zero (ne_of_gt hab)
+  have h2ab_ne_0 : 2 * (a * b) ≠ 0 := by positivity
   specialize h₃ (a * b) hab
   cases' h₃ with hab₁ hab₂
   -- f(ab) = ab → b^4 = 1 → b = 1 → f(b) = b → false
-  · field_simp [hab₁] at H₂
-    field_simp [ne_of_gt hb] at H₂
+  · rw [ hab₁, div_left_inj' h2ab_ne_0 ] at H₂
+    field_simp at H₂
     have hb₁ : b ^ 4 = 1 := by linear_combination -H₂
     obtain hb₂ := abs_eq_one_of_pow_eq_one b 4 (show 4 ≠ 0 by norm_num) hb₁
     rw [abs_of_pos hb] at hb₂; rw [hb₂] at hfb₁; exact hfb₁ h₁

Archive/Imo/Imo2013Q1.lean

@@ -67,12 +67,11 @@ theorem imo2013_q1 (n : ℕ+) (k : ℕ) :
     use m
     have hmpk : (m pk : ℚ) = 2 * t + 2 ^ pk.succ := by
       have : m pk = ⟨2 * t + 2 ^ pk.succ, _⟩ := if_neg (irrefl pk); simp [this]
-    have denom_ne_zero : (2 * (t : ℚ) + 2 * 2 ^ pk) ≠ 0 := by positivity
     calc
       ((1 : ℚ) + (2 ^ pk.succ - 1) / (n : ℚ) : ℚ)= 1 + (2 * 2 ^ pk - 1) / (2 * (t + 1) : ℕ) := by
         rw [ht, pow_succ]
       _ = (1 + 1 / (2 * t + 2 * 2 ^ pk)) * (1 + (2 ^ pk - 1) / (↑t + 1)) := by
-        field_simp [t.cast_add_one_ne_zero]
+        field_simp
         ring
       _ = (1 + 1 / (2 * t + 2 ^ pk.succ)) * (1 + (2 ^ pk - 1) / t_succ) := by
         -- porting note: used to work with `norm_cast`
@@ -90,12 +89,11 @@ theorem imo2013_q1 (n : ℕ+) (k : ℕ) :
     have hmpk : (m pk : ℚ) = 2 * t + 1 := by
       have : m pk = ⟨2 * t + 1, _⟩ := if_neg (irrefl pk)
       simp [this]
-    have denom_ne_zero : 2 * (t : ℚ) + 1 ≠ 0 := by norm_cast; apply (2 * t).succ_ne_zero
     calc
       ((1 : ℚ) + (2 ^ pk.succ - 1) / ↑n : ℚ) = 1 + (2 * 2 ^ pk - 1) / (2 * t + 1 : ℕ) := by
         rw [ht, pow_succ]
       _ = (1 + 1 / (2 * t + 1)) * (1 + (2 ^ pk - 1) / (t + 1)) := by
-        field_simp [t.cast_add_one_ne_zero]
+        field_simp
         ring
       _ = (1 + 1 / (2 * t + 1)) * (1 + (2 ^ pk - 1) / t_succ) := by norm_cast
       _ = (∏ i in Finset.range pk, (1 + 1 / (m i : ℚ))) * (1 + 1 / ↑(m pk)) := by

Mathlib/Analysis/Convex/Slope.lean

@@ -32,18 +32,14 @@ theorem ConvexOn.slope_mono_adjacent (hf : ConvexOn 𝕜 s f) {x y z : 𝕜} (hx
     linarith
   set a := (z - y) / (z - x)
   set b := (y - x) / (z - x)
-  have hy : a • x + b • z = y := by
-    field_simp
-    rw [div_eq_iff] <;> [ring; linarith]
+  have hy : a • x + b • z = y := by field_simp; ring
   have key :=
     hf.2 hx hz (show 0 ≤ a by apply div_nonneg <;> linarith)
       (show 0 ≤ b by apply div_nonneg <;> linarith)
-      (show a + b = 1 by
-        field_simp
-        rw [div_eq_iff] <;> [ring; linarith])
+      (show a + b = 1 by field_simp)
   rw [hy] at key
   replace key := mul_le_mul_of_nonneg_left key hxz.le
-  field_simp [hxy.ne', hyz.ne', hxz.ne', mul_comm (z - x) _] at key ⊢
+  field_simp [mul_comm (z - x) _] at key ⊢
   rw [div_le_div_right]
   · linarith
   · nlinarith
@@ -72,17 +68,13 @@ theorem StrictConvexOn.slope_strict_mono_adjacent (hf : StrictConvexOn 𝕜 s f)
     linarith
   set a := (z - y) / (z - x)
   set b := (y - x) / (z - x)
-  have hy : a • x + b • z = y := by
-    field_simp
-    rw [div_eq_iff] <;> [ring; linarith]
+  have hy : a • x + b • z = y := by field_simp; ring
   have key :=
     hf.2 hx hz hxz' (div_pos hyz hxz) (div_pos hxy hxz)
-      (show a + b = 1 by
-        field_simp
-        rw [div_eq_iff] <;> [ring; linarith])
+      (show a + b = 1 by field_simp)
   rw [hy] at key
   replace key := mul_lt_mul_of_pos_left key hxz
-  field_simp [hxy.ne', hyz.ne', hxz.ne', mul_comm (z - x) _] at key ⊢
+  field_simp [mul_comm (z - x) _] at key ⊢
   rw [div_lt_div_right]
   · linarith
   · nlinarith
@@ -247,12 +239,12 @@ theorem ConvexOn.secant_mono_aux1 (hf : ConvexOn 𝕜 s f) {x y z : 𝕜} (hx :
     _ ≤ (z - y) / (z - x) * f x + (y - x) / (z - x) * f z := hf.2 hx hz ha hb ?_
     _ = ((z - y) * f x + (y - x) * f z) / (z - x) := ?_
   · congr 1
-    field_simp [hxy'.ne', hyz'.ne', hxz'.ne']
+    field_simp
     ring
   · -- Porting note: this `show` wasn't needed in Lean 3
     show (z - y) / (z - x) + (y - x) / (z - x) = 1
-    field_simp [hxy'.ne', hyz'.ne', hxz'.ne']
-  · field_simp [hxy'.ne', hyz'.ne', hxz'.ne']
+    field_simp
+  · field_simp
 #align convex_on.secant_mono_aux1 ConvexOn.secant_mono_aux1
 
 theorem ConvexOn.secant_mono_aux2 (hf : ConvexOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s)
@@ -297,12 +289,12 @@ theorem StrictConvexOn.secant_strict_mono_aux1 (hf : StrictConvexOn 𝕜 s f) {x
     _ < (z - y) / (z - x) * f x + (y - x) / (z - x) * f z := (hf.2 hx hz (by linarith) ha hb ?_)
     _ = ((z - y) * f x + (y - x) * f z) / (z - x) := ?_
   · congr 1
-    field_simp [hxy'.ne', hyz'.ne', hxz'.ne']
+    field_simp
     ring
   · -- Porting note: this `show` wasn't needed in Lean 3
     show (z - y) / (z - x) + (y - x) / (z - x) = 1
-    field_simp [hxy'.ne', hyz'.ne', hxz'.ne']
-  · field_simp [hxy'.ne', hyz'.ne', hxz'.ne']
+    field_simp
+  · field_simp
 #align strict_convex_on.secant_strict_mono_aux1 StrictConvexOn.secant_strict_mono_aux1
 
 theorem StrictConvexOn.secant_strict_mono_aux2 (hf : StrictConvexOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s)

Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean

@@ -130,7 +130,7 @@ theorem convexOn_zpow : ∀ m : ℤ, ConvexOn ℝ (Ioi 0) fun x : ℝ => x ^ m
     simp_rw [zpow_negSucc]
     refine' ⟨convex_Ioi _, _⟩
     rintro a (ha : 0 < a) b (hb : 0 < b) μ ν hμ hν h
-    field_simp [ha.ne', hb.ne']
+    field_simp
     rw [div_le_div_iff]
     · -- Porting note: added type ascription to LHS
       calc
@@ -168,7 +168,7 @@ theorem strictConcaveOn_log_Ioi : StrictConcaveOn ℝ (Ioi 0) log := by
     calc
       log z - log y = log (z / y) := by rw [← log_div hz.ne' hy.ne']
       _ < z / y - 1 := (log_lt_sub_one_of_pos hyz' hyz'')
-      _ = y⁻¹ * (z - y) := by field_simp [hy.ne']
+      _ = y⁻¹ * (z - y) := by field_simp
   · have h : 0 < y - x := by linarith
     rw [lt_div_iff h]
     have hxy' : 0 < x / y := by positivity
@@ -177,7 +177,7 @@ theorem strictConcaveOn_log_Ioi : StrictConcaveOn ℝ (Ioi 0) log := by
       rw [div_eq_one_iff_eq hy.ne'] at h
       simp [h]
     calc
-      y⁻¹ * (y - x) = 1 - x / y := by field_simp [hy.ne']
+      y⁻¹ * (y - x) = 1 - x / y := by field_simp
       _ < -log (x / y) := by linarith [log_lt_sub_one_of_pos hxy' hxy'']
       _ = -(log x - log y) := by rw [log_div hx.ne' hy.ne']
       _ = log y - log x := by ring
@@ -204,16 +204,16 @@ theorem one_add_mul_self_lt_rpow_one_add {s : ℝ} (hs : -1 ≤ s) (hs' : s ≠
     -- but now Lean doesn't guess we are talking about `1` fast enough.
     haveI : (1 : ℝ) ∈ Ioi 0 := zero_lt_one
     convert strictConcaveOn_log_Ioi.secant_strict_mono this hs2 hs1 hs4 hs3 _ using 1
-    · field_simp [log_one]
-    · field_simp [log_one]
+    · field_simp
+    · field_simp
     · nlinarith
   · rw [← div_lt_iff hp, ← div_lt_div_right hs']
     -- Porting note: previously we could write `zero_lt_one` inline,
     -- but now Lean doesn't guess we are talking about `1` fast enough.
     haveI : (1 : ℝ) ∈ Ioi 0 := zero_lt_one
     convert strictConcaveOn_log_Ioi.secant_strict_mono this hs1 hs2 hs3 hs4 _ using 1
-    · field_simp [log_one, hp.ne']
-    · field_simp [log_one]
+    · field_simp
+    · field_simp
     · nlinarith
 #align one_add_mul_self_lt_rpow_one_add one_add_mul_self_lt_rpow_one_add
 
@@ -251,10 +251,10 @@ theorem strictConvexOn_rpow {p : ℝ} (hp : 1 < p) : StrictConvexOn ℝ (Ici 0)
     convert this using 1
     · have H : (x / y) ^ p = x ^ p / y ^ p := div_rpow hx hy.le _
       ring_nf at H ⊢
-      field_simp [hy.ne', hy'.ne'] at H ⊢
+      field_simp at H ⊢
       linear_combination H
     · ring_nf at H1 ⊢
-      field_simp [hy.ne', hy'.ne']
+      field_simp
       linear_combination p * (-y + x) * H1
   · have hyz' : 0 < z - y := by linarith only [hyz]
     have hyz'' : 1 < z / y := by rwa [one_lt_div hy]
@@ -265,11 +265,11 @@ theorem strictConvexOn_rpow {p : ℝ} (hp : 1 < p) : StrictConvexOn ℝ (Ici 0)
     rw [lt_div_iff hyz', ← div_lt_div_right hy']
     convert this using 1
     · ring_nf at H1 ⊢
-      field_simp [hy.ne', hy'.ne'] at H1 ⊢
+      field_simp at H1 ⊢
       linear_combination p * (y - z) * y ^ p * H1
     · have H : (z / y) ^ p = z ^ p / y ^ p := div_rpow hz hy.le _
       ring_nf at H ⊢
-      field_simp [hy.ne', hy'.ne'] at H ⊢
+      field_simp at H ⊢
       linear_combination -H
 #align strict_convex_on_rpow strictConvexOn_rpow
 

Mathlib/Data/Complex/Exponential.lean

@@ -907,7 +907,6 @@ theorem cos_sub_cos : cos x - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)
 #align complex.cos_sub_cos Complex.cos_sub_cos
 
 theorem cos_add_cos : cos x + cos y = 2 * cos ((x + y) / 2) * cos ((x - y) / 2) := by
-  have h2 : (2 : ℂ) ≠ 0 := by norm_num
   calc
     cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) := ?_
     _ =
@@ -916,7 +915,7 @@ theorem cos_add_cos : cos x + cos y = 2 * cos ((x + y) / 2) * cos ((x - y) / 2)
       ?_
     _ = 2 * cos ((x + y) / 2) * cos ((x - y) / 2) := ?_
 
-  · congr <;> field_simp [h2]
+  · congr <;> field_simp
   · rw [cos_add, cos_sub]
   ring
 #align complex.cos_add_cos Complex.cos_add_cos
@@ -1046,9 +1045,8 @@ theorem sin_sq : sin x ^ 2 = 1 - cos x ^ 2 := by rw [← sin_sq_add_cos_sq x, ad
 #align complex.sin_sq Complex.sin_sq
 
 theorem inv_one_add_tan_sq {x : ℂ} (hx : cos x ≠ 0) : (1 + tan x ^ 2)⁻¹ = cos x ^ 2 := by
-  have : cos x ^ 2 ≠ 0 := pow_ne_zero 2 hx
   rw [tan_eq_sin_div_cos, div_pow]
-  field_simp [this]
+  field_simp
 #align complex.inv_one_add_tan_sq Complex.inv_one_add_tan_sq
 
 theorem tan_sq_div_one_add_tan_sq {x : ℂ} (hx : cos x ≠ 0) :
@@ -2001,7 +1999,7 @@ theorem one_sub_div_pow_le_exp_neg {n : ℕ} {t : ℝ} (ht' : t ≤ n) : (1 - t
   · abel
   · rw [← Real.exp_nat_mul]
     congr 1
-    field_simp [(Nat.cast_ne_zero (R := ℝ)).mpr hn]
+    field_simp
     ring_nf
   · rwa [add_comm, ← sub_eq_add_neg, sub_nonneg, div_le_one]
     positivity

Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean

@@ -262,7 +262,7 @@ theorem exists_frobenius_solution_fractionRing_aux (m n : ℕ) (r' q' : 𝕎 k)
     simpa only [Ne.def, map_zero] using
       (IsFractionRing.injective (𝕎 k) (FractionRing (𝕎 k))).ne hq'''
   rw [zpow_sub₀ (FractionRing.p_nonzero p k)]
-  field_simp [FractionRing.p_nonzero p k]
+  field_simp -- [FractionRing.p_nonzero p k]
   simp only [IsFractionRing.fieldEquivOfRingEquiv, IsLocalization.ringEquivOfRingEquiv_eq,
     RingEquiv.coe_ofBijective]
   convert congr_arg (fun x => algebraMap (𝕎 k) (FractionRing (𝕎 k)) x) key using 1