awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
e : X ≅ Y
⊢ Eq (α := Skeleton.{v₁, u₁} C) (toSkeleton X) (toSkeleton Y)

Tactic:
Quotient.sound ⟨e⟩

Premises used: Nonempty.intro, CategoryTheory.InducedCategory, Quotient.sound, CategoryTheory.Skeleton
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
Y : Skeleton.{v₁, u₁} C
⊢ toSkeleton X = Y ↔ Nonempty.{v₁ + 1} (X ≅ Functor.obj (fromSkeleton C) Y)

Tactic:
Quotient.mk_eq_iff_out

Premises used: Quotient.mk_eq_iff_out, Quot.out, CategoryTheory.IsIsomorphic, Quotient.out, CategoryTheory.InducedCategory, Classical.choose, CategoryTheory.Skeleton
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
⊢ F.mapSkeleton.obj (toSkeleton X) = toSkeleton (F.obj X)

Tactic:
congr_toSkeleton_of_iso <| F.mapIso <| fromSkeletonToSkeletonIso X

Premises used: CategoryTheory.congr_toSkeleton_of_iso, CategoryTheory.Functor.mapIso, CategoryTheory.fromSkeletonToSkeletonIso
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.Full
⊢ F.mapSkeleton.Full

Tactic:
inferInstanceAs <| (_ ⋙ _).Full

Premises used: _private.0.CategoryTheory.Functor.instFullSkeletonMapSkeleton._proof_1
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.Faithful
⊢ F.mapSkeleton.Faithful

Tactic:
inferInstanceAs <| (_ ⋙ _).Faithful

Premises used: _private.0.CategoryTheory.Functor.instFaithfulSkeletonMapSkeleton._proof_1
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.EssSurj
⊢ F.mapSkeleton.EssSurj

Tactic:
inferInstanceAs <| (_ ⋙ _).EssSurj

Premises used: _private.0.CategoryTheory.Functor.instEssSurjSkeletonMapSkeleton._proof_1
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
⊢ (Iso.hom
          (fromSkeletonToSkeletonIso
            (F.obj
              (obj.{v₁, v₁, u₁, u₁} (C := Skeleton.{v₁, u₁} C) (Equivalence.functor (skeletonEquivalence C))
                (obj (toSkeletonFunctor C) X)))) ≫
        F.map (map (Equivalence.functor (skeletonEquivalence C)) (map (toSkeletonFunctor C) f)) ≫
          Iso.inv
            (fromSkeletonToSkeletonIso
              (F.obj
                (obj.{v₁, v₁, u₁, u₁} (C := Skeleton.{v₁, u₁} C) (Equivalence.functor (skeletonEquivalence C))
                  (obj (toSkeletonFunctor C) Y))))) ≫
      InducedCategory.Hom.hom
        (Iso.hom
          ((fun (X : C) ↦
              (mapIso (toSkeletonFunctor D) (F.mapIso (fromSkeletonToSkeletonIso X)) :
                Iso (C := Skeleton.{v₂, u₂} D)
                  (obj (toSkeletonFunctor D)
                    (F.obj
                      (obj.{v₁, v₁, u₁, u₁} (C := Skeleton.{v₁, u₁} C) (Equivalence.functor (skeletonEquivalence C))
                        (obj (toSkeletonFunctor C) X))))
                  (obj (toSkeletonFunctor D) (F.obj X))))
            Y)) =
    InducedCategory.Hom.hom
        (Iso.hom
          ((fun (X : C) ↦
              (mapIso (toSkeletonFunctor D) (F.mapIso (fromSkeletonToSkeletonIso X)) :
                Iso (C := Skeleton.{v₂, u₂} D)
                  (obj (toSkeletonFunctor D)
                    (F.obj
                      (obj.{v₁, v₁, u₁, u₁} (C := Skeleton.{v₁, u₁} C) (Equivalence.functor (skeletonEquivalence C))
                        (obj (toSkeletonFunctor C) X))))
                  (obj (toSkeletonFunctor D) (F.obj X))))
            X)) ≫
      ((F ⋙ toSkeletonFunctor D).map f).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
inst_3 : F.Faithful
⊢ Function.Injective F.mapSkeleton.obj

