awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a r : α
h₁ :
  HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) *
      (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) =
    0
h₂ :
  HMul.hMul (α := α) ((f * g : (a : α) → α) a : α)
        (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) -
      HMul.hMul (α := α) ((g * f : (a : α) → α) a : α)
        (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) =
    0
h₃ :
  HMul.hMul (α := α) ((f * g : (a : α) → α) a : α)
      (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) =
    HMul.hMul (α := α) ((g * f : (a : α) → α) a : α)
      (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α))
h₄ :
  (f * g : (a : α) → α)
      (a * (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α))) =
    HMul.hMul (α := α) ((g * f : (a : α) → α) a : α)
      (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α))
h₅ :
  Eq (α := α)
    ((f * g : (a : α) → α)
        (a * (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α))) :
      α)
    ((g * f : (a : α) → α)
        (a * (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α))) :
      α)
h₆ :
  Eq (α := α)
    (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α)
        (a *
          (r *
            HSub.hSub (α := α) (β := α) (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α) a : α)
              ((g * f : (a : α) → α) a : α))) :
      α)
    ((g * f : (a : α) → α)
        (a *
          (r *
            HSub.hSub (α := α) (β := α) (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α) a : α)
              ((g * f : (a : α) → α) a : α))) :
      α)
⊢ HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) * r *
      HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) =
    0
have h₇ : Eq (α := α)
  (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α)
    (a *
      (r *
        HSub.hSub (α := α) (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α) a)
          (Function.comp (β := α) (⇑g : (a : α) → α) (⇑f : (a : α) → α) a))))
  (Function.comp (β := α) (⇑g : (a : α) → α) (⇑f : (a : α) → α)
    (a *
      (r *
        HSub.hSub (α := α) (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α) a)
          (Function.comp (β := α) (⇑g : (a : α) → α) (⇑f : (a : α) → α) a))))
