bump to nightly-2024-02-14-08

mathlib commit leanprover-community/mathlib@65a1391

Mathbin/Algebra/GcdMonoid/Basic.lean

@@ -1059,8 +1059,8 @@ end Lcm
 
 namespace GCDMonoid
 
-#print GCDMonoid.prime_of_irreducible /-
-theorem prime_of_irreducible [GCDMonoid α] {x : α} (hi : Irreducible x) : Prime x :=
+#print Irreducible.prime /-
+theorem prime [GCDMonoid α] {x : α} (hi : Irreducible x) : Prime x :=
   ⟨hi.NeZero,
     ⟨hi.1, fun a b h => by
       cases' gcd_dvd_left x a with y hy
@@ -1071,13 +1071,13 @@ theorem prime_of_irreducible [GCDMonoid α] {x : α} (hi : Irreducible x) : Prim
       · left
         rw [hy]
         exact dvd_trans (associated_mul_unit_left _ _ hu).Dvd (gcd_dvd_right x a)⟩⟩
-#align gcd_monoid.prime_of_irreducible GCDMonoid.prime_of_irreducible
+#align gcd_monoid.prime_of_irreducible Irreducible.prime
 -/
 
-#print GCDMonoid.irreducible_iff_prime /-
+#print irreducible_iff_prime /-
 theorem irreducible_iff_prime [GCDMonoid α] {p : α} : Irreducible p ↔ Prime p :=
-  ⟨prime_of_irreducible, Prime.irreducible⟩
-#align gcd_monoid.irreducible_iff_prime GCDMonoid.irreducible_iff_prime
+  ⟨prime, Prime.irreducible⟩
+#align gcd_monoid.irreducible_iff_prime irreducible_iff_prime
 -/
 
 end GCDMonoid

Mathbin/Algebra/Order/Nonneg/Ring.lean

