awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.TotalComplexSymmetry
Goal:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c : ComplexShape J
inst_2 : TotalComplexShape c₁ c₂ c
inst_3 : TotalComplexShape c₂ c₁ c
inst_4 : TotalComplexShapeSymmetry c₁ c₂ c
inst_5 : K.HasTotal c
inst_6 : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : ¬c₁.Rel i₁ (c₁.next i₁)
neg :
  HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j') (c₁.σ c₂ c i₁ i₂) 0 =
    CategoryStruct.comp (Y := K.flip.toGradedObject.mapObj (c₂.π c₁ c) j') (K.flip.d₂ c i₂ i₁ j')
      (K.flip.totalDesc fun (i₂ : I₂) (i₁ : I₁) (h : c₂.π c₁ c (i₂, i₁) = j') ↦
        HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ (K.total c).X j') (c₁.σ c₂ c i₁ i₂) (K.ιTotal c i₁ i₂ j' ⋯))
neg₁ :
  HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j') (c₁.σ c₂ c i₁ i₂) 0 =
    CategoryStruct.comp (Y := K.flip.toGradedObject.mapObj (c₂.π c₁ c) j')
      (0 : (K.flip.X i₂).X i₁ ⟶ K.flip.toGradedObject.mapObj (c₂.π c₁ c) j')
      (K.flip.totalDesc fun (i₂ : I₂) (i₁ : I₁) (h : c₂.π c₁ c (i₂, i₁) = j') ↦
          HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ (K.total c).X j') (c₁.σ c₂ c i₁ i₂) (K.ιTotal c i₁ i₂ j' ⋯) :
        (K.flip.total c).X j' ⟶ (K.total c).X j')
neg₂ :
  Eq (α := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j') 0
    (CategoryStruct.comp (Y := K.flip.toGradedObject.mapObj (c₂.π c₁ c) j')
      (0 : (K.flip.X i₂).X i₁ ⟶ K.flip.toGradedObject.mapObj (c₂.π c₁ c) j')
      (K.flip.totalDesc fun (i₂ : I₂) (i₁ : I₁) (h : c₂.π c₁ c (i₂, i₁) = j') ↦
          HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ (K.total c).X j') (c₁.σ c₂ c i₁ i₂) (K.ιTotal c i₁ i₂ j' ⋯) :
        (K.flip.total c).X j' ⟶ (K.total c).X j'))
neg₃ neg₄ : Eq.{v_1 + 1} (α := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j') 0 0
⊢ HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j') (c₁.σ c₂ c i₁ i₂) (K.d₁ c i₁ i₂ j') =
    CategoryStruct.comp (Y := K.flip.toGradedObject.mapObj (c₂.π c₁ c) j') (K.flip.d₂ c i₂ i₁ j')
      (K.flip.totalDesc fun (i₂ : I₂) (i₁ : I₁) (h : c₂.π c₁ c (i₂, i₁) = j') ↦
        HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ (K.total c).X j') (c₁.σ c₂ c i₁ i₂) (K.ιTotal c i₁ i₂ j' ⋯))

Tactic:
rw [K.d₁_eq_zero _ _ _ _ h₂, K.flip.d₂_eq_zero _ _ _ _ h₂, smul_zero, zero_comp]

Premises used: HomologicalComplex₂.d₂_eq_zero, smul_zero, HomologicalComplex₂.flip, HomologicalComplex₂.d₁_eq_zero, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.TotalComplexSymmetry
Goal:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c : ComplexShape J
inst_2 : TotalComplexShape c₁ c₂ c
inst_3 : TotalComplexShape c₂ c₁ c
inst_4 : TotalComplexShapeSymmetry c₁ c₂ c
inst_5 : K.HasTotal c
inst_6 : DecidableEq J
j j' : J
h₀ : ¬c.Rel j j'
neg :
  Eq (α := (K.flip.total c).X j ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
    (CategoryStruct.comp (Y := (K.total c).X j) (Iso.hom (K.totalFlipIsoX c j)) 0 :
      (K.flip.total c).X j ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
    (K.flip.D₂ c j j' ≫ Iso.hom (K.totalFlipIsoX c j') : K.flip.toGradedObject.mapObj (c₂.π c₁ c) j ⟶ (K.total c).X j')
neg₁ :
  Eq (α := (K.flip.total c).X j ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
    (CategoryStruct.comp (Y := (K.total c).X j) (Iso.hom (K.totalFlipIsoX c j)) 0 :
      (K.flip.total c).X j ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
    (CategoryStruct.comp (Y := K.flip.toGradedObject.mapObj (c₂.π c₁ c) j')
        (0 : K.flip.toGradedObject.mapObj (c₂.π c₁ c) j ⟶ K.flip.toGradedObject.mapObj (c₂.π c₁ c) j')
        (Iso.hom (K.totalFlipIsoX c j') : (K.flip.total c).X j' ⟶ (K.total c).X j') :
      K.flip.toGradedObject.mapObj (c₂.π c₁ c) j ⟶ (K.total c).X j')
neg₂ :
  Eq (α := (K.flip.total c).X j ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
    (CategoryStruct.comp (Y := (K.total c).X j) (Iso.hom (K.totalFlipIsoX c j)) 0 :
      (K.flip.total c).X j ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
    (0 : K.flip.toGradedObject.mapObj (c₂.π c₁ c) j ⟶ (K.total c).X j')
neg₃ neg₄ : Eq.{v_1 + 1} (α := (K.flip.total c).X j ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j') 0 0
⊢ Eq (α := (K.flip.total c).X j ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
    (Iso.hom (K.totalFlipIsoX c j) ≫ K.D₁ c j j' : (K.flip.total c).X j ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
    (K.flip.D₂ c j j' ≫ Iso.hom (K.totalFlipIsoX c j') : K.flip.toGradedObject.mapObj (c₂.π c₁ c) j ⟶ (K.total c).X j')

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

Premises used: CategoryTheory.Limits.comp_zero, HomologicalComplex₂.D₁_shape, HomologicalComplex₂.flip, HomologicalComplex₂.D₂_shape, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.TotalComplexSymmetry
Goal:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c : ComplexShape J
inst_2 : TotalComplexShape c₁ c₂ c
inst_3 : TotalComplexShape c₂ c₁ c
inst_4 : TotalComplexShapeSymmetry c₁ c₂ c
inst_5 : K.HasTotal c
inst_6 : DecidableEq J
j j' : J
pos :
  ∀ (h₀ : c.Rel j j'),
    Eq (α := (K.flip.total c).X j ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
      (Iso.hom (K.totalFlipIsoX c j) ≫ K.D₂ c j j' : (K.flip.total c).X j ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
      (K.flip.D₁ c j j' ≫ Iso.hom (K.totalFlipIsoX c j') :
        K.flip.toGradedObject.mapObj (c₂.π c₁ c) j ⟶ (K.total c).X j')
neg :
  ∀ (h₀ : ¬c.Rel j j'),
    Eq (α := (K.flip.total c).X j ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
      (Iso.hom (K.totalFlipIsoX c j) ≫ K.D₂ c j j' : (K.flip.total c).X j ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
      (K.flip.D₁ c j j' ≫ Iso.hom (K.totalFlipIsoX c j') :
        K.flip.toGradedObject.mapObj (c₂.π c₁ c) j ⟶ (K.total c).X j')
⊢ Eq (α := (K.flip.total c).X j ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
    (Iso.hom (K.totalFlipIsoX c j) ≫ K.D₂ c j j' : (K.flip.total c).X j ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
    (K.flip.D₁ c j j' ≫ Iso.hom (K.totalFlipIsoX c j') : K.flip.toGradedObject.mapObj (c₂.π c₁ c) j ⟶ (K.total c).X j')

Tactic:
by_cases h₀ : c.Rel j j'

Premises used: ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.TotalComplexSymmetry
Goal:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c : ComplexShape J
inst_2 : TotalComplexShape c₁ c₂ c
inst_3 : TotalComplexShape c₂ c₁ c
inst_4 : TotalComplexShapeSymmetry c₁ c₂ c
inst_5 : K.HasTotal c
inst_6 : DecidableEq J
j j' : J
h₀ : c.Rel j j'
pos :
  ∀ (i₂ : I₂) (i₁ : I₁) (h₁ : c₂.π c₁ c (i₂, i₁) = j),
    Eq (α := (K.flip.X i₂).X i₁ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
      (CategoryStruct.comp (Y := (K.flip.total c).X j)
        (K.flip.ιTotal c i₂ i₁ j h₁ : (K.flip.X i₂).X i₁ ⟶ (K.flip.total c).X j)
        (Iso.hom (K.totalFlipIsoX c j) ≫ K.D₂ c j j' : (K.flip.total c).X j ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j'))
      (CategoryStruct.comp (Y := (K.flip.total c).X j)
        (K.flip.ιTotal c i₂ i₁ j h₁ : (K.flip.X i₂).X i₁ ⟶ (K.flip.total c).X j)
        (K.flip.D₁ c j j' ≫ Iso.hom (K.totalFlipIsoX c j') :
          K.flip.toGradedObject.mapObj (c₂.π c₁ c) j ⟶ (K.total c).X j'))
⊢ Eq (α := (K.flip.total c).X j ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
    (Iso.hom (K.totalFlipIsoX c j) ≫ K.D₂ c j j' : (K.flip.total c).X j ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
    (K.flip.D₁ c j j' ≫ Iso.hom (K.totalFlipIsoX c j') : K.flip.toGradedObject.mapObj (c₂.π c₁ c) j ⟶ (K.total c).X j')

Tactic:
ext i₂ i₁ h₁
-- Module: Mathlib.Algebra.Homology.TotalComplexSymmetry
Goal:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c : ComplexShape J
inst_2 : TotalComplexShape c₁ c₂ c
inst_3 : TotalComplexShape c₂ c₁ c
inst_4 : TotalComplexShapeSymmetry c₁ c₂ c
inst_5 : K.HasTotal c
inst_6 : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
pos :
  Eq (α := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
    (CategoryStruct.comp (Y := (K.flip.total c).X j) (K.flip.ιTotal c i₂ i₁ j h₁)
      ((K.flip.totalDesc fun (i₂ : I₂) (i₁ : I₁) (h : c₂.π c₁ c (i₂, i₁) = j) ↦
          HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ (K.total c).X j) (c₁.σ c₂ c i₁ i₂) (K.ιTotal c i₁ i₂ j ⋯)) ≫
        K.D₂ c j j'))
    (CategoryStruct.comp (Y := (K.flip.total c).X j) (K.flip.ιTotal c i₂ i₁ j h₁)
      (K.flip.D₁ c j j' ≫
        K.flip.totalDesc fun (i₂ : I₂) (i₁ : I₁) (h : c₂.π c₁ c (i₂, i₁) = j') ↦
          HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ (K.total c).X j') (c₁.σ c₂ c i₁ i₂) (K.ιTotal c i₁ i₂ j' ⋯)))
⊢ Eq (α := (K.flip.X i₂).X i₁ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
    (CategoryStruct.comp (Y := (K.flip.total c).X j)
      (K.flip.ιTotal c i₂ i₁ j h₁ : (K.flip.X i₂).X i₁ ⟶ (K.flip.total c).X j)
      (Iso.hom (K.totalFlipIsoX c j) ≫ K.D₂ c j j' : (K.flip.total c).X j ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j'))
    (CategoryStruct.comp (Y := (K.flip.total c).X j)
      (K.flip.ιTotal c i₂ i₁ j h₁ : (K.flip.X i₂).X i₁ ⟶ (K.flip.total c).X j)
      (K.flip.D₁ c j j' ≫ Iso.hom (K.totalFlipIsoX c j') :
        K.flip.toGradedObject.mapObj (c₂.π c₁ c) j ⟶ (K.total c).X j'))

Tactic:
dsimp [totalFlipIsoX]

Premises used: HomologicalComplex₂.totalFlipIsoX
-- Module: Mathlib.Algebra.Homology.TotalComplexSymmetry
Goal:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c : ComplexShape J
inst_2 : TotalComplexShape c₁ c₂ c
inst_3 : TotalComplexShape c₂ c₁ c
inst_4 : TotalComplexShapeSymmetry c₁ c₂ c
inst_5 : K.HasTotal c
inst_6 : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
pos :
  HSMul.hSMul (β := (K.flip.X i₂).X i₁ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j') (c₁.σ c₂ c i₁ i₂) (K.d₂ c i₁ i₂ j') =
    CategoryStruct.comp (Y := K.flip.toGradedObject.mapObj (c₂.π c₁ c) j') (K.flip.d₁ c i₂ i₁ j')
      (K.flip.totalDesc fun (i₂ : I₂) (i₁ : I₁) (h : c₂.π c₁ c (i₂, i₁) = j') ↦
        HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ (K.total c).X j') (c₁.σ c₂ c i₁ i₂) (K.ιTotal c i₁ i₂ j' ⋯))
⊢ Eq (α := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
    (CategoryStruct.comp (Y := (K.flip.total c).X j) (K.flip.ιTotal c i₂ i₁ j h₁)
      ((K.flip.totalDesc fun (i₂ : I₂) (i₁ : I₁) (h : c₂.π c₁ c (i₂, i₁) = j) ↦
          HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ (K.total c).X j) (c₁.σ c₂ c i₁ i₂) (K.ιTotal c i₁ i₂ j ⋯)) ≫
        K.D₂ c j j'))
    (CategoryStruct.comp (Y := (K.flip.total c).X j) (K.flip.ιTotal c i₂ i₁ j h₁)
      (K.flip.D₁ c j j' ≫
        K.flip.totalDesc fun (i₂ : I₂) (i₁ : I₁) (h : c₂.π c₁ c (i₂, i₁) = j') ↦
          HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ (K.total c).X j') (c₁.σ c₂ c i₁ i₂) (K.ιTotal c i₁ i₂ j' ⋯)))

Tactic:
rw [ι_totalDesc_assoc, Linear.units_smul_comp, ι_D₂, ι_D₁_assoc]

Premises used: HomologicalComplex₂.ι_D₁_assoc, CategoryTheory.Linear.units_smul_comp, HomologicalComplex₂.ι_totalDesc_assoc, HomologicalComplex₂.ι_D₂
-- Module: Mathlib.Algebra.Homology.TotalComplexSymmetry
Goal:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c : ComplexShape J
inst_2 : TotalComplexShape c₁ c₂ c
inst_3 : TotalComplexShape c₂ c₁ c
inst_4 : TotalComplexShapeSymmetry c₁ c₂ c
inst_5 : K.HasTotal c
inst_6 : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
pos :
  HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j') (c₁.σ c₂ c i₁ i₂) (K.d₂ c i₁ i₂ j') =
    CategoryStruct.comp (Y := K.flip.toGradedObject.mapObj (c₂.π c₁ c) j') (K.flip.d₁ c i₂ i₁ j')
      (K.flip.totalDesc fun (i₂ : I₂) (i₁ : I₁) (h : c₂.π c₁ c (i₂, i₁) = j') ↦
        HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ (K.total c).X j') (c₁.σ c₂ c i₁ i₂) (K.ιTotal c i₁ i₂ j' ⋯))
⊢ HSMul.hSMul (β := (K.flip.X i₂).X i₁ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j') (c₁.σ c₂ c i₁ i₂) (K.d₂ c i₁ i₂ j') =
    CategoryStruct.comp (Y := K.flip.toGradedObject.mapObj (c₂.π c₁ c) j') (K.flip.d₁ c i₂ i₁ j')
      (K.flip.totalDesc fun (i₂ : I₂) (i₁ : I₁) (h : c₂.π c₁ c (i₂, i₁) = j') ↦
        HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ (K.total c).X j') (c₁.σ c₂ c i₁ i₂) (K.ιTotal c i₁ i₂ j' ⋯))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.TotalComplexSymmetry
Goal:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c : ComplexShape J
inst_2 : TotalComplexShape c₁ c₂ c
inst_3 : TotalComplexShape c₂ c₁ c
inst_4 : TotalComplexShapeSymmetry c₁ c₂ c
inst_5 : K.HasTotal c
inst_6 : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
pos :
  ∀ (h₂ : c₂.Rel i₂ (c₂.next i₂)),
    HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j') (c₁.σ c₂ c i₁ i₂) (K.d₂ c i₁ i₂ j') =
      CategoryStruct.comp (Y := K.flip.toGradedObject.mapObj (c₂.π c₁ c) j') (K.flip.d₁ c i₂ i₁ j')
        (K.flip.totalDesc fun (i₂ : I₂) (i₁ : I₁) (h : c₂.π c₁ c (i₂, i₁) = j') ↦
          HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ (K.total c).X j') (c₁.σ c₂ c i₁ i₂) (K.ιTotal c i₁ i₂ j' ⋯))
neg :
  ∀ (h₂ : ¬c₂.Rel i₂ (c₂.next i₂)),
    HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j') (c₁.σ c₂ c i₁ i₂) (K.d₂ c i₁ i₂ j') =
      CategoryStruct.comp (Y := K.flip.toGradedObject.mapObj (c₂.π c₁ c) j') (K.flip.d₁ c i₂ i₁ j')
        (K.flip.totalDesc fun (i₂ : I₂) (i₁ : I₁) (h : c₂.π c₁ c (i₂, i₁) = j') ↦
          HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ (K.total c).X j') (c₁.σ c₂ c i₁ i₂) (K.ιTotal c i₁ i₂ j' ⋯))
⊢ HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j') (c₁.σ c₂ c i₁ i₂) (K.d₂ c i₁ i₂ j') =
    CategoryStruct.comp (Y := K.flip.toGradedObject.mapObj (c₂.π c₁ c) j') (K.flip.d₁ c i₂ i₁ j')
      (K.flip.totalDesc fun (i₂ : I₂) (i₁ : I₁) (h : c₂.π c₁ c (i₂, i₁) = j') ↦
        HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ (K.total c).X j') (c₁.σ c₂ c i₁ i₂) (K.ιTotal c i₁ i₂ j' ⋯))

Tactic:
by_cases h₂ : c₂.Rel i₂ (c₂.next i₂)

Premises used: ComplexShape.next, ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.TotalComplexSymmetry
Goal:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c : ComplexShape J
inst_2 : TotalComplexShape c₁ c₂ c
inst_3 : TotalComplexShape c₂ c₁ c
inst_4 : TotalComplexShapeSymmetry c₁ c₂ c
inst_5 : K.HasTotal c
inst_6 : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₂.Rel i₂ (c₂.next i₂)
rw : c.next (c₂.π c₁ c (i₂, i₁)) = j'
rw₁ : c.next j = j'
rw₂ rw₃ : j' = j'
⊢ c₂.π c₁ c (c₂.next i₂, i₁) = j'

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

Premises used: ComplexShape.next_π₁, ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.TotalComplexSymmetry
Goal:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c : ComplexShape J
inst_2 : TotalComplexShape c₁ c₂ c
inst_3 : TotalComplexShape c₂ c₁ c
inst_4 : TotalComplexShapeSymmetry c₁ c₂ c
inst_5 : K.HasTotal c
inst_6 : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₂.Rel i₂ (c₂.next i₂)
⊢ c₂.π c₁ c (c₂.next i₂, i₁) = j'

Tactic:
have h₃ : ComplexShape.π c₂ c₁ c (ComplexShape.next c₂ i₂, i₁) = j' := by
        rw [← ComplexShape.next_π₁ c₁ c h₂ i₁, h₁, c.next_eq' h₀]
-- Module: Mathlib.Algebra.Homology.TotalComplexSymmetry
Goal:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c : ComplexShape J
inst_2 : TotalComplexShape c₁ c₂ c
inst_3 : TotalComplexShape c₂ c₁ c
inst_4 : TotalComplexShapeSymmetry c₁ c₂ c
inst_5 : K.HasTotal c
inst_6 : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₂.Rel i₂ (c₂.next i₂)
h₃ : c₂.π c₁ c (c₂.next i₂, i₁) = j'
rw : c₁.π c₂ c (i₁, c₂.next i₂) = c₂.π c₁ c (c₂.next 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₂) = j'

Tactic:
rw [← h₃, ComplexShape.π_symm c₁ c₂ c]

Premises used: ComplexShape.π_symm
-- Module: Mathlib.Algebra.Homology.TotalComplexSymmetry
Goal:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c : ComplexShape J
inst_2 : TotalComplexShape c₁ c₂ c
inst_3 : TotalComplexShape c₂ c₁ c
inst_4 : TotalComplexShapeSymmetry c₁ c₂ c
inst_5 : K.HasTotal c
inst_6 : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₂.Rel i₂ (c₂.next i₂)
h₃ : c₂.π c₁ c (c₂.next i₂, i₁) = j'
⊢ c₁.π c₂ c (i₁, c₂.next i₂) = j'

Tactic:
have h₄ : ComplexShape.π c₁ c₂ c (i₁, ComplexShape.next c₂ i₂) = j' := by
        rw [← h₃, ComplexShape.π_symm c₁ c₂ c]
-- Module: Mathlib.Algebra.Homology.TotalComplexSymmetry
Goal:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c : ComplexShape J
inst_2 : TotalComplexShape c₁ c₂ c
inst_3 : TotalComplexShape c₂ c₁ c
inst_4 : TotalComplexShapeSymmetry c₁ c₂ c
inst_5 : K.HasTotal c
inst_6 : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₂.Rel i₂ (c₂.next i₂)
h₃ : c₂.π c₁ c (c₂.next i₂, i₁) = j'
h₄ : c₁.π c₂ c (i₁, c₂.next i₂) = j'
pos :
  HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
      (c₂.ε₁ c₁ c (i₂, i₁) * c₁.σ c₂ c i₁ (c₂.next i₂))
      ((K.X i₁).d i₂ (c₂.next i₂) ≫ K.ιTotal c i₁ (c₂.next i₂) j' h₄ : (K.X i₁).X i₂ ⟶ (K.total c).X j') =
    HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
      (c₂.ε₁ c₁ c (i₂, i₁) * c₁.σ c₂ c i₁ (c₂.next i₂))
      (HomologicalComplex.Hom.f (K.flip.d i₂ (c₂.next i₂)) i₁ ≫ K.ιTotal c i₁ (c₂.next i₂) j' ⋯ :
        (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
⊢ HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j') (c₁.σ c₂ c i₁ i₂) (K.d₂ c i₁ i₂ j') =
    CategoryStruct.comp (Y := K.flip.toGradedObject.mapObj (c₂.π c₁ c) j') (K.flip.d₁ c i₂ i₁ j')
      (K.flip.totalDesc fun (i₂ : I₂) (i₁ : I₁) (h : c₂.π c₁ c (i₂, i₁) = j') ↦
        HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ (K.total c).X j') (c₁.σ c₂ c i₁ i₂) (K.ιTotal c i₁ i₂ j' ⋯))

Tactic:
rw [K.d₂_eq _ _ h₂ _ h₄, K.flip.d₁_eq _ h₂ _ _ h₃, Linear.units_smul_comp,
        assoc, ι_totalDesc, Linear.comp_units_smul, smul_smul, smul_smul,
        ComplexShape.σ_ε₂ c₁ c i₁ h₂]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Linear.units_smul_comp, HomologicalComplex₂.d₁_eq, smul_smul, HomologicalComplex₂.flip, HomologicalComplex₂.ι_totalDesc, CategoryTheory.Linear.comp_units_smul, ComplexShape.σ_ε₂, HomologicalComplex₂.d₂_eq
-- Module: Mathlib.Algebra.Homology.TotalComplexSymmetry
Goal:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c : ComplexShape J
inst_2 : TotalComplexShape c₁ c₂ c
inst_3 : TotalComplexShape c₂ c₁ c
inst_4 : TotalComplexShapeSymmetry c₁ c₂ c
inst_5 : K.HasTotal c
inst_6 : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₂.Rel i₂ (c₂.next i₂)
h₃ : c₂.π c₁ c (c₂.next i₂, i₁) = j'
h₄ : c₁.π c₂ c (i₁, c₂.next i₂) = j'
⊢ HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
      (c₂.ε₁ c₁ c (i₂, i₁) * c₁.σ c₂ c i₁ (c₂.next i₂))
      ((K.X i₁).d i₂ (c₂.next i₂) ≫ K.ιTotal c i₁ (c₂.next i₂) j' h₄ : (K.X i₁).X i₂ ⟶ (K.total c).X j') =
    HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
      (c₂.ε₁ c₁ c (i₂, i₁) * c₁.σ c₂ c i₁ (c₂.next i₂))
      (HomologicalComplex.Hom.f (K.flip.d i₂ (c₂.next i₂)) i₁ ≫ K.ιTotal c i₁ (c₂.next i₂) j' ⋯ :
        (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.TotalComplexSymmetry
Goal:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c : ComplexShape J
inst_2 : TotalComplexShape c₁ c₂ c
inst_3 : TotalComplexShape c₂ c₁ c
inst_4 : TotalComplexShapeSymmetry c₁ c₂ c
inst_5 : K.HasTotal c
inst_6 : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : ¬c₂.Rel i₂ (c₂.next i₂)
neg :
  HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j') (c₁.σ c₂ c i₁ i₂) 0 =
    CategoryStruct.comp (Y := K.flip.toGradedObject.mapObj (c₂.π c₁ c) j') (K.flip.d₁ c i₂ i₁ j')
      (K.flip.totalDesc fun (i₂ : I₂) (i₁ : I₁) (h : c₂.π c₁ c (i₂, i₁) = j') ↦
        HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ (K.total c).X j') (c₁.σ c₂ c i₁ i₂) (K.ιTotal c i₁ i₂ j' ⋯))
neg₁ :
  HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j') (c₁.σ c₂ c i₁ i₂) 0 =
    CategoryStruct.comp (Y := K.flip.toGradedObject.mapObj (c₂.π c₁ c) j')
      (0 : (K.flip.X i₂).X i₁ ⟶ K.flip.toGradedObject.mapObj (c₂.π c₁ c) j')
      (K.flip.totalDesc fun (i₂ : I₂) (i₁ : I₁) (h : c₂.π c₁ c (i₂, i₁) = j') ↦
          HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ (K.total c).X j') (c₁.σ c₂ c i₁ i₂) (K.ιTotal c i₁ i₂ j' ⋯) :
        (K.flip.total c).X j' ⟶ (K.total c).X j')
neg₂ :
  Eq (α := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j') 0
    (CategoryStruct.comp (Y := K.flip.toGradedObject.mapObj (c₂.π c₁ c) j')
      (0 : (K.flip.X i₂).X i₁ ⟶ K.flip.toGradedObject.mapObj (c₂.π c₁ c) j')
      (K.flip.totalDesc fun (i₂ : I₂) (i₁ : I₁) (h : c₂.π c₁ c (i₂, i₁) = j') ↦
          HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ (K.total c).X j') (c₁.σ c₂ c i₁ i₂) (K.ιTotal c i₁ i₂ j' ⋯) :
        (K.flip.total c).X j' ⟶ (K.total c).X j'))
neg₃ neg₄ : Eq.{v_1 + 1} (α := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j') 0 0
⊢ HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j') (c₁.σ c₂ c i₁ i₂) (K.d₂ c i₁ i₂ j') =
    CategoryStruct.comp (Y := K.flip.toGradedObject.mapObj (c₂.π c₁ c) j') (K.flip.d₁ c i₂ i₁ j')
      (K.flip.totalDesc fun (i₂ : I₂) (i₁ : I₁) (h : c₂.π c₁ c (i₂, i₁) = j') ↦
        HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ (K.total c).X j') (c₁.σ c₂ c i₁ i₂) (K.ιTotal c i₁ i₂ j' ⋯))

Tactic:
rw [K.d₂_eq_zero _ _ _ _ h₂, K.flip.d₁_eq_zero _ _ _ _ h₂, smul_zero, zero_comp]

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