awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
⊢ (n₁ * y + x * y).negOnePow •
      𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
        K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + x + y)) =
    (n₁ * y + x * y).negOnePow •
      (Functor.obj (shiftFunctor₁ C x) K).ιTotal (up ℤ) n₁ (n₂ + y) (n + y) ⋯ ≫
        HomologicalComplex.Hom.f (Iso.hom (K.totalShift₁Iso x)) (n + y) ≫
          HomologicalComplex.Hom.f
            (NatTrans.app (Iso.hom (shiftFunctorComm (CochainComplex.{v_1, u_1, 0} C ℤ) x y)) (K.total (up ℤ))) n
have w : HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
    (K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) sorry) =
  HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
    (Iso.hom (K.shiftFunctor₁XXIso n₁ x (n₁ + x) sorry (n₂ + y)) ≫
      K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) sorry ≫
        (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x (n + y) (n + x + y) sorry).inv ≫
          Iso.hom ((K.total (up ℤ)).XIsoOfEq sorry))
Tactic: rw [id_comp, comp_id,
    ι_totalShift₁Iso_hom_f_assoc _ x n₁ (n₂ + y) (n + y) (by lia) _ rfl (n + x + y) (by lia),
    CochainComplex.shiftFunctorComm_hom_app_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
⊢ HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯) =
    HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (Iso.hom (K.shiftFunctor₁XXIso n₁ x (n₁ + x) ⋯ (n₂ + y)) ≫
        K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫
          (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x (n + y) (n + x + y) ⋯).inv ≫
            Iso.hom ((K.total (up ℤ)).XIsoOfEq ⋯))
have w : HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
    (K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) sorry) =
  HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
    (𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
      K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) sorry ≫
        ((K.total (up ℤ)).XIsoOfEq sorry).inv ≫ Iso.hom ((K.total (up ℤ)).XIsoOfEq sorry))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
⊢ HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯) =
    HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
        K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫
          ((K.total (up ℤ)).XIsoOfEq ⋯).inv ≫ Iso.hom ((K.total (up ℤ)).XIsoOfEq ⋯))
have w : HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
    (K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) sorry) =
  (n₁ * y + x * y).negOnePow •
    𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫ K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) sorry ≫ 𝟙 ((K.total (up ℤ)).X (n + x + y))
Tactic: rw [Iso.inv_hom_id, comp_id, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
w :
  HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯) =
    (n₁ * y + x * y).negOnePow •
      𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
        K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + x + y))
⊢ HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯) =
    HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
        K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫
          ((K.total (up ℤ)).XIsoOfEq ⋯).inv ≫ Iso.hom ((K.total (up ℤ)).XIsoOfEq ⋯))
have w₁ : HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
    (K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) sorry) =
  HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
    (𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫ K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) sorry)
Tactic: rw [Iso.inv_hom_id, comp_id, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
w :
  HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯) =
    (n₁ * y + x * y).negOnePow •
      𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
        K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + x + y))
w₁ :
  HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯) =
    HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫ K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯)
⊢ HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯) =
    HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
      (𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
        K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫
          ((K.total (up ℤ)).XIsoOfEq ⋯).inv ≫ Iso.hom ((K.total (up ℤ)).XIsoOfEq ⋯))
have w₂ : HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
    (K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) sorry) =
  HSMul.hSMul (β := (K.X (n₁ + x)).X (n₂ + y) ⟶ (K.total (up ℤ)).X (n + x + y)) (n₁ * y + x * y).negOnePow
    (K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) sorry)
Tactic: rw [Iso.inv_hom_id, comp_id, id_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
⊢ K.flip.HasTotal c ↔ K.HasTotal c
have mp : K.flip.HasTotal c → K.HasTotal c
Tactic: constructor
-- 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
mp : K.flip.HasTotal c → K.HasTotal c
⊢ K.flip.HasTotal c ↔ K.HasTotal c
have mpr : K.HasTotal c → K.flip.HasTotal c
Tactic: constructor
-- 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
h : K.flip.HasTotal c
⊢ K.HasTotal c
have mp : K.flip.flip.HasTotal c
Tactic: change K.flip.flip.HasTotal 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
h : K.flip.HasTotal c
⊢ K.flip.flip.HasTotal c
have mp : ∀ (this : TotalComplexShapeSymmetry c₂ c₁ c), K.flip.flip.HasTotal c
Tactic: have := TotalComplexShapeSymmetry.symmetry 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
i₂ : I₂
i₁ : I₁
h rw : c₂.π c₁ c (i₂, i₁) = j
⊢ c₁.π c₂ c (i₁, i₂) = j
have rw₁ : j = j
Tactic: rw [← ComplexShape.π_symm c₁ c₂ c 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
i₁ : I₁
i₂ : I₂
h rw : c₁.π c₂ c (i₁, i₂) = j
⊢ c₂.π c₁ c (i₂, i₁) = j
have rw₁ : j = j
Tactic: rw [ComplexShape.π_symm c₁ c₂ c 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
⊢ 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)
have 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 sorry))
        (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 sorry))) =
    K.flip.ιTotal c i₁ i₂ j hi ≫ 𝟙 ((K.flip.total c).X j)
Tactic: ext
-- 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
⊢ 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)
have 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 sorry))
        (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.ιTotal c i₁ i₂ j hi ≫ 𝟙 ((K.total c).X j)
Tactic: ext
-- 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₁)