awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homotopy (goal)
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 1)
⊢ Eq (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌)
    ((↾fun (x : X _⦋n + 1⦌) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x ▷ Δ[1] ≫ H.h)
                (op ⦋n + 1 + 1⦌)) :
            (a : (fun (X : Type u) ↦ X) ((Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1 + 1⦌))
          (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                  (a : Fin (n + 1 + 1)) → (↑((Δ[n + 1] ⊗ Δ[1]).nonDegenerate (n + 1 + 1)) : Type u))
                i.succ) :
            (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) ≫
      δ Y i.castSucc.succ)
    ((↾fun (x : X _⦋n + 1⦌) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x ▷ Δ[1] ≫ H.h)
                (op ⦋n + 1 + 1⦌)) :
            (a : (fun (X : Type u) ↦ X) ((Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1 + 1⦌))
          (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                  (a : Fin (n + 1 + 1)) → (↑((Δ[n + 1] ⊗ Δ[1]).nonDegenerate (n + 1 + 1)) : Type u))
                i.castSucc) :
            (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) ≫
      δ Y i.castSucc.succ)
have h : ∀ (x : X _⦋n + 1⦌),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x : X _⦋n + 1⦌) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x ▷ Δ[1] ≫ H.h)
                    (op ⦋n + 1 + 1⦌)) :
                (a : (fun (X : Type u) ↦ X) ((Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1 + 1⦌))
              (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                      (a : Fin (n + 1 + 1)) → (↑((Δ[n + 1] ⊗ Δ[1]).nonDegenerate (n + 1 + 1)) : Type u))
                    i.succ) :
                (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) ≫
          δ Y i.castSucc.succ))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x : X _⦋n + 1⦌) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x ▷ Δ[1] ≫ H.h)
                    (op ⦋n + 1 + 1⦌)) :
                (a : (fun (X : Type u) ↦ X) ((Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1 + 1⦌))
              (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                      (a : Fin (n + 1 + 1)) → (↑((Δ[n + 1] ⊗ Δ[1]).nonDegenerate (n + 1 + 1)) : Type u))
                    i.castSucc) :
                (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) ≫
          δ Y i.castSucc.succ))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homotopy (goal)
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
⊢ (↾fun (x : X _⦋n + 1⦌) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x ▷ Δ[1] ≫ H.h)
                (op ⦋n + 1 + 1⦌)) :
            (a : (fun (X : Type u) ↦ X) ((Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1 + 1⦌))
          (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                  (a : Fin (n + 1 + 1)) → (↑((Δ[n + 1] ⊗ Δ[1]).nonDegenerate (n + 1 + 1)) : Type u))
                j.castSucc) :
            (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) ≫
      δ Y i.succ =
    δ X i ≫
      ↾fun (x : X _⦋n⦌) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x ▷ Δ[1] ≫ H.h) (op ⦋n + 1⦌)) :
            (a : (fun (X : Type u) ↦ X) ((Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1⦌))
          (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                  (a : Fin (n + 1)) → (↑((Δ[n] ⊗ Δ[1]).nonDegenerate (n + 1)) : Type u))
                j) :
            (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)
have h : ∀ (x : X _⦋n + 1⦌),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x : X _⦋n + 1⦌) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x ▷ Δ[1] ≫ H.h)
                    (op ⦋n + 1 + 1⦌)) :
                (a : (fun (X : Type u) ↦ X) ((Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1 + 1⦌))
              (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                      (a : Fin (n + 1 + 1)) → (↑((Δ[n + 1] ⊗ Δ[1]).nonDegenerate (n + 1 + 1)) : Type u))
                    j.castSucc) :
                (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) ≫
          δ Y i.succ))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (δ X i ≫
          ↾fun (x : X _⦋n⦌) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x ▷ Δ[1] ≫ H.h) (op ⦋n + 1⦌)) :
                (a : (fun (X : Type u) ↦ X) ((Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1⦌))
              (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                      (a : Fin (n + 1)) → (↑((Δ[n] ⊗ Δ[1]).nonDegenerate (n + 1)) : Type u))
                    j) :
                (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homotopy (goal)
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
x : X _⦋n + 1⦌
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x : X _⦋n + 1⦌) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x ▷ Δ[1] ≫ H.h)
                    (op ⦋n + 1 + 1⦌)) :
                (a : (fun (X : Type u) ↦ X) ((Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1 + 1⦌))
              (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                      (a : Fin (n + 1 + 1)) → (↑((Δ[n + 1] ⊗ Δ[1]).nonDegenerate (n + 1 + 1)) : Type u))
                    j.castSucc) :
                (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) ≫
          δ Y i.succ))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (δ X i ≫
          ↾fun (x : X _⦋n⦌) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x ▷ Δ[1] ≫ H.h) (op ⦋n + 1⦌)) :
                (a : (fun (X : Type u) ↦ X) ((Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1⦌))
              (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                      (a : Fin (n + 1)) → (↑((Δ[n] ⊗ Δ[1]).nonDegenerate (n + 1)) : Type u))
                    j) :
                (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)))
      x
