awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
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] 0) : (a : Δ[n] _⦋n + 1⦌) → Δ[n] _⦋n⦌)
                        ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n + 1⦌) (SimplexCategory.σ 0) :
                          Δ[n] _⦋n + 1⦌))))) :
              (a : X _⦋n⦌) → X _⦋n⦌)
            x,
          (ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[1] 0) : (a : Δ[1] _⦋n + 1⦌) → Δ[1] _⦋n⦌)
            (stdSimplex.objMk₁ 1)).1 :
      X _⦋n⦌)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app ι₁ (op ⦋n⦌)) : (a : X _⦋n⦌) → X _⦋n⦌ ⊗ Δ[1] _⦋n⦌) x).1 :
      X _⦋n⦌)
h₁ :
  ∀ (k : Fin (n + 1)),
    Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 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] 0) : (a : Δ[n] _⦋n + 1⦌) → Δ[n] _⦋n⦌)
                                ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n + 1⦌)
                                    (SimplexCategory.σ 0) :
                                  Δ[n] _⦋n + 1⦌))))) :
                      (a : X _⦋n⦌) → X _⦋n⦌)
                    x,
                  (ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[1] 0) : (a : Δ[1] _⦋n + 1⦌) → Δ[1] _⦋n⦌)
                    (stdSimplex.objMk₁ 1)).2 :
              Δ[1] _⦋n⦌) :
            (a : Fin (n + 1)) → Fin (1 + 1))
          k :
        Fin (HAdd.hAdd (α := ℕ) 1 1))
      ((((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 :
        Fin (HAdd.hAdd (α := ℕ) 1 1))
⊢ 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] 0) : (a : Δ[n] _⦋n + 1⦌) → Δ[n] _⦋n⦌)
                      ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n + 1⦌) (SimplexCategory.σ 0) :
                        Δ[n] _⦋n + 1⦌))))) :
            (a : X _⦋n⦌) → X _⦋n⦌)
          x,
        (ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[1] 0) : (a : Δ[1] _⦋n + 1⦌) → Δ[1] _⦋n⦌) (stdSimplex.objMk₁ 1)) :
      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⦌))

Tactic:
ext k : 2
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
⊢ 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] 0) : (a : Δ[n] _⦋n + 1⦌) → Δ[n] _⦋n⦌)
                        ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n + 1⦌) (SimplexCategory.σ 0) :
                          Δ[n] _⦋n + 1⦌))))) :
              (a : X _⦋n⦌) → X _⦋n⦌)
            x,
          (ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[1] 0) : (a : Δ[1] _⦋n + 1⦌) → Δ[1] _⦋n⦌)
            (stdSimplex.objMk₁ 1)).1 :
      X _⦋n⦌)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app ι₁ (op ⦋n⦌)) : (a : X _⦋n⦌) → X _⦋n⦌ ⊗ Δ[1] _⦋n⦌) x).1 :
      X _⦋n⦌)

Tactic:
simp [dsimp% SimplexCategory.δ_comp_σ_self (i := (0 : Fin (n + 1)))]

Premises used: SimplexCategory.δ_comp_σ_self
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
k : Fin (n + 1)
⊢ LT.lt (α := Fin (n + 2 + 1)) (Fin.castSucc 0) 1

Tactic:
tauto
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
k : Fin (n + 1)
h :
  Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 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] 0) : (a : Δ[n] _⦋n + 1⦌) → Δ[n] _⦋n⦌)
                              ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n + 1⦌)
                                  (SimplexCategory.σ 0) :
                                Δ[n] _⦋n + 1⦌))))) :
                    (a : X _⦋n⦌) → X _⦋n⦌)
                  x,
                stdSimplex.objMk₁ (Fin.pred 1 ⋯)) :
              X _⦋n⦌ × Δ[1] _⦋n⦌).2 :
          (a : Fin (n + 1)) → Fin (1 + 1))
        k :
      Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((((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 :
      Fin (HAdd.hAdd (α := ℕ) 1 1))
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 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] 0) : (a : Δ[n] _⦋n + 1⦌) → Δ[n] _⦋n⦌)
                              ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n + 1⦌)
                                  (SimplexCategory.σ 0) :
                                Δ[n] _⦋n + 1⦌))))) :
                    (a : X _⦋n⦌) → X _⦋n⦌)
                  x,
                (ConcreteCategory.hom (FC := TypeCat.Fun) (δ Δ[1] 0) : (a : Δ[1] _⦋n + 1⦌) → Δ[1] _⦋n⦌)
                  (stdSimplex.objMk₁ 1)).2 :
            Δ[1] _⦋n⦌) :
          (a : Fin (n + 1)) → Fin (1 + 1))
        k :
      Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((((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 :
      Fin (HAdd.hAdd (α := ℕ) 1 1))

Tactic:
rw [stdSimplex.δ_objMk₁_of_lt _ _ (by tauto)]

Premises used: SSet.stdSimplex.δ_objMk₁_of_lt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
k : Fin (n + 1)
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 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] 0) : (a : Δ[n] _⦋n + 1⦌) → Δ[n] _⦋n⦌)
                              ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n + 1⦌)
                                  (SimplexCategory.σ 0) :
                                Δ[n] _⦋n + 1⦌))))) :
                    (a : X _⦋n⦌) → X _⦋n⦌)
                  x,
                stdSimplex.objMk₁ (Fin.pred 1 ⋯)) :
              X _⦋n⦌ × Δ[1] _⦋n⦌).2 :
          (a : Fin (n + 1)) → Fin (1 + 1))
        k :
      Fin (HAdd.hAdd (α := ℕ) 1 1))
    ((((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 :
      Fin (HAdd.hAdd (α := ℕ) 1 1))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
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))
                      (Fin.last n)) :
                  (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)) ≫
            δ Y (Fin.last (n + 1))))
        x =
      TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌))) x