Tactic: rw [mul_assoc, sub_mul, sub_eq_zero, ← map_mul_right, ← map_mul_right, coe_mul, coe_mul,
        comp_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CharZero (goal)
Goal:
α : Type u_1
R : Type u_2
S : Type u_3
n : ℕ
inst : AddMonoidWithOne R
inst_1 : CharZero R
⊢ Ne.{u_2 + 1} (α := R) 2 0
have rw : Ne (α := ℕ) 2 0
Tactic: rw [← Nat.cast_two, Nat.cast_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CharZero (goal)
Goal:
R : Type u_2
S : Type u_3
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
ϕ : R →+* S
inst_2 : CharZero S
a b : ℕ
h : Eq.{u_2 + 1} (α := R) (↑a : R) (↑b : R)
⊢ Eq.{u_3 + 1} (α := S) (↑a : S) (↑b : S)
have rw : Eq.{u_3 + 1} (α := S) ((ϕ : (a : R) → S) (↑a : R) : S) ((↑b : S) : S)
Tactic: rw [← map_natCast ϕ, ← map_natCast ϕ, h]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CharZero (goal)
Goal:
R : Type u_2
S : Type u_3
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
ϕ : R →+* S
inst_2 : CharZero S
a b : ℕ
h : Eq.{u_2 + 1} (α := R) (↑a : R) (↑b : R)
rw : Eq.{u_3 + 1} (α := S) ((ϕ : (a : R) → S) (↑a : R) : S) ((↑b : S) : S)
⊢ Eq.{u_3 + 1} (α := S) (↑a : S) (↑b : S)
have rw₁ : Eq.{u_3 + 1} (α := S) ((ϕ : (a : R) → S) (↑a : R) : S) ((ϕ : (a : R) → S) (↑b : R) : S)
Tactic: rw [← map_natCast ϕ, ← map_natCast ϕ, h]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CharZero (goal)
Goal:
R : Type u_2
S : Type u_3
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
ϕ : R →+* S
inst_2 : CharZero S
a b : ℕ
h : Eq.{u_2 + 1} (α := R) (↑a : R) (↑b : R)
rw : Eq.{u_3 + 1} (α := S) ((ϕ : (a : R) → S) (↑a : R) : S) ((↑b : S) : S)
rw₁ : Eq.{u_3 + 1} (α := S) ((ϕ : (a : R) → S) (↑a : R) : S) ((ϕ : (a : R) → S) (↑b : R) : S)
⊢ Eq.{u_3 + 1} (α := S) (↑a : S) (↑b : S)
have rw₂ : Eq.{u_3 + 1} (α := S) ((ϕ : (a : R) → S) (↑b : R) : S) ((ϕ : (a : R) → S) (↑b : R) : S)
Tactic: rw [← map_natCast ϕ, ← map_natCast ϕ, h]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CharZero (goal)
Goal:
R : Type u_2
S : Type u_3
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
ϕ : R →+* S
hϕ : Injective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑ϕ : (a : R) → S)
hR : CharZero R
a b : ℕ
h : Eq.{u_3 + 1} (α := S) (↑a : S) (↑b : S)
⊢ a = b
have rwa : Eq.{u_2 + 1} (α := R) (↑a : R) (↑b : R)
Tactic: rwa [← @Nat.cast_inj R, ← hϕ.eq_iff, map_natCast ϕ, map_natCast ϕ]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CharZero (goal)
Goal:
R : Type u_2
S : Type u_3
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
ϕ : R →+* S
hϕ : Injective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑ϕ : (a : R) → S)
hR : CharZero R
a b : ℕ
h : Eq.{u_3 + 1} (α := S) (↑a : S) (↑b : S)
rwa : Eq.{u_2 + 1} (α := R) (↑a : R) (↑b : R)
⊢ a = b
have rwa₁ : Eq.{u_3 + 1} (α := S) ((ϕ : (a : R) → S) (↑a : R) : S) ((ϕ : (a : R) → S) (↑b : R) : S)
Tactic: rwa [← @Nat.cast_inj R, ← hϕ.eq_iff, map_natCast ϕ, map_natCast ϕ]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CharZero (goal)
Goal:
R : Type u_2
S : Type u_3
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
ϕ : R →+* S
hϕ : Injective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑ϕ : (a : R) → S)
hR : CharZero R
a b : ℕ
h : Eq.{u_3 + 1} (α := S) (↑a : S) (↑b : S)
rwa : Eq.{u_2 + 1} (α := R) (↑a : R) (↑b : R)
rwa₁ : Eq.{u_3 + 1} (α := S) ((ϕ : (a : R) → S) (↑a : R) : S) ((ϕ : (a : R) → S) (↑b : R) : S)
⊢ a = b
have rwa₂ : Eq.{u_3 + 1} (α := S) ((↑a : S) : S) ((ϕ : (a : R) → S) (↑b : R) : S)
Tactic: rwa [← @Nat.cast_inj R, ← hϕ.eq_iff, map_natCast ϕ, map_natCast ϕ]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CharZero (hypothesis)
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
n : ℕ
a b : R
h : (↑n : R) * a = (↑n : R) * b
⊢ n = 0 ∨ a = b
have h₁ : Eq.{u_2 + 1} (α := R) (↑n : R) 0 ∨ a = b
Tactic: rw [← sub_eq_zero, ← mul_sub, mul_eq_zero, sub_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Ring.CharZero (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : CharZero R
u : Rˣ
⊢ u ≠ -u
have simp_rw : ¬u = -u
Tactic: simp_rw [ne_eq, Units.ext_iff, Units.val_neg, eq_neg_iff_add_eq_zero, ← two_mul,
    Units.mul_left_eq_zero, two_ne_zero, not_false_iff]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CharZero (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : CharZero R
u : Rˣ
simp_rw : ¬u = -u
⊢ u ≠ -u
have simp_rw₁ : ¬(↑u : R) = (↑(-u) : R)
Tactic: simp_rw [ne_eq, Units.ext_iff, Units.val_neg, eq_neg_iff_add_eq_zero, ← two_mul,
    Units.mul_left_eq_zero, two_ne_zero, not_false_iff]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CharZero (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : CharZero R
u : Rˣ
simp_rw : ¬u = -u
simp_rw₁ : ¬(↑u : R) = (↑(-u) : R)
⊢ u ≠ -u
have simp_rw₂ : ¬(↑u : R) = -(↑u : R)
Tactic: simp_rw [ne_eq, Units.ext_iff, Units.val_neg, eq_neg_iff_add_eq_zero, ← two_mul,
    Units.mul_left_eq_zero, two_ne_zero, not_false_iff]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CharZero (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : CharZero R
u : Rˣ
simp_rw : ¬u = -u
simp_rw₁ : ¬(↑u : R) = (↑(-u) : R)
simp_rw₂ : ¬(↑u : R) = -(↑u : R)
⊢ u ≠ -u
have simp_rw₃ : ¬(↑u : R) + (↑u : R) = 0
Tactic: simp_rw [ne_eq, Units.ext_iff, Units.val_neg, eq_neg_iff_add_eq_zero, ← two_mul,
    Units.mul_left_eq_zero, two_ne_zero, not_false_iff]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CharZero (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : CharZero R
u : Rˣ
simp_rw : ¬u = -u
simp_rw₁ : ¬(↑u : R) = (↑(-u) : R)
simp_rw₂ : ¬(↑u : R) = -(↑u : R)
simp_rw₃ : ¬(↑u : R) + (↑u : R) = 0
⊢ u ≠ -u
have simp_rw₄ : ¬2 * (↑u : R) = 0
Tactic: simp_rw [ne_eq, Units.ext_iff, Units.val_neg, eq_neg_iff_add_eq_zero, ← two_mul,
    Units.mul_left_eq_zero, two_ne_zero, not_false_iff]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CharZero (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : CharZero R
u : Rˣ
simp_rw : ¬u = -u
simp_rw₁ : ¬(↑u : R) = (↑(-u) : R)
simp_rw₂ : ¬(↑u : R) = -(↑u : R)
simp_rw₃ : ¬(↑u : R) + (↑u : R) = 0
simp_rw₄ : ¬2 * (↑u : R) = 0
⊢ u ≠ -u
have simp_rw₅ : ¬Eq.{u_2 + 1} (α := R) 2 0
Tactic: simp_rw [ne_eq, Units.ext_iff, Units.val_neg, eq_neg_iff_add_eq_zero, ← two_mul,
    Units.mul_left_eq_zero, two_ne_zero, not_false_iff]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CharZero (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : CharZero R
u : Rˣ
simp_rw : ¬u = -u
simp_rw₁ : ¬(↑u : R) = (↑(-u) : R)
simp_rw₂ : ¬(↑u : R) = -(↑u : R)
simp_rw₃ : ¬(↑u : R) + (↑u : R) = 0
simp_rw₄ : ¬2 * (↑u : R) = 0
simp_rw₅ : ¬Eq.{u_2 + 1} (α := R) 2 0
⊢ u ≠ -u
have simp_rw₆ : ¬False
Tactic: simp_rw [ne_eq, Units.ext_iff, Units.val_neg, eq_neg_iff_add_eq_zero, ← two_mul,
    Units.mul_left_eq_zero, two_ne_zero, not_false_iff]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
a b : R
h : Commute a b
⊢ a * a - b * b = (a + b) * (a - b)
have rw : a * a - b * b = a * (a - b) + b * (a - b)
Tactic: rw [add_mul, mul_sub, mul_sub, h.eq, sub_add_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
a b : R
h : Commute a b
rw : a * a - b * b = a * (a - b) + b * (a - b)
⊢ a * a - b * b = (a + b) * (a - b)
have rw₁ : a * a - b * b = a * a - a * b + b * (a - b)
Tactic: rw [add_mul, mul_sub, mul_sub, h.eq, sub_add_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
a b : R
h : Commute a b
rw : a * a - b * b = a * (a - b) + b * (a - b)
rw₁ : a * a - b * b = a * a - a * b + b * (a - b)
⊢ a * a - b * b = (a + b) * (a - b)
have rw₂ : a * a - b * b = a * a - a * b + (b * a - b * b)
Tactic: rw [add_mul, mul_sub, mul_sub, h.eq, sub_add_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
a b : R
h : Commute a b
rw : a * a - b * b = a * (a - b) + b * (a - b)
rw₁ : a * a - b * b = a * a - a * b + b * (a - b)
rw₂ : a * a - b * b = a * a - a * b + (b * a - b * b)
⊢ a * a - b * b = (a + b) * (a - b)
have rw₃ : a * a - b * b = a * a - b * a + (b * a - b * b)
Tactic: rw [add_mul, mul_sub, mul_sub, h.eq, sub_add_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
a b : R
h : Commute a b
rw : a * a - b * b = a * (a - b) + b * (a - b)
rw₁ : a * a - b * b = a * a - a * b + b * (a - b)
rw₂ : a * a - b * b = a * a - a * b + (b * a - b * b)
rw₃ : a * a - b * b = a * a - b * a + (b * a - b * b)
⊢ a * a - b * b = (a + b) * (a - b)
have rw₄ : a * a - b * b = a * a - b * b
Tactic: rw [add_mul, mul_sub, mul_sub, h.eq, sub_add_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
a b : R
h : Commute a b
⊢ a * a - b * b = (a - b) * (a + b)
have rw : a * a - b * b = (a - b) * a + (a - b) * b
Tactic: rw [mul_add, sub_mul, sub_mul, h.eq, sub_add_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
a b : R
h : Commute a b
rw : a * a - b * b = (a - b) * a + (a - b) * b
⊢ a * a - b * b = (a - b) * (a + b)
have rw₁ : a * a - b * b = a * a - b * a + (a - b) * b
Tactic: rw [mul_add, sub_mul, sub_mul, h.eq, sub_add_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
a b : R
h : Commute a b
rw : a * a - b * b = (a - b) * a + (a - b) * b
rw₁ : a * a - b * b = a * a - b * a + (a - b) * b
⊢ a * a - b * b = (a - b) * (a + b)
have rw₂ : a * a - b * b = a * a - b * a + (a * b - b * b)
Tactic: rw [mul_add, sub_mul, sub_mul, h.eq, sub_add_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
a b : R
h : Commute a b
rw : a * a - b * b = (a - b) * a + (a - b) * b
rw₁ : a * a - b * b = a * a - b * a + (a - b) * b
rw₂ : a * a - b * b = a * a - b * a + (a * b - b * b)
⊢ a * a - b * b = (a - b) * (a + b)
have rw₃ : a * a - b * b = a * a - b * a + (b * a - b * b)
Tactic: rw [mul_add, sub_mul, sub_mul, h.eq, sub_add_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
a b : R
h : Commute a b
rw : a * a - b * b = (a - b) * a + (a - b) * b
rw₁ : a * a - b * b = a * a - b * a + (a - b) * b
rw₂ : a * a - b * b = a * a - b * a + (a * b - b * b)
rw₃ : a * a - b * b = a * a - b * a + (b * a - b * b)
⊢ a * a - b * b = (a - b) * (a + b)
have rw₄ : a * a - b * b = a * a - b * b
Tactic: rw [mul_add, sub_mul, sub_mul, h.eq, sub_add_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
inst_1 : NoZeroDivisors R
a b : R
h : Commute a b
⊢ a * a = b * b ↔ a = b ∨ a = -b
have rw : a * a - b * b = 0 ↔ a = b ∨ a = -b
Tactic: rw [← sub_eq_zero, h.mul_self_sub_mul_self_eq, mul_eq_zero, or_comm, sub_eq_zero,
    add_eq_zero_iff_eq_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
inst_1 : NoZeroDivisors R
a b : R
h : Commute a b
rw : a * a - b * b = 0 ↔ a = b ∨ a = -b
⊢ a * a = b * b ↔ a = b ∨ a = -b
have rw₁ : (a + b) * (a - b) = 0 ↔ a = b ∨ a = -b
Tactic: rw [← sub_eq_zero, h.mul_self_sub_mul_self_eq, mul_eq_zero, or_comm, sub_eq_zero,
    add_eq_zero_iff_eq_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
inst_1 : NoZeroDivisors R
a b : R
h : Commute a b
rw : a * a - b * b = 0 ↔ a = b ∨ a = -b
rw₁ : (a + b) * (a - b) = 0 ↔ a = b ∨ a = -b
⊢ a * a = b * b ↔ a = b ∨ a = -b
have rw₂ : a + b = 0 ∨ a - b = 0 ↔ a = b ∨ a = -b
Tactic: rw [← sub_eq_zero, h.mul_self_sub_mul_self_eq, mul_eq_zero, or_comm, sub_eq_zero,
    add_eq_zero_iff_eq_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
inst_1 : NoZeroDivisors R
a b : R
h : Commute a b
rw : a * a - b * b = 0 ↔ a = b ∨ a = -b
rw₁ : (a + b) * (a - b) = 0 ↔ a = b ∨ a = -b
rw₂ : a + b = 0 ∨ a - b = 0 ↔ a = b ∨ a = -b
⊢ a * a = b * b ↔ a = b ∨ a = -b
have rw₃ : a - b = 0 ∨ a + b = 0 ↔ a = b ∨ a = -b
Tactic: rw [← sub_eq_zero, h.mul_self_sub_mul_self_eq, mul_eq_zero, or_comm, sub_eq_zero,
    add_eq_zero_iff_eq_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
inst_1 : NoZeroDivisors R
a b : R
h : Commute a b
rw : a * a - b * b = 0 ↔ a = b ∨ a = -b
rw₁ : (a + b) * (a - b) = 0 ↔ a = b ∨ a = -b
rw₂ : a + b = 0 ∨ a - b = 0 ↔ a = b ∨ a = -b
rw₃ : a - b = 0 ∨ a + b = 0 ↔ a = b ∨ a = -b
⊢ a * a = b * b ↔ a = b ∨ a = -b
have rw₄ : a = b ∨ a + b = 0 ↔ a = b ∨ a = -b
Tactic: rw [← sub_eq_zero, h.mul_self_sub_mul_self_eq, mul_eq_zero, or_comm, sub_eq_zero,
    add_eq_zero_iff_eq_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
inst_1 : NoZeroDivisors R
a b : R
h : Commute a b
rw : a * a - b * b = 0 ↔ a = b ∨ a = -b
rw₁ : (a + b) * (a - b) = 0 ↔ a = b ∨ a = -b
rw₂ : a + b = 0 ∨ a - b = 0 ↔ a = b ∨ a = -b
rw₃ : a - b = 0 ∨ a + b = 0 ↔ a = b ∨ a = -b
rw₄ : a = b ∨ a + b = 0 ↔ a = b ∨ a = -b
⊢ a * a = b * b ↔ a = b ∨ a = -b
have rw₅ : a = b ∨ a = -b ↔ a = b ∨ a = -b
Tactic: rw [← sub_eq_zero, h.mul_self_sub_mul_self_eq, mul_eq_zero, or_comm, sub_eq_zero,
    add_eq_zero_iff_eq_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Ring R
a b : R
h : Commute a b
⊢ HPow.hPow (β := ℕ) a 2 - HPow.hPow (β := ℕ) b 2 = (a + b) * (a - b)
have rw : a * a - HPow.hPow (β := ℕ) b 2 = (a + b) * (a - b)
Tactic: rw [sq, sq, h.mul_self_sub_mul_self_eq]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Ring R
a b : R
h : Commute a b
rw : a * a - HPow.hPow (β := ℕ) b 2 = (a + b) * (a - b)
⊢ HPow.hPow (β := ℕ) a 2 - HPow.hPow (β := ℕ) b 2 = (a + b) * (a - b)
have rw₁ : a * a - b * b = (a + b) * (a - b)
Tactic: rw [sq, sq, h.mul_self_sub_mul_self_eq]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Ring R
a b : R
h : Commute a b
rw : a * a - HPow.hPow (β := ℕ) b 2 = (a + b) * (a - b)
rw₁ : a * a - b * b = (a + b) * (a - b)
⊢ HPow.hPow (β := ℕ) a 2 - HPow.hPow (β := ℕ) b 2 = (a + b) * (a - b)
have rw₂ : (a + b) * (a - b) = (a + b) * (a - b)
Tactic: rw [sq, sq, h.mul_self_sub_mul_self_eq]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Ring R
a b : R
inst_1 : NoZeroDivisors R
h : Commute a b
⊢ HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2 ↔ a = b ∨ a = -b
have rw : HPow.hPow (β := ℕ) a 2 - HPow.hPow (β := ℕ) b 2 = 0 ↔ a = b ∨ a = -b
Tactic: rw [← sub_eq_zero, h.sq_sub_sq, mul_eq_zero, add_eq_zero_iff_eq_neg, sub_eq_zero, or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Ring R
a b : R
inst_1 : NoZeroDivisors R
h : Commute a b
rw : HPow.hPow (β := ℕ) a 2 - HPow.hPow (β := ℕ) b 2 = 0 ↔ a = b ∨ a = -b
⊢ HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2 ↔ a = b ∨ a = -b
have rw₁ : (a + b) * (a - b) = 0 ↔ a = b ∨ a = -b
Tactic: rw [← sub_eq_zero, h.sq_sub_sq, mul_eq_zero, add_eq_zero_iff_eq_neg, sub_eq_zero, or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Ring R
a b : R
inst_1 : NoZeroDivisors R
h : Commute a b
rw : HPow.hPow (β := ℕ) a 2 - HPow.hPow (β := ℕ) b 2 = 0 ↔ a = b ∨ a = -b
rw₁ : (a + b) * (a - b) = 0 ↔ a = b ∨ a = -b
⊢ HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2 ↔ a = b ∨ a = -b
have rw₂ : a + b = 0 ∨ a - b = 0 ↔ a = b ∨ a = -b
Tactic: rw [← sub_eq_zero, h.sq_sub_sq, mul_eq_zero, add_eq_zero_iff_eq_neg, sub_eq_zero, or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Ring R
a b : R
inst_1 : NoZeroDivisors R
h : Commute a b
rw : HPow.hPow (β := ℕ) a 2 - HPow.hPow (β := ℕ) b 2 = 0 ↔ a = b ∨ a = -b
rw₁ : (a + b) * (a - b) = 0 ↔ a = b ∨ a = -b
rw₂ : a + b = 0 ∨ a - b = 0 ↔ a = b ∨ a = -b
⊢ HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2 ↔ a = b ∨ a = -b
have rw₃ : a = -b ∨ a - b = 0 ↔ a = b ∨ a = -b
Tactic: rw [← sub_eq_zero, h.sq_sub_sq, mul_eq_zero, add_eq_zero_iff_eq_neg, sub_eq_zero, or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Ring R
a b : R
inst_1 : NoZeroDivisors R
h : Commute a b
rw : HPow.hPow (β := ℕ) a 2 - HPow.hPow (β := ℕ) b 2 = 0 ↔ a = b ∨ a = -b
rw₁ : (a + b) * (a - b) = 0 ↔ a = b ∨ a = -b
rw₂ : a + b = 0 ∨ a - b = 0 ↔ a = b ∨ a = -b
rw₃ : a = -b ∨ a - b = 0 ↔ a = b ∨ a = -b
⊢ HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2 ↔ a = b ∨ a = -b
have rw₄ : a = -b ∨ a = b ↔ a = b ∨ a = -b
Tactic: rw [← sub_eq_zero, h.sq_sub_sq, mul_eq_zero, add_eq_zero_iff_eq_neg, sub_eq_zero, or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Ring R
a b : R
inst_1 : NoZeroDivisors R
h : Commute a b
rw : HPow.hPow (β := ℕ) a 2 - HPow.hPow (β := ℕ) b 2 = 0 ↔ a = b ∨ a = -b
rw₁ : (a + b) * (a - b) = 0 ↔ a = b ∨ a = -b
rw₂ : a + b = 0 ∨ a - b = 0 ↔ a = b ∨ a = -b
rw₃ : a = -b ∨ a - b = 0 ↔ a = b ∨ a = -b
rw₄ : a = -b ∨ a = b ↔ a = b ∨ a = -b
⊢ HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2 ↔ a = b ∨ a = -b
have rw₅ : a = b ∨ a = -b ↔ a = b ∨ a = -b
Tactic: rw [← sub_eq_zero, h.sq_sub_sq, mul_eq_zero, add_eq_zero_iff_eq_neg, sub_eq_zero, or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Monoid R
inst_1 : HasDistribNeg R
n : ℕ
h : HPow.hPow (α := R) (-1) n = -1
⊢ HPow.hPow (α := R) (-1) (n + 1) = 1
have rw : HPow.hPow (α := R) (-1) n * -1 = 1
Tactic: rw [pow_succ, h, neg_one_mul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Monoid R
inst_1 : HasDistribNeg R
n : ℕ
h : HPow.hPow (α := R) (-1) n = -1
rw : HPow.hPow (α := R) (-1) n * -1 = 1
⊢ HPow.hPow (α := R) (-1) (n + 1) = 1
have rw₁ : HMul.hMul (α := R) (-1) (-1) = 1
Tactic: rw [pow_succ, h, neg_one_mul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Monoid R
inst_1 : HasDistribNeg R
n : ℕ
h : HPow.hPow (α := R) (-1) n = -1
rw : HPow.hPow (α := R) (-1) n * -1 = 1
rw₁ : HMul.hMul (α := R) (-1) (-1) = 1
⊢ HPow.hPow (α := R) (-1) (n + 1) = 1
have rw₂ : Eq.{u + 1} (α := R) (- -1) 1
Tactic: rw [pow_succ, h, neg_one_mul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Monoid R
inst_1 : HasDistribNeg R
n : ℕ
h : HPow.hPow (α := R) (-1) n = -1
rw : HPow.hPow (α := R) (-1) n * -1 = 1
rw₁ : HMul.hMul (α := R) (-1) (-1) = 1
rw₂ : Eq.{u + 1} (α := R) (- -1) 1
⊢ HPow.hPow (α := R) (-1) (n + 1) = 1
have rw₃ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [pow_succ, h, neg_one_mul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Monoid R
inst_1 : HasDistribNeg R
n : ℕ
h : HPow.hPow (α := R) (-1) n = 1
⊢ HPow.hPow (α := R) (-1) (n + 1) = -1
have rw : HPow.hPow (α := R) (-1) n * -1 = -1
Tactic: rw [pow_succ, h, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Monoid R
inst_1 : HasDistribNeg R
n : ℕ
h : HPow.hPow (α := R) (-1) n = 1
rw : HPow.hPow (α := R) (-1) n * -1 = -1
⊢ HPow.hPow (α := R) (-1) (n + 1) = -1
have rw₁ : HMul.hMul (α := R) 1 (-1) = -1
Tactic: rw [pow_succ, h, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Monoid R
inst_1 : HasDistribNeg R
n : ℕ
h : HPow.hPow (α := R) (-1) n = 1
rw : HPow.hPow (α := R) (-1) n * -1 = -1
rw₁ : HMul.hMul (α := R) 1 (-1) = -1
⊢ HPow.hPow (α := R) (-1) (n + 1) = -1
have rw₂ : Eq.{u + 1} (α := R) (-1) (-1)
Tactic: rw [pow_succ, h, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Ring R
a : R
n : ℕ
⊢ HPow.hPow (α := R) (-1) n * a = 0 ↔ a = 0
have inl : ∀ (h : HPow.hPow (α := R) (-1) n = 1), HPow.hPow (α := R) (-1) n * a = 0 ↔ a = 0
Tactic: rcases neg_one_pow_eq_or R n with h | h
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Ring R
a : R
n : ℕ
inl : ∀ (h : HPow.hPow (α := R) (-1) n = 1), HPow.hPow (α := R) (-1) n * a = 0 ↔ a = 0
⊢ HPow.hPow (α := R) (-1) n * a = 0 ↔ a = 0
have inr : ∀ (h : HPow.hPow (α := R) (-1) n = -1), HPow.hPow (α := R) (-1) n * a = 0 ↔ a = 0
Tactic: rcases neg_one_pow_eq_or R n with h | h
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Ring R
a : R
n : ℕ
⊢ a * HPow.hPow (α := R) (-1) n = 0 ↔ a = 0
have inl : ∀ (h : HPow.hPow (α := R) (-1) n = 1), a * HPow.hPow (α := R) (-1) n = 0 ↔ a = 0
Tactic: obtain h | h := neg_one_pow_eq_or R n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Ring R
a : R
n : ℕ
inl : ∀ (h : HPow.hPow (α := R) (-1) n = 1), a * HPow.hPow (α := R) (-1) n = 0 ↔ a = 0
⊢ a * HPow.hPow (α := R) (-1) n = 0 ↔ a = 0
have inr : ∀ (h : HPow.hPow (α := R) (-1) n = -1), a * HPow.hPow (α := R) (-1) n = 0 ↔ a = 0
Tactic: obtain h | h := neg_one_pow_eq_or R n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
⊢ HPow.hPow (α := R) (-1) n = HPow.hPow (α := R) (-1) (n % 2)
have rw : HPow.hPow (α := R) (-1) (n % 2) * HPow.hPow (α := R) (β := ℕ) (-1) 2 ^ (n / 2) =
  HPow.hPow (α := R) (-1) ((n % 2 + 2 * (n / 2)) % 2)
Tactic: rw [← Nat.mod_add_div n 2, pow_add, pow_mul]