bump to nightly-2023-08-07-11

mathlib commit leanprover-community/mathlib@32a7e53

Mathbin/Algebra/BigOperators/Fin.lean

@@ -361,7 +361,7 @@ end Fin
 /-- Equivalence between `fin n → fin m` and `fin (m ^ n)`. -/
 @[simps]
 def finFunctionFinEquiv {m n : ℕ} : (Fin n → Fin m) ≃ Fin (m ^ n) :=
-  Equiv.ofRightInverseOfCardLe (le_of_eq <| by simp_rw [Fintype.card_fun, Fintype.card_fin])
+  Equiv.ofRightInverseOfCardLE (le_of_eq <| by simp_rw [Fintype.card_fun, Fintype.card_fin])
     (fun f =>
       ⟨∑ i, f i * m ^ (i : ℕ), by
         induction' n with n ih generalizing f
@@ -412,7 +412,7 @@ theorem finFunctionFinEquiv_single {m n : ℕ} [NeZero m] (i : Fin n) (j : Fin m
 #print finPiFinEquiv /-
 /-- Equivalence between `Π i : fin m, fin (n i)` and `fin (∏ i : fin m, n i)`. -/
 def finPiFinEquiv {m : ℕ} {n : Fin m → ℕ} : (∀ i : Fin m, Fin (n i)) ≃ Fin (∏ i : Fin m, n i) :=
-  Equiv.ofRightInverseOfCardLe (le_of_eq <| by simp_rw [Fintype.card_pi, Fintype.card_fin])
+  Equiv.ofRightInverseOfCardLE (le_of_eq <| by simp_rw [Fintype.card_pi, Fintype.card_fin])
     (fun f =>
       ⟨∑ i, f i * ∏ j, n (Fin.castLEEmb i.is_lt.le j),
         by

Mathbin/AlgebraicTopology/DoldKan/Equivalence.lean

@@ -153,15 +153,15 @@ def Γ : ChainComplex A ℕ ⥤ SimplicialObject A :=
 /-- The comparison isomorphism between `normalized_Moore_complex A` and
 the functor `idempotents.dold_kan.N` from the pseudoabelian case -/
 @[simps]
-def comparisonN : (n : SimplicialObject A ⥤ _) ≅ Idempotents.DoldKan.n :=
+def comparisonN : (n : SimplicialObject A ⥤ _) ≅ Idempotents.DoldKan.N :=
   calc
     n ≅ n ⋙ 𝟭 _ := Functor.leftUnitor n
     _ ≅ n ⋙ (toKaroubi_equivalence _).Functor ⋙ (toKaroubi_equivalence _).inverse :=
       (isoWhiskerLeft _ (toKaroubi_equivalence _).unitIso)
     _ ≅ (n ⋙ (toKaroubi_equivalence _).Functor) ⋙ (toKaroubi_equivalence _).inverse := (Iso.refl _)
     _ ≅ N₁ ⋙ (toKaroubi_equivalence _).inverse :=
       (isoWhiskerRight (N₁_iso_normalizedMooreComplex_comp_toKaroubi A).symm _)
-    _ ≅ Idempotents.DoldKan.n := by rfl
+    _ ≅ Idempotents.DoldKan.N := by rfl
 #align category_theory.abelian.dold_kan.comparison_N CategoryTheory.Abelian.DoldKan.comparisonN
 
 /-- The Dold-Kan equivalence for abelian categories -/

Mathbin/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean

@@ -49,47 +49,62 @@ namespace DoldKan
 
 open AlgebraicTopology.DoldKan
 
+#print CategoryTheory.Idempotents.DoldKan.N /-
 /-- The functor `N` for the equivalence is obtained by composing
 `N' : simplicial_object C ⥤ karoubi (chain_complex C ℕ)` and the inverse
 of the equivalence `chain_complex C ℕ ≌ karoubi (chain_complex C ℕ)`. -/
 @[simps, nolint unused_arguments]
-def n : SimplicialObject C ⥤ ChainComplex C ℕ :=
+def N : SimplicialObject C ⥤ ChainComplex C ℕ :=
   N₁ ⋙ (toKaroubi_equivalence _).inverse
-#align category_theory.idempotents.dold_kan.N CategoryTheory.Idempotents.DoldKan.n
+#align category_theory.idempotents.dold_kan.N CategoryTheory.Idempotents.DoldKan.N
+-/
 
+#print CategoryTheory.Idempotents.DoldKan.Γ /-
 /-- The functor `Γ` for the equivalence is `Γ'`. -/
 @[simps, nolint unused_arguments]
 def Γ : ChainComplex C ℕ ⥤ SimplicialObject C :=
   Γ₀
 #align category_theory.idempotents.dold_kan.Γ CategoryTheory.Idempotents.DoldKan.Γ
+-/
 
+#print CategoryTheory.Idempotents.DoldKan.hN₁ /-
 theorem hN₁ :
     (toKaroubi_equivalence (SimplicialObject C)).Functor ⋙ Preadditive.DoldKan.equivalence.Functor =
       N₁ :=
   Functor.congr_obj (functorExtension₁_comp_whiskeringLeft_toKaroubi _ _) N₁
 #align category_theory.idempotents.dold_kan.hN₁ CategoryTheory.Idempotents.DoldKan.hN₁
+-/
 
+#print CategoryTheory.Idempotents.DoldKan.hΓ₀ /-
 theorem hΓ₀ :
     (toKaroubi_equivalence (ChainComplex C ℕ)).Functor ⋙ Preadditive.DoldKan.equivalence.inverse =
       Γ ⋙ (toKaroubi_equivalence _).Functor :=
   Functor.congr_obj (functorExtension₂_comp_whiskeringLeft_toKaroubi _ _) Γ₀
 #align category_theory.idempotents.dold_kan.hΓ₀ CategoryTheory.Idempotents.DoldKan.hΓ₀
+-/
 
+#print CategoryTheory.Idempotents.DoldKan.equivalence /-
 /-- The Dold-Kan equivalence for pseudoabelian categories given
 by the functors `N` and `Γ`. It is obtained by applying the results in
 `compatibility.lean` to the equivalence `preadditive.dold_kan.equivalence`. -/
 def equivalence : SimplicialObject C ≌ ChainComplex C ℕ :=
   Compatibility.equivalence (eqToIso hN₁) (eqToIso hΓ₀)
 #align category_theory.idempotents.dold_kan.equivalence CategoryTheory.Idempotents.DoldKan.equivalence
+-/
 
-theorem equivalence_functor : (equivalence : SimplicialObject C ≌ _).Functor = n :=
+#print CategoryTheory.Idempotents.DoldKan.equivalence_functor /-
+theorem equivalence_functor : (equivalence : SimplicialObject C ≌ _).Functor = N :=
   rfl
 #align category_theory.idempotents.dold_kan.equivalence_functor CategoryTheory.Idempotents.DoldKan.equivalence_functor
+-/
 
+#print CategoryTheory.Idempotents.DoldKan.equivalence_inverse /-
 theorem equivalence_inverse : (equivalence : SimplicialObject C ≌ _).inverse = Γ :=
   rfl
 #align category_theory.idempotents.dold_kan.equivalence_inverse CategoryTheory.Idempotents.DoldKan.equivalence_inverse
+-/
 
+#print CategoryTheory.Idempotents.DoldKan.hη /-
 /-- The natural isomorphism `NΓ' satisfies the compatibility that is needed
 for the construction of our counit isomorphism `η` -/
 theorem hη :
@@ -102,19 +117,25 @@ theorem hη :
     preadditive.dold_kan.equivalence_counit_iso, N₂Γ₂_to_karoubi_iso_hom, eq_to_hom_map,
     eq_to_hom_trans_assoc, eq_to_hom_app] using N₂Γ₂_compatible_with_N₁Γ₀ K
 #align category_theory.idempotents.dold_kan.hη CategoryTheory.Idempotents.DoldKan.hη
+-/
 
+#print CategoryTheory.Idempotents.DoldKan.η /-
 /-- The counit isomorphism induced by `N₁Γ₀` -/
 @[simps]
-def η : Γ ⋙ n ≅ 𝟭 (ChainComplex C ℕ) :=
+def η : Γ ⋙ N ≅ 𝟭 (ChainComplex C ℕ) :=
   Compatibility.equivalenceCounitIso
     (N₁Γ₀ : (Γ : ChainComplex C ℕ ⥤ _) ⋙ N₁ ≅ (toKaroubi_equivalence _).Functor)
 #align category_theory.idempotents.dold_kan.η CategoryTheory.Idempotents.DoldKan.η
+-/
 
+#print CategoryTheory.Idempotents.DoldKan.equivalence_counitIso /-
 theorem equivalence_counitIso :
-    DoldKan.equivalence.counitIso = (η : Γ ⋙ n ≅ 𝟭 (ChainComplex C ℕ)) :=
+    DoldKan.equivalence.counitIso = (η : Γ ⋙ N ≅ 𝟭 (ChainComplex C ℕ)) :=
   Compatibility.equivalenceCounitIso_eq hη
 #align category_theory.idempotents.dold_kan.equivalence_counit_iso CategoryTheory.Idempotents.DoldKan.equivalence_counitIso
+-/
 
+#print CategoryTheory.Idempotents.DoldKan.hε /-
 theorem hε :
     Compatibility.υ (eqToIso hN₁) =
       (Γ₂N₁ :
@@ -129,15 +150,20 @@ theorem hε :
   dsimp
   simpa only [id_comp, eq_to_hom_app, eq_to_hom_map, eq_to_hom_trans]
 #align category_theory.idempotents.dold_kan.hε CategoryTheory.Idempotents.DoldKan.hε
+-/
 
+#print CategoryTheory.Idempotents.DoldKan.ε /-
 /-- The unit isomorphism induced by `Γ₂N₁`. -/
-def ε : 𝟭 (SimplicialObject C) ≅ n ⋙ Γ :=
+def ε : 𝟭 (SimplicialObject C) ≅ N ⋙ Γ :=
   Compatibility.equivalenceUnitIso (eqToIso hΓ₀) Γ₂N₁
 #align category_theory.idempotents.dold_kan.ε CategoryTheory.Idempotents.DoldKan.ε
+-/
 
-theorem equivalence_unitIso : DoldKan.equivalence.unitIso = (ε : 𝟭 (SimplicialObject C) ≅ n ⋙ Γ) :=
+#print CategoryTheory.Idempotents.DoldKan.equivalence_unitIso /-
+theorem equivalence_unitIso : DoldKan.equivalence.unitIso = (ε : 𝟭 (SimplicialObject C) ≅ N ⋙ Γ) :=
   Compatibility.equivalenceUnitIso_eq hε
 #align category_theory.idempotents.dold_kan.equivalence_unit_iso CategoryTheory.Idempotents.DoldKan.equivalence_unitIso
+-/
 
 end DoldKan
 

Mathbin/Analysis/Calculus/DiffContOnCl.lean

@@ -104,10 +104,10 @@ protected theorem differentiableAt (h : DiffContOnCl 𝕜 f s) (hs : IsOpen s) (
 #align diff_cont_on_cl.differentiable_at DiffContOnCl.differentiableAt
 -/
 
-#print DiffContOnCl.differentiable_at' /-
-theorem differentiable_at' (h : DiffContOnCl 𝕜 f s) (hx : s ∈ 𝓝 x) : DifferentiableAt 𝕜 f x :=
+#print DiffContOnCl.differentiableAt' /-
+theorem differentiableAt' (h : DiffContOnCl 𝕜 f s) (hx : s ∈ 𝓝 x) : DifferentiableAt 𝕜 f x :=
   h.DifferentiableOn.DifferentiableAt hx
-#align diff_cont_on_cl.differentiable_at' DiffContOnCl.differentiable_at'
+#align diff_cont_on_cl.differentiable_at' DiffContOnCl.differentiableAt'
 -/
 
 #print DiffContOnCl.mono /-

Mathbin/CategoryTheory/Functor/Category.lean

@@ -92,9 +92,11 @@ theorem comp_app {F G H : C ⥤ D} (α : F ⟶ G) (β : G ⟶ H) (X : C) :
 #align category_theory.nat_trans.comp_app CategoryTheory.NatTrans.comp_app
 -/
 
+#print CategoryTheory.NatTrans.comp_app_assoc /-
 theorem comp_app_assoc {F G H : C ⥤ D} (α : F ⟶ G) (β : G ⟶ H) (X : C) {X' : D} (f : H.obj X ⟶ X') :
     (α ≫ β).app X ≫ f = α.app X ≫ β.app X ≫ f := by rw [comp_app, assoc]
 #align category_theory.nat_trans.comp_app_assoc CategoryTheory.NatTrans.comp_app_assoc
+-/
 
 #print CategoryTheory.NatTrans.app_naturality /-
 theorem app_naturality {F G : C ⥤ D ⥤ E} (T : F ⟶ G) (X : C) {Y Z : D} (f : Y ⟶ Z) :

Mathbin/CategoryTheory/Limits/Final.lean

@@ -450,10 +450,10 @@ theorem zigzag_of_eqvGen_quot_rel {F : C ⥤ D} {d : D} {f₁ f₂ : Σ X, d ⟶
 #align category_theory.functor.final.zigzag_of_eqv_gen_quot_rel CategoryTheory.Functor.Final.zigzag_of_eqvGen_quot_rel
 -/
 
-#print CategoryTheory.Functor.Final.cofinal_of_colimit_comp_coyoneda_iso_pUnit /-
+#print CategoryTheory.Functor.cofinal_of_colimit_comp_coyoneda_iso_pUnit /-
 /-- If `colimit (F ⋙ coyoneda.obj (op d)) ≅ punit` for all `d : D`, then `F` is cofinal.
 -/
-theorem cofinal_of_colimit_comp_coyoneda_iso_pUnit
+theorem CategoryTheory.Functor.cofinal_of_colimit_comp_coyoneda_iso_pUnit
     (I : ∀ d, colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit) : Final F :=
   ⟨fun d =>
     by
@@ -471,7 +471,7 @@ theorem cofinal_of_colimit_comp_coyoneda_iso_pUnit
     have t := Types.colimit_eq.{v, v} e
     clear e y₁ y₂
     exact zigzag_of_eqv_gen_quot_rel t⟩
-#align category_theory.functor.final.cofinal_of_colimit_comp_coyoneda_iso_punit CategoryTheory.Functor.Final.cofinal_of_colimit_comp_coyoneda_iso_pUnit
+#align category_theory.functor.final.cofinal_of_colimit_comp_coyoneda_iso_punit CategoryTheory.Functor.cofinal_of_colimit_comp_coyoneda_iso_pUnit
 -/
 
 end Final

Mathbin/Data/Finset/Lattice.lean

@@ -2225,35 +2225,35 @@ theorem exists_min_image (s : Finset β) (f : β → α) (h : s.Nonempty) :
 
 end ExistsMaxMin
 
-#print Finset.is_glb_iff_is_least /-
-theorem is_glb_iff_is_least [LinearOrder α] (i : α) (s : Finset α) (hs : s.Nonempty) :
+#print Finset.isGLB_iff_isLeast /-
+theorem isGLB_iff_isLeast [LinearOrder α] (i : α) (s : Finset α) (hs : s.Nonempty) :
     IsGLB (s : Set α) i ↔ IsLeast (↑s) i :=
   by
   refine' ⟨fun his => _, IsLeast.isGLB⟩
   suffices i = min' s hs by rw [this]; exact is_least_min' s hs
   rw [IsGLB, IsGreatest, mem_lowerBounds, mem_upperBounds] at his 
   exact le_antisymm (his.1 (Finset.min' s hs) (Finset.min'_mem s hs)) (his.2 _ (Finset.min'_le s))
-#align finset.is_glb_iff_is_least Finset.is_glb_iff_is_least
+#align finset.is_glb_iff_is_least Finset.isGLB_iff_isLeast
 -/
 
-#print Finset.is_lub_iff_is_greatest /-
-theorem is_lub_iff_is_greatest [LinearOrder α] (i : α) (s : Finset α) (hs : s.Nonempty) :
+#print Finset.isLUB_iff_isGreatest /-
+theorem isLUB_iff_isGreatest [LinearOrder α] (i : α) (s : Finset α) (hs : s.Nonempty) :
     IsLUB (s : Set α) i ↔ IsGreatest (↑s) i :=
-  @is_glb_iff_is_least αᵒᵈ _ i s hs
-#align finset.is_lub_iff_is_greatest Finset.is_lub_iff_is_greatest
+  @isGLB_iff_isLeast αᵒᵈ _ i s hs
+#align finset.is_lub_iff_is_greatest Finset.isLUB_iff_isGreatest
 -/
 
-#print Finset.is_glb_mem /-
-theorem is_glb_mem [LinearOrder α] {i : α} (s : Finset α) (his : IsGLB (s : Set α) i)
+#print Finset.isGLB_mem /-
+theorem isGLB_mem [LinearOrder α] {i : α} (s : Finset α) (his : IsGLB (s : Set α) i)
     (hs : s.Nonempty) : i ∈ s := by rw [← mem_coe]; exact ((is_glb_iff_is_least i s hs).mp his).1
-#align finset.is_glb_mem Finset.is_glb_mem
+#align finset.is_glb_mem Finset.isGLB_mem
 -/
 
-#print Finset.is_lub_mem /-
-theorem is_lub_mem [LinearOrder α] {i : α} (s : Finset α) (his : IsLUB (s : Set α) i)
+#print Finset.isLUB_mem /-
+theorem isLUB_mem [LinearOrder α] {i : α} (s : Finset α) (his : IsLUB (s : Set α) i)
     (hs : s.Nonempty) : i ∈ s :=
-  @is_glb_mem αᵒᵈ _ i s his hs
-#align finset.is_lub_mem Finset.is_lub_mem
+  @isGLB_mem αᵒᵈ _ i s his hs
+#align finset.is_lub_mem Finset.isLUB_mem
 -/
 
 end Finset

Mathbin/Data/Fintype/Card.lean

@@ -866,28 +866,28 @@ variable [Fintype α] [Fintype β]
 
 open Fintype
 
-#print Equiv.ofLeftInverseOfCardLe /-
+#print Equiv.ofLeftInverseOfCardLE /-
 /-- Construct an equivalence from functions that are inverse to each other. -/
 @[simps]
-def ofLeftInverseOfCardLe (hβα : card β ≤ card α) (f : α → β) (g : β → α) (h : LeftInverse g f) :
+def ofLeftInverseOfCardLE (hβα : card β ≤ card α) (f : α → β) (g : β → α) (h : LeftInverse g f) :
     α ≃ β where
   toFun := f
   invFun := g
   left_inv := h
   right_inv := h.rightInverse_of_card_le hβα
-#align equiv.of_left_inverse_of_card_le Equiv.ofLeftInverseOfCardLe
+#align equiv.of_left_inverse_of_card_le Equiv.ofLeftInverseOfCardLE
 -/
 
-#print Equiv.ofRightInverseOfCardLe /-
+#print Equiv.ofRightInverseOfCardLE /-
 /-- Construct an equivalence from functions that are inverse to each other. -/
 @[simps]
-def ofRightInverseOfCardLe (hαβ : card α ≤ card β) (f : α → β) (g : β → α) (h : RightInverse g f) :
+def ofRightInverseOfCardLE (hαβ : card α ≤ card β) (f : α → β) (g : β → α) (h : RightInverse g f) :
     α ≃ β where
   toFun := f
   invFun := g
   left_inv := h.leftInverse_of_card_le hαβ
   right_inv := h
-#align equiv.of_right_inverse_of_card_le Equiv.ofRightInverseOfCardLe
+#align equiv.of_right_inverse_of_card_le Equiv.ofRightInverseOfCardLE
 -/
 
 end Equiv
@@ -922,11 +922,11 @@ noncomputable def Finset.equivOfCardEq {s t : Finset α} (h : s.card = t.card) :
 #align finset.equiv_of_card_eq Finset.equivOfCardEq
 -/
 
-#print Fintype.card_Prop /-
+#print Fintype.card_prop /-
 @[simp]
-theorem Fintype.card_Prop : Fintype.card Prop = 2 :=
+theorem Fintype.card_prop : Fintype.card Prop = 2 :=
   rfl
-#align fintype.card_Prop Fintype.card_Prop
+#align fintype.card_Prop Fintype.card_prop
 -/
 
 #print set_fintype_card_le_univ /-
@@ -959,28 +959,28 @@ theorem equiv_of_fintype_self_embedding_to_embedding [Finite α] (e : α ↪ α)
 #align function.embedding.equiv_of_fintype_self_embedding_to_embedding Function.Embedding.equiv_of_fintype_self_embedding_to_embedding
 -/
 
-#print Function.Embedding.is_empty_of_card_lt /-
+#print Function.Embedding.isEmpty_of_card_lt /-
 /-- If `‖β‖ < ‖α‖` there are no embeddings `α ↪ β`.
 This is a formulation of the pigeonhole principle.
 
 Note this cannot be an instance as it needs `h`. -/
 @[simp]
-theorem is_empty_of_card_lt [Fintype α] [Fintype β] (h : Fintype.card β < Fintype.card α) :
+theorem isEmpty_of_card_lt [Fintype α] [Fintype β] (h : Fintype.card β < Fintype.card α) :
     IsEmpty (α ↪ β) :=
   ⟨fun f =>
     let ⟨x, y, Ne, feq⟩ := Fintype.exists_ne_map_eq_of_card_lt f h
     Ne <| f.Injective feq⟩
-#align function.embedding.is_empty_of_card_lt Function.Embedding.is_empty_of_card_lt
+#align function.embedding.is_empty_of_card_lt Function.Embedding.isEmpty_of_card_lt
 -/
 
-#print Function.Embedding.truncOfCardLe /-
+#print Function.Embedding.truncOfCardLE /-
 /-- A constructive embedding of a fintype `α` in another fintype `β` when `card α ≤ card β`. -/
-def truncOfCardLe [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β]
+def truncOfCardLE [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β]
     (h : Fintype.card α ≤ Fintype.card β) : Trunc (α ↪ β) :=
   (Fintype.truncEquivFin α).bind fun ea =>
     (Fintype.truncEquivFin β).map fun eb =>
       ea.toEmbedding.trans ((Fin.castLEEmb h).toEmbedding.trans eb.symm.toEmbedding)
-#align function.embedding.trunc_of_card_le Function.Embedding.truncOfCardLe
+#align function.embedding.trunc_of_card_le Function.Embedding.truncOfCardLE
 -/
 
 #print Function.Embedding.nonempty_of_card_le /-
@@ -1160,11 +1160,11 @@ protected theorem Fintype.false [Infinite α] (h : Fintype α) : False :=
 #align fintype.false Fintype.false
 -/
 
-#print is_empty_fintype /-
+#print isEmpty_fintype /-
 @[simp]
-theorem is_empty_fintype {α : Type _} : IsEmpty (Fintype α) ↔ Infinite α :=
+theorem isEmpty_fintype {α : Type _} : IsEmpty (Fintype α) ↔ Infinite α :=
   ⟨fun ⟨h⟩ => ⟨fun h' => (@nonempty_fintype α h').elim h⟩, fun ⟨h⟩ => ⟨fun h' => h h'.Finite⟩⟩
-#align is_empty_fintype is_empty_fintype
+#align is_empty_fintype isEmpty_fintype
 -/
 
 #print fintypeOfNotInfinite /-
@@ -1211,7 +1211,7 @@ namespace Infinite
 
 #print Infinite.of_not_fintype /-
 theorem of_not_fintype (h : Fintype α → False) : Infinite α :=
-  is_empty_fintype.mp ⟨h⟩
+  isEmpty_fintype.mp ⟨h⟩
 #align infinite.of_not_fintype Infinite.of_not_fintype
 -/
 

Mathbin/Data/Real/Ereal.lean

@@ -78,11 +78,11 @@ def Real.toEReal : ℝ → EReal :=
 
 namespace EReal
 
-#print EReal.decidableLt /-
+#print EReal.decidableLT /-
 -- things unify with `with_bot.decidable_lt` later if we we don't provide this explicitly.
-instance decidableLt : DecidableRel ((· < ·) : EReal → EReal → Prop) :=
+instance decidableLT : DecidableRel ((· < ·) : EReal → EReal → Prop) :=
   WithBot.decidableLT
-#align ereal.decidable_lt EReal.decidableLt
+#align ereal.decidable_lt EReal.decidableLT
 -/
 
 -- TODO: Provide explicitly, otherwise it is inferred noncomputably from `complete_linear_order`

Mathbin/GroupTheory/Congruence.lean

@@ -1503,12 +1503,12 @@ end Units
 
 section Actions
 
-#print Con.smulinst /-
+#print Con.instSMul /-
 @[to_additive]
-instance smulinst {α M : Type _} [MulOneClass M] [SMul α M] [IsScalarTower α M M] (c : Con M) :
+instance instSMul {α M : Type _} [MulOneClass M] [SMul α M] [IsScalarTower α M M] (c : Con M) :
     SMul α c.Quotient where smul a := Quotient.map' ((· • ·) a) fun x y => c.smul a
-#align con.has_smul Con.smulinst
-#align add_con.has_vadd AddCon.smulinst
+#align con.has_smul Con.instSMul
+#align add_con.has_vadd AddCon.instVAdd
 -/
 
 #print Con.coe_smul /-