diff --git a/Mathbin/Algebra/Category/Mon/Colimits.lean b/Mathbin/Algebra/Category/Mon/Colimits.lean
index c45fe57153..c715794be2 100644
--- a/Mathbin/Algebra/Category/Mon/Colimits.lean
+++ b/Mathbin/Algebra/Category/Mon/Colimits.lean
@@ -52,6 +52,7 @@ and the identifications given by the morphisms in the diagram.
 
 variable {J : Type v} [SmallCategory J] (F : J ⥤ MonCat.{v})
 
+#print MonCat.Colimits.Prequotient /-
 /-- An inductive type representing all monoid expressions (without relations)
 on a collection of types indexed by the objects of `J`.
 -/
@@ -62,12 +63,14 @@ inductive Prequotient-- There's always `of`
   | one : prequotient
   | mul : prequotient → prequotient → prequotient
 #align Mon.colimits.prequotient MonCat.Colimits.Prequotient
+-/
 
 instance : Inhabited (Prequotient F) :=
   ⟨Prequotient.one⟩
 
 open Prequotient
 
+#print MonCat.Colimits.Relation /-
 /-- The relation on `prequotient` saying when two expressions are equal
 because of the monoid laws, or
 because one element is mapped to another by a morphism in the diagram.
@@ -97,7 +100,9 @@ inductive Relation : Prequotient F → Prequotient F → Prop-- Make it an equiv
   | one_mul : ∀ x, relation (mul one x) x
   | mul_one : ∀ x, relation (mul x one) x
 #align Mon.colimits.relation MonCat.Colimits.Relation
+-/
 
+#print MonCat.Colimits.colimitSetoid /-
 /-- The setoid corresponding to monoid expressions modulo monoid relations and identifications.
 -/
 def colimitSetoid : Setoid (Prequotient F)
@@ -105,16 +110,20 @@ def colimitSetoid : Setoid (Prequotient F)
   R := Relation F
   iseqv := ⟨Relation.refl, Relation.symm, Relation.trans⟩
 #align Mon.colimits.colimit_setoid MonCat.Colimits.colimitSetoid
+-/
 
 attribute [instance] colimit_setoid
 
+#print MonCat.Colimits.ColimitType /-
 /-- The underlying type of the colimit of a diagram in `Mon`.
 -/
 def ColimitType : Type v :=
   Quotient (colimitSetoid F)
 deriving Inhabited
 #align Mon.colimits.colimit_type MonCat.Colimits.ColimitType
+-/
 
+#print MonCat.Colimits.monoidColimitType /-
 instance monoidColimitType : Monoid (ColimitType F)
     where
   mul := by
@@ -157,28 +166,38 @@ instance monoidColimitType : Monoid (ColimitType F)
     apply relation.mul_one
     rfl
 #align Mon.colimits.monoid_colimit_type MonCat.Colimits.monoidColimitType
+-/
 
+#print MonCat.Colimits.quot_one /-
 @[simp]
 theorem quot_one : Quot.mk Setoid.r one = (1 : ColimitType F) :=
   rfl
 #align Mon.colimits.quot_one MonCat.Colimits.quot_one
+-/
 
+#print MonCat.Colimits.quot_mul /-
 @[simp]
 theorem quot_mul (x y) :
     Quot.mk Setoid.r (mul x y) = (Quot.mk Setoid.r x * Quot.mk Setoid.r y : ColimitType F) :=
   rfl
 #align Mon.colimits.quot_mul MonCat.Colimits.quot_mul
+-/
 
+#print MonCat.Colimits.colimit /-
 /-- The bundled monoid giving the colimit of a diagram. -/
 def colimit : MonCat :=
   ⟨ColimitType F, by infer_instance⟩
 #align Mon.colimits.colimit MonCat.Colimits.colimit
+-/
 
+#print MonCat.Colimits.coconeFun /-
 /-- The function from a given monoid in the diagram to the colimit monoid. -/
 def coconeFun (j : J) (x : F.obj j) : ColimitType F :=
   Quot.mk _ (of j x)
 #align Mon.colimits.cocone_fun MonCat.Colimits.coconeFun
+-/
 
+#print MonCat.Colimits.coconeMorphism /-
 /-- The monoid homomorphism from a given monoid in the diagram to the colimit monoid. -/
 def coconeMorphism (j : J) : F.obj j ⟶ colimit F
     where
@@ -186,7 +205,9 @@ def coconeMorphism (j : J) : F.obj j ⟶ colimit F
   map_one' := Quot.sound (Relation.one _)
   map_mul' x y := Quot.sound (Relation.mul _ _ _)
 #align Mon.colimits.cocone_morphism MonCat.Colimits.coconeMorphism
