awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : HasInitial.{v_1, u_1} C
inst_2 : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst_3 : P.IsClosedUnderBinaryCoproducts
X Y : C
e : X ≅ Y
hX : P X
⊢ ∀ {T : C} (f : initial.{v_1, u_1} C ⟶ T) (g : X ⟶ T),
    CategoryStruct.comp (Y :=
        Functor.obj.{0, v_1, 0, u_1}
          (Functor.obj (Functor.const (Discrete WalkingPair))
            (Cocone.pt (F := Limits.pair (initial.{v_1, u_1} C) X) (BinaryCofan.mk (initial.to Y) e.hom)))
          { as := WalkingPair.right : Discrete WalkingPair })
        (BinaryCofan.inr (BinaryCofan.mk (initial.to Y) e.hom))
        ((fun {T : C} (x : initial.{v_1, u_1} C ⟶ T) (f : X ⟶ T) ↦ e.inv ≫ f) f g) =
      g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : HasInitial.{v_1, u_1} C
inst_2 : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst_3 : P.IsClosedUnderBinaryCoproducts
X Y : C
e : X ≅ Y
hX : P X
let : P Y
⊢ P Y

Tactic:
let h : IsColimit (BinaryCofan.mk (initial.to Y) e.hom) :=
      BinaryCofan.IsColimit.mk _ (fun _ f ↦ e.inv ≫ f) (by cat_disch) (by simp) (by cat_disch)
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : HasInitial.{v_1, u_1} C
inst_2 : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst_3 : P.IsClosedUnderBinaryCoproducts
X Y : C
e : X ≅ Y
hX : P X
h : IsColimit (F := Limits.pair (initial.{v_1, u_1} C) X) (BinaryCofan.mk (initial.to Y) e.hom) :=
  BinaryCofan.IsColimit.mk (BinaryCofan.mk (initial.to Y) e.hom)
    (fun {T : C} (x : initial.{v_1, u_1} C ⟶ T) (f : X ⟶ T) ↦ e.inv ≫ f) ⋯ ⋯ ⋯
⊢ P Y

Tactic:
P.prop_of_isColimit_binaryCofan h P.prop_initial hX

Premises used: CategoryTheory.ObjectProperty.prop_initial, CategoryTheory.ObjectProperty.prop_of_isColimit_binaryCofan
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : HasInitial.{v_1, u_1} C
inst_2 : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst_3 : P.IsClosedUnderBinaryCoproducts
X Y : C
e : X ≅ Y
hX : P X
h : IsColimit (F := Limits.pair (initial.{v_1, u_1} C) X) (BinaryCofan.mk (initial.to Y) e.hom) :=
  BinaryCofan.IsColimit.mk (BinaryCofan.mk (initial.to Y) e.hom)
    (fun {T : C} (x : initial.{v_1, u_1} C ⟶ T) (f : X ⟶ T) ↦ e.inv ≫ f) ⋯ ⋯ ⋯
⊢ P Y

Tactic:
exact P.prop_of_isColimit_binaryCofan h P.prop_initial hX

Premises used: CategoryTheory.ObjectProperty.prop_initial, CategoryTheory.ObjectProperty.prop_of_isColimit_binaryCofan
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasInitial.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
inst_2 : Q.IsClosedUnderBinaryCoproducts
inst_3 : Q.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
⊢ P.binaryCoproductsClosure ≤ Q ↔ P ≤ Q

Tactic:
⟨fun h ↦ (P.le_colimitsClosure _).trans h, fun h ↦ ?_⟩

Premises used: CategoryTheory.Limits.WalkingPair, CategoryTheory.ObjectProperty.le_colimitsClosure, Iff.intro, LE.le.trans, CategoryTheory.Discrete
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasInitial.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
inst_2 : Q.IsClosedUnderBinaryCoproducts
inst_3 : Q.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
refine : ∀ (h : P ≤ Q), P.binaryCoproductsClosure ≤ Q
⊢ P.binaryCoproductsClosure ≤ Q ↔ P ≤ Q

Tactic:
refine ⟨fun h ↦ (P.le_colimitsClosure _).trans h, fun h ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasInitial.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
inst_2 : Q.IsClosedUnderBinaryCoproducts
inst_3 : Q.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
h : P ≤ Q
this : Q.IsClosedUnderIsomorphisms := ⋯
⊢ P.binaryCoproductsClosure ≤ Q

Tactic:
colimitsClosure_le h

