awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst_2 : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n + 1⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op : X _⦋n + 1⦌ ⟶ X _⦋n⦌)
have pos : Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
  (CategoryStruct.comp (Y := X _⦋n⦌)
      (HomologicalComplex.d K[X] (n + 1) n : HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
      (HomologicalComplex.Hom.f PInfty n) :
    X _⦋n + 1⦌ ⟶ X _⦋n⦌)
  (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op : X _⦋n + 1⦌ ⟶ X _⦋n⦌)
Tactic: simp only [Γ₀.Obj.Termwise.mapMono_δ₀' _ i hi]
-- 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 : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst_2 : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (HomologicalComplex.d K[X] (n + 1) n : HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op : X _⦋n + 1⦌ ⟶ X _⦋n⦌)
have pos : Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
  (HomologicalComplex.Hom.f PInfty (n + 1) ≫ ∑ i : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i :
    HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
  (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op)
Tactic: rw [← PInfty.comm _ n, AlternatingFaceMapComplex.obj_d_eq]
-- 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 : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst_2 : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ ∑ i : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i :
      HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op)
have pos : Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
  (∑ j : Fin (n + 2), HomologicalComplex.Hom.f PInfty (n + 1) ≫ (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j) :
    HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
  (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op)
Tactic: simp only [Preadditive.comp_sum]
-- 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 : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst_2 : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (∑ j : Fin (n + 2), HomologicalComplex.Hom.f PInfty (n + 1) ≫ (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j) :
      HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op)
have pos : Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
  (HomologicalComplex.Hom.f PInfty (n + 1) ≫
      HSMul.hSMul (β := X _⦋n + 1⦌ ⟶ X _⦋n⦌) (HPow.hPow (α := ℤ) (-1) (↑0 : ℕ)) (X.δ 0) :
    HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
  (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op)
Tactic: rw [Finset.sum_eq_single (0 : Fin (n + 2))]
-- 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 : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst_2 : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
pos :
  Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫
        HSMul.hSMul (β := X _⦋n + 1⦌ ⟶ X _⦋n⦌) (HPow.hPow (α := ℤ) (-1) (↑0 : ℕ)) (X.δ 0) :
      HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op)
⊢ Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (∑ j : Fin (n + 2), HomologicalComplex.Hom.f PInfty (n + 1) ≫ (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j) :
      HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op)
have pos₁ : ∀ (b : Fin (n + 2)),
  Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ b →
    b ≠ 0 →
      Eq (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
        (HomologicalComplex.Hom.f PInfty (n + 1) ≫ (HPow.hPow (α := ℤ) (-1) (↑b : ℕ) • X.δ b)) 0
Tactic: rw [Finset.sum_eq_single (0 : Fin (n + 2))]
-- 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 : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst_2 : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
pos :
  Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫
        HSMul.hSMul (β := X _⦋n + 1⦌ ⟶ X _⦋n⦌) (HPow.hPow (α := ℤ) (-1) (↑0 : ℕ)) (X.δ 0) :
      HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op)
pos₁ :
  ∀ (b : Fin (n + 2)),
    Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ b →
      b ≠ 0 →
        Eq (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
          (HomologicalComplex.Hom.f PInfty (n + 1) ≫ (HPow.hPow (α := ℤ) (-1) (↑b : ℕ) • X.δ b)) 0
⊢ Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (∑ j : Fin (n + 2), HomologicalComplex.Hom.f PInfty (n + 1) ≫ (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j) :
      HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op)
have pos₂ : 0 ∉ Finset.univ →
  Eq (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫
      HSMul.hSMul (β := X _⦋n + 1⦌ ⟶ X _⦋n⦌) (HPow.hPow (α := ℤ) (-1) (↑0 : ℕ)) (X.δ 0))
    0
Tactic: rw [Finset.sum_eq_single (0 : Fin (n + 2))]
-- 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 : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst_2 : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
h_1 : Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ b
hb : b ≠ 0
⊢ ¬Isδ₀ (SimplexCategory.δ b)
have rw : ¬b = 0
Tactic: rw [Isδ₀.iff]
-- 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 : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst_2 : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
h_1 : Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ b
hb : b ≠ 0
⊢ Eq (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ (HPow.hPow (α := ℤ) (-1) (↑b : ℕ) • X.δ b)) 0
have pos : HSMul.hSMul (β := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n) (HPow.hPow (α := ℤ) (-1) (↑b : ℕ))
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.δ b) =
  0
Tactic: rw [Preadditive.comp_zsmul, SimplicialObject.δ,
        PInfty_comp_map_mono_eq_zero X (SimplexCategory.δ b) h
          (by
            rw [Isδ₀.iff]
            exact hb),
        zsmul_zero]
-- 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 : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst_2 : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
h_1 : Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ b
hb : b ≠ 0
pos :
  HSMul.hSMul (β := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n) (HPow.hPow (α := ℤ) (-1) (↑b : ℕ))
      (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.δ b) =
    0
⊢ Eq (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ (HPow.hPow (α := ℤ) (-1) (↑b : ℕ) • X.δ b)) 0
have pos₁ : HSMul.hSMul (β := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n) (HPow.hPow (α := ℤ) (-1) (↑b : ℕ))
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map (SimplexCategory.δ b).op) =
  0
Tactic: rw [Preadditive.comp_zsmul, SimplicialObject.δ,
        PInfty_comp_map_mono_eq_zero X (SimplexCategory.δ b) h
          (by
            rw [Isδ₀.iff]
            exact hb),
        zsmul_zero]
-- 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 : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst_2 : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
h_1 : Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ b
hb : b ≠ 0
pos :
  HSMul.hSMul (β := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n) (HPow.hPow (α := ℤ) (-1) (↑b : ℕ))
      (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.δ b) =
    0
pos₁ :
  HSMul.hSMul (β := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n) (HPow.hPow (α := ℤ) (-1) (↑b : ℕ))
      (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map (SimplexCategory.δ b).op) =
    0
⊢ Eq (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ (HPow.hPow (α := ℤ) (-1) (↑b : ℕ) • X.δ b)) 0
have pos₂ : HSMul.hSMul (β := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n) (HPow.hPow (α := ℤ) (-1) (↑b : ℕ))
    0 =
  0
Tactic: rw [Preadditive.comp_zsmul, SimplicialObject.δ,
        PInfty_comp_map_mono_eq_zero X (SimplexCategory.δ b) h
          (by
            rw [Isδ₀.iff]
            exact hb),
        zsmul_zero]
-- 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 : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst_2 : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
h_1 : Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ b
hb : b ≠ 0
pos :
  HSMul.hSMul (β := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n) (HPow.hPow (α := ℤ) (-1) (↑b : ℕ))
      (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.δ b) =
    0
pos₁ :
  HSMul.hSMul (β := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n) (HPow.hPow (α := ℤ) (-1) (↑b : ℕ))
      (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map (SimplexCategory.δ b).op) =
    0
pos₂ :
  HSMul.hSMul (β := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n) (HPow.hPow (α := ℤ) (-1) (↑b : ℕ))
      0 =
    0
⊢ Eq (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ (HPow.hPow (α := ℤ) (-1) (↑b : ℕ) • X.δ b)) 0
have pos₃ : Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n) 0 0
Tactic: rw [Preadditive.comp_zsmul, SimplicialObject.δ,
        PInfty_comp_map_mono_eq_zero X (SimplexCategory.δ b) h
          (by
            rw [Isδ₀.iff]
            exact hb),
        zsmul_zero]
-- 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 : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst_2 : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫
        HSMul.hSMul (β := X _⦋n + 1⦌ ⟶ X _⦋n⦌) (HPow.hPow (α := ℤ) (-1) (↑0 : ℕ)) (X.δ 0) :
      HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op)
