awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.Additive
X : SimplicialObject.{v_1, u_1} C
q n m : ℕ
hnm : c.Rel m n
unfold :
  Eq (α :=
    HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] n ⟶
      HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] m)
    ((if n < q then 0
      else HPow.hPow (α := ℤ) (-1) (n - q) • ((Functor.obj (whiskering C D) G).obj X).σ (⟨n - q, ⋯⟩ : Fin (n + 1))) ≫
      eqToHom ⋯)
    (G.map ((if n < q then 0 else HPow.hPow (α := ℤ) (-1) (n - q) • X.σ (⟨n - q, ⋯⟩ : Fin (n + 1))) ≫ eqToHom ⋯))
⊢ Eq.{v_2 + 1} (α :=
    HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] n ⟶
      HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] m)
    (hσ' q n m hnm) (G.map (hσ' q n m hnm))

Tactic:
unfold hσ' hσ

Premises used: AlgebraicTopology.DoldKan.hσ, AlgebraicTopology.DoldKan.hσ'
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.Additive
X : SimplicialObject.{v_1, u_1} C
q n m : ℕ
hnm : c.Rel m n
pos :
  n < q →
    Eq.{v_2 + 1} (α :=
      HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] n ⟶
        HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] m)
      (0 ≫ eqToHom ⋯) (G.map (0 ≫ eqToHom ⋯))
neg :
  ¬n < q →
    Eq (α :=
      HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] n ⟶
        HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] m)
      ((HPow.hPow (α := ℤ) (-1) (n - q) • ((Functor.obj (whiskering C D) G).obj X).σ (⟨n - q, ⋯⟩ : Fin (n + 1))) ≫
        eqToHom ⋯)
      (G.map ((HPow.hPow (α := ℤ) (-1) (n - q) • X.σ (⟨n - q, ⋯⟩ : Fin (n + 1))) ≫ eqToHom ⋯))
⊢ Eq (α :=
    HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] n ⟶
      HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] m)
    ((if n < q then 0
      else HPow.hPow (α := ℤ) (-1) (n - q) • ((Functor.obj (whiskering C D) G).obj X).σ (⟨n - q, ⋯⟩ : Fin (n + 1))) ≫
      eqToHom ⋯)
    (G.map ((if n < q then 0 else HPow.hPow (α := ℤ) (-1) (n - q) • X.σ (⟨n - q, ⋯⟩ : Fin (n + 1))) ≫ eqToHom ⋯))

Tactic:
split_ifs
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.Additive
X : SimplicialObject.{v_1, u_1} C
q n m : ℕ
hnm : c.Rel m n
h : n < q
⊢ Eq.{v_2 + 1} (α :=
    HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] n ⟶
      HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] m)
    (0 ≫ eqToHom ⋯) (G.map (0 ≫ eqToHom ⋯))

Tactic:
simp only [Functor.map_zero, zero_comp]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.Additive
X : SimplicialObject.{v_1, u_1} C
q n m : ℕ
hnm : c.Rel m n
h : ¬n < q
neg :
  Eq (α :=
    HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] n ⟶
      HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] m)
    ((HPow.hPow (α := ℤ) (-1) (n - q) • ((Functor.obj (whiskering C D) G).obj X).σ (⟨n - q, ⋯⟩ : Fin (n + 1))) ≫
      eqToHom ⋯)
    ((HPow.hPow (α := ℤ) (-1) (n - q) • G.map (X.σ (⟨n - q, ⋯⟩ : Fin (n + 1)))) ≫ eqToHom ⋯)
⊢ Eq (α :=
    HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] n ⟶
      HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] m)
    ((HPow.hPow (α := ℤ) (-1) (n - q) • ((Functor.obj (whiskering C D) G).obj X).σ (⟨n - q, ⋯⟩ : Fin (n + 1))) ≫
      eqToHom ⋯)
    (G.map ((HPow.hPow (α := ℤ) (-1) (n - q) • X.σ (⟨n - q, ⋯⟩ : Fin (n + 1))) ≫ eqToHom ⋯))