Premises used: CategoryTheory.ObjectProperty.colimitsClosure_le
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasInitial.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
inst_2 : Q.IsClosedUnderBinaryCoproducts
inst_3 : Q.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
h : P ≤ Q
this : Q.IsClosedUnderIsomorphisms := ⋯
⊢ P.binaryCoproductsClosure ≤ Q

Tactic:
exact colimitsClosure_le h

Premises used: CategoryTheory.ObjectProperty.colimitsClosure_le
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
H : ∀ (J : Type w) [Finite J], IsClosedUnderColimitsOfShape.{w, w, v_1, u_1} P (Discrete J)
J : Type
h : Finite J
rw : IsClosedUnderColimitsOfShape.{w, w, v_1, u_1} P (Discrete (Shrink.{w, 0} J))
⊢ P.IsClosedUnderColimitsOfShape (Discrete J)

Tactic:
rw [P.isClosedUnderColimitsOfShape_iff_of_equivalence
      (Discrete.equivalence (equivShrink.{w} _))]
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
H : ∀ (J : Type w) [Finite J], IsClosedUnderColimitsOfShape.{w, w, v_1, u_1} P (Discrete J)
J : Type
h : Finite J
⊢ IsClosedUnderColimitsOfShape.{w, w, v_1, u_1} P (Discrete (Shrink.{w, 0} J))

Tactic:
H _
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
H : ∀ (J : Type w) [Finite J], IsClosedUnderColimitsOfShape.{w, w, v_1, u_1} P (Discrete J)
J : Type
h : Finite J
⊢ IsClosedUnderColimitsOfShape.{w, w, v_1, u_1} P (Discrete (Shrink.{w, 0} J))

Tactic:
exact H _
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderFiniteCoproducts
J : Type u_2
inst_2 : Finite J
obtain : ∀ (n : ℕ) (e : J ≃ Fin n), IsClosedUnderColimitsOfShape.{u_2, u_2, v_1, u_1} P (Discrete J)
⊢ IsClosedUnderColimitsOfShape.{u_2, u_2, v_1, u_1} P (Discrete J)

Tactic:
obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin J

Premises used: Finite.exists_equiv_fin
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderFiniteCoproducts
J : Type u_2
inst_2 : Finite J
n : ℕ
e : J ≃ Fin n
⊢ P.IsClosedUnderColimitsOfShape (Discrete (Fin n))

Tactic:
have : P.IsClosedUnderColimitsOfShape (Discrete (Fin n)) :=
    IsClosedUnderFiniteCoproducts.isClosedUnderColimitsOfShape _
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderFiniteCoproducts
J : Type u_2
inst_2 : Finite J
n : ℕ
e : J ≃ Fin n
this : P.IsClosedUnderColimitsOfShape (Discrete (Fin n))
⊢ IsClosedUnderColimitsOfShape.{u_2, u_2, v_1, u_1} P (Discrete J)

Tactic:
IsClosedUnderColimitsOfShape.of_equivalence (Discrete.equivalence e.symm)

Premises used: CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape.of_equivalence, CategoryTheory.Discrete.equivalence, Equiv.symm
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderFiniteCoproducts
J : Type u_2
inst_2 : Finite J
n : ℕ
e : J ≃ Fin n
this : P.IsClosedUnderColimitsOfShape (Discrete (Fin n))
⊢ IsClosedUnderColimitsOfShape.{u_2, u_2, v_1, u_1} P (Discrete J)

Tactic:
exact IsClosedUnderColimitsOfShape.of_equivalence (Discrete.equivalence e.symm)

Premises used: CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape.of_equivalence, CategoryTheory.Discrete.equivalence, Equiv.symm
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderFiniteCoproducts
J : Type u_2
inst_2 : Finite J
f : J → C
F : Cofan.{u_2, v_1, u_1} f
hF : IsColimit F
h : ∀ (j : J), P (f j)
j : J
⊢ P (Functor.obj.{u_2, v_1, u_2, u_1} (Discrete.functor f) { as := j : Discrete J })

Tactic:
h j
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderFiniteCoproducts
J : Type u_2
inst_2 : Finite J
f : J → C
F : Cofan.{u_2, v_1, u_1} f
hF : IsColimit F
h : ∀ (j : J), P (f j)
j : J
⊢ P (Functor.obj.{u_2, v_1, u_2, u_1} (Discrete.functor f) { as := j : Discrete J })

