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₁)
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
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
⊢ 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₂)

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₂)
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
pos₁ : c₁.π c₂ c₁₂ (i₁, c₂.next 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₁₂'') 0

Tactic:
rw [totalAux.d₂_eq K c₁₂ i₁ h₄ 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₁)
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₁₂
pos₂ pos₃ : c₁₂.next i₁₂ = c₁₂.next i₁₂
⊢ c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'

Tactic:
rw [← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₄, ← c₁₂.next_eq' 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₂)
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
⊢ 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

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

Premises used: HomologicalComplex₂.totalAux.ιMapObj_D₁, CategoryTheory.Category.assoc, CategoryTheory.Linear.units_smul_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 i₂ (c₂.next i₂)
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
pos₁ :
  HSMul.hSMul (β := K.toGradedObject (i₁, i₂) ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'') (c₁.ε₂ c₂ c₁₂ (i₁, i₂)) 0 =
    0
pos₂ pos₃ : 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: CategoryTheory.Limits.comp_zero, smul_zero, HomologicalComplex₂.d₁_eq_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₁)
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) (-K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'')
neg₁ :
  Eq (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'')
    (K.D₂ c₁₂ i₁₂ i₁₂' ≫ 0) (-K.D₁ c₁₂ i₁₂ i₁₂' ≫ 0)
neg₂ :
  Eq (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'') 0
    (-K.D₁ c₁₂ i₁₂ i₁₂' ≫ 0)
neg₃ :
  Eq.{v_1 + 1} (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) 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₁₂'') (-K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'')

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

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

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

Premises used: HomologicalComplex₂.D₁_shape, HomologicalComplex₂.D₂_shape, 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₁₂
⊢ 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:
simp
-- 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 L M : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
φ : K ⟶ L
e : K ≅ L
ψ : L ⟶ M
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₁₂'
rw :
  HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂') 0
      (K.D₂ c₁₂ i₁₂ i₁₂') =
    0
rw₁ : HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂') 0 0 = 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂') 0 0
⊢ HAdd.hAdd (α := 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₁₂, K.D₂_shape c₁₂ _ _ h₁₂, zero_add]

Premises used: HomologicalComplex₂.D₁_shape, zero_add, 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 L M : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
φ : K ⟶ L
e : K ≅ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
x₁ y₁ : I₁
h₁ : x₁ = y₁
x₂ y₂ : I₂
h₂ : x₂ = y₂
i₁₂ : I₁₂
h : c₁.π c₂ c₁₂ (y₁, y₂) = i₁₂
rw : c₁.π c₂ c₁₂ (y₁, x₂) = i₁₂
rw₁ : c₁.π c₂ c₁₂ (y₁, y₂) = i₁₂
rw₂ rw₃ : i₁₂ = i₁₂
⊢ c₁.π c₂ c₁₂ (x₁, x₂) = i₁₂

