awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
h :
  ∀ (i : I) (t : A i ⟶ X) (b : B i ⟶ S) (w : t ≫ πX = f i ≫ b),
    Eq (α := functorObjSrcFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ Y)
      (CategoryStruct.comp (Y := ∐ functorObjSrcFamily f πX)
        (Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w } :
          functorObjSrcFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶
            ∐ functorObjSrcFamily f πX)
        (CategoryStruct.comp (Y := ∐ functorObjSrcFamily f πY)
            (functorMapSrc f τ : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjSrcFamily f πY)
            (functorObjTop f πY : ∐ functorObjSrcFamily f πY ⟶ Y) :
          ∐ functorObjSrcFamily f πX ⟶ Y))
      (CategoryStruct.comp (Y := ∐ functorObjSrcFamily f πX)
        (Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w } :
          functorObjSrcFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶
            ∐ functorObjSrcFamily f πX)
        (functorObjTop f πX ≫ Arrow.Hom.left τ : ∐ functorObjSrcFamily f πX ⟶ (Arrow.mk πY).left))
⊢ Eq (α := ∐ functorObjSrcFamily f πX ⟶ Y)
    (CategoryStruct.comp (Y := ∐ functorObjSrcFamily f πY)
        (functorMapSrc f τ : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjSrcFamily f πY)
        (functorObjTop f πY : ∐ functorObjSrcFamily f πY ⟶ Y) :
      ∐ functorObjSrcFamily f πX ⟶ Y)
    (functorObjTop f πX ≫ Arrow.Hom.left τ : ∐ functorObjSrcFamily f πX ⟶ (Arrow.mk πY).left)

Tactic:
ext ⟨i, t, b, w⟩
-- 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 T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
⊢ Eq (α := functorObjSrcFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ Y)
    (CategoryStruct.comp (Y := ∐ functorObjSrcFamily f πX)
      (Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w } :
        functorObjSrcFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ ∐ functorObjSrcFamily f πX)
      (CategoryStruct.comp (Y := ∐ functorObjSrcFamily f πY)
          (functorMapSrc f τ : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjSrcFamily f πY)
          (functorObjTop f πY : ∐ functorObjSrcFamily f πY ⟶ Y) :
        ∐ functorObjSrcFamily f πX ⟶ Y))
    (CategoryStruct.comp (Y := ∐ functorObjSrcFamily f πX)
      (Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w } :
        functorObjSrcFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ ∐ functorObjSrcFamily f πX)
      (functorObjTop f πX ≫ Arrow.Hom.left τ : ∐ functorObjSrcFamily f πX ⟶ (Arrow.mk πY).left))

Tactic:
simp [ι_functorMapSrc_assoc f τ i t b w _ rfl]

Premises used: CategoryTheory.SmallObject.ι_functorMapSrc_assoc, rfl
-- 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 T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
b' : B i ⟶ T
hb' : b ≫ Arrow.Hom.right τ = b'
t' : A i ⟶ Y
ht' : t ≫ Arrow.Hom.left τ = t'
subst :
  Eq (α :=
    functorObjTgtFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ ∐ functorObjTgtFamily f πY)
    (CategoryStruct.comp (Y := ∐ functorObjTgtFamily f πX)
        (Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } :
          functorObjTgtFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶
            ∐ functorObjTgtFamily f πX)
        (functorMapTgt f τ : ∐ functorObjTgtFamily f πX ⟶ ∐ functorObjTgtFamily f πY) :
      functorObjTgtFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ ∐ functorObjTgtFamily f πY)
    (Sigma.ι (functorObjTgtFamily f πY) { i := i, t := t ≫ Arrow.Hom.left τ, b := b ≫ Arrow.Hom.right τ, w := ⋯ } :
      functorObjTgtFamily f πY
          { i := i, t := t ≫ Arrow.Hom.left τ, b := b ≫ Arrow.Hom.right τ, w := ⋯ : FunctorObjIndex f πY } ⟶
        ∐ functorObjTgtFamily f πY)
