awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralSequence.ComplexShape (goal)
Goal:
u : ℤ × ℤ
i i' j : ℕ × ℕ
h : (↑i.fst : ℤ) + u.fst = (↑j.fst : ℤ) ∧ (↑i.snd : ℤ) + u.snd = (↑j.snd : ℤ)
h_1 : (↑i'.fst : ℤ) + u.fst = (↑j.fst : ℤ) ∧ (↑i'.snd : ℤ) + u.snd = (↑j.snd : ℤ)
⊢ i = i'
have fst : i.fst = i'.fst
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralSequence.ComplexShape (goal)
Goal:
u : ℤ × ℤ
i i' j : ℕ × ℕ
h : (↑i.fst : ℤ) + u.fst = (↑j.fst : ℤ) ∧ (↑i.snd : ℤ) + u.snd = (↑j.snd : ℤ)
h_1 : (↑i'.fst : ℤ) + u.fst = (↑j.fst : ℤ) ∧ (↑i'.snd : ℤ) + u.snd = (↑j.snd : ℤ)
fst : i.fst = i'.fst
⊢ i = i'
have snd : i.snd = i'.snd
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralSequence.ComplexShape (goal)
Goal:
l : ℕ
u : ℤ × ℤ
i j j' : ℤ × Fin l
h : i.fst + u.fst = j.fst ∧ (↑(↑i.snd : ℕ) : ℤ) + u.snd = (↑(↑j.snd : ℕ) : ℤ)
h_1 : i.fst + u.fst = j'.fst ∧ (↑(↑i.snd : ℕ) : ℤ) + u.snd = (↑(↑j'.snd : ℕ) : ℤ)
⊢ j = j'
have fst : j.fst = j'.fst
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralSequence.ComplexShape (goal)
Goal:
l : ℕ
u : ℤ × ℤ
i j j' : ℤ × Fin l
h : i.fst + u.fst = j.fst ∧ (↑(↑i.snd : ℕ) : ℤ) + u.snd = (↑(↑j.snd : ℕ) : ℤ)
h_1 : i.fst + u.fst = j'.fst ∧ (↑(↑i.snd : ℕ) : ℤ) + u.snd = (↑(↑j'.snd : ℕ) : ℤ)
fst : j.fst = j'.fst
⊢ j = j'
have snd : (↑j.snd : ℕ) = (↑j'.snd : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralSequence.ComplexShape (goal)
Goal:
l : ℕ
u : ℤ × ℤ
i i' j : ℤ × Fin l
h : i.fst + u.fst = j.fst ∧ (↑(↑i.snd : ℕ) : ℤ) + u.snd = (↑(↑j.snd : ℕ) : ℤ)
h_1 : i'.fst + u.fst = j.fst ∧ (↑(↑i'.snd : ℕ) : ℤ) + u.snd = (↑(↑j.snd : ℕ) : ℤ)
⊢ i = i'
have fst : i.fst = i'.fst
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralSequence.ComplexShape (goal)
Goal:
l : ℕ
u : ℤ × ℤ
i i' j : ℤ × Fin l
h : i.fst + u.fst = j.fst ∧ (↑(↑i.snd : ℕ) : ℤ) + u.snd = (↑(↑j.snd : ℕ) : ℤ)
h_1 : i'.fst + u.fst = j.fst ∧ (↑(↑i'.snd : ℕ) : ℤ) + u.snd = (↑(↑j.snd : ℕ) : ℤ)
fst : i.fst = i'.fst
⊢ i = i'
have snd : (↑i.snd : ℕ) = (↑i'.snd : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ Eq (α := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (K.d₁ c₁₂ i₁ i₂ i₁₂) 0
have dsimp : HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
    (CategoryStruct.comp (Y := (K.X (c₁.next i₁)).X i₂) (HomologicalComplex.Hom.f (K.d i₁ (c₁.next i₁)) i₂)
      (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂)) =
  0
Tactic: dsimp [d₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      (CategoryStruct.comp (Y := (K.X (c₁.next i₁)).X i₂) (HomologicalComplex.Hom.f (K.d i₁ (c₁.next i₁)) i₂)
        (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂)) =
    0
have rw : HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
    (CategoryStruct.comp (Y := (K.X (c₁.next i₁)).X i₂) (0 : (K.X i₁).X i₂ ⟶ (K.X (c₁.next i₁)).X i₂)
      (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂ :
        K.toGradedObject (c₁.next i₁, i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂)) =
  0
Tactic: rw [K.shape_f _ _ h, zero_comp, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₁.Rel i₁ (c₁.next i₁)
rw :
  HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      (CategoryStruct.comp (Y := (K.X (c₁.next i₁)).X i₂) (0 : (K.X i₁).X i₂ ⟶ (K.X (c₁.next i₁)).X i₂)
        (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂ :
          K.toGradedObject (c₁.next i₁, i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂)) =
    0
⊢ HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      (CategoryStruct.comp (Y := (K.X (c₁.next i₁)).X i₂) (HomologicalComplex.Hom.f (K.d i₁ (c₁.next i₁)) i₂)
        (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂)) =
    0
have rw₁ : HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂)) 0 = 0
Tactic: rw [K.shape_f _ _ h, zero_comp, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₁.Rel i₁ (c₁.next i₁)
rw :
  HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      (CategoryStruct.comp (Y := (K.X (c₁.next i₁)).X i₂) (0 : (K.X i₁).X i₂ ⟶ (K.X (c₁.next i₁)).X i₂)
        (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂ :
          K.toGradedObject (c₁.next i₁, i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂)) =
    0
rw₁ : HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂)) 0 = 0
⊢ HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      (CategoryStruct.comp (Y := (K.X (c₁.next i₁)).X i₂) (HomologicalComplex.Hom.f (K.d i₁ (c₁.next i₁)) i₂)
        (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂)) =
    0
have rw₂ : Eq.{v_1 + 1} (α := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) 0 0
Tactic: rw [K.shape_f _ _ h, zero_comp, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ Eq (α := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (K.d₂ c₁₂ i₁ i₂ i₁₂) 0
have dsimp : HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂))
    (CategoryStruct.comp (Y := (K.X i₁).X (c₂.next i₂)) ((K.X i₁).d i₂ (c₂.next i₂))
      (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂)) =
  0
Tactic: dsimp [d₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂))
      (CategoryStruct.comp (Y := (K.X i₁).X (c₂.next i₂)) ((K.X i₁).d i₂ (c₂.next i₂))
        (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂)) =
    0
have rw : HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂))
    (CategoryStruct.comp (Y := (K.X i₁).X (c₂.next i₂)) (0 : (K.X i₁).X i₂ ⟶ (K.X i₁).X (c₂.next i₂))
      (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂ :
        K.toGradedObject (i₁, c₂.next i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂)) =
  0
Tactic: rw [HomologicalComplex.shape _ _ _ h, zero_comp, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₂.Rel i₂ (c₂.next i₂)
rw :
  HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂))
      (CategoryStruct.comp (Y := (K.X i₁).X (c₂.next i₂)) (0 : (K.X i₁).X i₂ ⟶ (K.X i₁).X (c₂.next i₂))
        (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂ :
          K.toGradedObject (i₁, c₂.next i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂)) =
    0
⊢ HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂))
      (CategoryStruct.comp (Y := (K.X i₁).X (c₂.next i₂)) ((K.X i₁).d i₂ (c₂.next i₂))
        (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂)) =
    0
