awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.PInfty (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
Y : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C := Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) Y
Y₂ : SimplicialObject.{v_1, u_1} C := Y.X
Y₃ : SimplicialObject (Karoubi.{v_1, u_1} C) :=
  Functor.obj (Functor.obj (whiskering C (Karoubi.{v_1, u_1} C)) (toKaroubi C)) Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C :=
  Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    (Functor.obj (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C)) Y.X)
P₁ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₁] K[Y₁] := PInfty
P₂ : Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[Y₂] K[Y₂] := PInfty
P₃ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₃] K[Y₃] := PInfty
P₄ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₄] K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  Eq.{v_1 + 1} (α := KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌ ⟶ KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n :
      HomologicalComplex.X
          (Functor.obj (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C)) (KaroubiFunctorCategoryEmbedding.obj Y)) n ⟶
        HomologicalComplex.X
          (Functor.obj (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C)) (KaroubiFunctorCategoryEmbedding.obj Y)) n)
    ((KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      HomologicalComplex.Hom.f PInfty n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌))
π : Y₄ ⟶ Y₄ :=
  CategoryTheory.Functor.map
    (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) ⋙
      karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    Y.p
⊢ Y.p.app (op ⦋n⦌) ≫
      CategoryStruct.comp (Y :=
        KaroubiFunctorCategoryEmbedding.obj
              { X := Y.X, p := 𝟙 Y.X, idem := ⋯ :
                Karoubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) } _⦋n⦌.X)
        (Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty n)) (Y.p.app (op ⦋n⦌)) =
    Y.p.app (op ⦋n⦌) ≫ (P₄.f n).f
have eq : Eq (α := Y₄ _⦋n⦌.X ⟶ (HomologicalComplex.X K[Y₄] n).X)
  (Karoubi.Hom.f (π.app (op ⦋n⦌) ≫ HomologicalComplex.Hom.f PInfty n))
  (Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty n ≫ π.app (op ⦋n⦌)))
Tactic: have eq := Karoubi.hom_ext_iff.mp (PInfty_f_naturality n π)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.PInfty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
Y : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C := Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) Y
Y₂ : SimplicialObject.{v_1, u_1} C := Y.X
Y₃ : SimplicialObject (Karoubi.{v_1, u_1} C) :=
  Functor.obj (Functor.obj (whiskering C (Karoubi.{v_1, u_1} C)) (toKaroubi C)) Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C :=
  Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    (Functor.obj (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C)) Y.X)
P₁ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₁] K[Y₁] := PInfty
P₂ : Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[Y₂] K[Y₂] := PInfty
P₃ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₃] K[Y₃] := PInfty
P₄ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₄] K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  Eq.{v_1 + 1} (α := KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌ ⟶ KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n :
      HomologicalComplex.X
          (Functor.obj (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C)) (KaroubiFunctorCategoryEmbedding.obj Y)) n ⟶
        HomologicalComplex.X
          (Functor.obj (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C)) (KaroubiFunctorCategoryEmbedding.obj Y)) n)
    ((KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      HomologicalComplex.Hom.f PInfty n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌))
π : Y₄ ⟶ Y₄ :=
  CategoryTheory.Functor.map
    (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) ⋙
      karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    Y.p
eq :
  Eq (α := Y₄ _⦋n⦌.X ⟶ Y₄ _⦋n⦌.X) (Y.p.app (op ⦋n⦌) ≫ Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty n))
    (CategoryStruct.comp (Y := Y₄ _⦋n⦌.X) (Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty n)) (Y.p.app (op ⦋n⦌)))
⊢ Y.p.app (op ⦋n⦌) ≫
      CategoryStruct.comp (Y :=
        KaroubiFunctorCategoryEmbedding.obj
              { X := Y.X, p := 𝟙 Y.X, idem := ⋯ :
                Karoubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) } _⦋n⦌.X)
        (Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty n)) (Y.p.app (op ⦋n⦌)) =
    Y.p.app (op ⦋n⦌) ≫ (P₄.f n).f
have rw : Y.p.app (op ⦋n⦌) ≫ Y.p.app (op ⦋n⦌) ≫ Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty n) = Y.p.app (op ⦋n⦌) ≫ (P₄.f n).f
Tactic: rw [← eq, app_idem_assoc Y (op ⦋n⦌)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.PInfty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
Y : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C := Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) Y
Y₂ : SimplicialObject.{v_1, u_1} C := Y.X
Y₃ : SimplicialObject (Karoubi.{v_1, u_1} C) :=
  Functor.obj (Functor.obj (whiskering C (Karoubi.{v_1, u_1} C)) (toKaroubi C)) Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C :=
  Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    (Functor.obj (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C)) Y.X)