Tactic:
exact h j
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.IsClosedUnderFiniteCoproducts
J : Type u_2
inst_2 : Finite J
f : J → C
inst_3 : HasCoproduct.{u_2, v_1, u_1} f
h : ∀ (j : J), P (f j)
⊢ P (sigmaObj.{u_2, v_1, u_1} f)

Tactic:
P.prop_of_isColimit_cofan (colimit.isColimit (Discrete.functor f)) h

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Discrete.functor, CategoryTheory.Limits.colimit, CategoryTheory.ObjectProperty.prop_of_isColimit_cofan
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.ContainsZero
inst_2 : P.IsClosedUnderIsomorphisms
X : C
p : P.ColimitOfShape (Discrete PEmpty.{1}) X
obtain : ∀ (Z : C) (hZ : IsZero.{v_1, u_1} Z) (hZ₂ : P Z), P X
⊢ P X

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

Premises used: CategoryTheory.ObjectProperty.exists_prop_of_containsZero
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.ContainsZero
inst_2 : P.IsClosedUnderIsomorphisms
X : C
p : P.ColimitOfShape (Discrete PEmpty.{1}) X
Z : C
hZ : IsZero.{v_1, u_1} Z
hZ₂ : P Z
⊢ (Cocone.precompose p.toColimitPresentation (P := P).diag.uniqueFromEmpty.inv).obj
      { pt := X, ι := p.toColimitPresentation (P := P).ι : Cocone p.toColimitPresentation (P := P).diag } ≅
    asEmptyCocone X

Tactic:
exact Cocone.ext (Iso.refl _) (by rintro ⟨⟨⟩⟩)

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.ContainsZero
inst_2 : P.IsClosedUnderIsomorphisms
X : C
p : P.ColimitOfShape (Discrete PEmpty.{1}) X
Z : C
hZ : IsZero.{v_1, u_1} Z
hZ₂ : P Z
have : ∀ (hX : IsInitial.{v_1, u_1} X), P X
⊢ P X

Tactic:
have hX : IsInitial X :=
      (IsColimit.equivOfNatIsoOfIso p.diag.uniqueFromEmpty _ _
        (by exact Cocone.ext (Iso.refl _) (by rintro ⟨⟨⟩⟩))).1 p.isColimit
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.ContainsZero
inst_2 : P.IsClosedUnderIsomorphisms
X : C
p : P.ColimitOfShape (Discrete PEmpty.{1}) X
Z : C
hZ : IsZero.{v_1, u_1} Z
hZ₂ : P Z
hX : IsInitial.{v_1, u_1} X
⊢ P X

Tactic:
P.prop_of_isZero (IsZero.of_iso hZ
      (IsColimit.coconePointUniqueUpToIso hX (IsZero.isInitial hZ)))

Premises used: CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.ObjectProperty.prop_of_isZero, CategoryTheory.Limits.IsZero.isInitial, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : P.ContainsZero
inst_2 : P.IsClosedUnderIsomorphisms
X : C
p : P.ColimitOfShape (Discrete PEmpty.{1}) X
Z : C
hZ : IsZero.{v_1, u_1} Z
hZ₂ : P Z
hX : IsInitial.{v_1, u_1} X
⊢ P X

Tactic:
exact P.prop_of_isZero (IsZero.of_iso hZ
      (IsColimit.coconePointUniqueUpToIso hX (IsZero.isInitial hZ)))

Premises used: CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.ObjectProperty.prop_of_isZero, CategoryTheory.Limits.IsZero.isInitial, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : HasFiniteCoproducts.{v_1, u_1} C
inst_2 : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst_3 : P.IsClosedUnderBinaryCoproducts
⊢ P.IsClosedUnderIsomorphisms

Tactic:
have := IsClosedUnderBinaryCoproducts.closedUnderIsomorphisms P
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : HasFiniteCoproducts.{v_1, u_1} C
inst_2 : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst_3 : P.IsClosedUnderBinaryCoproducts
this : P.IsClosedUnderIsomorphisms
⊢ HasFiniteCoproducts.{v_1, u_1} P.FullSubcategory

Tactic:
have := hasFiniteCoproducts_of_has_binary_and_initial (C := P.FullSubcategory)
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : HasFiniteCoproducts.{v_1, u_1} C
inst_2 : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst_3 : P.IsClosedUnderBinaryCoproducts
this_1 : P.IsClosedUnderIsomorphisms
this : HasFiniteCoproducts.{v_1, u_1} P.FullSubcategory
⊢ ∀ (J : Type) [Finite J], PreservesColimitsOfShape (Discrete J) P.ι