have h : Eq (α := Y _⦋n + 1⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x ▷ Δ[1] ≫ H.h) (op ⦋n + 1⦌)) :
        (a : (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1⦌) → Y _⦋n + 1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (δ (tensorObj (𝒞 := Functor.category) Δ[n + 1] Δ[1]) i.succ) :
            (a : (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌) → (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1⦌)
          (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                  (a : Fin (n + 1 + 1)) → (↑((Δ[n + 1] ⊗ Δ[1]).nonDegenerate (n + 1 + 1)) : Type u))
                j.castSucc) :
            (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌) :
        tensorObj (𝒞 := Functor.category) Δ[n + 1] Δ[1] _⦋n + 1⦌) :
    Y _⦋n + 1⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (δ X i) : (a : X _⦋n + 1⦌) → X _⦋n⦌) x : X _⦋n⦌) ▷
                Δ[1] ≫
              H.h)
            (op ⦋n + 1⦌)) :
        (a : (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌) → Y _⦋n + 1⦌)
      (↑((prodStdSimplex.nonDegenerateEquiv₁ : (a : Fin (n + 1)) → (↑((Δ[n] ⊗ Δ[1]).nonDegenerate (n + 1)) : Type u))
            j) :
        (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌) :
    Y _⦋n + 1⦌)
Tactic: simp only [TypeCat.Fun.toFun_apply, types_comp_apply, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
      ← SSet.δ_naturality_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homotopy (goal)
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
x : X _⦋n + 1⦌
⊢ Eq (α := X _⦋n + 1⦌ × Δ[1] _⦋n + 1⦌)
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
              (X.map
                (Quiver.Hom.op
                  (((stdSimplex.objEquiv : Δ[n + 1] _⦋n + 1⦌ ≃ (unop (op ⦋n + 1⦌) ⟶ ⦋n + 1⦌)) :
                      (a : Δ[n + 1] _⦋n + 1⦌) → ⦋n + 1⦌ ⟶ ⦋n + 1⦌)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[n + 1] i.succ) :
                        (a : Δ[n + 1] _⦋n + 1 + 1⦌) → Δ[n + 1] _⦋n + 1⦌)
                      ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1 + 1⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n + 1 + 1⦌)
                          (SimplexCategory.σ j.castSucc) :
                        Δ[n + 1] _⦋n + 1 + 1⦌))))) :
            (a : X _⦋n + 1⦌) → X _⦋n + 1⦌)
          x,
        (ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[1] i.succ) : (a : Δ[1] _⦋n + 1 + 1⦌) → Δ[1] _⦋n + 1⦌)
          (stdSimplex.objMk₁ j.castSucc.castSucc.succ)) :
      X _⦋n + 1⦌ × Δ[1] _⦋n + 1⦌)
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (δ X i) : (a : X _⦋n + 1⦌) → X _⦋n⦌) x : X _⦋n⦌))
                (op ⦋n + 1⦌)) :
            (a : Δ[n] _⦋n + 1⦌) → X _⦋n + 1⦌)
          ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n + 1⦌) (SimplexCategory.σ j) :
            Δ[n] _⦋n + 1⦌),
        stdSimplex.objMk₁ j.castSucc.succ) :
      X _⦋n + 1⦌ × Δ[1] _⦋n + 1⦌)
