case x
α : Type ?u.183606
inst✝ : Monoid α
a b : ℕ
⊢ (multiplicity ↑a ↑b).Dom ↔ (multiplicity a b).Dom

case x
α : Type ?u.183606
inst✝ : Monoid α
a b : ℕ
⊢ ∀ (h₁ : (multiplicity ↑a ↑b).Dom) (h₂ : (multiplicity a b).Dom),
    Part.get (multiplicity ↑a ↑b) h₁ = Part.get (multiplicity a b) h₂
α : Type ?u.183606
inst✝ : Monoid α
a b : ℕ
⊢ multiplicity ↑a ↑b = multiplicity a b
apply Part.ext'
case x
α : Type ?u.183606
inst✝ : Monoid α
a b : ℕ
⊢ (∃ n, ¬↑a ^ (n + 1) ∣ ↑b) ↔ ∃ n, ¬a ^ (n + 1) ∣ b
case x
α : Type ?u.183606
inst✝ : Monoid α
a b : ℕ
⊢ (multiplicity ↑a ↑b).Dom ↔ (multiplicity a b).Dom
rw [← @finite_iff_dom ℕ, @finite_def ℕ, ← @finite_iff_dom ℤ, @finite_def ℤ]
no goals
case x
α : Type ?u.183606
inst✝ : Monoid α
a b : ℕ
⊢ (∃ n, ¬↑a ^ (n + 1) ∣ ↑b) ↔ ∃ n, ¬a ^ (n + 1) ∣ b
norm_cast
case x
α : Type ?u.183606
inst✝ : Monoid α
a b : ℕ
h1 : (multiplicity ↑a ↑b).Dom
h2 : (multiplicity a b).Dom
⊢ Part.get (multiplicity ↑a ↑b) h1 = Part.get (multiplicity a b) h2
case x
α : Type ?u.183606
inst✝ : Monoid α
a b : ℕ
⊢ ∀ (h₁ : (multiplicity ↑a ↑b).Dom) (h₂ : (multiplicity a b).Dom),
    Part.get (multiplicity ↑a ↑b) h₁ = Part.get (multiplicity a b) h₂
intro h1 h2
case x.a.h
α : Type ?u.183606
inst✝ : Monoid α
a b : ℕ
h1 : (multiplicity ↑a ↑b).Dom
h2 : (multiplicity a b).Dom
⊢ ∀ (n : ℕ), (fun n => ¬↑a ^ (n + 1) ∣ ↑b) n → (fun n => ¬a ^ (n + 1) ∣ b) n
case x.a
α : Type ?u.183606
inst✝ : Monoid α
a b : ℕ
h1 : (multiplicity ↑a ↑b).Dom
h2 : (multiplicity a b).Dom
⊢ Part.get (multiplicity a b) h2 ≤ Part.get (multiplicity ↑a ↑b) h1
apply Nat.find_mono
case x.a.h
α : Type ?u.183606
inst✝ : Monoid α
a b : ℕ
h1 : (multiplicity ↑a ↑b).Dom
h2 : (multiplicity a b).Dom
⊢ ∀ (n : ℕ), (fun n => ¬a ^ (n + 1) ∣ b) n → (fun n => ¬a ^ (n + 1) ∣ b) n
case x.a.h
α : Type ?u.183606
inst✝ : Monoid α
a b : ℕ
h1 : (multiplicity ↑a ↑b).Dom
h2 : (multiplicity a b).Dom
⊢ ∀ (n : ℕ), (fun n => ¬↑a ^ (n + 1) ∣ ↑b) n → (fun n => ¬a ^ (n + 1) ∣ b) n
norm_cast
no goals
case x.a.h
α : Type ?u.183606
inst✝ : Monoid α
a b : ℕ
h1 : (multiplicity ↑a ↑b).Dom
h2 : (multiplicity a b).Dom
⊢ ∀ (n : ℕ), (fun n => ¬a ^ (n + 1) ∣ b) n → (fun n => ¬a ^ (n + 1) ∣ b) n
simp