α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
hfin : Finite a b
hdiv : a ∣ b
h : Part.get (multiplicity a b) hfin = 0
⊢ False
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
hfin : Finite a b
hdiv : a ∣ b
⊢ 0 < Part.get (multiplicity a b) hfin
refine' zero_lt_iff.2 fun h => _
no goals
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
hfin : Finite a b
hdiv : a ∣ b
h : Part.get (multiplicity a b) hfin = 0
⊢ False
simpa [hdiv] using is_greatest' hfin (lt_one_iff.mpr h)