diff --git a/Mathbin/Algebra/Order/Hom/Ring.lean b/Mathbin/Algebra/Order/Hom/Ring.lean
index 5a1544b749..f6afaf45c0 100644
--- a/Mathbin/Algebra/Order/Hom/Ring.lean
+++ b/Mathbin/Algebra/Order/Hom/Ring.lean
@@ -301,26 +301,26 @@ theorem id_apply (a : α) : OrderRingHom.id α a = a :=
 #align order_ring_hom.id_apply OrderRingHom.id_apply
 -/
 
-#print OrderRingHom.coe_RingHom_id /-
+#print OrderRingHom.coe_ringHom_id /-
 @[simp]
-theorem coe_RingHom_id : (OrderRingHom.id α : α →+* α) = RingHom.id α :=
+theorem coe_ringHom_id : (OrderRingHom.id α : α →+* α) = RingHom.id α :=
   rfl
-#align order_ring_hom.coe_ring_hom_id OrderRingHom.coe_RingHom_id
+#align order_ring_hom.coe_ring_hom_id OrderRingHom.coe_ringHom_id
 -/
 
-#print OrderRingHom.coe_OrderAddMonoidHom_id /-
+#print OrderRingHom.coe_orderAddMonoidHom_id /-
 @[simp]
-theorem coe_OrderAddMonoidHom_id : (OrderRingHom.id α : α →+o α) = OrderAddMonoidHom.id α :=
+theorem coe_orderAddMonoidHom_id : (OrderRingHom.id α : α →+o α) = OrderAddMonoidHom.id α :=
   rfl
-#align order_ring_hom.coe_order_add_monoid_hom_id OrderRingHom.coe_OrderAddMonoidHom_id
+#align order_ring_hom.coe_order_add_monoid_hom_id OrderRingHom.coe_orderAddMonoidHom_id
 -/
 
-#print OrderRingHom.coe_OrderMonoidWithZeroHom_id /-
+#print OrderRingHom.coe_orderMonoidWithZeroHom_id /-
 @[simp]
-theorem coe_OrderMonoidWithZeroHom_id :
+theorem coe_orderMonoidWithZeroHom_id :
     (OrderRingHom.id α : α →*₀o α) = OrderMonoidWithZeroHom.id α :=
   rfl
-#align order_ring_hom.coe_order_monoid_with_zero_hom_id OrderRingHom.coe_OrderMonoidWithZeroHom_id
+#align order_ring_hom.coe_order_monoid_with_zero_hom_id OrderRingHom.coe_orderMonoidWithZeroHom_id
 -/
 
 #print OrderRingHom.comp /-
diff --git a/Mathbin/Algebra/Order/LatticeGroup.lean b/Mathbin/Algebra/Order/LatticeGroup.lean
index f31dffbb30..e2e4b47c72 100644
--- a/Mathbin/Algebra/Order/LatticeGroup.lean
+++ b/Mathbin/Algebra/Order/LatticeGroup.lean
@@ -662,15 +662,15 @@ theorem mabs_mul_le [CovariantClass α α (· * ·) (· ≤ ·)] (a b : α) : |a
 #align lattice_ordered_comm_group.abs_add_le LatticeOrderedCommGroup.abs_add_le
 -/
 
-#print LatticeOrderedCommGroup.abs_inv_comm /-
+#print LatticeOrderedCommGroup.abs_div_comm /-
 -- |a - b| = |b - a|
 @[to_additive]
-theorem abs_inv_comm (a b : α) : |a / b| = |b / a| :=
+theorem abs_div_comm (a b : α) : |a / b| = |b / a| :=
   by
   unfold Abs.abs
   rw [inv_div a b, ← inv_inv (a / b), inv_div, sup_comm]