have rw₁ : HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂)) 0 = 0
Tactic: rw [HomologicalComplex.shape _ _ _ h, zero_comp, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₂.Rel i₂ (c₂.next i₂)
rw :
  HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂))
      (CategoryStruct.comp (Y := (K.X i₁).X (c₂.next i₂)) (0 : (K.X i₁).X i₂ ⟶ (K.X i₁).X (c₂.next i₂))
        (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂ :
          K.toGradedObject (i₁, c₂.next i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂)) =
    0
rw₁ : HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂)) 0 = 0
⊢ HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂))
      (CategoryStruct.comp (Y := (K.X i₁).X (c₂.next i₂)) ((K.X i₁).d i₂ (c₂.next i₂))
        (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂)) =
    0
have rw₂ : Eq.{v_1 + 1} (α := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) 0 0
Tactic: rw [HomologicalComplex.shape _ _ _ h, zero_comp, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁ i₁' : I₁
h : c₁.Rel i₁ i₁'
i₂ : I₂
i₁₂ : I₁₂
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ =
    HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      ((K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂)
have obtain : ∀ (h : c₁.Rel i₁ (c₁.next i₁)),
  K.d₁ c₁₂ i₁ i₂ i₁₂ =
    HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      (CategoryStruct.comp (Y := (K.X (c₁.next i₁)).X i₂) (HomologicalComplex.Hom.f (K.d i₁ (c₁.next i₁)) i₂)
        (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂))
Tactic: obtain rfl := c₁.next_eq' h
Cleared hypotheses: i₁', h
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁ i₁' : I₁
h : c₁.Rel i₁ i₁'
i₂ : I₂
i₁₂ : I₁₂
h' : c₁.π c₂ c₁₂ (i₁', i₂) = i₁₂
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ =
    HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      ((K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂ h')
have rw : HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
    ((K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂) =
  HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
    ((K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂ h')
Tactic: rw [d₁_eq' K c₁₂ h i₂ i₁₂, K.toGradedObject.ιMapObjOrZero_eq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁ i₁' : I₁
h : c₁.Rel i₁ i₁'
i₂ : I₂
i₁₂ : I₁₂
h' : c₁.π c₂ c₁₂ (i₁', i₂) = i₁₂
rw :
  HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      ((K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂) =
    HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      ((K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂ h')
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ =
    HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      ((K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂ h')
have rw₁ : HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
    ((K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂ h') =
  HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
    ((K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂ h')
Tactic: rw [d₁_eq' K c₁₂ h i₂ i₁₂, K.toGradedObject.ιMapObjOrZero_eq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁ : I₁
i₂ i₂' : I₂
h : c₂.Rel i₂ i₂'
i₁₂ : I₁₂
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂ =
    HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂))
      ((K.X i₁).d i₂ i₂' ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂)
have obtain : ∀ (h : c₂.Rel i₂ (c₂.next i₂)),
  K.d₂ c₁₂ i₁ i₂ i₁₂ =
    HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂))
      (CategoryStruct.comp (Y := (K.X i₁).X (c₂.next i₂)) ((K.X i₁).d i₂ (c₂.next i₂))
        (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂))
Tactic: obtain rfl := c₂.next_eq' h
Cleared hypotheses: i₂', h
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁ : I₁
i₂ i₂' : I₂
h : c₂.Rel i₂ i₂'
i₁₂ : I₁₂
h' : c₁.π c₂ c₁₂ (i₁, i₂') = i₁₂
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂ =
    HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂))
      ((K.X i₁).d i₂ i₂' ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂ h')
have rw : HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂))
    ((K.X i₁).d i₂ i₂' ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂) =
  HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂))
    ((K.X i₁).d i₂ i₂' ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂ h')
Tactic: rw [d₂_eq' K c₁₂ i₁ h i₁₂, K.toGradedObject.ιMapObjOrZero_eq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁ : I₁
i₂ i₂' : I₂
h : c₂.Rel i₂ i₂'
i₁₂ : I₁₂
h' : c₁.π c₂ c₁₂ (i₁, i₂') = i₁₂
rw :
  HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂))
      ((K.X i₁).d i₂ i₂' ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂) =
    HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂))
      ((K.X i₁).d i₂ i₂' ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂ h')
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂ =
    HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂))
      ((K.X i₁).d i₂ i₂' ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂ h')
have rw₁ : HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂))
    ((K.X i₁).d i₂ i₂' ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂ h') =
  HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂))
    ((K.X i₁).d i₂ i₂' ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂ h')
