awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexSymmetry (goal)
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')
⊢ 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')
have neg₃ : Eq.{v_1 + 1} (α := (K.flip.total c).X j ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j') 0 0
Tactic: rw [K.D₁_shape _ _ _ h₀, K.flip.D₂_shape c _ _ h₀, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexSymmetry (goal)
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
⊢ 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')
have 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')
Tactic: by_cases h₀ : c.Rel j j'
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexSymmetry (goal)
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')
⊢ 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')
have 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')
Tactic: by_cases h₀ : c.Rel j j'
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexSymmetry (goal)
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'
⊢ 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')
have 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'))
Tactic: ext i₂ i₁ h₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexSymmetry (goal)
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
⊢ 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'))
have 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 sorry)) ≫
      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' sorry)))
Tactic: dsimp [totalFlipIsoX]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexSymmetry (goal)
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
⊢ 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' ⋯)))
have 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' sorry))
Tactic: rw [ι_totalDesc_assoc, Linear.units_smul_comp, ι_D₂, ι_D₁_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexSymmetry (goal)
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
⊢ 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' ⋯))
have 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' sorry))
Tactic: by_cases h₂ : c₂.Rel i₂ (c₂.next i₂)
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexSymmetry (goal)
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' ⋯))
⊢ 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' ⋯))
have 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' sorry))
Tactic: by_cases h₂ : c₂.Rel i₂ (c₂.next i₂)
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexSymmetry (goal)
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'
have rw : c.next (c₂.π c₁ c (i₂, i₁)) = j'
Tactic: rw [← ComplexShape.next_π₁ c₁ c h₂ i₁, h₁, c.next_eq' h₀]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexSymmetry (goal)
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'
⊢ c₂.π c₁ c (c₂.next i₂, i₁) = j'
have rw₁ : c.next j = j'
Tactic: rw [← ComplexShape.next_π₁ c₁ c h₂ i₁, h₁, c.next_eq' h₀]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexSymmetry (goal)
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'
⊢ c₂.π c₁ c (c₂.next i₂, i₁) = j'
have rw₂ : j' = j'
Tactic: rw [← ComplexShape.next_π₁ c₁ c h₂ i₁, h₁, c.next_eq' h₀]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexSymmetry (hypothesis)
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₂)
⊢ 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' ⋯))
have h₃ : 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₀]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexSymmetry (goal)
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'
have rw : c₁.π c₂ c (i₁, c₂.next i₂) = c₂.π c₁ c (c₂.next i₂, i₁)
Tactic: rw [← h₃, ComplexShape.π_symm c₁ c₂ c]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexSymmetry (goal)
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₁)
⊢ c₁.π c₂ c (i₁, c₂.next i₂) = j'
have rw₁ : c₁.π c₂ c (i₁, c₂.next i₂) = c₁.π c₂ c (i₁, c₂.next i₂)
Tactic: rw [← h₃, ComplexShape.π_symm c₁ c₂ c]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexSymmetry (hypothesis)
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'
⊢ 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' ⋯))
have h₄ : 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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexSymmetry (goal)
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₂) (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' ⋯))
have 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' sorry :
      (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) 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₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexSymmetry (goal)
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₂)
⊢ 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' ⋯))
have 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' sorry))
Tactic: rw [K.d₂_eq_zero _ _ _ _ h₂, K.flip.d₁_eq_zero _ _ _ _ h₂, smul_zero, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexSymmetry (goal)
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' ⋯))
⊢ 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' ⋯))
have 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' sorry) :
      (K.flip.total c).X j' ⟶ (K.total c).X j')
Tactic: rw [K.d₂_eq_zero _ _ _ _ h₂, K.flip.d₁_eq_zero _ _ _ _ h₂, smul_zero, zero_comp]