awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty.{v, u} C
refine_2 : ∀ (i : α), (P i).isoClosure ≤ isoClosure (⨆ (a : α), P a)
⊢ LE.le.{u} (α := ObjectProperty.{v, u} C) (⨆ (a : α), (P a).isoClosure) (isoClosure (⨆ (a : α), P a))

Tactic:
simp only [iSup_le_iff]

Premises used: iSup_le_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty.{v, u} C
a : α
refine_2 : P a ≤ isoClosure (⨆ (a : α), P a)
⊢ (P a).isoClosure ≤ isoClosure (⨆ (a : α), P a)

Tactic:
rw [isoClosure_le_iff]

Premises used: CategoryTheory.ObjectProperty.isoClosure_le_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty.{v, u} C
a : α
⊢ P a ≤ isoClosure (⨆ (a : α), P a)

Tactic:
(le_iSup P a).trans (le_isoClosure _)

Premises used: CategoryTheory.ObjectProperty.le_isoClosure, le_iSup, LE.le.trans
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty.{v, u} C
a : α
⊢ P a ≤ isoClosure (⨆ (a : α), P a)

Tactic:
exact (le_iSup P a).trans (le_isoClosure _)

Premises used: CategoryTheory.ObjectProperty.le_isoClosure, le_iSup, LE.le.trans
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty.{v, u} C
X : C
inst_1 : ∀ (a : α), (P a).IsClosedUnderIsomorphisms
⊢ IsClosedUnderIsomorphisms.{v, u} (C := C) (⨆ (a : α), P a)

Tactic:
simp only [isClosedUnderIsomorphisms_iff_isoClosure_eq_self,
    isoClosure_iSup, isoClosure_eq_self]

Premises used: CategoryTheory.ObjectProperty.isClosedUnderIsomorphisms_iff_isoClosure_eq_self, CategoryTheory.ObjectProperty.isoClosure_iSup, CategoryTheory.ObjectProperty.isoClosure_eq_self
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
⊢ ¬P = ⊥ ↔ ∃ (X : C), P X

Tactic:
simp [← le_bot_iff, not_le_iff_exists]

Premises used: le_bot_iff, CategoryTheory.ObjectProperty.not_le_iff_exists
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
rw : P.Nonempty ↔ ∃ (X : C), P X
rw₁ rw₂ : (∃ (X : C), P X) ↔ ∃ (X : C), P X
⊢ P.Nonempty ↔ ¬P = ⊥

Tactic:
rw [ne_bot_iff_exists, nonempty_iff]

Premises used: CategoryTheory.ObjectProperty.nonempty_iff, CategoryTheory.ObjectProperty.ne_bot_iff_exists
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
rw : ¬¬P = ⊥ ↔ P = ⊥
rw₁ rw₂ : P = ⊥ ↔ P = ⊥
⊢ ¬P.Nonempty ↔ P = ⊥

Tactic:
rw [P.nonempty_iff_ne_bot, not_not]

Premises used: CategoryTheory.ObjectProperty.nonempty_iff_ne_bot, Classical.not_not
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h : ∀ (X : C), map ⊤ P.ι X ↔ P.isoClosure X
⊢ map ⊤ P.ι = P.isoClosure

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X : C
h : map ⊤ P.ι X → P.isoClosure X
h₁ : P.isoClosure X → map ⊤ P.ι X
⊢ map ⊤ P.ι X ↔ P.isoClosure X

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X Y : C
hY : P Y
left : ⊤ (FullSubcategory.mk (P := P) Y hY)
e : P.ι.obj (FullSubcategory.mk (P := P) Y hY) ≅ X
⊢ P.isoClosure X

Tactic:
⟨Y, hY, ⟨e.symm⟩⟩

Premises used: Nonempty.intro, CategoryTheory.ObjectProperty.isoClosure, Exists.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X Y : C
hY : P Y
left : ⊤ (FullSubcategory.mk (P := P) Y hY)
e : P.ι.obj (FullSubcategory.mk (P := P) Y hY) ≅ X
⊢ P.isoClosure X