⊢ Eq (α :=
    functorObjTgtFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ ∐ functorObjTgtFamily f πY)
    (CategoryStruct.comp (Y := ∐ functorObjTgtFamily f πX)
        (Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } :
          functorObjTgtFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶
            ∐ functorObjTgtFamily f πX)
        (functorMapTgt f τ : ∐ functorObjTgtFamily f πX ⟶ ∐ functorObjTgtFamily f πY) :
      functorObjTgtFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ ∐ functorObjTgtFamily f πY)
    (Sigma.ι (functorObjTgtFamily f πY) { i := i, t := t', b := b', w := ⋯ } :
      functorObjTgtFamily f πY { i := i, t := t', b := b', w := ⋯ : FunctorObjIndex f πY } ⟶ ∐ functorObjTgtFamily f πY)

Tactic:
subst hb' ht'
-- 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 T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
⊢ Eq (α :=
    functorObjTgtFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ ∐ functorObjTgtFamily f πY)
    (CategoryStruct.comp (Y := ∐ functorObjTgtFamily f πX)
        (Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } :
          functorObjTgtFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶
            ∐ functorObjTgtFamily f πX)
        (functorMapTgt f τ : ∐ functorObjTgtFamily f πX ⟶ ∐ functorObjTgtFamily f πY) :
      functorObjTgtFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ ∐ functorObjTgtFamily f πY)
    (Sigma.ι (functorObjTgtFamily f πY) { i := i, t := t ≫ Arrow.Hom.left τ, b := b ≫ Arrow.Hom.right τ, w := ⋯ } :
      functorObjTgtFamily f πY
          { i := i, t := t ≫ Arrow.Hom.left τ, b := b ≫ Arrow.Hom.right τ, w := ⋯ : FunctorObjIndex f πY } ⟶
        ∐ functorObjTgtFamily f πY)

Tactic:
simp [functorMapTgt]

Premises used: CategoryTheory.SmallObject.functorMapTgt
-- 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 T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
h :
  ∀ (i : I) (t : A i ⟶ X) (b : B i ⟶ S) (w : t ≫ πX = f i ≫ b),
    Eq (α :=
      functorObjSrcFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ ∐ functorObjTgtFamily f πY)
      (CategoryStruct.comp (Y := ∐ functorObjSrcFamily f πX)
          (Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w } :
            functorObjSrcFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶
              ∐ functorObjSrcFamily f πX)
          (CategoryStruct.comp (Y := ∐ functorObjTgtFamily f πX)
              (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
              (functorMapTgt f τ : ∐ functorObjTgtFamily f πX ⟶ ∐ functorObjTgtFamily f πY) :
            ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πY) :
        functorObjSrcFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ ∐ functorObjTgtFamily f πY)
      (CategoryStruct.comp (Y := ∐ functorObjSrcFamily f πX)
          (Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w } :
            functorObjSrcFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶
              ∐ functorObjSrcFamily f πX)
          (CategoryStruct.comp (Y := ∐ functorObjSrcFamily f πY)
              (functorMapSrc f τ : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjSrcFamily f πY)
              (functorObjLeft f πY : ∐ functorObjSrcFamily f πY ⟶ ∐ functorObjTgtFamily f πY) :
            ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πY) :
        functorObjSrcFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ ∐ functorObjTgtFamily f πY)