P₁ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₁] K[Y₁] := PInfty
P₂ : Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[Y₂] K[Y₂] := PInfty
P₃ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₃] K[Y₃] := PInfty
P₄ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₄] K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  Eq.{v_1 + 1} (α := KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌ ⟶ KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n :
      HomologicalComplex.X
          (Functor.obj (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C)) (KaroubiFunctorCategoryEmbedding.obj Y)) n ⟶
        HomologicalComplex.X
          (Functor.obj (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C)) (KaroubiFunctorCategoryEmbedding.obj Y)) n)
    ((KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      HomologicalComplex.Hom.f PInfty n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌))
π : Y₄ ⟶ Y₄ :=
  CategoryTheory.Functor.map
    (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) ⋙
      karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    Y.p
eq :
  Eq (α := Y₄ _⦋n⦌.X ⟶ Y₄ _⦋n⦌.X) (Y.p.app (op ⦋n⦌) ≫ Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty n))
    (CategoryStruct.comp (Y := Y₄ _⦋n⦌.X) (Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty n)) (Y.p.app (op ⦋n⦌)))
rw :
  Y.p.app (op ⦋n⦌) ≫ Y.p.app (op ⦋n⦌) ≫ Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty n) =
    Y.p.app (op ⦋n⦌) ≫ (P₄.f n).f
⊢ Y.p.app (op ⦋n⦌) ≫
      CategoryStruct.comp (Y :=
        KaroubiFunctorCategoryEmbedding.obj
              { X := Y.X, p := 𝟙 Y.X, idem := ⋯ :
                Karoubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) } _⦋n⦌.X)
        (Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty n)) (Y.p.app (op ⦋n⦌)) =
    Y.p.app (op ⦋n⦌) ≫ (P₄.f n).f
