awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
h : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : W f'
e : Arrow.mk f' ≅ Arrow.mk f
⊢ IsIso (F.map f')

Tactic:
have := h _ hf'
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
h : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : W f'
e : Arrow.mk f' ≅ Arrow.mk f
this : IsIso (F.map f')
⊢ IsIso (F.map (Arrow.Hom.left e.inv) ≫ F.map f' ≫ F.map (Arrow.Hom.right e.hom))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
W : MorphismProperty.{v_1, u_1} C₁
F : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
G : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
inst_3 : G.ReflectsIsomorphisms
mp : W.IsInvertedBy (F ⋙ G) → W.IsInvertedBy F
mpr : W.IsInvertedBy F → W.IsInvertedBy (F ⋙ G)
⊢ W.IsInvertedBy (F ⋙ G) ↔ W.IsInvertedBy F

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
W : MorphismProperty.{v_1, u_1} C₁
F : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
G : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
inst_3 : G.ReflectsIsomorphisms
h : W.IsInvertedBy (F ⋙ G)
X Y : C₁
f : X ⟶ Y
hf : W f
⊢ IsIso (G.map (F.map f))

Tactic:
have : IsIso (G.map (F.map f)) := h _ hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
W : MorphismProperty.{v_1, u_1} C₁
F : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
G : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
inst_3 : G.ReflectsIsomorphisms
h : W.IsInvertedBy (F ⋙ G)
X Y : C₁
f : X ⟶ Y
hf : W f
this : IsIso (G.map (F.map f))
⊢ IsIso (F.map f)

Tactic:
isIso_of_reflects_iso (F.map f) G

Premises used: CategoryTheory.isIso_of_reflects_iso, CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
W : MorphismProperty.{v_1, u_1} C₁
F : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
G : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
inst_3 : G.ReflectsIsomorphisms
h : W.IsInvertedBy (F ⋙ G)
X Y : C₁
f : X ⟶ Y
hf : W f
this : IsIso (G.map (F.map f))
⊢ IsIso (F.map f)

Tactic:
exact isIso_of_reflects_iso (F.map f) G

Premises used: CategoryTheory.isIso_of_reflects_iso, CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
W : MorphismProperty.{v_1, u_1} C₁
F : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
G : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
inst_3 : G.ReflectsIsomorphisms
hF : W.IsInvertedBy F
⊢ W.IsInvertedBy (F ⋙ G)

Tactic:
IsInvertedBy.of_comp W F hF G

Premises used: CategoryTheory.MorphismProperty.IsInvertedBy.of_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
W : MorphismProperty.{v_1, u_1} C₁
F : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
G : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
inst_3 : G.ReflectsIsomorphisms
hF : W.IsInvertedBy F
⊢ W.IsInvertedBy (F ⋙ G)

Tactic:
exact IsInvertedBy.of_comp W F hF G

Premises used: CategoryTheory.MorphismProperty.IsInvertedBy.of_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
⊢ W.IsInvertedBy F ↔ W ≤ inverseImage (isomorphisms D) F

Tactic:
Iff.rfl

Premises used: CategoryTheory.MorphismProperty.inverseImage, Iff.rfl, CategoryTheory.MorphismProperty.IsInvertedBy
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
F : Functor.{v, v', u, u'} C D
rw : W ≤ inverseImage (isomorphisms D) F ↔ W.map F ≤ isomorphisms D
rw₁ rw₂ : W ≤ inverseImage (isomorphisms D) F ↔ W ≤ inverseImage (isomorphisms D) F
⊢ W.IsInvertedBy F ↔ W.map F ≤ isomorphisms D

Tactic:
rw [iff_le_inverseImage_isomorphisms, map_le_iff]

Premises used: CategoryTheory.MorphismProperty.map_le_iff, CategoryTheory.MorphismProperty.IsInvertedBy.iff_le_inverseImage_isomorphisms
-- Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
W : MorphismProperty.{v_1, u_1} C₁
F : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
G : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
⊢ (W.map F).IsInvertedBy G ↔ W.IsInvertedBy (F ⋙ G)

Tactic:
simp only [IsInvertedBy.iff_map_le_isomorphisms, map_map]

Premises used: CategoryTheory.MorphismProperty.IsInvertedBy.iff_map_le_isomorphisms, CategoryTheory.MorphismProperty.map_map
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
A B : C
i : A ⟶ B
inst_1 : IsIso i
⊢ T.llp i

Tactic:
fun _ _ _ _ ↦ inferInstance

Premises used: CategoryTheory.MorphismProperty.llp, inferInstance
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
⊢ T.rlp f

Tactic:
fun _ _ _ _ ↦ inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.rlp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
X x x_1 : C
p : x ⟶ x_1
hp : T p
⊢ HasLiftingProperty (𝟙 X) p

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
X Y Z : C
i : X ⟶ Y
j : Y ⟶ Z
hi : T.llp i
hj : T.llp j
x x_1 : C
p : x ⟶ x_1
hp : T p
⊢ HasLiftingProperty i p

Tactic:
have := hi _ hp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
X Y Z : C
i : X ⟶ Y
j : Y ⟶ Z
hi : T.llp i
hj : T.llp j
x x_1 : C
p : x ⟶ x_1
hp : T p
this : HasLiftingProperty i p
⊢ HasLiftingProperty j p

Tactic:
have := hj _ hp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
X Y Z : C
i : X ⟶ Y
j : Y ⟶ Z
hi : T.llp i
hj : T.llp j
x x_1 : C
p : x ⟶ x_1
hp : T p
this_1 : HasLiftingProperty i p
this : HasLiftingProperty j p
⊢ HasLiftingProperty (i ≫ j) p

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
X x x_1 : C
p : x ⟶ x_1
hp : T p
⊢ HasLiftingProperty p (𝟙 X)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
X Y Z : C
i : X ⟶ Y
j : Y ⟶ Z
hi : T.rlp i
hj : T.rlp j
x x_1 : C
p : x ⟶ x_1
hp : T p
⊢ HasLiftingProperty p i

Tactic:
have := hi _ hp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
X Y Z : C
i : X ⟶ Y
j : Y ⟶ Z
hi : T.rlp i
hj : T.rlp j
x x_1 : C
p : x ⟶ x_1
hp : T p
this : HasLiftingProperty p i
⊢ HasLiftingProperty p j

Tactic:
have := hj _ hp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
X Y Z : C
i : X ⟶ Y
j : Y ⟶ Z
hi : T.rlp i
hj : T.rlp j
x x_1 : C
p : x ⟶ x_1
hp : T p
this_1 : HasLiftingProperty p i
this : HasLiftingProperty p j
⊢ HasLiftingProperty p (i ≫ j)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
J : Type u_1
hW :
  ∀ (X₁ X₂ : J → C) [inst_1 : Limits.HasCoproduct.{u_1, v, u} X₁] [inst_2 : Limits.HasCoproduct.{u_1, v, u} X₂]
    (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), T.llp (f j)) →
      T.llp (X := Limits.sigmaObj.{u_1, v, u} X₁) (Y := Limits.sigmaObj.{u_1, v, u} X₂) (Limits.Sigma.map f)
⊢ T.llp.IsStableUnderCoproductsOfShape J

Tactic:
apply IsStableUnderCoproductsOfShape.mk

Premises used: CategoryTheory.MorphismProperty.IsStableUnderCoproductsOfShape.mk
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
J : Type u_1
A B : J → C
hW :
  ∀ [inst_1 : Limits.HasCoproduct.{u_1, v, u} A] [inst_2 : Limits.HasCoproduct.{u_1, v, u} B] (f : (j : J) → A j ⟶ B j),
    (∀ (j : J), T.llp (f j)) →
      T.llp (X := Limits.sigmaObj.{u_1, v, u} A) (Y := Limits.sigmaObj.{u_1, v, u} B) (Limits.Sigma.map f)
⊢ ∀ [inst_1 : Limits.HasCoproduct.{u_1, v, u} A] [inst_2 : Limits.HasCoproduct.{u_1, v, u} B] (f : (j : J) → A j ⟶ B j),
    (∀ (j : J), T.llp (f j)) →
      T.llp (X := Limits.sigmaObj.{u_1, v, u} A) (Y := Limits.sigmaObj.{u_1, v, u} B) (Limits.Sigma.map f)

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
J : Type u_1
A B : J → C
inst_1 : Limits.HasCoproduct.{u_1, v, u} A
hW :
  ∀ [inst_2 : Limits.HasCoproduct.{u_1, v, u} B] (f : (j : J) → A j ⟶ B j),
    (∀ (j : J), T.llp (f j)) →
      T.llp (X := Limits.sigmaObj.{u_1, v, u} A) (Y := Limits.sigmaObj.{u_1, v, u} B) (Limits.Sigma.map f)
⊢ ∀ [inst_2 : Limits.HasCoproduct.{u_1, v, u} B] (f : (j : J) → A j ⟶ B j),
    (∀ (j : J), T.llp (f j)) →
      T.llp (X := Limits.sigmaObj.{u_1, v, u} A) (Y := Limits.sigmaObj.{u_1, v, u} B) (Limits.Sigma.map f)

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
J : Type u_1
A B : J → C
inst_1 : Limits.HasCoproduct.{u_1, v, u} A
inst_2 : Limits.HasCoproduct.{u_1, v, u} B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.llp (f j)
X Y : C
p : X ⟶ Y
hp : T p
⊢ ∀ (j : J), HasLiftingProperty (f j) p

Tactic:
have := fun j ↦ hf j _ hp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
J : Type u_1
A B : J → C
inst_1 : Limits.HasCoproduct.{u_1, v, u} A
inst_2 : Limits.HasCoproduct.{u_1, v, u} B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.llp (f j)
X Y : C
p : X ⟶ Y
hp : T p
this : ∀ (j : J), HasLiftingProperty (f j) p
⊢ HasLiftingProperty (A := Limits.sigmaObj.{u_1, v, u} A) (B := Limits.sigmaObj.{u_1, v, u} B) (Limits.Sigma.map f) p

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
J : Type u_1
hW :
  ∀ (X₁ X₂ : J → C) [inst_1 : Limits.HasProduct.{u_1, v, u} X₁] [inst_2 : Limits.HasProduct.{u_1, v, u} X₂]
    (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), T.rlp (f j)) →
      T.rlp (X := Limits.piObj.{u_1, v, u} X₁) (Y := Limits.piObj.{u_1, v, u} X₂) (Limits.Pi.map f)
⊢ T.rlp.IsStableUnderProductsOfShape J

Tactic:
apply IsStableUnderProductsOfShape.mk

Premises used: CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape.mk
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
J : Type u_1
A B : J → C
hW :
  ∀ [inst_1 : Limits.HasProduct.{u_1, v, u} A] [inst_2 : Limits.HasProduct.{u_1, v, u} B] (f : (j : J) → A j ⟶ B j),
    (∀ (j : J), T.rlp (f j)) →
      T.rlp (X := Limits.piObj.{u_1, v, u} A) (Y := Limits.piObj.{u_1, v, u} B) (Limits.Pi.map f)
⊢ ∀ [inst_1 : Limits.HasProduct.{u_1, v, u} A] [inst_2 : Limits.HasProduct.{u_1, v, u} B] (f : (j : J) → A j ⟶ B j),
    (∀ (j : J), T.rlp (f j)) →
      T.rlp (X := Limits.piObj.{u_1, v, u} A) (Y := Limits.piObj.{u_1, v, u} B) (Limits.Pi.map f)

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
J : Type u_1
A B : J → C
inst_1 : Limits.HasProduct.{u_1, v, u} A
hW :
  ∀ [inst_2 : Limits.HasProduct.{u_1, v, u} B] (f : (j : J) → A j ⟶ B j),
    (∀ (j : J), T.rlp (f j)) →
      T.rlp (X := Limits.piObj.{u_1, v, u} A) (Y := Limits.piObj.{u_1, v, u} B) (Limits.Pi.map f)
⊢ ∀ [inst_2 : Limits.HasProduct.{u_1, v, u} B] (f : (j : J) → A j ⟶ B j),
    (∀ (j : J), T.rlp (f j)) →
      T.rlp (X := Limits.piObj.{u_1, v, u} A) (Y := Limits.piObj.{u_1, v, u} B) (Limits.Pi.map f)

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
J : Type u_1
A B : J → C
inst_1 : Limits.HasProduct.{u_1, v, u} A
inst_2 : Limits.HasProduct.{u_1, v, u} B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.rlp (f j)
X Y : C
p : X ⟶ Y
hp : T p
⊢ ∀ (j : J), HasLiftingProperty p (f j)

Tactic:
have := fun j ↦ hf j _ hp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
J : Type u_1
A B : J → C
inst_1 : Limits.HasProduct.{u_1, v, u} A
inst_2 : Limits.HasProduct.{u_1, v, u} B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.rlp (f j)
X Y : C
p : X ⟶ Y
hp : T p
this : ∀ (j : J), HasLiftingProperty p (f j)
⊢ HasLiftingProperty (X := Limits.piObj.{u_1, v, u} A) (Y := Limits.piObj.{u_1, v, u} B) p (Limits.Pi.map f)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T T' : MorphismProperty.{v, u} C
⊢ T ≤ T'.llp ↔ T' ≤ T.rlp

Tactic:
⟨fun h _ _ _ hp _ _ _ hi ↦ h _ hi _ hp,
    fun h _ _ _ hi _ _ _ hp ↦ h _ hp _ hi⟩

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
⊢ GaloisConnection (α := MorphismProperty.{v, u} C) (β := (MorphismProperty.{v, u} C)ᵒᵈ)
    ((⇑OrderDual.toDual : (a : MorphismProperty C) → (MorphismProperty C)ᵒᵈ) ∘ llp)
    (rlp ∘ (⇑OrderDual.ofDual : (a : (MorphismProperty C)ᵒᵈ) → MorphismProperty C))

Tactic:
fun _ _ ↦ le_llp_iff_le_rlp _ _

Premises used: CategoryTheory.MorphismProperty.llp, CategoryTheory.MorphismProperty.le_llp_iff_le_rlp, CategoryTheory.MorphismProperty.rlp, GaloisConnection
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
rw rw₁ : T.rlp ≤ T.rlp
⊢ T ≤ T.rlp.llp

Tactic:
rw [le_llp_iff_le_rlp]

Premises used: CategoryTheory.MorphismProperty.le_llp_iff_le_rlp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
⊢ T.rlp.llp.rlp = T.rlp

Tactic:
gc_llp_rlp.u_l_u_eq_u T

Premises used: CategoryTheory.MorphismProperty.llp, CategoryTheory.MorphismProperty.gc_llp_rlp, CategoryTheory.MorphismProperty.rlp, GaloisConnection.u_l_u_eq_u
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
⊢ T.llp.rlp.llp = T.llp

Tactic:
gc_llp_rlp.l_u_l_eq_l T

Premises used: CategoryTheory.MorphismProperty.llp, GaloisConnection.l_u_l_eq_l, CategoryTheory.MorphismProperty.gc_llp_rlp, CategoryTheory.MorphismProperty.rlp, OrderDual
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Antitone (α := MorphismProperty.{v, u} C) rlp

Tactic:
fun _ _ h ↦ gc_llp_rlp.monotone_u h

Premises used: GaloisConnection.monotone_u, CategoryTheory.MorphismProperty.gc_llp_rlp, CategoryTheory.MorphismProperty.rlp, Antitone
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Antitone (α := MorphismProperty.{v, u} C) llp

Tactic:
fun _ _ h ↦ gc_llp_rlp.monotone_l h

Premises used: CategoryTheory.MorphismProperty.llp, CategoryTheory.MorphismProperty.gc_llp_rlp, Antitone, GaloisConnection.monotone_l
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
A B : C
i : A ⟶ B
hi : T.pushouts i
⊢ T.rlp.llp i

Tactic:
(T.rlp.llp.isStableUnderCobaseChange_iff_pushouts_le).1 inferInstance i
    (pushouts_monotone T.le_llp_rlp _ hi)

Premises used: CategoryTheory.MorphismProperty.isStableUnderCobaseChange_iff_pushouts_le, inferInstance, CategoryTheory.MorphismProperty.le_llp_rlp, Iff.mp, CategoryTheory.MorphismProperty.pushouts_monotone
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
A B : C
i : A ⟶ B
hi : T.pushouts i
⊢ T.rlp.llp i

Tactic:
exact (T.rlp.llp.isStableUnderCobaseChange_iff_pushouts_le).1 inferInstance i
    (pushouts_monotone T.le_llp_rlp _ hi)

Premises used: CategoryTheory.MorphismProperty.isStableUnderCobaseChange_iff_pushouts_le, inferInstance, CategoryTheory.MorphismProperty.le_llp_rlp, Iff.mp, CategoryTheory.MorphismProperty.pushouts_monotone
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
a : T.pushouts.rlp ≤ T.rlp
a₁ : T.rlp ≤ T.pushouts.rlp
⊢ T.pushouts.rlp = T.rlp

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
⊢ T.pushouts.rlp ≤ T.rlp

Tactic:
antitone_rlp T.le_pushouts

Premises used: CategoryTheory.MorphismProperty.le_pushouts, CategoryTheory.MorphismProperty.antitone_rlp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
⊢ T.pushouts.rlp ≤ T.rlp

Tactic:
exact antitone_rlp T.le_pushouts

Premises used: CategoryTheory.MorphismProperty.le_pushouts, CategoryTheory.MorphismProperty.antitone_rlp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
a : T.pushouts ≤ T.rlp.llp
⊢ T.rlp ≤ T.pushouts.rlp

Tactic:
rw [← le_llp_iff_le_rlp]

Premises used: CategoryTheory.MorphismProperty.le_llp_iff_le_rlp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
⊢ T.pushouts ≤ T.rlp.llp

Tactic:
T.pushouts_le_llp_rlp

Premises used: CategoryTheory.MorphismProperty.pushouts_le_llp_rlp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
⊢ T.pushouts ≤ T.rlp.llp

Tactic:
exact T.pushouts_le_llp_rlp

Premises used: CategoryTheory.MorphismProperty.pushouts_le_llp_rlp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
J : Type w
A B : C
i : A ⟶ B
hi : colimitsOfShape.{v, u, w, w} T (Discrete J) i
⊢ T.rlp.llp i

Tactic:
MorphismProperty.colimitsOfShape_le _ (colimitsOfShape_monotone T.le_llp_rlp _ _ hi)

Premises used: CategoryTheory.MorphismProperty.colimitsOfShape_le, CategoryTheory.MorphismProperty.colimitsOfShape_monotone, CategoryTheory.MorphismProperty.le_llp_rlp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
J : Type w
A B : C
i : A ⟶ B
hi : colimitsOfShape.{v, u, w, w} T (Discrete J) i
⊢ T.rlp.llp i

Tactic:
exact MorphismProperty.colimitsOfShape_le _ (colimitsOfShape_monotone T.le_llp_rlp _ _ hi)

Premises used: CategoryTheory.MorphismProperty.colimitsOfShape_le, CategoryTheory.MorphismProperty.colimitsOfShape_monotone, CategoryTheory.MorphismProperty.le_llp_rlp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
A B : C
i : A ⟶ B
hi : coproducts.{w, v, u} T i
⊢ ∃ (J : Type w), colimitsOfShape.{v, u, w, w} T (Discrete J) i

Tactic:
rw [coproducts_iff] at hi

Premises used: CategoryTheory.MorphismProperty.coproducts_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
A B : C
i : A ⟶ B
hi : ∃ (J : Type w), colimitsOfShape.{v, u, w, w} T (Discrete J) i
obtain : ∀ (J : Type w) (hi : colimitsOfShape.{v, u, w, w} T (Discrete J) i), T.rlp.llp i
⊢ T.rlp.llp i

Tactic:
obtain ⟨J, hi⟩ := hi
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
A B : C
i : A ⟶ B
J : Type w
hi : colimitsOfShape.{v, u, w, w} T (Discrete J) i
⊢ T.rlp.llp i

Tactic:
T.colimitsOfShape_discrete_le_llp_rlp J _ hi

Premises used: CategoryTheory.MorphismProperty.colimitsOfShape_discrete_le_llp_rlp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
A B : C
i : A ⟶ B
J : Type w
hi : colimitsOfShape.{v, u, w, w} T (Discrete J) i
⊢ T.rlp.llp i

Tactic:
exact T.colimitsOfShape_discrete_le_llp_rlp J _ hi

Premises used: CategoryTheory.MorphismProperty.colimitsOfShape_discrete_le_llp_rlp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
a : (coproducts.{w, v, u} T).rlp ≤ T.rlp
a₁ : T.rlp ≤ (coproducts.{w, v, u} T).rlp
⊢ (coproducts.{w, v, u} T).rlp = T.rlp

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
⊢ (coproducts.{w, v, u} T).rlp ≤ T.rlp

Tactic:
antitone_rlp T.le_coproducts

Premises used: CategoryTheory.MorphismProperty.le_coproducts, CategoryTheory.MorphismProperty.antitone_rlp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
⊢ (coproducts.{w, v, u} T).rlp ≤ T.rlp

Tactic:
exact antitone_rlp T.le_coproducts

Premises used: CategoryTheory.MorphismProperty.le_coproducts, CategoryTheory.MorphismProperty.antitone_rlp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
a : coproducts.{w, v, u} T ≤ T.rlp.llp
⊢ T.rlp ≤ (coproducts.{w, v, u} T).rlp

Tactic:
rw [← le_llp_iff_le_rlp]

Premises used: CategoryTheory.MorphismProperty.le_llp_iff_le_rlp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
⊢ coproducts.{w, v, u} T ≤ T.rlp.llp

Tactic:
T.coproducts_le_llp_rlp

Premises used: CategoryTheory.MorphismProperty.coproducts_le_llp_rlp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
⊢ coproducts.{w, v, u} T ≤ T.rlp.llp

Tactic:
exact T.coproducts_le_llp_rlp

Premises used: CategoryTheory.MorphismProperty.coproducts_le_llp_rlp
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
⊢ T.retracts ≤ T.rlp.llp

Tactic:
le_trans (retracts_monotone T.le_llp_rlp) T.rlp.llp.retracts_le

Premises used: CategoryTheory.MorphismProperty.llp, CategoryTheory.MorphismProperty.retracts_le, CategoryTheory.MorphismProperty.le_llp_rlp, CategoryTheory.MorphismProperty.rlp, CategoryTheory.MorphismProperty.retracts_monotone, le_trans
-- Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
Goal:
C : Type u
inst : Category.{v, u} C
T : MorphismProperty.{v, u} C
a : T.retracts.rlp ≤ T.rlp
a₁ : T.rlp ≤ T.retracts.rlp
⊢ T.retracts.rlp = T.rlp

Tactic:
apply le_antisymm

Premises used: le_antisymm