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 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) →
  (i : Shrink.{t, w} I) ×
    Shrink.{t, v}
      ((A ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ X) ×
        (B ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ S)) :=
  fun (x : FunctorObjIndex f πX) ↦
    Sigma.mk (β := fun (i : Shrink.{t, w} I) ↦
      Shrink.{t, v}
        ((A ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ X) ×
          (B ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ S)))
      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)
      ((equivShrink
            ((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)) ⟶
                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)) ⟶
                S)) :
          (a :
              (A
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  X) ×
                (B
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  S)) →
            Shrink.{t, v}
              ((A
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  X) ×
                (B
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  S)))
        (eqToHom ⋯ ≫ x.t, eqToHom ⋯ ≫ x.b))
i₁ : I
t₁ : A i₁ ⟶ X
b₁ : B i₁ ⟶ S
w : t₁ ≫ πX = f i₁ ≫ b₁
i₂ : I
t₂ : A i₂ ⟶ X
b₂ : B i₂ ⟶ S
w_1 : t₂ ≫ πX = f i₂ ≫ b₂
h : φ { i := i₁, t := t₁, b := b₁, w := w : FunctorObjIndex f πX } = φ { i := i₂, t := t₂, b := b₂, w := w_1 }
⊢ i₁ = i₂

Tactic:
simpa [φ] using congr_arg Sigma.fst h

Premises used: Sigma.fst, congr_arg
-- 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) →
  (i : Shrink.{t, w} I) ×
    Shrink.{t, v}
      ((A ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ X) ×
        (B ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ S)) :=
  fun (x : FunctorObjIndex f πX) ↦
    Sigma.mk (β := fun (i : Shrink.{t, w} I) ↦
      Shrink.{t, v}
        ((A ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ X) ×
          (B ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ S)))
      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)
      ((equivShrink
            ((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)) ⟶
                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)) ⟶
                S)) :
          (a :
              (A
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  X) ×
                (B
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  S)) →
            Shrink.{t, v}
              ((A
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  X) ×
                (B
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  S)))
        (eqToHom ⋯ ≫ x.t, eqToHom ⋯ ≫ x.b))
i₁ : I
t₁ : A i₁ ⟶ X
b₁ : B i₁ ⟶ S
w : t₁ ≫ πX = f i₁ ≫ b₁
i₂ : I
t₂ : A i₂ ⟶ X
b₂ : B i₂ ⟶ S
w_1 : t₂ ≫ πX = f i₂ ≫ b₂
h : φ { i := i₁, t := t₁, b := b₁, w := w : FunctorObjIndex f πX } = φ { i := i₂, t := t₂, b := b₂, w := w_1 }
obtain :
  ∀ (t₂ : A i₁ ⟶ X) (b₂ : B i₁ ⟶ S) (w_2 : t₂ ≫ πX = f i₁ ≫ b₂)
    (h : φ { i := i₁, t := t₁, b := b₁, w := w : FunctorObjIndex f πX } = φ { i := i₁, t := t₂, b := b₂, w := w_2 }),
    { i := i₁, t := t₁, b := b₁, w := w : FunctorObjIndex f πX } = { i := i₁, t := t₂, b := b₂, w := w_2 }
⊢ { i := i₁, t := t₁, b := b₁, w := w : FunctorObjIndex f πX } = { i := i₂, t := t₂, b := b₂, w := w_1 }

Tactic:
obtain rfl : i₁ = i₂ := by simpa [φ] using congr_arg Sigma.fst h

Premises used: 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 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) →
  (i : Shrink.{t, w} I) ×
    Shrink.{t, v}
      ((A ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ X) ×
        (B ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ S)) :=
  fun (x : FunctorObjIndex f πX) ↦
    Sigma.mk (β := fun (i : Shrink.{t, w} I) ↦
      Shrink.{t, v}
        ((A ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ X) ×
          (B ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ S)))
      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)
      ((equivShrink
            ((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)) ⟶
                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)) ⟶
                S)) :
          (a :
              (A
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  X) ×
                (B
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  S)) →
            Shrink.{t, v}
              ((A
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  X) ×
                (B
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  S)))
        (eqToHom ⋯ ≫ x.t, eqToHom ⋯ ≫ x.b))
i₁ : I
t₁ : A i₁ ⟶ X
b₁ : B i₁ ⟶ S
w : t₁ ≫ πX = f i₁ ≫ b₁
t₂ : A i₁ ⟶ X
b₂ : B i₁ ⟶ S
w_1 : t₂ ≫ πX = f i₁ ≫ b₂
h : φ { i := i₁, t := t₁, b := b₁, w := w : FunctorObjIndex f πX } = φ { i := i₁, t := t₂, b := b₂, w := w_1 }
⊢ { i := i₁, t := t₁, b := b₁, w := w : FunctorObjIndex f πX } = { i := i₁, t := t₂, b := b₂, w := w_1 }

Tactic:
simpa [cancel_epi, φ] using h

Premises used: CategoryTheory.cancel_epi
-- 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) →
  (i : Shrink.{t, w} I) ×
    Shrink.{t, v}
      ((A ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ X) ×
        (B ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ S)) :=
  fun (x : FunctorObjIndex f πX) ↦
    Sigma.mk (β := fun (i : Shrink.{t, w} I) ↦
      Shrink.{t, v}
        ((A ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ X) ×
          (B ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ S)))
      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)
      ((equivShrink
            ((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)) ⟶
                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)) ⟶
                S)) :
          (a :
              (A
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  X) ×
                (B
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  S)) →
            Shrink.{t, v}
              ((A
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  X) ×
                (B
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  S)))
        (eqToHom ⋯ ≫ x.t, eqToHom ⋯ ≫ x.b))
