[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing R
a b : R
h : Commute a b
⊢ a * a - b * b = (a + b) * (a - b)
[PROOFSTEP]
rw [add_mul, mul_sub, mul_sub, h.eq, sub_add_sub_cancel]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing R
a b : R
h : Commute a b
⊢ a * a - b * b = (a - b) * (a + b)
[PROOFSTEP]
rw [mul_add, sub_mul, sub_mul, h.eq, sub_add_sub_cancel]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NoZeroDivisors R
a b : R
h : Commute a b
⊢ a * a = b * b ↔ a = b ∨ a = -b
[PROOFSTEP]
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]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonAssocRing R
a : R
⊢ a * a - 1 = (a + 1) * (a - 1)
[PROOFSTEP]
rw [← (Commute.one_right a).mul_self_sub_mul_self_eq, mul_one]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : NonAssocRing R
inst✝ : NoZeroDivisors R
a : R
⊢ a * a = 1 ↔ a = 1 ∨ a = -1
[PROOFSTEP]
rw [← (Commute.one_right a).mul_self_eq_mul_self_iff, mul_one]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ u⁻¹ = u ↔ u = 1 ∨ u = -1
[PROOFSTEP]
rw [inv_eq_iff_mul_eq_one]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ u * u = 1 ↔ u = 1 ∨ u = -1
[PROOFSTEP]
simp only [ext_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ ↑(u * u) = ↑1 ↔ ↑u = ↑1 ∨ ↑u = ↑(-1)
[PROOFSTEP]
push_cast
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ ↑u * ↑u = 1 ↔ ↑u = 1 ∨ ↑u = -1
[PROOFSTEP]
exact mul_self_eq_one_iff