Tactic:
exact ⟨Y, hY, ⟨e.symm⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X Y : C
hY : P Y
e : X ≅ Y
⊢ ⊤ (FullSubcategory.mk (P := P) Y hY)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X Y : C
hY : P Y
e : X ≅ Y
⊢ map ⊤ P.ι X

Tactic:
exact ⟨⟨Y, hY⟩, by simp, ⟨e.symm⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.ContainsZero
⊢ ∃ (Z : C), IsZero.{v, u} Z ∧ P Z

Tactic:
ContainsZero.exists_zero

Premises used: CategoryTheory.ObjectProperty.ContainsZero.exists_zero
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
⊢ P.Nonempty

Tactic:
nonempty_of_prop P.exists_prop_of_containsZero.choose_spec.2

Premises used: Exists.choose_spec, CategoryTheory.ObjectProperty.nonempty_of_prop, And.right, CategoryTheory.ObjectProperty.exists_prop_of_containsZero
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.ContainsZero
inst_2 : P.IsClosedUnderIsomorphisms
Z : C
hZ : IsZero.{v, u} Z
obtain : ∀ (Z₀ : C) (hZ₀ : IsZero.{v, u} Z₀) (h₀ : P Z₀), P Z
⊢ P Z

Tactic:
obtain ⟨Z₀, hZ₀, h₀⟩ := P.exists_prop_of_containsZero

Premises used: CategoryTheory.ObjectProperty.exists_prop_of_containsZero
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.ContainsZero
inst_2 : P.IsClosedUnderIsomorphisms
Z : C
hZ : IsZero.{v, u} Z
Z₀ : C
hZ₀ : IsZero.{v, u} Z₀
h₀ : P Z₀
⊢ P Z

Tactic:
P.prop_of_iso (hZ₀.iso hZ) h₀

Premises used: CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.Limits.IsZero.iso
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.ContainsZero
inst_2 : P.IsClosedUnderIsomorphisms
Z : C
hZ : IsZero.{v, u} Z
Z₀ : C
hZ₀ : IsZero.{v, u} Z₀
h₀ : P Z₀
⊢ P Z

Tactic:
exact P.prop_of_iso (hZ₀.iso hZ) h₀

Premises used: CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.Limits.IsZero.iso
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.ContainsZero
inst_2 : P.IsClosedUnderIsomorphisms
inst_3 : HasZeroObject.{v, u} C
⊢ P 0

Tactic:
P.prop_of_isZero (isZero_zero C)

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.ObjectProperty.prop_of_isZero
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : HasZeroObject.{v, u} C
⊢ ⊤ 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasZeroMorphisms.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_5 : F.PreservesZeroMorphisms
obtain : ∀ (Z : C) (h₁ : IsZero.{v, u} Z) (h₂ : P Z), ∃ (Z : D), IsZero.{v', u'} Z ∧ P.map F Z
⊢ ∃ (Z : D), IsZero.{v', u'} Z ∧ P.map F Z

Tactic:
obtain ⟨Z, h₁, h₂⟩ := P.exists_prop_of_containsZero

Premises used: CategoryTheory.ObjectProperty.exists_prop_of_containsZero
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasZeroMorphisms.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_5 : F.PreservesZeroMorphisms
Z : C
h₁ : IsZero.{v, u} Z
h₂ : P Z
⊢ ∃ (Z : D), IsZero.{v', u'} Z ∧ P.map F Z

Tactic:
⟨F.obj Z, F.map_isZero h₁, P.prop_map_obj F h₂⟩

Premises used: CategoryTheory.ObjectProperty.prop_map_obj, CategoryTheory.Functor.map_isZero, And.intro, Exists.intro, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasZeroMorphisms.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_5 : F.PreservesZeroMorphisms
Z : C
h₁ : IsZero.{v, u} Z
h₂ : P Z
⊢ ∃ (Z : D), IsZero.{v', u'} Z ∧ P.map F Z

