awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁₂
h₁ : c₁₂.Rel 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₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'') (-K.d₁ c₁₂ i₁ i₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'')
have pos : K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ 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.ιMapObj (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂' sorry)) ≫
      K.D₂ c₁₂ i₁₂' i₁₂''
Tactic: rw [totalAux.d₁_eq K 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₁₂'' : I₁₂
h₁ : c₁₂.Rel 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₁)
pos :
  K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ 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.ιMapObj (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂' ⋯)) ≫
        K.D₂ c₁₂ i₁₂' i₁₂''
⊢ Eq (α := K.toGradedObject (i₁, i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'')
    (K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'') (-K.d₁ c₁₂ i₁ i₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'')
have pos₁ : c₁.π c₂ c₁₂ (c₁.next i₁, i₂) = i₁₂'
Tactic: rw [totalAux.d₁_eq K 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₁₂'' : I₁₂
h₁ : c₁₂.Rel 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₁)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ 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.ιMapObj (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂' ⋯)) ≫
        K.D₂ c₁₂ i₁₂' i₁₂''
have pos : K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' =
  -HSMul.hSMul (β := K.toGradedObject (i₁, 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.d₂ c₁₂ (c₁.next i₁) i₂ i₁₂''))
Tactic: simp only [Linear.units_smul_comp, assoc, totalAux.ιMapObj_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₁₂
h₁ : c₁₂.Rel 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₁)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' =
    -HSMul.hSMul (β := K.toGradedObject (i₁, 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.d₂ c₁₂ (c₁.next i₁) i₂ i₁₂''))
have pos : ∀ (h₄ : c₂.Rel i₂ (c₂.next i₂)),
  K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' =
    -HSMul.hSMul (β := K.toGradedObject (i₁, 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.d₂ c₁₂ (c₁.next i₁) i₂ i₁₂''))
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₁₂'' : I₁₂
h₁ : c₁₂.Rel 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₁)
pos :
  ∀ (h₄ : c₂.Rel i₂ (c₂.next i₂)),
    K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' =
      -HSMul.hSMul (β := K.toGradedObject (i₁, 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.d₂ c₁₂ (c₁.next i₁) i₂ i₁₂''))
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' =
    -HSMul.hSMul (β := K.toGradedObject (i₁, 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.d₂ c₁₂ (c₁.next i₁) i₂ i₁₂''))
have neg : ∀ (h₄ : ¬c₂.Rel i₂ (c₂.next i₂)),
  K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' =
    -HSMul.hSMul (β := K.toGradedObject (i₁, 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.d₂ c₁₂ (c₁.next i₁) i₂ i₁₂''))
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₁₂'' : I₁₂
h₁ : c₁₂.Rel 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₁)
h₄ : c₂.Rel i₂ (c₂.next i₂)
⊢ c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'
have rw : c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = c₁₂.next i₁₂
Tactic: rw [← c₁₂.next_eq' h₁, ← h, ComplexShape.next_π₂ c₁ c₁₂ 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₁₂
h₁ : c₁₂.Rel 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₁)
h₄ : c₂.Rel i₂ (c₂.next i₂)
rw : c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = c₁₂.next i₁₂
⊢ c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'
have rw₁ : c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))
Tactic: rw [← c₁₂.next_eq' h₁, ← h, ComplexShape.next_π₂ c₁ c₁₂ 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₁₂
h₁ : c₁₂.Rel 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₁)
h₄ : c₂.Rel i₂ (c₂.next i₂)
rw : c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = c₁₂.next i₁₂
rw₁ : c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))
⊢ c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'
have rw₂ : c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = c₁.π c₂ c₁₂ (i₁, c₂.next i₂)
Tactic: rw [← c₁₂.next_eq' h₁, ← h, ComplexShape.next_π₂ c₁ c₁₂ i₁ h₄]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (hypothesis)
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₁₂
h₁ : c₁₂.Rel 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₁)
h₄ : c₂.Rel i₂ (c₂.next i₂)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' =
    -HSMul.hSMul (β := K.toGradedObject (i₁, 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.d₂ c₁₂ (c₁.next i₁) i₂ i₁₂''))