-#align lattice_ordered_comm_group.abs_inv_comm LatticeOrderedCommGroup.abs_inv_comm
-#align lattice_ordered_comm_group.abs_neg_comm LatticeOrderedCommGroup.abs_neg_comm
+#align lattice_ordered_comm_group.abs_inv_comm LatticeOrderedCommGroup.abs_div_comm
+#align lattice_ordered_comm_group.abs_neg_comm LatticeOrderedCommGroup.abs_sub_comm
 -/
 
 #print LatticeOrderedCommGroup.abs_abs_div_abs_le /-
diff --git a/Mathbin/Algebra/Ring/BooleanRing.lean b/Mathbin/Algebra/Ring/BooleanRing.lean
index cc7e5215f0..a3a6c70bc7 100644
--- a/Mathbin/Algebra/Ring/BooleanRing.lean
+++ b/Mathbin/Algebra/Ring/BooleanRing.lean
@@ -682,7 +682,7 @@ protected def BoundedLatticeHom.asBoolRing (f : BoundedLatticeHom α β) :
   toFun := toBoolRing ∘ f ∘ ofBoolRing
   map_zero' := f.map_bot'
   map_one' := f.map_top'
-  map_add' := map_symm_diff' f
+  map_add' := map_symmDiff' f
   map_mul' := f.map_inf'
 #align bounded_lattice_hom.as_boolring BoundedLatticeHom.asBoolRing
 -/
