awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.TotalComplex
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 (c₂.next i₂) (c₂.next (c₂.next i₂))
pos : c₁.π c₂ c₁₂ (i₁, c₂.next (c₂.next 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 i₁).X (c₂.next i₂)) ((K.X i₁).d i₂ (c₂.next i₂))
        (K.d₂ c₁₂ i₁ (c₂.next i₂) i₁₂'')) =
    0

Tactic:
rw [totalAux.d₂_eq K c₁₂ i₁ h₄ i₁₂'', Linear.comp_units_smul,
            HomologicalComplex.d_comp_d_assoc, zero_comp, smul_zero, smul_zero]

Premises used: HomologicalComplex₂.totalAux.d₂_eq, HomologicalComplex.d_comp_d_assoc, smul_zero, CategoryTheory.Linear.comp_units_smul, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.TotalComplex
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 (c₂.next i₂) (c₂.next (c₂.next i₂))
pos : c₁₂.next (c₁.π c₂ c₁₂ (i₁, c₂.next i₂)) = i₁₂''
pos₁ : c₁₂.next (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))) = i₁₂''
pos₂ : c₁₂.next (c₁₂.next i₁₂) = i₁₂''
pos₃ : c₁₂.next i₁₂' = i₁₂''
pos₄ pos₅ : i₁₂'' = i₁₂''
⊢ c₁.π c₂ c₁₂ (i₁, c₂.next (c₂.next i₂)) = i₁₂''

Tactic:
rw [← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₄, ← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₃,
            h, c₁₂.next_eq' h₁, c₁₂.next_eq' h₂]

Premises used: ComplexShape.next_π₂, ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.TotalComplex
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 (c₂.next i₂) (c₂.next (c₂.next i₂))
neg :
  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
neg₁ :
  HSMul.hSMul (β := K.toGradedObject (i₁, i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'') (c₁.ε₂ c₂ c₁₂ (i₁, i₂)) 0 =
    0
neg₂ neg₃ : Eq.{v_1 + 1} (α := K.toGradedObject (i₁, i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'') 0 0
⊢ 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:
rw [K.d₂_eq_zero c₁₂ _ _ _ h₄, comp_zero, smul_zero]

Premises used: HomologicalComplex₂.d₂_eq_zero, CategoryTheory.Limits.comp_zero, smul_zero
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₂)
neg : Eq (α := K.toGradedObject (i₁, i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'') (0 ≫ K.D₂ c₁₂ i₁₂' i₁₂'') 0
neg₁ neg₂ : Eq.{v_1 + 1} (α := K.toGradedObject (i₁, i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'') 0 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

Tactic:
rw [K.d₂_eq_zero c₁₂ _ _ _ h₃, zero_comp]

Premises used: HomologicalComplex₂.d₂_eq_zero, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂''
neg :
  Eq (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'')
    (K.D₂ c₁₂ i₁₂ i₁₂' ≫ 0) 0
neg₁ neg₂ :
  Eq.{v_1 + 1} (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'') 0 0
⊢ Eq (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'')
    (K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'') 0

Tactic:
rw [K.D₂_shape c₁₂ _ _ h₂, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, HomologicalComplex₂.D₂_shape
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂'
neg :
  Eq (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'')
    (0 ≫ K.D₂ c₁₂ i₁₂' i₁₂'') 0
neg₁ neg₂ :
  Eq.{v_1 + 1} (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'') 0 0
⊢ Eq (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'')
    (K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'') 0

Tactic:
rw [K.D₂_shape c₁₂ _ _ h₁, zero_comp]

Premises used: HomologicalComplex₂.D₂_shape, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂
pos :
  ∀ (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₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'') (-K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'')
neg :
  ∀ (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₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'') (-K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'')
⊢ Eq (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'')
    (K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'') (-K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'')

Tactic:
by_cases h₁ : c₁₂.Rel i₁₂ i₁₂'

Premises used: ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂'
pos :
  ∀ (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₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'') (-K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'')
neg :
  ∀ (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₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'') (-K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'')
⊢ Eq (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'')
    (K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'') (-K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'')

Tactic:
by_cases h₂ : c₁₂.Rel i₁₂' i₁₂''

Premises used: ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂''
pos :
  ∀ (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₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'')
      (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h ≫ (-K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂''))
⊢ Eq (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'')
    (K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'') (-K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'')

Tactic:
ext ⟨i₁, i₂⟩ h
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂
pos :
  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₁₂'')
⊢ 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₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'')
    (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h ≫ (-K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂''))

Tactic:
simp only [totalAux.ιMapObj_D₂_assoc, comp_neg, totalAux.ιMapObj_D₁_assoc]

Premises used: CategoryTheory.Preadditive.comp_neg, HomologicalComplex₂.totalAux.ιMapObj_D₂_assoc, HomologicalComplex₂.totalAux.ιMapObj_D₁_assoc
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂
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₁₂'') (-K.d₁ c₁₂ i₁ i₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'')
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₁₂'') (-K.d₁ c₁₂ 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₁₂'')

Tactic:
by_cases h₃ : c₁.Rel i₁ (c₁.next i₁)

Premises used: ComplexShape.next, ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂''
pos₁ : c₁.π c₂ c₁₂ (c₁.next i₁, 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₁₂'')

Tactic:
rw [totalAux.d₁_eq K c₁₂ h₃ i₂ i₁₂']

Premises used: HomologicalComplex₂.totalAux.d₁_eq
-- Module: Mathlib.Algebra.Homology.TotalComplex
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.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.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₁₂''

Tactic:
simp only [Linear.units_smul_comp, assoc, totalAux.ιMapObj_D₂]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Linear.units_smul_comp, HomologicalComplex₂.totalAux.ιMapObj_D₂
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂''))
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₁₂''))
⊢ 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₂)

