rcases show r = 0 ∨ r = 1 from le_one_iff_eq_zero_or_one.mp hr with (rfl | rfl)
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
r : M
hr : r ≤ 1
hhr : 1 < r
hd : r ∣ 1
⊢ 2 ∣ r
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
hr : 0 ≤ 1
hhr : 1 < 0
hd : 0 ∣ 1
⊢ 2 ∣ 0

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈open
hr : 1 ≤ 1
hhr : 1 < 1
hd : 1 ∣ 1
⊢ 2 ∣ 1