Tactic:
fun _ _ h ↦ skeleton_skeletal C ⟨F.mapSkeleton.preimageIso <| eqToIso h⟩

Premises used: CategoryTheory.eqToIso, Nonempty.intro, CategoryTheory.skeleton_skeletal, CategoryTheory.Functor.preimageIso, CategoryTheory.Functor.mapSkeleton, Function.Injective
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.EssSurj
⊢ Function.Surjective F.mapSkeleton.obj

Tactic:
fun Y ↦ let ⟨X, h⟩ := EssSurj.mem_essImage F.mapSkeleton Y; ⟨X, skeleton_skeletal D h⟩

Premises used: Exists, _private.0.CategoryTheory.Functor.mapSkeleton_surjective.match_1, CategoryTheory.Functor.EssSurj.mem_essImage, CategoryTheory.skeleton_skeletal, CategoryTheory.Functor.mapSkeleton, Exists.intro, Eq, Function.Surjective, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
a₁ b₁ a₂ b₂ : C
i₁ : a₁ ≅ a₂
i₂ : b₁ ≅ b₂
⊢ Eq (α := Prop) ((fun (X Y : C) ↦ Nonempty.{v₁ + 1} (X ⟶ Y)) a₁ b₁) ((fun (X Y : C) ↦ Nonempty.{v₁ + 1} (X ⟶ Y)) a₂ b₂)

Tactic:
propext
              ⟨Nonempty.map fun f => i₁.inv ≫ f ≫ i₂.hom,
                Nonempty.map fun f => i₁.hom ≫ f ≫ i₂.inv⟩

Premises used: Iff.intro, propext, CategoryTheory.CategoryStruct.comp, Nonempty.map, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
a₁ b₁ a₂ b₂ : C
i₁ : a₁ ≅ a₂
i₂ : b₁ ≅ b₂
⊢ Eq (α := Prop) ((fun (X Y : C) ↦ Nonempty.{v₁ + 1} (X ⟶ Y)) a₁ b₁) ((fun (X Y : C) ↦ Nonempty.{v₁ + 1} (X ⟶ Y)) a₂ b₂)

Tactic:
exact
            propext
              ⟨Nonempty.map fun f => i₁.inv ≫ f ≫ i₂.hom,
                Nonempty.map fun f => i₁.hom ≫ f ≫ i₂.inv⟩

Premises used: Iff.intro, propext, CategoryTheory.CategoryStruct.comp, Nonempty.map, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
⊢ ∀ (a : ThinSkeleton.{v₁, u₁} C), Quotient.lift₂ (fun (X Y : C) ↦ Nonempty.{v₁ + 1} (X ⟶ Y)) ⋯ a a

Tactic:
Quotient.ind fun a => ?_

Premises used: Quotient.ind, CategoryTheory.ThinSkeleton
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
refine : ∀ (a : C), Quotient.lift₂ (fun (X Y : C) ↦ Nonempty.{v₁ + 1} (X ⟶ Y)) ⋯ ⟦a⟧ ⟦a⟧
⊢ ∀ (a : ThinSkeleton.{v₁, u₁} C), Quotient.lift₂ (fun (X Y : C) ↦ Nonempty.{v₁ + 1} (X ⟶ Y)) ⋯ a a

Tactic:
refine Quotient.ind fun a => ?_

Premises used: Quotient.ind
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
a : C
⊢ Quotient.lift₂ (fun (X Y : C) ↦ Nonempty.{v₁ + 1} (X ⟶ Y)) ⋯ ⟦a⟧ ⟦a⟧

Tactic:
⟨𝟙 _⟩

Premises used: CategoryTheory.CategoryStruct.id, Nonempty.intro
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
a : C
⊢ Quotient.lift₂ (fun (X Y : C) ↦ Nonempty.{v₁ + 1} (X ⟶ Y)) ⋯ ⟦a⟧ ⟦a⟧