Tactic: rw [d₂_eq' K c₁₂ i₁ h i₁₂, K.toGradedObject.ιMapObjOrZero_eq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
⊢ Eq (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂') (K.D₁ c₁₂ i₁₂ i₁₂') 0
have hfg : ∀ (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂),
  Eq (α := K.toGradedObject (i₁, i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
    (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h ≫ K.D₁ c₁₂ i₁₂ i₁₂')
    (CategoryStruct.comp (Y := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂)
      (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h) 0)
Tactic: ext ⟨i₁, i₂⟩ h
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ Eq (α := K.toGradedObject (i₁, i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
    (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h ≫ K.D₁ c₁₂ i₁₂ i₁₂')
    (CategoryStruct.comp (Y := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂)
      (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h) 0)
have hfg : Eq (α := K.toGradedObject (i₁, i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂') (K.d₁ c₁₂ i₁ i₂ i₁₂') 0
Tactic: simp only [totalAux.ιMapObj_D₁, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ Eq (α := K.toGradedObject (i₁, i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂') (K.d₁ c₁₂ i₁ i₂ i₁₂') 0
have pos : ∀ (h₁ : c₁.Rel i₁ (c₁.next i₁)),
  Eq (α := K.toGradedObject (i₁, i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂') (K.d₁ c₁₂ i₁ i₂ i₁₂') 0
Tactic: by_cases h₁ : c₁.Rel i₁ (c₁.next i₁)
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
pos :
  ∀ (h₁ : c₁.Rel i₁ (c₁.next i₁)),
    Eq (α := K.toGradedObject (i₁, i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂') (K.d₁ c₁₂ i₁ i₂ i₁₂') 0
⊢ Eq (α := K.toGradedObject (i₁, i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂') (K.d₁ c₁₂ i₁ i₂ i₁₂') 0
have neg : ∀ (h₁ : ¬c₁.Rel i₁ (c₁.next i₁)),
  Eq (α := K.toGradedObject (i₁, i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂') (K.d₁ c₁₂ i₁ i₂ i₁₂') 0
Tactic: by_cases h₁ : c₁.Rel i₁ (c₁.next i₁)
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₁ : c₁.Rel i₁ (c₁.next i₁)
⊢ Eq (α := K.toGradedObject (i₁, i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂') (K.d₁ c₁₂ i₁ i₂ i₁₂') 0
have pos : c₁.π c₂ c₁₂ (c₁.next i₁, i₂) ≠ i₁₂'
Tactic: rw [K.d₁_eq_zero' c₁₂ h₁ i₂ i₁₂']
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
⊢ Eq (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂') (K.D₂ c₁₂ i₁₂ i₁₂') 0
have hfg : ∀ (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂),
  Eq (α := K.toGradedObject (i₁, i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
    (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h ≫ K.D₂ c₁₂ i₁₂ i₁₂')
    (CategoryStruct.comp (Y := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂)
      (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h) 0)
Tactic: ext ⟨i₁, i₂⟩ h