[GOAL]
α : Type u_1
inst✝¹ : Group α
inst✝ : HasDistribNeg α
a : α
⊢ (-a)⁻¹ = -a⁻¹
[PROOFSTEP]
rw [eq_comm, eq_inv_iff_mul_eq_one, neg_mul, mul_neg, neg_neg, mul_left_inv]
[GOAL]
α : Type u_1
inst✝ : NonUnitalCommRing α
a b✝ c✝ b c x : α
h : x * x - b * x + c = 0
⊢ ∃ y, y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c
[PROOFSTEP]
have : c = x * (b - x) := (eq_neg_of_add_eq_zero_right h).trans (by simp [mul_sub, mul_comm])
[GOAL]
α : Type u_1
inst✝ : NonUnitalCommRing α
a b✝ c✝ b c x : α
h : x * x - b * x + c = 0
⊢ -(x * x - b * x) = x * (b - x)
[PROOFSTEP]
simp [mul_sub, mul_comm]
[GOAL]
α : Type u_1
inst✝ : NonUnitalCommRing α
a b✝ c✝ b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ ∃ y, y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c
[PROOFSTEP]
refine' ⟨b - x, _, by simp, by rw [this]⟩
[GOAL]
α : Type u_1
inst✝ : NonUnitalCommRing α
a b✝ c✝ b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ x + (b - x) = b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : NonUnitalCommRing α
a b✝ c✝ b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ x * (b - x) = c
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
inst✝ : NonUnitalCommRing α
a b✝ c✝ b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ (b - x) * (b - x) - b * (b - x) + c = 0
[PROOFSTEP]
rw [this, sub_add, ← sub_mul, sub_self]
[GOAL]
α : Type u_1
inst✝¹ : NonAssocRing α
inst✝ : Nontrivial α
a : α
h : a + 1 = a
⊢ a + 1 = a + 0
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
inst✝¹ : NonAssocRing α
inst✝ : Nontrivial α
a : α
h : a - 1 = a
⊢ a + -1 = a + -0
[PROOFSTEP]
simp [← sub_eq_add_neg, h]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsLeftCancelMulZero α
x y : α
h : x * y = 0
⊢ x = 0 ∨ y = 0
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsLeftCancelMulZero α
x y : α
h : x * y = 0
hx : x = 0
⊢ x = 0 ∨ y = 0
case neg α : Type u_1 inst✝¹ : Ring α inst✝ : IsLeftCancelMulZero α x y : α h : x * y = 0 hx : ¬x = 0 ⊢ x = 0 ∨ y = 0
[PROOFSTEP]
{ left
  exact hx
}
[GOAL]
case pos
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsLeftCancelMulZero α
x y : α
h : x * y = 0
hx : x = 0
⊢ x = 0 ∨ y = 0
[PROOFSTEP]
left
[GOAL]
case pos.h
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsLeftCancelMulZero α
x y : α
h : x * y = 0
hx : x = 0
⊢ x = 0
[PROOFSTEP]
exact hx
[GOAL]
case neg
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsLeftCancelMulZero α
x y : α
h : x * y = 0
hx : ¬x = 0
⊢ x = 0 ∨ y = 0
[PROOFSTEP]
{ right
  rw [← sub_zero (x * y), ← mul_zero x, ← mul_sub] at h 
  have := (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero) hx h
  rwa [sub_zero] at this 
}
[GOAL]
case neg
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsLeftCancelMulZero α
x y : α
h : x * y = 0
hx : ¬x = 0
⊢ x = 0 ∨ y = 0
[PROOFSTEP]
right
[GOAL]
case neg.h
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsLeftCancelMulZero α
x y : α
h : x * y = 0
hx : ¬x = 0
⊢ y = 0
[PROOFSTEP]
rw [← sub_zero (x * y), ← mul_zero x, ← mul_sub] at h 
[GOAL]
case neg.h
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsLeftCancelMulZero α
x y : α
h : x * (y - 0) = x * 0
hx : ¬x = 0
⊢ y = 0
[PROOFSTEP]
have := (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero) hx h
[GOAL]
case neg.h
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsLeftCancelMulZero α
x y : α
h : x * (y - 0) = x * 0
hx : ¬x = 0
this : y - 0 = 0
⊢ y = 0
[PROOFSTEP]
rwa [sub_zero] at this 
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsRightCancelMulZero α
x y : α
h : x * y = 0
⊢ x = 0 ∨ y = 0
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsRightCancelMulZero α
x y : α
h : x * y = 0
hy : y = 0
⊢ x = 0 ∨ y = 0
case neg α : Type u_1 inst✝¹ : Ring α inst✝ : IsRightCancelMulZero α x y : α h : x * y = 0 hy : ¬y = 0 ⊢ x = 0 ∨ y = 0
[PROOFSTEP]
{ right
  exact hy
}
[GOAL]
case pos
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsRightCancelMulZero α
x y : α
h : x * y = 0
hy : y = 0
⊢ x = 0 ∨ y = 0
[PROOFSTEP]
right
[GOAL]
case pos.h
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsRightCancelMulZero α
x y : α
h : x * y = 0
hy : y = 0
⊢ y = 0
[PROOFSTEP]
exact hy
[GOAL]
case neg
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsRightCancelMulZero α
x y : α
h : x * y = 0
hy : ¬y = 0
⊢ x = 0 ∨ y = 0
[PROOFSTEP]
{ left
  rw [← sub_zero (x * y), ← zero_mul y, ← sub_mul] at h 
  have := (IsRightCancelMulZero.mul_right_cancel_of_ne_zero) hy h
  rwa [sub_zero] at this 
}
[GOAL]
case neg
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsRightCancelMulZero α
x y : α
h : x * y = 0
hy : ¬y = 0
⊢ x = 0 ∨ y = 0
[PROOFSTEP]
left
[GOAL]
case neg.h
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsRightCancelMulZero α
x y : α
h : x * y = 0
hy : ¬y = 0
⊢ x = 0
[PROOFSTEP]
rw [← sub_zero (x * y), ← zero_mul y, ← sub_mul] at h 
[GOAL]
case neg.h
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsRightCancelMulZero α
x y : α
h : (x - 0) * y = 0 * y
hy : ¬y = 0
⊢ x = 0
[PROOFSTEP]
have := (IsRightCancelMulZero.mul_right_cancel_of_ne_zero) hy h
[GOAL]
case neg.h
α : Type u_1
inst✝¹ : Ring α
inst✝ : IsRightCancelMulZero α
x y : α
h : (x - 0) * y = 0 * y
hy : ¬y = 0
this : x - 0 = 0
⊢ x = 0
[PROOFSTEP]
rwa [sub_zero] at this 
[GOAL]
α : Type ?u.21715
inst✝¹ : Ring α
inst✝ : NoZeroDivisors α
a✝ b✝ c✝ : α
ha : a✝ ≠ 0
h : a✝ * b✝ = a✝ * c✝
⊢ b✝ = c✝
[PROOFSTEP]
rw [← sub_eq_zero, ← mul_sub] at h 
[GOAL]
α : Type ?u.21715
inst✝¹ : Ring α
inst✝ : NoZeroDivisors α
a✝ b✝ c✝ : α
ha : a✝ ≠ 0
h✝ : a✝ * b✝ = a✝ * c✝
h : a✝ * (b✝ - c✝) = 0
⊢ b✝ = c✝
[PROOFSTEP]
exact sub_eq_zero.1 ((eq_zero_or_eq_zero_of_mul_eq_zero h).resolve_left ha)
[GOAL]
α : Type ?u.21715
inst✝¹ : Ring α
inst✝ : NoZeroDivisors α
a✝ b✝ c✝ : α
hb : b✝ ≠ 0
h : a✝ * b✝ = c✝ * b✝
⊢ a✝ = c✝
[PROOFSTEP]
rw [← sub_eq_zero, ← sub_mul] at h 
[GOAL]
α : Type ?u.21715
inst✝¹ : Ring α
inst✝ : NoZeroDivisors α
a✝ b✝ c✝ : α
hb : b✝ ≠ 0
h✝ : a✝ * b✝ = c✝ * b✝
h : (a✝ - c✝) * b✝ = 0
⊢ a✝ = c✝
[PROOFSTEP]
exact sub_eq_zero.1 ((eq_zero_or_eq_zero_of_mul_eq_zero h).resolve_right hb)
