awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
n : ℕ
x : X _⦋n + 1⦌
hx : Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.degenerate (n + 1)) x
⊢ Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) (n + 1))
    (X.ιChainComplex x ≫ Hom.f PInfty (n + 1)) 0
have hx₁ : ∃ (i : Fin (n + 1)) (y : X _⦋n⦌),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y = x
Tactic: simp only [degenerate_eq_iUnion_range_σ, Set.mem_iUnion, Set.mem_range] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
n : ℕ
x : X _⦋n + 1⦌
hx :
  ∃ (i : Fin (n + 1)) (y : X _⦋n⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y = x
X' : SimplicialObject.{v, u} C :=
  Functor.obj (Functor.obj (SimplicialObject.whiskering (Type w) C) (Functor.obj sigmaConst R)) X
⊢ Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) (n + 1))
    (X.ιChainComplex x ≫ Hom.f PInfty (n + 1)) 0
have succ : ∀ (i : Fin (n + 1)) (y : X _⦋n⦌),
  Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) (n + 1))
    (X.ιChainComplex
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y) ≫
      Hom.f PInfty (n + 1))
    0
Tactic: obtain ⟨i, y, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
n : ℕ
X' : SimplicialObject.{v, u} C :=
  Functor.obj (Functor.obj (SimplicialObject.whiskering (Type w) C) (Functor.obj sigmaConst R)) X
i : Fin (n + 1)
y : X _⦋n⦌
⊢ Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) (n + 1))
    (X.ιChainComplex
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y) ≫
      Hom.f PInfty (n + 1))
    0
have trans : Eq (α :=
  R ⟶
    HomologicalComplex.X.{v, u, 0}
      (AlgebraicTopology.AlternatingFaceMapComplex.obj
        (Functor.obj (Functor.obj (sigmaConst ⋙ SimplicialObject.whiskering (Type w) C) R) X))
      (n + 1))
  (X.ιChainComplex ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y) ≫
    Hom.f PInfty (n + 1))
  (X.ιChainComplex y ≫ X'.σ i ≫ Hom.f PInfty (n + 1))
Tactic: trans X.ιChainComplex y ≫ X'.σ i ≫ (PInfty (X := X')).f _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
n : ℕ
X' : SimplicialObject.{v, u} C :=
  Functor.obj (Functor.obj (SimplicialObject.whiskering (Type w) C) (Functor.obj sigmaConst R)) X
i : Fin (n + 1)
y : X _⦋n⦌
trans :
  Eq (α :=
    R ⟶
      HomologicalComplex.X.{v, u, 0}
        (AlgebraicTopology.AlternatingFaceMapComplex.obj
          (Functor.obj (Functor.obj (sigmaConst ⋙ SimplicialObject.whiskering (Type w) C) R) X))
        (n + 1))
    (X.ιChainComplex
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y) ≫
      Hom.f PInfty (n + 1))
    (X.ιChainComplex y ≫ X'.σ i ≫ Hom.f PInfty (n + 1))
⊢ Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) (n + 1))
    (X.ιChainComplex
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y) ≫
      Hom.f PInfty (n + 1))
    0
have trans₁ : Eq (α :=
  R ⟶
    HomologicalComplex.X.{v, u, 0}
      (AlgebraicTopology.AlternatingFaceMapComplex.obj
        (Functor.obj (Functor.obj (sigmaConst ⋙ SimplicialObject.whiskering (Type w) C) R) X))
      (n + 1))
  (X.ιChainComplex y ≫ X'.σ i ≫ Hom.f PInfty (n + 1)) 0
Tactic: trans X.ιChainComplex y ≫ X'.σ i ≫ (PInfty (X := X')).f _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.normalizedChainComplex R) n) (X.ιNormalizedChainComplex x)
    (Sigma.ι.{w, v, u} (C := C) (fun (x : (↑(X.nonDegenerate n) : Type w)) ↦ R)
      (Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx))
have dsimp : Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.normalizedChainComplex R) n)
  (Sigma.ι.{w, v, u} (C := C) (fun (x : X _⦋n⦌) ↦ R) x ≫ Hom.f (X.toNormalizedChainComplex R) n)
  (Sigma.ι.{w, v, u} (C := C) (fun (x : (↑(X.nonDegenerate n) : Type w)) ↦ R)
    (Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx))
Tactic: dsimp [ιNormalizedChainComplex, ιChainComplex]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.normalizedChainComplex R) n)
    (Sigma.ι.{w, v, u} (C := C) (fun (x : X _⦋n⦌) ↦ R) x ≫ Hom.f (X.toNormalizedChainComplex R) n)
    (Sigma.ι.{w, v, u} (C := C) (fun (x : (↑(X.nonDegenerate n) : Type w)) ↦ R)
      (Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx))
