α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : 0 < multiplicity a b
⊢ a ^ 1 ∣ b
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : 0 < multiplicity a b
⊢ a ∣ b
rw [← pow_one a]
case a
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : 0 < multiplicity a b
⊢ ↑1 ≤ multiplicity a b
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : 0 < multiplicity a b
⊢ a ^ 1 ∣ b
apply pow_dvd_of_le_multiplicity
no goals
case a
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : 0 < multiplicity a b
⊢ ↑1 ≤ multiplicity a b
simpa only [Nat.cast_one, PartENat.pos_iff_one_le] using h