bump to nightly-2023-06-13-13

mathlib commit leanprover-community/mathlib@9fb8964

Mathbin/MeasureTheory/Function/ConditionalExpectation/Basic.lean

@@ -98,7 +98,7 @@ noncomputable irreducible_def condexp (m : MeasurableSpace α) {m0 : MeasurableS
     if h : SigmaFinite (μ.trim hm) ∧ Integrable f μ then
       if strongly_measurable[m] f then f
       else
-        (@aeStronglyMeasurable'_condexpL1 _ _ _ _ _ m m0 μ hm h.1 _).mk
+        (@aEStronglyMeasurable'_condexpL1 _ _ _ _ _ m m0 μ hm h.1 _).mk
           (@condexpL1 _ _ _ _ _ _ _ hm μ h.1 f)
     else 0
   else 0
@@ -119,7 +119,7 @@ theorem condexp_of_sigmaFinite (hm : m ≤ m0) [hμm : SigmaFinite (μ.trim hm)]
     μ[f|m] =
       if Integrable f μ then
         if strongly_measurable[m] f then f
-        else aeStronglyMeasurable'_condexpL1.mk (condexpL1 hm μ f)
+        else aEStronglyMeasurable'_condexpL1.mk (condexpL1 hm μ f)
       else 0 :=
   by
   rw [condexp, dif_pos hm]
@@ -213,13 +213,13 @@ theorem condexp_congr_ae (h : f =ᵐ[μ] g) : μ[f|m] =ᵐ[μ] μ[g|m] :=
         (condexp_ae_eq_condexp_L1 hm g).symm)
 #align measure_theory.condexp_congr_ae MeasureTheory.condexp_congr_ae
 
-theorem condexp_of_aeStronglyMeasurable' (hm : m ≤ m0) [hμm : SigmaFinite (μ.trim hm)] {f : α → F'}
-    (hf : AeStronglyMeasurable' m f μ) (hfi : Integrable f μ) : μ[f|m] =ᵐ[μ] f :=
+theorem condexp_of_aEStronglyMeasurable' (hm : m ≤ m0) [hμm : SigmaFinite (μ.trim hm)] {f : α → F'}
+    (hf : AEStronglyMeasurable' m f μ) (hfi : Integrable f μ) : μ[f|m] =ᵐ[μ] f :=
   by
   refine' ((condexp_congr_ae hf.ae_eq_mk).trans _).trans hf.ae_eq_mk.symm
   rw [condexp_of_strongly_measurable hm hf.strongly_measurable_mk
       ((integrable_congr hf.ae_eq_mk).mp hfi)]
-#align measure_theory.condexp_of_ae_strongly_measurable' MeasureTheory.condexp_of_aeStronglyMeasurable'
+#align measure_theory.condexp_of_ae_strongly_measurable' MeasureTheory.condexp_of_aEStronglyMeasurable'
 
 theorem integrable_condexp : Integrable (μ[f|m]) μ :=
   by
@@ -255,7 +255,7 @@ theorem ae_eq_condexp_of_forall_set_integral_eq (hm : m ≤ m0) [SigmaFinite (μ
     {f g : α → F'} (hf : Integrable f μ)
     (hg_int_finite : ∀ s, measurable_set[m] s → μ s < ∞ → IntegrableOn g s μ)
     (hg_eq : ∀ s : Set α, measurable_set[m] s → μ s < ∞ → ∫ x in s, g x ∂μ = ∫ x in s, f x ∂μ)
-    (hgm : AeStronglyMeasurable' m g μ) : g =ᵐ[μ] μ[f|m] :=
+    (hgm : AEStronglyMeasurable' m g μ) : g =ᵐ[μ] μ[f|m] :=
   by
   refine'
     ae_eq_of_forall_set_integral_eq_of_sigma_finite' hm hg_int_finite

Mathbin/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean

@@ -284,11 +284,11 @@ theorem condexpInd_ae_eq_condexpIndSmul (hm : m ≤ m0) [SigmaFinite (μ.trim hm
 
 variable {hm : m ≤ m0} [SigmaFinite (μ.trim hm)]
 
-theorem aeStronglyMeasurable'_condexpInd (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : G) :
-    AeStronglyMeasurable' m (condexpInd hm μ s x) μ :=
-  AeStronglyMeasurable'.congr (aeStronglyMeasurable'_condexpIndSmul hm hs hμs x)
+theorem aEStronglyMeasurable'_condexpInd (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : G) :
+    AEStronglyMeasurable' m (condexpInd hm μ s x) μ :=
+  AEStronglyMeasurable'.congr (aEStronglyMeasurable'_condexpIndSmul hm hs hμs x)
     (condexpInd_ae_eq_condexpIndSmul hm hs hμs x).symm
-#align measure_theory.ae_strongly_measurable'_condexp_ind MeasureTheory.aeStronglyMeasurable'_condexpInd
+#align measure_theory.ae_strongly_measurable'_condexp_ind MeasureTheory.aEStronglyMeasurable'_condexpInd
 
 @[simp]
 theorem condexpInd_empty : condexpInd hm μ ∅ = (0 : G →L[ℝ] α →₁[μ] G) :=
@@ -470,8 +470,8 @@ theorem set_integral_condexpL1Clm (f : α →₁[μ] F') (hs : measurable_set[m]
   exact tendsto_nhds_unique h_left h_right
 #align measure_theory.set_integral_condexp_L1_clm MeasureTheory.set_integral_condexpL1Clm
 
-theorem aeStronglyMeasurable'_condexpL1Clm (f : α →₁[μ] F') :
-    AeStronglyMeasurable' m (condexpL1Clm hm μ f) μ :=
+theorem aEStronglyMeasurable'_condexpL1Clm (f : α →₁[μ] F') :
+    AEStronglyMeasurable' m (condexpL1Clm hm μ f) μ :=
   by
   refine'
     Lp.induction ENNReal.one_ne_top
@@ -490,7 +490,7 @@ theorem aeStronglyMeasurable'_condexpL1Clm (f : α →₁[μ] F') :
     rw [this]
     refine' IsClosed.preimage (condexp_L1_clm hm μ).Continuous _
     exact is_closed_ae_strongly_measurable' hm
-#align measure_theory.ae_strongly_measurable'_condexp_L1_clm MeasureTheory.aeStronglyMeasurable'_condexpL1Clm
+#align measure_theory.ae_strongly_measurable'_condexp_L1_clm MeasureTheory.aEStronglyMeasurable'_condexpL1Clm
 
 theorem condexpL1Clm_lpMeas (f : lpMeas F' ℝ m 1 μ) : condexpL1Clm hm μ (f : α →₁[μ] F') = ↑f :=
   by
@@ -519,10 +519,10 @@ theorem condexpL1Clm_lpMeas (f : lpMeas F' ℝ m 1 μ) : condexpL1Clm hm μ (f :
       exact LinearIsometryEquiv.continuous _
 #align measure_theory.condexp_L1_clm_Lp_meas MeasureTheory.condexpL1Clm_lpMeas
 
-theorem condexpL1Clm_of_aeStronglyMeasurable' (f : α →₁[μ] F') (hfm : AeStronglyMeasurable' m f μ) :
+theorem condexpL1Clm_of_aEStronglyMeasurable' (f : α →₁[μ] F') (hfm : AEStronglyMeasurable' m f μ) :
     condexpL1Clm hm μ f = f :=
   condexpL1Clm_lpMeas (⟨f, hfm⟩ : lpMeas F' ℝ m 1 μ)
-#align measure_theory.condexp_L1_clm_of_ae_strongly_measurable' MeasureTheory.condexpL1Clm_of_aeStronglyMeasurable'
+#align measure_theory.condexp_L1_clm_of_ae_strongly_measurable' MeasureTheory.condexpL1Clm_of_aEStronglyMeasurable'
 
 /-- Conditional expectation of a function, in L1. Its value is 0 if the function is not
 integrable. The function-valued `condexp` should be used instead in most cases. -/
@@ -548,16 +548,16 @@ theorem condexpL1_measure_zero (hm : m ≤ m0) : condexpL1 hm (0 : Measure α) f
   setToFun_measure_zero _ rfl
 #align measure_theory.condexp_L1_measure_zero MeasureTheory.condexpL1_measure_zero
 
-theorem aeStronglyMeasurable'_condexpL1 {f : α → F'} :
-    AeStronglyMeasurable' m (condexpL1 hm μ f) μ :=
+theorem aEStronglyMeasurable'_condexpL1 {f : α → F'} :
+    AEStronglyMeasurable' m (condexpL1 hm μ f) μ :=
   by
   by_cases hf : integrable f μ
   · rw [condexp_L1_eq hf]
     exact ae_strongly_measurable'_condexp_L1_clm _
   · rw [condexp_L1_undef hf]
     refine' ae_strongly_measurable'.congr _ (coe_fn_zero _ _ _).symm
     exact strongly_measurable.ae_strongly_measurable' (@strongly_measurable_zero _ _ m _ _)
-#align measure_theory.ae_strongly_measurable'_condexp_L1 MeasureTheory.aeStronglyMeasurable'_condexpL1
+#align measure_theory.ae_strongly_measurable'_condexp_L1 MeasureTheory.aEStronglyMeasurable'_condexpL1
 
 theorem condexpL1_congr_ae (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (h : f =ᵐ[μ] g) :
     condexpL1 hm μ f = condexpL1 hm μ g :=
@@ -597,14 +597,14 @@ theorem condexpL1_sub (hf : Integrable f μ) (hg : Integrable g μ) :
   setToFun_sub _ hf hg
 #align measure_theory.condexp_L1_sub MeasureTheory.condexpL1_sub
 
-theorem condexpL1_of_aeStronglyMeasurable' (hfm : AeStronglyMeasurable' m f μ)
+theorem condexpL1_of_aEStronglyMeasurable' (hfm : AEStronglyMeasurable' m f μ)
     (hfi : Integrable f μ) : condexpL1 hm μ f =ᵐ[μ] f :=
   by
   rw [condexp_L1_eq hfi]
   refine' eventually_eq.trans _ (integrable.coe_fn_to_L1 hfi)
   rw [condexp_L1_clm_of_ae_strongly_measurable']
   exact ae_strongly_measurable'.congr hfm (integrable.coe_fn_to_L1 hfi).symm
-#align measure_theory.condexp_L1_of_ae_strongly_measurable' MeasureTheory.condexpL1_of_aeStronglyMeasurable'
+#align measure_theory.condexp_L1_of_ae_strongly_measurable' MeasureTheory.condexpL1_of_aEStronglyMeasurable'
 
 theorem condexpL1_mono {E} [NormedLatticeAddCommGroup E] [CompleteSpace E] [NormedSpace ℝ E]
     [OrderedSMul ℝ E] {f g : α → E} (hf : Integrable f μ) (hg : Integrable g μ) (hfg : f ≤ᵐ[μ] g) :

Mathbin/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean

@@ -78,10 +78,10 @@ noncomputable def condexpL2 (hm : m ≤ m0) : (α →₂[μ] E) →L[𝕜] lpMea
 
 variable {𝕜}
 
-theorem aeStronglyMeasurable'_condexpL2 (hm : m ≤ m0) (f : α →₂[μ] E) :
-    AeStronglyMeasurable' m (condexpL2 𝕜 hm f) μ :=
+theorem aEStronglyMeasurable'_condexpL2 (hm : m ≤ m0) (f : α →₂[μ] E) :
+    AEStronglyMeasurable' m (condexpL2 𝕜 hm f) μ :=
   lpMeas.aeStronglyMeasurable' _
-#align measure_theory.ae_strongly_measurable'_condexp_L2 MeasureTheory.aeStronglyMeasurable'_condexpL2
+#align measure_theory.ae_strongly_measurable'_condexp_L2 MeasureTheory.aEStronglyMeasurable'_condexpL2
 
 theorem integrableOn_condexpL2_of_measure_ne_top (hm : m ≤ m0) (hμs : μ s ≠ ∞) (f : α →₂[μ] E) :
     IntegrableOn (condexpL2 𝕜 hm f) s μ :=
@@ -141,7 +141,7 @@ theorem condexpL2_indicator_of_measurable (hm : m ≤ m0) (hs : measurable_set[m
 #align measure_theory.condexp_L2_indicator_of_measurable MeasureTheory.condexpL2_indicator_of_measurable
 
 theorem inner_condexpL2_eq_inner_fun (hm : m ≤ m0) (f g : α →₂[μ] E)
-    (hg : AeStronglyMeasurable' m g μ) : ⟪(condexpL2 𝕜 hm f : α →₂[μ] E), g⟫₂ = ⟪f, g⟫₂ :=
+    (hg : AEStronglyMeasurable' m g μ) : ⟪(condexpL2 𝕜 hm f : α →₂[μ] E), g⟫₂ = ⟪f, g⟫₂ :=
   by
   symm
   rw [← sub_eq_zero, ← inner_sub_left, condexp_L2]
@@ -409,8 +409,8 @@ noncomputable def condexpIndSmul (hm : m ≤ m0) (hs : MeasurableSet s) (hμs :
   (toSpanSingleton ℝ x).compLpL 2 μ (condexpL2 ℝ hm (indicatorConstLp 2 hs hμs (1 : ℝ)))
 #align measure_theory.condexp_ind_smul MeasureTheory.condexpIndSmul
 
-theorem aeStronglyMeasurable'_condexpIndSmul (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ∞)
-    (x : G) : AeStronglyMeasurable' m (condexpIndSmul hm hs hμs x) μ :=
+theorem aEStronglyMeasurable'_condexpIndSmul (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ∞)
+    (x : G) : AEStronglyMeasurable' m (condexpIndSmul hm hs hμs x) μ :=
   by
   have h : ae_strongly_measurable' m (condexp_L2 ℝ hm (indicator_const_Lp 2 hs hμs (1 : ℝ))) μ :=
     ae_strongly_measurable'_condexp_L2 _ _
@@ -423,7 +423,7 @@ theorem aeStronglyMeasurable'_condexpIndSmul (hm : m ≤ m0) (hs : MeasurableSet
     refine' eventually_eq.trans _ (coe_fn_comp_LpL _ _).symm
     rw [Lp_meas_coe]
   exact ae_strongly_measurable'.continuous_comp (to_span_singleton ℝ x).Continuous h
-#align measure_theory.ae_strongly_measurable'_condexp_ind_smul MeasureTheory.aeStronglyMeasurable'_condexpIndSmul
+#align measure_theory.ae_strongly_measurable'_condexp_ind_smul MeasureTheory.aEStronglyMeasurable'_condexpIndSmul
 
 theorem condexpIndSmul_add (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x y : G) :
     condexpIndSmul hm hs hμs (x + y) = condexpIndSmul hm hs hμs x + condexpIndSmul hm hs hμs y := by

Mathbin/MeasureTheory/Function/ConditionalExpectation/Real.lean

@@ -348,7 +348,7 @@ theorem condexp_stronglyMeasurable_mul_of_bound (hm : m ≤ m0) [IsFiniteMeasure
 #align measure_theory.condexp_strongly_measurable_mul_of_bound MeasureTheory.condexp_stronglyMeasurable_mul_of_bound
 
 theorem condexp_strongly_measurable_mul_of_bound₀ (hm : m ≤ m0) [IsFiniteMeasure μ] {f g : α → ℝ}
-    (hf : AeStronglyMeasurable' m f μ) (hg : Integrable g μ) (c : ℝ)
+    (hf : AEStronglyMeasurable' m f μ) (hg : Integrable g μ) (c : ℝ)
     (hf_bound : ∀ᵐ x ∂μ, ‖f x‖ ≤ c) : μ[f * g|m] =ᵐ[μ] f * μ[g|m] :=
   by
   have : μ[f * g|m] =ᵐ[μ] μ[hf.mk f * g|m] :=
@@ -412,7 +412,7 @@ theorem condexp_stronglyMeasurable_mul {f g : α → ℝ} (hf : strongly_measura
 #align measure_theory.condexp_strongly_measurable_mul MeasureTheory.condexp_stronglyMeasurable_mul
 
 /-- Pull-out property of the conditional expectation. -/
-theorem condexp_strongly_measurable_mul₀ {f g : α → ℝ} (hf : AeStronglyMeasurable' m f μ)
+theorem condexp_strongly_measurable_mul₀ {f g : α → ℝ} (hf : AEStronglyMeasurable' m f μ)
     (hfg : Integrable (f * g) μ) (hg : Integrable g μ) : μ[f * g|m] =ᵐ[μ] f * μ[g|m] :=
   by
   have : μ[f * g|m] =ᵐ[μ] μ[hf.mk f * g|m] :=

Mathbin/MeasureTheory/Function/ConditionalExpectation/Unique.lean

@@ -74,7 +74,7 @@ theorem Lp.ae_eq_zero_of_forall_set_integral_eq_zero' (hm : m ≤ m0) (f : Lp E'
     (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞)
     (hf_int_finite : ∀ s, measurable_set[m] s → μ s < ∞ → IntegrableOn f s μ)
     (hf_zero : ∀ s : Set α, measurable_set[m] s → μ s < ∞ → ∫ x in s, f x ∂μ = 0)
-    (hf_meas : AeStronglyMeasurable' m f μ) : f =ᵐ[μ] 0 :=
+    (hf_meas : AEStronglyMeasurable' m f μ) : f =ᵐ[μ] 0 :=
   by
   let f_meas : Lp_meas E' 𝕜 m p μ := ⟨f, hf_meas⟩
   have hf_f_meas : f =ᵐ[μ] f_meas := by simp only [coeFn_coe_base', Subtype.coe_mk]
@@ -95,7 +95,7 @@ theorem Lp.ae_eq_of_forall_set_integral_eq' (hm : m ≤ m0) (f g : Lp E' p μ) (
     (hp_ne_top : p ≠ ∞) (hf_int_finite : ∀ s, measurable_set[m] s → μ s < ∞ → IntegrableOn f s μ)
     (hg_int_finite : ∀ s, measurable_set[m] s → μ s < ∞ → IntegrableOn g s μ)
     (hfg : ∀ s : Set α, measurable_set[m] s → μ s < ∞ → ∫ x in s, f x ∂μ = ∫ x in s, g x ∂μ)
-    (hf_meas : AeStronglyMeasurable' m f μ) (hg_meas : AeStronglyMeasurable' m g μ) : f =ᵐ[μ] g :=
+    (hf_meas : AEStronglyMeasurable' m f μ) (hg_meas : AEStronglyMeasurable' m g μ) : f =ᵐ[μ] g :=
   by
   suffices h_sub : ⇑(f - g) =ᵐ[μ] 0
   · rw [← sub_ae_eq_zero]; exact (Lp.coe_fn_sub f g).symm.trans h_sub
@@ -125,7 +125,7 @@ theorem ae_eq_of_forall_set_integral_eq_of_sigma_finite' (hm : m ≤ m0) [SigmaF
     {f g : α → F'} (hf_int_finite : ∀ s, measurable_set[m] s → μ s < ∞ → IntegrableOn f s μ)
     (hg_int_finite : ∀ s, measurable_set[m] s → μ s < ∞ → IntegrableOn g s μ)
     (hfg_eq : ∀ s : Set α, measurable_set[m] s → μ s < ∞ → ∫ x in s, f x ∂μ = ∫ x in s, g x ∂μ)
-    (hfm : AeStronglyMeasurable' m f μ) (hgm : AeStronglyMeasurable' m g μ) : f =ᵐ[μ] g :=
+    (hfm : AEStronglyMeasurable' m f μ) (hgm : AEStronglyMeasurable' m g μ) : f =ᵐ[μ] g :=
   by
   rw [← ae_eq_trim_iff_of_ae_strongly_measurable' hm hfm hgm]
   have hf_mk_int_finite :

Mathbin/Order/Category/BddLat.lean

@@ -82,13 +82,13 @@ instance hasForgetToLat : HasForget₂ BddLat LatCat
       map := fun X Y => BoundedLatticeHom.toLatticeHom }
 #align BddLat.has_forget_to_Lat BddLat.hasForgetToLat
 
-instance hasForgetToSemilatSup : HasForget₂ BddLat SemilatSup
+instance hasForgetToSemilatSup : HasForget₂ BddLat SemilatSupCat
     where forget₂ :=
     { obj := fun X => ⟨X⟩
       map := fun X Y => BoundedLatticeHom.toSupBotHom }
 #align BddLat.has_forget_to_SemilatSup BddLat.hasForgetToSemilatSup
 
-instance hasForgetToSemilatInf : HasForget₂ BddLat SemilatInf
+instance hasForgetToSemilatInf : HasForget₂ BddLat SemilatInfCat
     where forget₂ :=
     { obj := fun X => ⟨X⟩
       map := fun X Y => BoundedLatticeHom.toInfTopHom }
@@ -105,32 +105,32 @@ theorem coe_forget_to_latCat (X : BddLat) : ↥((forget₂ BddLat LatCat).obj X)
 #align BddLat.coe_forget_to_Lat BddLat.coe_forget_to_latCat
 
 @[simp]
-theorem coe_forget_to_semilatSup (X : BddLat) : ↥((forget₂ BddLat SemilatSup).obj X) = ↥X :=
+theorem coe_forget_to_semilatSupCat (X : BddLat) : ↥((forget₂ BddLat SemilatSupCat).obj X) = ↥X :=
   rfl
-#align BddLat.coe_forget_to_SemilatSup BddLat.coe_forget_to_semilatSup
+#align BddLat.coe_forget_to_SemilatSup BddLat.coe_forget_to_semilatSupCat
 
 @[simp]
-theorem coe_forget_to_semilatInf (X : BddLat) : ↥((forget₂ BddLat SemilatInf).obj X) = ↥X :=
+theorem coe_forget_to_semilatInfCat (X : BddLat) : ↥((forget₂ BddLat SemilatInfCat).obj X) = ↥X :=
   rfl
-#align BddLat.coe_forget_to_SemilatInf BddLat.coe_forget_to_semilatInf
+#align BddLat.coe_forget_to_SemilatInf BddLat.coe_forget_to_semilatInfCat
 
 theorem forget_latCat_partOrdCat_eq_forget_bddOrdCat_partOrdCat :
     forget₂ BddLat LatCat ⋙ forget₂ LatCat PartOrdCat =
       forget₂ BddLat BddOrdCat ⋙ forget₂ BddOrdCat PartOrdCat :=
   rfl
 #align BddLat.forget_Lat_PartOrd_eq_forget_BddOrd_PartOrd BddLat.forget_latCat_partOrdCat_eq_forget_bddOrdCat_partOrdCat
 
-theorem forget_semilatSup_partOrdCat_eq_forget_bddOrdCat_partOrdCat :
-    forget₂ BddLat SemilatSup ⋙ forget₂ SemilatSup PartOrdCat =
+theorem forget_semilatSupCat_partOrdCat_eq_forget_bddOrdCat_partOrdCat :
+    forget₂ BddLat SemilatSupCat ⋙ forget₂ SemilatSupCat PartOrdCat =
       forget₂ BddLat BddOrdCat ⋙ forget₂ BddOrdCat PartOrdCat :=
   rfl
-#align BddLat.forget_SemilatSup_PartOrd_eq_forget_BddOrd_PartOrd BddLat.forget_semilatSup_partOrdCat_eq_forget_bddOrdCat_partOrdCat
+#align BddLat.forget_SemilatSup_PartOrd_eq_forget_BddOrd_PartOrd BddLat.forget_semilatSupCat_partOrdCat_eq_forget_bddOrdCat_partOrdCat
 
-theorem forget_semilatInf_partOrdCat_eq_forget_bddOrdCat_partOrdCat :
-    forget₂ BddLat SemilatInf ⋙ forget₂ SemilatInf PartOrdCat =
+theorem forget_semilatInfCat_partOrdCat_eq_forget_bddOrdCat_partOrdCat :
+    forget₂ BddLat SemilatInfCat ⋙ forget₂ SemilatInfCat PartOrdCat =
       forget₂ BddLat BddOrdCat ⋙ forget₂ BddOrdCat PartOrdCat :=
   rfl
-#align BddLat.forget_SemilatInf_PartOrd_eq_forget_BddOrd_PartOrd BddLat.forget_semilatInf_partOrdCat_eq_forget_bddOrdCat_partOrdCat
+#align BddLat.forget_SemilatInf_PartOrd_eq_forget_BddOrd_PartOrd BddLat.forget_semilatInfCat_partOrdCat_eq_forget_bddOrdCat_partOrdCat
 
 /-- Constructs an equivalence between bounded lattices from an order isomorphism
 between them. -/
@@ -170,15 +170,17 @@ theorem bddLat_dual_comp_forget_to_latCat :
   rfl
 #align BddLat_dual_comp_forget_to_Lat bddLat_dual_comp_forget_to_latCat
 
-theorem bddLat_dual_comp_forget_to_semilatSup :
-    BddLat.dual ⋙ forget₂ BddLat SemilatSup = forget₂ BddLat SemilatInf ⋙ SemilatInf.dual :=
+theorem bddLat_dual_comp_forget_to_semilatSupCat :
+    BddLat.dual ⋙ forget₂ BddLat SemilatSupCat =
+      forget₂ BddLat SemilatInfCat ⋙ SemilatInfCat.dual :=
   rfl
-#align BddLat_dual_comp_forget_to_SemilatSup bddLat_dual_comp_forget_to_semilatSup
+#align BddLat_dual_comp_forget_to_SemilatSup bddLat_dual_comp_forget_to_semilatSupCat
 
-theorem bddLat_dual_comp_forget_to_semilatInf :
-    BddLat.dual ⋙ forget₂ BddLat SemilatInf = forget₂ BddLat SemilatSup ⋙ SemilatSup.dual :=
+theorem bddLat_dual_comp_forget_to_semilatInfCat :
+    BddLat.dual ⋙ forget₂ BddLat SemilatInfCat =
+      forget₂ BddLat SemilatSupCat ⋙ SemilatSupCat.dual :=
   rfl
-#align BddLat_dual_comp_forget_to_SemilatInf bddLat_dual_comp_forget_to_semilatInf
+#align BddLat_dual_comp_forget_to_SemilatInf bddLat_dual_comp_forget_to_semilatInfCat
 
 /-- The functor that adds a bottom and a top element to a lattice. This is the free functor. -/
 def latToBddLat : LatCat.{u} ⥤ BddLat