R : Type u_1
inst✝¹ : MulZeroClass R
b : R
inst✝ : Nontrivial R
ra : IsRightRegular 0
⊢ False
R : Type u_1
inst✝¹ : MulZeroClass R
a b : R
inst✝ : Nontrivial R
ra : IsRightRegular a
⊢ a ≠ 0
rintro rfl
case intro.intro
R : Type u_1
inst✝¹ : MulZeroClass R
b : R
inst✝ : Nontrivial R
ra : IsRightRegular 0
x y : R
xy : x ≠ y
⊢ False
R : Type u_1
inst✝¹ : MulZeroClass R
b : R
inst✝ : Nontrivial R
ra : IsRightRegular 0
⊢ False
rcases exists_pair_ne R with ⟨x, y, xy⟩
case intro.intro
R : Type u_1
inst✝¹ : MulZeroClass R
b : R
inst✝ : Nontrivial R
ra : IsRightRegular 0
x y : R
xy : x ≠ y
⊢ x * 0 = y * 0
case intro.intro
R : Type u_1
inst✝¹ : MulZeroClass R
b : R
inst✝ : Nontrivial R
ra : IsRightRegular 0
x y : R
xy : x ≠ y
⊢ False
refine' xy (ra (_ : x * 0 = y * 0))
no goals
case intro.intro
R : Type u_1
inst✝¹ : MulZeroClass R
b : R
inst✝ : Nontrivial R
ra : IsRightRegular 0
x y : R
xy : x ≠ y
⊢ x * 0 = y * 0
rw [mul_zero, mul_zero]