Tactic:
simp only [eqToHom_map, Functor.map_comp, Functor.map_zsmul]

Premises used: CategoryTheory.eqToHom_map, CategoryTheory.Functor.map_zsmul, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.Additive
X : SimplicialObject.{v_1, u_1} C
q n m : ℕ
hnm : c.Rel m n
h : ¬n < q
⊢ Eq (α :=
    HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] n ⟶
      HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] m)
    ((HPow.hPow (α := ℤ) (-1) (n - q) • ((Functor.obj (whiskering C D) G).obj X).σ (⟨n - q, ⋯⟩ : Fin (n + 1))) ≫
      eqToHom ⋯)
    ((HPow.hPow (α := ℤ) (-1) (n - q) • G.map (X.σ (⟨n - q, ⋯⟩ : Fin (n + 1)))) ≫ eqToHom ⋯)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.Additive
X : SimplicialObject.{v_1, u_1} C
q n : ℕ
unfold :
  Eq.{v_2 + 1} (α :=
    HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] n ⟶
      HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] n)
    (HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) n)
    (G.map (HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) n))
⊢ Eq.{v_2 + 1} (α :=
    HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] n ⟶
      HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] n)
    (HomologicalComplex.Hom.f (Hσ q) n) (G.map (HomologicalComplex.Hom.f (Hσ q) n))

Tactic:
unfold Hσ

Premises used: AlgebraicTopology.DoldKan.Hσ
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.Additive
X : SimplicialObject.{v_1, u_1} C
q n : ℕ
⊢ Eq (α :=
    HomologicalComplex.X (Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} C c) (G.mapHomologicalComplex c) K[X]) n ⟶
      HomologicalComplex.X (Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} C c) (G.mapHomologicalComplex c) K[X]) n)
    (HomologicalComplex.Hom.f (CategoryTheory.Functor.map (G.mapHomologicalComplex c) (nullHomotopicMap' (hσ' q))) n)
    (HomologicalComplex.Hom.f (nullHomotopicMap' fun (i j : ℕ) (hij : c.Rel j i) ↦ G.map (hσ' q i j hij)) n)

Tactic:
have eq := HomologicalComplex.congr_hom (map_nullHomotopicMap' G (@hσ' _ _ _ X q)) n
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.Additive
X : SimplicialObject.{v_1, u_1} C
q n : ℕ
eq :
  Eq (α :=
    HomologicalComplex.X (Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} C c) (G.mapHomologicalComplex c) K[X]) n ⟶
      HomologicalComplex.X (Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} C c) (G.mapHomologicalComplex c) K[X]) n)
    (HomologicalComplex.Hom.f (CategoryTheory.Functor.map (G.mapHomologicalComplex c) (nullHomotopicMap' (hσ' q))) n)
    (HomologicalComplex.Hom.f (nullHomotopicMap' fun (i j : ℕ) (hij : c.Rel j i) ↦ G.map (hσ' q i j hij)) n)
⊢ Eq (α :=
    HomologicalComplex.X (Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} C c) (G.mapHomologicalComplex c) K[X]) n ⟶
      HomologicalComplex.X (Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} C c) (G.mapHomologicalComplex c) K[X]) n)
    (G.map (HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) n))
    (HomologicalComplex.Hom.f (nullHomotopicMap' fun (i j : ℕ) (hij : c.Rel j i) ↦ hσ' q i j hij) n)

Tactic:
simp only [Functor.mapHomologicalComplex_map_f, ← map_hσ'] at eq

Premises used: CategoryTheory.Functor.mapHomologicalComplex_map_f, AlgebraicTopology.DoldKan.map_hσ'
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.Additive
X : SimplicialObject.{v_1, u_1} C
q n : ℕ
eq :
  Eq (α :=
    HomologicalComplex.X (Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} C c) (G.mapHomologicalComplex c) K[X]) n ⟶
      HomologicalComplex.X (Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} C c) (G.mapHomologicalComplex c) K[X]) n)
    (G.map (HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) n))
    (HomologicalComplex.Hom.f (nullHomotopicMap' fun (i j : ℕ) (hij : c.Rel j i) ↦ hσ' q i j hij) n)
