chore(CategoryTheory/MorphismProperty): Use le instead of subset (lea…

…nprover-community#12520)

Mathlib/Algebra/Homology/Localization.lean

@@ -89,9 +89,9 @@ variable (C : Type*) [Category C] {ι : Type*} (c : ComplexShape ι) [Preadditiv
 lemma HomologicalComplexUpToQuasiIso.Q_inverts_homotopyEquivalences :
     (HomologicalComplex.homotopyEquivalences C c).IsInvertedBy
       HomologicalComplexUpToQuasiIso.Q :=
-  MorphismProperty.IsInvertedBy.of_subset _ _ _
+  MorphismProperty.IsInvertedBy.of_le _ _ _
     (Localization.inverts Q (HomologicalComplex.quasiIso C c))
-    (homotopyEquivalences_subset_quasiIso C c)
+    (homotopyEquivalences_le_quasiIso C c)
 
 namespace HomotopyCategory
 
@@ -198,7 +198,7 @@ instance : HomologicalComplexUpToQuasiIso.Qh.IsLocalization (HomotopyCategory.qu
   Functor.IsLocalization.of_comp (HomotopyCategory.quotient C c)
     Qh (HomologicalComplex.homotopyEquivalences C c)
     (HomotopyCategory.quasiIso C c) (HomologicalComplex.quasiIso C c)
-    (homotopyEquivalences_subset_quasiIso C c)
+    (homotopyEquivalences_le_quasiIso C c)
     (HomotopyCategory.quasiIso_eq_quasiIso_map_quotient C c)
 
 end
@@ -236,9 +236,9 @@ lemma ComplexShape.QFactorsThroughHomotopy_of_exists_prev [CategoryWithHomology
   areEqualizedByLocalization {K L f g} h := by
     have : DecidableRel c.Rel := by classical infer_instance
     exact h.map_eq_of_inverts_homotopyEquivalences hc _
-      (MorphismProperty.IsInvertedBy.of_subset _ _ _
+      (MorphismProperty.IsInvertedBy.of_le _ _ _
         (Localization.inverts _ (HomologicalComplex.quasiIso C _))
-        (homotopyEquivalences_subset_quasiIso C _))
+        (homotopyEquivalences_le_quasiIso C _))
 
 end Cylinder
 

Mathlib/Algebra/Homology/QuasiIso.lean

@@ -497,8 +497,8 @@ instance : QuasiIso e.inv := (inferInstance : QuasiIso e.symm.hom)
 
 variable (C c)
 
-lemma homotopyEquivalences_subset_quasiIso [CategoryWithHomology C] :
-    homotopyEquivalences C c ⊆ quasiIso C c := by
+lemma homotopyEquivalences_le_quasiIso [CategoryWithHomology C] :
+    homotopyEquivalences C c ≤ quasiIso C c := by
   rintro K L _ ⟨e, rfl⟩
   simp only [HomologicalComplex.mem_quasiIso_iff]
   infer_instance

Mathlib/CategoryTheory/Localization/Composition.lean

@@ -34,11 +34,11 @@ def StrictUniversalPropertyFixedTarget.comp
     (h₁ : StrictUniversalPropertyFixedTarget L₁ W₁ E)
     (h₂ : StrictUniversalPropertyFixedTarget L₂ W₂ E)
     (W₃ : MorphismProperty C₁) (hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂))
-    (hW₁₃ : W₁ ⊆ W₃) (hW₂₃ : W₂ ⊆ W₃.map L₁) :
+    (hW₁₃ : W₁ ≤ W₃) (hW₂₃ : W₂ ≤ W₃.map L₁) :
     StrictUniversalPropertyFixedTarget (L₁ ⋙ L₂) W₃ E where
   inverts := hW₃
-  lift F hF := h₂.lift (h₁.lift F (MorphismProperty.IsInvertedBy.of_subset _ _  F hF hW₁₃)) (by
-    refine' MorphismProperty.IsInvertedBy.of_subset _ _ _ _ hW₂₃
+  lift F hF := h₂.lift (h₁.lift F (MorphismProperty.IsInvertedBy.of_le _ _  F hF hW₁₃)) (by
+    refine' MorphismProperty.IsInvertedBy.of_le _ _ _ _ hW₂₃
     simpa only [MorphismProperty.IsInvertedBy.map_iff, h₁.fac F] using hF)
   fac F hF := by rw [Functor.assoc, h₂.fac, h₁.fac]
   uniq F₁ F₂ h := h₂.uniq _ _ (h₁.uniq _ _ (by simpa only [Functor.assoc] using h))
@@ -55,7 +55,7 @@ variable (L₁ W₁ L₂ W₂)
 
 lemma comp [L₁.IsLocalization W₁] [L₂.IsLocalization W₂]
     (W₃ : MorphismProperty C₁) (hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂))
-    (hW₁₃ : W₁ ⊆ W₃) (hW₂₃ : W₂ ⊆ W₃.map L₁) :
+    (hW₁₃ : W₁ ≤ W₃) (hW₂₃ : W₂ ≤ W₃.map L₁) :
     (L₁ ⋙ L₂).IsLocalization W₃ := by
   -- The proof proceeds by reducing to the case of the constructed
   -- localized categories, which satisfy the strict universal property
@@ -74,7 +74,7 @@ lemma comp [L₁.IsLocalization W₁] [L₂.IsLocalization W₂]
           W₂.isoClosure_respectsIso E₂.functor
         rw [MorphismProperty.map_isoClosure] at eq
         rw [eq]
-        apply W₂.subset_isoClosure }
+        apply W₂.le_isoClosure }
   have := LocalizerMorphism.IsLocalizedEquivalence.of_equivalence Φ (by rfl)
   -- The fact that `Φ` is a localized equivalence allows to consider
   -- the induced equivalence of categories `E₃ : C₃ ≅ W₂'.Localization`, and
@@ -94,9 +94,9 @@ lemma comp [L₁.IsLocalization W₁] [L₂.IsLocalization W₂]
   have hW₃' : W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q) := by
     simpa only [← MorphismProperty.IsInvertedBy.iff_comp _ _ E₃.inverse,
       MorphismProperty.IsInvertedBy.iff_of_iso W₃ iso] using hW₃
-  have hW₂₃' : W₂' ⊆ W₃.map W₁.Q := (MorphismProperty.monotone_map _ _ E₂.functor hW₂₃).trans
+  have hW₂₃' : W₂' ≤ W₃.map W₁.Q := (MorphismProperty.monotone_map E₂.functor hW₂₃).trans
     (by simpa only [W₃.map_map]
-      using subset_of_eq (W₃.map_eq_of_iso (compUniqFunctor L₁ W₁.Q W₁)))
+      using le_of_eq (W₃.map_eq_of_iso (compUniqFunctor L₁ W₁.Q W₁)))
   have : (W₁.Q ⋙ W₂'.Q).IsLocalization W₃ := by
     refine' IsLocalization.mk' _ _ _ _
     all_goals
@@ -108,7 +108,7 @@ lemma comp [L₁.IsLocalization W₁] [L₂.IsLocalization W₂]
 
 lemma of_comp (W₃ : MorphismProperty C₁)
     [L₁.IsLocalization W₁] [(L₁ ⋙ L₂).IsLocalization W₃]
-    (hW₁₃ : W₁ ⊆ W₃) (hW₂₃ : W₂ = W₃.map L₁) :
+    (hW₁₃ : W₁ ≤ W₃) (hW₂₃ : W₂ = W₃.map L₁) :
     L₂.IsLocalization W₂ := by
     have : (L₁ ⋙ W₂.Q).IsLocalization W₃ :=
       comp L₁ W₂.Q W₁ W₂ W₃ (fun X Y f hf => Localization.inverts W₂.Q W₂ _

Mathlib/CategoryTheory/Localization/Equivalence.lean

@@ -66,7 +66,7 @@ the case of a functor `L₂ : C₂ ⥤ D` for a suitable `W₂ : MorphismPropert
 we have an equivalence of category `E : C₁ ≌ C₂` and an isomorphism `E.functor ⋙ L₂ ≅ L₁`. -/
 lemma of_equivalence_source (L₁ : C₁ ⥤ D) (W₁ : MorphismProperty C₁)
     (L₂ : C₂ ⥤ D) (W₂ : MorphismProperty C₂)
-    (E : C₁ ≌ C₂) (hW₁ : W₁ ⊆ W₂.isoClosure.inverseImage E.functor) (hW₂ : W₂.IsInvertedBy L₂)
+    (E : C₁ ≌ C₂) (hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor) (hW₂ : W₂.IsInvertedBy L₂)
     [L₁.IsLocalization W₁] (iso : E.functor ⋙ L₂ ≅ L₁) : L₂.IsLocalization W₂ := by
   have h : W₁.IsInvertedBy (E.functor ⋙ W₂.Q) := fun _ _ f hf => by
     obtain ⟨_, _, f', hf', ⟨e⟩⟩ := hW₁ f hf
@@ -99,7 +99,7 @@ a suitable `W₂ : MorphismProperty C₂`. -/
 lemma of_equivalences (L₁ : C₁ ⥤ D₁) (W₁ : MorphismProperty C₁) [L₁.IsLocalization W₁]
     (L₂ : C₂ ⥤ D₂) (W₂ : MorphismProperty C₂)
     (E : C₁ ≌ C₂) (E' : D₁ ≌ D₂) [CatCommSq E.functor L₁ L₂ E'.functor]
-    (hW₁ : W₁ ⊆ W₂.isoClosure.inverseImage E.functor) (hW₂ : W₂.IsInvertedBy L₂) :
+    (hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor) (hW₂ : W₂.IsInvertedBy L₂) :
     L₂.IsLocalization W₂ := by
   haveI : (E.functor ⋙ L₂).IsLocalization W₁ :=
     of_equivalence_target L₁ W₁ _ E' ((CatCommSq.iso _ _ _ _).symm)

Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean

@@ -42,7 +42,7 @@ structure LocalizerMorphism where
   /-- a functor between the two categories -/
   functor : C₁ ⥤ C₂
   /-- the functor is compatible with the `MorphismProperty` -/
-  map : W₁ ⊆ W₂.inverseImage functor
+  map : W₁ ≤ W₂.inverseImage functor
 
 namespace LocalizerMorphism
 
@@ -157,7 +157,7 @@ lemma IsLocalizedEquivalence.of_isLocalization_of_isLocalization
 an equivalence of categories and that `W₁` and `W₂` essentially correspond to each
 other via this equivalence, then `Φ` is a localized equivalence. -/
 lemma IsLocalizedEquivalence.of_equivalence [Φ.functor.IsEquivalence]
-    (h : W₂ ⊆ W₁.map Φ.functor) : IsLocalizedEquivalence Φ := by
+    (h : W₂ ≤ W₁.map Φ.functor) : IsLocalizedEquivalence Φ := by
   haveI : Functor.IsLocalization (Φ.functor ⋙ MorphismProperty.Q W₂) W₁ := by
     refine' Functor.IsLocalization.of_equivalence_source W₂.Q W₂ (Φ.functor ⋙ W₂.Q) W₁
       (Functor.asEquivalence Φ.functor).symm _ (Φ.inverts W₂.Q)

Mathlib/CategoryTheory/Localization/Pi.lean

@@ -89,7 +89,7 @@ instance {J : Type} [Finite J] {C : Type u₁} {D : Type u₂} [Category.{v₁}
   refine Functor.IsLocalization.of_equivalences L₁
     (MorphismProperty.pi (fun _ => W)) L₂ _ E E' ?_ ?_
   · intro X Y f hf
-    exact MorphismProperty.subset_isoClosure _ _ (fun ⟨j⟩ => hf j)
+    exact MorphismProperty.le_isoClosure _ _ (fun ⟨j⟩ => hf j)
   · intro X Y f hf
     have : ∀ (j : Discrete J), IsIso ((L₂.map f).app j) :=
       fun j => Localization.inverts L W _ (hf j)

Mathlib/CategoryTheory/Localization/Predicate.lean

@@ -104,7 +104,7 @@ instance : Inhabited (StrictUniversalPropertyFixedTarget W.Q W E) :=
 /-- When `W` consists of isomorphisms, the identity satisfies the universal property
 of the localization. -/
 @[simps]
-def strictUniversalPropertyFixedTargetId (hW : W ⊆ MorphismProperty.isomorphisms C) :
+def strictUniversalPropertyFixedTargetId (hW : W ≤ MorphismProperty.isomorphisms C) :
     StrictUniversalPropertyFixedTarget (𝟭 C) W E
     where
   inverts X Y f hf := hW f hf
@@ -147,7 +147,7 @@ theorem IsLocalization.mk' (h₁ : Localization.StrictUniversalPropertyFixedTarg
             rfl } }
 #align category_theory.functor.is_localization.mk' CategoryTheory.Functor.IsLocalization.mk'
 
-theorem IsLocalization.for_id (hW : W ⊆ MorphismProperty.isomorphisms C) : (𝟭 C).IsLocalization W :=
+theorem IsLocalization.for_id (hW : W ≤ MorphismProperty.isomorphisms C) : (𝟭 C).IsLocalization W :=
   IsLocalization.mk' _ _ (Localization.strictUniversalPropertyFixedTargetId W _ hW)
     (Localization.strictUniversalPropertyFixedTargetId W _ hW)
 #align category_theory.functor.is_localization.for_id CategoryTheory.Functor.IsLocalization.for_id
@@ -442,7 +442,7 @@ theorem of_equivalence_target {E : Type*} [Category E] (L' : C ⥤ E) (eq : D 
 #align category_theory.functor.is_localization.of_equivalence_target CategoryTheory.Functor.IsLocalization.of_equivalence_target
 
 lemma of_isEquivalence (L : C ⥤ D) (W : MorphismProperty C)
-    (hW : W ⊆ MorphismProperty.isomorphisms C) [IsEquivalence L] :
+    (hW : W ≤ MorphismProperty.isomorphisms C) [IsEquivalence L] :
     L.IsLocalization W := by
   haveI : (𝟭 C).IsLocalization W := for_id W hW
   exact of_equivalence_target (𝟭 C) W L L.asEquivalence L.leftUnitor

Mathlib/CategoryTheory/MorphismProperty/Basic.lean

@@ -5,7 +5,7 @@ Authors: Andrew Yang
 -/
 import Mathlib.CategoryTheory.Comma.Arrow
 import Mathlib.CategoryTheory.Pi.Basic
-import Mathlib.Order.CompleteLattice
+import Mathlib.Order.CompleteBooleanAlgebra
 
 #align_import category_theory.morphism_property from "leanprover-community/mathlib"@"7f963633766aaa3ebc8253100a5229dd463040c7"
 
@@ -36,9 +36,12 @@ def MorphismProperty :=
   ∀ ⦃X Y : C⦄ (_ : X ⟶ Y), Prop
 #align category_theory.morphism_property CategoryTheory.MorphismProperty
 
-instance : CompleteLattice (MorphismProperty C) := by
-  dsimp only [MorphismProperty]
-  infer_instance
+instance : CompleteBooleanAlgebra (MorphismProperty C) where
+  le P₁ P₂ := ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P₁ f → P₂ f
+  __ := inferInstanceAs (CompleteBooleanAlgebra (∀ ⦃X Y : C⦄ (_ : X ⟶ Y), Prop))
+
+lemma MorphismProperty.le_def {P Q : MorphismProperty C} :
+    P ≤ Q ↔ ∀ {X Y : C} (f : X ⟶ Y), P f → Q f := Iff.rfl
 
 instance : Inhabited (MorphismProperty C) :=
   ⟨⊤⟩
@@ -55,26 +58,10 @@ lemma ext (W W' : MorphismProperty C) (h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f
   funext X Y f
   rw [h]
 
+@[simp]
 lemma top_apply {X Y : C} (f : X ⟶ Y) : (⊤ : MorphismProperty C) f := by
   simp only [top_eq]
 
-instance : HasSubset (MorphismProperty C) :=
-  ⟨fun P₁ P₂ => ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (_ : P₁ f), P₂ f⟩
-
-instance : IsTrans (MorphismProperty C) (· ⊆ ·) :=
-  ⟨fun _ _ _ h₁₂ h₂₃ _ _ _ h => h₂₃ _ (h₁₂ _ h)⟩
-
-instance : Inter (MorphismProperty C) :=
-  ⟨fun P₁ P₂ _ _ f => P₁ f ∧ P₂ f⟩
-
-lemma subset_iff_le (P Q : MorphismProperty C) : P ⊆ Q ↔ P ≤ Q := Iff.rfl
-
-instance : IsAntisymm (MorphismProperty C) (· ⊆ ·) :=
-  ⟨fun P Q => by simpa only [subset_iff_le] using le_antisymm⟩
-
-instance : IsRefl (MorphismProperty C) (· ⊆ ·) :=
-  ⟨fun P => by simpa only [subset_iff_le] using le_refl P⟩
-
 /-- The morphism property in `Cᵒᵖ` associated to a morphism property in `C` -/
 @[simp]
 def op (P : MorphismProperty C) : MorphismProperty Cᵒᵖ := fun _ _ f => P f.unop
@@ -109,9 +96,9 @@ def map (P : MorphismProperty C) (F : C ⥤ D) : MorphismProperty D := fun _ _ f
 lemma map_mem_map (P : MorphismProperty C) (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) (hf : P f) :
     (P.map F) (F.map f) := ⟨X, Y, f, hf, ⟨Iso.refl _⟩⟩
 
-lemma monotone_map (P Q : MorphismProperty C) (F : C ⥤ D) (h : P ⊆ Q) :
-    P.map F ⊆ Q.map F := by
-  intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
+lemma monotone_map (F : C ⥤ D) :
+    Monotone (map · F) := by
+  intro P Q h X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
   exact ⟨X', Y', f', h _ hf', ⟨e⟩⟩
 
 /-- A morphism property `RespectsIso` if it still holds when composed with an isomorphism -/
@@ -132,7 +119,7 @@ theorem RespectsIso.unop {P : MorphismProperty Cᵒᵖ} (h : RespectsIso P) : Re
 def isoClosure (P : MorphismProperty C) : MorphismProperty C :=
   fun _ _ f => ∃ (Y₁ Y₂ : C) (f' : Y₁ ⟶ Y₂) (_ : P f'), Nonempty (Arrow.mk f' ≅ Arrow.mk f)
 
-lemma subset_isoClosure (P : MorphismProperty C) : P ⊆ P.isoClosure :=
+lemma le_isoClosure (P : MorphismProperty C) : P ≤ P.isoClosure :=
   fun _ _ f hf => ⟨_, _, f, hf, ⟨Iso.refl _⟩⟩
 
 lemma isoClosure_respectsIso (P : MorphismProperty C) :
@@ -144,9 +131,8 @@ lemma isoClosure_respectsIso (P : MorphismProperty C) :
     ⟨_, _, f', hf', ⟨Arrow.isoMk (asIso iso.hom.left)
       (asIso iso.hom.right ≪≫ e) (by simp)⟩⟩⟩
 
-lemma monotone_isoClosure (P Q : MorphismProperty C) (h : P ⊆ Q) :
-    P.isoClosure ⊆ Q.isoClosure := by
-  intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
+lemma monotone_isoClosure : Monotone (isoClosure (C := C)) := by
+  intro P Q h X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
   exact ⟨X', Y', f', h _ hf', ⟨e⟩⟩
 
 theorem RespectsIso.cancel_left_isIso {P : MorphismProperty C} (hP : RespectsIso P) {X Y Z : C}
@@ -182,54 +168,57 @@ theorem RespectsIso.of_respects_arrow_iso (P : MorphismProperty C)
     simp only [Category.id_comp]
 #align category_theory.morphism_property.respects_iso.of_respects_arrow_iso CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso
 
-lemma RespectsIso.isoClosure_eq {P : MorphismProperty C} (hP : P.RespectsIso) :
-    P.isoClosure = P := by
-  refine' le_antisymm _ (P.subset_isoClosure)
+lemma isoClosure_eq_iff {P : MorphismProperty C} :
+    P.isoClosure = P ↔ P.RespectsIso := by
+  refine ⟨(· ▸ P.isoClosure_respectsIso), fun hP ↦ le_antisymm ?_ (P.le_isoClosure)⟩
   intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
   exact (hP.arrow_mk_iso_iff e).1 hf'
 
+lemma RespectsIso.isoClosure_eq {P : MorphismProperty C} (hP : P.RespectsIso) :
+    P.isoClosure = P := by rwa [isoClosure_eq_iff]
+
 @[simp]
 lemma isoClosure_isoClosure (P : MorphismProperty C) :
     P.isoClosure.isoClosure = P.isoClosure :=
   P.isoClosure_respectsIso.isoClosure_eq
 
-lemma isoClosure_subset_iff (P Q : MorphismProperty C) (hQ : RespectsIso Q) :
-    P.isoClosure ⊆ Q ↔ P ⊆ Q := by
+lemma isoClosure_le_iff (P Q : MorphismProperty C) (hQ : RespectsIso Q) :
+    P.isoClosure ≤ Q ↔ P ≤ Q := by
   constructor
-  · exact P.subset_isoClosure.trans
+  · exact P.le_isoClosure.trans
   · intro h
-    exact (monotone_isoClosure _ _ h).trans (by rw [hQ.isoClosure_eq])
+    exact (monotone_isoClosure h).trans (by rw [hQ.isoClosure_eq])
 
 lemma map_respectsIso (P : MorphismProperty C) (F : C ⥤ D) :
     (P.map F).RespectsIso := by
   apply RespectsIso.of_respects_arrow_iso
   intro f g e ⟨X', Y', f', hf', ⟨e'⟩⟩
   exact ⟨X', Y', f', hf', ⟨e' ≪≫ e⟩⟩
 
-lemma map_subset_iff (P : MorphismProperty C) (F : C ⥤ D)
-    (Q : MorphismProperty D) (hQ : RespectsIso Q):
-    P.map F ⊆ Q ↔ ∀ (X Y : C) (f : X ⟶ Y), P f → Q (F.map f) := by
+lemma map_le_iff {P : MorphismProperty C} {F : C ⥤ D} {Q : MorphismProperty D}
+    (hQ : RespectsIso Q) :
+    P.map F ≤ Q ↔ P ≤ Q.inverseImage F := by
   constructor
   · intro h X Y f hf
     exact h (F.map f) (map_mem_map P F f hf)
   · intro h X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
-    exact (hQ.arrow_mk_iso_iff e).1 (h _ _ _ hf')
+    exact (hQ.arrow_mk_iso_iff e).1 (h _ hf')
 
 @[simp]
 lemma map_isoClosure (P : MorphismProperty C) (F : C ⥤ D) :
     P.isoClosure.map F = P.map F := by
-  apply subset_antisymm
-  · rw [map_subset_iff _ _ _ (P.map_respectsIso F)]
+  apply le_antisymm
+  · rw [map_le_iff (P.map_respectsIso F)]
     intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
     exact ⟨_, _, f', hf', ⟨F.mapArrow.mapIso e⟩⟩
-  · exact monotone_map _ _ _ (subset_isoClosure P)
+  · exact monotone_map _ (le_isoClosure P)
 
 lemma map_id_eq_isoClosure (P : MorphismProperty C) :
     P.map (𝟭 _) = P.isoClosure := by
-  apply subset_antisymm
-  · rw [map_subset_iff _ _ _ P.isoClosure_respectsIso]
+  apply le_antisymm
+  · rw [map_le_iff P.isoClosure_respectsIso]
     intro X Y f hf
-    exact P.subset_isoClosure _ hf
+    exact P.le_isoClosure _ hf
   · intro X Y f hf
     exact hf
 
@@ -240,11 +229,11 @@ lemma map_id (P : MorphismProperty C) (hP : RespectsIso P) :
 @[simp]
 lemma map_map (P : MorphismProperty C) (F : C ⥤ D) {E : Type*} [Category E] (G : D ⥤ E) :
     (P.map F).map G = P.map (F ⋙ G) := by
-  apply subset_antisymm
-  · rw [map_subset_iff _ _ _ (map_respectsIso _ (F ⋙ G))]
+  apply le_antisymm
+  · rw [map_le_iff (map_respectsIso _ (F ⋙ G))]
     intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
     exact ⟨X', Y', f', hf', ⟨G.mapArrow.mapIso e⟩⟩
-  · rw [map_subset_iff _ _ _ (map_respectsIso _ G)]
+  · rw [map_le_iff (map_respectsIso _ G)]
     intro X Y f hf
     exact map_mem_map _ _ _ (map_mem_map _ _ _ hf)
 
@@ -261,23 +250,23 @@ theorem RespectsIso.inverseImage {P : MorphismProperty D} (h : RespectsIso P) (F
 lemma map_eq_of_iso (P : MorphismProperty C) {F G : C ⥤ D} (e : F ≅ G) :
     P.map F = P.map G := by
   revert F G e
-  suffices ∀ {F G : C ⥤ D} (_ : F ≅ G), P.map F ⊆ P.map G from
+  suffices ∀ {F G : C ⥤ D} (_ : F ≅ G), P.map F ≤ P.map G from
     fun F G e => le_antisymm (this e) (this e.symm)
   intro F G e X Y f ⟨X', Y', f', hf', ⟨e'⟩⟩
   exact ⟨X', Y', f', hf', ⟨((Functor.mapArrowFunctor _ _).mapIso e.symm).app (Arrow.mk f') ≪≫ e'⟩⟩
 
-lemma map_inverseImage_subset (P : MorphismProperty D) (F : C ⥤ D) :
-    (P.inverseImage F).map F ⊆ P.isoClosure :=
+lemma map_inverseImage_le (P : MorphismProperty D) (F : C ⥤ D) :
+    (P.inverseImage F).map F ≤ P.isoClosure :=
   fun _ _ _ ⟨_, _, f, hf, ⟨e⟩⟩ => ⟨_, _, F.map f, hf, ⟨e⟩⟩
 
 lemma inverseImage_equivalence_inverse_eq_map_functor
     (P : MorphismProperty D) (hP : RespectsIso P) (E : C ≌ D) :
     P.inverseImage E.functor = P.map E.inverse := by
-  apply subset_antisymm
+  apply le_antisymm
   · intro X Y f hf
     refine' ⟨_, _, _, hf, ⟨_⟩⟩
     exact ((Functor.mapArrowFunctor _ _).mapIso E.unitIso.symm).app (Arrow.mk f)
-  · rw [map_subset_iff _ _ _ (hP.inverseImage E.functor)]
+  · rw [map_le_iff (hP.inverseImage E.functor)]
     intro X Y f hf
     exact (hP.arrow_mk_iso_iff
       (((Functor.mapArrowFunctor _ _).mapIso E.counitIso).app (Arrow.mk f))).2 hf

Mathlib/CategoryTheory/MorphismProperty/Composition.lean

@@ -96,7 +96,7 @@ theorem StableUnderInverse.unop {P : MorphismProperty Cᵒᵖ} (h : StableUnderI
 #align category_theory.morphism_property.stable_under_inverse.unop CategoryTheory.MorphismProperty.StableUnderInverse.unop
 
 theorem respectsIso_of_isStableUnderComposition {P : MorphismProperty C}
-    [P.IsStableUnderComposition] (hP : isomorphisms C ⊆ P) :
+    [P.IsStableUnderComposition] (hP : isomorphisms C ≤ P) :
     RespectsIso P :=
   ⟨fun _ _ hf => P.comp_mem _ _ (hP _ (isomorphisms.infer_property _)) hf,
     fun _ _ hf => P.comp_mem _ _ hf (hP _ (isomorphisms.infer_property _))⟩