[Merged by Bors] - field_simp: Use positivity as a discharger

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/Imo2008Q2.lean

@@ -68,10 +68,7 @@ theorem imo2008_q2b : Set.Infinite rationalSolutions := by
     simp only [Set.mem_setOf_eq] at hs_in_W ⊢
     rcases hs_in_W with ⟨x, y, z, h₁, t, ht_gt_zero, hx_t, hy_t, hz_t⟩
     use x, y, z
-    have ht_ne_zero : t ≠ 0 := ne_of_gt ht_gt_zero
-    have ht1_ne_zero : t + 1 ≠ 0; linarith [ht_gt_zero]
     have key_gt_zero : t ^ 2 + t + 1 > 0; linarith [pow_pos ht_gt_zero 2, ht_gt_zero]
-    have key_ne_zero : t ^ 2 + t + 1 ≠ 0 := ne_of_gt key_gt_zero
     have h₂ : x ≠ 1 := by rw [hx_t]; field_simp; linarith [key_gt_zero]
     have h₃ : y ≠ 1 := by rw [hy_t]; field_simp; linarith [key_gt_zero]
     have h₄ : z ≠ 1 := by rw [hz_t]; linarith [key_gt_zero]

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

Archive/Imo/Imo2013Q5.lean

@@ -60,7 +60,7 @@ theorem le_of_all_pow_lt_succ {x y : ℝ} (hx : 1 < x) (hy : 1 < y)
   have hNp : 0 < N := by exact_mod_cast (one_div_pos.mpr hxmy).trans hN
   have :=
     calc
-      1 = (x - y) * (1 / (x - y)) := by field_simp [ne_of_gt hxmy]
+      1 = (x - y) * (1 / (x - y)) := by field_simp
       _ < (x - y) * N := by gcongr
       _ ≤ x ^ N - y ^ N := hn N hNp
   linarith [h N hNp]

Archive/Wiedijk100Theorems/AreaOfACircle.lean

@@ -111,13 +111,13 @@ theorem area_disc : volume (disc r) = NNReal.pi * r ^ 2 := by
               ((hasDerivAt_const x (r : ℝ)⁻¹).mul (hasDerivAt_id' x)))).add
         ((hasDerivAt_id' x).mul ((((hasDerivAt_id' x).pow 2).const_sub ((r : ℝ) ^ 2)).sqrt _))
       using 1