have rw₁ : Y.p.app (op ⦋n⦌) ≫ Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty n) = Y.p.app (op ⦋n⦌) ≫ (P₄.f n).f
Tactic: rw [← eq, app_idem_assoc Y (op ⦋n⦌)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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 : ℕ
⊢ HomologicalComplex.Hom.f (P q) 0 = 𝟙 (HomologicalComplex.X K[X] 0)
have zero : HomologicalComplex.Hom.f (P 0) 0 = 𝟙 (HomologicalComplex.X K[X] 0)
Tactic: induction q with
  | zero => rfl
  | succ q hq =>
    simp only [P_succ, HomologicalComplex.add_f_apply, HomologicalComplex.comp_f,
      HomologicalComplex.id_f, id_comp, hq, Hσ_eq_zero, add_zero]
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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 : ℕ
zero : HomologicalComplex.Hom.f (P 0) 0 = 𝟙 (HomologicalComplex.X K[X] 0)
⊢ HomologicalComplex.Hom.f (P q) 0 = 𝟙 (HomologicalComplex.X K[X] 0)
have succ : ∀ (q : ℕ) (hq : HomologicalComplex.Hom.f (P q) 0 = 𝟙 (HomologicalComplex.X K[X] 0)),
  HomologicalComplex.Hom.f (P (q + 1)) 0 = 𝟙 (HomologicalComplex.X K[X] 0)
Tactic: induction q with
  | zero => rfl
  | succ q hq =>
    simp only [P_succ, HomologicalComplex.add_f_apply, HomologicalComplex.comp_f,
      HomologicalComplex.id_f, id_comp, hq, Hσ_eq_zero, add_zero]
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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 : ℕ
⊢ HAdd.hAdd (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (P q) (Q q) = 𝟙 K[X]
have rw : P q + HSub.hSub (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (𝟙 K[X]) (P q) = 𝟙 K[X]
Tactic: rw [Q]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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 : ℕ
⊢ Q (q + 1) = HSub.hSub (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (Q q) (P q ≫ Hσ q)
have simp : 𝟙 K[X] - HAdd.hAdd (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (P q) (P q ≫ Hσ q) =
  HSub.hSub (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (𝟙 K[X]) (P q) - P q ≫ Hσ q
Tactic: simp only [Q, P_succ, comp_add, comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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 n : ℕ
⊢ HigherFacesVanish.{v_1, u_1} (C := C) (X := X) (Y := HomologicalComplex.X K[X] (n + 1)) (q + 1)
    (HomologicalComplex.Hom.f (P (q + 1)) (n + 1))
have simp : HigherFacesVanish (Y := HomologicalComplex.X K[X] (n + 1)) (q + 1)
  ((P q ≫ HAdd.hAdd (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (𝟙 K[X]) (Hσ q)).f (n + 1))
Tactic: simp only [P_succ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish 0 φ
⊢ φ ≫ HomologicalComplex.Hom.f (P 0) (n + 1) = φ
have zero : φ ≫ HomologicalComplex.Hom.f (𝟙 K[X]) (n + 1) = φ
Tactic: simp only [P_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : ∀ (v : HigherFacesVanish q φ), φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
⊢ φ ≫ HomologicalComplex.Hom.f (P (q + 1)) (n + 1) = φ
have succ : Eq (α := Y ⟶ HomologicalComplex.X K[X] (n + 1)) (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0
Tactic: simp only [P_succ, comp_add, HomologicalComplex.comp_f, HomologicalComplex.add_f_apply,
      comp_id, ← assoc, hq v.of_succ, add_eq_left]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : ∀ (v : HigherFacesVanish q φ), φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
⊢ Eq (α := Y ⟶ HomologicalComplex.X K[X] (n + 1)) (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0
have pos : ∀ (hqn : n < q), Eq (α := Y ⟶ HomologicalComplex.X K[X] (n + 1)) (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0
Tactic: by_cases! hqn : n < q
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : ∀ (v : HigherFacesVanish q φ), φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
pos : ∀ (hqn : n < q), Eq (α := Y ⟶ HomologicalComplex.X K[X] (n + 1)) (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0
⊢ Eq (α := Y ⟶ HomologicalComplex.X K[X] (n + 1)) (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0
have neg : ∀ (hqn : q ≤ n), Eq (α := Y ⟶ HomologicalComplex.X K[X] (n + 1)) (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0
Tactic: by_cases! hqn : n < q
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : ∀ (v : HigherFacesVanish q φ), φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : q ≤ n
⊢ Eq (α := Y ⟶ HomologicalComplex.X K[X] (n + 1)) (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0
have neg : ∀ (a : ℕ) (ha : q + a = n),
  Eq (α := Y ⟶ HomologicalComplex.X K[X] (n + 1)) (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0
Tactic: obtain ⟨a, ha⟩ := Nat.le.dest hqn
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : ∀ (v : HigherFacesVanish q φ), φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : q ≤ n
a : ℕ
ha : q + a = n
⊢ Eq (α := Y ⟶ HomologicalComplex.X K[X] (n + 1)) (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0
have hnaq : n = a + q
Tactic: have hnaq : n = a + q := by lia
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : ∀ (v : HigherFacesVanish q φ), φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : q ≤ n
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ Eq (α := Y ⟶ HomologicalComplex.X K[X] (n + 1)) (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0
have neg : (φ ≫ X.δ (⟨a + 1, sorry⟩ : Fin (n + 2))) ≫ X.σ (⟨a, sorry⟩ : Fin (n + 1)) = 0
Tactic: simp only [v.of_succ.comp_Hσ_eq hnaq, neg_eq_zero, ← assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : ∀ (v : HigherFacesVanish q φ), φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : q ≤ n
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ n + 1 ≤ (↑(⟨a, ⋯⟩ : Fin (n + 1)) : ℕ) + (q + 1)
have simp : a + (q + 1) ≤ a + (q + 1)
Tactic: simp only [hnaq, add_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : ∀ (v : HigherFacesVanish q φ), φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : q ≤ n
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ (φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2))) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) = 0
have eq : φ ≫ X.δ (⟨a, sorry⟩ : Fin (n + 1)).succ = 0
Tactic: have eq := v ⟨a, by lia⟩ (by
        simp only [hnaq, add_assoc]
        rfl)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
⊢ φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
have zero : ∀ (v : HigherFacesVanish 0 φ), φ ≫ HomologicalComplex.Hom.f (P 0) (n + 1) = φ
Tactic: induction q with
  | zero =>
    simp only [P_zero]
    apply comp_id
  | succ q hq =>
    simp only [P_succ, comp_add, HomologicalComplex.comp_f, HomologicalComplex.add_f_apply,
      comp_id, ← assoc, hq v.of_succ, add_eq_left]
    by_cases! hqn : n < q
    · exact v.of_succ.comp_Hσ_eq_zero hqn
    · obtain ⟨a, ha⟩ := Nat.le.dest hqn
      have hnaq : n = a + q := by lia
      simp only [v.of_succ.comp_Hσ_eq hnaq, neg_eq_zero, ← assoc]
      have eq := v ⟨a, by lia⟩ (by
        simp only [hnaq, add_assoc]
        rfl)
      simp only [Fin.succ_mk] at eq
      simp only [eq, zero_comp]
Cleared hypotheses: q, v
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
zero : ∀ (v : HigherFacesVanish 0 φ), φ ≫ HomologicalComplex.Hom.f (P 0) (n + 1) = φ
⊢ φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
have succ : ∀ (q : ℕ) (hq : ∀ (v : HigherFacesVanish q φ), φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ)
  (v : HigherFacesVanish (q + 1) φ), φ ≫ HomologicalComplex.Hom.f (P (q + 1)) (n + 1) = φ
Tactic: induction q with
  | zero =>
    simp only [P_zero]
    apply comp_id
  | succ q hq =>
    simp only [P_succ, comp_add, HomologicalComplex.comp_f, HomologicalComplex.add_f_apply,
      comp_id, ← assoc, hq v.of_succ, add_eq_left]
    by_cases! hqn : n < q
    · exact v.of_succ.comp_Hσ_eq_zero hqn
    · obtain ⟨a, ha⟩ := Nat.le.dest hqn
      have hnaq : n = a + q := by lia
      simp only [v.of_succ.comp_Hσ_eq hnaq, neg_eq_zero, ← assoc]
      have eq := v ⟨a, by lia⟩ (by
        simp only [hnaq, add_assoc]
        rfl)
      simp only [Fin.succ_mk] at eq
      simp only [eq, zero_comp]
Cleared hypotheses: q, v
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
⊢ φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ ↔ HigherFacesVanish q φ
have mp : φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ → HigherFacesVanish q φ
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
mp : φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ → HigherFacesVanish q φ
⊢ φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ ↔ HigherFacesVanish q φ
have mpr : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
hφ : φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
⊢ HigherFacesVanish q φ
have mp : HigherFacesVanish q (φ ≫ HomologicalComplex.Hom.f (P q) (n + 1))
Tactic: rw [← hφ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
hφ : φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
⊢ HigherFacesVanish q (φ ≫ HomologicalComplex.Hom.f (P q) (n + 1))
have mp : HigherFacesVanish.{v_1, u_1} (C := C) (X := X) (Y := X _⦋n + 1⦌) q
  (HomologicalComplex.Hom.f (P q) (n + 1) : HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
Tactic: apply HigherFacesVanish.of_comp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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 n : ℕ
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f (P q) n ≫ HomologicalComplex.Hom.f (P q) n) (HomologicalComplex.Hom.f (P q) n)
have zero : Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0)
  (HomologicalComplex.Hom.f (P q) 0 ≫ HomologicalComplex.Hom.f (P q) 0) (HomologicalComplex.Hom.f (P q) 0)
Tactic: rcases n with (_ | n)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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 n : ℕ
zero :
  Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0)
    (HomologicalComplex.Hom.f (P q) 0 ≫ HomologicalComplex.Hom.f (P q) 0) (HomologicalComplex.Hom.f (P q) 0)
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f (P q) n ≫ HomologicalComplex.Hom.f (P q) n) (HomologicalComplex.Hom.f (P q) n)
have succ : ∀ (n : ℕ),
  Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
    (HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (P q) (n + 1))
    (HomologicalComplex.Hom.f (P q) (n + 1))
Tactic: rcases n with (_ | n)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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 : ℕ
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0)
    (HomologicalComplex.Hom.f (P q) 0 ≫ HomologicalComplex.Hom.f (P q) 0) (HomologicalComplex.Hom.f (P q) 0)
have zero : Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0)
  (𝟙 (HomologicalComplex.X K[X] 0) ≫ 𝟙 (HomologicalComplex.X K[X] 0)) (𝟙 (HomologicalComplex.X K[X] 0))
Tactic: rw [P_f_0_eq q, comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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 : ℕ
zero :
  Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0)
    (𝟙 (HomologicalComplex.X K[X] 0) ≫ 𝟙 (HomologicalComplex.X K[X] 0)) (𝟙 (HomologicalComplex.X K[X] 0))
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0)
    (HomologicalComplex.Hom.f (P q) 0 ≫ HomologicalComplex.Hom.f (P q) 0) (HomologicalComplex.Hom.f (P q) 0)
have zero₁ : Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0) (𝟙 (HomologicalComplex.X K[X] 0))
  (𝟙 (HomologicalComplex.X K[X] 0))
Tactic: rw [P_f_0_eq q, comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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 : ℕ
⊢ Eq.{v_1 + 1} (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (P q ≫ P q) (P q)
have h : ∀ (n : ℕ),
  Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) (HomologicalComplex.Hom.f (P q ≫ P q) n)
    (HomologicalComplex.Hom.f (P q) n)
Tactic: ext n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Projections (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 : ℕ
⊢ Eq.{v_1 + 1} (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (Q q ≫ Q q) (Q q)
have h : ∀ (n : ℕ),
  Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) (HomologicalComplex.Hom.f (Q q ≫ Q q) n)
    (HomologicalComplex.Hom.f (Q q) n)
Tactic: ext n