-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homotopy (goal)
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
h :
  Eq (α := X _⦋n⦌)
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
                (X.map
                  (Quiver.Hom.op
                    (((stdSimplex.objEquiv : Δ[n] _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋n⦌) → ⦋n⦌ ⟶ ⦋n⦌)
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[n] (Fin.last (n + 1))) :
                          (a : Δ[n] _⦋n + 1⦌) → Δ[n] _⦋n⦌)
                        ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n + 1⦌)
                            (SimplexCategory.σ (Fin.last n)) :
                          Δ[n] _⦋n + 1⦌))))) :
              (a : X _⦋n⦌) → X _⦋n⦌)
            x,
          (ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[1] (Fin.last (n + 1))) : (a : Δ[1] _⦋n + 1⦌) → Δ[1] _⦋n⦌)
            (stdSimplex.objMk₁ (Fin.last n).castSucc.succ)).1 :
      X _⦋n⦌)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app ι₀ (op ⦋n⦌)) : (a : X _⦋n⦌) → X _⦋n⦌ ⊗ Δ[1] _⦋n⦌) x).1 :
      X _⦋n⦌)
⊢ Eq (α := X _⦋n⦌ × Δ[1] _⦋n⦌)
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
              (X.map
                (Quiver.Hom.op
                  (((stdSimplex.objEquiv : Δ[n] _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋n⦌) → ⦋n⦌ ⟶ ⦋n⦌)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[n] (Fin.last (n + 1))) :
                        (a : Δ[n] _⦋n + 1⦌) → Δ[n] _⦋n⦌)
                      ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n + 1⦌)
                          (SimplexCategory.σ (Fin.last n)) :
                        Δ[n] _⦋n + 1⦌))))) :
            (a : X _⦋n⦌) → X _⦋n⦌)
          x,
        (ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[1] (Fin.last (n + 1))) : (a : Δ[1] _⦋n + 1⦌) → Δ[1] _⦋n⦌)
          (stdSimplex.objMk₁ (Fin.last n).castSucc.succ)) :
      X _⦋n⦌ × Δ[1] _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app ι₀ (op ⦋n⦌)) : (a : X _⦋n⦌) → X _⦋n⦌ ⊗ Δ[1] _⦋n⦌) x :
      tensorObj (𝒞 := types) (X _⦋n⦌) (Δ[1] _⦋n⦌))
have h₁ : ∀ (k : Fin (n + 1)),
  (↑(((((ConcreteCategory.hom (FC := TypeCat.Fun)
                        (X.map
                          (Quiver.Hom.op
                            (((stdSimplex.objEquiv : Δ[n] _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋n⦌) → ⦋n⦌ ⟶ ⦋n⦌)
                              ((ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[n] (Fin.last (n + 1))) :
                                  (a : Δ[n] _⦋n + 1⦌) → Δ[n] _⦋n⦌)
                                ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n + 1⦌)
                                    (SimplexCategory.σ (Fin.last n)) :
                                  Δ[n] _⦋n + 1⦌))))) :
                      (a : X _⦋n⦌) → X _⦋n⦌)
                    x,
                  (ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[1] (Fin.last (n + 1))) :
                      (a : Δ[1] _⦋n + 1⦌) → Δ[1] _⦋n⦌)
                    (stdSimplex.objMk₁ (Fin.last n).castSucc.succ)).2 :
              Δ[1] _⦋n⦌) :
            (a : Fin (n + 1)) → Fin (1 + 1))
          k) :
      ℕ) =
    (↑((((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app ι₀ (op ⦋n⦌)) : (a : X _⦋n⦌) → X _⦋n⦌ ⊗ Δ[1] _⦋n⦌)
                x).2 :
            (a : Fin (n + 1)) → Fin (1 + 1))
          k) :
      ℕ)
Tactic: ext k