Tactic:
have := PreservesFiniteCoproducts.of_preserves_binary_and_initial P.ι
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : HasFiniteCoproducts.{v_1, u_1} C
inst_2 : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst_3 : P.IsClosedUnderBinaryCoproducts
this_1 : P.IsClosedUnderIsomorphisms
this_2 : HasFiniteCoproducts.{v_1, u_1} P.FullSubcategory
this : ∀ (J : Type) [Finite J], PreservesColimitsOfShape (Discrete J) P.ι
⊢ P.IsClosedUnderFiniteCoproducts

Tactic:
⟨fun J _ ↦ P.isClosedUnderColimitsOfShape_of_preservesColimitsOfShape_ι _⟩

Premises used: CategoryTheory.ObjectProperty.IsClosedUnderFiniteCoproducts.mk, CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_of_preservesColimitsOfShape_ι, CategoryTheory.Discrete
-- Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_1 : HasFiniteCoproducts.{v_1, u_1} C
inst_2 : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst_3 : P.IsClosedUnderBinaryCoproducts
this_1 : P.IsClosedUnderIsomorphisms
this_2 : HasFiniteCoproducts.{v_1, u_1} P.FullSubcategory
this : ∀ (J : Type) [Finite J], PreservesColimitsOfShape (Discrete J) P.ι
⊢ P.IsClosedUnderFiniteCoproducts

Tactic:
exact ⟨fun J _ ↦ P.isClosedUnderColimitsOfShape_of_preservesColimitsOfShape_ι _⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.Nonempty
⊢ Nonempty.{u + 1} P.FullSubcategory

Tactic:
Nonempty.intro ⟨P.arbitrary, P.prop_arbitrary⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, Nonempty.intro, CategoryTheory.ObjectProperty.arbitrary, CategoryTheory.ObjectProperty.prop_arbitrary
-- Module: Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
f g : X ⟶ Y
h : f.hom = g.hom
⊢ f = g

Tactic:
InducedCategory.hom_ext h

Premises used: CategoryTheory.InducedCategory.hom_ext
-- Module: Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X : P.FullSubcategory
⊢ P.ι.obj X = X.obj (P := P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
f : X ⟶ Y
⊢ P.ι.map f = f.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X : P.FullSubcategory
⊢ P (P.ι.obj X)

Tactic:
X.2

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X : P.FullSubcategory
⊢ InducedCategory.Hom.hom (𝟙 X) = 𝟙 (X.obj (P := P))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X Y Z : P.FullSubcategory
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).hom = f.hom ≫ g.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
⊢ Function.Surjective.{v + 1, v + 1} (α := X.obj (P := P) ⟶ Y.obj (P := P)) (homMk (P := P))

Tactic:
fun f ↦ ⟨f.hom, rfl⟩

Premises used: Exists.intro, CategoryTheory.InducedCategory.Hom.hom, Function.Surjective, rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
⊢ P.ι.Full

Tactic:
P.fullyFaithfulι.full

Premises used: CategoryTheory.ObjectProperty.fullyFaithfulι, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
⊢ P.ι.Faithful

Tactic:
P.fullyFaithfulι.faithful

Premises used: CategoryTheory.ObjectProperty.fullyFaithfulι, CategoryTheory.Functor.FullyFaithful.faithful
-- Module: Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
e : X ≅ Y
⊢ e.hom.hom ≫ e.inv.hom = 𝟙 (X.obj (P := P))

Tactic:
P.ι.congr_map e.hom_inv_id

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Functor.congr_map
-- Module: Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
e : X ≅ Y
⊢ e.inv.hom ≫ e.hom.hom = 𝟙 (Y.obj (P := P))

Tactic:
P.ι.congr_map e.inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.ObjectProperty.ι, CategoryTheory.Functor.congr_map
-- Module: Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
f : X ⟶ Y
inst_1 : IsIso f
⊢ IsIso f.hom

Tactic:
P.ι.map_isIso f

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.Functor.map_isIso
-- Module: Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
f : X ⟶ Y
inst_1 : IsIso f
⊢ (inv f).hom = inv f.hom

Tactic:
IsIso.eq_inv_of_hom_inv_id (P.ι.congr_map (asIso f).hom_inv_id)

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.Iso.hom_inv_id, CategoryTheory.IsIso.eq_inv_of_hom_inv_id, CategoryTheory.Functor.congr_map, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
f : X ⟶ Y
⊢ IsIso f.hom ↔ IsIso f