Tactic:
exact ⟨𝟙 _⟩
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
x x_1 : ThinSkeleton.{v₁, u₁} C
f₁ down : x ≤ x_1
⊢ { down := { down := f₁ : PLift (x ≤ x_1) } : ULift.{u₁, 0} (PLift (x ≤ x_1)) } = { down := { down := down } }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
⊢ F ⋙ toThinSkeleton D = toThinSkeleton C ⋙ map F

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, Quotient.map, CategoryTheory.ThinSkeleton, Quotient, CategoryTheory.toThinSkeleton, Quotient.mk', CategoryTheory.homOfLE, Quot.map, rfl
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
inst_3 : Quiver.IsThin.{u₁, v₁} C
⊢ Functor.IsEquivalence.{u₁, v₁, u₁, u₁} (C := ThinSkeleton.{v₁, u₁} C) (fromThinSkeleton C)

Tactic:
(equivalence C).isEquivalence_functor

Premises used: CategoryTheory.ThinSkeleton.fromThinSkeleton, CategoryTheory.ThinSkeleton.equivalence, CategoryTheory.Equivalence.isEquivalence_functor
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Quiver.IsThin.{u₁, v₁} C
X Y : C
f : X ⟶ Y
g : Y ⟶ X
⊢ X ≈ Y

Tactic:
⟨iso_of_both_ways f g⟩

Premises used: CategoryTheory.iso_of_both_ways, CategoryTheory.IsIsomorphic, Nonempty.intro
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
inst_3 : Quiver.IsThin.{u₁, v₁} C
a b : C
f : a ⟶ b
g : b ⟶ a
⊢ ⟦a⟧ = ⟦b⟧

Tactic:
apply Quotient.sound (equiv_of_both_ways f g)

Premises used: CategoryTheory.ThinSkeleton.equiv_of_both_ways, Quotient.sound
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Quiver.IsThin.{u₁, v₁} C
⊢ Skeletal.{u₁, u₁} (ThinSkeleton.{v₁, u₁} C)

Tactic:
fun X Y =>
  Quotient.inductionOn₂ X Y fun _ _ h => h.elim fun i => i.1.le.antisymm i.2.le

Premises used: CategoryTheory.Skeletal, Quotient.inductionOn₂
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
inst_3 : Quiver.IsThin.{u₁, v₁} C
F : Functor.{v₃, v₂, u₃, u₂} E D
G : Functor.{v₂, v₁, u₂, u₁} D C
⊢ map (F ⋙ G) = map F ⋙ map G

Tactic:
Functor.eq_of_iso skeletal <|
    NatIso.ofComponents fun X => Quotient.recOnSubsingleton X fun _ => Iso.refl _

Premises used: CategoryTheory.Functor.eq_of_iso, Quotient.recOnSubsingleton, CategoryTheory.ThinSkeleton.skeletal, CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Quiver.IsThin.{u₁, v₁} C
⊢ Eq (α := ThinSkeleton.{v₁, u₁} C ⥤ ThinSkeleton.{v₁, u₁} C) (map (𝟭 C)) (𝟭 (ThinSkeleton.{v₁, u₁} C))

Tactic:
Functor.eq_of_iso skeletal <|
    NatIso.ofComponents fun X => Quotient.recOnSubsingleton X fun _ => Iso.refl _

Premises used: CategoryTheory.Functor.eq_of_iso, Quotient.recOnSubsingleton, CategoryTheory.ThinSkeleton.skeletal, CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Quiver.IsThin.{u₁, v₁} C
F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} D C
h : F₁ ≅ F₂
⊢ map F₁ = map F₂

Tactic:
Functor.eq_of_iso skeletal
    { hom := mapNatTrans h.hom
      inv := mapNatTrans h.inv }

Premises used: CategoryTheory.Functor.eq_of_iso, CategoryTheory.Iso.mk, CategoryTheory.ThinSkeleton.skeletal, CategoryTheory.Iso.hom, CategoryTheory.ThinSkeleton.mapNatTrans, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
R : Functor.{v₂, v₁, u₂, u₁} D C
L : Functor.{v₁, v₂, u₁, u₂} C D
h : L ⊣ R
X : ThinSkeleton.{v₁, u₁} C
this : Setoid C := isIsomorphicSetoid.{v₁, u₁} C
⊢ Functor.obj (𝟭 (ThinSkeleton.{v₁, u₁} C)) X ⟶ (map L ⋙ map R).obj X