Tactic:
rw [h₁, 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₁₂
x₁ y₁ : I₁
h₁ : x₁ = y₁
x₂ y₂ : I₂
h₂ : x₂ = y₂
i₁₂ : I₁₂
h : c₁.π c₂ c₁₂ (y₁, y₂) = i₁₂
subst :
  ∀ (h : c₁.π c₂ c₁₂ (x₁, x₂) = i₁₂),
    Eq (α := (K.X x₁).X x₂ ⟶ (K.total c₁₂).X i₁₂) ((XXIsoOfEq C c₁ c₂ K ⋯ ⋯).hom ≫ K.ιTotal c₁₂ x₁ x₂ i₁₂ h)
      (K.ιTotal c₁₂ x₁ x₂ i₁₂ ⋯)
⊢ Eq (α := (K.X x₁).X x₂ ⟶ (K.total c₁₂).X i₁₂) ((XXIsoOfEq C c₁ c₂ K h₁ h₂).hom ≫ K.ιTotal c₁₂ y₁ y₂ i₁₂ h)
    (K.ιTotal c₁₂ x₁ x₂ i₁₂ ⋯)

Tactic:
subst 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₁₂
x₁ : I₁
x₂ : I₂
i₁₂ : I₁₂
h : c₁.π c₂ c₁₂ (x₁, x₂) = i₁₂
⊢ Eq (α := (K.X x₁).X x₂ ⟶ (K.total c₁₂).X i₁₂) ((XXIsoOfEq C c₁ c₂ K ⋯ ⋯).hom ≫ K.ιTotal c₁₂ x₁ x₂ i₁₂ h)
    (K.ιTotal c₁₂ x₁ x₂ i₁₂ ⋯)

Tactic:
simp
-- 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 L M : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
φ : K ⟶ L
e : K ≅ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
x₁ y₁ : I₁
h₁ : x₁ = y₁
x₂ y₂ : I₂
h₂ : x₂ = y₂
i₁₂ : I₁₂
h : c₁.π c₂ c₁₂ (x₁, x₂) = i₁₂
rw : c₁.π c₂ c₁₂ (y₁, y₂) = c₁.π c₂ c₁₂ (x₁, x₂)
rw₁ : c₁.π c₂ c₁₂ (y₁, y₂) = c₁.π c₂ c₁₂ (y₁, x₂)
rw₂ rw₃ : c₁.π c₂ c₁₂ (y₁, y₂) = c₁.π c₂ c₁₂ (y₁, y₂)
⊢ c₁.π c₂ c₁₂ (y₁, y₂) = i₁₂

Tactic:
rw [← h, 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₁₂
x₁ y₁ : I₁
h₁ : x₁ = y₁
x₂ y₂ : I₂
h₂ : x₂ = y₂
i₁₂ : I₁₂
h : c₁.π c₂ c₁₂ (x₁, x₂) = i₁₂
subst :
  Eq (α := (K.X x₁).X x₂ ⟶ (K.total c₁₂).X i₁₂) ((XXIsoOfEq C c₁ c₂ K ⋯ ⋯).inv ≫ K.ιTotal c₁₂ x₁ x₂ i₁₂ h)
    (K.ιTotal c₁₂ x₁ x₂ i₁₂ ⋯)
⊢ Eq (α := (K.X y₁).X y₂ ⟶ (K.total c₁₂).X i₁₂) ((XXIsoOfEq C c₁ c₂ K h₁ h₂).inv ≫ K.ιTotal c₁₂ x₁ x₂ i₁₂ h)
    (K.ιTotal c₁₂ y₁ y₂ i₁₂ ⋯)

Tactic:
subst 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₁₂
x₁ : I₁
x₂ : I₂
i₁₂ : I₁₂
h : c₁.π c₂ c₁₂ (x₁, x₂) = i₁₂
⊢ Eq (α := (K.X x₁).X x₂ ⟶ (K.total c₁₂).X i₁₂) ((XXIsoOfEq C c₁ c₂ K ⋯ ⋯).inv ≫ K.ιTotal c₁₂ x₁ x₂ i₁₂ h)
    (K.ιTotal c₁₂ x₁ x₂ i₁₂ ⋯)

Tactic:
simp
-- 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₂
i₁₂ : I₁₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ Eq (α := (K.X i₁).X i₂ ⟶ (K.total c₁₂).X i₁₂) (K.ιTotalOrZero c₁₂ i₁ i₂ i₁₂) (K.ιTotal c₁₂ i₁ i₂ i₁₂ h)

Tactic:
dif_pos h

Premises used: HomologicalComplex₂.toGradedObject, HomologicalComplex₂.ιTotal, dif_pos, CategoryTheory.Limits.colimit, CategoryTheory.GradedObject.ιMapObjOrZero, HomologicalComplex₂.ιTotalOrZero, CategoryTheory.GradedObject.mapObj
-- 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₂
i₁₂ : I₁₂
h : c₁.π c₂ c₁₂ (i₁, i₂) ≠ i₁₂
⊢ Eq (α := (K.X i₁).X i₂ ⟶ (K.total c₁₂).X i₁₂) (K.ιTotalOrZero c₁₂ i₁ i₂ i₁₂) 0

Tactic:
dif_neg h

Premises used: HomologicalComplex₂.toGradedObject, dif_neg, CategoryTheory.Limits.colimit, CategoryTheory.GradedObject.ιMapObjOrZero, HomologicalComplex₂.ιTotalOrZero, CategoryTheory.GradedObject.mapObj
-- 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₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ Eq (α := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
    (CategoryStruct.comp (Y := (K.total c₁₂).X i₁₂) (K.ιTotal c₁₂ i₁ i₂ i₁₂ h) (K.D₁ c₁₂ i₁₂ i₁₂'))
    (K.d₁ c₁₂ i₁ i₂ i₁₂')

Tactic:
apply totalAux.ιMapObj_D₁

Premises used: 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₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ Eq (α := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
    (CategoryStruct.comp (Y := (K.total c₁₂).X i₁₂) (K.ιTotal c₁₂ i₁ i₂ i₁₂ h) (K.D₂ c₁₂ i₁₂ i₁₂'))
    (K.d₂ c₁₂ i₁ i₂ i₁₂')

Tactic:
apply totalAux.ιMapObj_D₂

Premises used: 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₁
h : c₁.Rel i₁ i₁'
i₂ : I₂
i₁₂ : I₁₂
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ =
    HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ (K.total c₁₂).X i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      ((K.d i₁ i₁').f i₂ ≫ K.ιTotalOrZero c₁₂ i₁' i₂ i₁₂)

Tactic:
totalAux.d₁_eq' _ _ h _ _

Premises used: CategoryTheory.Limits.colimit, HomologicalComplex₂.ιTotalOrZero, CategoryTheory.GradedObject.mapObj, 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₁
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.total c₁₂).X i₁₂) (c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      ((K.d i₁ i₁').f i₂ ≫ K.ιTotal c₁₂ i₁' i₂ i₁₂ h')

Tactic:
totalAux.d₁_eq _ _ h _ _ _

Premises used: HomologicalComplex₂.ιTotal, HomologicalComplex₂.totalAux.d₁_eq, CategoryTheory.Limits.colimit, CategoryTheory.GradedObject.mapObj
-- 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₂' : I₂
h : c₂.Rel i₂ i₂'
i₁₂ : I₁₂
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂ =
    HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ (K.total c₁₂).X i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂))
      ((K.X i₁).d i₂ i₂' ≫ K.ιTotalOrZero c₁₂ i₁ i₂' i₁₂)

Tactic:
totalAux.d₂_eq' _ _ _ h _

Premises used: HomologicalComplex₂.totalAux.d₂_eq', CategoryTheory.Limits.colimit, HomologicalComplex₂.ιTotalOrZero, CategoryTheory.GradedObject.mapObj
-- 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₂' : 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.total c₁₂).X i₁₂) (c₁.ε₂ c₂ c₁₂ (i₁, i₂))
      ((K.X i₁).d i₂ i₂' ≫ K.ιTotal c₁₂ i₁ i₂' i₁₂ h')

Tactic:
totalAux.d₂_eq _ _ _ h _ _

Premises used: HomologicalComplex₂.totalAux.d₂_eq, HomologicalComplex₂.ιTotal, CategoryTheory.Limits.colimit, CategoryTheory.GradedObject.mapObj
-- 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₁₂
A : C
i₁₂ : I₁₂
f : (i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂ → ((K.X i₁).X i₂ ⟶ A)
i₁ : I₁
i₂ : I₂
hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ CategoryStruct.comp (Y := (K.total c₁₂).X i₁₂) (K.ιTotal c₁₂ i₁ i₂ i₁₂ hi) (K.totalDesc f) = f i₁ i₂ hi

Tactic:
simp [totalDesc, ιTotal]

Premises used: HomologicalComplex₂.ιTotal, HomologicalComplex₂.totalDesc
-- 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₁₂
A : C
i₁₂ : I₁₂
f g : (K.total c₁₂).X i₁₂ ⟶ A
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂), K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ f = K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ g
hfg :
  ∀ (i : I₁ × I₂) (hij : c₁.π c₂ c₁₂ i = i₁₂),
    K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ hij ≫ f = K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ hij ≫ g
⊢ f = g

Tactic:
apply GradedObject.mapObj_ext

Premises used: CategoryTheory.GradedObject.mapObj_ext
-- 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₁₂
A : C
i₁₂ : I₁₂
f g : (K.total c₁₂).X i₁₂ ⟶ A
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂), K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ f = K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ g
i₁ : I₁
i₂ : I₂
hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ hi ≫ f =
    K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ hi ≫ g

Tactic:
h i₁ i₂ hi

Premises used: HomologicalComplex₂.toGradedObject, HomologicalComplex₂.ιTotal, CategoryTheory.Limits.colimit, CategoryTheory.GradedObject.mapObj