-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
x : X _⦋n⦌
k : Fin (n + 1 + 1 + 1)
h :
  Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 1))
    (((((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x) (op ⦋n + 1 + 1⦌)) :
                    (a : Δ[n] _⦋n + 1 + 1⦌) → X _⦋n + 1 + 1⦌)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ Δ[n] i.succ) : (a : Δ[n] _⦋n + 1⦌) → Δ[n] _⦋n + 1 + 1⦌)
                      ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n + 1⦌) (SimplexCategory.σ j) :
                        Δ[n] _⦋n + 1⦌) :
                    Δ[n] _⦋n + 1 + 1⦌),
                stdSimplex.objMk₁ j.castSucc.succ.castSucc) :
              X _⦋n + 1 + 1⦌ × Δ[1] _⦋n + 1 + 1⦌).2 :
          (a : Fin (n + 1 + 1 + 1)) → Fin (1 + 1))
        k :
      Fin (HAdd.hAdd (α := ℕ) 1 1))
    (((((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (NatTrans.app
                        ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X)
                          ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) x :
                            X _⦋n + 1⦌))
                        (op ⦋n + 1 + 1⦌)) :
                    (a : Δ[n + 1] _⦋n + 1 + 1⦌) → X _⦋n + 1 + 1⦌)
                  ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1 + 1⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n + 1 + 1⦌)
                      (SimplexCategory.σ j.castSucc) :
                    Δ[n + 1] _⦋n + 1 + 1⦌),
                stdSimplex.objMk₁ j.castSucc.castSucc.succ) :
              X _⦋n + 1 + 1⦌ × Δ[1] _⦋n + 1 + 1⦌).2 :
          (a : Fin (n + 1 + 1 + 1)) → Fin (1 + 1))
        k :
      Fin (HAdd.hAdd (α := ℕ) 1 1))
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 1))
    (((((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x) (op ⦋n + 1 + 1⦌)) :
                    (a : Δ[n] _⦋n + 1 + 1⦌) → X _⦋n + 1 + 1⦌)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ Δ[n] i.succ) : (a : Δ[n] _⦋n + 1⦌) → Δ[n] _⦋n + 1 + 1⦌)
                      ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n + 1⦌) (SimplexCategory.σ j) :
                        Δ[n] _⦋n + 1⦌) :
                    Δ[n] _⦋n + 1 + 1⦌),
                (ConcreteCategory.hom (FC := TypeCat.Fun) (σ Δ[1] i.succ) : (a : Δ[1] _⦋n + 1⦌) → Δ[1] _⦋n + 1 + 1⦌)
                  (stdSimplex.objMk₁ j.castSucc.succ)).2 :
            Δ[1] _⦋n + 1 + 1⦌) :
          (a : Fin (n + 1 + 1 + 1)) → Fin (1 + 1))
        k :
      Fin (HAdd.hAdd (α := ℕ) 1 1))
    (((((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (NatTrans.app
                        ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X)
                          ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) x :
                            X _⦋n + 1⦌))
                        (op ⦋n + 1 + 1⦌)) :
                    (a : Δ[n + 1] _⦋n + 1 + 1⦌) → X _⦋n + 1 + 1⦌)
                  ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1 + 1⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n + 1 + 1⦌)
                      (SimplexCategory.σ j.castSucc) :
                    Δ[n + 1] _⦋n + 1 + 1⦌),
                stdSimplex.objMk₁ j.castSucc.castSucc.succ) :
              X _⦋n + 1 + 1⦌ × Δ[1] _⦋n + 1 + 1⦌).2 :
          (a : Fin (n + 1 + 1 + 1)) → Fin (1 + 1))
        k :
      Fin (HAdd.hAdd (α := ℕ) 1 1))

Tactic:
rw [stdSimplex.σ_objMk₁_of_le _ _ (by simpa)]

Premises used: SSet.stdSimplex.σ_objMk₁_of_le