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'
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')
⊢ 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₂ : 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' 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]
-- 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' ⋯))
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'))
⊢ 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₃ : Eq.{v_1 + 1} (α := (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j') 0 0
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'
⊢ 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 (α := (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')
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
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')
⊢ 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 (α := (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')
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
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')
⊢ 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 (α := (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')
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
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
h : c.Rel j j'
⊢ HAdd.hAdd (α := (K.flip.total c).X j ⟶ (K.total c).X j') (β := (K.flip.total c).X j ⟶ (K.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')
      (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') =
    HAdd.hAdd (α := (K.flip.total c).X j ⟶ (K.total c).X j') (β := (K.flip.total c).X j ⟶ (K.total c).X j')
      (K.flip.D₁ c j j' ≫ Iso.hom (K.totalFlipIsoX c j') : (K.flip.total c).X j ⟶ (K.total c).X j')
      (K.flip.D₂ c j j' ≫ Iso.hom (K.totalFlipIsoX c j') : (K.flip.total c).X j ⟶ (K.total c).X j')
have rw : HAdd.hAdd (α := (K.flip.total c).X j ⟶ (K.total c).X j') (β := (K.flip.total c).X j ⟶ (K.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')
    (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') =
  HAdd.hAdd (α := (K.flip.total c).X j ⟶ (K.total c).X j') (β := (K.flip.total c).X j ⟶ (K.total c).X j')
    (K.flip.D₁ c j j' ≫ Iso.hom (K.totalFlipIsoX c j') : (K.flip.total c).X j ⟶ (K.total c).X j')
    (K.flip.D₂ c j j' ≫ Iso.hom (K.totalFlipIsoX c j') : (K.flip.total c).X j ⟶ (K.total c).X j')
Tactic: rw [add_comm]
-- 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
i₁ : I₁
i₂ : I₂
j : J
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
i₁ : I₁
i₂ : I₂
j : J
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
inst_7 : TotalComplexShapeSymmetry c₂ c₁ c
inst_8 : TotalComplexShapeSymmetrySymmetry c₁ c₂ c
⊢ Eq (α := K.flip.flip.total c ≅ K.flip.total c) (K.flip.totalFlipIso c : K.flip.flip.total c ≅ K.flip.total c)
    (Iso.symm (K.totalFlipIso c) : K.total c ≅ K.flip.total c)
have w : ∀ (j : J) (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c (i₁, i₂) = j),
  Eq (α := (K.flip.flip.X i₁).X i₂ ⟶ (K.flip.total c).X j)
    (CategoryStruct.comp (Y := (K.flip.flip.total c).X j)
        (K.flip.flip.ιTotal c i₁ i₂ j h : (K.flip.flip.X i₁).X i₂ ⟶ (K.flip.flip.total c).X j)
        (HomologicalComplex.Hom.f (Iso.hom (K.flip.totalFlipIso c)) j :
          (K.flip.flip.total c).X j ⟶ (K.flip.total c).X j) :
      (K.flip.flip.X i₁).X i₂ ⟶ (K.flip.total c).X j)
    (CategoryStruct.comp (Y := (K.flip.flip.total c).X j) (K.flip.flip.ιTotal c i₁ i₂ j h)
        (HomologicalComplex.Hom.f (Iso.hom (Iso.symm (K.totalFlipIso c))) j) :
      (K.flip.flip.X i₁).X i₂ ⟶ (K.flip.total c).X j)
Tactic: ext j 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
inst_7 : TotalComplexShapeSymmetry c₂ c₁ c
inst_8 : TotalComplexShapeSymmetrySymmetry c₁ c₂ c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
⊢ Eq (α := (K.flip.flip.X i₁).X i₂ ⟶ (K.flip.total c).X j)
    (CategoryStruct.comp (Y := (K.flip.flip.total c).X j)
        (K.flip.flip.ιTotal c i₁ i₂ j h : (K.flip.flip.X i₁).X i₂ ⟶ (K.flip.flip.total c).X j)
        (HomologicalComplex.Hom.f (Iso.hom (K.flip.totalFlipIso c)) j :
          (K.flip.flip.total c).X j ⟶ (K.flip.total c).X j) :
      (K.flip.flip.X i₁).X i₂ ⟶ (K.flip.total c).X j)
    (CategoryStruct.comp (Y := (K.flip.flip.total c).X j) (K.flip.flip.ιTotal c i₁ i₂ j h)
        (HomologicalComplex.Hom.f (Iso.hom (Iso.symm (K.totalFlipIso c))) j) :
      (K.flip.flip.X i₁).X i₂ ⟶ (K.flip.total c).X j)
have w : 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) =
  CategoryStruct.comp (Y := (K.flip.flip.total c).X j) (K.flip.flip.ιTotal c i₁ i₂ j h)
    (HomologicalComplex.Hom.f (Iso.inv (K.totalFlipIso c)) j)
Tactic: rw [Iso.symm_hom, ιTotal_totalFlipIso_f_hom]
-- 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
inst_7 : TotalComplexShapeSymmetry c₂ c₁ c
inst_8 : TotalComplexShapeSymmetrySymmetry c₁ c₂ c
j : J
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 ⋯) =
    CategoryStruct.comp (Y := (K.flip.flip.total c).X j) (K.flip.flip.ιTotal c i₁ i₂ j h)
      (HomologicalComplex.Hom.f (Iso.inv (K.totalFlipIso c)) j)
have w : 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) =
  CategoryStruct.comp (Y := (K.total c).X j) (K.ιTotal c i₁ i₂ j h)
    (HomologicalComplex.Hom.f (Iso.inv (K.totalFlipIso c)) j)
Tactic: dsimp only [flip_flip]
-- 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
inst_7 : TotalComplexShapeSymmetry c₂ c₁ c
inst_8 : TotalComplexShapeSymmetrySymmetry c₁ c₂ c
j : J
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 ⋯) =
    CategoryStruct.comp (Y := (K.total c).X j) (K.ιTotal c i₁ i₂ j h)
      (HomologicalComplex.Hom.f (Iso.inv (K.totalFlipIso c)) j)
have w : 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) =
  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)
Tactic: rw [ιTotal_totalFlipIso_f_inv, ComplexShape.σ_symm]
-- 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
inst_7 : TotalComplexShapeSymmetry c₂ c₁ c
inst_8 : TotalComplexShapeSymmetrySymmetry c₁ c₂ c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
w :
  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 ⋯) =
    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 ⋯)
⊢ 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 ⋯) =
    CategoryStruct.comp (Y := (K.total c).X j) (K.ιTotal c i₁ i₂ j h)
      (HomologicalComplex.Hom.f (Iso.inv (K.totalFlipIso c)) j)
have w₁ : 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) =
  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)
