awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y : Split.{v_1, u_1} C
Φ : X ⟶ Y
n : ℕ
h :
  Eq (α := X.s.N n ⟶ Y.X _⦋n⦌)
    (Φ.f n ≫
      CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (Y.s.cofan (op ⦋n⦌)))
        (Cofan.inj (Y.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
          Splitting.summand Y.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (Y.s.cofan (op ⦋n⦌)))
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[Y.X] n ⟶ HomologicalComplex.X K[Y.X] n))
    (CategoryStruct.comp (Y := X.X _⦋n⦌)
      (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
          (Cofan.inj (X.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
            Splitting.summand X.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
              Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
          (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X.X] n ⟶ HomologicalComplex.X K[X.X] n) :
        X.s.N n ⟶ X.X _⦋n⦌)
      (CategoryStruct.comp (Y := X.X _⦋n⦌)
          (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X.X] n ⟶ HomologicalComplex.X K[X.X] n)
          (Φ.F.app (op ⦋n⦌)) :
        X.X _⦋n⦌ ⟶ Y.X _⦋n⦌))
⊢ Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj (nondegComplexFunctor ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) X))
        n ⟶
      HomologicalComplex.X (Karoubi.X (Functor.obj (forget C ⋙ N₁) Y)) n)
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f
        (Functor.map (nondegComplexFunctor ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Φ ≫
          Iso.hom
            ((fun (S : Split.{v_1, u_1} C) ↦
                (S.s.toKaroubiNondegComplexIsoN₁ :
                  Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
                    (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) S.s.nondegComplex) (Functor.obj N₁ S.X)))
              Y)))
      n)
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f
        (Iso.hom
            ((fun (S : Split.{v_1, u_1} C) ↦
                (S.s.toKaroubiNondegComplexIsoN₁ :
                  Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
                    (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) S.s.nondegComplex) (Functor.obj N₁ S.X)))
              X) ≫
          Functor.map (forget C ⋙ N₁) Φ))
      n)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y : Split.{v_1, u_1} C
Φ : X ⟶ Y
n : ℕ
h :
  Eq (α := X.s.N n ⟶ Y.X _⦋n⦌)
    (Φ.f n ≫
      CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (Y.s.cofan (op ⦋n⦌)))
        (Cofan.inj (Y.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
          Splitting.summand Y.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (Y.s.cofan (op ⦋n⦌)))
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[Y.X] n ⟶ HomologicalComplex.X K[Y.X] n))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
      (Cofan.inj (X.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
        Splitting.summand X.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n ≫ Φ.F.app (op ⦋n⦌) : HomologicalComplex.X K[X.X] n ⟶ Y.X _⦋n⦌))
⊢ Eq (α := X.s.N n ⟶ Y.X _⦋n⦌)
    (Φ.f n ≫
      CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (Y.s.cofan (op ⦋n⦌)))
        (Cofan.inj (Y.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
          Splitting.summand Y.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (Y.s.cofan (op ⦋n⦌)))
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[Y.X] n ⟶ HomologicalComplex.X K[Y.X] n))
    (CategoryStruct.comp (Y := X.X _⦋n⦌)
      (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
          (Cofan.inj (X.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
            Splitting.summand X.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
              Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
          (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X.X] n ⟶ HomologicalComplex.X K[X.X] n) :
        X.s.N n ⟶ X.X _⦋n⦌)
      (CategoryStruct.comp (Y := X.X _⦋n⦌)
          (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X.X] n ⟶ HomologicalComplex.X K[X.X] n)
          (Φ.F.app (op ⦋n⦌)) :
        X.X _⦋n⦌ ⟶ Y.X _⦋n⦌))

Tactic:
simp only [assoc, PInfty_f_idem_assoc]