have pos : Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
  (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.δ 0 : HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] n)
  (CategoryStruct.comp (Y := X _⦋n + 1⦌)
    (HomologicalComplex.Hom.f PInfty (n + 1) : HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
    (X.map (Quiver.Hom.op (SimplexCategory.δ 0))))
Tactic: simp only [hi.eq_δ₀, Fin.val_zero, pow_zero, one_zsmul]
-- 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 n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n'⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
have neg : Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌) (0 : X _⦋n'⦌ ⟶ X _⦋n⦌) (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
Tactic: rw [Γ₀.Obj.Termwise.mapMono_eq_zero _ i _ hi, zero_comp]
-- 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 n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
neg :
  Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌) (0 : X _⦋n'⦌ ⟶ X _⦋n⦌) (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
⊢ Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n'⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
have rw : ⦋n'⦌ ≠ ⦋n⦌
Tactic: rw [Γ₀.Obj.Termwise.mapMono_eq_zero _ i _ hi, zero_comp]
-- 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 n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌) (0 : X _⦋n'⦌ ⟶ X _⦋n⦌) (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
have neg : ⦋n⦌.len ≠ n'
Tactic: rw [PInfty_comp_map_mono_eq_zero]
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
⊢ ((Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X).X.map θ ≫
      Splitting.desc (Γ₀.splitting K[X]) Δ' fun (A : Splitting.IndexSet Δ') ↦
        HomologicalComplex.Hom.f PInfty
            (unop (A.fst (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }))).len ≫
          X.map A.e.op) =
    (Splitting.desc (Γ₀.splitting K[X]) Δ fun (A : Splitting.IndexSet Δ) ↦
        HomologicalComplex.Hom.f PInfty
            (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
          X.map A.e.op) ≫
      (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).map θ
have h : ∀ (A : Splitting.IndexSet Δ),
  Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X])) Δ A ⟶
      (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).obj Δ')
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K[X]) Δ) A ≫
      (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X).X.map θ ≫
        Splitting.desc (Γ₀.splitting K[X]) Δ' fun (A : Splitting.IndexSet Δ') ↦
          HomologicalComplex.Hom.f PInfty
              (unop (A.fst (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }))).len ≫
            X.map A.e.op)
    (CategoryStruct.comp (Y :=
      Cocone.pt (F := Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X])) Δ))
        (Splitting.cofan (Γ₀.splitting K[X]) Δ))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K[X]) Δ) A)
      ((Splitting.desc (Γ₀.splitting K[X]) Δ fun (A : Splitting.IndexSet Δ) ↦
          HomologicalComplex.Hom.f PInfty
              (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
            X.map A.e.op) ≫
        (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).map θ))