Tactic: rw [ιTotal_totalFlipIso_f_inv, ComplexShape.σ_symm]
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : NoZeroDivisors R
⊢ ¬IsPrimePow.{u_1} (R := R) 0
have simp : ∀ (x : R) (x_1 : ℕ), 0 < x_1 → x ^ x_1 = 0 → ¬Prime x
Tactic: simp only [isPrimePow_def, not_exists, not_and', and_imp]
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : NoZeroDivisors R
x : R
n : ℕ
_hn : 0 < n
hx : x ^ n = 0
⊢ ¬Prime x
have rw : ¬Prime.{u_1} (M := R) 0
Tactic: rw [eq_zero_of_pow_eq_zero hx]
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : R
hn_1 : IsPrimePow n
k : ℕ
hk : k ≠ 0
p : R
k' : ℕ
hp : Prime p
hk' : 0 < k'
hn : p ^ k' = n
⊢ p ^ (k * k') = n ^ k
have rw : (p ^ k') ^ k = n ^ k
Tactic: rw [pow_mul', hn]
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : R
hn_1 : IsPrimePow n
k : ℕ
hk : k ≠ 0
p : R
k' : ℕ
hp : Prime p
hk' : 0 < k'
hn : p ^ k' = n
rw : (p ^ k') ^ k = n ^ k
⊢ p ^ (k * k') = n ^ k
have rw₁ : n ^ k = n ^ k
Tactic: rw [pow_mul', hn]
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
n : ℕ
⊢ IsPrimePow n ↔ ∃ (p : ℕ), p ≤ n ∧ ∃ (k : ℕ), k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
have rw : (∃ (p : ℕ), ∃ (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔
  ∃ (p : ℕ), p ≤ n ∧ ∃ (k : ℕ), k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Tactic: rw [isPrimePow_nat_iff]
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
n : ℕ
⊢ (∃ (p : ℕ), ∃ (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔
    ∃ (p : ℕ), p ≤ n ∧ ∃ (k : ℕ), k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
have refine : (∃ (p : ℕ), ∃ (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n) →
  ∃ (p : ℕ), p ≤ n ∧ ∃ (k : ℕ), k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Tactic: refine Iff.symm ⟨fun ⟨p, _, k, _, hp, hk, hn⟩ => ⟨p, k, hp, hk, hn⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ ∃ (p_1 : ℕ), p_1 ≤ p ^ k ∧ ∃ (k_1 : ℕ), k_1 ≤ p ^ k ∧ Nat.Prime p_1 ∧ 0 < k_1 ∧ p_1 ^ k_1 = p ^ k
have refine : p ≤ p ^ k
Tactic: refine ⟨p, ?_, k, (Nat.lt_pow_self hp.one_lt).le, hp, hk, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.IsPrimePow (goal)
Goal:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
| p ≤ p ^ k
have lhs : p
Tactic: lhs