have h₅ : c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'
Tactic: have h₅ : ComplexShape.π c₁ c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂' := by
            rw [← c₁₂.next_eq' h₁, ← h, ComplexShape.next_π₂ c₁ c₁₂ 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₁₂
h₁ : c₁₂.Rel 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₁)
h₄ : c₂.Rel i₂ (c₂.next i₂)
h₅ : c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'
⊢ c₁.π c₂ c₁₂ (c₁.next i₁, c₂.next i₂) = i₁₂''
have rw : c₁.π c₂ c₁₂ (c₁.next i₁, c₂.next i₂) = c₁₂.next i₁₂'
Tactic: rw [← c₁₂.next_eq' h₂, ← ComplexShape.next_π₁ c₂ c₁₂ h₃, 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₁₂
h₁ : c₁₂.Rel 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₁)
h₄ : c₂.Rel i₂ (c₂.next i₂)
h₅ : c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'
rw : c₁.π c₂ c₁₂ (c₁.next i₁, c₂.next i₂) = c₁₂.next i₁₂'
⊢ c₁.π c₂ c₁₂ (c₁.next i₁, c₂.next i₂) = i₁₂''
have rw₁ : c₁₂.next (c₁.π c₂ c₁₂ (i₁, c₂.next i₂)) = c₁₂.next i₁₂'
Tactic: rw [← c₁₂.next_eq' h₂, ← ComplexShape.next_π₁ c₂ c₁₂ h₃, 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₁₂
h₁ : c₁₂.Rel 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₁)
h₄ : c₂.Rel i₂ (c₂.next i₂)
h₅ : c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'
rw : c₁.π c₂ c₁₂ (c₁.next i₁, c₂.next i₂) = c₁₂.next i₁₂'
rw₁ : c₁₂.next (c₁.π c₂ c₁₂ (i₁, c₂.next i₂)) = c₁₂.next i₁₂'
⊢ c₁.π c₂ c₁₂ (c₁.next i₁, c₂.next i₂) = i₁₂''
have rw₂ : c₁₂.next i₁₂' = c₁₂.next i₁₂'
Tactic: rw [← c₁₂.next_eq' h₂, ← ComplexShape.next_π₁ c₂ c₁₂ h₃, h₅]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (hypothesis)
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₁₂
h₁ : c₁₂.Rel 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₁)
h₄ : c₂.Rel i₂ (c₂.next i₂)
h₅ : c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' =
    -HSMul.hSMul (β := K.toGradedObject (i₁, 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.d₂ c₁₂ (c₁.next i₁) i₂ i₁₂''))
have h₆ : c₁.π c₂ c₁₂ (c₁.next i₁, c₂.next i₂) = i₁₂''
Tactic: have h₆ : ComplexShape.π c₁ c₂ c₁₂ (c₁.next i₁, c₂.next i₂) = i₁₂'' := by
            rw [← c₁₂.next_eq' h₂, ← ComplexShape.next_π₁ c₂ c₁₂ h₃, 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₁₂
h₁ : c₁₂.Rel 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₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'') (-K.d₁ c₁₂ i₁ i₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'')
have neg : Eq (α := K.toGradedObject (i₁, i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'')
  (K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'') 0
Tactic: rw [K.d₁_eq_zero c₁₂ _ _ _ h₃, zero_comp, neg_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₁₂
h₁ : c₁₂.Rel 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₁₂' ≫ K.D₁ c₁₂ 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₁₂' ≫ K.D₁ c₁₂ 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₁₂'' : I₁₂
h₁ : c₁₂.Rel 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₁)
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₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'') 0
⊢ Eq (α := K.toGradedObject (i₁, i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'')
    (K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ 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₁₂' ≫ K.D₁ c₁₂ 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₁₂'' : I₁₂
h₁ : c₁₂.Rel 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₁)
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₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'') 0
have pos : 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.ιMapObj (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂' sorry)) ≫
    K.D₁ c₁₂ i₁₂' i₁₂'' =
  0
Tactic: rw [totalAux.d₂_eq K c₁₂ i₁ h₄ 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₁₂'' : I₁₂
h₁ : c₁₂.Rel 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₁)
h₄ : c₂.Rel i₂ (c₂.next i₂)
pos :
  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.ιMapObj (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂' ⋯)) ≫
      K.D₁ c₁₂ i₁₂' i₁₂'' =
    0
⊢ Eq (α := K.toGradedObject (i₁, i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'')
    (K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'') 0
have pos₁ : c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'
Tactic: rw [totalAux.d₂_eq K c₁₂ i₁ h₄ 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₁₂'' : I₁₂
h₁ : c₁₂.Rel 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₁)
h₄ : c₂.Rel i₂ (c₂.next i₂)
⊢ c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'
have pos : c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂)) = i₁₂'
Tactic: rw [← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₄, ← c₁₂.next_eq' h₁, 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₁₂
h₁ : c₁₂.Rel 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₁)
h₄ : c₂.Rel i₂ (c₂.next i₂)
pos : c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂)) = i₁₂'
⊢ c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'
have pos₁ : c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂)) = c₁₂.next i₁₂
Tactic: rw [← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₄, ← c₁₂.next_eq' h₁, 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₁₂
h₁ : c₁₂.Rel 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₁)
h₄ : c₂.Rel i₂ (c₂.next i₂)
pos : c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂)) = i₁₂'
pos₁ : c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂)) = c₁₂.next i₁₂
⊢ c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'
have pos₂ : c₁₂.next i₁₂ = c₁₂.next i₁₂
Tactic: rw [← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₄, ← c₁₂.next_eq' h₁, 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₁₂
h₁ : c₁₂.Rel 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₁)
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.ιMapObj (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂' ⋯)) ≫
      K.D₁ c₁₂ i₁₂' i₁₂'' =
    0
have pos : HSMul.hSMul (β := K.toGradedObject (i₁, 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.d₁ c₁₂ i₁ (c₂.next i₂) i₁₂'')) =
  0
Tactic: simp only [Linear.units_smul_comp, assoc, totalAux.ιMapObj_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₁₂
h₁ : c₁₂.Rel 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₁)
h₄ : c₂.Rel i₂ (c₂.next i₂)
⊢ HSMul.hSMul (β := K.toGradedObject (i₁, 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.d₁ c₁₂ i₁ (c₂.next i₂) i₁₂'')) =
    0
have pos : HSMul.hSMul (β := K.toGradedObject (i₁, 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₂)) 0) =
  0
Tactic: rw [K.d₁_eq_zero c₁₂ _ _ _ h₃, comp_zero, smul_zero]