Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: case h₁
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✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝¹ : HasPushouts C
inst✝ : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
π₁ π₂ π₃ : Arrow C
τ : π₁ ⟶ π₂
τ' : π₂ ⟶ π₃
⊢ pushout.map (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) (functorObjTop f π₃.hom) (functorObjLeft f π₃.hom)
      (Arrow.Hom.left τ ≫ Arrow.Hom.left τ') (functorMapTgt f (τ ≫ τ')) (functorMapSrc f (τ ≫ τ')) ⋯ ⋯ =
    pushout.map (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) (functorObjTop f π₂.hom) (functorObjLeft f π₂.hom)
        (Arrow.Hom.left τ) (functorMapTgt f τ) (functorMapSrc f τ) ⋯ ⋯ ≫
      pushout.map (functorObjTop f π₂.hom) (functorObjLeft f π₂.hom) (functorObjTop f π₃.hom) (functorObjLeft f π₃.hom)
        (Arrow.Hom.left τ') (functorMapTgt f τ') (functorMapSrc f τ') ⋯ ⋯

Tactic:
ext ⟨i, t, b, w⟩

Goal state after:
case h₁.h₀
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✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝¹ : HasPushouts C
inst✝ : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
π₁ π₂ π₃ : Arrow C
τ : π₁ ⟶ π₂
τ' : π₂ ⟶ π₃
⊢ pushout.inl (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) ≫
      pushout.map (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) (functorObjTop f π₃.hom) (functorObjLeft f π₃.hom)
        (Arrow.Hom.left τ ≫ Arrow.Hom.left τ') (functorMapTgt f (τ ≫ τ')) (functorMapSrc f (τ ≫ τ')) ⋯ ⋯ =
    pushout.inl (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) ≫
      pushout.map (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) (functorObjTop f π₂.hom) (functorObjLeft f π₂.hom)
          (Arrow.Hom.left τ) (functorMapTgt f τ) (functorMapSrc f τ) ⋯ ⋯ ≫
        pushout.map (functorObjTop f π₂.hom) (functorObjLeft f π₂.hom) (functorObjTop f π₃.hom)
          (functorObjLeft f π₃.hom) (Arrow.Hom.left τ') (functorMapTgt f τ') (functorMapSrc f τ') ⋯ ⋯

case h₁
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✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝¹ : HasPushouts C
inst✝ : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
π₁ π₂ π₃ : Arrow C
τ : π₁ ⟶ π₂
τ' : π₂ ⟶ π₃
i : I
t : A i ⟶ π₁.left
b : B i ⟶ π₁.right
w : t ≫ π₁.hom = f i ≫ b
⊢ Sigma.ι (functorObjTgtFamily f π₁.hom) { i := i, t := t, b := b, w := w } ≫
      pushout.inr (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) ≫
        pushout.map (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) (functorObjTop f π₃.hom)
          (functorObjLeft f π₃.hom) (Arrow.Hom.left τ ≫ Arrow.Hom.left τ') (functorMapTgt f (τ ≫ τ'))
          (functorMapSrc f (τ ≫ τ')) ⋯ ⋯ =
    Sigma.ι (functorObjTgtFamily f π₁.hom) { i := i, t := t, b := b, w := w } ≫
      pushout.inr (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) ≫
        pushout.map (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) (functorObjTop f π₂.hom)
            (functorObjLeft f π₂.hom) (Arrow.Hom.left τ) (functorMapTgt f τ) (functorMapSrc f τ) ⋯ ⋯ ≫
          pushout.map (functorObjTop f π₂.hom) (functorObjLeft f π₂.hom) (functorObjTop f π₃.hom)
            (functorObjLeft f π₃.hom) (Arrow.Hom.left τ') (functorMapTgt f τ') (functorMapSrc f τ') ⋯ ⋯