Tactic: apply (Γ₀.splitting K[X]).hom_ext'
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X])) Δ A ⟶
      (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).obj Δ')
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K[X]) Δ) A ≫
      (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X).X.map θ ≫
        Splitting.desc (Γ₀.splitting K[X]) Δ' fun (A : Splitting.IndexSet Δ') ↦
          HomologicalComplex.Hom.f PInfty
              (unop (A.fst (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }))).len ≫
            X.map A.e.op)
    (CategoryStruct.comp (Y :=
      Cocone.pt (F := Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X])) Δ))
        (Splitting.cofan (Γ₀.splitting K[X]) Δ))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K[X]) Δ) A)
      ((Splitting.desc (Γ₀.splitting K[X]) Δ fun (A : Splitting.IndexSet Δ) ↦
          HomologicalComplex.Hom.f PInfty
              (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
            X.map A.e.op) ≫
        (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).map θ))
have h : Eq (α :=
  Splitting.summand (Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X])) Δ A ⟶
    (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).obj Δ')
  (Cofan.inj (Splitting.cofan (Γ₀.splitting K[X]) Δ) A ≫
    (Γ₀.obj K[X]).map θ ≫
      Splitting.desc (Γ₀.splitting K[X]) Δ' fun (A : Splitting.IndexSet Δ') ↦
        HomologicalComplex.Hom.f PInfty
            (unop (A.fst (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }))).len ≫
          X.map A.e.op)
  (CategoryStruct.comp (Y :=
    Cocone.pt (F := Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X])) Δ))
      (Splitting.cofan (Γ₀.splitting K[X]) Δ))
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K[X]) Δ) A)
    ((Splitting.desc (Γ₀.splitting K[X]) Δ fun (A : Splitting.IndexSet Δ) ↦
        HomologicalComplex.Hom.f PInfty
            (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
          X.map A.e.op) ≫
      (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).map θ))