⊢ Eq (α := X _⦋n⦌ ⟶ Y _⦋n⦌)
    ((↾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))
                (Fin.last n)) :
            (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)) ≫
      δ Y (Fin.last (n + 1)))
    (f.app (op ⦋n⦌))

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
h :
  Eq (α := Y _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x ▷ Δ[1] ≫ H.h) (op ⦋n⦌)) :
          (a : (Δ[n] ⊗ Δ[1]) _⦋n⦌) → Y _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (δ (tensorObj (𝒞 := Functor.category) Δ[n] Δ[1]) (Fin.last (n + 1))) :
              (a : (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌) → (Δ[n] ⊗ Δ[1]) _⦋n⦌)
            (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                    (a : Fin (n + 1)) → (↑((Δ[n] ⊗ Δ[1]).nonDegenerate (n + 1)) : Type u))
                  (Fin.last n)) :
              (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌) :
          tensorObj (𝒞 := Functor.category) Δ[n] Δ[1] _⦋n⦌) :
      Y _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((ι₀ ≫ H.h).app (op ⦋n⦌)) : (a : X _⦋n⦌) → Y _⦋n⦌) x : Y _⦋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))
                    (Fin.last n)) :
                (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)) ≫
          δ Y (Fin.last (n + 1))))
      x =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌))) x

Tactic:
simp only [TypeCat.Fun.toFun_apply, types_comp_apply, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
      ← SSet.δ_naturality_apply, ← H.h₀]

Premises used: SSet.δ_naturality_apply, TypeCat.Fun.coe_mk, TypeCat.hom_ofHom, SSet.Homotopy.h₀, TypeCat.Fun.toFun_apply, CategoryTheory.types_comp_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
h :
  Eq (α := Y _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (H.h.app (op ⦋n⦌)) : (a : X _⦋n⦌ ⊗ Δ[1] _⦋n⦌) → Y _⦋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⦌) :
      Y _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (H.h.app (op ⦋n⦌)) : (a : X _⦋n⦌ ⊗ Δ[1] _⦋n⦌) → Y _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app ι₀ (op ⦋n⦌)) : (a : X _⦋n⦌) → X _⦋n⦌ ⊗ Δ[1] _⦋n⦌) x :
          tensorObj (𝒞 := types) (X _⦋n⦌) (Δ[1] _⦋n⦌)) :
      Y _⦋n⦌)
⊢ Eq (α := Y _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x ▷ Δ[1] ≫ H.h) (op ⦋n⦌)) :
          (a : (Δ[n] ⊗ Δ[1]) _⦋n⦌) → Y _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (δ (tensorObj (𝒞 := Functor.category) Δ[n] Δ[1]) (Fin.last (n + 1))) :
              (a : (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌) → (Δ[n] ⊗ Δ[1]) _⦋n⦌)
            (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                    (a : Fin (n + 1)) → (↑((Δ[n] ⊗ Δ[1]).nonDegenerate (n + 1)) : Type u))
                  (Fin.last n)) :
              (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌) :
          tensorObj (𝒞 := Functor.category) Δ[n] Δ[1] _⦋n⦌) :
      Y _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((ι₀ ≫ H.h).app (op ⦋n⦌)) : (a : X _⦋n⦌) → Y _⦋n⦌) x : Y _⦋n⦌)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
h :
  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⦌))
⊢ Eq (α := Y _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (H.h.app (op ⦋n⦌)) : (a : X _⦋n⦌ ⊗ Δ[1] _⦋n⦌) → Y _⦋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⦌) :
      Y _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (H.h.app (op ⦋n⦌)) : (a : X _⦋n⦌ ⊗ Δ[1] _⦋n⦌) → Y _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app ι₀ (op ⦋n⦌)) : (a : X _⦋n⦌) → X _⦋n⦌ ⊗ Δ[1] _⦋n⦌) x :
          tensorObj (𝒞 := types) (X _⦋n⦌) (Δ[1] _⦋n⦌)) :
      Y _⦋n⦌)

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
⊢ 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⦌)

Tactic:
simp [dsimp% SimplexCategory.δ_comp_σ_succ (i := Fin.last n)]

Premises used: SimplexCategory.δ_comp_σ_succ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
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:
simp [stdSimplex.δ_objMk₁_of_le, stdSimplex.objMk₁_apply_eq_zero_iff, ← Fin.castSucc_succ]

Premises used: Fin.castSucc_succ, SSet.stdSimplex.δ_objMk₁_of_le, SSet.stdSimplex.objMk₁_apply_eq_zero_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
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.succ) :
                  (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) ≫
            δ Y i.castSucc))
        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
⊢ (↾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⦌)) ≫
      δ Y i.castSucc =
    δ 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⦌)

Tactic:
ext x