Tactic:
⟨fun _ ↦ (P.isoMk (asIso f.hom)).isIso_hom, fun _ ↦ inferInstance⟩

Premises used: inferInstance, CategoryTheory.Iso.isIso_hom, CategoryTheory.ObjectProperty.isoMk, Iff.intro, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
P P' : ObjectProperty.{v, u} C
h : P ≤ P'
⊢ (ιOfLE (P := P) (P' := P') h).Full

Tactic:
(fullyFaithfulιOfLE h).full

Premises used: CategoryTheory.Functor.FullyFaithful.full, CategoryTheory.ObjectProperty.fullyFaithfulιOfLE
-- Module: Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
P P' : ObjectProperty.{v, u} C
h : P ≤ P'
⊢ (ιOfLE (P := P) (P' := P') h).Faithful

Tactic:
(fullyFaithfulιOfLE h).faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, CategoryTheory.ObjectProperty.fullyFaithfulιOfLE
-- Module: Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v', u'} D
F : Functor.{v, v', u, u'} C D
hF : ∀ (X : C), P (F.obj X)
X : C
⊢ P.ι.obj ((P.lift F hF).obj X) = F.obj X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v', u'} D
F : Functor.{v, v', u, u'} C D
hF : ∀ (X : C), P (F.obj X)
X Y : C
f : X ⟶ Y
⊢ P.ι.map ((P.lift F hF).map f) = F.map f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v', u'} D
F : Functor.{v, v', u, u'} C D
hF : ∀ (X : C), P (F.obj X)
inst_2 : F.Faithful
⊢ (P.lift F hF).Faithful

Tactic:
Functor.Faithful.of_comp_iso (P.liftCompιIso F hF)

Premises used: CategoryTheory.ObjectProperty.liftCompιIso, CategoryTheory.Functor.Faithful.of_comp_iso
-- Module: Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P Q : ObjectProperty.{v', u'} D
F : Functor.{v, v', u, u'} C D
hF : ∀ (X : C), P (F.obj X)
inst_2 : F.Full
⊢ (P.lift F hF).Full

Tactic:
Functor.Full.of_comp_faithful_iso (P.liftCompιIso F hF)

Premises used: CategoryTheory.ObjectProperty.liftCompιIso, CategoryTheory.Functor.Full.of_comp_faithful_iso
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_3, u_1} J
inst_2 : Category.{v_5, u_3} C
F : Functor.{v_1, v_3, u_5, u_1} K J
G : Functor.{v_3, v_5, u_1, u_3} J C
⊢ preservesLimit F G ↔ PreservesLimit F G

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_3, u_1} J
inst_2 : Category.{v_5, u_3} C
F F' : Functor.{v_1, v_3, u_5, u_1} K J
e : F ≅ F'
h : ∀ (G : Functor.{v_3, v_5, u_1, u_3} J C), preservesLimit F G ↔ preservesLimit F' G
⊢ Eq (α := ObjectProperty (Functor.{v_3, v_5, u_1, u_3} J C)) (preservesLimit F) (preservesLimit F')

Tactic:
ext G
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_3, u_1} J
inst_2 : Category.{v_5, u_3} C
F F' : Functor.{v_1, v_3, u_5, u_1} K J
e : F ≅ F'
G : Functor.{v_3, v_5, u_1, u_3} J C
⊢ PreservesLimit F G ↔ PreservesLimit F' G

Tactic:
⟨fun h ↦ preservesLimit_of_iso_diagram _ e,
    fun h ↦ preservesLimit_of_iso_diagram _ e.symm⟩

Premises used: CategoryTheory.Limits.preservesLimit_of_iso_diagram, Iff.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_3, u_1} J
inst_2 : Category.{v_5, u_3} C
F F' : Functor.{v_1, v_3, u_5, u_1} K J
e : F ≅ F'
G : Functor.{v_3, v_5, u_1, u_3} J C
⊢ PreservesLimit F G ↔ PreservesLimit F' G

Tactic:
exact ⟨fun h ↦ preservesLimit_of_iso_diagram _ e,
    fun h ↦ preservesLimit_of_iso_diagram _ e.symm⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_3, u_1} J
inst_2 : Category.{v_5, u_3} C
F : Functor.{v_1, v_3, u_5, u_1} K J
G : Functor.{v_3, v_5, u_1, u_3} J C
⊢ preservesColimit F G ↔ PreservesColimit F G

Tactic:
Iff.rfl

Premises used: Iff.rfl