awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c_1 : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst_1 : AddMonoid I
c : ComplexShape I
inst_2 : c.TensorSigns
p : ℤ
⊢ (p + 1).negOnePow = -p.negOnePow
have rw : -p.negOnePow = -p.negOnePow
Tactic: rw [Int.negOnePow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c_1 : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst_1 : AddMonoid I
c : ComplexShape I
inst_2 : c.TensorSigns
x x_1 x_2 : I
⊢ 1 = HMul.hMul (α := ℤˣ) 1 1
have rw : Eq (α := ℤˣ) 1 1
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c_1 : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst_1 : AddMonoid I
c : ComplexShape I
inst_2 : c.TensorSigns
x x_1 x_2 : I
⊢ c.ε₂ c c (x, c.π c c (x_1, x_2)) * c.ε₁ c c (x_1, x_2) = c.ε₁ c c (c.π c c (x, x_1), x_2) * c.ε₂ c c (x, x_1)
have dsimp : c.ε x * 1 = 1 * c.ε x
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c_1 : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst_1 : AddMonoid I
c : ComplexShape I
inst_2 : c.TensorSigns
x x_1 x_2 : I
⊢ c.ε x * 1 = 1 * c.ε x
have rw : c.ε x * 1 = c.ε x
Tactic: rw [one_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c_1 : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst_1 : AddMonoid I
c : ComplexShape I
inst_2 : c.TensorSigns
x x_1 x_2 : I
rw : c.ε x * 1 = c.ε x
⊢ c.ε x * 1 = 1 * c.ε x
have rw₁ : c.ε x = c.ε x
Tactic: rw [one_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c_1 : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst_1 : AddMonoid I
c : ComplexShape I
inst_2 : c.TensorSigns
x x_1 x_2 : I
⊢ c.ε₂ c c (c.π c c (x, x_1), x_2) = c.ε₂ c c (x, c.π c c (x_1, x_2)) * c.ε₂ c c (x_1, x_2)
have dsimp : c.ε (x + x_1) = c.ε x * c.ε x_1
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c_1 : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst_1 : AddMonoid I
c : ComplexShape I
inst_2 : c.TensorSigns
x x_1 x_2 : I
⊢ c.ε (x + x_1) = c.ε x * c.ε x_1
have rw : c.ε x * c.ε x_1 = c.ε x * c.ε x_1
Tactic: rw [ε_add]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₂
i₂ i₂' : I₁
h₂ : c₂.Rel i₁ i₁'
h₁ : c₁.Rel i₂ i₂'
⊢ HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
        | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂') with
        | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
        ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (-match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
          | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁', i₂) with
        | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
have rw : HMul.hMul (α := ℤˣ) (β := ℤˣ)
    (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
      | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
      ℤˣ)
    (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂') with
      | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
      ℤˣ) =
  -HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
        | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁', i₂) with
        | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
Tactic: rw [neg_mul, ComplexShape.ε₂_ε₁ c₁₂ h₁ h₂, neg_mul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₂
i₂ i₂' : I₁
h₂ : c₂.Rel i₁ i₁'
h₁ : c₁.Rel i₂ i₂'
rw :
  HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
        | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂') with
        | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
        ℤˣ) =
    -HMul.hMul (α := ℤˣ) (β := ℤˣ)
        (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
          | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
          ℤˣ)
        (match (motive := I₂ × I₁ → ℤˣ) (i₁', i₂) with
          | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
          ℤˣ)
⊢ HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
        | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂') with
        | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
        ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (-match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
          | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁', i₂) with
        | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
have rw₁ : HMul.hMul (α := ℤˣ) (β := ℤˣ)
    (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
      | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
      ℤˣ)
    (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂') with
      | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
      ℤˣ) =
  -(-c₁.ε₁ c₂ c₁₂ (i₂, i₁) * c₁.ε₂ c₂ c₁₂ (i₂', i₁))
Tactic: rw [neg_mul, ComplexShape.ε₂_ε₁ c₁₂ h₁ h₂, neg_mul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₂
i₂ i₂' : I₁
h₂ : c₂.Rel i₁ i₁'
h₁ : c₁.Rel i₂ i₂'
rw :
  HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
        | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂') with
        | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
        ℤˣ) =
    -HMul.hMul (α := ℤˣ) (β := ℤˣ)
        (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
          | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
          ℤˣ)
        (match (motive := I₂ × I₁ → ℤˣ) (i₁', i₂) with
          | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
          ℤˣ)
rw₁ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
        | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂') with
        | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
        ℤˣ) =
    -(-c₁.ε₁ c₂ c₁₂ (i₂, i₁) * c₁.ε₂ c₂ c₁₂ (i₂', i₁))
⊢ HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
        | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂') with
        | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
        ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (-match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
          | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁', i₂) with
        | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
have rw₂ : HMul.hMul (α := ℤˣ) (β := ℤˣ)
    (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
      | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
      ℤˣ)
    (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂') with
      | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
      ℤˣ) =
  - -(c₁.ε₁ c₂ c₁₂ (i₂, i₁) * c₁.ε₂ c₂ c₁₂ (i₂', i₁))
Tactic: rw [neg_mul, ComplexShape.ε₂_ε₁ c₁₂ h₁ h₂, neg_mul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₂
i₂ i₂' : I₁
h₂ : c₂.Rel i₁ i₁'
h₁ : c₁.Rel i₂ i₂'
rw :
  HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
        | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂') with
        | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
        ℤˣ) =
    -HMul.hMul (α := ℤˣ) (β := ℤˣ)
        (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
          | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
          ℤˣ)
        (match (motive := I₂ × I₁ → ℤˣ) (i₁', i₂) with
          | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
          ℤˣ)
rw₁ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
        | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂') with
        | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
        ℤˣ) =
    -(-c₁.ε₁ c₂ c₁₂ (i₂, i₁) * c₁.ε₂ c₂ c₁₂ (i₂', i₁))
rw₂ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
        | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂') with
        | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
        ℤˣ) =
    - -(c₁.ε₁ c₂ c₁₂ (i₂, i₁) * c₁.ε₂ c₂ c₁₂ (i₂', i₁))
⊢ HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
        | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂') with
        | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
        ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (-match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
          | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
      (match (motive := I₂ × I₁ → ℤˣ) (i₁', i₂) with
        | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
        ℤˣ)
have rw₃ : HMul.hMul (α := ℤˣ) (β := ℤˣ)
    (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂) with
      | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂) :
      ℤˣ)
    (match (motive := I₂ × I₁ → ℤˣ) (i₁, i₂') with
      | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂) :
      ℤˣ) =
  c₁.ε₁ c₂ c₁₂ (i₂, i₁) * c₁.ε₂ c₂ c₁₂ (i₂', i₁)
Tactic: rw [neg_mul, ComplexShape.ε₂_ε₁ c₁₂ h₁ h₂, neg_mul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
p q : ℤ
⊢ (p * q).negOnePow * 1 = q.negOnePow * ((p + 1) * q).negOnePow
have rw : (p * q).negOnePow = q.negOnePow * ((p + 1) * q).negOnePow
Tactic: rw [mul_one, ← Int.negOnePow_add, add_comm q, add_mul, one_mul, Int.negOnePow_add,
      Int.negOnePow_add, mul_assoc, Int.units_mul_self, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
p q : ℤ
rw : (p * q).negOnePow = q.negOnePow * ((p + 1) * q).negOnePow
⊢ (p * q).negOnePow * 1 = q.negOnePow * ((p + 1) * q).negOnePow
have rw₁ : (p * q).negOnePow = (q + (p + 1) * q).negOnePow
Tactic: rw [mul_one, ← Int.negOnePow_add, add_comm q, add_mul, one_mul, Int.negOnePow_add,
      Int.negOnePow_add, mul_assoc, Int.units_mul_self, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
p q : ℤ
rw : (p * q).negOnePow = q.negOnePow * ((p + 1) * q).negOnePow
rw₁ : (p * q).negOnePow = (q + (p + 1) * q).negOnePow
⊢ (p * q).negOnePow * 1 = q.negOnePow * ((p + 1) * q).negOnePow
have rw₂ : (p * q).negOnePow = ((p + 1) * q + q).negOnePow
Tactic: rw [mul_one, ← Int.negOnePow_add, add_comm q, add_mul, one_mul, Int.negOnePow_add,
      Int.negOnePow_add, mul_assoc, Int.units_mul_self, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
p q : ℤ
rw : (p * q).negOnePow = q.negOnePow * ((p + 1) * q).negOnePow
rw₁ : (p * q).negOnePow = (q + (p + 1) * q).negOnePow
rw₂ : (p * q).negOnePow = ((p + 1) * q + q).negOnePow
⊢ (p * q).negOnePow * 1 = q.negOnePow * ((p + 1) * q).negOnePow
have rw₃ : (p * q).negOnePow = (p * q + 1 * q + q).negOnePow
Tactic: rw [mul_one, ← Int.negOnePow_add, add_comm q, add_mul, one_mul, Int.negOnePow_add,
      Int.negOnePow_add, mul_assoc, Int.units_mul_self, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
p q : ℤ
rw : (p * q).negOnePow = q.negOnePow * ((p + 1) * q).negOnePow
rw₁ : (p * q).negOnePow = (q + (p + 1) * q).negOnePow
rw₂ : (p * q).negOnePow = ((p + 1) * q + q).negOnePow
rw₃ : (p * q).negOnePow = (p * q + 1 * q + q).negOnePow
⊢ (p * q).negOnePow * 1 = q.negOnePow * ((p + 1) * q).negOnePow
have rw₄ : (p * q).negOnePow = (p * q + q + q).negOnePow
Tactic: rw [mul_one, ← Int.negOnePow_add, add_comm q, add_mul, one_mul, Int.negOnePow_add,
      Int.negOnePow_add, mul_assoc, Int.units_mul_self, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
p q : ℤ
rw : (p * q).negOnePow = q.negOnePow * ((p + 1) * q).negOnePow
rw₁ : (p * q).negOnePow = (q + (p + 1) * q).negOnePow
rw₂ : (p * q).negOnePow = ((p + 1) * q + q).negOnePow
rw₃ : (p * q).negOnePow = (p * q + 1 * q + q).negOnePow
rw₄ : (p * q).negOnePow = (p * q + q + q).negOnePow
⊢ (p * q).negOnePow * 1 = q.negOnePow * ((p + 1) * q).negOnePow
have rw₅ : (p * q).negOnePow = (p * q + q).negOnePow * q.negOnePow
Tactic: rw [mul_one, ← Int.negOnePow_add, add_comm q, add_mul, one_mul, Int.negOnePow_add,
      Int.negOnePow_add, mul_assoc, Int.units_mul_self, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
p q : ℤ
rw : (p * q).negOnePow = q.negOnePow * ((p + 1) * q).negOnePow
rw₁ : (p * q).negOnePow = (q + (p + 1) * q).negOnePow
rw₂ : (p * q).negOnePow = ((p + 1) * q + q).negOnePow
rw₃ : (p * q).negOnePow = (p * q + 1 * q + q).negOnePow
rw₄ : (p * q).negOnePow = (p * q + q + q).negOnePow
rw₅ : (p * q).negOnePow = (p * q + q).negOnePow * q.negOnePow
⊢ (p * q).negOnePow * 1 = q.negOnePow * ((p + 1) * q).negOnePow
have rw₆ : (p * q).negOnePow = (p * q).negOnePow * q.negOnePow * q.negOnePow
Tactic: rw [mul_one, ← Int.negOnePow_add, add_comm q, add_mul, one_mul, Int.negOnePow_add,
      Int.negOnePow_add, mul_assoc, Int.units_mul_self, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
p q : ℤ
rw : (p * q).negOnePow = q.negOnePow * ((p + 1) * q).negOnePow
rw₁ : (p * q).negOnePow = (q + (p + 1) * q).negOnePow
rw₂ : (p * q).negOnePow = ((p + 1) * q + q).negOnePow
rw₃ : (p * q).negOnePow = (p * q + 1 * q + q).negOnePow
rw₄ : (p * q).negOnePow = (p * q + q + q).negOnePow
rw₅ : (p * q).negOnePow = (p * q + q).negOnePow * q.negOnePow
rw₆ : (p * q).negOnePow = (p * q).negOnePow * q.negOnePow * q.negOnePow
⊢ (p * q).negOnePow * 1 = q.negOnePow * ((p + 1) * q).negOnePow
have rw₇ : (p * q).negOnePow = (p * q).negOnePow * (q.negOnePow * q.negOnePow)
Tactic: rw [mul_one, ← Int.negOnePow_add, add_comm q, add_mul, one_mul, Int.negOnePow_add,
      Int.negOnePow_add, mul_assoc, Int.units_mul_self, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
p q : ℤ
rw : (p * q).negOnePow = q.negOnePow * ((p + 1) * q).negOnePow
rw₁ : (p * q).negOnePow = (q + (p + 1) * q).negOnePow
rw₂ : (p * q).negOnePow = ((p + 1) * q + q).negOnePow
rw₃ : (p * q).negOnePow = (p * q + 1 * q + q).negOnePow
rw₄ : (p * q).negOnePow = (p * q + q + q).negOnePow
rw₅ : (p * q).negOnePow = (p * q + q).negOnePow * q.negOnePow
rw₆ : (p * q).negOnePow = (p * q).negOnePow * q.negOnePow * q.negOnePow
rw₇ : (p * q).negOnePow = (p * q).negOnePow * (q.negOnePow * q.negOnePow)
⊢ (p * q).negOnePow * 1 = q.negOnePow * ((p + 1) * q).negOnePow
have rw₈ : (p * q).negOnePow = (p * q).negOnePow * 1
Tactic: rw [mul_one, ← Int.negOnePow_add, add_comm q, add_mul, one_mul, Int.negOnePow_add,
      Int.negOnePow_add, mul_assoc, Int.units_mul_self, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
p q : ℤ
rw : (p * q).negOnePow = q.negOnePow * ((p + 1) * q).negOnePow
rw₁ : (p * q).negOnePow = (q + (p + 1) * q).negOnePow
rw₂ : (p * q).negOnePow = ((p + 1) * q + q).negOnePow
rw₃ : (p * q).negOnePow = (p * q + 1 * q + q).negOnePow
rw₄ : (p * q).negOnePow = (p * q + q + q).negOnePow
rw₅ : (p * q).negOnePow = (p * q + q).negOnePow * q.negOnePow
rw₆ : (p * q).negOnePow = (p * q).negOnePow * q.negOnePow * q.negOnePow
rw₇ : (p * q).negOnePow = (p * q).negOnePow * (q.negOnePow * q.negOnePow)
rw₈ : (p * q).negOnePow = (p * q).negOnePow * 1
⊢ (p * q).negOnePow * 1 = q.negOnePow * ((p + 1) * q).negOnePow
have rw₉ : (p * q).negOnePow = (p * q).negOnePow
Tactic: rw [mul_one, ← Int.negOnePow_add, add_comm q, add_mul, one_mul, Int.negOnePow_add,
      Int.negOnePow_add, mul_assoc, Int.units_mul_self, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
p q : ℤ
⊢ (p * q).negOnePow * p.negOnePow = 1 * (p * (q + 1)).negOnePow
have rw : (p * q).negOnePow * p.negOnePow = (p * (q + 1)).negOnePow
Tactic: rw [one_mul, ← Int.negOnePow_add, mul_add, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
p q : ℤ
rw : (p * q).negOnePow * p.negOnePow = (p * (q + 1)).negOnePow
⊢ (p * q).negOnePow * p.negOnePow = 1 * (p * (q + 1)).negOnePow
have rw₁ : (p * q + p).negOnePow = (p * (q + 1)).negOnePow
Tactic: rw [one_mul, ← Int.negOnePow_add, mul_add, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
p q : ℤ
rw : (p * q).negOnePow * p.negOnePow = (p * (q + 1)).negOnePow
rw₁ : (p * q + p).negOnePow = (p * (q + 1)).negOnePow
⊢ (p * q).negOnePow * p.negOnePow = 1 * (p * (q + 1)).negOnePow
have rw₂ : (p * q + p).negOnePow = (p * q + p * 1).negOnePow
Tactic: rw [one_mul, ← Int.negOnePow_add, mul_add, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
inst_1 : TotalComplexShape c₂ c₁ c₁₂
inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂
p q : ℤ
rw : (p * q).negOnePow * p.negOnePow = (p * (q + 1)).negOnePow
rw₁ : (p * q + p).negOnePow = (p * (q + 1)).negOnePow
rw₂ : (p * q + p).negOnePow = (p * q + p * 1).negOnePow
⊢ (p * q).negOnePow * p.negOnePow = 1 * (p * (q + 1)).negOnePow
have rw₃ : (p * q + p).negOnePow = (p * q + p).negOnePow
Tactic: rw [one_mul, ← Int.negOnePow_add, mul_add, mul_one]