case intro
α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
⊢ ↑u ∣ a
α : Type u_1
inst✝ : Monoid α
a b u : α
hu : IsUnit u
⊢ u ∣ a
rcases hu with ⟨u, rfl⟩
no goals
case intro
α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
⊢ ↑u ∣ a
apply Units.coe_dvd