+-/
 
+#print MonCat.Colimits.cocone_naturality /-
 @[simp]
 theorem cocone_naturality {j j' : J} (f : j ⟶ j') :
     F.map f ≫ coconeMorphism F j' = coconeMorphism F j :=
@@ -195,19 +216,25 @@ theorem cocone_naturality {j j' : J} (f : j ⟶ j') :
   apply Quot.sound
   apply Relation.Map
 #align Mon.colimits.cocone_naturality MonCat.Colimits.cocone_naturality
+-/
 
+#print MonCat.Colimits.cocone_naturality_components /-
 @[simp]
 theorem cocone_naturality_components (j j' : J) (f : j ⟶ j') (x : F.obj j) :
     (coconeMorphism F j') (F.map f x) = (coconeMorphism F j) x := by rw [← cocone_naturality F f];
   rfl
 #align Mon.colimits.cocone_naturality_components MonCat.Colimits.cocone_naturality_components
+-/
 
+#print MonCat.Colimits.colimitCocone /-
 /-- The cocone over the proposed colimit monoid. -/
 def colimitCocone : Cocone F where
   pt := colimit F
   ι := { app := coconeMorphism F }
 #align Mon.colimits.colimit_cocone MonCat.Colimits.colimitCocone
+-/
 
+#print MonCat.Colimits.descFunLift /-
 /-- The function from the free monoid on the diagram to the cone point of any other cocone. -/
 @[simp]
 def descFunLift (s : Cocone F) : Prequotient F → s.pt
@@ -215,7 +242,9 @@ def descFunLift (s : Cocone F) : Prequotient F → s.pt
   | one => 1
   | mul x y => desc_fun_lift x * desc_fun_lift y
 #align Mon.colimits.desc_fun_lift MonCat.Colimits.descFunLift
+-/
 
+#print MonCat.Colimits.descFun /-
 /-- The function from the colimit monoid to the cone point of any other cocone. -/
 def descFun (s : Cocone F) : ColimitType F → s.pt :=
   by
@@ -246,7 +275,9 @@ def descFun (s : Cocone F) : ColimitType F → s.pt :=
     -- mul_one
     · rw [mul_one]
 #align Mon.colimits.desc_fun MonCat.Colimits.descFun
+-/
 
+#print MonCat.Colimits.descMorphism /-
 /-- The monoid homomorphism from the colimit monoid to the cone point of any other cocone. -/
 def descMorphism (s : Cocone F) : colimit F ⟶ s.pt
     where
@@ -254,7 +285,9 @@ def descMorphism (s : Cocone F) : colimit F ⟶ s.pt
   map_one' := rfl
   map_mul' x y := by induction x <;> induction y <;> rfl
 #align Mon.colimits.desc_morphism MonCat.Colimits.descMorphism
+-/
 
+#print MonCat.Colimits.colimitIsColimit /-
 /-- Evidence that the proposed colimit is the colimit. -/
 def colimitIsColimit : IsColimit (colimitCocone F)
     where
@@ -271,7 +304,9 @@ def colimitIsColimit : IsColimit (colimitCocone F)
     · simp [*]
     rfl
 #align Mon.colimits.colimit_is_colimit MonCat.Colimits.colimitIsColimit
+-/
 
+#print MonCat.Colimits.hasColimits_monCat /-
 instance hasColimits_monCat : HasColimits MonCat
     where HasColimitsOfShape J 𝒥 :=
     {
@@ -280,6 +315,7 @@ instance hasColimits_monCat : HasColimits MonCat
           { Cocone := colimit_cocone F
             IsColimit := colimit_is_colimit F } }
 #align Mon.colimits.has_colimits_Mon MonCat.Colimits.hasColimits_monCat
+-/
 
 end MonCat.Colimits
 
diff --git a/Mathbin/Algebra/Homology/LocalCohomology.lean b/Mathbin/Algebra/Homology/LocalCohomology.lean
index b004d74863..147002d746 100644
--- a/Mathbin/Algebra/Homology/LocalCohomology.lean
+++ b/Mathbin/Algebra/Homology/LocalCohomology.lean
@@ -79,11 +79,11 @@ def ringModIdeals (I : D ⥤ Ideal R) : D ⥤ ModuleCat.{u} R
 #align local_cohomology.ring_mod_ideals localCohomology.ringModIdeals
 -/
 
-#print localCohomology.moduleCat_enough_projectives' /-
+#print localCohomology.moduleCat_enoughProjectives' /-
 -- TODO:  Once this file is ported, move this file to the right location.
-instance moduleCat_enough_projectives' : EnoughProjectives (ModuleCat.{u} R) :=
+instance moduleCat_enoughProjectives' : EnoughProjectives (ModuleCat.{u} R) :=
   ModuleCat.moduleCat_enoughProjectives.{u}
-#align local_cohomology.Module_enough_projectives' localCohomology.moduleCat_enough_projectives'
+#align local_cohomology.Module_enough_projectives' localCohomology.moduleCat_enoughProjectives'
 -/
 
 #print localCohomology.diagram /-
@@ -153,26 +153,26 @@ def idealPowersDiagram (J : Ideal R) : ℕᵒᵖ ⥤ Ideal R
 #align local_cohomology.ideal_powers_diagram localCohomology.idealPowersDiagram
 -/
 
-#print localCohomology.SelfLeRadical /-
+#print localCohomology.SelfLERadical /-
 /-- The full subcategory of all ideals with radical containing `J` -/
-def SelfLeRadical (J : Ideal R) : Type u :=
+def SelfLERadical (J : Ideal R) : Type u :=
   FullSubcategory fun J' : Ideal R => J ≤ J'.radical
 deriving Category
-#align local_cohomology.self_le_radical localCohomology.SelfLeRadical
+#align local_cohomology.self_le_radical localCohomology.SelfLERadical
 -/
 
-#print localCohomology.SelfLeRadical.inhabited /-
-instance SelfLeRadical.inhabited (J : Ideal R) : Inhabited (SelfLeRadical J)
+#print localCohomology.SelfLERadical.inhabited /-
+instance SelfLERadical.inhabited (J : Ideal R) : Inhabited (SelfLERadical J)
     where default := ⟨J, Ideal.le_radical⟩
-#align local_cohomology.self_le_radical.inhabited localCohomology.SelfLeRadical.inhabited
+#align local_cohomology.self_le_radical.inhabited localCohomology.SelfLERadical.inhabited
 -/
 
-#print localCohomology.selfLeRadicalDiagram /-
+#print localCohomology.selfLERadicalDiagram /-
 /-- The diagram of all ideals with radical containing `J`, represented as a functor.
 This is the "largest" diagram that computes local cohomology with support in `J`. -/
-def selfLeRadicalDiagram (J : Ideal R) : SelfLeRadical J ⥤ Ideal R :=
+def selfLERadicalDiagram (J : Ideal R) : SelfLERadical J ⥤ Ideal R :=
   fullSubcategoryInclusion _
-#align local_cohomology.self_le_radical_diagram localCohomology.selfLeRadicalDiagram
+#align local_cohomology.self_le_radical_diagram localCohomology.selfLERadicalDiagram
 -/
 
 end Diagrams
@@ -199,12 +199,12 @@ def localCohomology (J : Ideal R) (i : ℕ) : ModuleCat.{u} R ⥤ ModuleCat.{u}
 #align local_cohomology localCohomology
 -/
 
-#print localCohomology.ofSelfLeRadical /-
+#print localCohomology.ofSelfLERadical /-
 /-- Local cohomology as the direct limit of `Ext^i(R/J', M)` over *all* ideals `J'` with radical
 containing `J`. -/
-def localCohomology.ofSelfLeRadical (J : Ideal R) (i : ℕ) : ModuleCat.{u} R ⥤ ModuleCat.{u} R :=
-  ofDiagram.{u} (selfLeRadicalDiagram.{u} J) i
-#align local_cohomology.of_self_le_radical localCohomology.ofSelfLeRadical
+def localCohomology.ofSelfLERadical (J : Ideal R) (i : ℕ) : ModuleCat.{u} R ⥤ ModuleCat.{u} R :=
+  ofDiagram.{u} (selfLERadicalDiagram.{u} J) i
+#align local_cohomology.of_self_le_radical localCohomology.ofSelfLERadical
 -/
 
 end ModelsForLocalCohomology
@@ -224,17 +224,17 @@ section LocalCohomologyEquiv
 
 variable {R : Type u} [CommRing R]
 
-#print localCohomology.idealPowersToSelfLeRadical /-
+#print localCohomology.idealPowersToSelfLERadical /-
 /-- Lifting `ideal_powers_diagram J` from a diagram valued in `ideals R` to a diagram
 valued in `self_le_radical J`. -/
-def idealPowersToSelfLeRadical (J : Ideal R) : ℕᵒᵖ ⥤ SelfLeRadical J :=
+def idealPowersToSelfLERadical (J : Ideal R) : ℕᵒᵖ ⥤ SelfLERadical J :=
   FullSubcategory.lift _ (idealPowersDiagram J) fun k =>
     by
     change _ ≤ (J ^ unop k).radical
     cases unop k
     · simp only [Ideal.radical_top, pow_zero, Ideal.one_eq_top, le_top]
     · simp only [J.radical_pow _ n.succ_pos, Ideal.le_radical]
-#align local_cohomology.ideal_powers_to_self_le_radical localCohomology.idealPowersToSelfLeRadical
+#align local_cohomology.ideal_powers_to_self_le_radical localCohomology.idealPowersToSelfLERadical
 -/
 
 variable {I J K : Ideal R}
@@ -255,7 +255,7 @@ theorem Ideal.exists_pow_le_of_le_radical_of_fG (hIJ : I ≤ J.radical) (hJ : J.
 /-- The diagram of powers of `J` is initial in the diagram of all ideals with
 radical containing `J`. This uses noetherianness. -/
 instance ideal_powers_initial [hR : IsNoetherian R R] :
-    Functor.Initial (idealPowersToSelfLeRadical J)
+    Functor.Initial (idealPowersToSelfLERadical J)
     where out J' := by
     apply @zigzag_is_connected _ _ _
     · intro j1 j2
@@ -265,48 +265,48 @@ instance ideal_powers_initial [hR : IsNoetherian R R] :
       cases' le_total (unop j1.left) (unop j2.left) with h
       right; exact ⟨costructured_arrow.hom_mk (hom_of_le h).op (AsTrue.get trivial)⟩
       left; exact ⟨costructured_arrow.hom_mk (hom_of_le h).op (AsTrue.get trivial)⟩
-    · obtain ⟨k, hk⟩ := Ideal.exists_pow_le_of_le_radical_of_fG J'.2 (is_noetherian_def.mp hR _)
+    · obtain ⟨k, hk⟩ := Ideal.exists_pow_le_of_le_radical_of_fg J'.2 (is_noetherian_def.mp hR _)
       exact ⟨costructured_arrow.mk (⟨⟨hk⟩⟩ : (ideal_powers_to_self_le_radical J).obj (op k) ⟶ J')⟩
 #align local_cohomology.ideal_powers_initial localCohomology.ideal_powers_initial
 
 /-- Local cohomology (defined in terms of powers of `J`) agrees with local
 cohomology computed over all ideals with radical containing `J`. -/
 def isoSelfLeRadical (J : Ideal R) [IsNoetherian R R] (i : ℕ) :
-    localCohomology.ofSelfLeRadical J i ≅ localCohomology J i :=
-  (localCohomology.isoOfFinal.{u, u, 0} (idealPowersToSelfLeRadical J) (selfLeRadicalDiagram J)
+    localCohomology.ofSelfLERadical J i ≅ localCohomology J i :=
+  (localCohomology.isoOfFinal.{u, u, 0} (idealPowersToSelfLERadical J) (selfLERadicalDiagram J)
         i).symm ≪≫
     HasColimit.isoOfNatIso (Iso.refl _)
 #align local_cohomology.iso_self_le_radical localCohomology.isoSelfLeRadical
 
 /-- Casting from the full subcategory of ideals with radical containing `J` to the full
 subcategory of ideals with radical containing `K`. -/
-def SelfLeRadical.cast (hJK : J.radical = K.radical) : SelfLeRadical J ⥤ SelfLeRadical K :=
+def SelfLERadical.cast (hJK : J.radical = K.radical) : SelfLERadical J ⥤ SelfLERadical K :=
   FullSubcategory.map fun L hL =>
     by
     rw [← Ideal.radical_le_radical_iff] at hL ⊢
     exact hJK.symm.trans_le hL
-#align local_cohomology.self_le_radical.cast localCohomology.SelfLeRadical.cast
+#align local_cohomology.self_le_radical.cast localCohomology.SelfLERadical.cast
 
 -- TODO generalize this to the equivalence of full categories for any `iff`.
-instance SelfLeRadical.castIsEquivalence (hJK : J.radical = K.radical) :
-    IsEquivalence (SelfLeRadical.cast hJK)
+instance SelfLERadical.castIsEquivalence (hJK : J.radical = K.radical) :
+    IsEquivalence (SelfLERadical.cast hJK)
     where
-  inverse := SelfLeRadical.cast hJK.symm
+  inverse := SelfLERadical.cast hJK.symm
   unitIso := by tidy
   counitIso := by tidy
-#align local_cohomology.self_le_radical.cast_is_equivalence localCohomology.SelfLeRadical.castIsEquivalence
+#align local_cohomology.self_le_radical.cast_is_equivalence localCohomology.SelfLERadical.castIsEquivalence
 
 /-- The natural isomorphism between local cohomology defined using the `of_self_le_radical`
 diagram, assuming `J.radical = K.radical`. -/
-def SelfLeRadical.isoOfSameRadical (hJK : J.radical = K.radical) (i : ℕ) :
-    ofSelfLeRadical J i ≅ ofSelfLeRadical K i :=
-  (isoOfFinal.{u, u, u} (SelfLeRadical.cast hJK.symm) _ _).symm
-#align local_cohomology.self_le_radical.iso_of_same_radical localCohomology.SelfLeRadical.isoOfSameRadical
+def SelfLERadical.isoOfSameRadical (hJK : J.radical = K.radical) (i : ℕ) :
+    ofSelfLERadical J i ≅ ofSelfLERadical K i :=
+  (isoOfFinal.{u, u, u} (SelfLERadical.cast hJK.symm) _ _).symm
+#align local_cohomology.self_le_radical.iso_of_same_radical localCohomology.SelfLERadical.isoOfSameRadical
 
 /-- Local cohomology agrees on ideals with the same radical. -/
 def isoOfSameRadical [IsNoetherian R R] (hJK : J.radical = K.radical) (i : ℕ) :
     localCohomology J i ≅ localCohomology K i :=
-  (isoSelfLeRadical J i).symm ≪≫ SelfLeRadical.isoOfSameRadical hJK i ≪≫ isoSelfLeRadical K i
+  (isoSelfLeRadical J i).symm ≪≫ SelfLERadical.isoOfSameRadical hJK i ≪≫ isoSelfLeRadical K i
 #align local_cohomology.iso_of_same_radical localCohomology.isoOfSameRadical
 
 end LocalCohomologyEquiv
diff --git a/Mathbin/Data/Set/Ncard.lean b/Mathbin/Data/Set/Ncard.lean
index 1194e1dee1..eaeed60895 100644
--- a/Mathbin/Data/Set/Ncard.lean
+++ b/Mathbin/Data/Set/Ncard.lean
@@ -164,16 +164,16 @@ theorem ncard_ne_zero_of_mem (h : a ∈ s)
 #align set.ncard_ne_zero_of_mem Set.ncard_ne_zero_of_mem
 -/
 
-#print Set.Finite_of_ncard_ne_zero /-
-theorem Finite_of_ncard_ne_zero (hs : s.ncard ≠ 0) : s.Finite :=
+#print Set.finite_of_ncard_ne_zero /-
+theorem finite_of_ncard_ne_zero (hs : s.ncard ≠ 0) : s.Finite :=
   s.finite_or_infinite.elim id fun h => (hs h.ncard).elim
-#align set.finite_of_ncard_ne_zero Set.Finite_of_ncard_ne_zero
+#align set.finite_of_ncard_ne_zero Set.finite_of_ncard_ne_zero
 -/
 
-#print Set.Finite_of_ncard_pos /-
-theorem Finite_of_ncard_pos (hs : 0 < s.ncard) : s.Finite :=
-  Finite_of_ncard_ne_zero hs.Ne.symm
-#align set.finite_of_ncard_pos Set.Finite_of_ncard_pos
+#print Set.finite_of_ncard_pos /-
+theorem finite_of_ncard_pos (hs : 0 < s.ncard) : s.Finite :=
+  finite_of_ncard_ne_zero hs.Ne.symm
+#align set.finite_of_ncard_pos Set.finite_of_ncard_pos
 -/
 
 #print Set.nonempty_of_ncard_ne_zero /-
@@ -406,17 +406,17 @@ theorem ncard_image_iff
 #align set.ncard_image_iff Set.ncard_image_iff
 -/
 
-#print Set.ncard_image_ofInjective /-
-theorem ncard_image_ofInjective (s : Set α) (H : f.Injective) : (f '' s).ncard = s.ncard :=
+#print Set.ncard_image_of_injective /-
+theorem ncard_image_of_injective (s : Set α) (H : f.Injective) : (f '' s).ncard = s.ncard :=
   ncard_image_of_injOn fun x _ y _ h => H h
-#align set.ncard_image_of_injective Set.ncard_image_ofInjective
+#align set.ncard_image_of_injective Set.ncard_image_of_injective
 -/
 
-#print Set.ncard_preimage_ofInjective_subset_range /-
-theorem ncard_preimage_ofInjective_subset_range {s : Set β} (H : f.Injective)
+#print Set.ncard_preimage_of_injective_subset_range /-
+theorem ncard_preimage_of_injective_subset_range {s : Set β} (H : f.Injective)
     (hs : s ⊆ Set.range f) : (f ⁻¹' s).ncard = s.ncard := by
   rw [← ncard_image_of_injective _ H, image_preimage_eq_iff.mpr hs]
-#align set.ncard_preimage_of_injective_subset_range Set.ncard_preimage_ofInjective_subset_range
+#align set.ncard_preimage_of_injective_subset_range Set.ncard_preimage_of_injective_subset_range
 -/
 
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic to_finite_tac -/
@@ -437,7 +437,7 @@ theorem fiber_ncard_ne_zero_iff_mem_image {y : β}
 #print Set.ncard_map /-
 @[simp]
 theorem ncard_map (f : α ↪ β) : (f '' s).ncard = s.ncard :=
-  ncard_image_ofInjective _ f.Injective
+  ncard_image_of_injective _ f.Injective
 #align set.ncard_map Set.ncard_map
 -/
 
@@ -554,8 +554,8 @@ theorem ncard_strictMono [Finite α] : @StrictMono (Set α) _ _ _ ncard := fun _
 -/
 
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic to_finite_tac -/
-#print Set.ncard_eq_ofBijective /-
-theorem ncard_eq_ofBijective {n : ℕ} (f : ∀ i, i < n → α)
+#print Set.ncard_eq_of_bijective /-
+theorem ncard_eq_of_bijective {n : ℕ} (f : ∀ i, i < n → α)
     (hf : ∀ a ∈ s, ∃ i, ∃ h : i < n, f i h = a) (hf' : ∀ (i) (h : i < n), f i h ∈ s)
     (f_inj : ∀ (i j) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j)
     (hs : s.Finite := by
@@ -565,7 +565,7 @@ theorem ncard_eq_ofBijective {n : ℕ} (f : ∀ i, i < n → α)
   rw [ncard_eq_to_finset_card _ hs]
   apply Finset.card_eq_of_bijective
   all_goals simpa
-#align set.ncard_eq_of_bijective Set.ncard_eq_ofBijective
+#align set.ncard_eq_of_bijective Set.ncard_eq_of_bijective
 -/
 
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic to_finite_tac -/
@@ -951,24 +951,24 @@ theorem exists_intermediate_Set (i : ℕ) (h₁ : i + s.ncard ≤ t.ncard) (h₂
 #align set.exists_intermediate_set Set.exists_intermediate_Set
 -/
 
-#print Set.exists_intermediate_Set' /-
-theorem exists_intermediate_Set' {m : ℕ} (hs : s.ncard ≤ m) (ht : m ≤ t.ncard) (h : s ⊆ t) :
+#print Set.exists_intermediate_set' /-
+theorem exists_intermediate_set' {m : ℕ} (hs : s.ncard ≤ m) (ht : m ≤ t.ncard) (h : s ⊆ t) :
     ∃ r : Set α, s ⊆ r ∧ r ⊆ t ∧ r.ncard = m :=
   by
   obtain ⟨r, hsr, hrt, hc⟩ :=
     exists_intermediate_set (m - s.ncard) (by rwa [tsub_add_cancel_of_le hs]) h
   rw [tsub_add_cancel_of_le hs] at hc 
   exact ⟨r, hsr, hrt, hc⟩
-#align set.exists_intermediate_set' Set.exists_intermediate_Set'
+#align set.exists_intermediate_set' Set.exists_intermediate_set'
 -/
 
-#print Set.exists_smaller_Set /-
+#print Set.exists_smaller_set /-
 /-- We can shrink `s` to any smaller size. -/
-theorem exists_smaller_Set (s : Set α) (i : ℕ) (h₁ : i ≤ s.ncard) :
+theorem exists_smaller_set (s : Set α) (i : ℕ) (h₁ : i ≤ s.ncard) :
     ∃ t : Set α, t ⊆ s ∧ t.ncard = i :=
   (exists_intermediate_Set i (by simpa) (empty_subset s)).imp fun t ht =>
     ⟨ht.2.1, by simpa using ht.2.2⟩
-#align set.exists_smaller_set Set.exists_smaller_Set
+#align set.exists_smaller_set Set.exists_smaller_set
 -/
 
 /- warning: set.infinite.exists_subset_ncard_eq clashes with set.Infinite.exists_subset_ncard_eq -> Set.Infinite.exists_subset_ncard_eq
diff --git a/Mathbin/LinearAlgebra/ExteriorAlgebra/OfAlternating.lean b/Mathbin/LinearAlgebra/ExteriorAlgebra/OfAlternating.lean
index 7cd2c8aad8..a40c376349 100644
--- a/Mathbin/LinearAlgebra/ExteriorAlgebra/OfAlternating.lean
+++ b/Mathbin/LinearAlgebra/ExteriorAlgebra/OfAlternating.lean
@@ -34,15 +34,18 @@ variable [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup N']
 
 variable [Module R M] [Module R N] [Module R N']
 
+#print AlternatingMap.ModuleAddCommGroup /-
 -- This instance can't be found where it's needed if we don't remind lean that it exists.
-instance AlternatingMap.moduleAddCommGroup {ι : Type _} : Module R (AlternatingMap R M N ι) := by
+instance AlternatingMap.ModuleAddCommGroup {ι : Type _} : Module R (AlternatingMap R M N ι) := by
   infer_instance
-#align alternating_map.module_add_comm_group AlternatingMap.moduleAddCommGroup
+#align alternating_map.module_add_comm_group AlternatingMap.ModuleAddCommGroup
+-/
 
 namespace ExteriorAlgebra
 
 open CliffordAlgebra hiding ι
 
+#print ExteriorAlgebra.liftAlternating /-
 /-- Build a map out of the exterior algebra given a collection of alternating maps acting on each
 exterior power -/
 def liftAlternating : (∀ i, AlternatingMap R M N (Fin i)) →ₗ[R] ExteriorAlgebra R M →ₗ[R] N :=
@@ -69,7 +72,9 @@ def liftAlternating : (∀ i, AlternatingMap R M N (Fin i)) →ₗ[R] ExteriorAl
     ext i : 1
     exact AlternatingMap.curryLeft_same _ _
 #align exterior_algebra.lift_alternating ExteriorAlgebra.liftAlternating
+-/
 
+#print ExteriorAlgebra.liftAlternating_ι /-
 @[simp]
 theorem liftAlternating_ι (f : ∀ i, AlternatingMap R M N (Fin i)) (m : M) :
     liftAlternating f (ι R m) = f 1 ![m] :=
@@ -78,7 +83,9 @@ theorem liftAlternating_ι (f : ∀ i, AlternatingMap R M N (Fin i)) (m : M) :
   rw [foldl_ι, LinearMap.mk₂_apply, AlternatingMap.curryLeft_apply_apply]
   congr
 #align exterior_algebra.lift_alternating_ι ExteriorAlgebra.liftAlternating_ι
+-/
 
+#print ExteriorAlgebra.liftAlternating_ι_mul /-
 theorem liftAlternating_ι_mul (f : ∀ i, AlternatingMap R M N (Fin i)) (m : M)
     (x : ExteriorAlgebra R M) :
     liftAlternating f (ι R m * x) = liftAlternating (fun i => (f i.succ).curryLeft m) x :=
@@ -87,7 +94,9 @@ theorem liftAlternating_ι_mul (f : ∀ i, AlternatingMap R M N (Fin i)) (m : M)
   rw [foldl_mul, foldl_ι]
   rfl
 #align exterior_algebra.lift_alternating_ι_mul ExteriorAlgebra.liftAlternating_ι_mul
+-/
 
+#print ExteriorAlgebra.liftAlternating_one /-
 @[simp]
 theorem liftAlternating_one (f : ∀ i, AlternatingMap R M N (Fin i)) :
     liftAlternating f (1 : ExteriorAlgebra R M) = f 0 0 :=
@@ -95,13 +104,17 @@ theorem liftAlternating_one (f : ∀ i, AlternatingMap R M N (Fin i)) :
   dsimp [lift_alternating]
   rw [foldl_one]
 #align exterior_algebra.lift_alternating_one ExteriorAlgebra.liftAlternating_one
+-/
 
+#print ExteriorAlgebra.liftAlternating_algebraMap /-
 @[simp]
 theorem liftAlternating_algebraMap (f : ∀ i, AlternatingMap R M N (Fin i)) (r : R) :
     liftAlternating f (algebraMap _ (ExteriorAlgebra R M) r) = r • f 0 0 := by
   rw [Algebra.algebraMap_eq_smul_one, map_smul, lift_alternating_one]
 #align exterior_algebra.lift_alternating_algebra_map ExteriorAlgebra.liftAlternating_algebraMap
+-/
 
+#print ExteriorAlgebra.liftAlternating_apply_ιMulti /-
 @[simp]
 theorem liftAlternating_apply_ιMulti {n : ℕ} (f : ∀ i, AlternatingMap R M N (Fin i))
     (v : Fin n → M) : liftAlternating f (ιMulti R n v) = f n v :=
@@ -114,13 +127,17 @@ theorem liftAlternating_apply_ιMulti {n : ℕ} (f : ∀ i, AlternatingMap R M N
     congr
     exact Matrix.cons_head_tail _
 #align exterior_algebra.lift_alternating_apply_ι_multi ExteriorAlgebra.liftAlternating_apply_ιMulti
+-/
 
+#print ExteriorAlgebra.liftAlternating_comp_ιMulti /-
 @[simp]
 theorem liftAlternating_comp_ιMulti {n : ℕ} (f : ∀ i, AlternatingMap R M N (Fin i)) :
     (liftAlternating f).compAlternatingMap (ιMulti R n) = f n :=
   AlternatingMap.ext <| liftAlternating_apply_ιMulti f
 #align exterior_algebra.lift_alternating_comp_ι_multi ExteriorAlgebra.liftAlternating_comp_ιMulti
+-/
 
+#print ExteriorAlgebra.liftAlternating_comp /-
 @[simp]
 theorem liftAlternating_comp (g : N →ₗ[R] N') (f : ∀ i, AlternatingMap R M N (Fin i)) :
     (liftAlternating fun i => g.compAlternatingMap (f i)) = g ∘ₗ liftAlternating f :=
@@ -135,7 +152,9 @@ theorem liftAlternating_comp (g : N →ₗ[R] N') (f : ∀ i, AlternatingMap R M
   · rw [lift_alternating_ι_mul, lift_alternating_ι_mul, ← hx]
     simp_rw [AlternatingMap.curryLeft_compAlternatingMap]
 #align exterior_algebra.lift_alternating_comp ExteriorAlgebra.liftAlternating_comp
+-/
 
+#print ExteriorAlgebra.liftAlternating_ιMulti /-
 @[simp]
 theorem liftAlternating_ιMulti :
     liftAlternating (ι_multi R) = (LinearMap.id : ExteriorAlgebra R M →ₗ[R] ExteriorAlgebra R M) :=
@@ -149,7 +168,9 @@ theorem liftAlternating_ιMulti :
     simp_rw [lift_alternating_ι_mul, ι_multi_succ_curry_left, lift_alternating_comp,
       LinearMap.comp_apply, LinearMap.mulLeft_apply, hx]
 #align exterior_algebra.lift_alternating_ι_multi ExteriorAlgebra.liftAlternating_ιMulti
+-/
 
+#print ExteriorAlgebra.liftAlternatingEquiv /-
 /-- `exterior_algebra.lift_alternating` is an equivalence. -/
 @[simps apply symm_apply]
 def liftAlternatingEquiv : (∀ i, AlternatingMap R M N (Fin i)) ≃ₗ[R] ExteriorAlgebra R M →ₗ[R] N
@@ -162,7 +183,9 @@ def liftAlternatingEquiv : (∀ i, AlternatingMap R M N (Fin i)) ≃ₗ[R] Exter
   right_inv F :=
     (liftAlternating_comp _ _).trans <| by rw [lift_alternating_ι_multi, LinearMap.comp_id]
 #align exterior_algebra.lift_alternating_equiv ExteriorAlgebra.liftAlternatingEquiv
+-/
 
+#print ExteriorAlgebra.lhom_ext /-
 /-- To show that two linear maps from the exterior algebra agree, it suffices to show they agree on
 the exterior powers.
 
@@ -172,6 +195,7 @@ theorem lhom_ext ⦃f g : ExteriorAlgebra R M →ₗ[R] N⦄
     (h : ∀ i, f.compAlternatingMap (ιMulti R i) = g.compAlternatingMap (ιMulti R i)) : f = g :=
   liftAlternatingEquiv.symm.Injective <| funext h
 #align exterior_algebra.lhom_ext ExteriorAlgebra.lhom_ext
+-/
 
 end ExteriorAlgebra
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 7cc1a497cc..5840a74594 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -10,15 +10,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "b85d825e0d9c8bb54263971eb6a50cc63567f0b5",
+    "rev": "2005b4210392b46495fcb550539467d383198e16",
     "name": "lean3port",
-    "inputRev?": "b85d825e0d9c8bb54263971eb6a50cc63567f0b5"}},
+    "inputRev?": "2005b4210392b46495fcb550539467d383198e16"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "52d95f2b56b6e50a976e92f6391d10b10c64a75b",
+    "rev": "d93a0a4d5d3c5f6e89a1b904d3fc09ac2b743950",
     "name": "mathlib",
-    "inputRev?": "52d95f2b56b6e50a976e92f6391d10b10c64a75b"}},
+    "inputRev?": "d93a0a4d5d3c5f6e89a1b904d3fc09ac2b743950"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
diff --git a/lakefile.lean b/lakefile.lean
index 2eaee3684b..e351605b60 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-06-26-01"
+def tag : String := "nightly-2023-06-26-03"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"b85d825e0d9c8bb54263971eb6a50cc63567f0b5"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"2005b4210392b46495fcb550539467d383198e16"
 
 @[default_target]
 lean_lib Mathbin where