Premises used: CategoryTheory.Category.assoc, AlgebraicTopology.DoldKan.PInfty_f_idem_assoc
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y : Split.{v_1, u_1} C
Φ : X ⟶ Y
n : ℕ
h :
  Eq (α := X.s.N n ⟶ Y.X _⦋n⦌)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
        (Cofan.inj (X.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
        (Φ.F.app (op ⦋n⦌) ≫ HomologicalComplex.Hom.f PInfty n) :
      Splitting.summand X.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶ Y.X _⦋n⦌)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
      (Cofan.inj (X.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
        Splitting.summand X.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n ≫ Φ.F.app (op ⦋n⦌) : HomologicalComplex.X K[X.X] n ⟶ Y.X _⦋n⦌))
⊢ Eq (α := X.s.N n ⟶ Y.X _⦋n⦌)
    (Φ.f n ≫
      CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (Y.s.cofan (op ⦋n⦌)))
        (Cofan.inj (Y.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
          Splitting.summand Y.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (Y.s.cofan (op ⦋n⦌)))
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[Y.X] n ⟶ HomologicalComplex.X K[Y.X] n))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
      (Cofan.inj (X.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
        Splitting.summand X.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n ≫ Φ.F.app (op ⦋n⦌) : HomologicalComplex.X K[X.X] n ⟶ Y.X _⦋n⦌))

Tactic:
erw [← Split.cofan_inj_naturality_symm_assoc Φ (Splitting.IndexSet.id (op ⦋n⦌))]

