α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
k : ℕ
⊢ ↑k ≤ multiplicity a b → a ^ k ∣ b
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
k : ℕ
⊢ ↑k ≤ multiplicity a b → a ^ k ∣ b
rw [← PartENat.some_eq_natCast]
no goals
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
k : ℕ
⊢ ↑k ≤ multiplicity a b → a ^ k ∣ b
exact
  Nat.casesOn k
    (fun _ => by
      rw [_root_.pow_zero]
      exact one_dvd _)
    fun k ⟨_, h₂⟩ => by_contradiction fun hk => Nat.find_min _ (lt_of_succ_le (h₂ ⟨k, hk⟩)) hk
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
k : ℕ
x✝ : ↑zero ≤ multiplicity a b
⊢ 1 ∣ b
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
k : ℕ
x✝ : ↑zero ≤ multiplicity a b
⊢ a ^ zero ∣ b
rw [_root_.pow_zero]
no goals
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
k : ℕ
x✝ : ↑zero ≤ multiplicity a b
⊢ 1 ∣ b
exact one_dvd _