-    · have h : sqrt ((1 : ℝ) - x ^ 2 / (r : ℝ) ^ 2) * r = sqrt ((r : ℝ) ^ 2 - x ^ 2) := by
-        rw [← sqrt_sq hle, ← sqrt_mul, sub_mul, sqrt_sq hle, mul_comm_div,
-          div_self (pow_ne_zero 2 hlt.ne'), one_mul, mul_one]
-        simpa [sqrt_sq hle, div_le_one (pow_pos hlt 2)] using sq_le_sq' hx1.le hx2.le
+    · have h₁ : (r:ℝ) ^ 2 - x ^ 2 > 0 := sub_pos_of_lt (sq_lt_sq' hx1 hx2)
+      have h : sqrt ((r:ℝ) ^ 2 - x ^ 2) ^ 3 = ((r:ℝ) ^ 2 - x ^ 2) * sqrt ((r: ℝ) ^ 2 - x ^ 2) := by
+        rw [pow_three, ← mul_assoc, mul_self_sqrt (by positivity)]
       field_simp
-      rw [h, mul_left_comm, ← sq, neg_mul_eq_mul_neg, mul_div_mul_left (-x ^ 2) _ two_ne_zero,
-        add_left_comm, div_add_div_same, ← sub_eq_add_neg, div_sqrt, two_mul]
+      ring_nf
+      rw [h]
+      ring
     · suffices -(1 : ℝ) < (r : ℝ)⁻¹ * x by exact this.ne'
       calc
         -(1 : ℝ) = (r : ℝ)⁻¹ * -r := by simp [inv_mul_cancel hlt.ne']

Archive/Wiedijk100Theorems/InverseTriangleSum.lean

@@ -35,6 +35,6 @@ theorem Theorem100.inverse_triangle_sum :
   simp_rw [if_neg (Nat.succ_ne_zero _), Nat.succ_eq_add_one]
   have A : (n + 1 + 1 : ℚ) ≠ 0 := by norm_cast; norm_num
   push_cast
-  field_simp [Nat.cast_add_one_ne_zero]
+  field_simp
   ring
 #align theorem_100.inverse_triangle_sum Theorem100.inverse_triangle_sum

Mathlib/Algebra/Order/ToIntervalMod.lean

@@ -1015,7 +1015,7 @@ theorem toIcoDiv_zero_one (b : α) : toIcoDiv (zero_lt_one' α) 0 b = ⌊b⌋ :=
 theorem toIcoMod_eq_add_fract_mul (a b : α) :
     toIcoMod hp a b = a + Int.fract ((b - a) / p) * p := by
   rw [toIcoMod, toIcoDiv_eq_floor, Int.fract]
-  field_simp [hp.ne.symm]
+  field_simp
   ring
 #align to_Ico_mod_eq_add_fract_mul toIcoMod_eq_add_fract_mul
 
@@ -1026,7 +1026,7 @@ theorem toIcoMod_eq_fract_mul (b : α) : toIcoMod hp 0 b = Int.fract (b / p) * p
 theorem toIocMod_eq_sub_fract_mul (a b : α) :
     toIocMod hp a b = a + p - Int.fract ((a + p - b) / p) * p := by
   rw [toIocMod, toIocDiv_eq_neg_floor, Int.fract]
-  field_simp [hp.ne.symm]
+  field_simp
   ring
 #align to_Ioc_mod_eq_sub_fract_mul toIocMod_eq_sub_fract_mul
 

Mathlib/Algebra/QuadraticDiscriminant.lean

@@ -134,7 +134,7 @@ theorem discrim_le_zero (h : ∀ x : K, 0 ≤ a * x * x + b * x + c) : discrim a
   -- if a > 0
   · have ha' : 0 ≤ 4 * a := mul_nonneg zero_le_four ha.le
     convert neg_nonpos.2 (mul_nonneg ha' (h (-b / (2 * a)))) using 1
-    field_simp [ha.ne']
+    field_simp
     ring
 #align discrim_le_zero discrim_le_zero
 

Mathlib/Analysis/Analytic/Basic.lean

@@ -202,7 +202,7 @@ theorem isLittleO_of_lt_radius (h : ↑r < p.radius) :
   refine' ⟨_, rt, C, Or.inr zero_lt_one, fun n => _⟩
   calc
     |‖p n‖ * (r : ℝ) ^ n| = ‖p n‖ * (t : ℝ) ^ n * (r / t : ℝ) ^ n := by
-      field_simp [mul_right_comm, abs_mul, this.ne']
+      field_simp [mul_right_comm, abs_mul]
     _ ≤ C * (r / t : ℝ) ^ n := by gcongr; apply hC
 #align formal_multilinear_series.is_o_of_lt_radius FormalMultilinearSeries.isLittleO_of_lt_radius
 
@@ -670,7 +670,7 @@ theorem HasFPowerSeriesOnBall.uniform_geometric_approx' {r' : ℝ≥0}
   calc
     ‖(p n) fun _ : Fin n => y‖
     _ ≤ ‖p n‖ * ∏ _i : Fin n, ‖y‖ := ContinuousMultilinearMap.le_op_norm _ _
-    _ = ‖p n‖ * (r' : ℝ) ^ n * (‖y‖ / r') ^ n := by field_simp [hr'0.ne', mul_right_comm]
+    _ = ‖p n‖ * (r' : ℝ) ^ n * (‖y‖ / r') ^ n := by field_simp [mul_right_comm]
     _ ≤ C * a ^ n * (‖y‖ / r') ^ n := by gcongr ?_ * _; apply hp
     _ ≤ C * (a * (‖y‖ / r')) ^ n := by rw [mul_pow, mul_assoc]
 #align has_fpower_series_on_ball.uniform_geometric_approx' HasFPowerSeriesOnBall.uniform_geometric_approx'
@@ -758,7 +758,7 @@ theorem HasFPowerSeriesOnBall.isBigO_image_sub_image_sub_deriv_principal
         _ = B n := by
           -- porting note: in the original, `B` was in the `field_simp`, but now Lean does not
           -- accept it. The current proof works in Lean 4, but does not in Lean 3.
-          field_simp [pow_succ, hr'0.ne']
+          field_simp [pow_succ]
           simp only [mul_assoc, mul_comm, mul_left_comm]
     have hBL : HasSum B (L y) := by
       apply HasSum.mul_left

Mathlib/Analysis/BoxIntegral/Basic.lean

@@ -603,7 +603,7 @@ theorem dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq (h : Integra
           dist (∑ J in π₀.boxes, integralSum f vol (πi J)) (∑ J in π₀.boxes, integral J l f vol) :=
       dist_triangle _ _ _
     _ ≤ ε + δ' + ∑ _J in π₀.boxes, δ' := (add_le_add this (dist_sum_sum_le_of_le _ hπiδ'))
-    _ = ε + δ := by field_simp [H0.ne']; ring
+    _ = ε + δ := by field_simp; ring
 #align box_integral.integrable.dist_integral_sum_sum_integral_le_of_mem_base_set_of_Union_eq BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq
 
 /-- **Henstock-Sacks inequality**. Let `r : ℝⁿ → (0, ∞)` be a function such that for any tagged

Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean

@@ -139,7 +139,6 @@ theorem IsOpen.exists_smooth_support_eq {s : Set E} (hs : IsOpen s) :
       exact ⟨R, fun x => hR (mem_range_self _)⟩
     choose R hR using this
     let M := max (((Finset.range (n + 1)).image R).max' (by simp)) 1
-    have M_pos : 0 < M := zero_lt_one.trans_le (le_max_right _ _)
     have δnpos : 0 < δ n := δpos n
     have IR : ∀ i ≤ n, R i ≤ M := by
       intro i hi
@@ -157,7 +156,7 @@ theorem IsOpen.exists_smooth_support_eq {s : Set E} (hs : IsOpen s) :
       _ = M⁻¹ * δ n * ‖iteratedFDeriv ℝ i (g n) x‖ := by
         rw [norm_smul, Real.norm_of_nonneg]; positivity
       _ ≤ M⁻¹ * δ n * M := (mul_le_mul_of_nonneg_left ((hR i x).trans (IR i hi)) (by positivity))
-      _ = δ n := by field_simp [M_pos.ne']
+      _ = δ n := by field_simp
   choose r rpos hr using this
   have S : ∀ x, Summable fun n => (r n • g n) x := by
     intro x
@@ -328,7 +327,7 @@ variable (E)
 theorem w_integral {D : ℝ} (Dpos : 0 < D) : ∫ x : E, w D x ∂μ = 1 := by
   simp_rw [w, integral_smul]
   rw [integral_comp_inv_smul_of_nonneg μ (u : E → ℝ) Dpos.le, abs_of_nonneg Dpos.le, mul_comm]
-  field_simp [Dpos.ne', (u_int_pos E).ne']
+  field_simp [(u_int_pos E).ne']
 #align exists_cont_diff_bump_base.W_integral ExistsContDiffBumpBase.w_integral
 
 theorem w_support {D : ℝ} (Dpos : 0 < D) : support (w D : E → ℝ) = ball 0 D := by
@@ -557,16 +556,15 @@ instance (priority := 100) {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E
         calc
           2 / (R + 1) * ‖x‖ ≤ 2 / (R + 1) * 1 :=
             mul_le_mul_of_nonneg_left hx (div_nonneg zero_le_two A.le)
-          _ = 1 - (R - 1) / (R + 1) := by field_simp [A.ne']; ring
+          _ = 1 - (R - 1) / (R + 1) := by field_simp; ring
       support := fun R hR => by
         have A : 0 < (R + 1) / 2 := by linarith
         have A' : 0 < R + 1 := by linarith
         have C : (R - 1) / (R + 1) < 1 := by apply (div_lt_one _).2 <;> linarith
         simp only [hR, if_true, support_comp_inv_smul₀ A.ne', y_support _ (IR R hR) C,
           _root_.smul_ball A.ne', Real.norm_of_nonneg A.le, smul_zero]
         refine' congr (congr_arg ball (Eq.refl 0)) _
-        field_simp [A'.ne']
-        ring }
+        field_simp; ring }
 
 end ExistsContDiffBumpBase
 

Mathlib/Analysis/Calculus/Taylor.lean

@@ -162,15 +162,11 @@ theorem hasDerivWithinAt_taylor_coeff_within {f : ℝ → E} {x y : ℝ} {k : 
       (-((k ! : ℝ)⁻¹ * (x - y) ^ k)) t y := by
     -- Commuting the factors:
     have : -((k ! : ℝ)⁻¹ * (x - y) ^ k) = ((k + 1 : ℝ) * k !)⁻¹ * (-(k + 1) * (x - y) ^ k) := by
-      field_simp [k.factorial_ne_zero]
-      -- Porting note: was `ring_nf`
-      rw [mul_div_mul_right, ← neg_add_rev, neg_mul, neg_div, mul_div_cancel_left]
-      · exact k.cast_add_one_ne_zero
-      · simp [k.factorial_ne_zero]
+      field_simp; ring
     rw [this]
     exact (monomial_has_deriv_aux y x _).hasDerivWithinAt.const_mul _
   convert this.smul hf using 1
-  field_simp [Nat.cast_add_one_ne_zero k, Nat.factorial_ne_zero k]
+  field_simp
   rw [neg_div, neg_smul, sub_eq_add_neg]
 #align has_deriv_within_at_taylor_coeff_within hasDerivWithinAt_taylor_coeff_within
 
@@ -256,7 +252,7 @@ theorem taylor_mean_remainder {f : ℝ → ℝ} {g g' : ℝ → ℝ} {x x₀ : 
   simp only [taylorWithinEval_self] at h
   rw [mul_comm, ← div_left_inj' (g'_ne y hy), mul_div_cancel _ (g'_ne y hy)] at h
   rw [← h]
-  field_simp [g'_ne y hy, n.factorial_ne_zero]
+  field_simp [g'_ne y hy]
   ring
 #align taylor_mean_remainder taylor_mean_remainder
 
@@ -289,16 +285,7 @@ theorem taylor_mean_remainder_lagrange {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ
   use y, hy
   simp only [sub_self, zero_pow', Ne.def, Nat.succ_ne_zero, not_false_iff, zero_sub, mul_neg] at h
   rw [h, neg_div, ← div_neg, neg_mul, neg_neg]
-  field_simp
-  -- Porting note: was `ring`
-  conv_lhs =>
-    arg 2
-    rw [← mul_assoc, mul_comm]
-  rw [mul_assoc, mul_div_mul_left _ _ (xy_ne y hy)]
-  conv_lhs =>
-    arg 2
-    rw [mul_comm]
-  nth_rw 1 [mul_comm]
+  field_simp [xy_ne y hy];  ring
 #align taylor_mean_remainder_lagrange taylor_mean_remainder_lagrange
 
 /-- **Taylor's theorem** with the Cauchy form of the remainder.

Mathlib/Analysis/Complex/LocallyUniformLimit.lean

@@ -61,7 +61,7 @@ theorem norm_cderiv_le (hr : 0 < r) (hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M)
   have h2 := circleIntegral.norm_integral_le_of_norm_le_const hr.le h1
   simp only [cderiv, norm_smul]
   refine' (mul_le_mul le_rfl h2 (norm_nonneg _) (norm_nonneg _)).trans (le_of_eq _)
-  field_simp [_root_.abs_of_nonneg Real.pi_pos.le, Real.pi_pos.ne.symm, hr.ne.symm]
+  field_simp [_root_.abs_of_nonneg Real.pi_pos.le]
   ring
 #align complex.norm_cderiv_le Complex.norm_cderiv_le
 

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)