Premises used: ComplexShape.next, ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₂))
rw₂ rw₃ : c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = c₁.π c₂ c₁₂ (i₁, c₂.next i₂)
⊢ c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'

Tactic:
rw [← c₁₂.next_eq' h₁, ← h, ComplexShape.next_π₂ c₁ c₁₂ i₁ h₄]

Premises used: ComplexShape.next_π₂, ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂'

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₄]
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂'
rw₂ rw₃ : c₁₂.next i₁₂' = c₁₂.next i₁₂'
⊢ c₁.π c₂ c₁₂ (c₁.next i₁, c₂.next i₂) = i₁₂''

Tactic:
rw [← c₁₂.next_eq' h₂, ← ComplexShape.next_π₁ c₂ c₁₂ h₃, h₅]

Premises used: ComplexShape.next_π₁, ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂''

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₅]
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂'
h₆ : c₁.π c₂ c₁₂ (c₁.next 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₁₂''))

Tactic:
simp only [totalAux.d₂_eq K c₁₂ _ h₄ _ h₅, totalAux.d₂_eq K c₁₂ _ h₄ _ h₆,
            Linear.units_smul_comp, assoc, totalAux.ιMapObj_D₁, Linear.comp_units_smul,
            totalAux.d₁_eq K c₁₂ h₃ _ _ h₆, HomologicalComplex.Hom.comm_assoc, smul_smul,
            ComplexShape.ε₂_ε₁ c₁₂ h₃ h₄, neg_mul, Units.neg_smul]

Premises used: HomologicalComplex₂.totalAux.ιMapObj_D₁, CategoryTheory.Category.assoc, HomologicalComplex₂.totalAux.d₂_eq, CategoryTheory.Linear.units_smul_comp, smul_smul, HomologicalComplex₂.totalAux.d₁_eq, ComplexShape.ε₂_ε₁, CategoryTheory.Linear.comp_units_smul, Units.neg_smul, HomologicalComplex.Hom.comm_assoc, neg_mul
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂''))

Tactic:
simp only [K.d₂_eq_zero c₁₂ _ _ _ h₄, zero_comp, comp_zero, smul_zero, neg_zero]

Premises used: HomologicalComplex₂.d₂_eq_zero, CategoryTheory.Limits.comp_zero, smul_zero, CategoryTheory.Limits.zero_comp, neg_zero
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁)
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
⊢ 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₁₂'')

Tactic:
rw [K.d₁_eq_zero c₁₂ _ _ _ h₃, zero_comp, neg_zero]

Premises used: HomologicalComplex₂.d₁_eq_zero, CategoryTheory.Limits.zero_comp, neg_zero