α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b c d : α
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
hab : Finite a b
⊢ ↑(Part.get (multiplicity a b) (_ : (multiplicity a b).Dom)) ≤ multiplicity c d
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b c d : α
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
hab : Finite a b
⊢ multiplicity a b ≤ multiplicity c d
rw [← PartENat.natCast_get (finite_iff_dom.1 hab)]
no goals
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b c d : α
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
hab : Finite a b
⊢ ↑(Part.get (multiplicity a b) (_ : (multiplicity a b).Dom)) ≤ multiplicity c d
exact le_multiplicity_of_pow_dvd (h _ (pow_multiplicity_dvd _))
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b c d : α
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
hab : ¬Finite a b
this : ∀ (n : ℕ), c ^ n ∣ d
⊢ multiplicity a b ≤ multiplicity c d
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b c d : α
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
hab : ¬Finite a b
⊢ multiplicity a b ≤ multiplicity c d
have : ∀ n : ℕ, c ^ n ∣ d := fun n => h n (not_finite_iff_forall.1 hab _)
no goals
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b c d : α
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
hab : ¬Finite a b
this : ∀ (n : ℕ), c ^ n ∣ d
⊢ multiplicity a b ≤ multiplicity c d
rw [eq_top_iff_not_finite.2 hab, eq_top_iff_not_finite.2 (not_finite_iff_forall.2 this)]