diff --git a/Mathbin/Algebra/Hom/Iterate.lean b/Mathbin/Algebra/Hom/Iterate.lean
index c4d04e6d45..6e65291c7a 100644
--- a/Mathbin/Algebra/Hom/Iterate.lean
+++ b/Mathbin/Algebra/Hom/Iterate.lean
@@ -56,13 +56,11 @@ theorem iterate_map_one (f : M →* M) (n : ℕ) : (f^[n]) 1 = 1 :=
 #align add_monoid_hom.iterate_map_zero AddMonoidHom.iterate_map_zero
 -/
 
-#print MonoidHom.iterate_map_mul /-
 @[simp, to_additive]
 theorem iterate_map_mul (f : M →* M) (n : ℕ) (x y) : (f^[n]) (x * y) = (f^[n]) x * (f^[n]) y :=
   Semiconj₂.iterate f.map_mul n x y
 #align monoid_hom.iterate_map_mul MonoidHom.iterate_map_mul
 #align add_monoid_hom.iterate_map_add AddMonoidHom.iterate_map_add
--/
 
 end
 
@@ -163,17 +161,13 @@ theorem iterate_map_zero : (f^[n]) 0 = 0 :=
 #align ring_hom.iterate_map_zero RingHom.iterate_map_zero
 -/
 
-#print RingHom.iterate_map_add /-
 theorem iterate_map_add : (f^[n]) (x + y) = (f^[n]) x + (f^[n]) y :=
   f.toAddMonoidHom.iterate_map_add n x y
 #align ring_hom.iterate_map_add RingHom.iterate_map_add
--/
 
-#print RingHom.iterate_map_mul /-
 theorem iterate_map_mul : (f^[n]) (x * y) = (f^[n]) x * (f^[n]) y :=
   f.toMonoidHom.iterate_map_mul n x y
 #align ring_hom.iterate_map_mul RingHom.iterate_map_mul
--/
 
 #print RingHom.iterate_map_pow /-
 theorem iterate_map_pow (a) (n m : ℕ) : (f^[n]) (a ^ m) = (f^[n]) a ^ m :=
diff --git a/Mathbin/Algebra/Lie/Nilpotent.lean b/Mathbin/Algebra/Lie/Nilpotent.lean
index 413c6f4da4..a9a3061ad8 100644
--- a/Mathbin/Algebra/Lie/Nilpotent.lean
+++ b/Mathbin/Algebra/Lie/Nilpotent.lean
@@ -250,8 +250,8 @@ instance (priority := 100) trivialIsNilpotent [IsTrivial L M] : IsNilpotent R L
 #align lie_module.trivial_is_nilpotent LieModule.trivialIsNilpotent
 -/
 
-#print LieModule.nilpotent_endo_of_nilpotent_module /-
-theorem nilpotent_endo_of_nilpotent_module [hM : IsNilpotent R L M] :
+#print LieModule.exists_forall_pow_toEndomorphism_eq_zero /-
+theorem exists_forall_pow_toEndomorphism_eq_zero [hM : IsNilpotent R L M] :
     ∃ k : ℕ, ∀ x : L, toEndomorphism R L M x ^ k = 0 :=
   by
   obtain ⟨k, hM⟩ := hM
@@ -259,7 +259,7 @@ theorem nilpotent_endo_of_nilpotent_module [hM : IsNilpotent R L M] :
   intro x; ext m
   rw [LinearMap.pow_apply, LinearMap.zero_apply, ← @LieSubmodule.mem_bot R L M, ← hM]
   exact iterate_to_endomorphism_mem_lower_central_series R L M x m k
-#align lie_module.nilpotent_endo_of_nilpotent_module LieModule.nilpotent_endo_of_nilpotent_module
+#align lie_module.nilpotent_endo_of_nilpotent_module LieModule.exists_forall_pow_toEndomorphism_eq_zero
 -/
 
 #print LieModule.iInf_max_gen_zero_eigenspace_eq_top_of_nilpotent /-
@@ -641,7 +641,7 @@ open LieAlgebra
 #print LieAlgebra.nilpotent_ad_of_nilpotent_algebra /-
 theorem LieAlgebra.nilpotent_ad_of_nilpotent_algebra [IsNilpotent R L] :
     ∃ k : ℕ, ∀ x : L, ad R L x ^ k = 0 :=