diff --git a/Mathbin/Data/Finset/Image.lean b/Mathbin/Data/Finset/Image.lean
index 3892df70ed..fadfeda033 100644
--- a/Mathbin/Data/Finset/Image.lean
+++ b/Mathbin/Data/Finset/Image.lean
@@ -684,7 +684,7 @@ theorem image_sdiff [DecidableEq α] {f : α → β} (s t : Finset α) (hf : Inj
 #print Finset.image_symmDiff /-
 theorem image_symmDiff [DecidableEq α] {f : α → β} (s t : Finset α) (hf : Injective f) :
     (s ∆ t).image f = s.image f ∆ t.image f :=
-  coe_injective <| by push_cast ; exact Set.image_symm_diff hf _ _
+  coe_injective <| by push_cast ; exact Set.image_symmDiff hf _ _
 #align finset.image_symm_diff Finset.image_symmDiff
 -/
 
diff --git a/Mathbin/Data/Finset/Pointwise.lean b/Mathbin/Data/Finset/Pointwise.lean
index a3636c4b11..a54ceef1f7 100644
--- a/Mathbin/Data/Finset/Pointwise.lean
+++ b/Mathbin/Data/Finset/Pointwise.lean
@@ -2633,10 +2633,10 @@ theorem smul_finset_sdiff₀ (ha : a ≠ 0) : a • (s \ t) = a • s \ a • t
 #align finset.smul_finset_sdiff₀ Finset.smul_finset_sdiff₀
 -/
 
-#print Finset.smul_finset_symm_diff₀ /-
-theorem smul_finset_symm_diff₀ (ha : a ≠ 0) : a • s ∆ t = (a • s) ∆ (a • t) :=
+#print Finset.smul_finset_symmDiff₀ /-
+theorem smul_finset_symmDiff₀ (ha : a ≠ 0) : a • s ∆ t = (a • s) ∆ (a • t) :=
   image_symmDiff _ _ <| MulAction.injective₀ ha
-#align finset.smul_finset_symm_diff₀ Finset.smul_finset_symm_diff₀
+#align finset.smul_finset_symm_diff₀ Finset.smul_finset_symmDiff₀
 -/
 
 #print Finset.smul_univ₀ /-
diff --git a/Mathbin/Data/LazyList/Basic.lean b/Mathbin/Data/LazyList/Basic.lean
index 6dc060c437..afbfbbc230 100644
--- a/Mathbin/Data/LazyList/Basic.lean
+++ b/Mathbin/Data/LazyList/Basic.lean
@@ -25,10 +25,10 @@ universe u
 
 namespace Thunk
 
-#print Thunk.pure /-
+#print Thunk.mk /-
 /-- Creates a thunk with a (non-lazy) constant value. -/
-def pure {α} (x : α) : Thunk α := fun _ => x
-#align thunk.mk Thunk.pure
+def mk {α} (x : α) : Thunk α := fun _ => x
+#align thunk.mk Thunk.mk
 -/
 
 instance {α : Type u} [DecidableEq α] : DecidableEq (Thunk α)
@@ -74,7 +74,7 @@ instance {α : Type u} [DecidableEq α] : DecidableEq (LazyList α)
 protected def traverse {m : Type u → Type u} [Applicative m] {α β : Type u} (f : α → m β) :
     LazyList α → m (LazyList β)
   | LazyList.nil => pure LazyList.nil
-  | LazyList.cons x xs => LazyList.cons <$> f x <*> Thunk.pure <$> traverse (xs ())
+  | LazyList.cons x xs => LazyList.cons <$> f x <*> Thunk.mk <$> traverse (xs ())
 #align lazy_list.traverse LazyList.traverse
 -/
 
diff --git a/Mathbin/Data/Set/Image.lean b/Mathbin/Data/Set/Image.lean
index 17c8a1fac0..a2bda4765f 100644
--- a/Mathbin/Data/Set/Image.lean
+++ b/Mathbin/Data/Set/Image.lean
@@ -548,11 +548,11 @@ theorem subset_image_diff (f : α → β) (s t : Set α) : f '' s \ f '' t ⊆ f
 #align set.subset_image_diff Set.subset_image_diff
 -/
 
-#print Set.subset_image_symm_diff /-
-theorem subset_image_symm_diff : (f '' s) ∆ (f '' t) ⊆ f '' s ∆ t :=
+#print Set.subset_image_symmDiff /-
+theorem subset_image_symmDiff : (f '' s) ∆ (f '' t) ⊆ f '' s ∆ t :=
   (union_subset_union (subset_image_diff _ _ _) <| subset_image_diff _ _ _).trans
     (image_union _ _ _).Superset
-#align set.subset_image_symm_diff Set.subset_image_symm_diff
+#align set.subset_image_symm_diff Set.subset_image_symmDiff
 -/
 
 #print Set.image_diff /-
@@ -563,10 +563,10 @@ theorem image_diff {f : α → β} (hf : Injective f) (s t : Set α) : f '' (s \
 #align set.image_diff Set.image_diff
 -/
 
-#print Set.image_symm_diff /-
-theorem image_symm_diff (hf : Injective f) (s t : Set α) : f '' s ∆ t = (f '' s) ∆ (f '' t) := by
+#print Set.image_symmDiff /-
+theorem image_symmDiff (hf : Injective f) (s t : Set α) : f '' s ∆ t = (f '' s) ∆ (f '' t) := by
   simp_rw [Set.symmDiff_def, image_union, image_diff hf]
-#align set.image_symm_diff Set.image_symm_diff
+#align set.image_symm_diff Set.image_symmDiff
 -/
 
 #print Set.Nonempty.image /-
diff --git a/Mathbin/Data/Set/Ncard.lean b/Mathbin/Data/Set/Ncard.lean
index 9b95b8e22b..fc47a2a416 100644
--- a/Mathbin/Data/Set/Ncard.lean
+++ b/Mathbin/Data/Set/Ncard.lean
@@ -757,8 +757,8 @@ theorem ncard_union_eq (h : Disjoint s t)
 -/
 
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic to_finite_tac -/
-#print Set.ncard_diff_add_ncard_eq_ncard /-
-theorem ncard_diff_add_ncard_eq_ncard (h : s ⊆ t)
+#print Set.ncard_diff_add_ncard_of_subset /-
+theorem ncard_diff_add_ncard_of_subset (h : s ⊆ t)
     (ht : t.Finite := by
       run_tac
         to_finite_tac) :
@@ -768,7 +768,7 @@ theorem ncard_diff_add_ncard_eq_ncard (h : s ⊆ t)
     ncard_eq_to_finset_card _ (ht.diff s), finite.to_finset_diff]
   refine' Finset.card_sdiff_add_card_eq_card _
   rwa [finite.to_finset_subset_to_finset]
-#align set.ncard_diff_add_ncard_eq_ncard Set.ncard_diff_add_ncard_eq_ncard
+#align set.ncard_diff_add_ncard_eq_ncard Set.ncard_diff_add_ncard_of_subset
 -/
 
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic to_finite_tac -/
diff --git a/Mathbin/Data/Set/Pointwise/Smul.lean b/Mathbin/Data/Set/Pointwise/Smul.lean
index 11b6aa6b7f..9e9e8bc2ab 100644
--- a/Mathbin/Data/Set/Pointwise/Smul.lean
+++ b/Mathbin/Data/Set/Pointwise/Smul.lean
@@ -1222,12 +1222,12 @@ theorem smul_set_sdiff : a • (s \ t) = a • s \ a • t :=
 #align set.vadd_set_sdiff Set.vadd_set_sdiff
 -/
 
-#print Set.smul_set_symm_diff /-
+#print Set.smul_set_symmDiff /-
 @[to_additive]
-theorem smul_set_symm_diff : a • s ∆ t = (a • s) ∆ (a • t) :=
-  image_symm_diff (MulAction.injective a) _ _
-#align set.smul_set_symm_diff Set.smul_set_symm_diff
-#align set.vadd_set_symm_diff Set.vadd_set_symm_diff
+theorem smul_set_symmDiff : a • s ∆ t = (a • s) ∆ (a • t) :=
+  image_symmDiff (MulAction.injective a) _ _
+#align set.smul_set_symm_diff Set.smul_set_symmDiff
+#align set.vadd_set_symm_diff Set.vadd_set_symmDiff
 -/
 
 #print Set.smul_set_univ /-
@@ -1373,10 +1373,10 @@ theorem smul_set_sdiff₀ (ha : a ≠ 0) : a • (s \ t) = a • s \ a • t :=
 #align set.smul_set_sdiff₀ Set.smul_set_sdiff₀
 -/
 
-#print Set.smul_set_symm_diff₀ /-
-theorem smul_set_symm_diff₀ (ha : a ≠ 0) : a • s ∆ t = (a • s) ∆ (a • t) :=
-  image_symm_diff (MulAction.injective₀ ha) _ _
-#align set.smul_set_symm_diff₀ Set.smul_set_symm_diff₀
+#print Set.smul_set_symmDiff₀ /-
+theorem smul_set_symmDiff₀ (ha : a ≠ 0) : a • s ∆ t = (a • s) ∆ (a • t) :=
+  image_symmDiff (MulAction.injective₀ ha) _ _
+#align set.smul_set_symm_diff₀ Set.smul_set_symmDiff₀
 -/
 
 #print Set.smul_set_univ₀ /-
diff --git a/Mathbin/FieldTheory/SplittingField/Construction.lean b/Mathbin/FieldTheory/SplittingField/Construction.lean
index df10532839..3de57148c8 100644
--- a/Mathbin/FieldTheory/SplittingField/Construction.lean
+++ b/Mathbin/FieldTheory/SplittingField/Construction.lean
@@ -314,7 +314,7 @@ instance inhabited : Inhabited (SplittingField f) :=
 -/
 
 instance {S : Type _} [DistribSMul S K] [IsScalarTower S K K] : SMul S (SplittingField f) :=
-  Submodule.Quotient.hasSmul' _
+  Submodule.Quotient.instSMul' _
 
 #print Polynomial.SplittingField.algebra /-
 instance algebra : Algebra K (SplittingField f) :=
diff --git a/Mathbin/LinearAlgebra/Quotient.lean b/Mathbin/LinearAlgebra/Quotient.lean
index 65767b1d62..0321e451c4 100644
--- a/Mathbin/LinearAlgebra/Quotient.lean
+++ b/Mathbin/LinearAlgebra/Quotient.lean
@@ -147,19 +147,19 @@ section SMul
 
 variable {S : Type _} [SMul S R] [SMul S M] [IsScalarTower S R M] (P : Submodule R M)
 
-#print Submodule.Quotient.hasSmul' /-
-instance hasSmul' : SMul S (M ⧸ P) :=
+#print Submodule.Quotient.instSMul' /-
+instance instSMul' : SMul S (M ⧸ P) :=
   ⟨fun a =>
     Quotient.map' ((· • ·) a) fun x y h =>
       leftRel_apply.mpr <| by simpa [smul_sub] using P.smul_mem (a • 1 : R) (left_rel_apply.mp h)⟩
-#align submodule.quotient.has_smul' Submodule.Quotient.hasSmul'
+#align submodule.quotient.has_smul' Submodule.Quotient.instSMul'
 -/
 
-#print Submodule.Quotient.hasSmul /-
+#print Submodule.Quotient.instSMul /-
 /-- Shortcut to help the elaborator in the common case. -/
-instance hasSmul : SMul R (M ⧸ P) :=
-  Quotient.hasSmul' P
-#align submodule.quotient.has_smul Submodule.Quotient.hasSmul
+instance instSMul : SMul R (M ⧸ P) :=
+  Quotient.instSMul' P
+#align submodule.quotient.has_smul Submodule.Quotient.instSMul
 -/
 
 #print Submodule.Quotient.mk_smul /-
@@ -222,18 +222,18 @@ instance smulZeroClass (P : Submodule R M) : SMulZeroClass R (M ⧸ P) :=
 #align submodule.quotient.smul_zero_class Submodule.Quotient.smulZeroClass
 -/
 
-#print Submodule.Quotient.distribSmul' /-
-instance distribSmul' [SMul S R] [DistribSMul S M] [IsScalarTower S R M] (P : Submodule R M) :
+#print Submodule.Quotient.distribSMul' /-
+instance distribSMul' [SMul S R] [DistribSMul S M] [IsScalarTower S R M] (P : Submodule R M) :
     DistribSMul S (M ⧸ P) :=
   Function.Surjective.distribSMul ⟨mk, rfl, fun _ _ => rfl⟩ (surjective_quot_mk _)
     P.Quotient.mk_smul
-#align submodule.quotient.distrib_smul' Submodule.Quotient.distribSmul'
+#align submodule.quotient.distrib_smul' Submodule.Quotient.distribSMul'
 -/
 
-#print Submodule.Quotient.distribSmul /-
-instance distribSmul (P : Submodule R M) : DistribSMul R (M ⧸ P) :=
-  Quotient.distribSmul' P
-#align submodule.quotient.distrib_smul Submodule.Quotient.distribSmul
+#print Submodule.Quotient.distribSMul /-
+instance distribSMul (P : Submodule R M) : DistribSMul R (M ⧸ P) :=
+  Quotient.distribSMul' P
+#align submodule.quotient.distrib_smul Submodule.Quotient.distribSMul
 -/
 
 #print Submodule.Quotient.distribMulAction' /-
diff --git a/Mathbin/Order/Hom/Lattice.lean b/Mathbin/Order/Hom/Lattice.lean
index 8d9a12c217..ee6de8f4b8 100644
--- a/Mathbin/Order/Hom/Lattice.lean
+++ b/Mathbin/Order/Hom/Lattice.lean
@@ -325,11 +325,11 @@ theorem map_sdiff' (a b : α) : f (a \ b) = f a \ f b := by
 #align map_sdiff' map_sdiff'
 -/
 
-#print map_symm_diff' /-
+#print map_symmDiff' /-
 /-- Special case of `map_symm_diff` for boolean algebras. -/
-theorem map_symm_diff' (a b : α) : f (a ∆ b) = f a ∆ f b := by
+theorem map_symmDiff' (a b : α) : f (a ∆ b) = f a ∆ f b := by
   rw [symmDiff, symmDiff, map_sup, map_sdiff', map_sdiff']
-#align map_symm_diff' map_symm_diff'
+#align map_symm_diff' map_symmDiff'
 -/
 
 end BooleanAlgebra
diff --git a/Mathbin/Order/LiminfLimsup.lean b/Mathbin/Order/LiminfLimsup.lean
index 40f9f5f92f..7408d64e01 100644
--- a/Mathbin/Order/LiminfLimsup.lean
+++ b/Mathbin/Order/LiminfLimsup.lean
@@ -1554,8 +1554,8 @@ section Order
 
 open Filter
 
-#print Monotone.isBoundedUnder_le_comp /-
-theorem Monotone.isBoundedUnder_le_comp [Nonempty β] [LinearOrder β] [Preorder γ] [NoMaxOrder γ]
+#print Monotone.isBoundedUnder_le_comp_iff /-
+theorem Monotone.isBoundedUnder_le_comp_iff [Nonempty β] [LinearOrder β] [Preorder γ] [NoMaxOrder γ]
     {g : β → γ} {f : α → β} {l : Filter α} (hg : Monotone g) (hg' : Tendsto g atTop atTop) :
     IsBoundedUnder (· ≤ ·) l (g ∘ f) ↔ IsBoundedUnder (· ≤ ·) l f :=
   by
@@ -1563,31 +1563,31 @@ theorem Monotone.isBoundedUnder_le_comp [Nonempty β] [LinearOrder β] [Preorder
   rintro ⟨c, hc⟩; rw [eventually_map] at hc 
   obtain ⟨b, hb⟩ : ∃ b, ∀ a ≥ b, c < g a := eventually_at_top.1 (hg'.eventually_gt_at_top c)
   exact ⟨b, hc.mono fun x hx => not_lt.1 fun h => (hb _ h.le).not_le hx⟩
-#align monotone.is_bounded_under_le_comp Monotone.isBoundedUnder_le_comp
+#align monotone.is_bounded_under_le_comp Monotone.isBoundedUnder_le_comp_iff
 -/
 
-#print Monotone.isBoundedUnder_ge_comp /-
-theorem Monotone.isBoundedUnder_ge_comp [Nonempty β] [LinearOrder β] [Preorder γ] [NoMinOrder γ]
+#print Monotone.isBoundedUnder_ge_comp_iff /-
+theorem Monotone.isBoundedUnder_ge_comp_iff [Nonempty β] [LinearOrder β] [Preorder γ] [NoMinOrder γ]
     {g : β → γ} {f : α → β} {l : Filter α} (hg : Monotone g) (hg' : Tendsto g atBot atBot) :
     IsBoundedUnder (· ≥ ·) l (g ∘ f) ↔ IsBoundedUnder (· ≥ ·) l f :=
   hg.dual.isBoundedUnder_le_comp hg'
-#align monotone.is_bounded_under_ge_comp Monotone.isBoundedUnder_ge_comp
+#align monotone.is_bounded_under_ge_comp Monotone.isBoundedUnder_ge_comp_iff
 -/
 
-#print Antitone.isBoundedUnder_le_comp /-
-theorem Antitone.isBoundedUnder_le_comp [Nonempty β] [LinearOrder β] [Preorder γ] [NoMaxOrder γ]
+#print Antitone.isBoundedUnder_le_comp_iff /-
+theorem Antitone.isBoundedUnder_le_comp_iff [Nonempty β] [LinearOrder β] [Preorder γ] [NoMaxOrder γ]
     {g : β → γ} {f : α → β} {l : Filter α} (hg : Antitone g) (hg' : Tendsto g atBot atTop) :
     IsBoundedUnder (· ≤ ·) l (g ∘ f) ↔ IsBoundedUnder (· ≥ ·) l f :=
   hg.dual_right.isBoundedUnder_ge_comp hg'
-#align antitone.is_bounded_under_le_comp Antitone.isBoundedUnder_le_comp
+#align antitone.is_bounded_under_le_comp Antitone.isBoundedUnder_le_comp_iff
 -/
 
-#print Antitone.isBoundedUnder_ge_comp /-
-theorem Antitone.isBoundedUnder_ge_comp [Nonempty β] [LinearOrder β] [Preorder γ] [NoMinOrder γ]
+#print Antitone.isBoundedUnder_ge_comp_iff /-
+theorem Antitone.isBoundedUnder_ge_comp_iff [Nonempty β] [LinearOrder β] [Preorder γ] [NoMinOrder γ]
     {g : β → γ} {f : α → β} {l : Filter α} (hg : Antitone g) (hg' : Tendsto g atTop atBot) :
     IsBoundedUnder (· ≥ ·) l (g ∘ f) ↔ IsBoundedUnder (· ≤ ·) l f :=
   hg.dual_right.isBoundedUnder_le_comp hg'
-#align antitone.is_bounded_under_ge_comp Antitone.isBoundedUnder_ge_comp
+#align antitone.is_bounded_under_ge_comp Antitone.isBoundedUnder_ge_comp_iff
 -/
 
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic is_bounded_default -/
diff --git a/Mathbin/RingTheory/AdjoinRoot.lean b/Mathbin/RingTheory/AdjoinRoot.lean
index fbf9bc7941..8adc23b183 100644
--- a/Mathbin/RingTheory/AdjoinRoot.lean
+++ b/Mathbin/RingTheory/AdjoinRoot.lean
@@ -119,10 +119,10 @@ def of : R →+* AdjoinRoot f :=
 -/
 
 instance [DistribSMul S R] [IsScalarTower S R R] : SMul S (AdjoinRoot f) :=
-  Submodule.Quotient.hasSmul' _
+  Submodule.Quotient.instSMul' _
 
 instance [DistribSMul S R] [IsScalarTower S R R] : DistribSMul S (AdjoinRoot f) :=
-  Submodule.Quotient.distribSmul' _
+  Submodule.Quotient.distribSMul' _
 
 #print AdjoinRoot.smul_mk /-
 @[simp]
diff --git a/Mathbin/Topology/Algebra/Order/MonotoneConvergence.lean b/Mathbin/Topology/Algebra/Order/MonotoneConvergence.lean
index 6a8de61d05..fe4183a46e 100644
--- a/Mathbin/Topology/Algebra/Order/MonotoneConvergence.lean
+++ b/Mathbin/Topology/Algebra/Order/MonotoneConvergence.lean
@@ -245,18 +245,18 @@ instance {ι : Type _} {α : ι → Type _} [∀ i, Preorder (α i)] [∀ i, Top
     [∀ i, InfConvergenceClass (α i)] : InfConvergenceClass (∀ i, α i) :=
   show InfConvergenceClass (∀ i, (α i)ᵒᵈ)ᵒᵈ from OrderDual.infConvergenceClass
 
-#print Pi.Sup_convergence_class' /-
-instance Pi.Sup_convergence_class' {ι : Type _} [Preorder α] [TopologicalSpace α]
+#print Pi.supConvergenceClass' /-
+instance Pi.supConvergenceClass' {ι : Type _} [Preorder α] [TopologicalSpace α]
     [SupConvergenceClass α] : SupConvergenceClass (ι → α) :=
   Pi.supConvergenceClass
-#align pi.Sup_convergence_class' Pi.Sup_convergence_class'
+#align pi.Sup_convergence_class' Pi.supConvergenceClass'
 -/
 
-#print Pi.Inf_convergence_class' /-
-instance Pi.Inf_convergence_class' {ι : Type _} [Preorder α] [TopologicalSpace α]
+#print Pi.infConvergenceClass' /-
+instance Pi.infConvergenceClass' {ι : Type _} [Preorder α] [TopologicalSpace α]
     [InfConvergenceClass α] : InfConvergenceClass (ι → α) :=
   Pi.infConvergenceClass
-#align pi.Inf_convergence_class' Pi.Inf_convergence_class'
+#align pi.Inf_convergence_class' Pi.infConvergenceClass'
 -/
 
 #print tendsto_of_monotone /-
diff --git a/Mathbin/Topology/ContinuousFunction/Algebra.lean b/Mathbin/Topology/ContinuousFunction/Algebra.lean
index c5a93ebe05..4a758d0b86 100644
--- a/Mathbin/Topology/ContinuousFunction/Algebra.lean
+++ b/Mathbin/Topology/ContinuousFunction/Algebra.lean
@@ -1025,7 +1025,6 @@ section
 
 variable {R : Type _} [LinearOrderedField R]
 
-#print min_eq_half_add_sub_abs_sub /-
 -- TODO:
 -- This lemma (and the next) could go all the way back in `algebra.order.field`,
 -- except that it is tedious to prove without tactics.
@@ -1034,13 +1033,10 @@ variable {R : Type _} [LinearOrderedField R]
 theorem min_eq_half_add_sub_abs_sub {x y : R} : min x y = 2⁻¹ * (x + y - |x - y|) := by
   cases' le_total x y with h h <;> field_simp [h, abs_of_nonneg, abs_of_nonpos, mul_two] <;> abel
 #align min_eq_half_add_sub_abs_sub min_eq_half_add_sub_abs_sub
--/
 
-#print max_eq_half_add_add_abs_sub /-
 theorem max_eq_half_add_add_abs_sub {x y : R} : max x y = 2⁻¹ * (x + y + |x - y|) := by
   cases' le_total x y with h h <;> field_simp [h, abs_of_nonneg, abs_of_nonpos, mul_two] <;> abel
 #align max_eq_half_add_add_abs_sub max_eq_half_add_add_abs_sub
--/
 
 end
 
@@ -1053,18 +1049,14 @@ variable {α : Type _} [TopologicalSpace α]
 variable {β : Type _} [LinearOrderedField β] [TopologicalSpace β] [OrderTopology β]
   [TopologicalRing β]
 
-#print ContinuousMap.inf_eq /-
 theorem inf_eq (f g : C(α, β)) : f ⊓ g = (2⁻¹ : β) • (f + g - |f - g|) :=
   ext fun x => by simpa using min_eq_half_add_sub_abs_sub
 #align continuous_map.inf_eq ContinuousMap.inf_eq
--/
 
-#print ContinuousMap.sup_eq /-
 -- Not sure why this is grosser than `inf_eq`:
 theorem sup_eq (f g : C(α, β)) : f ⊔ g = (2⁻¹ : β) • (f + g + |f - g|) :=
   ext fun x => by simpa [mul_add] using @max_eq_half_add_add_abs_sub _ _ (f x) (g x)
 #align continuous_map.sup_eq ContinuousMap.sup_eq
--/
 
 end Lattice
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 7e84b60bd0..e9b76bb78b 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -10,9 +10,9 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "cc4af89ac2712cea90c51bedcb8076e921f4bf3e",
+    "rev": "5d20d9445ac37c664aab52b7f062f6abb939b70d",
     "name": "lean3port",
-    "inputRev?": "cc4af89ac2712cea90c51bedcb8076e921f4bf3e"}},
+    "inputRev?": "5d20d9445ac37c664aab52b7f062f6abb939b70d"}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
     "subDir?": null,
@@ -22,9 +22,9 @@
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "6c5ad83c2ca4a6e03ae9e33fa52220712b8a9faf",
+    "rev": "4f0b2d5b5e6a9cce7a742dd139b3235affa81128",
     "name": "mathlib",
-    "inputRev?": "6c5ad83c2ca4a6e03ae9e33fa52220712b8a9faf"}},
+    "inputRev?": "4f0b2d5b5e6a9cce7a742dd139b3235affa81128"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
diff --git a/lakefile.lean b/lakefile.lean
index 7a238f8130..c6ee2a85bd 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-08-02-07"
+def tag : String := "nightly-2023-08-02-09"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"cc4af89ac2712cea90c51bedcb8076e921f4bf3e"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"5d20d9445ac37c664aab52b7f062f6abb939b70d"
 
 @[default_target]
 lean_lib Mathbin where