awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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 (α :=
    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:
simp [ιChainComplex, X']

Premises used: SSet.ιChainComplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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 (α :=
    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:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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
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))
⊢ 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))

Tactic:
dsimp [ιNormalizedChainComplex, ιChainComplex]

Premises used: SSet.ιChainComplex, SSet.ιNormalizedChainComplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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
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)
⊢ 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:
rw [← cancel_mono ((X.fromNormalizedChainComplex R).f n), Category.assoc,
    toNormalizedChainComplex_f_fromNormalizedChainComplex_f]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.Hom.f, SSet.fromNormalizedChainComplex, CategoryTheory.cancel_mono, SSet.toNormalizedChainComplex_f_fromNormalizedChainComplex_f
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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.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:
simp [fromNormalizedChainComplex, SimplicialObject.Splitting.fromNondegComplex_f]

Premises used: SSet.fromNormalizedChainComplex, CategoryTheory.SimplicialObject.Splitting.fromNondegComplex_f
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X Y : SSet
f : X ⟶ Y
R : C
n : ℕ
x_1 : (↑(X.nonDegenerate n) : Type w)
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ Eq.{v + 1} (α := R ⟶ Cocone.pt.{w, v, w, u} (X.cofanNormalizedChainComplex R n))
    (Cofan.inj.{w, v, u} (C := C) (f := fun (x : (↑(X.nonDegenerate n) : Type w)) ↦ R)
          (Cofan.mk (sigmaObj.{w, v, u} fun (x : (↑(X.nonDegenerate n) : Type w)) ↦ R)
            (Sigma.ι fun (x : (↑(X.nonDegenerate n) : Type w)) ↦ R))
          (Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx) ≫
        Iso.hom
          (Iso.refl
            (Cocone.pt.{w, v, w, u} (J := Discrete (↑(X.nonDegenerate n) : Type w)) (F :=
              Discrete.functor fun (x : (↑(X.nonDegenerate n) : Type w)) ↦ R)
              (Cofan.mk (sigmaObj.{w, v, u} fun (x : (↑(X.nonDegenerate n) : Type w)) ↦ R)
                (Sigma.ι fun (x : (↑(X.nonDegenerate n) : Type w)) ↦ R)))) :
      R ⟶ Cocone.pt.{w, v, w, u} (X.cofanNormalizedChainComplex R n))
    (Cofan.inj.{w, v, u} (X.cofanNormalizedChainComplex R n)
        (Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx) :
      R ⟶ Cocone.pt.{w, v, w, u} (X.cofanNormalizedChainComplex R n))

Tactic:
simpa using (X.ιNormalizedChainComplex_eq_ι R n x hx).symm

Premises used: _private.0.SSet.ιNormalizedChainComplex_eq_ι, Eq.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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 : ℕ
T : C
f g : HomologicalComplex.X.{v, u, 0} (X.normalizedChainComplex R) n ⟶ T
h : ∀ x ∈ X.nonDegenerate n, X.ιNormalizedChainComplex x ≫ f = X.ιNormalizedChainComplex x ≫ g
⊢ f = g

Tactic:
(X.isColimitCofanNormalizedChainComplex R n).hom_ext (fun ⟨x, hx⟩ ↦ h x hx)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Limits.colimit, CategoryTheory.Limits.Cocone.ι, CategoryTheory.CategoryStruct.comp, _private.0.SSet.normalizedChainComplex_hom_ext.match_1, SSet.isColimitCofanNormalizedChainComplex, SSet.cofanNormalizedChainComplex, Eq, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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
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
⊢ IsZero.{v, u} (HomologicalComplex.X.{v, u, 0} (X.normalizedChainComplex R) n)

Tactic:
rw [IsZero.iff_id_eq_zero]

Premises used: CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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
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
⊢ 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:
ext x hx
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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
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:
(h.not_gt (X.dim_lt_of_nonDegenerate ⟨x, hx⟩ d)).elim

Premises used: SSet.dim_lt_of_nonDegenerate, False.elim, Subtype.mk, LE.le.not_gt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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
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:
exact (h.not_gt (X.dim_lt_of_nonDegenerate ⟨x, hx⟩ d)).elim

Premises used: SSet.dim_lt_of_nonDegenerate, False.elim, Subtype.mk, LE.le.not_gt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X Y : SSet
f : X ⟶ Y
R : C
⊢ Eq.{v + 1} (α :=
    Quiver.Hom (V := ChainComplex.{v, u, 0} C ℕ) (X.chainComplex R)
      (AlgebraicTopology.AlternatingFaceMapComplex.obj
        (Functor.obj (Functor.obj (sigmaConst ⋙ SimplicialObject.whiskering (Type w) C) R) Y)))
    (chainComplexMap f R ≫ PInfty) (PInfty ≫ chainComplexMap f R)

Tactic:
(natTransPInfty _).naturality _

Premises used: AlgebraicTopology.DoldKan.natTransPInfty, AlgebraicTopology.DoldKan.PInfty, AlgebraicTopology.AlternatingFaceMapComplex.obj, AlgebraicTopology.AlternatingFaceMapComplex.map, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X Y : SSet
f : X ⟶ Y
R : C
⊢ Eq.{v + 1} (α := Quiver.Hom (V := ChainComplex.{v, u, 0} C ℕ) (X.chainComplex R) (Y.normalizedChainComplex R))
    (X.toNormalizedChainComplex R ≫ normalizedChainComplexMap f R) (chainComplexMap f R ≫ Y.toNormalizedChainComplex R)

