awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShape (hypothesis)
Goal:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i i' j k : ι
w₁ : c₁.Rel i k
w₂ : c₂.Rel k j
k' : ι
w₁' : c₁.Rel i' k'
w₂' : c₂.Rel k' j
⊢ i = i'
have w₃ : c₁.Rel i k'
Tactic: rw [c₂.prev_eq w₂ w₂'] at w₁
Cleared hypotheses: w₁, w₁', w₂'
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShape (goal)
Goal:
ι : Type u_1
c : ComplexShape ι
i : ι
⊢ Subsingleton.{max 1 (u_1 + 1)} { j : ι // c.Rel i j }
have allEq : ∀ (a b : { j : ι // c.Rel i j }), a = b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShape (goal)
Goal:
ι : Type u_1
c : ComplexShape ι
i j : ι
rij : c.Rel i j
k : ι
rik : c.Rel i k
⊢ Subtype.mk (p := fun (j : ι) ↦ c.Rel i j) j rij = Subtype.mk (p := fun (j : ι) ↦ c.Rel i j) k rik
have allEq : j = k
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShape (goal)
Goal:
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ c.next i = j
have apply : c.Rel i (c.next i)
Tactic: apply c.next_eq _ h
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShape (goal)
Goal:
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ c.Rel i (c.next i)
have rw : c.Rel i (if h : ∃ (j : ι), c.Rel i j then h.choose (p := c.Rel i) else i)
Tactic: rw [next]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShape (goal)
Goal:
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ c.Rel i (if h : ∃ (j : ι), c.Rel i j then h.choose (p := c.Rel i) else i)
have rw : c.Rel i (sorry.choose (p := c.Rel i))
Tactic: rw [dif_pos]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShape (goal)
Goal:
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
rw : c.Rel i (⋯.choose (p := c.Rel i))
⊢ c.Rel i (if h : ∃ (j : ι), c.Rel i j then h.choose (p := c.Rel i) else i)
have hc : ∃ (j : ι), c.Rel i j
Tactic: rw [dif_pos]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁, i₂) * 1 = -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
have rw : c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (c₁.ε₂ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂') * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))) =
  -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
Tactic: rw [← Int.units_mul_self (ComplexShape.ε₁ c₁ c₂ c₁₂ (i₁, i₂')), mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
| c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (c₁.ε₂ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂') * c₁.ε₁ c₂ c₁₂ (i₁, i₂')))
have arg : c₁.ε₂ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂') * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))
Tactic: arg 2
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
| c₁.ε₂ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂') * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))
have rw : -c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
Tactic: rw [← mul_assoc, ε₂_ε₁ c₁₂ h₁ h₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
| c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (c₁.ε₂ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂') * c₁.ε₁ c₂ c₁₂ (i₁, i₂')))
have arg : -c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
Tactic: arg 2
      rw [← mul_assoc, ε₂_ε₁ c₁₂ h₁ h₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (c₁.ε₂ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂') * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
have conv_lhs : c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (-c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
  -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
Tactic: conv_lhs =>
      arg 2
      rw [← mul_assoc, ε₂_ε₁ c₁₂ h₁ h₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (-c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
have rw : c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (-(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂)) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
  -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
Tactic: rw [neg_mul, neg_mul, neg_mul, mul_neg, neg_inj, ← mul_assoc, ← mul_assoc,
      Int.units_mul_self, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
rw :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (-(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂)) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (-c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
have rw₁ : c₁.ε₁ c₂ c₁₂ (i₁, i₂) * -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
  -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
Tactic: rw [neg_mul, neg_mul, neg_mul, mul_neg, neg_inj, ← mul_assoc, ← mul_assoc,
      Int.units_mul_self, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
rw :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (-(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂)) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
rw₁ :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (-c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
have rw₂ : c₁.ε₁ c₂ c₁₂ (i₁, i₂) * -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
  -(c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))
Tactic: rw [neg_mul, neg_mul, neg_mul, mul_neg, neg_inj, ← mul_assoc, ← mul_assoc,
      Int.units_mul_self, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
rw :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (-(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂)) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
rw₁ :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
rw₂ :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -(c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (-c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
have rw₃ : -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))) =
  -(c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))
Tactic: rw [neg_mul, neg_mul, neg_mul, mul_neg, neg_inj, ← mul_assoc, ← mul_assoc,
      Int.units_mul_self, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
rw :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (-(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂)) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
rw₁ :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
rw₂ :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -(c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))
rw₃ :
  -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))) =
    -(c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (-c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
have rw₄ : c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
  c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
Tactic: rw [neg_mul, neg_mul, neg_mul, mul_neg, neg_inj, ← mul_assoc, ← mul_assoc,
      Int.units_mul_self, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
rw :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (-(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂)) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
rw₁ :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
rw₂ :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -(c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))
rw₃ :
  -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))) =
    -(c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))
rw₄ :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (-c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
have rw₅ : c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂)) * c₁.ε₁ c₂ c₁₂ (i₁, i₂') =
  c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
Tactic: rw [neg_mul, neg_mul, neg_mul, mul_neg, neg_inj, ← mul_assoc, ← mul_assoc,
      Int.units_mul_self, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
rw :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (-(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂)) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
rw₁ :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
rw₂ :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -(c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))
rw₃ :
  -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))) =
    -(c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))
rw₄ :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
rw₅ :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂)) * c₁.ε₁ c₂ c₁₂ (i₁, i₂') =
    c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (-c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
have rw₆ : c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂') =
  c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
Tactic: rw [neg_mul, neg_mul, neg_mul, mul_neg, neg_inj, ← mul_assoc, ← mul_assoc,
      Int.units_mul_self, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
rw :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (-(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂)) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
rw₁ :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
rw₂ :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -(c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))
rw₃ :
  -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))) =
    -(c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))