@@ -86,11 +86,11 @@ instance distribLattice [DistribLattice α] {a : α} : DistribLattice { x : α /
 #align nonneg.distrib_lattice Nonneg.distribLattice
 -/
 
-#print Nonneg.densely_ordered /-
-instance densely_ordered [Preorder α] [DenselyOrdered α] {a : α} :
+#print Nonneg.instDenselyOrdered /-
+instance instDenselyOrdered [Preorder α] [DenselyOrdered α] {a : α} :
     DenselyOrdered { x : α // a ≤ x } :=
   show DenselyOrdered (Ici a) from Set.denselyOrdered
-#align nonneg.densely_ordered Nonneg.densely_ordered
+#align nonneg.densely_ordered Nonneg.instDenselyOrdered
 -/
 
 #print Nonneg.conditionallyCompleteLinearOrder /-

Mathbin/Algebra/Squarefree.lean

@@ -301,13 +301,13 @@ theorem squarefree_iff_nodup_normalizedFactors [NormalizationMonoid R] [Decidabl
 #align unique_factorization_monoid.squarefree_iff_nodup_normalized_factors UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors
 -/
 
-#print UniqueFactorizationMonoid.dvd_pow_iff_dvd_of_squarefree /-
-theorem dvd_pow_iff_dvd_of_squarefree {x y : R} {n : ℕ} (hsq : Squarefree x) (h0 : n ≠ 0) :
-    x ∣ y ^ n ↔ x ∣ y := by
+#print Squarefree.dvd_pow_iff_dvd /-
+theorem dvd_pow_iff_dvd {x y : R} {n : ℕ} (hsq : Squarefree x) (h0 : n ≠ 0) : x ∣ y ^ n ↔ x ∣ y :=
+  by
   classical
   haveI := UniqueFactorizationMonoid.toGCDMonoid R
   exact ⟨hsq.is_radical n y, fun h => h.pow h0⟩
-#align unique_factorization_monoid.dvd_pow_iff_dvd_of_squarefree UniqueFactorizationMonoid.dvd_pow_iff_dvd_of_squarefree
+#align unique_factorization_monoid.dvd_pow_iff_dvd_of_squarefree Squarefree.dvd_pow_iff_dvd
 -/
 
 end UniqueFactorizationMonoid

Mathbin/AlgebraicGeometry/EllipticCurve/Weierstrass.lean

@@ -769,7 +769,7 @@ open Ideal
 
 instance [IsDomain R] [NormalizedGCDMonoid R] : IsDomain W.CoordinateRing :=
   (Quotient.isDomain_iff_prime _).mpr <| by
-    simpa only [span_singleton_prime W.polynomial_ne_zero, ← GCDMonoid.irreducible_iff_prime] using
+    simpa only [span_singleton_prime W.polynomial_ne_zero, ← irreducible_iff_prime] using
       W.irreducible_polynomial
 
 #print WeierstrassCurve.Affine.CoordinateRing.instIsDomainCoordinateRing_of_Field /-

Mathbin/Analysis/InnerProductSpace/GramSchmidtOrtho.lean

@@ -223,7 +223,7 @@ theorem gramSchmidt_of_orthogonal {f : ι → E} (hf : Pairwise fun i j => ⟪f
   · congr
     apply Finset.sum_eq_zero
     intro j hj
-    rw [coe_eq_zero]
+    rw [NNReal.coe_eq_zero]
     suffices span 𝕜 (f '' Set.Iic j) ⟂ 𝕜 ∙ f i
       by
       apply orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero

Mathbin/Analysis/MeanInequalities.lean

@@ -236,7 +236,7 @@ namespace Real
 theorem geom_mean_le_arith_mean2_weighted {w₁ w₂ p₁ p₂ : ℝ} (hw₁ : 0 ≤ w₁) (hw₂ : 0 ≤ w₂)
     (hp₁ : 0 ≤ p₁) (hp₂ : 0 ≤ p₂) (hw : w₁ + w₂ = 1) : p₁ ^ w₁ * p₂ ^ w₂ ≤ w₁ * p₁ + w₂ * p₂ :=
   NNReal.geom_mean_le_arith_mean2_weighted ⟨w₁, hw₁⟩ ⟨w₂, hw₂⟩ ⟨p₁, hp₁⟩ ⟨p₂, hp₂⟩ <|
-    NNReal.coe_eq.1 <| by assumption
+    NNReal.coe_inj.1 <| by assumption
 #align real.geom_mean_le_arith_mean2_weighted Real.geom_mean_le_arith_mean2_weighted
 -/
 
@@ -246,7 +246,7 @@ theorem geom_mean_le_arith_mean3_weighted {w₁ w₂ w₃ p₁ p₂ p₃ : ℝ}
     p₁ ^ w₁ * p₂ ^ w₂ * p₃ ^ w₃ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃ :=
   NNReal.geom_mean_le_arith_mean3_weighted ⟨w₁, hw₁⟩ ⟨w₂, hw₂⟩ ⟨w₃, hw₃⟩ ⟨p₁, hp₁⟩ ⟨p₂, hp₂⟩
       ⟨p₃, hp₃⟩ <|
-    NNReal.coe_eq.1 hw
+    NNReal.coe_inj.1 hw
 #align real.geom_mean_le_arith_mean3_weighted Real.geom_mean_le_arith_mean3_weighted
 -/
 
@@ -257,7 +257,7 @@ theorem geom_mean_le_arith_mean4_weighted {w₁ w₂ w₃ w₄ p₁ p₂ p₃ p
     p₁ ^ w₁ * p₂ ^ w₂ * p₃ ^ w₃ * p₄ ^ w₄ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃ + w₄ * p₄ :=
   NNReal.geom_mean_le_arith_mean4_weighted ⟨w₁, hw₁⟩ ⟨w₂, hw₂⟩ ⟨w₃, hw₃⟩ ⟨w₄, hw₄⟩ ⟨p₁, hp₁⟩
       ⟨p₂, hp₂⟩ ⟨p₃, hp₃⟩ ⟨p₄, hp₄⟩ <|
-    NNReal.coe_eq.1 <| by assumption
+    NNReal.coe_inj.1 <| by assumption
 #align real.geom_mean_le_arith_mean4_weighted Real.geom_mean_le_arith_mean4_weighted
 -/
 
@@ -303,7 +303,7 @@ namespace NNReal
 witnesses of `0 ≤ p` and `0 ≤ q` for the denominators.  -/
 theorem young_inequality (a b : ℝ≥0) {p q : ℝ≥0} (hp : 1 < p) (hpq : 1 / p + 1 / q = 1) :
     a * b ≤ a ^ (p : ℝ) / p + b ^ (q : ℝ) / q :=
-  Real.young_inequality_of_nonneg a.coe_nonneg b.coe_nonneg ⟨hp, NNReal.coe_eq.2 hpq⟩
+  Real.young_inequality_of_nonneg a.coe_nonneg b.coe_nonneg ⟨hp, NNReal.coe_inj.2 hpq⟩
 #align nnreal.young_inequality NNReal.young_inequality
 -/
 

Mathbin/Analysis/Normed/Field/Basic.lean

@@ -730,8 +730,8 @@ theorem dist_inv_inv₀ {z w : α} (hz : z ≠ 0) (hw : w ≠ 0) : dist z⁻¹ w
 
 #print nndist_inv_inv₀ /-
 theorem nndist_inv_inv₀ {z w : α} (hz : z ≠ 0) (hw : w ≠ 0) :
-    nndist z⁻¹ w⁻¹ = nndist z w / (‖z‖₊ * ‖w‖₊) := by rw [← NNReal.coe_eq];
-  simp [-NNReal.coe_eq, dist_inv_inv₀ hz hw]
+    nndist z⁻¹ w⁻¹ = nndist z w / (‖z‖₊ * ‖w‖₊) := by rw [← NNReal.coe_inj];
+  simp [-NNReal.coe_inj, dist_inv_inv₀ hz hw]
 #align nndist_inv_inv₀ nndist_inv_inv₀
 -/
 

Mathbin/Analysis/NormedSpace/OperatorNorm.lean

@@ -679,7 +679,7 @@ theorem sSup_unit_ball_eq_norm {𝕜 𝕜₂ E F : Type _} [NormedAddCommGroup E
     [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [NormedSpace 𝕜 E]
     [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) :
     sSup ((fun x => ‖f x‖) '' ball 0 1) = ‖f‖ := by
-  simpa only [NNReal.coe_sSup, Set.image_image] using NNReal.coe_eq.2 f.Sup_unit_ball_eq_nnnorm
+  simpa only [NNReal.coe_sSup, Set.image_image] using NNReal.coe_inj.2 f.Sup_unit_ball_eq_nnnorm
 #align continuous_linear_map.Sup_unit_ball_eq_norm ContinuousLinearMap.sSup_unit_ball_eq_norm
 -/
 
@@ -705,7 +705,7 @@ theorem sSup_closed_unit_ball_eq_norm {𝕜 𝕜₂ E F : Type _} [NormedAddComm
     [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) :
     sSup ((fun x => ‖f x‖) '' closedBall 0 1) = ‖f‖ := by
   simpa only [NNReal.coe_sSup, Set.image_image] using
-    NNReal.coe_eq.2 f.Sup_closed_unit_ball_eq_nnnorm
+    NNReal.coe_inj.2 f.Sup_closed_unit_ball_eq_nnnorm
 #align continuous_linear_map.Sup_closed_unit_ball_eq_norm ContinuousLinearMap.sSup_closed_unit_ball_eq_norm
 -/
 

Mathbin/Analysis/SpecialFunctions/Pow/Nnreal.lean

@@ -67,7 +67,7 @@ theorem rpow_zero (x : ℝ≥0) : x ^ (0 : ℝ) = 1 :=
 @[simp]
 theorem rpow_eq_zero_iff {x : ℝ≥0} {y : ℝ} : x ^ y = 0 ↔ x = 0 ∧ y ≠ 0 :=
   by
-  rw [← NNReal.coe_eq, coe_rpow, ← NNReal.coe_eq_zero]
+  rw [← NNReal.coe_inj, coe_rpow, ← NNReal.coe_eq_zero]
   exact Real.rpow_eq_zero_iff_of_nonneg x.2
 #align nnreal.rpow_eq_zero_iff NNReal.rpow_eq_zero_iff
 -/
@@ -366,13 +366,13 @@ theorem rpow_one_div_eq_iff {x y : ℝ≥0} {z : ℝ} (hz : z ≠ 0) : x ^ (1 /
 
 #print NNReal.pow_rpow_inv_natCast /-
 theorem pow_rpow_inv_natCast (x : ℝ≥0) {n : ℕ} (hn : n ≠ 0) : (x ^ n) ^ (n⁻¹ : ℝ) = x := by
-  rw [← NNReal.coe_eq, coe_rpow, NNReal.coe_pow]; exact Real.pow_rpow_inv_natCast x.2 hn
+  rw [← NNReal.coe_inj, coe_rpow, NNReal.coe_pow]; exact Real.pow_rpow_inv_natCast x.2 hn
 #align nnreal.pow_nat_rpow_nat_inv NNReal.pow_rpow_inv_natCast
 -/
 
 #print NNReal.rpow_inv_natCast_pow /-
 theorem rpow_inv_natCast_pow (x : ℝ≥0) {n : ℕ} (hn : n ≠ 0) : (x ^ (n⁻¹ : ℝ)) ^ n = x := by
-  rw [← NNReal.coe_eq, NNReal.coe_pow, coe_rpow]; exact Real.rpow_inv_natCast_pow x.2 hn
+  rw [← NNReal.coe_inj, NNReal.coe_pow, coe_rpow]; exact Real.rpow_inv_natCast_pow x.2 hn
 #align nnreal.rpow_nat_inv_pow_nat NNReal.rpow_inv_natCast_pow
 -/
 

Mathbin/Data/Int/Bitwise.lean

@@ -204,23 +204,23 @@ theorem bit1_ne_zero (m : ℤ) : bit1 m ≠ 0 := by simpa only [bit0_zero] using
 #align int.bit1_ne_zero Int.bit1_ne_zero
 -/
 
-#print Int.testBit_zero /-
+#print Int.testBit_bit_zero /-
 @[simp]
-theorem testBit_zero (b) : ∀ n, testBit (bit b n) 0 = b
+theorem testBit_bit_zero (b) : ∀ n, testBit (bit b n) 0 = b
   | (n : ℕ) => by rw [bit_coe_nat] <;> apply Nat.testBit_zero
   | -[n+1] => by
     rw [bit_neg_succ] <;> dsimp [test_bit] <;> rw [Nat.testBit_zero] <;> clear test_bit_zero <;>
         cases b <;>
       rfl
-#align int.test_bit_zero Int.testBit_zero
+#align int.test_bit_zero Int.testBit_bit_zero
 -/
 
-#print Int.testBit_succ /-
+#print Int.testBit_bit_succ /-
 @[simp]
-theorem testBit_succ (m b) : ∀ n, testBit (bit b n) (Nat.succ m) = testBit n m
+theorem testBit_bit_succ (m b) : ∀ n, testBit (bit b n) (Nat.succ m) = testBit n m
   | (n : ℕ) => by rw [bit_coe_nat] <;> apply Nat.testBit_succ
   | -[n+1] => by rw [bit_neg_succ] <;> dsimp [test_bit] <;> rw [Nat.testBit_succ]
-#align int.test_bit_succ Int.testBit_succ
+#align int.test_bit_succ Int.testBit_bit_succ
 -/
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:337:4: warning: unsupported (TODO): `[tacs] -/

Mathbin/Data/Multiset/Basic.lean

@@ -577,7 +577,8 @@ theorem coe_toList (s : Multiset α) : (s.toList : Multiset α) = s :=
 
 #print Multiset.toList_eq_nil /-
 @[simp]
-theorem toList_eq_nil {s : Multiset α} : s.toList = [] ↔ s = 0 := by rw [← coe_eq_zero, coe_to_list]
+theorem toList_eq_nil {s : Multiset α} : s.toList = [] ↔ s = 0 := by
+  rw [← NNReal.coe_eq_zero, coe_to_list]
 #align multiset.to_list_eq_nil Multiset.toList_eq_nil
 -/
 

Mathbin/Data/Nat/Log.lean

@@ -46,7 +46,7 @@ def log (b : ℕ) : ℕ → ℕ
 theorem log_eq_zero_iff {b n : ℕ} : log b n = 0 ↔ n < b ∨ b ≤ 1 :=
   by
   rw [log, ite_eq_right_iff]
-  simp only [Nat.succ_ne_zero, imp_false, Decidable.not_and, not_le, not_lt]
+  simp only [Nat.succ_ne_zero, imp_false, Decidable.not_and_iff_or_not_not, not_le, not_lt]
 #align nat.log_eq_zero_iff Nat.log_eq_zero_iff
 -/
 

Mathbin/Data/Polynomial/Splits.lean

@@ -133,7 +133,7 @@ theorem splits_mul {f g : K[X]} (hf : Splits i f) (hg : Splits i g) : Splits i (
   if h : (f * g).map i = 0 then Or.inl h
   else
     Or.inr fun p hp hpf =>
-      ((PrincipalIdealRing.irreducible_iff_prime.1 hp).2.2 _ _
+      ((irreducible_iff_prime.1 hp).2.2 _ _
             (show p ∣ map i f * map i g by convert hpf <;> rw [Polynomial.map_mul])).elim
         (hf.resolve_left (fun hf => by simpa [hf] using h) hp)
         (hg.resolve_left (fun hg => by simpa [hg] using h) hp)

Mathbin/Data/Real/Ennreal.lean

@@ -585,7 +585,7 @@ theorem toNNReal_eq_toNNReal_iff (x y : ℝ≥0∞) :
 #print ENNReal.toReal_eq_toReal_iff /-
 theorem toReal_eq_toReal_iff (x y : ℝ≥0∞) :
     x.toReal = y.toReal ↔ x = y ∨ x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0 := by
-  simp only [ENNReal.toReal, NNReal.coe_eq, to_nnreal_eq_to_nnreal_iff]
+  simp only [ENNReal.toReal, NNReal.coe_inj, to_nnreal_eq_to_nnreal_iff]
 #align ennreal.to_real_eq_to_real_iff ENNReal.toReal_eq_toReal_iff
 -/
 
@@ -600,7 +600,7 @@ theorem toNNReal_eq_toNNReal_iff' {x y : ℝ≥0∞} (hx : x ≠ ⊤) (hy : y 
 #print ENNReal.toReal_eq_toReal_iff' /-
 theorem toReal_eq_toReal_iff' {x y : ℝ≥0∞} (hx : x ≠ ⊤) (hy : y ≠ ⊤) :
     x.toReal = y.toReal ↔ x = y := by
-  simp only [ENNReal.toReal, NNReal.coe_eq, to_nnreal_eq_to_nnreal_iff' hx hy]
+  simp only [ENNReal.toReal, NNReal.coe_inj, to_nnreal_eq_to_nnreal_iff' hx hy]
 #align ennreal.to_real_eq_to_real_iff' ENNReal.toReal_eq_toReal_iff'
 -/
 
@@ -1258,7 +1258,7 @@ theorem lt_iff_exists_add_pos_lt : a < b ↔ ∃ r : ℝ≥0, 0 < r ∧ a + r <
   refine' ⟨d - a, tsub_pos_iff_lt.2 ad, _⟩
   rw [some_eq_coe, ← coe_add]
   convert cb
-  have : Real.toNNReal c = d := by rw [← NNReal.coe_eq, Real.coe_toNNReal _ c_nonneg]; rfl
+  have : Real.toNNReal c = d := by rw [← NNReal.coe_inj, Real.coe_toNNReal _ c_nonneg]; rfl
   rw [add_comm, this]
   exact tsub_add_cancel_of_le ad.le
 #align ennreal.lt_iff_exists_add_pos_lt ENNReal.lt_iff_exists_add_pos_lt
@@ -2746,11 +2746,11 @@ theorem exists_mem_Ico_zpow {x y : ℝ≥0∞} (hx : x ≠ 0) (h'x : x ≠ ∞)
   by
   lift x to ℝ≥0 using h'x
   lift y to ℝ≥0 using h'y
-  have A : y ≠ 0 := by simpa only [Ne.def, coe_eq_zero] using (zero_lt_one.trans hy).ne'
+  have A : y ≠ 0 := by simpa only [Ne.def, NNReal.coe_eq_zero] using (zero_lt_one.trans hy).ne'
   obtain ⟨n, hn, h'n⟩ : ∃ n : ℤ, y ^ n ≤ x ∧ x < y ^ (n + 1) :=
     by
     refine' NNReal.exists_mem_Ico_zpow _ (one_lt_coe_iff.1 hy)
-    simpa only [Ne.def, coe_eq_zero] using hx
+    simpa only [Ne.def, NNReal.coe_eq_zero] using hx
   refine' ⟨n, _, _⟩
   · rwa [← ENNReal.coe_zpow A, ENNReal.coe_le_coe]
   · rwa [← ENNReal.coe_zpow A, ENNReal.coe_lt_coe]
@@ -2763,11 +2763,11 @@ theorem exists_mem_Ioc_zpow {x y : ℝ≥0∞} (hx : x ≠ 0) (h'x : x ≠ ∞)
   by
   lift x to ℝ≥0 using h'x
   lift y to ℝ≥0 using h'y
-  have A : y ≠ 0 := by simpa only [Ne.def, coe_eq_zero] using (zero_lt_one.trans hy).ne'
+  have A : y ≠ 0 := by simpa only [Ne.def, NNReal.coe_eq_zero] using (zero_lt_one.trans hy).ne'
   obtain ⟨n, hn, h'n⟩ : ∃ n : ℤ, y ^ n < x ∧ x ≤ y ^ (n + 1) :=
     by
     refine' NNReal.exists_mem_Ioc_zpow _ (one_lt_coe_iff.1 hy)
-    simpa only [Ne.def, coe_eq_zero] using hx
+    simpa only [Ne.def, NNReal.coe_eq_zero] using hx
   refine' ⟨n, _, _⟩
   · rwa [← ENNReal.coe_zpow A, ENNReal.coe_lt_coe]
   · rwa [← ENNReal.coe_zpow A, ENNReal.coe_le_coe]
@@ -2819,7 +2819,7 @@ theorem monotone_zpow {x : ℝ≥0∞} (hx : 1 ≤ x) : Monotone ((· ^ ·) x :
 protected theorem zpow_add {x : ℝ≥0∞} (hx : x ≠ 0) (h'x : x ≠ ∞) (m n : ℤ) :
     x ^ (m + n) = x ^ m * x ^ n := by
   lift x to ℝ≥0 using h'x
-  replace hx : x ≠ 0; · simpa only [Ne.def, coe_eq_zero] using hx
+  replace hx : x ≠ 0; · simpa only [Ne.def, NNReal.coe_eq_zero] using hx
   simp only [← coe_zpow hx, zpow_add₀ hx, coe_mul]
 #align ennreal.zpow_add ENNReal.zpow_add
 -/
@@ -3254,7 +3254,7 @@ theorem toReal_eq_toReal (ha : a ≠ ∞) (hb : b ≠ ∞) : ENNReal.toReal a =
   by
   lift a to ℝ≥0 using ha
   lift b to ℝ≥0 using hb
-  simp only [coe_eq_coe, NNReal.coe_eq, coe_to_real]
+  simp only [coe_eq_coe, NNReal.coe_inj, coe_to_real]
 #align ennreal.to_real_eq_to_real ENNReal.toReal_eq_toReal
 -/
 

Mathbin/Data/Real/Ereal.lean

@@ -1428,7 +1428,7 @@ theorem abs_eq_zero_iff {x : EReal} : x.abs = 0 ↔ x = 0 :=
   by
   induction x using EReal.rec
   · simp only [abs_bot, ENNReal.top_ne_zero, bot_ne_zero]
-  · simp only [EReal.abs, coe_eq_zero, ENNReal.ofReal_eq_zero, abs_nonpos_iff]
+  · simp only [EReal.abs, NNReal.coe_eq_zero, ENNReal.ofReal_eq_zero, abs_nonpos_iff]
   · simp only [abs_top, ENNReal.top_ne_zero, top_ne_zero]
 #align ereal.abs_eq_zero_iff EReal.abs_eq_zero_iff
 -/
@@ -1460,28 +1460,28 @@ theorem abs_mul (x y : EReal) : (x * y).abs = x.abs * y.abs :=
   case coe_coe x y => simp only [← coe_mul, EReal.abs, abs_mul, ENNReal.ofReal_mul (abs_nonneg _)]
   case pos_bot x hx =>
     simp only [coe_mul_bot_of_pos hx, hx.ne', abs_bot, WithTop.mul_top, Ne.def, abs_eq_zero_iff,
-      coe_eq_zero, not_false_iff]
+      NNReal.coe_eq_zero, not_false_iff]
   case neg_bot x hx =>
     simp only [coe_mul_bot_of_neg hx, hx.ne, abs_bot, WithTop.mul_top, Ne.def, abs_eq_zero_iff,
-      coe_eq_zero, not_false_iff, abs_top]
+      NNReal.coe_eq_zero, not_false_iff, abs_top]
   case pos_top x hx =>
-    simp only [coe_mul_top_of_pos hx, hx.ne', WithTop.mul_top, Ne.def, abs_eq_zero_iff, coe_eq_zero,
-      not_false_iff, abs_top]
+    simp only [coe_mul_top_of_pos hx, hx.ne', WithTop.mul_top, Ne.def, abs_eq_zero_iff,
+      NNReal.coe_eq_zero, not_false_iff, abs_top]
   case neg_top x hx =>
     simp only [coe_mul_top_of_neg hx, hx.ne, abs_bot, WithTop.mul_top, Ne.def, abs_eq_zero_iff,
-      coe_eq_zero, not_false_iff, abs_top]
+      NNReal.coe_eq_zero, not_false_iff, abs_top]
   case top_pos y hy =>
-    simp only [top_mul_coe_of_pos hy, hy.ne', WithTop.top_mul, Ne.def, abs_eq_zero_iff, coe_eq_zero,
-      not_false_iff, abs_top]
+    simp only [top_mul_coe_of_pos hy, hy.ne', WithTop.top_mul, Ne.def, abs_eq_zero_iff,
+      NNReal.coe_eq_zero, not_false_iff, abs_top]
   case top_neg y hy =>
     simp only [top_mul_coe_of_neg hy, hy.ne, abs_bot, WithTop.top_mul, Ne.def, abs_eq_zero_iff,
-      coe_eq_zero, not_false_iff, abs_top]
+      NNReal.coe_eq_zero, not_false_iff, abs_top]
   case bot_pos y hy =>
     simp only [bot_mul_coe_of_pos hy, hy.ne', abs_bot, WithTop.top_mul, Ne.def, abs_eq_zero_iff,
-      coe_eq_zero, not_false_iff]
+      NNReal.coe_eq_zero, not_false_iff]
   case bot_neg y hy =>
     simp only [bot_mul_coe_of_neg hy, hy.ne, abs_bot, WithTop.top_mul, Ne.def, abs_eq_zero_iff,
-      coe_eq_zero, not_false_iff, abs_top]
+      NNReal.coe_eq_zero, not_false_iff, abs_top]
 #align ereal.abs_mul EReal.abs_mul
 -/