⊢ Eq (α := ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πY)
    (CategoryStruct.comp (Y := ∐ functorObjTgtFamily f πX)
        (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
        (functorMapTgt f τ : ∐ functorObjTgtFamily f πX ⟶ ∐ functorObjTgtFamily f πY) :
      ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πY)
    (CategoryStruct.comp (Y := ∐ functorObjSrcFamily f πY)
        (functorMapSrc f τ : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjSrcFamily f πY)
        (functorObjLeft f πY : ∐ functorObjSrcFamily f πY ⟶ ∐ functorObjTgtFamily f πY) :
      ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πY)

Tactic:
ext ⟨i, t, b, w⟩
-- 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 T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
⊢ Eq (α :=
    functorObjSrcFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ ∐ functorObjTgtFamily f πY)
    (CategoryStruct.comp (Y := ∐ functorObjSrcFamily f πX)
        (Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w } :
          functorObjSrcFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶
            ∐ functorObjSrcFamily f πX)
        (CategoryStruct.comp (Y := ∐ functorObjTgtFamily f πX)
            (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
            (functorMapTgt f τ : ∐ functorObjTgtFamily f πX ⟶ ∐ functorObjTgtFamily f πY) :
          ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πY) :
      functorObjSrcFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ ∐ functorObjTgtFamily f πY)
    (CategoryStruct.comp (Y := ∐ functorObjSrcFamily f πX)
        (Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w } :
          functorObjSrcFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶
            ∐ functorObjSrcFamily f πX)
        (CategoryStruct.comp (Y := ∐ functorObjSrcFamily f πY)
            (functorMapSrc f τ : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjSrcFamily f πY)
            (functorObjLeft f πY : ∐ functorObjSrcFamily f πY ⟶ ∐ functorObjTgtFamily f πY) :
          ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πY) :
      functorObjSrcFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ ∐ functorObjTgtFamily f πY)

Tactic:
simp [ι_functorMapTgt f τ i t b w _ rfl, ι_functorMapSrc_assoc f τ i t b w _ rfl]

Premises used: CategoryTheory.SmallObject.ι_functorMapSrc_assoc, CategoryTheory.SmallObject.ι_functorMapTgt, rfl
-- 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_1 X_1 : C
πX_1 : X_1 ⟶ S_1
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX_1)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX_1) (Z := ∐ functorObjTgtFamily f πX_1)
    (functorObjTop f πX_1 : ∐ functorObjSrcFamily f πX_1 ⟶ X_1)
    (functorObjLeft f πX_1 : ∐ functorObjSrcFamily f πX_1 ⟶ ∐ functorObjTgtFamily f πX_1)
S T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst_3 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_4 : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
inst_5 :
  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_6 :
  HasPushout (X := ∐ functorObjSrcFamily f πY) (Z := ∐ functorObjTgtFamily f πY)
    (functorObjTop f πY : ∐ functorObjSrcFamily f πY ⟶ Y)
    (functorObjLeft f πY : ∐ functorObjSrcFamily f πY ⟶ ∐ functorObjTgtFamily f πY)
⊢ Eq (α := ∐ functorObjSrcFamily f πX ⟶ Y) (functorObjTop f πX ≫ Arrow.Hom.left τ : ∐ functorObjSrcFamily f πX ⟶ Y)
    (CategoryStruct.comp (Y := ∐ functorObjSrcFamily f πY)
        (functorMapSrc f τ : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjSrcFamily f πY)
        (functorObjTop f πY : ∐ functorObjSrcFamily f πY ⟶ Y) :
      ∐ functorObjSrcFamily f πX ⟶ Y)

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 T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
inst_3 :
  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_4 :
  HasPushout (X := ∐ functorObjSrcFamily f πY) (Z := ∐ functorObjTgtFamily f πY)
    (functorObjTop f πY : ∐ functorObjSrcFamily f πY ⟶ Y)
    (functorObjLeft f πY : ∐ functorObjSrcFamily f πY ⟶ ∐ functorObjTgtFamily f πY)
