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

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

Premises used: CategoryTheory.Limits.comp_zero, HomologicalComplex₂.D₁_shape, HomologicalComplex₂.flip, HomologicalComplex₂.D₂_shape, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.TotalComplexSymmetry
Goal:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c : ComplexShape J
inst_2 : TotalComplexShape c₁ c₂ c
inst_3 : TotalComplexShape c₂ c₁ c
inst_4 : TotalComplexShapeSymmetry c₁ c₂ c
inst_5 : K.HasTotal c
inst_6 : DecidableEq J
j j' : J
h : c.Rel j j'
rw 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')
⊢ 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]

Premises used: add_comm
-- 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
⊢ Eq (α := (K.flip.total c).X j ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
    (HomologicalComplex.Hom.f (Iso.hom (K.totalFlipIso 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' ≫ HomologicalComplex.Hom.f (Iso.hom (K.totalFlipIso c)) j' :
      K.flip.toGradedObject.mapObj (c₂.π c₁ c) j ⟶ (K.total c).X j')

Tactic:
apply totalFlipIsoX_hom_D₁

Premises used: HomologicalComplex₂.totalFlipIsoX_hom_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
⊢ Eq (α := (K.flip.total c).X j ⟶ K.toGradedObject.mapObj (c₁.π c₂ c) j')
    (HomologicalComplex.Hom.f (Iso.hom (K.totalFlipIso 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' ≫ HomologicalComplex.Hom.f (Iso.hom (K.totalFlipIso c)) j' :
      K.flip.toGradedObject.mapObj (c₂.π c₁ c) j ⟶ (K.total c).X j')

Tactic:
apply totalFlipIsoX_hom_D₂

Premises used: HomologicalComplex₂.totalFlipIsoX_hom_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
i₁ : I₁
i₂ : I₂
j : J
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
i₁ : I₁
i₂ : I₂
j : J
h : c₂.π c₁ c (i₂, i₁) = 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)
      (HomologicalComplex.Hom.f (Iso.hom (K.totalFlipIso c)) j : (K.flip.total c).X j ⟶ (K.total c).X 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:
simp [totalFlipIso, totalFlipIsoX]

Premises used: HomologicalComplex₂.totalFlipIso, 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
i₁ : I₁
i₂ : I₂
j : J
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
i₁ : I₁
i₂ : I₂
j : J
h : c₁.π c₂ 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) =
    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 ⋯)

Tactic:
simp [totalFlipIso, totalFlipIsoX]

Premises used: HomologicalComplex₂.totalFlipIso, 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
⊢ K.flip.flip.HasTotal c

Tactic:
(inferInstance : K.HasTotal c)

Premises used: inferInstance, HomologicalComplex₂.flip
-- 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
inst_7 : TotalComplexShapeSymmetry c₂ c₁ c
inst_8 : TotalComplexShapeSymmetrySymmetry c₁ c₂ c
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)
⊢ 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)

Tactic:
ext j 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
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 ⋯) =
    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)
⊢ 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:
rw [Iso.symm_hom, ιTotal_totalFlipIso_f_hom]

Premises used: CategoryTheory.Iso.symm_hom, HomologicalComplex₂.ιTotal_totalFlipIso_f_hom
-- 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
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 ⋯) =
    CategoryStruct.comp (Y := (K.total c).X j) (K.ιTotal c i₁ i₂ j h)
      (HomologicalComplex.Hom.f (Iso.inv (K.totalFlipIso c)) 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)

Tactic:
dsimp only [flip_flip]

Premises used: HomologicalComplex₂.flip_flip
-- 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
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 ⋯)
w₁ 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)

Tactic:
rw [ιTotal_totalFlipIso_f_inv, ComplexShape.σ_symm]

Premises used: ComplexShape.σ_symm, HomologicalComplex₂.ιTotal_totalFlipIso_f_inv
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : R
⊢ IsPrimePow n ↔ ∃ (p : R), ∃ (k : ℕ), Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
Iff.rfl

Premises used: Iff.rfl, IsPrimePow
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : R
h : ∃ (p : R), ∃ (k : ℕ), Prime p ∧ 0 < k ∧ p ^ k = n
p : R
k : ℕ
hp : Prime p
hk : 0 < k
hn rwa rwa₁ rwa₂ rwa₃ : p ^ k = n
⊢ p ^ (k - 1 + 1) = n

Tactic:
rwa [Nat.sub_add_cancel hk]