have rw : Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n)
  (Sigma.ι.{w, v, u} (C := C) (fun (x : X _⦋n⦌) ↦ R) x ≫ Hom.f PInfty n :
    R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n)
  (Sigma.ι.{w, v, u} (C := C) (fun (x : (↑(X.nonDegenerate n) : Type w)) ↦ R)
        (Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx) ≫
      Hom.f (X.fromNormalizedChainComplex R) n :
    R ⟶ HomologicalComplex.X.{v, u, 0} (X.chainComplex R) n)
Tactic: rw [← cancel_mono ((X.fromNormalizedChainComplex R).f n), Category.assoc,
    toNormalizedChainComplex_f_fromNormalizedChainComplex_f]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
n d : ℕ
inst_3 : X.HasDimensionLT d
h : d ≤ n
⊢ IsZero.{v, u} (HomologicalComplex.X.{v, u, 0} (X.normalizedChainComplex R) n)
have rw : Eq.{v + 1} (α :=
  HomologicalComplex.X.{v, u, 0} (X.normalizedChainComplex R) n ⟶
    HomologicalComplex.X.{v, u, 0} (X.normalizedChainComplex R) n)
  (𝟙 (HomologicalComplex.X.{v, u, 0} (X.normalizedChainComplex R) n)) 0
Tactic: rw [IsZero.iff_id_eq_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
n d : ℕ
inst_3 : X.HasDimensionLT d
h : d ≤ n
⊢ Eq.{v + 1} (α :=
    HomologicalComplex.X.{v, u, 0} (X.normalizedChainComplex R) n ⟶
      HomologicalComplex.X.{v, u, 0} (X.normalizedChainComplex R) n)
    (𝟙 (HomologicalComplex.X.{v, u, 0} (X.normalizedChainComplex R) n)) 0
have h₁ : ∀ (x : X _⦋n⦌) (hx : x ∈ X.nonDegenerate n),
  X.ιNormalizedChainComplex x ≫ 𝟙 (HomologicalComplex.X.{v, u, 0} (X.normalizedChainComplex R) n) =
    CategoryStruct.comp (Y := HomologicalComplex.X.{v, u, 0} (X.normalizedChainComplex R) n)
      (X.ιNormalizedChainComplex x) 0
Tactic: ext x hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
inst_3 : CategoryWithHomology.{v, u} C
n d : ℕ
inst_4 : X.HasDimensionLT d
h : d ≤ n
⊢ ExactAt.{v, u, 0} (X.chainComplex R) n
have rw : ExactAt.{v, u, 0} (X.normalizedChainComplex R) n
Tactic: rw [exactAt_iff_of_quasiIsoAt (X.toNormalizedChainComplex R)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
inst_3 : CategoryWithHomology.{v, u} C
n d : ℕ
inst_4 : X.HasDimensionLT d
h : d ≤ n
⊢ IsZero.{v, u} (SSet.homology.{w, v, u} X R n)
have rw : ExactAt.{v, u, 0} (X.chainComplex R) n
Tactic: rw [← exactAt_iff_isZero_homology]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homotopy (goal)
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
⊢ 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))
                0) :
            (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)) ≫
      δ Y 0)
    (g.app (op ⦋n⦌))
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))
                    0) :
                (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)) ≫
          δ Y 0))
      x =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app (op ⦋n⦌))) 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 : ℕ
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))
                    0) :
                (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)) ≫
          δ Y 0))
      x =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app (op ⦋n⦌))) x
have 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]) 0) :
            (a : (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌) → (Δ[n] ⊗ Δ[1]) _⦋n⦌)
          (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                  (a : Fin (n + 1)) → (↑((Δ[n] ⊗ Δ[1]).nonDegenerate (n + 1)) : Type u))
                0) :
            (Δ[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: simp only [TypeCat.Fun.toFun_apply, types_comp_apply, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
      ← SSet.δ_naturality_apply, ← H.h₁]
-- 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⦌
⊢ 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]) 0) :
              (a : (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌) → (Δ[n] ⊗ Δ[1]) _⦋n⦌)
            (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                    (a : Fin (n + 1)) → (↑((Δ[n] ⊗ Δ[1]).nonDegenerate (n + 1)) : Type u))
                  0) :
              (Δ[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⦌)
have 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] 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⦌) :
    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: dsimp
-- 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⦌
⊢ 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] 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⦌) :
      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⦌)
have 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] 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: apply congr_arg
-- 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⦌
⊢ 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⦌))
have 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⦌)
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 : ℕ
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⦌)
⊢ 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⦌))
have 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))
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 : ℕ
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,
                (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))
have 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 sorry)) :
            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: rw [stdSimplex.δ_objMk₁_of_lt _ _ (by tauto)]