Tactic:
exact ⟨F.obj Z, F.map_isZero h₁, P.prop_map_obj F h₂⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
obtain : ∀ (Z : C) (hZ : IsZero.{v, u} Z) (hP : P Z), ∃ (Z : C), IsZero.{v, u} Z ∧ P.isoClosure Z
⊢ ∃ (Z : C), IsZero.{v, u} Z ∧ P.isoClosure Z

Tactic:
obtain ⟨Z, hZ, hP⟩ := P.exists_prop_of_containsZero

Premises used: CategoryTheory.ObjectProperty.exists_prop_of_containsZero
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
Z : C
hZ : IsZero.{v, u} Z
hP : P Z
⊢ ∃ (Z : C), IsZero.{v, u} Z ∧ P.isoClosure Z

Tactic:
⟨Z, hZ, P.le_isoClosure _ hP⟩

Premises used: CategoryTheory.ObjectProperty.le_isoClosure, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
Z : C
hZ : IsZero.{v, u} Z
hP : P Z
⊢ ∃ (Z : C), IsZero.{v, u} Z ∧ P.isoClosure Z

Tactic:
exact ⟨Z, hZ, P.le_isoClosure _ hP⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
inst_3 : P.IsClosedUnderIsomorphisms
inst_4 : Q.ContainsZero
obtain : ∀ (Z : C) (hZ : IsZero.{v, u} Z) (hQ : Q Z), ∃ (Z : C), IsZero.{v, u} Z ∧ (P ⊓ Q) Z
⊢ ∃ (Z : C), IsZero.{v, u} Z ∧ (P ⊓ Q) Z

Tactic:
obtain ⟨Z, hZ, hQ⟩ := Q.exists_prop_of_containsZero

Premises used: CategoryTheory.ObjectProperty.exists_prop_of_containsZero
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
inst_3 : P.IsClosedUnderIsomorphisms
inst_4 : Q.ContainsZero
Z : C
hZ : IsZero.{v, u} Z
hQ : Q Z
⊢ ∃ (Z : C), IsZero.{v, u} Z ∧ (P ⊓ Q) Z

Tactic:
⟨Z, hZ, P.prop_of_isZero hZ, hQ⟩

Premises used: And.intro, Exists.intro, CategoryTheory.ObjectProperty.prop_of_isZero
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
inst_3 : P.IsClosedUnderIsomorphisms
inst_4 : Q.ContainsZero
Z : C
hZ : IsZero.{v, u} Z
hQ : Q Z
⊢ ∃ (Z : C), IsZero.{v, u} Z ∧ (P ⊓ Q) Z

Tactic:
exact ⟨Z, hZ, P.prop_of_isZero hZ, hQ⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
obtain : ∀ (Z : C) (hZ : IsZero.{v, u} Z) (mem : P Z), ∃ (Z : Cᵒᵖ), IsZero.{v, u} Z ∧ P.op Z
⊢ ∃ (Z : Cᵒᵖ), IsZero.{v, u} Z ∧ P.op Z

Tactic:
obtain ⟨Z, hZ, mem⟩ := P.exists_prop_of_containsZero

Premises used: CategoryTheory.ObjectProperty.exists_prop_of_containsZero
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
Z : C
hZ : IsZero.{v, u} Z
mem : P Z
⊢ ∃ (Z : Cᵒᵖ), IsZero.{v, u} Z ∧ P.op Z

Tactic:
⟨op Z, hZ.op, mem⟩

Premises used: CategoryTheory.Limits.IsZero.op, Opposite.op, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
Z : C
hZ : IsZero.{v, u} Z
mem : P Z
⊢ ∃ (Z : Cᵒᵖ), IsZero.{v, u} Z ∧ P.op Z

Tactic:
exact ⟨op Z, hZ.op, mem⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P_1 Q : ObjectProperty.{v, u} C
P : ObjectProperty.{v, u} Cᵒᵖ
inst_2 : ContainsZero.{v, u} P
obtain : ∀ (Z : Cᵒᵖ) (hZ : IsZero.{v, u} Z) (mem : P Z), ∃ (Z : C), IsZero.{v, u} Z ∧ P.unop Z
⊢ ∃ (Z : C), IsZero.{v, u} Z ∧ P.unop Z

