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 : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 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,
                stdSimplex.objMk₁ (j.castSucc.castSucc.succ.castPred ⋯)) :
              X _⦋n + 1⦌ × Δ[1] _⦋n + 1⦌).2 :
          (a : Fin (n + 1 + 1)) → Fin (1 + 1))
        k :
      Fin (HAdd.hAdd (α := ℕ) 1 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⦌).2 :
          (a : Fin (n + 1 + 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 : ℕ
i j : Fin (n + 1)
hij : i ≤ j
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
⊢ (↾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⦌)

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
x : X _⦋n⦌
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⦌)
⊢ 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:
simp only [TypeCat.Fun.toFun_apply, types_comp_apply, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
      ← SSet.σ_naturality_apply]

Premises used: TypeCat.Fun.coe_mk, TypeCat.hom_ofHom, TypeCat.Fun.toFun_apply, SSet.σ_naturality_apply, CategoryTheory.types_comp_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
x : X _⦋n⦌
h :
  Eq (α := X _⦋n + 1 + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ j.succ).op) :
          (a : X _⦋n + 1⦌) → X _⦋n + 1 + 1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ i).op) : (a : X _⦋n⦌) → X _⦋n + 1⦌) x :
          X _⦋n + 1⦌) :
      X _⦋n + 1 + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ j.succ).op) :
          (a : X _⦋n + 1⦌) → X _⦋n + 1 + 1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) x : X _⦋n + 1⦌) :
      X _⦋n + 1 + 1⦌)
⊢ 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:
simp [SimplexCategory.σ_comp_σ hij, SSet.yonedaEquiv_symm_app_objEquiv_symm.{u}]

Premises used: SimplexCategory.σ_comp_σ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
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⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ j.succ).op) :
          (a : X _⦋n + 1⦌) → X _⦋n + 1 + 1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ i).op) : (a : X _⦋n⦌) → X _⦋n + 1⦌) x :
          X _⦋n + 1⦌) :
      X _⦋n + 1 + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ j.succ).op) :
          (a : X _⦋n + 1⦌) → X _⦋n + 1 + 1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) x : X _⦋n + 1⦌) :
      X _⦋n + 1 + 1⦌)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
x : X _⦋n⦌
k : Fin (n + 1 + 1 + 1)
⊢ i.castSucc.castSucc < j.castSucc.succ

Tactic:
simpa
-- 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
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.succ))
        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.castSucc) :
                  (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)))
        x
⊢ (↾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.succ =
    σ 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.castSucc) :
            (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)

Tactic:
ext x
-- 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⦌
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.succ) :
              (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.castSucc) :
          (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌) :
      Y _⦋n + 1 + 1⦌)
⊢ 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.succ))
      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.castSucc) :
                (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)))
      x

Tactic:
simp only [TypeCat.Fun.toFun_apply, types_comp_apply, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
      ← SSet.σ_naturality_apply]

Premises used: TypeCat.Fun.coe_mk, TypeCat.hom_ofHom, TypeCat.Fun.toFun_apply, SSet.σ_naturality_apply, CategoryTheory.types_comp_apply
-- 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⦌
h :
  Eq (α := X _⦋n + 1 + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ j.castSucc).op) :
          (a : X _⦋n + 1⦌) → X _⦋n + 1 + 1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ i).op) : (a : X _⦋n⦌) → X _⦋n + 1⦌) x :
          X _⦋n + 1⦌) :
      X _⦋n + 1 + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ j.castSucc).op) :
          (a : X _⦋n + 1⦌) → X _⦋n + 1 + 1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) x : X _⦋n + 1⦌) :
      X _⦋n + 1 + 1⦌)
⊢ 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.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)).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.castSucc) :
              Δ[n + 1] _⦋n + 1 + 1⦌),
          stdSimplex.objMk₁ j.castSucc.castSucc.succ).1 :
      X _⦋n + 1 + 1⦌)

Tactic:
simp [← SimplexCategory.σ_comp_σ hij, SSet.yonedaEquiv_symm_app_objEquiv_symm.{u}]

Premises used: SimplexCategory.σ_comp_σ
-- 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⦌
⊢ Eq (α := X _⦋n + 1 + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ j.castSucc).op) :
          (a : X _⦋n + 1⦌) → X _⦋n + 1 + 1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ i).op) : (a : X _⦋n⦌) → X _⦋n + 1⦌) x :
          X _⦋n + 1⦌) :
      X _⦋n + 1 + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ j.castSucc).op) :
          (a : X _⦋n + 1⦌) → X _⦋n + 1 + 1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) x : X _⦋n + 1⦌) :
      X _⦋n + 1 + 1⦌)

Tactic:
rfl
-- 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)
⊢ j.castSucc.succ ≤ i.succ.castSucc

Tactic:
simpa
-- 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)
⊢ 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))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
S : Truncated 2
x y : OneTruncation₂ S
f g : x ⟶ y
h : f.edge = g.edge
⊢ f = g

Tactic:
Truncated.Edge.ext h

Premises used: SSet.Truncated.Edge.ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
S T : Truncated 2
f : S ⟶ T
x : OneTruncation₂ S
h :
  (Truncated.Edge.map (𝟙rq x) f).edge =
    Truncated.Edge.edge (x₀ :=
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (f.app
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                  Truncated.Edge._proof_1))) :
          (a : (fun (X : Type u_1) ↦ X) (S.obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 }))) →
            (fun (X : Type u_1) ↦ X) (T.obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 })))
        x)
      (x₁ :=
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (f.app
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                  Truncated.Edge._proof_1))) :
          (a : (fun (X : Type u_1) ↦ X) (S.obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 }))) →
            (fun (X : Type u_1) ↦ X) (T.obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 })))
        x)
      (𝟙rq
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (f.app
                (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))) :
            (a : (fun (X : Type u_1) ↦ X) (S.obj (op { obj := ⦋0⦌, property := _proof_1 }))) →
              (fun (X : Type u_1) ↦ X) (T.obj (op { obj := ⦋0⦌, property := _proof_1 })))
          x))
⊢ Truncated.Edge.map (𝟙rq x) f =
    𝟙rq
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))) :
          (a : (fun (X : Type u_1) ↦ X) (S.obj (op { obj := ⦋0⦌, property := _proof_1 }))) →
            (fun (X : Type u_1) ↦ X) (T.obj (op { obj := ⦋0⦌, property := _proof_1 })))
        x)

Tactic:
ext