⊢ CategoryStruct.comp (Y :=
      pushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
        (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
        (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX))
      (pushout.inl (functorObjTop f πX) (functorObjLeft f πX) :
        X ⟶
          pushout (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 πY) (functorMap f τ) (πFunctorObj f πY) : functorObj f πX ⟶ T) =
    CategoryStruct.comp (Y :=
      pushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
        (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
        (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX))
      (pushout.inl (functorObjTop f πX) (functorObjLeft f πX) :
        X ⟶
          pushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
            (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
            (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX))
      (πFunctorObj f πX ≫ Arrow.Hom.right τ : functorObj f πX ⟶ (Arrow.mk πY).right)

Tactic:
simp [functorMap]

Premises used: CategoryTheory.SmallObject.functorMap
-- 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 :=
      pushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
        (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
        (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX))
      (pushout.inl (functorObjTop f πX) (functorObjLeft f πX) :
        X ⟶
          pushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
            (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
            (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX))
      (functorMap f (𝟙 (Arrow.mk πX)) : functorObj f πX ⟶ functorObj f πX) =
    CategoryStruct.comp (Y :=
      pushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
        (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
        (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX))
      (pushout.inl (functorObjTop f πX) (functorObjLeft f πX) :
        X ⟶
          pushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
            (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
            (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX))
      (𝟙 (functorObj f πX) : functorObj f πX ⟶ functorObj f πX)

Tactic:
simp [functorMap]

Premises used: CategoryTheory.SmallObject.functorMap
-- 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)
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
⊢ b ≫ Arrow.Hom.right (𝟙 (Arrow.mk πX)) = b

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)
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
⊢ t ≫ Arrow.Hom.left (𝟙 (Arrow.mk πX)) = t

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)
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
⊢ Eq (α := functorObjTgtFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ functorObj f πX)
    (CategoryStruct.comp (Y := ∐ functorObjTgtFamily f πX)
      (Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } :
        functorObjTgtFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ ∐ functorObjTgtFamily f πX)
      (CategoryStruct.comp (Y :=
          pushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
            (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
            (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX))
          (pushout.inr (functorObjTop f πX) (functorObjLeft f πX) :
            ∐ functorObjTgtFamily f πX ⟶
              pushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
                (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
                (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX))
          (functorMap f (𝟙 (Arrow.mk πX)) : functorObj f πX ⟶ functorObj f πX) :
        ∐ functorObjTgtFamily f πX ⟶ functorObj f πX))
    (CategoryStruct.comp (Y := ∐ functorObjTgtFamily f πX)
      (Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } :
        functorObjTgtFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ ∐ functorObjTgtFamily f πX)
      (CategoryStruct.comp (Y :=
          pushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
            (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
            (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX))
          (pushout.inr (functorObjTop f πX) (functorObjLeft f πX) :
            ∐ functorObjTgtFamily f πX ⟶
              pushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
                (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
                (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX))
          (𝟙 (functorObj f πX) : functorObj f πX ⟶ functorObj f πX) :
        ∐ functorObjTgtFamily f πX ⟶ functorObj f πX))

Tactic:
simp [functorMap,
      ι_functorMapTgt_assoc f (𝟙 (Arrow.mk πX)) i t b w b (by simp) t (by simp)]

Premises used: CategoryTheory.SmallObject.functorMap, CategoryTheory.CategoryStruct.id, CategoryTheory.Arrow.mk, CategoryTheory.SmallObject.ι_functorMapTgt_assoc
-- 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 T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
inst_3 :
  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_4 :
  HasPushout (X := ∐ functorObjSrcFamily f πY) (Z := ∐ functorObjTgtFamily f πY)
    (functorObjTop f πY : ∐ functorObjSrcFamily f πY ⟶ Y)
    (functorObjLeft f πY : ∐ functorObjSrcFamily f πY ⟶ ∐ functorObjTgtFamily f πY)
⊢ Eq (α := X ⟶ functorObj f πY) (CategoryStruct.comp (Y := functorObj f πX) (ιFunctorObj f πX) (functorMap f τ))
    (Arrow.Hom.left τ ≫ ιFunctorObj f πY)

Tactic:
simp [ιFunctorObj, functorMap]

Premises used: CategoryTheory.SmallObject.functorMap, 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)
i : I
t : A i ⟶ X
b : B i ⟶ S
sq : CommSq t (f i) πX b
⊢ CategoryStruct.comp (Y := functorObj f πX)
      (Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := ⋯ } ≫ ρFunctorObj f πX) (πFunctorObj f πX) =
    b

Tactic:
simp