rw :
  Eq.{v_2 + 1} (α :=
    HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] n ⟶
      HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] n)
    (HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) n)
    (HomologicalComplex.Hom.f (nullHomotopicMap' fun (i j : ℕ) (hij : c.Rel j i) ↦ hσ' q i j hij) n)
⊢ Eq.{v_2 + 1} (α :=
    HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] n ⟶
      HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] n)
    (HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) n)
    (G.map (HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) n))

Tactic:
rw [eq]
-- Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.Additive
X : SimplicialObject.{v_1, u_1} C
q n : ℕ
eq :
  Eq (α :=
    HomologicalComplex.X (Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} C c) (G.mapHomologicalComplex c) K[X]) n ⟶
      HomologicalComplex.X (Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} C c) (G.mapHomologicalComplex c) K[X]) n)
    (G.map (HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) n))
    (HomologicalComplex.Hom.f (nullHomotopicMap' fun (i j : ℕ) (hij : c.Rel j i) ↦ hσ' q i j hij) n)
h : Eq (α := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.down ℕ))
  (Functor.obj (Functor.obj (whiskering C D) G ⋙ alternatingFaceMapComplex D) X)
  (Functor.obj
    (Functor.comp (D := ChainComplex.{v_1, u_1, 0} C ℕ) (alternatingFaceMapComplex C)
      (G.mapHomologicalComplex (ComplexShape.down ℕ)))
    X) :=
  ⋯
⊢ Eq.{v_2 + 1} (α :=
    HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] n ⟶
      HomologicalComplex.X K[(Functor.obj (whiskering C D) G).obj X] n)
    (HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) n)
    (HomologicalComplex.Hom.f (nullHomotopicMap' fun (i j : ℕ) (hij : c.Rel j i) ↦ hσ' q i j hij) n)

Tactic:
congr
-- Module: Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
q : ℕ
refine_1 :
  P (q + 1) =
    HAdd.hAdd (α := Quiver.Hom (V := HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.down ℕ)) K[X] K[X]) (P q)
      (P q ≫ Hσ q)
refine_2 :
  HAdd.hAdd (α := Quiver.Hom (V := HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.down ℕ)) K[X] K[X]) (𝟙 K[X])
      (P q ≫ 0) =
    𝟙 K[X]
⊢ Homotopy (C := K[X]) (P (q + 1)) (𝟙 K[X])

Tactic:
refine
      Homotopy.trans (Homotopy.ofEq ?_)
        (Homotopy.trans
          (Homotopy.add (homotopyPToId q) (Homotopy.compLeft (homotopyHσToZero q) (P q)))
          (Homotopy.ofEq ?_))

Premises used: Homotopy.ofEq, AlgebraicTopology.DoldKan.homotopyHσToZero, Homotopy.add, Homotopy.trans, Homotopy.compLeft, AlgebraicTopology.DoldKan.P
-- Module: Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
q : ℕ
⊢ P (q + 1) =
    HAdd.hAdd (α := Quiver.Hom (V := HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.down ℕ)) K[X] K[X]) (P q)
      (P q ≫ Hσ q)

Tactic:
simp only [P_succ, comp_add, comp_id]

Premises used: CategoryTheory.Category.comp_id, AlgebraicTopology.DoldKan.P_succ, CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
q : ℕ
⊢ HAdd.hAdd (α := Quiver.Hom (V := HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.down ℕ)) K[X] K[X]) (𝟙 K[X])
      (P q ≫ 0) =
    𝟙 K[X]

