α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
n : ℕ
⊢ multiplicity a b = ↑n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
n : ℕ
⊢ multiplicity a b = ↑n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b
rw [← PartENat.some_eq_natCast]
no goals
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
n : ℕ
⊢ multiplicity a b = ↑n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b
exact
  ⟨fun h =>
    let ⟨h₁, h₂⟩ := eq_some_iff.1 h
    h₂ ▸ ⟨pow_multiplicity_dvd _, is_greatest (by
            rw [PartENat.lt_coe_iff]
            exact ⟨h₁, lt_succ_self _⟩)⟩,
    fun h => eq_some_iff.2 ⟨⟨n, h.2⟩, Eq.symm <| unique' h.1 h.2⟩⟩
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
n : ℕ
h : multiplicity a b = ↑n
h₁ : (multiplicity a b).Dom
h₂ : Part.get (multiplicity a b) h₁ = n
⊢ ∃ h, Part.get (multiplicity a b) h < Part.get (multiplicity a b) h₁ + 1
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
n : ℕ
h : multiplicity a b = ↑n
h₁ : (multiplicity a b).Dom
h₂ : Part.get (multiplicity a b) h₁ = n
⊢ multiplicity a b < ↑(Part.get (multiplicity a b) h₁ + 1)
rw [PartENat.lt_coe_iff]
no goals
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
n : ℕ
h : multiplicity a b = ↑n
h₁ : (multiplicity a b).Dom
h₂ : Part.get (multiplicity a b) h₁ = n
⊢ ∃ h, Part.get (multiplicity a b) h < Part.get (multiplicity a b) h₁ + 1
exact ⟨h₁, lt_succ_self _⟩