awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (goal)
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 : ℕ
x x_1 : SimplicialObject.{v_1, u_1} C
f : x ⟶ x_1
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
      (Functor.obj (alternatingFaceMapComplex C) x_1))
    (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ nullHomotopicMap' (hσ' q))
    (nullHomotopicMap' (hσ' q) ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
have rw : Eq.{v_1 + 1} (α :=
  Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
    (Functor.obj (alternatingFaceMapComplex C) x_1))
  (nullHomotopicMap' fun (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel j i) ↦
    HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) i ≫ hσ' q i j hij)
  (nullHomotopicMap' fun (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel j i) ↦
    hσ' q i j hij ≫ HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) j)
Tactic: rw [nullHomotopicMap'_comp, comp_nullHomotopicMap']
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (goal)
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 : ℕ
x x_1 : SimplicialObject.{v_1, u_1} C
f : x ⟶ x_1
⊢ Eq.{v_1 + 1} (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
      (Functor.obj (alternatingFaceMapComplex C) x_1))
    (nullHomotopicMap' fun (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel j i) ↦
      HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) i ≫ hσ' q i j hij)
    (nullHomotopicMap' fun (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel j i) ↦
      hσ' q i j hij ≫ HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) j)
have e_h : Eq.{v_1 + 1} (α :=
  (i j : ℕ) →
    (ComplexShape.down ℕ).Rel j i →
      (HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) x) i ⟶
        HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) x_1) j))
  (fun (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel j i) ↦
    HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) i ≫ hσ' q i j hij)
  fun (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel j i) ↦
  hσ' q i j hij ≫ HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) j
Tactic: congr
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (goal)
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 : ℕ
x x_1 : SimplicialObject.{v_1, u_1} C
f : x ⟶ x_1
⊢ Eq.{v_1 + 1} (α :=
    (i j : ℕ) →
      (ComplexShape.down ℕ).Rel j i →
        (HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) x) i ⟶
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) x_1) j))
    (fun (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel j i) ↦
      HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) i ≫ hσ' q i j hij)
    fun (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel j i) ↦
    hσ' q i j hij ≫ HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) j
have e_h : ∀ (n m : ℕ) (hnm : (ComplexShape.down ℕ).Rel m n),
  Eq (α :=
    HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) x) n ⟶
      HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) x_1) m)
    (HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) n ≫ hσ' q n m hnm)
    (hσ' q n m hnm ≫ HomologicalComplex.Hom.f (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) m)
Tactic: ext n m hnm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (goal)
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
⊢ 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))
have 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, sorry⟩ : Fin (n + 1))) ≫
    eqToHom sorry)
  (G.map ((if n < q then 0 else HPow.hPow (α := ℤ) (-1) (n - q) • X.σ (⟨n - q, sorry⟩ : Fin (n + 1))) ≫ eqToHom sorry))
Tactic: unfold hσ' hσ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (goal)
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
⊢ 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 ⋯))
have 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 sorry) (G.map (0 ≫ eqToHom sorry))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (goal)
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 ⋯))
⊢ 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 ⋯))
have 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, sorry⟩ : Fin (n + 1))) ≫
      eqToHom sorry)
    (G.map ((HPow.hPow (α := ℤ) (-1) (n - q) • X.σ (⟨n - q, sorry⟩ : Fin (n + 1))) ≫ eqToHom sorry))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (goal)
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 ⋯)
    (G.map ((HPow.hPow (α := ℤ) (-1) (n - q) • X.σ (⟨n - q, ⋯⟩ : Fin (n + 1))) ≫ eqToHom ⋯))
have 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, sorry⟩ : Fin (n + 1))) ≫
    eqToHom sorry)
  ((HPow.hPow (α := ℤ) (-1) (n - q) • G.map (X.σ (⟨n - q, sorry⟩ : Fin (n + 1)))) ≫ eqToHom sorry)
Tactic: simp only [eqToHom_map, Functor.map_comp, Functor.map_zsmul]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (goal)
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.{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))
have 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))
Tactic: unfold Hσ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (hypothesis)
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.{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))
have 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)
Tactic: have eq := HomologicalComplex.congr_hom (map_nullHomotopicMap' G (@hσ' _ _ _ X q)) n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (hypothesis)
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.{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))
have 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)
Tactic: simp only [Functor.mapHomologicalComplex_map_f, ← map_hσ'] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Homotopies (goal)
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)
⊢ 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))
have 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)
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence (goal)
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 : ℕ
⊢ Homotopy (C := K[X]) (P (q + 1)) (𝟙 K[X])
have 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)
Tactic: refine
      Homotopy.trans (Homotopy.ofEq ?_)
        (Homotopy.trans
          (Homotopy.add (homotopyPToId q) (Homotopy.compLeft (homotopyHσToZero q) (P q)))
          (Homotopy.ofEq ?_))
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence (goal)
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)
⊢ Homotopy (C := K[X]) (P (q + 1)) (𝟙 K[X])
have 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]
Tactic: refine
      Homotopy.trans (Homotopy.ofEq ?_)
        (Homotopy.trans
          (Homotopy.add (homotopyPToId q) (Homotopy.compLeft (homotopyHσToZero q) (P q)))
          (Homotopy.ofEq ?_))
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence (goal)
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 =
    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
have 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
Tactic: rcases n with _ | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence (goal)
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
⊢ 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
have 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)
Tactic: rcases n with _ | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
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
⊢ Eq (α := HomologicalComplex.X K[X] n ⟶ X.obj (op Δ')) (HomologicalComplex.Hom.f PInfty n ≫ X.map i.op) 0
have 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
Tactic: induction Δ' using SimplexCategory.rec with | _ m
Cleared hypotheses: Δ', i, hi, h₁, h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (hypothesis)
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⦌
⊢ False
have h₃ : ⦋n⦌.len ≠ n
Tactic: rw [← h] at h₁
Cleared hypotheses: h₁, h₂, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
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
⊢ Eq (α := HomologicalComplex.X K[X] n ⟶ X _⦋m⦌) (HomologicalComplex.Hom.f PInfty n ≫ X.map i.op) 0
have 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
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)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
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
⊢ Eq (α := HomologicalComplex.X K[X] n ⟶ X _⦋m⦌) (HomologicalComplex.Hom.f PInfty n ≫ X.map i.op) 0
have 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
Tactic: rcases k with _ | k
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
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
⊢ Eq (α := HomologicalComplex.X K[X] n ⟶ X _⦋m⦌) (HomologicalComplex.Hom.f PInfty n ≫ X.map i.op) 0
have 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
Tactic: rcases k with _ | k
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (hypothesis)
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
⊢ Eq (α := HomologicalComplex.X K[X] n ⟶ X _⦋m⦌) (HomologicalComplex.Hom.f PInfty n ≫ X.map i.op) 0
have hk₁ : n = m + 1
Tactic: change n = m + 1 at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
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
⊢ Eq (α := HomologicalComplex.X K[X] n ⟶ X _⦋m⦌) (HomologicalComplex.Hom.f PInfty n ≫ X.map i.op) 0
have 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
Tactic: subst hk
Cleared hypotheses: n, i, hi, h₁, h₂, hk
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
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
m : ℕ
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
have mk : ∀ (j : Fin (m + 2)) [hi : Mono (SimplexCategory.δ j)] (h₂ : ¬Isδ₀ (SimplexCategory.δ j)),
  Eq (α := HomologicalComplex.X K[X] (m + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + 1) ≫ X.map (SimplexCategory.δ j).op) 0
Tactic: obtain ⟨j, rfl⟩ := eq_δ_of_mono i
Cleared hypotheses: i, hi, h₂