Tactic: change _ ≫ (Γ₀.obj K[X]).map θ ≫ _ = _
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X])) Δ A ⟶
      (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).obj Δ')
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K[X]) Δ) A ≫
      (Γ₀.obj K[X]).map θ ≫
        Splitting.desc (Γ₀.splitting K[X]) Δ' fun (A : Splitting.IndexSet Δ') ↦
          HomologicalComplex.Hom.f PInfty
              (unop (A.fst (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }))).len ≫
            X.map A.e.op)
    (CategoryStruct.comp (Y :=
      Cocone.pt (F := Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X])) Δ))
        (Splitting.cofan (Γ₀.splitting K[X]) Δ))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K[X]) Δ) A)
      ((Splitting.desc (Γ₀.splitting K[X]) Δ fun (A : Splitting.IndexSet Δ) ↦
          HomologicalComplex.Hom.f PInfty
              (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
            X.map A.e.op) ≫
        (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).map θ))
have h : CategoryStruct.comp (Y := HomologicalComplex.X K[X] (image (θ.unop ≫ A.e)).len)
    (Γ₀.Obj.Termwise.mapMono K[X] (image.ι (θ.unop ≫ A.e)))
    (HomologicalComplex.Hom.f PInfty
        (unop ((A.pull θ).fst (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }))).len ≫
      X.map (A.pull θ).e.op) =
  HomologicalComplex.Hom.f PInfty
      (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
    X.map A.e.op ≫ (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).map θ
Tactic: simp only [Splitting.ι_desc_assoc, assoc, Γ₀.Obj.map_on_summand'_assoc,
              Splitting.ι_desc]
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ CategoryStruct.comp (Y := HomologicalComplex.X K[X] (image (θ.unop ≫ A.e)).len)
      (Γ₀.Obj.Termwise.mapMono K[X] (image.ι (θ.unop ≫ A.e)))
      (HomologicalComplex.Hom.f PInfty
          (unop ((A.pull θ).fst (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }))).len ≫
        X.map (A.pull θ).e.op) =
    HomologicalComplex.Hom.f PInfty
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      X.map A.e.op ≫ (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).map θ
have h : HomologicalComplex.Hom.f PInfty
      (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
    X.map (Quiver.Hom.op (image.ι (θ.unop ≫ A.e))) ≫ X.map (A.pull θ).e.op =
  HomologicalComplex.Hom.f PInfty
      (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
    X.map A.e.op ≫ (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).map θ
Tactic: erw [Γ₀_obj_termwise_mapMono_comp_PInfty_assoc X (image.ι (θ.unop ≫ A.e))]
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ HomologicalComplex.Hom.f PInfty
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      X.map (Quiver.Hom.op (image.ι (θ.unop ≫ A.e))) ≫ X.map (A.pull θ).e.op =
    HomologicalComplex.Hom.f PInfty
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      X.map A.e.op ≫ (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).map θ
have h : HomologicalComplex.Hom.f PInfty
      (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
    X.map (Quiver.Hom.op (image.ι (θ.unop ≫ A.e))) ≫ X.map (A.pull θ).e.op =
  HomologicalComplex.Hom.f PInfty
      (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
    X.map A.e.op ≫ X.map θ
Tactic: dsimp only [toKaroubi]