Tactic:
simp only [add_zero, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, add_zero
-- Module: Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
q n : ℕ
hqn : n < q
⊢ Eq (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] (n + 1))
    (Homotopy.hom (f := P (q + 1)) (homotopyPToId X (q + 1)) n (n + 1)) (Homotopy.hom (homotopyPToId X q) n (n + 1))

Tactic:
simp only [homotopyHσToZero, AlternatingFaceMapComplex.obj_X, Homotopy.trans_hom,
    Homotopy.ofEq_hom, Pi.zero_apply, Homotopy.add_hom, Homotopy.compLeft_hom, add_zero,
    Homotopy.nullHomotopy'_hom, ComplexShape.down_Rel, hσ'_eq_zero hqn (c_mk (n + 1) n rfl),
    dite_eq_ite, ite_self, comp_zero, zero_add, homotopyPToId]

Premises used: ite_self, CategoryTheory.Limits.comp_zero, ComplexShape.down_Rel, Pi.zero_apply, AlgebraicTopology.DoldKan.homotopyPToId, zero_add, Homotopy.ofEq_hom, AlgebraicTopology.DoldKan.homotopyHσToZero, Homotopy.add_hom, HAdd.hAdd, AlgebraicTopology.DoldKan.c_mk, AlgebraicTopology.DoldKan.hσ'_eq_zero, Homotopy.trans_hom, Homotopy.compLeft_hom, dite_eq_ite, add_zero, OfNat.ofNat, AlgebraicTopology.AlternatingFaceMapComplex.obj_X, rfl, Homotopy.nullHomotopy'_hom
-- Module: Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
zero :
  HomologicalComplex.Hom.f PInfty 0 =
    HAdd.hAdd (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0) (β :=
        HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0)
        ((dNext 0 : (a : (i j : ℕ) → K[X].X i ⟶ K[X].X j) → K[X].X 0 ⟶ K[X].X 0) fun (i j : ℕ) ↦
            Homotopy.hom (f := P (j + 1)) (homotopyPToId X (j + 1)) i j :
          HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0)
        ((prevD 0 : (a : (i j : ℕ) → K[X].X i ⟶ K[X].X j) → K[X].X 0 ⟶ K[X].X 0) fun (i j : ℕ) ↦
            Homotopy.hom (f := P (j + 1)) (homotopyPToId X (j + 1)) i j :
          HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0) +
      HomologicalComplex.Hom.f (𝟙 K[X]) 0