rw₄ :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
rw₅ :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂)) * c₁.ε₁ c₂ c₁₂ (i₁, i₂') =
    c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
rw₆ :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂') =
    c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (-c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
have rw₇ : 1 * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂') = c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
Tactic: rw [neg_mul, neg_mul, neg_mul, mul_neg, neg_inj, ← mul_assoc, ← mul_assoc,
      Int.units_mul_self, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ComplexShapeSigns (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
rw :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (-(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂)) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
rw₁ :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
rw₂ :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -(c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))
rw₃ :
  -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))) =
    -(c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))
rw₄ :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
rw₅ :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂)) * c₁.ε₁ c₂ c₁₂ (i₁, i₂') =
    c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
rw₆ :
  c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂') =
    c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
rw₇ : 1 * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂') = c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (-c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
have rw₈ : c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂') = c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
Tactic: rw [neg_mul, neg_mul, neg_mul, mul_neg, neg_inj, ← mul_assoc, ← mul_assoc,
      Int.units_mul_self, 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
i₁ i₁' i₂ i₂' : I
h : c.Rel i₁ i₁'
h_1 : c.Rel i₂ i₂'
⊢ c.ε i₁ * 1 = -1 * c.ε i₁'
have rw : c.ε i₁ * 1 = -(1 * c.ε i₁')
Tactic: rw [neg_mul, one_mul, mul_one, c.ε_succ h, 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_1 : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst_1 : AddMonoid I
c : ComplexShape I
inst_2 : c.TensorSigns
i₁ i₁' i₂ i₂' : I
h : c.Rel i₁ i₁'
h_1 : c.Rel i₂ i₂'
rw : c.ε i₁ * 1 = -(1 * c.ε i₁')
⊢ c.ε i₁ * 1 = -1 * c.ε i₁'
have rw₁ : c.ε i₁ * 1 = -c.ε i₁'
Tactic: rw [neg_mul, one_mul, mul_one, c.ε_succ h, 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_1 : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst_1 : AddMonoid I
c : ComplexShape I
inst_2 : c.TensorSigns
i₁ i₁' i₂ i₂' : I
h : c.Rel i₁ i₁'
h_1 : c.Rel i₂ i₂'
rw : c.ε i₁ * 1 = -(1 * c.ε i₁')
rw₁ : c.ε i₁ * 1 = -c.ε i₁'
⊢ c.ε i₁ * 1 = -1 * c.ε i₁'
have rw₂ : c.ε i₁ = -c.ε i₁'
Tactic: rw [neg_mul, one_mul, mul_one, c.ε_succ h, 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_1 : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst_1 : AddMonoid I
c : ComplexShape I
inst_2 : c.TensorSigns
i₁ i₁' i₂ i₂' : I
h : c.Rel i₁ i₁'
h_1 : c.Rel i₂ i₂'
rw : c.ε i₁ * 1 = -(1 * c.ε i₁')
rw₁ : c.ε i₁ * 1 = -c.ε i₁'
rw₂ : c.ε i₁ = -c.ε i₁'
⊢ c.ε i₁ * 1 = -1 * c.ε i₁'
have rw₃ : c.ε i₁ = - -c.ε i₁
Tactic: rw [neg_mul, one_mul, mul_one, c.ε_succ h, 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_1 : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst_1 : AddMonoid I
c : ComplexShape I
inst_2 : c.TensorSigns
i₁ i₁' i₂ i₂' : I
h : c.Rel i₁ i₁'
h_1 : c.Rel i₂ i₂'
rw : c.ε i₁ * 1 = -(1 * c.ε i₁')
rw₁ : c.ε i₁ * 1 = -c.ε i₁'
rw₂ : c.ε i₁ = -c.ε i₁'
rw₃ : c.ε i₁ = - -c.ε i₁
⊢ c.ε i₁ * 1 = -1 * c.ε i₁'
have rw₄ : c.ε i₁ = c.ε i₁
Tactic: rw [neg_mul, one_mul, mul_one, c.ε_succ h, 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_1 : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst_1 : AddMonoid I
c : ComplexShape I
inst_2 : c.TensorSigns
q : ℕ
⊢ HPow.hPow (α := ℤˣ) (-1) q = -HPow.hPow (α := ℤˣ) (-1) (q + 1)
have rw : HPow.hPow (α := ℤˣ) (-1) q = -(HPow.hPow (α := ℤˣ) (-1) q * HPow.hPow (α := ℤˣ) (β := ℕ) (-1) 1)
Tactic: rw [pow_add, pow_one, mul_neg, mul_one, 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_1 : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst_1 : AddMonoid I
c : ComplexShape I
inst_2 : c.TensorSigns
q : ℕ
rw : HPow.hPow (α := ℤˣ) (-1) q = -(HPow.hPow (α := ℤˣ) (-1) q * HPow.hPow (α := ℤˣ) (β := ℕ) (-1) 1)
⊢ HPow.hPow (α := ℤˣ) (-1) q = -HPow.hPow (α := ℤˣ) (-1) (q + 1)
have rw₁ : HPow.hPow (α := ℤˣ) (-1) q = -(HPow.hPow (α := ℤˣ) (-1) q * -1)
Tactic: rw [pow_add, pow_one, mul_neg, mul_one, 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_1 : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst_1 : AddMonoid I
c : ComplexShape I
inst_2 : c.TensorSigns
q : ℕ
rw : HPow.hPow (α := ℤˣ) (-1) q = -(HPow.hPow (α := ℤˣ) (-1) q * HPow.hPow (α := ℤˣ) (β := ℕ) (-1) 1)
rw₁ : HPow.hPow (α := ℤˣ) (-1) q = -(HPow.hPow (α := ℤˣ) (-1) q * -1)
⊢ HPow.hPow (α := ℤˣ) (-1) q = -HPow.hPow (α := ℤˣ) (-1) (q + 1)
have rw₂ : HPow.hPow (α := ℤˣ) (-1) q = - -(HPow.hPow (α := ℤˣ) (-1) q * 1)
Tactic: rw [pow_add, pow_one, mul_neg, mul_one, 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_1 : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst_1 : AddMonoid I
c : ComplexShape I
inst_2 : c.TensorSigns
q : ℕ
rw : HPow.hPow (α := ℤˣ) (-1) q = -(HPow.hPow (α := ℤˣ) (-1) q * HPow.hPow (α := ℤˣ) (β := ℕ) (-1) 1)
rw₁ : HPow.hPow (α := ℤˣ) (-1) q = -(HPow.hPow (α := ℤˣ) (-1) q * -1)
rw₂ : HPow.hPow (α := ℤˣ) (-1) q = - -(HPow.hPow (α := ℤˣ) (-1) q * 1)
⊢ HPow.hPow (α := ℤˣ) (-1) q = -HPow.hPow (α := ℤˣ) (-1) (q + 1)
have rw₃ : HPow.hPow (α := ℤˣ) (-1) q = - -HPow.hPow (α := ℤˣ) (-1) q
Tactic: rw [pow_add, pow_one, mul_neg, mul_one, 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_1 : ComplexShape J
inst : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst_1 : AddMonoid I
c : ComplexShape I
inst_2 : c.TensorSigns
q : ℕ
rw : HPow.hPow (α := ℤˣ) (-1) q = -(HPow.hPow (α := ℤˣ) (-1) q * HPow.hPow (α := ℤˣ) (β := ℕ) (-1) 1)
rw₁ : HPow.hPow (α := ℤˣ) (-1) q = -(HPow.hPow (α := ℤˣ) (-1) q * -1)
rw₂ : HPow.hPow (α := ℤˣ) (-1) q = - -(HPow.hPow (α := ℤˣ) (-1) q * 1)
rw₃ : HPow.hPow (α := ℤˣ) (-1) q = - -HPow.hPow (α := ℤˣ) (-1) q
⊢ HPow.hPow (α := ℤˣ) (-1) q = -HPow.hPow (α := ℤˣ) (-1) (q + 1)
have rw₄ : HPow.hPow (α := ℤˣ) (-1) q = HPow.hPow (α := ℤˣ) (-1) q
Tactic: rw [pow_add, pow_one, mul_neg, mul_one, neg_neg]