Tactic:
simp [normalizedChainComplexMap, ← chainComplexMap_PInfty_assoc]

Premises used: SSet.normalizedChainComplexMap, SSet.chainComplexMap_PInfty_assoc
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X Y : SSet
f : X ⟶ Y
R : C
n : ℕ
x : X _⦋n⦌
⊢ Eq.{v + 1} (α := R ⟶ HomologicalComplex.X.{v, u, 0} (Y.normalizedChainComplex R) n)
    (X.ιNormalizedChainComplex x ≫ Hom.f (normalizedChainComplexMap f R) n)
    (Y.ιNormalizedChainComplex
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
          (a : (fun (X : Type w) ↦ X) (X _⦋n⦌)) → (fun (X : Type w) ↦ X) (Y _⦋n⦌))
        x))

Tactic:
simpa only [comp_f, eval_map, ιNormalizedChainComplex,
    ιChainComplex_toNormalizedChainComplex_f_assoc, ι_chainComplexMap_f_assoc] using
    X.ιChainComplex x ≫=
      (eval _ _ n).congr_map (toNormalizedChainComplex_normalizedChainComplexMap f R)

Premises used: SSet.ιChainComplex, HomologicalComplex.eval_map, SSet.ιChainComplex_toNormalizedChainComplex_f_assoc, HomologicalComplex.eval, HomologicalComplex.comp_f, SSet.toNormalizedChainComplex_normalizedChainComplexMap, CategoryTheory.Functor.congr_map, SSet.ι_chainComplexMap_f_assoc, SSet.ιNormalizedChainComplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X Y : SSet
f : X ⟶ Y
R : C
inst_3 : CategoryWithHomology.{v, u} C
⊢ QuasiIso.{v, u, 0} (K := X.chainComplex R) (X.toNormalizedChainComplex R)

Tactic:
(X.homotopyEquivNormalizedChainComplex R).quasiIso_hom

Premises used: CategoryTheory.Functor.comp, HomotopyEquiv.quasiIso_hom, SSet.homotopyEquivNormalizedChainComplex, SSet.toNormalizedChainComplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X Y : SSet
f : X ⟶ Y
R : C
inst_3 : CategoryWithHomology.{v, u} C
⊢ QuasiIso.{v, u, 0} (K := X.normalizedChainComplex R) (X.fromNormalizedChainComplex R)

Tactic:
(X.homotopyEquivNormalizedChainComplex R).quasiIso_inv

Premises used: CategoryTheory.Functor.comp, HomotopyEquiv.quasiIso_inv, SSet.fromNormalizedChainComplex, SSet.homotopyEquivNormalizedChainComplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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
rw : ExactAt.{v, u, 0} (X.normalizedChainComplex R) n
⊢ ExactAt.{v, u, 0} (X.chainComplex R) n

Tactic:
rw [exactAt_iff_of_quasiIsoAt (X.toNormalizedChainComplex R)]

Premises used: exactAt_iff_of_quasiIsoAt, SSet.toNormalizedChainComplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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.normalizedChainComplex R) n

Tactic:
.of_isZero (X.isZero_normalizedChainComplex_X_of_hasDimensionLT R n d)

Premises used: HomologicalComplex.ExactAt.of_isZero, SSet.isZero_normalizedChainComplex_X_of_hasDimensionLT
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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.normalizedChainComplex R) n

Tactic:
exact .of_isZero (X.isZero_normalizedChainComplex_X_of_hasDimensionLT R n d)
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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
rw : ExactAt.{v, u, 0} (X.chainComplex R) n
⊢ IsZero.{v, u} (SSet.homology.{w, v, u} X R n)

Tactic:
rw [← exactAt_iff_isZero_homology]

Premises used: HomologicalComplex.exactAt_iff_isZero_homology
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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

Tactic:
X.exactAt_chainComplex_of_hasDimensionLT R n d

Premises used: SSet.exactAt_chainComplex_of_hasDimensionLT
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
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

Tactic:
exact X.exactAt_chainComplex_of_hasDimensionLT R n d

Premises used: SSet.exactAt_chainComplex_of_hasDimensionLT
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
⊢ ι₀ ≫ H.h = f

Tactic:
RelativeMorphism.Homotopy.h₀ H

Premises used: SSet.RelativeMorphism.Homotopy.h₀
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
⊢ ι₁ ≫ H.h = g

Tactic:
RelativeMorphism.Homotopy.h₁ H

Premises used: SSet.RelativeMorphism.Homotopy.h₁
-- 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))
                      0) :
                  (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)) ≫
            δ Y 0))
        x =
      TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (g.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))
                0) :
            (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)) ≫
      δ Y 0)
    (g.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]) 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⦌)
⊢ 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:
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, TypeCat.Fun.toFun_apply, SSet.Homotopy.h₁, 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] 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⦌)
⊢ 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:
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] 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⦌))
⊢ 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:
apply congr_arg

Premises used: congr_arg