-- Mathlib/CategoryTheory/SmallObject/Construction.lean
@[simp]
lemma functorMap_id : functorMap f (𝟙 (Arrow.mk πX)) = 𝟙 _

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

Tactic:
simp

Result:
no goals

Proof state:
case h₁.h.mk
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)
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
⊢ Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } ≫
      pushout.inr (functorObjTop f πX) (functorObjLeft f πX) ≫ functorMap f (𝟙 (Arrow.mk πX)) =
    Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } ≫
      pushout.inr (functorObjTop f πX) (functorObjLeft f πX) ≫ 𝟙 (functorObj f πX)

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

Result:
no goals

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

Tactic:
simp

Result:
no goals

Proof state:
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)
⊢ pushout.inl (functorObjTop f πX) (functorObjLeft f πX) ≫ functorMap f (𝟙 (Arrow.mk πX)) =
    pushout.inl (functorObjTop f πX) (functorObjLeft f πX) ≫ 𝟙 (functorObj f πX)

Tactic:
simp [functorMap]

Result:
no goals

Proof state:
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)
⊢ functorMap f (𝟙 (Arrow.mk πX)) = 𝟙 (functorObj f πX)

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

Result:
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)
⊢ pushout.inl (functorObjTop f πX) (functorObjLeft f πX) ≫ functorMap f (𝟙 (Arrow.mk πX)) =
    pushout.inl (functorObjTop f πX) (functorObjLeft f πX) ≫ 𝟙 (functorObj f πX)

case h₁.h.mk
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)
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
⊢ Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } ≫
      pushout.inr (functorObjTop f πX) (functorObjLeft f πX) ≫ functorMap f (𝟙 (Arrow.mk πX)) =
    Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } ≫
      pushout.inr (functorObjTop f πX) (functorObjLeft f πX) ≫ 𝟙 (functorObj f πX)