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
h : K.flip.HasTotal c
this : TotalComplexShapeSymmetry c₂ c₁ c
⊢ K.flip.flip.HasTotal c

Tactic:
infer_instance
-- 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
h : K.HasTotal c
⊢ K.flip.HasTotal c

Tactic:
infer_instance
-- 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
i₂ : I₂
i₁ : I₁
h rw : c₂.π c₁ c (i₂, i₁) = j
rw₁ rw₂ : j = j
⊢ c₁.π c₂ c (i₁, i₂) = j

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

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
i₁ : I₁
i₂ : I₂
h rw : c₁.π c₂ c (i₁, i₂) = j
rw₁ rw₂ : j = j
⊢ c₂.π c₁ c (i₂, i₁) = j

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

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
h :
  ∀ (i₁ : I₂) (i₂ : I₁) (hi : c₂.π c₁ c (i₁, i₂) = j),
    CategoryStruct.comp (Y := (K.flip.total c).X j) (K.flip.ιTotal c i₁ i₂ j hi)
        (CategoryStruct.comp (Y := (K.total c).X 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.totalDesc fun (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c (i₁, i₂) = j) ↦
            HSMul.hSMul (β := (K.flip.X i₂).X i₁ ⟶ (K.flip.total c).X j) (c₁.σ c₂ c i₁ i₂)
              (K.flip.ιTotal c i₂ i₁ j ⋯))) =
      K.flip.ιTotal c i₁ i₂ j hi ≫ 𝟙 ((K.flip.total c).X j)
⊢ CategoryStruct.comp (Y := (K.total c).X 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.totalDesc fun (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c (i₁, i₂) = j) ↦
        HSMul.hSMul (β := (K.flip.X i₂).X i₁ ⟶ (K.flip.total c).X j) (c₁.σ c₂ c i₁ i₂) (K.flip.ιTotal c i₂ i₁ j ⋯)) =
    𝟙 ((K.flip.total c).X j)

Tactic:
ext
-- 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
i₁ : I₂
i₂ : I₁
hi : c₂.π c₁ c (i₁, i₂) = j
⊢ CategoryStruct.comp (Y := (K.flip.total c).X j) (K.flip.ιTotal c i₁ i₂ j hi)
      (CategoryStruct.comp (Y := (K.total c).X 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.totalDesc fun (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c (i₁, i₂) = j) ↦
          HSMul.hSMul (β := (K.flip.X i₂).X i₁ ⟶ (K.flip.total c).X j) (c₁.σ c₂ c i₁ i₂) (K.flip.ιTotal c i₂ i₁ j ⋯))) =
    K.flip.ιTotal c i₁ i₂ j hi ≫ 𝟙 ((K.flip.total c).X j)

Tactic:
simp
-- 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
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (hi : c₁.π c₂ c (i₁, i₂) = j),
    CategoryStruct.comp (Y := (K.total c).X j) (K.ιTotal c i₁ i₂ j hi)
        (CategoryStruct.comp (Y := (K.flip.total c).X j)
          (K.totalDesc fun (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c (i₁, i₂) = j) ↦
            HSMul.hSMul (β := (K.flip.X i₂).X i₁ ⟶ (K.flip.total c).X j) (c₁.σ c₂ c i₁ i₂) (K.flip.ιTotal 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 ⋯))) =
      K.ιTotal c i₁ i₂ j hi ≫ 𝟙 ((K.total c).X j)
⊢ CategoryStruct.comp (Y := (K.flip.total c).X j)
      (K.totalDesc fun (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c (i₁, i₂) = j) ↦
        HSMul.hSMul (β := (K.flip.X i₂).X i₁ ⟶ (K.flip.total c).X j) (c₁.σ c₂ c i₁ i₂) (K.flip.ιTotal 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 ⋯)) =
    𝟙 ((K.total c).X j)

Tactic:
ext
-- 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
i₁ : I₁
i₂ : I₂
hi : c₁.π c₂ c (i₁, i₂) = j
⊢ CategoryStruct.comp (Y := (K.total c).X j) (K.ιTotal c i₁ i₂ j hi)
      (CategoryStruct.comp (Y := (K.flip.total c).X j)
        (K.totalDesc fun (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c (i₁, i₂) = j) ↦
          HSMul.hSMul (β := (K.flip.X i₂).X i₁ ⟶ (K.flip.total c).X j) (c₁.σ c₂ c i₁ i₂) (K.flip.ιTotal 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 ⋯))) =
    K.ιTotal c i₁ i₂ j hi ≫ 𝟙 ((K.total c).X j)

Tactic:
simp
-- 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: CategoryTheory.Linear.units_smul_comp, HomologicalComplex₂.ι_totalDesc_assoc, HomologicalComplex₂.ι_D₂_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 (i₂, c₁.next i₁) = j'

Tactic:
rw [← ComplexShape.next_π₂ c₂ c i₂ h₂, 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 (i₂, c₁.next i₁) = j'

Tactic:
have h₃ : ComplexShape.π c₂ c₁ c ⟨i₂, c₁.next i₁⟩ = j' := by
        rw [← ComplexShape.next_π₂ c₂ c i₂ h₂, 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 (i₂, c₁.next i₁) = j'
rw : c₁.π c₂ c (c₁.next i₁, i₂) = c₂.π c₁ c (i₂, c₁.next i₁)
rw₁ rw₂ : c₁.π c₂ c (c₁.next i₁, i₂) = c₁.π c₂ c (c₁.next i₁, i₂)
⊢ c₁.π c₂ c (c₁.next i₁, 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 (i₂, c₁.next i₁) = j'
⊢ c₁.π c₂ c (c₁.next i₁, i₂) = j'

Tactic:
have h₄ : ComplexShape.π c₁ c₂ c ⟨c₁.next i₁, 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 (i₂, c₁.next i₁) = j'
h₄ : c₁.π c₂ c (c₁.next i₁, 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 (c₁.next i₁) i₂)
      (HomologicalComplex.Hom.f (K.d i₁ (c₁.next i₁)) i₂ ≫ K.ιTotal c (c₁.next i₁) 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 (c₁.next i₁) i₂)
      ((K.flip.X i₂).d i₁ (c₁.next i₁) ≫ K.ιTotal c (c₁.next i₁) 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 h₂ i₂]

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 (i₂, c₁.next i₁) = j'
h₄ : c₁.π c₂ c (c₁.next i₁, i₂) = j'
⊢ HSMul.hSMul (β := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
      (c₂.ε₂ c₁ c (i₂, i₁) * c₁.σ c₂ c (c₁.next i₁) i₂)
      (HomologicalComplex.Hom.f (K.d i₁ (c₁.next i₁)) i₂ ≫ K.ιTotal c (c₁.next i₁) 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 (c₁.next i₁) i₂)
      ((K.flip.X i₂).d i₁ (c₁.next i₁) ≫ K.ιTotal c (c₁.next i₁) i₂ j' ⋯ :
        (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')

Tactic:
dsimp only [flip_X_X, flip_X_d]

Premises used: HomologicalComplex₂.flip_X_X, HomologicalComplex₂.flip_X_d