Tactic:
obtain ⟨Z, hZ, mem⟩ := P.exists_prop_of_containsZero

Premises used: CategoryTheory.ObjectProperty.exists_prop_of_containsZero
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P_1 Q : ObjectProperty.{v, u} C
P : ObjectProperty.{v, u} Cᵒᵖ
inst_2 : ContainsZero.{v, u} P
Z : Cᵒᵖ
hZ : IsZero.{v, u} Z
mem : P Z
⊢ ∃ (Z : C), IsZero.{v, u} Z ∧ P.unop Z

Tactic:
⟨Z.unop, hZ.unop, mem⟩

Premises used: And.intro, Exists.intro, Opposite.unop, CategoryTheory.Limits.IsZero.unop
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P_1 Q : ObjectProperty.{v, u} C
P : ObjectProperty.{v, u} Cᵒᵖ
inst_2 : ContainsZero.{v, u} P
Z : Cᵒᵖ
hZ : IsZero.{v, u} Z
mem : P Z
⊢ ∃ (Z : C), IsZero.{v, u} Z ∧ P.unop Z

Tactic:
exact ⟨Z.unop, hZ.unop, mem⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
obtain : ∀ (X : C) (h₁ : IsZero.{v, u} X) (h₂ : P X), ∃ (X : P.FullSubcategory), IsZero.{v, u} X
⊢ ∃ (X : P.FullSubcategory), IsZero.{v, u} X

Tactic:
obtain ⟨X, h₁, h₂⟩ := P.exists_prop_of_containsZero

Premises used: CategoryTheory.ObjectProperty.exists_prop_of_containsZero
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
X : C
h₁ : IsZero.{v, u} X
h₂ : P X
⊢ ∃ (X : P.FullSubcategory), IsZero.{v, u} X

Tactic:
⟨_, IsZero.of_full_of_faithful_of_isZero P.ι ⟨X, h₂⟩ h₁⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.ObjectProperty.ι, CategoryTheory.Limits.IsZero.of_full_of_faithful_of_isZero, Exists.intro
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
X : C
h₁ : IsZero.{v, u} X
h₂ : P X
⊢ ∃ (X : P.FullSubcategory), IsZero.{v, u} X

Tactic:
exact ⟨_, IsZero.of_full_of_faithful_of_isZero P.ι ⟨X, h₂⟩ h₁⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
inst_3 : Q.ContainsZero
inst_4 : Q.IsClosedUnderIsomorphisms
obtain : ∀ (Z : C) (hZ : IsZero.{v, u} Z) (hP : P Z), ∃ (Z : C), IsZero.{v, u} Z ∧ (P ⊓ Q) Z
⊢ ∃ (Z : C), IsZero.{v, u} Z ∧ (P ⊓ Q) Z

Tactic:
obtain ⟨Z, hZ, hP⟩ := P.exists_prop_of_containsZero

Premises used: CategoryTheory.ObjectProperty.exists_prop_of_containsZero
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
inst_3 : Q.ContainsZero
inst_4 : Q.IsClosedUnderIsomorphisms
Z : C
hZ : IsZero.{v, u} Z
hP : P Z
⊢ ∃ (Z : C), IsZero.{v, u} Z ∧ (P ⊓ Q) Z

Tactic:
⟨Z, hZ, hP, Q.prop_of_isZero hZ⟩

Premises used: And.intro, Exists.intro, CategoryTheory.ObjectProperty.prop_of_isZero
-- Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v, u} C
inst_2 : P.ContainsZero
inst_3 : Q.ContainsZero
inst_4 : Q.IsClosedUnderIsomorphisms
Z : C
hZ : IsZero.{v, u} Z
hP : P Z
⊢ ∃ (Z : C), IsZero.{v, u} Z ∧ (P ⊓ Q) Z

Tactic:
exact ⟨Z, hZ, hP, Q.prop_of_isZero hZ⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderSubobjects
X Y : C
f : X ⟶ Y
inst_2 : Mono f
hY : P Y
⊢ P X

