awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (hypothesis)
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))
⊢ Small.{t, max v w} (FunctorObjIndex f πX)
have hφ : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (hypothesis)
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'
⊢ t' ≫ πY = f i ≫ b'
have this : Arrow.Hom.left τ ≫ (Arrow.mk πY).hom = (Arrow.mk πX).hom ≫ Arrow.Hom.right τ
Tactic: have := τ.w
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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 τ
⊢ t' ≫ πY = f i ≫ b'
have rw : t' ≫ πY = f i ≫ b ≫ Arrow.Hom.right τ
Tactic: rw [← hb', ← reassoc_of% w, ← ht', assoc, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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 τ
⊢ t' ≫ πY = f i ≫ b'
have rw₁ : t' ≫ πY = t ≫ πX ≫ Arrow.Hom.right τ
Tactic: rw [← hb', ← reassoc_of% w, ← ht', assoc, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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 τ
⊢ t' ≫ πY = f i ≫ b'
have rw₂ : (t ≫ Arrow.Hom.left τ) ≫ πY = t ≫ πX ≫ Arrow.Hom.right τ
Tactic: rw [← hb', ← reassoc_of% w, ← ht', assoc, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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 τ
⊢ t' ≫ πY = f i ≫ b'
have rw₃ : t ≫ Arrow.Hom.left τ ≫ πY = t ≫ πX ≫ Arrow.Hom.right τ
Tactic: rw [← hb', ← reassoc_of% w, ← ht', assoc, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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 τ
⊢ t' ≫ πY = f i ≫ b'
have rw₄ : t ≫ πX ≫ Arrow.Hom.right τ = t ≫ πX ≫ Arrow.Hom.right τ
Tactic: rw [← hb', ← reassoc_of% w, ← ht', assoc, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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'
⊢ 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)
have 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 := sorry } :
    functorObjSrcFamily f πY
        { i := i, t := t ≫ Arrow.Hom.left τ, b := b ≫ Arrow.Hom.right τ, w := sorry : FunctorObjIndex f πY } ⟶
      ∐ functorObjSrcFamily f πY)
Tactic: subst hb' ht'
Cleared hypotheses: b', hb', t', ht'
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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
⊢ 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)
have 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))
Tactic: ext ⟨i, t, b, w⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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'
⊢ 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)
have 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 := sorry } :
    functorObjTgtFamily f πY
        { i := i, t := t ≫ Arrow.Hom.left τ, b := b ≫ Arrow.Hom.right τ, w := sorry : FunctorObjIndex f πY } ⟶
      ∐ functorObjTgtFamily f πY)
Tactic: subst hb' ht'
Cleared hypotheses: b', hb', t', ht'
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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
⊢ 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)
have 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)
Tactic: ext ⟨i, t, b, w⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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 (α := functorObj f πX ⟶ T) (CategoryStruct.comp (Y := functorObj f πY) (functorMap f τ) (πFunctorObj f πY))
    (πFunctorObj f πX ≫ Arrow.Hom.right τ)
have h₀ : 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: ext ⟨i, t, b, w⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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)
⊢ functorMap f (𝟙 (Arrow.mk πX)) = 𝟙 (functorObj f πX)
have h₀ : 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: ext ⟨i, t, b, w⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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' S' Z' : C
πX' : X' ⟶ S'
ι' : X' ⟶ Z'
πZ' : Z' ⟶ S'
fac' : ι' ≫ πZ' = πX'
eX : X' ≅ X
eS : S' ≅ S
eZ : Z' ≅ functorObj f πX
commι : ι' ≫ eZ.hom = eX.hom ≫ ιFunctorObj f πX
commπ : πZ' ≫ eS.hom = eZ.hom ≫ πFunctorObj f πX
i : I
t : A i ⟶ X'
b : B i ⟶ S'
fac : t ≫ πX' = f i ≫ b
⊢ (t ≫ eX.hom) ≫ πX = f i ≫ b ≫ eS.hom
have rw : t ≫ eX.hom ≫ πX = f i ≫ b ≫ eS.hom
Tactic: rw [assoc, ← ιFunctorObj_πFunctorObj f πX, ← reassoc_of% commι, ← commπ,
        reassoc_of% fac', reassoc_of% fac]