Premises used: Nat.sub_add_cancel
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : NoZeroDivisors R
simp : ∀ (x : R) (x_1 : ℕ), 0 < x_1 → x ^ x_1 = 0 → ¬Prime x
⊢ ¬IsPrimePow.{u_1} (R := R) 0

Tactic:
simp only [isPrimePow_def, not_exists, not_and', and_imp]

Premises used: and_imp, not_exists, isPrimePow_def, not_and'
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : NoZeroDivisors R
x : R
n : ℕ
_hn : 0 < n
hx : x ^ n = 0
rw : ¬Prime.{u_1} (M := R) 0
⊢ ¬Prime x

Tactic:
rw [eq_zero_of_pow_eq_zero hx]

Premises used: eq_zero_of_pow_eq_zero
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : NoZeroDivisors R
x : R
n : ℕ
_hn : 0 < n
hx : x ^ n = 0
⊢ ¬Prime.{u_1} (M := R) 0

Tactic:
simp
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : R
h : IsPrimePow n
⊢ ¬IsUnit n

Tactic:
let ⟨_p, _k, hp, hk, hn⟩ := h
  hn ▸ (isUnit_pow_iff hk.ne').not.mpr hp.not_unit

Premises used: Iff.mpr, _private.0.IsPrimePow.not_unit.match_1, isUnit_pow_iff, IsUnit, Eq.rec, Iff.not, Prime.not_unit, LT.lt.ne', Not
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : R
h : IsUnit n
⊢ ¬IsPrimePow n

Tactic:
fun h' => h'.not_unit h

Premises used: Not, IsPrimePow.not_unit
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
R : Type u_1
inst : CommMonoidWithZero R
⊢ ¬IsPrimePow.{u_1} (R := R) 1

Tactic:
isUnit_one.not_isPrimePow

Premises used: IsUnit.not_isPrimePow, isUnit_one
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
R : Type u_1
inst : CommMonoidWithZero R
p : R
hp : Prime p
⊢ HPow.hPow (β := ℕ) p 1 = p

Tactic:
simp
-- Module: Mathlib.Algebra.IsPrimePow
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
rw₁ rw₂ : n ^ k = n ^ k
⊢ p ^ (k * k') = n ^ k

Tactic:
rw [pow_mul', hn]

Premises used: pow_mul'
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : NoZeroDivisors R
n : R
h : IsPrimePow n
⊢ n ≠ 0

Tactic:
fun t =>
  not_isPrimePow_zero (t ▸ h)

Premises used: not_isPrimePow_zero, Not
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
R : Type u_1
inst : CommMonoidWithZero R
n : R
h : IsPrimePow n
⊢ n ≠ 1

Tactic:
fun t =>
  not_isPrimePow_one (t ▸ h)

Premises used: not_isPrimePow_one, Not
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
n : ℕ
⊢ IsPrimePow n ↔ ∃ (p : ℕ), ∃ (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
simp only [isPrimePow_def, Nat.prime_iff]

Premises used: Nat.prime_iff, isPrimePow_def
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
p : ℕ
hp : Prime p
⊢ IsPrimePow p

Tactic:
_root_.Prime.isPrimePow (prime_iff.mp hp)

Premises used: Nat.prime_iff, Iff.mp, Prime.isPrimePow
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
n : ℕ
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
⊢ IsPrimePow n ↔ ∃ (p : ℕ), p ≤ n ∧ ∃ (k : ℕ), k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
rw [isPrimePow_nat_iff]

Premises used: isPrimePow_nat_iff
-- Module: Mathlib.Algebra.IsPrimePow
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

Tactic:
Iff.symm ⟨fun ⟨p, _, k, _, hp, hk, hn⟩ => ⟨p, k, hp, hk, hn⟩, ?_⟩

Premises used: Nat.Prime, Exists, And, HPow.hPow, And.intro, LT.lt, Iff.intro, Exists.intro, _private.0.isPrimePow_nat_iff_bounded.match_1, OfNat.ofNat, Eq, Iff.symm
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
n : ℕ
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
⊢ (∃ (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⟩, ?_⟩

Premises used: Iff.intro, Iff.symm
-- Module: Mathlib.Algebra.IsPrimePow
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

Tactic:
⟨p, ?_, k, (Nat.lt_pow_self hp.one_lt).le, hp, hk, rfl⟩

Premises used: Nat.lt_pow_self, Nat.Prime.one_lt, LT.lt.le, And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
refine : p ≤ p ^ 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

Tactic:
refine ⟨p, ?_, k, (Nat.lt_pow_self hp.one_lt).le, hp, hk, rfl⟩
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
lhs : p
| p ≤ p ^ k

Tactic:
lhs
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
rw : HPow.hPow (β := ℕ) p 1
| p

Tactic:
rw [← (pow_one p)]

Premises used: pow_one
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
rw rw₁ : p
rw₂ : HPow.hPow (β := ℕ) p 1
| p ≤ p ^ k

Tactic:
{lhs; rw [← (pow_one p)]}

Premises used: pow_one
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
conv : HPow.hPow (β := ℕ) p 1 ≤ p ^ k
⊢ p ≤ p ^ k

Tactic:
conv => {lhs; rw [← (pow_one p)]}

Premises used: pow_one
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ HPow.hPow (β := ℕ) p 1 ≤ p ^ k

Tactic:
Nat.pow_le_pow_right hp.one_lt.le hk

Premises used: Nat.Prime.one_lt, LT.lt.le, Nat.pow_le_pow_right
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ HPow.hPow (β := ℕ) p 1 ≤ p ^ k

Tactic:
exact Nat.pow_le_pow_right hp.one_lt.le hk

Premises used: Nat.Prime.one_lt, LT.lt.le, Nat.pow_le_pow_right
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
n : ℕ
rw :
  (∃ (p : ℕ), ∃ (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔
    ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p
⊢ IsPrimePow n ↔ ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p

Tactic:
rw [isPrimePow_nat_iff]

Premises used: isPrimePow_nat_iff
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
n : ℕ
mp :
  (∃ (p : ℕ), ∃ (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n) →
    ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p
mpr :
  (∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) →
    ∃ (p : ℕ), ∃ (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n
⊢ (∃ (p : ℕ), ∃ (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔
    ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p

Tactic:
constructor
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
p k : ℕ
hp' : Nat.Prime p
hk' : 0 < k
⊢ ∃ (k_1 : ℕ), k_1 ≤ Nat.log 2 (p ^ k) ∧ 0 < k_1 ∧ ∃ (p_1 : ℕ), p_1 ≤ p ^ k ∧ p ^ k = p_1 ^ k_1 ∧ Nat.Prime p_1

Tactic:
⟨k, ?_, hk', ⟨p, Nat.le_pow hk', rfl, hp'⟩⟩

Premises used: Nat.le_pow, And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
p k : ℕ
hp' : Nat.Prime p
hk' : 0 < k
mp : k ≤ Nat.log 2 (p ^ k)
⊢ ∃ (k_1 : ℕ), k_1 ≤ Nat.log 2 (p ^ k) ∧ 0 < k_1 ∧ ∃ (p_1 : ℕ), p_1 ≤ p ^ k ∧ p ^ k = p_1 ^ k_1 ∧ Nat.Prime p_1

Tactic:
refine ⟨k, ?_, hk', ⟨p, Nat.le_pow hk', rfl, hp'⟩⟩
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
p k : ℕ
hp' : Nat.Prime p
hk' : 0 < k
⊢ k = Nat.log 2 (HPow.hPow (α := ℕ) 2 k)

Tactic:
simp
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
p k : ℕ
hp' : Nat.Prime p
hk' : 0 < k
⊢ Nat.log 2 (HPow.hPow (α := ℕ) 2 k) ≤ Nat.log 2 (p ^ k)

Tactic:
Nat.log_mono Nat.one_lt_two Nat.AtLeastTwo.prop
                                   (Nat.pow_le_pow_left (Nat.Prime.two_le hp') k)

Premises used: Nat.one_lt_two, Nat.AtLeastTwo.prop, Nat.log_mono, Nat.Prime.two_le, Nat.pow_le_pow_left
-- Module: Mathlib.Algebra.IsPrimePow
Goal:
p k : ℕ
hp' : Nat.Prime p
hk' : 0 < k
k₁ : k = Nat.log 2 (HPow.hPow (α := ℕ) 2 k)
⊢ k ≤ Nat.log 2 (p ^ k)

Tactic:
calc
        k = Nat.log 2 (2 ^ k) := by simp
        _ ≤ Nat.log 2 (p ^ k) := Nat.log_mono Nat.one_lt_two Nat.AtLeastTwo.prop
                                   (Nat.pow_le_pow_left (Nat.Prime.two_le hp') k)

Premises used: Nat.one_lt_two, Nat.AtLeastTwo.prop, Nat.log_mono, HPow.hPow, Nat.Prime.two_le, Nat.log, OfNat.ofNat, Nat.pow_le_pow_left