Tactic:
exact Quotient.recOnSubsingleton X fun x => homOfLE ⟨h.unit.app x⟩
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
R : Functor.{v₂, v₁, u₂, u₁} D C
L : Functor.{v₁, v₂, u₁, u₂} C D
h : L ⊣ R
X : ThinSkeleton.{v₂, u₂} D
this : Setoid D := isIsomorphicSetoid.{v₂, u₂} D
⊢ (map R ⋙ map L).obj X ⟶ Functor.obj (𝟭 (ThinSkeleton.{v₂, u₂} D)) X

Tactic:
exact Quotient.recOnSubsingleton X fun x => homOfLE ⟨h.counit.app x⟩
-- Module: Mathlib.CategoryTheory.SmallObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
inst_1 : I.HasSmallObjectArgument
⊢ Fact (Cardinal.IsRegular.{w} I.smallObjectκ)

Tactic:
HasSmallObjectArgument.exists_cardinal.choose_spec.choose

Premises used: Exists.choose_spec, CategoryTheory.MorphismProperty.smallObjectκ, CategoryTheory.MorphismProperty.HasSmallObjectArgument.exists_cardinal, Exists.choose
-- Module: Mathlib.CategoryTheory.SmallObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
inst_1 : I.HasSmallObjectArgument
⊢ IsCardinalForSmallObjectArgument.{w, v, u} I I.smallObjectκ

Tactic:
HasSmallObjectArgument.exists_cardinal.choose_spec.choose_spec.choose_spec

Premises used: Exists.choose_spec, CategoryTheory.MorphismProperty.smallObjectκ, CategoryTheory.MorphismProperty.HasSmallObjectArgument.exists_cardinal
-- Module: Mathlib.CategoryTheory.SmallObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
inst_1 : I.HasSmallObjectArgument
⊢ I.rlp.llp.HasFunctorialFactorization I.rlp

Tactic:
hasFunctorialFactorization I I.smallObjectκ

Premises used: CategoryTheory.SmallObject.hasFunctorialFactorization, CategoryTheory.MorphismProperty.smallObjectκ
-- Module: Mathlib.CategoryTheory.SmallObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
inst_1 : I.HasSmallObjectArgument
⊢ I.rlp.llp =
    (transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts I.smallObjectκ.ord.ToType).retracts

Tactic:
llp_rlp_of_isCardinalForSmallObjectArgument' I I.smallObjectκ

Premises used: CategoryTheory.MorphismProperty.smallObjectκ, CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument'
-- Module: Mathlib.CategoryTheory.SmallObject.Basic
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
inst_1 : I.HasSmallObjectArgument
⊢ I.rlp.llp = (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts).retracts

Tactic:
llp_rlp_of_isCardinalForSmallObjectArgument I I.smallObjectκ