-  LieModule.nilpotent_endo_of_nilpotent_module R L L
+  LieModule.exists_forall_pow_toEndomorphism_eq_zero R L L
 #align lie_algebra.nilpotent_ad_of_nilpotent_algebra LieAlgebra.nilpotent_ad_of_nilpotent_algebra
 -/
 
diff --git a/Mathbin/Combinatorics/SimpleGraph/Basic.lean b/Mathbin/Combinatorics/SimpleGraph/Basic.lean
index d82fa55cce..413f502311 100644
--- a/Mathbin/Combinatorics/SimpleGraph/Basic.lean
+++ b/Mathbin/Combinatorics/SimpleGraph/Basic.lean
@@ -2262,18 +2262,18 @@ section InduceHom
 variable {G G'} {G'' : SimpleGraph X} {s : Set V} {t : Set W} {r : Set X} (φ : G →g G')
   (φst : Set.MapsTo φ s t) (ψ : G' →g G'') (ψtr : Set.MapsTo ψ t r)
 
-#print SimpleGraph.InduceHom /-
+#print SimpleGraph.induceHom /-
 /-- The restriction of a morphism of graphs to induced subgraphs. -/
-def InduceHom : G.induce s →g G'.induce t
+def induceHom : G.induce s →g G'.induce t
     where
   toFun := Set.MapsTo.restrict φ s t φst
   map_rel' _ _ := φ.map_rel'
-#align simple_graph.induce_hom SimpleGraph.InduceHom
+#align simple_graph.induce_hom SimpleGraph.induceHom
 -/
 
 #print SimpleGraph.coe_induceHom /-
 @[simp, norm_cast]
-theorem coe_induceHom : ⇑(InduceHom φ φst) = Set.MapsTo.restrict φ s t φst :=
+theorem coe_induceHom : ⇑(induceHom φ φst) = Set.MapsTo.restrict φ s t φst :=
   rfl
 #align simple_graph.coe_induce_hom SimpleGraph.coe_induceHom
 -/
@@ -2281,14 +2281,14 @@ theorem coe_induceHom : ⇑(InduceHom φ φst) = Set.MapsTo.restrict φ s t φst
 #print SimpleGraph.induceHom_id /-
 @[simp]
 theorem induceHom_id (G : SimpleGraph V) (s) :
-    InduceHom (Hom.id : G →g G) (Set.mapsTo_id s) = Hom.id := by ext x; rfl
+    induceHom (Hom.id : G →g G) (Set.mapsTo_id s) = Hom.id := by ext x; rfl
 #align simple_graph.induce_hom_id SimpleGraph.induceHom_id
 -/
 
 #print SimpleGraph.induceHom_comp /-
 @[simp]
 theorem induceHom_comp :
-    (InduceHom ψ ψtr).comp (InduceHom φ φst) = InduceHom (ψ.comp φ) (ψtr.comp φst) := by ext x; rfl
+    (induceHom ψ ψtr).comp (induceHom φ φst) = induceHom (ψ.comp φ) (ψtr.comp φst) := by ext x; rfl
 #align simple_graph.induce_hom_comp SimpleGraph.induceHom_comp
 -/
 
diff --git a/Mathbin/Combinatorics/SimpleGraph/Connectivity.lean b/Mathbin/Combinatorics/SimpleGraph/Connectivity.lean
index 38f9c93d42..cbe1a7b89d 100644
--- a/Mathbin/Combinatorics/SimpleGraph/Connectivity.lean
+++ b/Mathbin/Combinatorics/SimpleGraph/Connectivity.lean
@@ -2747,20 +2747,20 @@ abbrev Subgraph.Connected (H : G.Subgraph) : Prop :=
 #align simple_graph.subgraph.connected SimpleGraph.Subgraph.Connected
 -/
 
-#print SimpleGraph.singletonSubgraph_connected /-
-theorem singletonSubgraph_connected {v : V} : (G.singletonSubgraph v).Connected :=
-  by
+#print SimpleGraph.Subgraph.singletonSubgraph_connected /-
+theorem SimpleGraph.Subgraph.singletonSubgraph_connected {v : V} :
+    (G.singletonSubgraph v).Connected := by
   constructor
   rintro ⟨a, ha⟩ ⟨b, hb⟩
   simp only [singleton_subgraph_verts, Set.mem_singleton_iff] at ha hb 
   subst_vars
-#align simple_graph.singleton_subgraph_connected SimpleGraph.singletonSubgraph_connected
+#align simple_graph.singleton_subgraph_connected SimpleGraph.Subgraph.singletonSubgraph_connected
 -/
 
-#print SimpleGraph.subgraphOfAdj_connected /-
+#print SimpleGraph.Subgraph.subgraphOfAdj_connected /-
 @[simp]
-theorem subgraphOfAdj_connected {v w : V} (hvw : G.Adj v w) : (G.subgraphOfAdj hvw).Connected :=
-  by
+theorem SimpleGraph.Subgraph.subgraphOfAdj_connected {v w : V} (hvw : G.Adj v w) :
+    (G.subgraphOfAdj hvw).Connected := by
   constructor
   rintro ⟨a, ha⟩ ⟨b, hb⟩
   simp only [subgraph_of_adj_verts, Set.mem_insert_iff, Set.mem_singleton_iff] at ha hb 
@@ -2768,7 +2768,7 @@ theorem subgraphOfAdj_connected {v w : V} (hvw : G.Adj v w) : (G.subgraphOfAdj h
     first
     | rfl
     | · apply adj.reachable; simp
-#align simple_graph.subgraph_of_adj_connected SimpleGraph.subgraphOfAdj_connected
+#align simple_graph.subgraph_of_adj_connected SimpleGraph.Subgraph.subgraphOfAdj_connected
 -/
 
 #print SimpleGraph.Preconnected.set_univ_walk_nonempty /-
diff --git a/Mathbin/Combinatorics/SimpleGraph/Ends/Defs.lean b/Mathbin/Combinatorics/SimpleGraph/Ends/Defs.lean
index c33b645215..f5a58f2ea9 100644
--- a/Mathbin/Combinatorics/SimpleGraph/Ends/Defs.lean
+++ b/Mathbin/Combinatorics/SimpleGraph/Ends/Defs.lean
@@ -212,7 +212,7 @@ If `K ⊆ L`, the components outside of `L` are all contained in a single compon
 -/
 @[reducible]
 def hom (h : K ⊆ L) (C : G.ComponentCompl L) : G.ComponentCompl K :=
-  C.map <| InduceHom Hom.id <| Set.compl_subset_compl.2 h
+  C.map <| induceHom Hom.id <| Set.compl_subset_compl.2 h
 #align simple_graph.component_compl.hom SimpleGraph.ComponentCompl.hom
 -/
 
diff --git a/Mathbin/Data/Polynomial/Derivative.lean b/Mathbin/Data/Polynomial/Derivative.lean
index 8f5194391f..2e1df6975d 100644
--- a/Mathbin/Data/Polynomial/Derivative.lean
+++ b/Mathbin/Data/Polynomial/Derivative.lean
@@ -187,13 +187,11 @@ theorem derivative_X_add_C (c : R) : (X + C c).derivative = 1 := by
 #align polynomial.derivative_X_add_C Polynomial.derivative_X_add_C
 -/
 
-#print Polynomial.iterate_derivative_add /-
 @[simp]
 theorem iterate_derivative_add {f g : R[X]} {k : ℕ} :
     (derivative^[k]) (f + g) = (derivative^[k]) f + (derivative^[k]) g :=
   derivative.toAddMonoidHom.iterate_map_add _ _ _
 #align polynomial.iterate_derivative_add Polynomial.iterate_derivative_add
--/
 
 #print Polynomial.derivative_sum /-
 @[simp]
diff --git a/Mathbin/FieldTheory/PerfectClosure.lean b/Mathbin/FieldTheory/PerfectClosure.lean
index 58efd631e4..6e238219ce 100644
--- a/Mathbin/FieldTheory/PerfectClosure.lean
+++ b/Mathbin/FieldTheory/PerfectClosure.lean
@@ -44,12 +44,10 @@ def frobeniusEquiv [PerfectRing R p] : R ≃+* R :=
 #align frobenius_equiv frobeniusEquiv
 -/
 
-#print pthRoot /-
 /-- `p`-th root of an element in a `perfect_ring` as a `ring_hom`. -/
 def pthRoot [PerfectRing R p] : R →+* R :=
   (frobeniusEquiv R p).symm
 #align pth_root pthRoot
--/
 
 end Defs
 
@@ -65,96 +63,68 @@ theorem coe_frobeniusEquiv : ⇑(frobeniusEquiv R p) = frobenius R p :=
 #align coe_frobenius_equiv coe_frobeniusEquiv
 -/
 
-#print coe_frobeniusEquiv_symm /-
 @[simp]
 theorem coe_frobeniusEquiv_symm : ⇑(frobeniusEquiv R p).symm = pthRoot R p :=
   rfl
 #align coe_frobenius_equiv_symm coe_frobeniusEquiv_symm
--/
 
-#print frobenius_pthRoot /-
 @[simp]
 theorem frobenius_pthRoot (x : R) : frobenius R p (pthRoot R p x) = x :=
   (frobeniusEquiv R p).apply_symm_apply x
 #align frobenius_pth_root frobenius_pthRoot
--/
 
-#print pthRoot_pow_p /-
 @[simp]
 theorem pthRoot_pow_p (x : R) : pthRoot R p x ^ p = x :=
   frobenius_pthRoot x
 #align pth_root_pow_p pthRoot_pow_p
--/
 
-#print pthRoot_frobenius /-
 @[simp]
 theorem pthRoot_frobenius (x : R) : pthRoot R p (frobenius R p x) = x :=
   (frobeniusEquiv R p).symm_apply_apply x
 #align pth_root_frobenius pthRoot_frobenius
--/
 
-#print pthRoot_pow_p' /-
 @[simp]
 theorem pthRoot_pow_p' (x : R) : pthRoot R p (x ^ p) = x :=
   pthRoot_frobenius x
 #align pth_root_pow_p' pthRoot_pow_p'
--/
 
-#print leftInverse_pthRoot_frobenius /-
 theorem leftInverse_pthRoot_frobenius : LeftInverse (pthRoot R p) (frobenius R p) :=
   pthRoot_frobenius
 #align left_inverse_pth_root_frobenius leftInverse_pthRoot_frobenius
--/
 
-#print rightInverse_pthRoot_frobenius /-
 theorem rightInverse_pthRoot_frobenius : Function.RightInverse (pthRoot R p) (frobenius R p) :=
   frobenius_pthRoot
 #align right_inverse_pth_root_frobenius rightInverse_pthRoot_frobenius
--/
 
-#print commute_frobenius_pthRoot /-
 theorem commute_frobenius_pthRoot : Function.Commute (frobenius R p) (pthRoot R p) := fun x =>
   (frobenius_pthRoot x).trans (pthRoot_frobenius x).symm
 #align commute_frobenius_pth_root commute_frobenius_pthRoot
--/
 
-#print eq_pthRoot_iff /-
 theorem eq_pthRoot_iff {x y : R} : x = pthRoot R p y ↔ frobenius R p x = y :=
   (frobeniusEquiv R p).toEquiv.eq_symm_apply
 #align eq_pth_root_iff eq_pthRoot_iff
--/
 
-#print pthRoot_eq_iff /-
 theorem pthRoot_eq_iff {x y : R} : pthRoot R p x = y ↔ x = frobenius R p y :=
   (frobeniusEquiv R p).toEquiv.symm_apply_eq
 #align pth_root_eq_iff pthRoot_eq_iff
--/
 
-#print MonoidHom.map_pthRoot /-
 theorem MonoidHom.map_pthRoot (x : R) : f (pthRoot R p x) = pthRoot S p (f x) :=
   eq_pthRoot_iff.2 <| by rw [← f.map_frobenius, frobenius_pthRoot]
 #align monoid_hom.map_pth_root MonoidHom.map_pthRoot
--/
 
-#print MonoidHom.map_iterate_pthRoot /-
 theorem MonoidHom.map_iterate_pthRoot (x : R) (n : ℕ) :
     f ((pthRoot R p^[n]) x) = (pthRoot S p^[n]) (f x) :=
   Semiconj.iterate_right f.map_pthRoot n x
 #align monoid_hom.map_iterate_pth_root MonoidHom.map_iterate_pthRoot
--/
 
-#print RingHom.map_pthRoot /-
 theorem RingHom.map_pthRoot (x : R) : g (pthRoot R p x) = pthRoot S p (g x) :=
   g.toMonoidHom.map_pthRoot x
 #align ring_hom.map_pth_root RingHom.map_pthRoot
--/
 
-#print RingHom.map_iterate_pthRoot /-
 theorem RingHom.map_iterate_pthRoot (x : R) (n : ℕ) :
     g ((pthRoot R p^[n]) x) = (pthRoot S p^[n]) (g x) :=
   g.toMonoidHom.map_iterate_pthRoot x n
 #align ring_hom.map_iterate_pth_root RingHom.map_iterate_pthRoot
--/
 
 variable (p)
 
@@ -594,14 +564,12 @@ instance : PerfectRing (PerfectClosure K p) p
     induction_on e fun ⟨n, x⟩ => by simp only [lift_on_mk, frobenius_mk];
       exact (Quot.sound <| r.intro _ _).symm
 
-#print PerfectClosure.eq_pthRoot /-
 theorem eq_pthRoot (x : ℕ × K) : mk K p x = (pthRoot (PerfectClosure K p) p^[x.1]) (of K p x.2) :=
   by
   rcases x with ⟨m, x⟩
   induction' m with m ih; · rfl
   rw [iterate_succ_apply', ← ih] <;> rfl
 #align perfect_closure.eq_pth_root PerfectClosure.eq_pthRoot
--/
 
 #print PerfectClosure.lift /-
 /-- Given a field `K` of characteristic `p` and a perfect ring `L` of the same characteristic,
diff --git a/Mathbin/LinearAlgebra/BilinearForm.lean b/Mathbin/LinearAlgebra/BilinearForm.lean
index 2f7aa557a6..116fb1a9ea 100644
--- a/Mathbin/LinearAlgebra/BilinearForm.lean
+++ b/Mathbin/LinearAlgebra/BilinearForm.lean
@@ -1144,8 +1144,8 @@ theorem isSymm_neg {B : BilinForm R₁ M₁} : (-B).IsSymm ↔ B.IsSymm :=
 #align bilin_form.is_symm_neg BilinForm.isSymm_neg
 -/
 
-#print BilinForm.isSymm_iff_flip' /-
-theorem isSymm_iff_flip' [Algebra R₂ R] : B.IsSymm ↔ flipHom R₂ B = B :=
+#print BilinForm.isSymm_iff_flip /-
+theorem isSymm_iff_flip [Algebra R₂ R] : B.IsSymm ↔ flipHom R₂ B = B :=
   by
   constructor
   · intro h
@@ -1154,7 +1154,7 @@ theorem isSymm_iff_flip' [Algebra R₂ R] : B.IsSymm ↔ flipHom R₂ B = B :=
   · intro h x y
     conv_lhs => rw [← h]
     simp
-#align bilin_form.is_symm_iff_flip' BilinForm.isSymm_iff_flip'
+#align bilin_form.is_symm_iff_flip' BilinForm.isSymm_iff_flip
 -/
 
 #print BilinForm.IsAlt /-
diff --git a/Mathbin/MeasureTheory/Measure/Stieltjes.lean b/Mathbin/MeasureTheory/Measure/Stieltjes.lean
index 292ffddf0b..501e4d9d6e 100644
--- a/Mathbin/MeasureTheory/Measure/Stieltjes.lean
+++ b/Mathbin/MeasureTheory/Measure/Stieltjes.lean
@@ -35,8 +35,8 @@ open Filter Set
 
 open scoped Topology
 
-#print iInf_Ioi_eq_iInf_rat_gt /-
-theorem iInf_Ioi_eq_iInf_rat_gt {f : ℝ → ℝ} (x : ℝ) (hf : BddBelow (f '' Ioi x))
+#print Real.iInf_Ioi_eq_iInf_rat_gt /-
+theorem Real.iInf_Ioi_eq_iInf_rat_gt {f : ℝ → ℝ} (x : ℝ) (hf : BddBelow (f '' Ioi x))
     (hf_mono : Monotone f) : (⨅ r : Ioi x, f r) = ⨅ q : { q' : ℚ // x < q' }, f q :=
   by
   refine' le_antisymm _ _
@@ -60,7 +60,7 @@ theorem iInf_Ioi_eq_iInf_rat_gt {f : ℝ → ℝ} (x : ℝ) (hf : BddBelow (f ''
       exact ⟨u, u.prop, rfl⟩
     · refine' hf_mono (le_trans _ hyq.le)
       norm_cast
-#align infi_Ioi_eq_infi_rat_gt iInf_Ioi_eq_iInf_rat_gt
+#align infi_Ioi_eq_infi_rat_gt Real.iInf_Ioi_eq_iInf_rat_gt
 -/
 
 #print rightLim_eq_of_tendsto /-
@@ -72,19 +72,19 @@ theorem rightLim_eq_of_tendsto {α β : Type _} [LinearOrder α] [TopologicalSpa
 #align right_lim_eq_of_tendsto rightLim_eq_of_tendsto
 -/
 
-#print rightLim_eq_sInf /-
+#print Monotone.rightLim_eq_sInf /-
 -- todo after the port: move to topology/algebra/order/left_right_lim
-theorem rightLim_eq_sInf {α β : Type _} [LinearOrder α] [TopologicalSpace β]
+theorem Monotone.rightLim_eq_sInf {α β : Type _} [LinearOrder α] [TopologicalSpace β]
     [ConditionallyCompleteLinearOrder β] [OrderTopology β] {f : α → β} (hf : Monotone f) {x : α}
     [TopologicalSpace α] [OrderTopology α] (h : 𝓝[>] x ≠ ⊥) :
     Function.rightLim f x = sInf (f '' Ioi x) :=
   rightLim_eq_of_tendsto h (hf.tendsto_nhdsWithin_Ioi x)
-#align right_lim_eq_Inf rightLim_eq_sInf
+#align right_lim_eq_Inf Monotone.rightLim_eq_sInf
 -/
 
-#print exists_seq_monotone_tendsto_atTop_atTop /-
+#print Filter.exists_seq_monotone_tendsto_atTop_atTop /-
 -- todo after the port: move to order/filter/at_top_bot
-theorem exists_seq_monotone_tendsto_atTop_atTop (α : Type _) [SemilatticeSup α] [Nonempty α]
+theorem Filter.exists_seq_monotone_tendsto_atTop_atTop (α : Type _) [SemilatticeSup α] [Nonempty α]
     [(atTop : Filter α).IsCountablyGenerated] :
     ∃ xs : ℕ → α, Monotone xs ∧ Tendsto xs atTop atTop :=
   by
@@ -111,15 +111,15 @@ theorem exists_seq_monotone_tendsto_atTop_atTop (α : Type _) [SemilatticeSup α
     refine' ⟨i, hi.trans _⟩
     refine' Finset.le_sup'_of_le _ _ le_rfl
     rw [Finset.mem_range_succ_iff]
-#align exists_seq_monotone_tendsto_at_top_at_top exists_seq_monotone_tendsto_atTop_atTop
+#align exists_seq_monotone_tendsto_at_top_at_top Filter.exists_seq_monotone_tendsto_atTop_atTop
 -/
 
-#print exists_seq_antitone_tendsto_atTop_atBot /-
-theorem exists_seq_antitone_tendsto_atTop_atBot (α : Type _) [SemilatticeInf α] [Nonempty α]
+#print Filter.exists_seq_antitone_tendsto_atTop_atBot /-
+theorem Filter.exists_seq_antitone_tendsto_atTop_atBot (α : Type _) [SemilatticeInf α] [Nonempty α]
     [h2 : (atBot : Filter α).IsCountablyGenerated] :
     ∃ xs : ℕ → α, Antitone xs ∧ Tendsto xs atTop atBot :=
-  @exists_seq_monotone_tendsto_atTop_atTop αᵒᵈ _ _ h2
-#align exists_seq_antitone_tendsto_at_top_at_bot exists_seq_antitone_tendsto_atTop_atBot
+  @Filter.exists_seq_monotone_tendsto_atTop_atTop αᵒᵈ _ _ h2
+#align exists_seq_antitone_tendsto_at_top_at_bot Filter.exists_seq_antitone_tendsto_atTop_atBot
 -/
 
 #print iSup_eq_iSup_subseq_of_antitone /-
@@ -148,7 +148,7 @@ theorem tendsto_measure_Ico_atTop [SemilatticeSup α] [NoMaxOrder α]
   have h_mono : Monotone fun x => μ (Ico a x) := fun i j hij =>
     measure_mono (Ico_subset_Ico_right hij)
   convert tendsto_atTop_iSup h_mono
-  obtain ⟨xs, hxs_mono, hxs_tendsto⟩ := exists_seq_monotone_tendsto_atTop_atTop α
+  obtain ⟨xs, hxs_mono, hxs_tendsto⟩ := Filter.exists_seq_monotone_tendsto_atTop_atTop α
   have h_Ici : Ici a = ⋃ n, Ico a (xs n) := by
     ext1 x
     simp only [mem_Ici, mem_Union, mem_Ico, exists_and_left, iff_self_and]
@@ -170,7 +170,7 @@ theorem tendsto_measure_Ioc_atBot [SemilatticeInf α] [NoMinOrder α]
   have h_mono : Antitone fun x => μ (Ioc x a) := fun i j hij =>
     measure_mono (Ioc_subset_Ioc_left hij)
   convert tendsto_atBot_iSup h_mono
-  obtain ⟨xs, hxs_mono, hxs_tendsto⟩ := exists_seq_antitone_tendsto_atTop_atBot α
+  obtain ⟨xs, hxs_mono, hxs_tendsto⟩ := Filter.exists_seq_antitone_tendsto_atTop_atBot α
   have h_Iic : Iic a = ⋃ n, Ioc (xs n) a := by
     ext1 x
     simp only [mem_Iic, mem_Union, mem_Ioc, exists_and_right, iff_and_self]
@@ -194,7 +194,7 @@ theorem tendsto_measure_Iic_atTop [SemilatticeSup α] [(atTop : Filter α).IsCou
     exact tendsto_const_nhds
   have h_mono : Monotone fun x => μ (Iic x) := fun i j hij => measure_mono (Iic_subset_Iic.mpr hij)
   convert tendsto_atTop_iSup h_mono
-  obtain ⟨xs, hxs_mono, hxs_tendsto⟩ := exists_seq_monotone_tendsto_atTop_atTop α
+  obtain ⟨xs, hxs_mono, hxs_tendsto⟩ := Filter.exists_seq_monotone_tendsto_atTop_atTop α
   have h_univ : (univ : Set α) = ⋃ n, Iic (xs n) :=
     by
     ext1 x
@@ -270,7 +270,7 @@ theorem rightLim_eq (f : StieltjesFunction) (x : ℝ) : Function.rightLim f x =
 theorem iInf_Ioi_eq (f : StieltjesFunction) (x : ℝ) : (⨅ r : Ioi x, f r) = f x :=
   by
   suffices Function.rightLim f x = ⨅ r : Ioi x, f r by rw [← this, f.right_lim_eq]
-  rw [rightLim_eq_sInf f.mono, sInf_image']
+  rw [Monotone.rightLim_eq_sInf f.mono, sInf_image']
   rw [← ne_bot_iff]
   infer_instance
 #align stieltjes_function.infi_Ioi_eq StieltjesFunction.iInf_Ioi_eq
@@ -280,7 +280,7 @@ theorem iInf_Ioi_eq (f : StieltjesFunction) (x : ℝ) : (⨅ r : Ioi x, f r) = f
 theorem iInf_rat_gt_eq (f : StieltjesFunction) (x : ℝ) : (⨅ r : { r' : ℚ // x < r' }, f r) = f x :=
   by
   rw [← infi_Ioi_eq f x]
-  refine' (iInf_Ioi_eq_iInf_rat_gt _ _ f.mono).symm
+  refine' (Real.iInf_Ioi_eq_iInf_rat_gt _ _ f.mono).symm
   refine' ⟨f x, fun y => _⟩
   rintro ⟨y, hy_mem, rfl⟩
   exact f.mono (le_of_lt hy_mem)
diff --git a/Mathbin/Probability/Kernel/CondCdf.lean b/Mathbin/Probability/Kernel/CondCdf.lean
index 5745ae18b1..fcb8bc9a75 100644
--- a/Mathbin/Probability/Kernel/CondCdf.lean
+++ b/Mathbin/Probability/Kernel/CondCdf.lean
@@ -946,7 +946,7 @@ theorem continuousWithinAt_condCdf'_Ici (ρ : Measure (α × ℝ)) (a : α) (x :
   rw [sInf_image']
   have h' : (⨅ r : Ioi x, cond_cdf' ρ a r) = ⨅ r : { r' : ℚ // x < r' }, cond_cdf' ρ a r :=
     by
-    refine' iInf_Ioi_eq_iInf_rat_gt x _ (monotone_cond_cdf' ρ a)
+    refine' Real.iInf_Ioi_eq_iInf_rat_gt x _ (monotone_cond_cdf' ρ a)
     refine' ⟨0, fun z => _⟩
     rintro ⟨u, hux, rfl⟩
     exact cond_cdf'_nonneg ρ a u
diff --git a/Mathbin/Probability/Kernel/Condexp.lean b/Mathbin/Probability/Kernel/Condexp.lean
index 1d1650d7cb..ba0dc853f4 100644
--- a/Mathbin/Probability/Kernel/Condexp.lean
+++ b/Mathbin/Probability/Kernel/Condexp.lean
@@ -44,18 +44,18 @@ section AuxLemmas
 
 variable {Ω F : Type _} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {f : Ω → F}
 
-#print ProbabilityTheory.measurable_id'' /-
+#print measurable_id'' /-
 -- todo after the port: move to measure_theory/measurable_space, after measurable.mono
 theorem measurable_id'' (hm : m ≤ mΩ) : @Measurable Ω Ω mΩ m id :=
   measurable_id.mono le_rfl hm
-#align probability_theory.measurable_id'' ProbabilityTheory.measurable_id''
+#align probability_theory.measurable_id'' measurable_id''
 -/
 
-#print ProbabilityTheory.aemeasurable_id'' /-
+#print aemeasurable_id'' /-
 -- todo after the port: move to measure_theory/measurable_space, after measurable.mono
 theorem aemeasurable_id'' (μ : Measure Ω) (hm : m ≤ mΩ) : @AEMeasurable Ω Ω m mΩ id μ :=
   @Measurable.aemeasurable Ω Ω mΩ m id μ (measurable_id'' hm)
-#align probability_theory.ae_measurable_id'' ProbabilityTheory.aemeasurable_id''
+#align probability_theory.ae_measurable_id'' aemeasurable_id''
 -/
 
 #print MeasureTheory.AEStronglyMeasurable.comp_snd_map_prod_id /-
diff --git a/lake-manifest.json b/lake-manifest.json
index fc01c33eeb..bd502cde78 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": "a4b60b2f7cb286d3b1e39234cb680f3a29641ea9",
+    "rev": "99405f14f97b1679342be1ead510d56ae98bae30",
     "name": "lean3port",
-    "inputRev?": "a4b60b2f7cb286d3b1e39234cb680f3a29641ea9"}},
+    "inputRev?": "99405f14f97b1679342be1ead510d56ae98bae30"}},
   {"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": "c769b9d88f251ff1f0c92001fd4ef480d6ea0537",
+    "rev": "72b6e767aa1c478f6b5d9c51912b0e8a4f415b2e",
     "name": "mathlib",
-    "inputRev?": "c769b9d88f251ff1f0c92001fd4ef480d6ea0537"}},
+    "inputRev?": "72b6e767aa1c478f6b5d9c51912b0e8a4f415b2e"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
diff --git a/lakefile.lean b/lakefile.lean
index 1d062960bf..1b78514dc7 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-15-07"
+def tag : String := "nightly-2023-08-15-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"@"a4b60b2f7cb286d3b1e39234cb680f3a29641ea9"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"99405f14f97b1679342be1ead510d56ae98bae30"
 
 @[default_target]
 lean_lib Mathbin where