α : Type u_1
inst✝² : Nontrivial α
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : NoZeroDivisors α
h : IsRegular 0
⊢ False
α : Type u_1
inst✝² : Nontrivial α
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : NoZeroDivisors α
k : α
h : IsRegular k
⊢ k ≠ 0
rintro rfl
no goals
α : Type u_1
inst✝² : Nontrivial α
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : NoZeroDivisors α
h : IsRegular 0
⊢ False
exact not_not.mpr h.left not_isLeftRegular_zero