Premises used: CategoryTheory.MorphismProperty.smallObjectκ, CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument
-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
⊢ Eq (α := ∐ functorObjSrcFamily f πX ⟶ functorObj f πX)
    (functorObjTop f πX ≫ ιFunctorObj f πX : ∐ functorObjSrcFamily f πX ⟶ functorObj f πX)
    (CategoryStruct.comp (Y := ∐ functorObjTgtFamily f πX)
        (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
        (ρFunctorObj f πX : ∐ functorObjTgtFamily f πX ⟶ functorObj f πX) :
      ∐ functorObjSrcFamily f πX ⟶ functorObj f πX)

Tactic:
pushout.condition

Premises used: CategoryTheory.Limits.pushout.condition
-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
⊢ IsPushout (Z := ∐ functorObjSrcFamily f πX) (Y := ∐ functorObjTgtFamily f πX) (P := functorObj f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX) (ιFunctorObj f πX)
    (ρFunctorObj f πX : ∐ functorObjTgtFamily f πX ⟶ functorObj f πX)

Tactic:
IsPushout.of_hasPushout _ _

Premises used: CategoryTheory.IsPushout.of_hasPushout
-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
x : FunctorObjIndex f πX
⊢ Eq (α := A x.i ⟶ functorObj f πX) (f x.i ≫ Sigma.ι (functorObjTgtFamily f πX) x ≫ ρFunctorObj f πX)
    (x.t ≫ ιFunctorObj f πX)

Tactic:
simpa using (Sigma.ι (functorObjSrcFamily f πX) x ≫= functorObj_comm f πX).symm

Premises used: CategoryTheory.SmallObject.functorObjSrcFamily, CategoryTheory.Limits.Sigma.ι, CategoryTheory.SmallObject.functorObj_comm, Eq.symm, CategoryTheory.whisker_eq
-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
h :
  ∀ (b : FunctorObjIndex f πX),
    CategoryStruct.comp (Y := ∐ functorObjSrcFamily f πX)
        (Sigma.ι (functorObjSrcFamily f πX) b : functorObjSrcFamily f πX b ⟶ ∐ functorObjSrcFamily f πX)
        (functorObjTop f πX ≫ πX : ∐ functorObjSrcFamily f πX ⟶ S) =
      CategoryStruct.comp (Y := ∐ functorObjSrcFamily f πX)
        (Sigma.ι (functorObjSrcFamily f πX) b : functorObjSrcFamily f πX b ⟶ ∐ functorObjSrcFamily f πX)
        (CategoryStruct.comp (Y := ∐ functorObjTgtFamily f πX)
            (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
            (π'FunctorObj f πX : ∐ functorObjTgtFamily f πX ⟶ S) :
          ∐ functorObjSrcFamily f πX ⟶ S)
⊢ Eq (α := ∐ functorObjSrcFamily f πX ⟶ S) (functorObjTop f πX ≫ πX : ∐ functorObjSrcFamily f πX ⟶ S)
    (CategoryStruct.comp (Y := ∐ functorObjTgtFamily f πX)
        (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
        (π'FunctorObj f πX : ∐ functorObjTgtFamily f πX ⟶ S) :
      ∐ functorObjSrcFamily f πX ⟶ S)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
b : FunctorObjIndex f πX
⊢ CategoryStruct.comp (Y := ∐ functorObjSrcFamily f πX)
      (Sigma.ι (functorObjSrcFamily f πX) b : functorObjSrcFamily f πX b ⟶ ∐ functorObjSrcFamily f πX)
      (functorObjTop f πX ≫ πX : ∐ functorObjSrcFamily f πX ⟶ S) =
    CategoryStruct.comp (Y := ∐ functorObjSrcFamily f πX)
      (Sigma.ι (functorObjSrcFamily f πX) b : functorObjSrcFamily f πX b ⟶ ∐ functorObjSrcFamily f πX)
      (CategoryStruct.comp (Y := ∐ functorObjTgtFamily f πX)
          (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
          (π'FunctorObj f πX : ∐ functorObjTgtFamily f πX ⟶ S) :
        ∐ functorObjSrcFamily f πX ⟶ S)

Tactic:
simp [π'FunctorObj]

Premises used: CategoryTheory.SmallObject.π'FunctorObj
-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
⊢ Eq (α := ∐ functorObjTgtFamily f πX ⟶ S)
    (CategoryStruct.comp (Y := functorObj f πX) (ρFunctorObj f πX) (πFunctorObj f πX) : ∐ functorObjTgtFamily f πX ⟶ S)
    (π'FunctorObj f πX : ∐ functorObjTgtFamily f πX ⟶ S)

Tactic:
simp [πFunctorObj]

Premises used: CategoryTheory.SmallObject.πFunctorObj
-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
⊢ CategoryStruct.comp (Y := functorObj f πX) (ιFunctorObj f πX) (πFunctorObj f πX) = πX

Tactic:
simp [ιFunctorObj, πFunctorObj]

Premises used: CategoryTheory.SmallObject.πFunctorObj, CategoryTheory.SmallObject.ιFunctorObj
-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
inst_3 : LocallySmall.{t, v, u} C
inst_4 : Small.{t, w} I
x : FunctorObjIndex f πX
⊢ A
      ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I)
        ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i : Shrink.{t, w} I)) =
    A x.i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
inst_3 : LocallySmall.{t, v, u} C
inst_4 : Small.{t, w} I
x : FunctorObjIndex f πX
⊢ B
      ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I)
        ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i : Shrink.{t, w} I)) =
    B x.i

Tactic:
simp