chore: backport a few misc changes from #11070 to master (#11079)

A random collection of changes, backporting from the upcoming Lean bump.
- squeeze one simp
- backport one more simp change (which probably was missed in the previous backports)
- rewrite the `field_simp` in SolutionOfCubic: with the upcoming Lean bump, this would become **very** slow

Similar to #10996 and #11001.

Archive/Wiedijk100Theorems/SolutionOfCubic.lean

@@ -101,7 +101,6 @@ theorem cubic_eq_zero_iff (ha : a ≠ 0) (hω : IsPrimitiveRoot ω 3)
     a * x ^ 3 + b * x ^ 2 + c * x + d = 0 ↔
       x = s - t - b / (3 * a) ∨
         x = s * ω - t * ω ^ 2 - b / (3 * a) ∨ x = s * ω ^ 2 - t * ω - b / (3 * a) := by
-  have hi2 : (2 : K) ≠ 0 := nonzero_of_invertible _
   have hi3 : (3 : K) ≠ 0 := nonzero_of_invertible _
   have h9 : (9 : K) = 3 ^ 2 := by norm_num
   have h54 : (54 : K) = 2 * 3 ^ 3 := by norm_num
@@ -110,7 +109,9 @@ theorem cubic_eq_zero_iff (ha : a ≠ 0) (hω : IsPrimitiveRoot ω 3)
   have h₂ : ∀ x, a * x = 0 ↔ x = 0 := by intro x; simp [ha]
   have hp' : p = (3 * (c / a) - (b / a) ^ 2) / 9 := by field_simp [hp, h9]; ring_nf
   have hq' : q = (9 * (b / a) * (c / a) - 2 * (b / a) ^ 3 - 27 * (d / a)) / 54 := by
-    field_simp [hq, h54]; ring_nf
+    rw [hq, h54]
+    simp [field_simps, ha]
+    ring_nf
   rw [h₁, h₂, cubic_monic_eq_zero_iff (b / a) (c / a) (d / a) hω hp' hp_nonzero hq' hr hs3 ht x]
   have h₄ :=
     calc

Mathlib/Analysis/Calculus/Taylor.lean

@@ -284,7 +284,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 [xy_ne y hy, Nat.factorial];  ring
+  field_simp [xy_ne y hy, Nat.factorial]; ring
 #align taylor_mean_remainder_lagrange taylor_mean_remainder_lagrange
 
 /-- **Taylor's theorem** with the Cauchy form of the remainder.

Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean

@@ -220,7 +220,7 @@ theorem iff_isSplitMono_eq_zero {X Y : C} (f : X ⟶ Y) [IsSplitMono f] : IsZero
     rw [← Category.id_comp f, h, zero_comp]
   · intro h
     rw [← IsSplitMono.id f]
-    simp [h]
+    simp only [h, zero_comp]
 #align category_theory.limits.is_zero.iff_is_split_mono_eq_zero CategoryTheory.Limits.IsZero.iff_isSplitMono_eq_zero
 
 theorem iff_isSplitEpi_eq_zero {X Y : C} (f : X ⟶ Y) [IsSplitEpi f] : IsZero Y ↔ f = 0 := by

Mathlib/MeasureTheory/Integral/SetToL1.lean

@@ -1157,8 +1157,7 @@ theorem setToL1_mono_left' {T T' : Set α → E →L[ℝ] G''} {C C' : ℝ}
     (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C')
     (hTT' : ∀ s, MeasurableSet s → μ s < ∞ → ∀ x, T s x ≤ T' s x) (f : α →₁[μ] E) :
     setToL1 hT f ≤ setToL1 hT' f := by
-  induction f using Lp.induction with
-  | hp_ne_top h => exact one_ne_top h
+  induction f using Lp.induction (hp_ne_top := one_ne_top) with
   | @h_ind c s hs hμs =>
     rw [setToL1_simpleFunc_indicatorConst hT hs hμs, setToL1_simpleFunc_indicatorConst hT' hs hμs]
     exact hTT' s hs hμs c

Mathlib/Topology/Category/TopCat/EffectiveEpi.lean

@@ -69,7 +69,7 @@ theorem effectiveEpi_iff_quotientMap {B X : TopCat.{u}} (π : X ⟶ B) :
   /- The key to proving that the coequalizer has the quotient topology is
     `TopCat.coequalizer_isOpen_iff` which characterises the open sets in a coequalizer. -/
   · ext U
-    have : π ≫ i.hom = colimit.ι F WalkingParallelPair.one := by simp [← Iso.eq_comp_inv]
+    have : π ≫ i.hom = colimit.ι F WalkingParallelPair.one := by simp [i, ← Iso.eq_comp_inv]
     rw [isOpen_coinduced (f := (homeoOfIso i ∘ π)), coequalizer_isOpen_iff _ U, ← this]
     rfl