Premises used: CategoryTheory.SimplicialObject.Splitting.IndexSet.id, SimplexCategory.mk, Opposite.op, CategoryTheory.SimplicialObject.Split.cofan_inj_naturality_symm_assoc
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y : Split.{v_1, u_1} C
Φ : X ⟶ Y
n : ℕ
h h₁ :
  Eq (α := X.s.N n ⟶ Y.X _⦋n⦌)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
        (Cofan.inj (X.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
        (HomologicalComplex.Hom.f PInfty n ≫ Φ.F.app (op ⦋n⦌)) :
      Splitting.summand X.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶ Y.X _⦋n⦌)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
      (Cofan.inj (X.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
        Splitting.summand X.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n ≫ Φ.F.app (op ⦋n⦌) : HomologicalComplex.X K[X.X] n ⟶ Y.X _⦋n⦌))
⊢ Eq (α := X.s.N n ⟶ Y.X _⦋n⦌)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
        (Cofan.inj (X.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
        (Φ.F.app (op ⦋n⦌) ≫ HomologicalComplex.Hom.f PInfty n) :
      Splitting.summand X.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶ Y.X _⦋n⦌)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
      (Cofan.inj (X.s.cofan (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
        Splitting.summand X.s.N (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (X.s.cofan (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n ≫ Φ.F.app (op ⦋n⦌) : HomologicalComplex.X K[X.X] n ⟶ Y.X _⦋n⦌))

Tactic:
rw [PInfty_f_naturality]

Premises used: AlgebraicTopology.DoldKan.PInfty_f_naturality
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : Augmented.{v_1, u_1} C
e : X ≅ Y
ed : X.ExtraDegeneracy
⊢ Eq (α := Y.right ⟶ Y.right)
    (CategoryStruct.comp (Y := Y.left _⦋0⦌)
        (Iso.inv (Functor.mapIso point e) ≫ ed.s' ≫ NatTrans.app (Iso.hom (Functor.mapIso drop e)) (op ⦋0⦌))
        (Y.hom.app (op ⦋0⦌)) :
      Y.right ⟶ Y.right)
    (𝟙 Y.right : Y.right ⟶ Y.right)

Tactic:
simpa [w₀, ed.s'_comp_ε_assoc] using (point.mapIso e).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.SimplicialObject.Augmented.w₀, CategoryTheory.SimplicialObject.Augmented.point, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s'_comp_ε_assoc, CategoryTheory.Functor.mapIso
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : Augmented.{v_1, u_1} C
e : X ≅ Y
ed : X.ExtraDegeneracy
⊢ Eq (α := Y.left _⦋0⦌ ⟶ Y.left _⦋0⦌)
    (CategoryStruct.comp (Y := Functor.obj drop X _⦋0⦌) (NatTrans.app (Iso.inv (Functor.mapIso drop e)) (op ⦋0⦌))
          (ed.s 0 ≫ NatTrans.app (Iso.hom (Functor.mapIso drop e)) (op ⦋HAdd.hAdd (α := ℕ) 0 1⦌)) ≫
        Y.left.δ 1 :
      Y.left _⦋0⦌ ⟶ Y.left _⦋0⦌)
    (Y.hom.app (op ⦋0⦌) ≫
        Iso.inv (Functor.mapIso point e) ≫ ed.s' ≫ NatTrans.app (Iso.hom (Functor.mapIso drop e)) (op ⦋0⦌) :
      Y.left _⦋0⦌ ⟶ Y.left _⦋0⦌)

Tactic:
simp [← SimplicialObject.δ_naturality, s₀_comp_δ₁_assoc, w₀_assoc]

Premises used: CategoryTheory.SimplicialObject.δ_naturality, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s₀_comp_δ₁_assoc, CategoryTheory.SimplicialObject.Augmented.w₀_assoc
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : Augmented.{v_1, u_1} C
e : X ≅ Y
ed : X.ExtraDegeneracy
n : ℕ
⊢ Eq (α := Y.left _⦋n⦌ ⟶ Y.left _⦋n⦌)
    ((NatTrans.app (Iso.inv (Functor.mapIso drop e)) (op ⦋n⦌) ≫
          ed.s n ≫ NatTrans.app (Iso.hom (Functor.mapIso drop e)) (op ⦋n + 1⦌)) ≫
        Y.left.δ 0 :
      Y.left _⦋n⦌ ⟶ Y.left _⦋n⦌)
    (𝟙 (Y.left _⦋n⦌) : Y.left _⦋n⦌ ⟶ Y.left _⦋n⦌)

Tactic:
simpa [← SimplicialObject.δ_naturality] using
      congr_app (drop.mapIso e).inv_hom_id (op ⦋n⦌)

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.SimplicialObject.δ_naturality, CategoryTheory.SimplicialObject.Augmented.drop, SimplexCategory.mk, Opposite.op, CategoryTheory.congr_app, CategoryTheory.Functor.mapIso
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : Augmented.{v_1, u_1} C
e : X ≅ Y
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
⊢ Eq (α := Y.left _⦋n + 1⦌ ⟶ Y.left _⦋n + 1⦌)
    (CategoryStruct.comp (Y := Functor.obj drop X _⦋n + 1⦌)
          (NatTrans.app (Iso.inv (Functor.mapIso drop e)) (op ⦋n + 1⦌))
          (ed.s (n + 1) ≫ NatTrans.app (Iso.hom (Functor.mapIso drop e)) (op ⦋n + 1 + 1⦌)) ≫
        Y.left.δ i.succ :
      Y.left _⦋n + 1⦌ ⟶ Y.left _⦋n + 1⦌)
    (Y.left.δ i ≫
        NatTrans.app (Iso.inv (Functor.mapIso drop e)) (op ⦋n⦌) ≫
          ed.s n ≫ NatTrans.app (Iso.hom (Functor.mapIso drop e)) (op ⦋n + 1⦌) :
      Y.left _⦋n + 1⦌ ⟶ Y.left _⦋n + 1⦌)

Tactic:
simp [← SimplicialObject.δ_naturality, s_comp_δ_assoc,
      ← SimplicialObject.δ_naturality_assoc]

Premises used: CategoryTheory.SimplicialObject.δ_naturality, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ_assoc, CategoryTheory.SimplicialObject.δ_naturality_assoc
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : Augmented.{v_1, u_1} C
e : X ≅ Y
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
⊢ Eq (α := Y.left _⦋n⦌ ⟶ Y.left _⦋n + 1 + 1⦌)
    ((NatTrans.app (Iso.inv (Functor.mapIso drop e)) (op ⦋n⦌) ≫
          ed.s n ≫ NatTrans.app (Iso.hom (Functor.mapIso drop e)) (op ⦋n + 1⦌)) ≫
        Y.left.σ i.succ :
      Y.left _⦋n⦌ ⟶ Y.left _⦋n + 1 + 1⦌)
    (Y.left.σ i ≫
        CategoryStruct.comp (Y := Functor.obj drop X _⦋n + 1⦌)
          (NatTrans.app (Iso.inv (Functor.mapIso drop e)) (op ⦋n + 1⦌))
          (ed.s (n + 1) ≫ NatTrans.app (Iso.hom (Functor.mapIso drop e)) (op ⦋n + 1 + 1⦌)) :
      Y.left _⦋n⦌ ⟶ Y.left _⦋n + 1 + 1⦌)

Tactic:
simp [← SimplicialObject.σ_naturality, s_comp_σ_assoc,
      ← SimplicialObject.σ_naturality_assoc]

Premises used: CategoryTheory.SimplicialObject.σ_naturality_assoc, CategoryTheory.SimplicialObject.σ_naturality, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_σ_assoc
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
⊢ ed.section_.app (op ⦋0⦌) = ed.s'

Tactic:
simp [section_]

Premises used: CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.section_
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : SimplexCategoryᵒᵖ
dsimp : (ed.s' ≫ X.left.map (Quiver.Hom.op (SimplexCategory.isTerminalZero.from (unop n)))) ≫ X.hom.app n = 𝟙 X.right
⊢ ed.section_.app n ≫ X.hom.app n = 𝟙 X.right

Tactic:
dsimp [section_]

Premises used: CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.section_
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : SimplexCategoryᵒᵖ
rw : ed.s' ≫ X.hom.app (op ⦋0⦌) = 𝟙 X.right
⊢ (ed.s' ≫ X.left.map (Quiver.Hom.op (SimplexCategory.isTerminalZero.from (unop n)))) ≫ X.hom.app n = 𝟙 X.right

Tactic:
rw [assoc, dsimp% X.hom.naturality, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Comma.hom, CategoryTheory.Category.comp_id, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : SimplexCategoryᵒᵖ
⊢ ed.s' ≫ X.hom.app (op ⦋0⦌) = 𝟙 X.right

Tactic:
ed.s'_comp_ε

Premises used: CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s'_comp_ε
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : SimplexCategoryᵒᵖ
⊢ ed.s' ≫ X.hom.app (op ⦋0⦌) = 𝟙 X.right

Tactic:
exact ed.s'_comp_ε

Premises used: CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s'_comp_ε
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
dsimp :
  ed.s' ≫ X.left.map (SimplexCategory.σ₀Iter n ⋯).op =
    ed.s' ≫ X.left.map (Quiver.Hom.op (SimplexCategory.isTerminalZero.from ⦋n⦌))
⊢ ed.s' ≫ X.left.σ₀Iter n ⋯ = ed.section_.app (op ⦋n⦌)

Tactic:
dsimp [section_, SimplicialObject.σ₀Iter]

Premises used: CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.section_, CategoryTheory.SimplicialObject.σ₀Iter
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
e_a : SimplexCategory.σ₀Iter n ⋯ = SimplexCategory.isTerminalZero.from ⦋n⦌
⊢ ed.s' ≫ X.left.map (SimplexCategory.σ₀Iter n ⋯).op =
    ed.s' ≫ X.left.map (Quiver.Hom.op (SimplexCategory.isTerminalZero.from ⦋n⦌))

Tactic:
congr 3
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
⊢ SimplexCategory.σ₀Iter n ⋯ = SimplexCategory.isTerminalZero.from ⦋n⦌

Tactic:
subsingleton
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
⊢ (↑i.rev : ℕ) + (↑i : ℕ) = n

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
⊢ (↑i.rev : ℕ) + 1 + (↑i : ℕ) = n + 1

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
j : ℕ
hj : autoParam (j = (↑i.rev : ℕ)) h_eq._auto_1
⊢ j + (↑i : ℕ) = n

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
j : ℕ
hj : autoParam (j = (↑i.rev : ℕ)) h_eq._auto_1
⊢ j + 1 + (↑i : ℕ) = n + 1

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
j : ℕ
hj : j = (↑i.rev : ℕ)
subst : h ed i = X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ ed.s (↑i.rev : ℕ) ≫ X.left.σ₀Iter (↑i : ℕ) ⋯
⊢ h ed i = X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ ed.s j ≫ X.left.σ₀Iter (↑i : ℕ) ⋯

Tactic:
subst hj
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
⊢ h ed i = X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ ed.s (↑i.rev : ℕ) ≫ X.left.σ₀Iter (↑i : ℕ) ⋯

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
⊢ n = (↑(Fin.rev 0) : ℕ)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
⊢ Eq (α := Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left _⦋n⦌ ⟶ X.left _⦋n⦌) (h ed 0 ≫ X.left.δ 0)
    (NatTrans.app (𝟙 X.left) (op ⦋n⦌))

Tactic:
simp [h_eq_assoc ed (0 : Fin (n + 1)) n (by simp)]

Premises used: CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy.h_eq_assoc, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
dsimp : h ed (Fin.last n) ≫ X.left.δ (Fin.last (n + 1)) = X.hom.app (op ⦋n⦌) ≫ ed.section_.app (op ⦋n⦌)
⊢ h ed (Fin.last n) ≫ X.left.δ (Fin.last (n + 1)) = (X.hom ≫ ed.section_).app (op ⦋n⦌)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
⊢ 0 + (↑(Fin.last n) : ℕ) = n

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
rw : X.hom.app (op ⦋n⦌) ≫ ed.s' ≫ X.left.σ₀Iter (↑(Fin.last n) : ℕ) ⋯ = X.hom.app (op ⦋n⦌) ≫ ed.section_.app (op ⦋n⦌)
⊢ h ed (Fin.last n) ≫ X.left.δ (Fin.last (n + 1)) = X.hom.app (op ⦋n⦌) ≫ ed.section_.app (op ⦋n⦌)

Tactic:
rw [h_eq_assoc _ _ 0, X.left.σ₀Iter_δ' _ _ 1 (by grind),
      ed.s₀_comp_δ₁_assoc, X.δ₀Iter_hom_app_assoc _ (by grind)]

Premises used: CategoryTheory.SimplicialObject.σ₀Iter_δ', CategoryTheory.Comma.left, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s₀_comp_δ₁_assoc, CategoryTheory.SimplicialObject.Augmented.δ₀Iter_hom_app_assoc, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy.h_eq_assoc, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
⊢ X.hom.app (op ⦋n⦌) ≫ ed.s' ≫ X.left.σ₀Iter (↑(Fin.last n) : ℕ) ⋯ = X.hom.app (op ⦋n⦌) ≫ ed.section_.app (op ⦋n⦌)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
generalize :
  ∀ (k : Fin (n + 1 + 1)) (hk : j.succ.rev = k),
    h ed j.succ ≫ X.left.δ i.castSucc = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).δ i ≫ h ed j
⊢ h ed j.succ ≫ X.left.δ i.castSucc = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).δ i ≫ h ed j

Tactic:
generalize hk : j.succ.rev = k

Premises used: Fin.succ, Fin.rev
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
k : Fin (n + 1 + 1)
hk : j.succ.rev = k
dsimp : h ed j.succ ≫ X.left.δ i.castSucc = X.left.δ i ≫ h ed j
⊢ h ed j.succ ≫ X.left.δ i.castSucc = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).δ i ≫ h ed j

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
k : Fin (n + 1 + 1)
hk : j.succ.rev = k
rw :
  X.left.δ₀Iter (↑j.succ : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j.succ : ℕ) ⋯ ≫ X.left.δ i.castSucc =
    X.left.δ i ≫ X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯
⊢ h ed j.succ ≫ X.left.δ i.castSucc = X.left.δ i ≫ h ed j

Tactic:
rw [h_eq_assoc _ _ k, h_eq _ _ k]

Premises used: Fin.val, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy.h_eq, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy.h_eq_assoc
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
k : Fin (n + 1 + 1)
hk : j.succ.rev = k
dsimp :
  X.left.δ₀Iter ((↑j : ℕ) + 1) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑j : ℕ) + 1) ⋯ ≫ X.left.δ i.castSucc =
    X.left.δ i ≫ X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯
⊢ X.left.δ₀Iter (↑j.succ : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j.succ : ℕ) ⋯ ≫ X.left.δ i.castSucc =
    X.left.δ i ≫ X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
k : Fin (n + 1 + 1)
hk : j.succ.rev = k
⊢ (↑k : ℕ) + 1 + ((↑j : ℕ) + 1) = n + 1 + 1

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
k : Fin (n + 1 + 1)
hk : j.succ.rev = k
⊢ (↑k : ℕ) + (↑j : ℕ) = n

Tactic:
grind