succ :
  ∀ (n : ℕ),
    HomologicalComplex.Hom.f PInfty (n + 1) =
      HAdd.hAdd (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1)) (β :=
          HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
          ((dNext (n + 1) : (a : (i j : ℕ) → K[X].X i ⟶ K[X].X j) → K[X].X (n + 1) ⟶ K[X].X (n + 1)) fun (i j : ℕ) ↦
              Homotopy.hom (f := P (j + 1)) (homotopyPToId X (j + 1)) i j :
            HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
          ((prevD (n + 1) : (a : (i j : ℕ) → K[X].X i ⟶ K[X].X j) → K[X].X (n + 1) ⟶ K[X].X (n + 1)) fun (i j : ℕ) ↦
              Homotopy.hom (f := P (j + 1)) (homotopyPToId X (j + 1)) i j :
            HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1)) +
        HomologicalComplex.Hom.f (𝟙 K[X]) (n + 1)
⊢ HomologicalComplex.Hom.f PInfty n =
    HAdd.hAdd (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) (β :=
        HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n)
        ((dNext n : (a : (i j : ℕ) → K[X].X i ⟶ K[X].X j) → K[X].X n ⟶ K[X].X n) fun (i j : ℕ) ↦
            Homotopy.hom (f := P (j + 1)) (homotopyPToId X (j + 1)) i j :
          HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n)
        ((prevD n : (a : (i j : ℕ) → K[X].X i ⟶ K[X].X j) → K[X].X n ⟶ K[X].X n) fun (i j : ℕ) ↦
            Homotopy.hom (f := P (j + 1)) (homotopyPToId X (j + 1)) i j :
          HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) +
      HomologicalComplex.Hom.f (𝟙 K[X]) n

Tactic:
rcases n with _ | n
-- Module: Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
⊢ HomologicalComplex.Hom.f PInfty 0 =
    HAdd.hAdd (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0) (β :=
        HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0)
        ((dNext 0 : (a : (i j : ℕ) → K[X].X i ⟶ K[X].X j) → K[X].X 0 ⟶ K[X].X 0) fun (i j : ℕ) ↦
            Homotopy.hom (f := P (j + 1)) (homotopyPToId X (j + 1)) i j :
          HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0)
        ((prevD 0 : (a : (i j : ℕ) → K[X].X i ⟶ K[X].X j) → K[X].X 0 ⟶ K[X].X 0) fun (i j : ℕ) ↦
            Homotopy.hom (f := P (j + 1)) (homotopyPToId X (j + 1)) i j :
          HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0) +
      HomologicalComplex.Hom.f (𝟙 K[X]) 0

Tactic:
simpa only [Homotopy.dNext_zero_chainComplex, Homotopy.prevD_chainComplex,
        PInfty_f, P_f_0_eq, zero_add] using (homotopyPToId X 2).comm 0

Premises used: AlgebraicTopology.DoldKan.P_f_0_eq, Homotopy.dNext_zero_chainComplex, Homotopy.prevD_chainComplex, AlgebraicTopology.DoldKan.homotopyPToId, zero_add, AlgebraicTopology.DoldKan.PInfty_f, Homotopy.comm, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
⊢ HomologicalComplex.Hom.f PInfty (n + 1) =
    HAdd.hAdd (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1)) (β :=
        HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
        ((dNext (n + 1) : (a : (i j : ℕ) → K[X].X i ⟶ K[X].X j) → K[X].X (n + 1) ⟶ K[X].X (n + 1)) fun (i j : ℕ) ↦
            Homotopy.hom (f := P (j + 1)) (homotopyPToId X (j + 1)) i j :
          HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
        ((prevD (n + 1) : (a : (i j : ℕ) → K[X].X i ⟶ K[X].X j) → K[X].X (n + 1) ⟶ K[X].X (n + 1)) fun (i j : ℕ) ↦
            Homotopy.hom (f := P (j + 1)) (homotopyPToId X (j + 1)) i j :
          HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1)) +
      HomologicalComplex.Hom.f (𝟙 K[X]) (n + 1)

Tactic:
simpa only [Homotopy.dNext_succ_chainComplex, Homotopy.prevD_chainComplex,
          HomologicalComplex.id_f, PInfty_f, ← P_is_eventually_constant (le_refl <| n + 1),
          homotopyPToId_eventually_constant X (Nat.lt_add_one (Nat.succ n)),
          Homotopy.dNext_succ_chainComplex, Homotopy.prevD_chainComplex]
        using (homotopyPToId X (n + 2)).comm (n + 1)

Premises used: le_refl, Homotopy.prevD_chainComplex, HomologicalComplex.id_f, Nat.lt_add_one, AlgebraicTopology.DoldKan.homotopyPToId, AlgebraicTopology.DoldKan.PInfty_f, Homotopy.dNext_succ_chainComplex, HAdd.hAdd, AlgebraicTopology.DoldKan.P_is_eventually_constant, Homotopy.comm, AlgebraicTopology.DoldKan.homotopyPToId_eventually_constant, OfNat.ofNat, Nat.succ
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
Δ' : SimplexCategory
i : Δ' ⟶ ⦋n⦌
hi : Mono i
h₁ : Δ'.len ≠ n
h₂ : ¬Isδ₀ i
mk :
  ∀ (m : ℕ) (i : ⦋m⦌ ⟶ ⦋n⦌) [hi : Mono i] (h₁ : ⦋m⦌.len ≠ n) (h₂ : ¬Isδ₀ i),
    Eq (α := HomologicalComplex.X K[X] n ⟶ X _⦋m⦌) (HomologicalComplex.Hom.f PInfty n ≫ X.map i.op) 0
⊢ Eq (α := HomologicalComplex.X K[X] n ⟶ X.obj (op Δ')) (HomologicalComplex.Hom.f PInfty n ≫ X.map i.op) 0

Tactic:
induction Δ' using SimplexCategory.rec with | _ m
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
h : ⦋n⦌ = ⦋m⦌
⊢ ⦋n⦌.len ≠ n

Tactic:
rw [← h] at h₁
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
h : ⦋n⦌ = ⦋m⦌
h₃ : ⦋n⦌.len ≠ n
⊢ ¬Isδ₀ i

Tactic:
rw [← h] at h₁
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
h : ⦋n⦌ = ⦋m⦌
h₃ : ⦋n⦌.len ≠ n
h₄ : ¬Isδ₀ i
⊢ ⦋n⦌ = ⦋m⦌

Tactic:
rw [← h] at h₁
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋n⦌.len ≠ n
h₂ : ¬Isδ₀ i
h : ⦋n⦌ = ⦋m⦌
⊢ False

Tactic:
h₁ rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋n⦌.len ≠ n
h₂ : ¬Isδ₀ i
h : ⦋n⦌ = ⦋m⦌
⊢ False

Tactic:
exact h₁ rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
mk :
  ∀ (k : ℕ) (hk : ⦋n⦌.len = ⦋m⦌.len + k + 1),
    Eq (α := HomologicalComplex.X K[X] n ⟶ X _⦋m⦌) (HomologicalComplex.Hom.f PInfty n ≫ X.map i.op) 0
⊢ Eq (α := HomologicalComplex.X K[X] n ⟶ X _⦋m⦌) (HomologicalComplex.Hom.f PInfty n ≫ X.map i.op) 0

Tactic:
obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_lt (len_lt_of_mono i fun h => by
        rw [← h] at h₁
        exact h₁ rfl)

Premises used: SimplexCategory.len_lt_of_mono, Nat.exists_eq_add_of_lt
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
k : ℕ
hk : ⦋n⦌.len = ⦋m⦌.len + k + 1
mk :
  ∀ (hk : ⦋n⦌.len = ⦋m⦌.len + 0 + 1),
    Eq (α := HomologicalComplex.X K[X] n ⟶ X _⦋m⦌) (HomologicalComplex.Hom.f PInfty n ≫ X.map i.op) 0
mk₁ :
  ∀ (k : ℕ) (hk : ⦋n⦌.len = ⦋m⦌.len + (k + 1) + 1),
    Eq (α := HomologicalComplex.X K[X] n ⟶ X _⦋m⦌) (HomologicalComplex.Hom.f PInfty n ≫ X.map i.op) 0
⊢ Eq (α := HomologicalComplex.X K[X] n ⟶ X _⦋m⦌) (HomologicalComplex.Hom.f PInfty n ≫ X.map i.op) 0

Tactic:
rcases k with _ | k
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
hk : ⦋n⦌.len = ⦋m⦌.len + 0 + 1
⊢ n = m + 1

Tactic:
change n = m + 1 at hk
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
hk : n = m + 1
mk :
  ∀ (i : ⦋m⦌ ⟶ ⦋m + 1⦌) [hi : Mono i] (h₁ : ⦋m⦌.len ≠ m + 1) (h₂ : ¬Isδ₀ i),
    Eq (α := HomologicalComplex.X K[X] (m + 1) ⟶ X _⦋m⦌) (HomologicalComplex.Hom.f PInfty (m + 1) ≫ X.map i.op) 0
⊢ Eq (α := HomologicalComplex.X K[X] n ⟶ X _⦋m⦌) (HomologicalComplex.Hom.f PInfty n ≫ X.map i.op) 0

Tactic:
subst hk