[Merged by Bors] - chore: tidy various files

Mathlib/Algebra/GCDMonoid/Finset.lean

@@ -100,8 +100,8 @@ theorem lcm_union [DecidableEq β] : (s₁ ∪ s₂).lcm f = GCDMonoid.lcm (s₁
     fun a s _ ih ↦ by rw [insert_union, lcm_insert, lcm_insert, ih, lcm_assoc]
 #align finset.lcm_union Finset.lcm_union
 
-theorem lcm_congr {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ a ∈ s₂, f a = g a)
-    : s₁.lcm f = s₂.lcm g := by
+theorem lcm_congr {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ a ∈ s₂, f a = g a) :
+    s₁.lcm f = s₂.lcm g := by
   subst hs
   exact Finset.fold_congr hfg
 #align finset.lcm_congr Finset.lcm_congr

Mathlib/Algebra/Hom/Centroid.lean

@@ -88,8 +88,7 @@ section NonUnitalNonAssocSemiring
 
 variable [NonUnitalNonAssocSemiring α]
 
-instance : CentroidHomClass (CentroidHom α) α
-    where
+instance : CentroidHomClass (CentroidHom α) α where
   coe f := f.toFun
   coe_injective' f g h := by
     cases f
@@ -112,6 +111,7 @@ instance : CoeFun (CentroidHom α) fun _ ↦ α → α :=
 /- Porting note:
 `theorem to_fun_eq_coe {f : CentroidHom α} : f.toFun = (f : α → α) := rfl`
 removed because it is now a tautology -/
+#noalign centroid_hom.to_fun_eq_coe
 
 @[ext]
 theorem ext {f g : CentroidHom α} (h : ∀ a, f a = g a) : f = g :=
@@ -272,9 +272,7 @@ instance hasNsmul : SMul ℕ (CentroidHom α) :=
 
 instance hasNpowNat : Pow (CentroidHom α) ℕ :=
   ⟨fun f n ↦
-    { (f.toEnd ^ n :
-        AddMonoid.End
-          α) with
+    { (f.toEnd ^ n : AddMonoid.End α) with
       map_mul_left' := fun a b ↦ by
         induction' n with n ih
         · exact rfl
@@ -431,10 +429,7 @@ instance : Sub (CentroidHom α) :=
 
 instance hasZsmul : SMul ℤ (CentroidHom α) :=
   ⟨fun n f ↦
-    {
-      (SMul.smul n f :
-        α →+
-          α) with
+    { (SMul.smul n f : α →+ α) with
       map_mul_left' := fun a b ↦ by
         change n • f (a * b) = a * n • f b
         rw [map_mul_left f, ← mul_smul_comm]
@@ -470,8 +465,7 @@ theorem toEnd_zsmul (x : CentroidHom α) (n : ℤ) : (n • x).toEnd = n • x.t
 #align centroid_hom.to_End_zsmul CentroidHom.toEnd_zsmul
 
 instance : AddCommGroup (CentroidHom α) :=
-  toEnd_injective.addCommGroup _ toEnd_zero toEnd_add toEnd_neg toEnd_sub toEnd_nsmul
-    toEnd_zsmul
+  toEnd_injective.addCommGroup _ toEnd_zero toEnd_add toEnd_neg toEnd_sub toEnd_nsmul toEnd_zsmul
 
 @[simp, norm_cast]
 theorem coe_neg (f : CentroidHom α) : ⇑(-f) = -f :=
@@ -498,7 +492,7 @@ theorem toEnd_int_cast (z : ℤ) : (z : CentroidHom α).toEnd = ↑z :=
   rfl
 #align centroid_hom.to_End_int_cast CentroidHom.toEnd_int_cast
 
-instance : Ring (CentroidHom α) :=
+instance ring : Ring (CentroidHom α) :=
   toEnd_injective.ring _ toEnd_zero toEnd_one toEnd_add toEnd_mul toEnd_neg toEnd_sub
     toEnd_nsmul toEnd_zsmul toEnd_pow toEnd_nat_cast toEnd_int_cast
 
@@ -513,7 +507,7 @@ variable [NonUnitalRing α]
 /-- A prime associative ring has commutative centroid. -/
 @[reducible]
 def commRing (h : ∀ a b : α, (∀ r : α, a * r * b = 0) → a = 0 ∨ b = 0) : CommRing (CentroidHom α) :=
-  { CentroidHom.instRingCentroidHomToNonUnitalNonAssocSemiring with
+  { CentroidHom.ring with
     mul_comm := fun f g ↦ by
       ext
       refine' sub_eq_zero.1 ((or_self_iff _).1 <| (h _ _) fun r ↦ _)

Mathlib/Algebra/Order/Kleene.lean

@@ -290,17 +290,17 @@ end KleeneAlgebra
 
 namespace Prod
 
-instance [IdemSemiring α] [IdemSemiring β] : IdemSemiring (α × β) :=
-  { Prod.instSemiringProd, Prod.semilatticeSup _ _, Prod.orderBot _ _ with
+instance instIdemSemiring [IdemSemiring α] [IdemSemiring β] : IdemSemiring (α × β) :=
+  { Prod.instSemiring, Prod.semilatticeSup _ _, Prod.orderBot _ _ with
     add_eq_sup := fun _ _ ↦ ext (add_eq_sup _ _) (add_eq_sup _ _) }
 
 instance [IdemCommSemiring α] [IdemCommSemiring β] : IdemCommSemiring (α × β) :=
-  { Prod.instCommSemiringProd, Prod.instIdemSemiringProd with }
+  { Prod.instCommSemiring, Prod.instIdemSemiring with }
 
 variable [KleeneAlgebra α] [KleeneAlgebra β]
 
 instance : KleeneAlgebra (α × β) :=
-  { Prod.instIdemSemiringProd with
+  { Prod.instIdemSemiring with
     kstar := fun a ↦ (a.1∗, a.2∗)
     one_le_kstar := fun _ ↦ ⟨one_le_kstar, one_le_kstar⟩
     mul_kstar_le_kstar := fun _ ↦ ⟨mul_kstar_le_kstar, mul_kstar_le_kstar⟩
@@ -326,17 +326,17 @@ end Prod
 
 namespace Pi
 
-instance [∀ i, IdemSemiring (π i)] : IdemSemiring (∀ i, π i) :=
+instance instIdemSemiring [∀ i, IdemSemiring (π i)] : IdemSemiring (∀ i, π i) :=
   { Pi.semiring, Pi.semilatticeSup, Pi.orderBot with
     add_eq_sup := fun _ _ ↦ funext fun _ ↦ add_eq_sup _ _ }
 
 instance [∀ i, IdemCommSemiring (π i)] : IdemCommSemiring (∀ i, π i) :=
-  { Pi.commSemiring, Pi.instIdemSemiringForAll with }
+  { Pi.commSemiring, Pi.instIdemSemiring with }
 
 variable [∀ i, KleeneAlgebra (π i)]
 
 instance : KleeneAlgebra (∀ i, π i) :=
-  { Pi.instIdemSemiringForAll with
+  { Pi.instIdemSemiring with
     kstar := fun a i ↦ (a i)∗
     one_le_kstar := fun _ _ ↦ one_le_kstar
     mul_kstar_le_kstar := fun _ _ ↦ mul_kstar_le_kstar

Mathlib/Algebra/Ring/Prod.lean

@@ -33,67 +33,72 @@ variable {α β R R' S S' T T' : Type _}
 namespace Prod
 
 /-- Product of two distributive types is distributive. -/
-instance [Distrib R] [Distrib S] : Distrib (R × S) :=
+instance instDistrib [Distrib R] [Distrib S] : Distrib (R × S) :=
   { left_distrib := fun _ _ _ => mk.inj_iff.mpr ⟨left_distrib _ _ _, left_distrib _ _ _⟩
     right_distrib := fun _ _ _ => mk.inj_iff.mpr ⟨right_distrib _ _ _, right_distrib _ _ _⟩ }
 
 /-- Product of two `NonUnitalNonAssocSemiring`s is a `NonUnitalNonAssocSemiring`. -/
-instance [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] :
+instance instNonUnitalNonAssocSemiring [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] :
     NonUnitalNonAssocSemiring (R × S) :=
   { inferInstanceAs (AddCommMonoid (R × S)),
     inferInstanceAs (Distrib (R × S)),
     inferInstanceAs (MulZeroClass (R × S)) with }
 
 /-- Product of two `NonUnitalSemiring`s is a `NonUnitalSemiring`. -/
-instance [NonUnitalSemiring R] [NonUnitalSemiring S] : NonUnitalSemiring (R × S) :=
+instance instNonUnitalSemiring [NonUnitalSemiring R] [NonUnitalSemiring S] :
+    NonUnitalSemiring (R × S) :=
   { inferInstanceAs (NonUnitalNonAssocSemiring (R × S)),
     inferInstanceAs (SemigroupWithZero (R × S)) with }
 
 /-- Product of two `NonAssocSemiring`s is a `NonAssocSemiring`. -/
-instance [NonAssocSemiring R] [NonAssocSemiring S] : NonAssocSemiring (R × S) :=
+instance instNonAssocSemiring [NonAssocSemiring R] [NonAssocSemiring S] :
+    NonAssocSemiring (R × S) :=
   { inferInstanceAs (NonUnitalNonAssocSemiring (R × S)),
     inferInstanceAs (MulZeroOneClass (R × S)),
     inferInstanceAs (AddMonoidWithOne (R × S)) with }
 
 /-- Product of two semirings is a semiring. -/
-instance [Semiring R] [Semiring S] : Semiring (R × S) :=
+instance instSemiring [Semiring R] [Semiring S] : Semiring (R × S) :=
   { inferInstanceAs (NonUnitalSemiring (R × S)),
     inferInstanceAs (NonAssocSemiring (R × S)),
     inferInstanceAs (MonoidWithZero (R × S)) with }
 
 /-- Product of two `NonUnitalCommSemiring`s is a `NonUnitalCommSemiring`. -/
-instance [NonUnitalCommSemiring R] [NonUnitalCommSemiring S] : NonUnitalCommSemiring (R × S) :=
+instance instNonUnitalCommSemiring [NonUnitalCommSemiring R] [NonUnitalCommSemiring S] :
+    NonUnitalCommSemiring (R × S) :=
   { inferInstanceAs (NonUnitalSemiring (R × S)), inferInstanceAs (CommSemigroup (R × S)) with }
 
 /-- Product of two commutative semirings is a commutative semiring. -/
-instance [CommSemiring R] [CommSemiring S] : CommSemiring (R × S) :=
+instance instCommSemiring [CommSemiring R] [CommSemiring S] : CommSemiring (R × S) :=
   { inferInstanceAs (Semiring (R × S)), inferInstanceAs (CommMonoid (R × S)) with }
 
-instance [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] : NonUnitalNonAssocRing (R × S) :=
+instance instNonUnitalNonAssocRing [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] :
+    NonUnitalNonAssocRing (R × S) :=
   { inferInstanceAs (AddCommGroup (R × S)),
     inferInstanceAs (NonUnitalNonAssocSemiring (R × S)) with }
 
-instance [NonUnitalRing R] [NonUnitalRing S] : NonUnitalRing (R × S) :=
+instance instNonUnitalRing [NonUnitalRing R] [NonUnitalRing S] : NonUnitalRing (R × S) :=
   { inferInstanceAs (NonUnitalNonAssocRing (R × S)),
     inferInstanceAs (NonUnitalSemiring (R × S)) with }
 
-instance [NonAssocRing R] [NonAssocRing S] : NonAssocRing (R × S) :=
+instance instNonAssocRing [NonAssocRing R] [NonAssocRing S] : NonAssocRing (R × S) :=
   { inferInstanceAs (NonUnitalNonAssocRing (R × S)),
     inferInstanceAs (NonAssocSemiring (R × S)),
     inferInstanceAs (AddGroupWithOne (R × S)) with }
 
 /-- Product of two rings is a ring. -/
-instance [Ring R] [Ring S] : Ring (R × S) :=
+instance instRing [Ring R] [Ring S] : Ring (R × S) :=
   { inferInstanceAs (Semiring (R × S)),
     inferInstanceAs (AddCommGroup (R × S)),
     inferInstanceAs (AddGroupWithOne (R × S)) with }
 
 /-- Product of two `NonUnitalCommRing`s is a `NonUnitalCommRing`. -/
-instance [NonUnitalCommRing R] [NonUnitalCommRing S] : NonUnitalCommRing (R × S) :=
+instance instNonUnitalCommRing [NonUnitalCommRing R] [NonUnitalCommRing S] :
+    NonUnitalCommRing (R × S) :=
   { inferInstanceAs (NonUnitalRing (R × S)), inferInstanceAs (CommSemigroup (R × S)) with }
 
 /-- Product of two commutative rings is a commutative ring. -/
-instance [CommRing R] [CommRing S] : CommRing (R × S) :=
+instance instCommRing [CommRing R] [CommRing S] : CommRing (R × S) :=
   { inferInstanceAs (Ring (R × S)), inferInstanceAs (CommMonoid (R × S)) with }
 
 end Prod
@@ -162,7 +167,7 @@ variable [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S'] [NonUnita
 
 variable (f : R →ₙ+* R') (g : S →ₙ+* S')
 
-/-- `prod.map` as a `NonUnitalRingHom`. -/
+/-- `Prod.map` as a `NonUnitalRingHom`. -/
 def prodMap : R × S →ₙ+* R' × S' :=
   (f.comp (fst R S)).prod (g.comp (snd R S))
 #align non_unital_ring_hom.prod_map NonUnitalRingHom.prodMap
@@ -282,26 +287,26 @@ def prodComm : R × S ≃+* S × R :=
 #align ring_equiv.prod_comm RingEquiv.prodComm
 
 @[simp]
-theorem coe_prod_comm : ⇑(prodComm : R × S ≃+* S × R) = Prod.swap :=
+theorem coe_prodComm : ⇑(prodComm : R × S ≃+* S × R) = Prod.swap :=
   rfl
-#align ring_equiv.coe_prod_comm RingEquiv.coe_prod_comm
+#align ring_equiv.coe_prod_comm RingEquiv.coe_prodComm
 
 @[simp]
-theorem coe_prod_comm_symm : ⇑(prodComm : R × S ≃+* S × R).symm = Prod.swap :=
+theorem coe_prodComm_symm : ⇑(prodComm : R × S ≃+* S × R).symm = Prod.swap :=
   rfl
-#align ring_equiv.coe_prod_comm_symm RingEquiv.coe_prod_comm_symm
+#align ring_equiv.coe_prod_comm_symm RingEquiv.coe_prodComm_symm
 
 @[simp]
-theorem fst_comp_coe_prod_comm :
+theorem fst_comp_coe_prodComm :
     (RingHom.fst S R).comp ↑(prodComm : R × S ≃+* S × R) = RingHom.snd R S :=
   RingHom.ext fun _ => rfl
-#align ring_equiv.fst_comp_coe_prod_comm RingEquiv.fst_comp_coe_prod_comm
+#align ring_equiv.fst_comp_coe_prod_comm RingEquiv.fst_comp_coe_prodComm
 
 @[simp]
-theorem snd_comp_coe_prod_comm :
+theorem snd_comp_coe_prodComm :
     (RingHom.snd S R).comp ↑(prodComm : R × S ≃+* S × R) = RingHom.fst R S :=
   RingHom.ext fun _ => rfl
-#align ring_equiv.snd_comp_coe_prod_comm RingEquiv.snd_comp_coe_prod_comm
+#align ring_equiv.snd_comp_coe_prod_comm RingEquiv.snd_comp_coe_prodComm
 
 section
 

Mathlib/Analysis/Convex/StrictConvexSpace.lean

@@ -44,10 +44,10 @@ In a strictly convex space, we prove
 
 We also provide several lemmas that can be used as alternative constructors for `StrictConvex ℝ E`:
 
-- `StrictConvexSpace.ofStrictConvexClosedUnitBall`: if `closed_ball (0 : E) 1` is strictly
+- `StrictConvexSpace.of_strictConvex_closed_unit_ball`: if `closed_ball (0 : E) 1` is strictly
   convex, then `E` is a strictly convex space;
 
-- `StrictConvexSpace.ofNormAdd`: if `‖x + y‖ = ‖x‖ + ‖y‖` implies `SameRay ℝ x y` for all
+- `StrictConvexSpace.of_norm_add`: if `‖x + y‖ = ‖x‖ + ‖y‖` implies `SameRay ℝ x y` for all
   nonzero `x y : E`, then `E` is a strictly convex space.
 
 ## Implementation notes
@@ -69,7 +69,7 @@ open Convex Pointwise
 require balls of positive radius with center at the origin to be strictly convex in the definition,
 then prove that any closed ball is strictly convex in `strictConvex_closedBall` below.
 
-See also `StrictConvexSpace.ofStrictConvexClosedUnitBall`. -/
+See also `StrictConvexSpace.of_strictConvex_closed_unit_ball`. -/
 class StrictConvexSpace (𝕜 E : Type _) [NormedLinearOrderedField 𝕜] [NormedAddCommGroup E]
   [NormedSpace 𝕜 E] : Prop where
   strictConvex_closedBall : ∀ r : ℝ, 0 < r → StrictConvex 𝕜 (closedBall (0 : E) r)
@@ -90,65 +90,66 @@ theorem strictConvex_closedBall [StrictConvexSpace 𝕜 E] (x : E) (r : ℝ) :
 variable [NormedSpace ℝ E]
 
 /-- A real normed vector space is strictly convex provided that the unit ball is strictly convex. -/
-theorem StrictConvexSpace.ofStrictConvexClosedUnitBall [LinearMap.CompatibleSMul E E 𝕜 ℝ]
+theorem StrictConvexSpace.of_strictConvex_closed_unit_ball [LinearMap.CompatibleSMul E E 𝕜 ℝ]
     (h : StrictConvex 𝕜 (closedBall (0 : E) 1)) : StrictConvexSpace 𝕜 E :=
   ⟨fun r hr => by simpa only [smul_closedUnitBall_of_nonneg hr.le] using h.smul r⟩
-#align strict_convex_space.of_strict_convex_closed_unit_ball StrictConvexSpace.ofStrictConvexClosedUnitBall
+#align strict_convex_space.of_strict_convex_closed_unit_ball StrictConvexSpace.of_strictConvex_closed_unit_ball
 
 /-- Strict convexity is equivalent to `‖a • x + b • y‖ < 1` for all `x` and `y` of norm at most `1`
 and all strictly positive `a` and `b` such that `a + b = 1`. This lemma shows that it suffices to
 check this for points of norm one and some `a`, `b` such that `a + b = 1`. -/
-theorem StrictConvexSpace.ofNormComboLtOne
+theorem StrictConvexSpace.of_norm_combo_lt_one
     (h : ∀ x y : E, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b : ℝ, a + b = 1 ∧ ‖a • x + b • y‖ < 1) :
     StrictConvexSpace ℝ E := by
   refine'
-    StrictConvexSpace.ofStrictConvexClosedUnitBall ℝ
+    StrictConvexSpace.of_strictConvex_closed_unit_ball ℝ
       ((convex_closedBall _ _).strictConvex' fun x hx y hy hne => _)
   rw [interior_closedBall (0 : E) one_ne_zero, closedBall_diff_ball,
     mem_sphere_zero_iff_norm] at hx hy
   rcases h x y hx hy hne with ⟨a, b, hab, hlt⟩
   use b
   rwa [AffineMap.lineMap_apply_module, interior_closedBall (0 : E) one_ne_zero, mem_ball_zero_iff,
     sub_eq_iff_eq_add.2 hab.symm]
-#align strict_convex_space.of_norm_combo_lt_one StrictConvexSpace.ofNormComboLtOne
+#align strict_convex_space.of_norm_combo_lt_one StrictConvexSpace.of_norm_combo_lt_one
 
-theorem StrictConvexSpace.ofNormComboNeOne
+theorem StrictConvexSpace.of_norm_combo_ne_one
     (h :
       ∀ x y : E,
         ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b : ℝ, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ ‖a • x + b • y‖ ≠ 1) :
     StrictConvexSpace ℝ E := by
-  refine' StrictConvexSpace.ofStrictConvexClosedUnitBall ℝ ((convex_closedBall _ _).strictConvex _)
+  refine' StrictConvexSpace.of_strictConvex_closed_unit_ball ℝ
+    ((convex_closedBall _ _).strictConvex _)
   simp only [interior_closedBall _ one_ne_zero, closedBall_diff_ball, Set.Pairwise,
     frontier_closedBall _ one_ne_zero, mem_sphere_zero_iff_norm]
   intro x hx y hy hne
   rcases h x y hx hy hne with ⟨a, b, ha, hb, hab, hne'⟩
   exact ⟨_, ⟨a, b, ha, hb, hab, rfl⟩, mt mem_sphere_zero_iff_norm.1 hne'⟩
-#align strict_convex_space.of_norm_combo_ne_one StrictConvexSpace.ofNormComboNeOne
+#align strict_convex_space.of_norm_combo_ne_one StrictConvexSpace.of_norm_combo_ne_one
 
-theorem StrictConvexSpace.ofNormAddNeTwo
+theorem StrictConvexSpace.of_norm_add_ne_two
     (h : ∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2) : StrictConvexSpace ℝ E := by
   refine'
-    StrictConvexSpace.ofNormComboNeOne fun x y hx hy hne =>
+    StrictConvexSpace.of_norm_combo_ne_one fun x y hx hy hne =>
       ⟨1 / 2, 1 / 2, one_half_pos.le, one_half_pos.le, add_halves _, _⟩
   rw [← smul_add, norm_smul, Real.norm_of_nonneg one_half_pos.le, one_div, ← div_eq_inv_mul, Ne.def,
     div_eq_one_iff_eq (two_ne_zero' ℝ)]
   exact h hx hy hne
-#align strict_convex_space.of_norm_add_ne_two StrictConvexSpace.ofNormAddNeTwo
+#align strict_convex_space.of_norm_add_ne_two StrictConvexSpace.of_norm_add_ne_two
 
-theorem StrictConvexSpace.ofPairwiseSphereNormNeTwo
+theorem StrictConvexSpace.of_pairwise_sphere_norm_ne_two
     (h : (sphere (0 : E) 1).Pairwise fun x y => ‖x + y‖ ≠ 2) : StrictConvexSpace ℝ E :=
-  StrictConvexSpace.ofNormAddNeTwo fun _ _ hx hy =>
+  StrictConvexSpace.of_norm_add_ne_two fun _ _ hx hy =>
     h (mem_sphere_zero_iff_norm.2 hx) (mem_sphere_zero_iff_norm.2 hy)
-#align strict_convex_space.of_pairwise_sphere_norm_ne_two StrictConvexSpace.ofPairwiseSphereNormNeTwo
+#align strict_convex_space.of_pairwise_sphere_norm_ne_two StrictConvexSpace.of_pairwise_sphere_norm_ne_two
 
 /-- If `‖x + y‖ = ‖x‖ + ‖y‖` implies that `x y : E` are in the same ray, then `E` is a strictly
 convex space. See also a more -/
-theorem StrictConvexSpace.ofNormAdd
+theorem StrictConvexSpace.of_norm_add
     (h : ∀ x y : E, ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y) : StrictConvexSpace ℝ E := by
-  refine' StrictConvexSpace.ofPairwiseSphereNormNeTwo fun x hx y hy => mt fun h₂ => _
+  refine' StrictConvexSpace.of_pairwise_sphere_norm_ne_two fun x hx y hy => mt fun h₂ => _
   rw [mem_sphere_zero_iff_norm] at hx hy
   exact (sameRay_iff_of_norm_eq (hx.trans hy.symm)).1 (h x y hx hy h₂)
-#align strict_convex_space.of_norm_add StrictConvexSpace.ofNormAdd
+#align strict_convex_space.of_norm_add StrictConvexSpace.of_norm_add
 
 variable [StrictConvexSpace ℝ E] {x y z : E} {a b r : ℝ}
 

Mathlib/Analysis/Convex/Uniform.lean

@@ -134,7 +134,7 @@ variable [NormedAddCommGroup E] [NormedSpace ℝ E] [UniformConvexSpace E]
 
 -- See note [lower instance priority]
 instance (priority := 100) UniformConvexSpace.toStrictConvexSpace : StrictConvexSpace ℝ E :=
-  StrictConvexSpace.ofNormAddNeTwo fun _ _ hx hy hxy =>
+  StrictConvexSpace.of_norm_add_ne_two fun _ _ hx hy hxy =>
     let ⟨_, hδ, h⟩ := exists_forall_closed_ball_dist_add_le_two_sub E (norm_sub_pos_iff.2 hxy)
     ((h hx.le hy.le le_rfl).trans_lt <| sub_lt_self _ hδ).ne
 #align uniform_convex_space.to_strict_convex_space UniformConvexSpace.toStrictConvexSpace

Mathlib/Analysis/Normed/Field/Basic.lean

@@ -242,7 +242,7 @@ instance ULift.nonUnitalSeminormedRing : NonUnitalSeminormedRing (ULift α) :=
   using the sup norm. -/
 instance Prod.nonUnitalSeminormedRing [NonUnitalSeminormedRing β] :
     NonUnitalSeminormedRing (α × β) :=
-  { Prod.seminormedAddCommGroup, instNonUnitalRingProd with
+  { seminormedAddCommGroup, instNonUnitalRing with
     norm_mul := fun x y =>
       calc
         ‖x * y‖ = ‖(x.1 * y.1, x.2 * y.2)‖ := rfl
@@ -393,7 +393,7 @@ instance ULift.seminormedRing : SeminormedRing (ULift α) :=
 /-- Seminormed ring structure on the product of two seminormed rings,
   using the sup norm. -/
 instance Prod.seminormedRing [SeminormedRing β] : SeminormedRing (α × β) :=
-  { Prod.nonUnitalSeminormedRing, instRingProd with }
+  { nonUnitalSeminormedRing, instRing with }
 #align prod.semi_normed_ring Prod.seminormedRing
 
 /-- Seminormed ring structure on the product of finitely many seminormed rings,
@@ -452,7 +452,7 @@ instance ULift.normedRing : NormedRing (ULift α) :=
 
 /-- Normed ring structure on the product of two normed rings, using the sup norm. -/
 instance Prod.normedRing [NormedRing β] : NormedRing (α × β) :=
-  { Prod.nonUnitalNormedRing, instRingProd with }
+  { nonUnitalNormedRing, instRing with }
 #align prod.normed_ring Prod.normedRing
 
 /-- Normed ring structure on the product of finitely many normed rings, using the sup norm. -/