⊢ Function.Injective φ

Tactic:
have hφ : Function.Injective φ := by
    rintro ⟨i₁, t₁, b₁, _⟩ ⟨i₂, t₂, b₂, _⟩ h
    obtain rfl : i₁ = i₂ := by simpa [φ] using congr_arg Sigma.fst h
    simpa [cancel_epi, φ] using h
-- 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) →
  (i : Shrink.{t, w} I) ×
    Shrink.{t, v}
      ((A ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ X) ×
        (B ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ S)) :=
  fun (x : FunctorObjIndex f πX) ↦
    Sigma.mk (β := fun (i : Shrink.{t, w} I) ↦
      Shrink.{t, v}
        ((A ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ X) ×
          (B ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ S)))
      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)
      ((equivShrink
            ((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)) ⟶
                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)) ⟶
                S)) :
          (a :
              (A
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  X) ×
                (B
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  S)) →
            Shrink.{t, v}
              ((A
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  X) ×
                (B
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  S)))
        (eqToHom ⋯ ≫ x.t, eqToHom ⋯ ≫ x.b))
hφ : Function.Injective φ
⊢ Small.{t, max v w} (FunctorObjIndex f πX)

Tactic:
small_of_injective hφ

Premises used: small_of_injective
-- 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) →
  (i : Shrink.{t, w} I) ×
    Shrink.{t, v}
      ((A ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ X) ×
        (B ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ S)) :=
  fun (x : FunctorObjIndex f πX) ↦
    Sigma.mk (β := fun (i : Shrink.{t, w} I) ↦
      Shrink.{t, v}
        ((A ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ X) ×
          (B ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ S)))
      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)
      ((equivShrink
            ((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)) ⟶
                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)) ⟶
                S)) :
          (a :
              (A
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  X) ×
                (B
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  S)) →
            Shrink.{t, v}
              ((A
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  X) ×
                (B
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  S)))
        (eqToHom ⋯ ≫ x.t, eqToHom ⋯ ≫ x.b))
hφ : Function.Injective φ
⊢ Small.{t, max v w} (FunctorObjIndex f πX)

Tactic:
exact small_of_injective hφ

Premises used: small_of_injective
-- 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
⊢ Small.{t, max v w} (FunctorObjIndex f πX)

Tactic:
infer_instance
-- 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
x : FunctorObjIndex f πX
⊢ (x.t ≫ Arrow.Hom.left τ) ≫ πY = f x.i ≫ x.b ≫ Arrow.Hom.right τ

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_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
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'
⊢ Arrow.Hom.left τ ≫ (Arrow.mk πY).hom = (Arrow.mk πX).hom ≫ Arrow.Hom.right τ

Tactic:
have := τ.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_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
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'
this : Arrow.Hom.left τ ≫ πY = πX ≫ Arrow.Hom.right τ
rw : t' ≫ πY = f i ≫ b ≫ Arrow.Hom.right τ
rw₁ : t' ≫ πY = t ≫ πX ≫ Arrow.Hom.right τ
rw₂ : (t ≫ Arrow.Hom.left τ) ≫ πY = t ≫ πX ≫ Arrow.Hom.right τ
rw₃ : t ≫ Arrow.Hom.left τ ≫ πY = t ≫ πX ≫ Arrow.Hom.right τ
rw₄ rw₅ : t ≫ πX ≫ Arrow.Hom.right τ = t ≫ πX ≫ Arrow.Hom.right τ
⊢ t' ≫ πY = f i ≫ b'

Tactic:
rw [← hb', ← reassoc_of% w, ← ht', assoc, this]

Premises used: CategoryTheory.Category.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
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 (α :=
    functorObjSrcFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ ∐ functorObjSrcFamily 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)
        (functorMapSrc f τ : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjSrcFamily f πY) :
      functorObjSrcFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ ∐ functorObjSrcFamily f πY)
    (Sigma.ι (functorObjSrcFamily f πY) { i := i, t := t ≫ Arrow.Hom.left τ, b := b ≫ Arrow.Hom.right τ, w := ⋯ } :
      functorObjSrcFamily f πY
          { i := i, t := t ≫ Arrow.Hom.left τ, b := b ≫ Arrow.Hom.right τ, w := ⋯ : FunctorObjIndex f πY } ⟶
        ∐ functorObjSrcFamily f πY)
⊢ Eq (α :=
    functorObjSrcFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ ∐ functorObjSrcFamily 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)
        (functorMapSrc f τ : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjSrcFamily f πY) :
      functorObjSrcFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ ∐ functorObjSrcFamily f πY)
    (Sigma.ι (functorObjSrcFamily f πY) { i := i, t := t', b := b', w := ⋯ } :
      functorObjSrcFamily f πY { i := i, t := t', b := b', w := ⋯ : FunctorObjIndex f πY } ⟶ ∐ functorObjSrcFamily 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 (α :=
    functorObjSrcFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ ∐ functorObjSrcFamily 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)
        (functorMapSrc f τ : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjSrcFamily f πY) :
      functorObjSrcFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ ∐ functorObjSrcFamily f πY)
    (Sigma.ι (functorObjSrcFamily f πY) { i := i, t := t ≫ Arrow.Hom.left τ, b := b ≫ Arrow.Hom.right τ, w := ⋯ } :
      functorObjSrcFamily f πY
          { i := i, t := t ≫ Arrow.Hom.left τ, b := b ≫ Arrow.Hom.right τ, w := ⋯ : FunctorObjIndex f πY } ⟶
        ∐ functorObjSrcFamily f πY)

Tactic:
simp [functorMapSrc]

Premises used: CategoryTheory.SmallObject.functorMapSrc