Tactic:
IsClosedUnderSubobjects.prop_of_mono f hY

Premises used: CategoryTheory.ObjectProperty.IsClosedUnderSubobjects.prop_of_mono
-- Module: Mathlib.CategoryTheory.ObjectProperty.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderSubobjects
inst_2 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
h₂ : P S.X₂
have : ∀ (this : Mono S.f), P S.X₁
⊢ P S.X₁

Tactic:
have := hS.mono_f
-- Module: Mathlib.CategoryTheory.ObjectProperty.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderSubobjects
inst_2 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
h₂ : P S.X₂
this : Mono S.f
⊢ P S.X₁

Tactic:
P.prop_of_mono S.f h₂

Premises used: CategoryTheory.ShortComplex.f, CategoryTheory.ObjectProperty.prop_of_mono
-- Module: Mathlib.CategoryTheory.ObjectProperty.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderSubobjects
inst_2 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
h₂ : P S.X₂
this : Mono S.f
⊢ P S.X₁

Tactic:
exact P.prop_of_mono S.f h₂

Premises used: CategoryTheory.ShortComplex.f, CategoryTheory.ObjectProperty.prop_of_mono
-- Module: Mathlib.CategoryTheory.ObjectProperty.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderQuotients
X Y : C
f : X ⟶ Y
inst_2 : Epi f
hX : P X
⊢ P Y

Tactic:
IsClosedUnderQuotients.prop_of_epi f hX

Premises used: CategoryTheory.ObjectProperty.IsClosedUnderQuotients.prop_of_epi
-- Module: Mathlib.CategoryTheory.ObjectProperty.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderQuotients
inst_2 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
h₂ : P S.X₂
have : ∀ (this : Epi S.g), P S.X₃
⊢ P S.X₃

Tactic:
have := hS.epi_g
-- Module: Mathlib.CategoryTheory.ObjectProperty.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderQuotients
inst_2 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
h₂ : P S.X₂
this : Epi S.g
⊢ P S.X₃

Tactic:
P.prop_of_epi S.g h₂

Premises used: CategoryTheory.ObjectProperty.prop_of_epi, CategoryTheory.ShortComplex.g
-- Module: Mathlib.CategoryTheory.ObjectProperty.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderQuotients
inst_2 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
h₂ : P S.X₂
this : Epi S.g
⊢ P S.X₃

Tactic:
exact P.prop_of_epi S.g h₂

