[GOAL]
α : Type u_1
inst✝ : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), k * x = 0 → x = 0
⊢ IsLeftRegular k
[PROOFSTEP]
refine' fun x y (h' : k * x = k * y) => sub_eq_zero.mp (h _ _)
[GOAL]
α : Type u_1
inst✝ : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), k * x = 0 → x = 0
x y : α
h' : k * x = k * y
⊢ k * (x - y) = 0
[PROOFSTEP]
rw [mul_sub, sub_eq_zero, h']
[GOAL]
α : Type u_1
inst✝ : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), x * k = 0 → x = 0
⊢ IsRightRegular k
[PROOFSTEP]
refine' fun x y (h' : x * k = y * k) => sub_eq_zero.mp (h _ _)
[GOAL]
α : Type u_1
inst✝ : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), x * k = 0 → x = 0
x y : α
h' : x * k = y * k
⊢ (x - y) * k = 0
[PROOFSTEP]
rw [sub_mul, sub_eq_zero, h']
[GOAL]
α : Type u_1
inst✝² : Nontrivial α
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : NoZeroDivisors α
k : α
h : IsRegular k
⊢ k ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝² : Nontrivial α
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : NoZeroDivisors α
h : IsRegular 0
⊢ False
[PROOFSTEP]
exact not_not.mpr h.left not_isLeftRegular_zero
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : NoZeroDivisors α
⊢ MonoidWithZero α
[PROOFSTEP]
infer_instance