have h : Eq (α := X _⦋n + 1⦌)
  (((ConcreteCategory.hom (FC := TypeCat.Fun)
              (X.map
                (Quiver.Hom.op
                  (((stdSimplex.objEquiv : Δ[n + 1] _⦋n + 1⦌ ≃ (unop (op ⦋n + 1⦌) ⟶ ⦋n + 1⦌)) :
                      (a : Δ[n + 1] _⦋n + 1⦌) → ⦋n + 1⦌ ⟶ ⦋n + 1⦌)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[n + 1] i.succ) :
                        (a : Δ[n + 1] _⦋n + 1 + 1⦌) → Δ[n + 1] _⦋n + 1⦌)
                      ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1 + 1⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n + 1 + 1⦌)
                          (SimplexCategory.σ j.castSucc) :
                        Δ[n + 1] _⦋n + 1 + 1⦌))))) :
            (a : X _⦋n + 1⦌) → X _⦋n + 1⦌)
          x,
        (ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[1] i.succ) : (a : Δ[1] _⦋n + 1 + 1⦌) → Δ[1] _⦋n + 1⦌)
          (stdSimplex.objMk₁ j.castSucc.castSucc.succ)).1 :
    X _⦋n + 1⦌)
  (((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (δ X i) : (a : X _⦋n + 1⦌) → X _⦋n⦌) x : X _⦋n⦌))
                (op ⦋n + 1⦌)) :
            (a : Δ[n] _⦋n + 1⦌) → X _⦋n + 1⦌)
          ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n + 1⦌) (SimplexCategory.σ j) :
            Δ[n] _⦋n + 1⦌),
        stdSimplex.objMk₁ j.castSucc.succ).1 :
    X _⦋n + 1⦌)
Tactic: ext k : 2
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homotopy (goal)
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
x : X _⦋n + 1⦌
⊢ Eq (α := X _⦋n + 1⦌)
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
                (X.map
                  (Quiver.Hom.op
                    (((stdSimplex.objEquiv : Δ[n + 1] _⦋n + 1⦌ ≃ (unop (op ⦋n + 1⦌) ⟶ ⦋n + 1⦌)) :
                        (a : Δ[n + 1] _⦋n + 1⦌) → ⦋n + 1⦌ ⟶ ⦋n + 1⦌)
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[n + 1] i.succ) :
                          (a : Δ[n + 1] _⦋n + 1 + 1⦌) → Δ[n + 1] _⦋n + 1⦌)
                        ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1 + 1⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n + 1 + 1⦌)
                            (SimplexCategory.σ j.castSucc) :
                          Δ[n + 1] _⦋n + 1 + 1⦌))))) :
              (a : X _⦋n + 1⦌) → X _⦋n + 1⦌)
            x,
          (ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[1] i.succ) : (a : Δ[1] _⦋n + 1 + 1⦌) → Δ[1] _⦋n + 1⦌)
            (stdSimplex.objMk₁ j.castSucc.castSucc.succ)).1 :
      X _⦋n + 1⦌)
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app
                  ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (δ X i) : (a : X _⦋n + 1⦌) → X _⦋n⦌) x : X _⦋n⦌))
                  (op ⦋n + 1⦌)) :
              (a : Δ[n] _⦋n + 1⦌) → X _⦋n + 1⦌)
            ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n + 1⦌) (SimplexCategory.σ j) :
              Δ[n] _⦋n + 1⦌),
          stdSimplex.objMk₁ j.castSucc.succ).1 :
      X _⦋n + 1⦌)
have h : Eq (α := X _⦋n + 1⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ j).op) : (a : X _⦋n⦌) → X _⦋n + 1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.δ i).op) : (a : X _⦋n + 1⦌) → X _⦋n⦌) x :
        X _⦋n⦌) :
    X _⦋n + 1⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ j).op) : (a : X _⦋n⦌) → X _⦋n + 1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (δ X i) : (a : X _⦋n + 1⦌) → X _⦋n⦌) x : X _⦋n⦌) :
    X _⦋n + 1⦌)
Tactic: simp [SimplexCategory.δ_comp_σ_of_gt hij, SSet.yonedaEquiv_symm_app_objEquiv_symm.{u}]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homotopy (goal)
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
⊢ (↾fun (x : X _⦋n⦌) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x ▷ Δ[1] ≫ H.h) (op ⦋n + 1⦌)) :
            (a : (fun (X : Type u) ↦ X) ((Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1⦌))
          (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                  (a : Fin (n + 1)) → (↑((Δ[n] ⊗ Δ[1]).nonDegenerate (n + 1)) : Type u))
                j) :
            (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)) ≫
      σ Y i.castSucc =
    σ X i ≫
      ↾fun (x : X _⦋n + 1⦌) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x ▷ Δ[1] ≫ H.h)
                (op ⦋n + 1 + 1⦌)) :
            (a : (fun (X : Type u) ↦ X) ((Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1 + 1⦌))
          (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                  (a : Fin (n + 1 + 1)) → (↑((Δ[n + 1] ⊗ Δ[1]).nonDegenerate (n + 1 + 1)) : Type u))
                j.succ) :
            (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)