Premises used: CategoryTheory.ObjectProperty.prop_of_epi, CategoryTheory.ShortComplex.g
-- Module: Mathlib.CategoryTheory.ObjectProperty.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
⊢ ∀ {X Y : C} (f : X ⟶ Y) [Mono f] (hY : ⊤ Y), ⊤ X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
⊢ ∀ {X Y : C} (f : X ⟶ Y) [Epi f] (hX : ⊤ X), ⊤ Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P ≤ Q
⊢ (ιOfLE (P := P) (P' := Q) h).EssSurj ↔ Q ≤ P.isoClosure

Tactic:
⟨fun _ X hX ↦ ?_, fun hPQ ↦ ⟨fun ⟨Y, hY⟩ ↦ ?_⟩⟩

Premises used: CategoryTheory.ObjectProperty.ιOfLE, CategoryTheory.Functor.EssSurj.mk, CategoryTheory.Functor.essImage, Iff.intro, _private.0.CategoryTheory.ObjectProperty.essSurj_ιOfLE_iff.match_1
-- Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P ≤ Q
refine_1 : (ιOfLE (P := P) (P' := Q) h).EssSurj → ∀ (X : C) (hX : Q X), P.isoClosure X
refine_2 :
  ∀ (hPQ : Q ≤ P.isoClosure) (x : Q.FullSubcategory) (Y : C) (hY : Q Y),
    (ιOfLE (P := P) (P' := Q) h).essImage (FullSubcategory.mk (P := Q) Y hY)
⊢ (ιOfLE (P := P) (P' := Q) h).EssSurj ↔ Q ≤ P.isoClosure

Tactic:
refine ⟨fun _ X hX ↦ ?_, fun hPQ ↦ ⟨fun ⟨Y, hY⟩ ↦ ?_⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P ≤ Q
h_1 : (ιOfLE (P := P) (P' := Q) h).EssSurj
X : C
hX : Q X
⊢ P.isoClosure X

Tactic:
⟨_, ((ιOfLE h).objPreimage ⟨X, hX⟩).2,
      ⟨Q.ι.mapIso ((ιOfLE h).objObjPreimageIso ⟨X, hX⟩).symm⟩⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.ObjectProperty.ι, CategoryTheory.ObjectProperty.ιOfLE, CategoryTheory.ObjectProperty.FullSubcategory.property, Nonempty.intro, CategoryTheory.Functor.objPreimage, CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.ObjectProperty.isoClosure, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P ≤ Q
h_1 : (ιOfLE (P := P) (P' := Q) h).EssSurj
X : C
hX : Q X
⊢ P.isoClosure X

Tactic:
exact ⟨_, ((ιOfLE h).objPreimage ⟨X, hX⟩).2,
      ⟨Q.ι.mapIso ((ιOfLE h).objObjPreimageIso ⟨X, hX⟩).symm⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P ≤ Q
hPQ : Q ≤ P.isoClosure
x : Q.FullSubcategory
Y : C
hY : Q Y
refine_2 : ∀ (X : C) (hX : P X) (e : Y ≅ X), (ιOfLE (P := P) (P' := Q) h).essImage (FullSubcategory.mk (P := Q) Y hY)
⊢ (ιOfLE (P := P) (P' := Q) h).essImage (FullSubcategory.mk (P := Q) Y hY)

Tactic:
obtain ⟨X, hX, ⟨e⟩⟩ := hPQ _ hY
-- Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P ≤ Q
hPQ : Q ≤ P.isoClosure
x : Q.FullSubcategory
Y : C
hY : Q Y
X : C
hX : P X
e : Y ≅ X
⊢ (ιOfLE (P := P) (P' := Q) h).essImage (FullSubcategory.mk (P := Q) Y hY)

Tactic:
⟨⟨X, hX⟩, ⟨Q.ι.preimageIso e.symm⟩⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.ObjectProperty.ι, CategoryTheory.Functor.essImage, Nonempty.intro, CategoryTheory.Functor.preimageIso, Exists.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P ≤ Q
hPQ : Q ≤ P.isoClosure
x : Q.FullSubcategory
Y : C
hY : Q Y
X : C
hX : P X
e : Y ≅ X
⊢ (ιOfLE (P := P) (P' := Q) h).essImage (FullSubcategory.mk (P := Q) Y hY)

Tactic:
exact ⟨⟨X, hX⟩, ⟨Q.ι.preimageIso e.symm⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P ≤ Q
rw : (ιOfLE (P := P) (P' := Q) h).IsEquivalence ↔ (ιOfLE (P := P) (P' := Q) h).EssSurj
⊢ (ιOfLE (P := P) (P' := Q) h).IsEquivalence ↔ Q ≤ P.isoClosure

Tactic:
rw [← essSurj_ιOfLE_iff h]

Premises used: CategoryTheory.ObjectProperty.essSurj_ιOfLE_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P ≤ Q
⊢ (ιOfLE (P := P) (P' := Q) h).IsEquivalence ↔ (ιOfLE (P := P) (P' := Q) h).EssSurj

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ { }⟩

Premises used: inferInstance, CategoryTheory.Functor.IsEquivalence.mk, Iff.intro
-- Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence
Goal:
C : Type u
inst : Category.{v, u} C
P Q : ObjectProperty.{v, u} C
h : P ≤ Q
⊢ (ιOfLE (P := P) (P' := Q) h).IsEquivalence ↔ (ιOfLE (P := P) (P' := Q) h).EssSurj

Tactic:
exact ⟨fun _ ↦ inferInstance, fun _ ↦ { }⟩