have h : ∀ (x : X _⦋n⦌),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x : X _⦋n⦌) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x ▷ Δ[1] ≫ H.h) (op ⦋n + 1⦌)) :
                (a : (fun (X : Type u) ↦ X) ((Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1⦌))
              (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                      (a : Fin (n + 1)) → (↑((Δ[n] ⊗ Δ[1]).nonDegenerate (n + 1)) : Type u))
                    j) :
                (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)) ≫
          σ Y i.castSucc))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (σ X i ≫
          ↾fun (x : X _⦋n + 1⦌) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x ▷ Δ[1] ≫ H.h)
                    (op ⦋n + 1 + 1⦌)) :
                (a : (fun (X : Type u) ↦ X) ((Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1 + 1⦌))
              (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                      (a : Fin (n + 1 + 1)) → (↑((Δ[n + 1] ⊗ Δ[1]).nonDegenerate (n + 1 + 1)) : Type u))
                    j.succ) :
                (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homotopy (goal)
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
x : X _⦋n⦌
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x : X _⦋n⦌) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x ▷ Δ[1] ≫ H.h) (op ⦋n + 1⦌)) :
                (a : (fun (X : Type u) ↦ X) ((Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1⦌))
              (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                      (a : Fin (n + 1)) → (↑((Δ[n] ⊗ Δ[1]).nonDegenerate (n + 1)) : Type u))
                    j) :
                (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)) ≫
          σ Y i.castSucc))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (σ X i ≫
          ↾fun (x : X _⦋n + 1⦌) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x ▷ Δ[1] ≫ H.h)
                    (op ⦋n + 1 + 1⦌)) :
                (a : (fun (X : Type u) ↦ X) ((Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1 + 1⦌))
              (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                      (a : Fin (n + 1 + 1)) → (↑((Δ[n + 1] ⊗ Δ[1]).nonDegenerate (n + 1 + 1)) : Type u))
                    j.succ) :
                (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)))
      x
have h : Eq (α := Y _⦋n + 1 + 1⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x ▷ Δ[1] ≫ H.h) (op ⦋n + 1 + 1⦌)) :
        (a : (Δ[n] ⊗ Δ[1]) _⦋n + 1 + 1⦌) → Y _⦋n + 1 + 1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ (tensorObj (𝒞 := Functor.category) Δ[n] Δ[1]) i.castSucc) :
            (a : (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌) → (Δ[n] ⊗ Δ[1]) _⦋n + 1 + 1⦌)
          (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                  (a : Fin (n + 1)) → (↑((Δ[n] ⊗ Δ[1]).nonDegenerate (n + 1)) : Type u))
                j) :
            (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌) :
        tensorObj (𝒞 := Functor.category) Δ[n] Δ[1] _⦋n + 1 + 1⦌) :
    Y _⦋n + 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⦌) ▷
                Δ[1] ≫
              H.h)
            (op ⦋n + 1 + 1⦌)) :
        (a : (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌) → Y _⦋n + 1 + 1⦌)
      (↑((prodStdSimplex.nonDegenerateEquiv₁ :
              (a : Fin (n + 1 + 1)) → (↑((Δ[n + 1] ⊗ Δ[1]).nonDegenerate (n + 1 + 1)) : Type u))
            j.succ) :
        (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌) :
    Y _⦋n + 1 + 1⦌)
Tactic: simp only [TypeCat.Fun.toFun_apply, types_comp_apply, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
      ← SSet.σ_naturality_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homotopy (goal)
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
x : X _⦋n⦌
⊢ Eq (α := X _⦋n + 1 + 1⦌ × Δ[1] _⦋n + 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.castSucc) : (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.castSucc) : (a : Δ[1] _⦋n + 1⦌) → Δ[1] _⦋n + 1 + 1⦌)
          (stdSimplex.objMk₁ j.castSucc.succ)) :
      X _⦋n + 1 + 1⦌ × Δ[1] _⦋n + 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.succ) :
            Δ[n + 1] _⦋n + 1 + 1⦌),
        stdSimplex.objMk₁ j.castSucc.succ.succ) :
      X _⦋n + 1 + 1⦌ × Δ[1] _⦋n + 1 + 1⦌)
have h : Eq (α := X _⦋n + 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.castSucc) : (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.castSucc) : (a : Δ[1] _⦋n + 1⦌) → Δ[1] _⦋n + 1 + 1⦌)
          (stdSimplex.objMk₁ j.castSucc.succ)).1 :
    X _⦋n + 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.succ) :
            Δ[n + 1] _⦋n + 1 + 1⦌),
        stdSimplex.objMk₁ j.castSucc.succ.succ).1 :
    X _⦋n + 1 + 1⦌)
Tactic: ext k : 2