awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hdiv : a ∣ b
h : multiplicity a b = 0
⊢ False

Tactic:
simpa [hdiv] using FiniteMultiplicity.not_pow_dvd_of_multiplicity_lt
    (by by_contra! nh; simp [nh] at h) (lt_one_iff.mpr h)

Premises used: Iff.mpr, Nat.lt_one_iff, FiniteMultiplicity.not_pow_dvd_of_multiplicity_lt
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hdiv : a ∣ b
⊢ 0 < emultiplicity a b

Tactic:
lt_emultiplicity_of_lt_multiplicity (multiplicity_pos_of_dvd hdiv)

Premises used: lt_emultiplicity_of_lt_multiplicity, WithTop.some, multiplicity_pos_of_dvd
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
k : ℕ
hk : a ^ k ∣ b
hsucc : ¬a ^ (k + 1) ∣ b
⊢ FiniteMultiplicity a b

Tactic:
have : FiniteMultiplicity a b := ⟨k, hsucc⟩
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
k : ℕ
hk : a ^ k ∣ b
hsucc : ¬a ^ (k + 1) ∣ b
this : FiniteMultiplicity a b
simp : ∀ n < k, a ^ (n + 1) ∣ b
⊢ emultiplicity a b = (↑k : ℕ∞)

Tactic:
simp only [emultiplicity, this, ↓reduceDIte, Nat.cast_inj, find_eq_iff, hsucc, not_false_eq_true,
    Decidable.not_not, true_and]

Premises used: reduceDIte, Nat.cast_inj, Decidable.not_not, not_false_eq_true, Nat.find_eq_iff, true_and, emultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
k : ℕ
hk : a ^ k ∣ b
hsucc : ¬a ^ (k + 1) ∣ b
this : FiniteMultiplicity a b
⊢ ∀ n < k, a ^ (n + 1) ∣ b

Tactic:
fun n hn ↦ (pow_dvd_pow _ hn).trans hk

Premises used: pow_dvd_pow, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
k : ℕ
hk : a ^ k ∣ b
hsucc : ¬a ^ (k + 1) ∣ b
this : FiniteMultiplicity a b
⊢ ∀ n < k, a ^ (n + 1) ∣ b

Tactic:
exact fun n hn ↦ (pow_dvd_pow _ hn).trans hk

Premises used: pow_dvd_pow, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
k : ℕ
hk : a ^ k ∣ b
hsucc : ¬a ^ (k + 1) ∣ b
have have₁ have₂ : ∀ (this : FiniteMultiplicity a b), emultiplicity a b = (↑k : ℕ∞)
have₃ : ∀ (this : FiniteMultiplicity a b), ∀ n < k, a ^ (n + 1) ∣ b
⊢ emultiplicity a b = (↑k : ℕ∞)

Tactic:
classical
  have : FiniteMultiplicity a b := ⟨k, hsucc⟩
  simp only [emultiplicity, this, ↓reduceDIte, Nat.cast_inj, find_eq_iff, hsucc, not_false_eq_true,
    Decidable.not_not, true_and]
  exact fun n hn ↦ (pow_dvd_pow _ hn).trans hk

Premises used: pow_dvd_pow, reduceDIte, Nat.cast_inj, Decidable.not_not, not_false_eq_true, Nat.find_eq_iff, true_and, emultiplicity, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
k : ℕ
hk : a ^ k ∣ b
hsucc : ¬a ^ (k + 1) ∣ b
⊢ multiplicity a b = k

Tactic:
multiplicity_eq_of_emultiplicity_eq_some (emultiplicity_eq_of_dvd_of_not_dvd hk hsucc)

Premises used: emultiplicity_eq_of_dvd_of_not_dvd, multiplicity_eq_of_emultiplicity_eq_some
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
k : ℕ
hk : a ^ k ∣ b
⊢ (↑k : ℕ∞) ≤ emultiplicity a b

Tactic:
le_of_not_gt fun hk' => not_pow_dvd_of_emultiplicity_lt hk' hk

Premises used: le_of_not_gt, not_pow_dvd_of_emultiplicity_lt
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hf : FiniteMultiplicity a b
k : ℕ
hk : a ^ k ∣ b
⊢ k ≤ multiplicity a b

Tactic:
hf.le_multiplicity_of_le_emultiplicity (le_emultiplicity_of_pow_dvd hk)

Premises used: FiniteMultiplicity.le_multiplicity_of_le_emultiplicity, le_emultiplicity_of_pow_dvd
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
k : ℕ
⊢ a ^ k ∣ b ↔ (↑k : ℕ∞) ≤ emultiplicity a b

Tactic:
⟨le_emultiplicity_of_pow_dvd, pow_dvd_of_le_emultiplicity⟩

Premises used: le_emultiplicity_of_pow_dvd, pow_dvd_of_le_emultiplicity, Iff.intro
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hf : FiniteMultiplicity a b
k : ℕ
⊢ a ^ k ∣ b ↔ k ≤ multiplicity a b

Tactic:
exact_mod_cast hf.emultiplicity_eq_multiplicity ▸ pow_dvd_iff_le_emultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
k : ℕ
rw : emultiplicity a b < (↑k : ℕ∞) ↔ ¬(↑k : ℕ∞) ≤ emultiplicity a b
rw₁ rw₂ : emultiplicity a b < (↑k : ℕ∞) ↔ emultiplicity a b < (↑k : ℕ∞)
⊢ emultiplicity a b < (↑k : ℕ∞) ↔ ¬a ^ k ∣ b

Tactic:
rw [pow_dvd_iff_le_emultiplicity, not_le]

Premises used: not_le, pow_dvd_iff_le_emultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
k : ℕ
hf : FiniteMultiplicity a b
rw : multiplicity a b < k ↔ ¬k ≤ multiplicity a b
rw₁ rw₂ : multiplicity a b < k ↔ multiplicity a b < k
⊢ multiplicity a b < k ↔ ¬a ^ k ∣ b

Tactic:
rw [hf.pow_dvd_iff_le_multiplicity, not_le]

Premises used: not_le, FiniteMultiplicity.pow_dvd_iff_le_multiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
mp : emultiplicity a b = (↑n : ℕ∞) → a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b
mpr : a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b → emultiplicity a b = (↑n : ℕ∞)
⊢ emultiplicity a b = (↑n : ℕ∞) ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

Tactic:
constructor
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = (↑n : ℕ∞)
mp : a ^ n ∣ b
mp₁ : ¬a ^ (n + 1) ∣ b
⊢ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

Tactic:
constructor
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = (↑n : ℕ∞)
mp : (↑n : ℕ∞) ≤ emultiplicity a b
⊢ a ^ n ∣ b

Tactic:
apply pow_dvd_of_le_emultiplicity

Premises used: pow_dvd_of_le_emultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = (↑n : ℕ∞)
⊢ (↑n : ℕ∞) ≤ emultiplicity a b

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = (↑n : ℕ∞)
mp : emultiplicity a b < (↑(n + 1) : ℕ∞)
⊢ ¬a ^ (n + 1) ∣ b

Tactic:
apply not_pow_dvd_of_emultiplicity_lt

Premises used: not_pow_dvd_of_emultiplicity_lt
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = (↑n : ℕ∞)
mp : LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑(n + 1) : ℕ∞)
⊢ emultiplicity a b < (↑(n + 1) : ℕ∞)

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = (↑n : ℕ∞)
mp : n < n + 1
⊢ LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑(n + 1) : ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = (↑n : ℕ∞)
⊢ n < n + 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
mpr : a ^ n ∣ b → ¬a ^ (n + 1) ∣ b → emultiplicity a b = (↑n : ℕ∞)
⊢ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b → emultiplicity a b = (↑n : ℕ∞)

Tactic:
rw [and_imp]

Premises used: and_imp
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
⊢ a ^ n ∣ b → ¬a ^ (n + 1) ∣ b → emultiplicity a b = (↑n : ℕ∞)

Tactic:
apply emultiplicity_eq_of_dvd_of_not_dvd

Premises used: emultiplicity_eq_of_dvd_of_not_dvd
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hf : FiniteMultiplicity a b
n : ℕ
⊢ multiplicity a b = n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

Tactic:
simp [← emultiplicity_eq_coe, hf.emultiplicity_eq_multiplicity]

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, emultiplicity_eq_coe
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a b n : ℕ
inst : n.AtLeastTwo
⊢ emultiplicity a b = OfNat.ofNat n ↔
    HPow.hPow (β := ℕ) a (OfNat.ofNat n) ∣ b ∧ ¬a ^ HAdd.hAdd (α := ℕ) (OfNat.ofNat n) 1 ∣ b

Tactic:
emultiplicity_eq_coe

Premises used: emultiplicity_eq_coe
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
ha : IsUnit a
⊢ ¬FiniteMultiplicity a b

Tactic:
(·.not_unit ha)

Premises used: FiniteMultiplicity.not_unit, Not
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
b : α
⊢ ¬FiniteMultiplicity 1 b

Tactic:
simp
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
b : α
⊢ emultiplicity 1 b = ⊤

Tactic:
emultiplicity_eq_top.2 (FiniteMultiplicity.not_of_one_left _)

Premises used: Iff.mpr, FiniteMultiplicity.not_of_one_left, emultiplicity_eq_top
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a : α
ha : FiniteMultiplicity a 1
⊢ multiplicity a 1 = 0

Tactic:
simp [ha.multiplicity_eq_iff, ha.not_dvd_of_one_right]

Premises used: FiniteMultiplicity.multiplicity_eq_iff, FiniteMultiplicity.not_dvd_of_one_right
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a : α
u : αˣ
⊢ ¬FiniteMultiplicity (↑u : α) a

Tactic:
FiniteMultiplicity.not_of_isUnit_left a u.isUnit

Premises used: FiniteMultiplicity.not_of_isUnit_left, Units.isUnit
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
pos : ∀ (hf : FiniteMultiplicity a b), emultiplicity a b = 0 ↔ ¬a ∣ b
neg : ∀ (hf : ¬FiniteMultiplicity a b), emultiplicity a b = 0 ↔ ¬a ∣ b
⊢ emultiplicity a b = 0 ↔ ¬a ∣ b

Tactic:
by_cases hf : FiniteMultiplicity a b

Premises used: FiniteMultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hf : FiniteMultiplicity a b
pos : HPow.hPow (β := ℕ) a 0 ∣ b ∧ ¬a ^ HAdd.hAdd (α := ℕ) 0 1 ∣ b ↔ ¬a ∣ b
⊢ emultiplicity a b = 0 ↔ ¬a ∣ b

Tactic:
rw [← ENat.coe_zero, emultiplicity_eq_coe]

Premises used: emultiplicity_eq_coe, ENat.coe_zero
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hf : FiniteMultiplicity a b
⊢ HPow.hPow (β := ℕ) a 0 ∣ b ∧ ¬a ^ HAdd.hAdd (α := ℕ) 0 1 ∣ b ↔ ¬a ∣ b

Tactic:
simp
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hf : ¬FiniteMultiplicity a b
⊢ emultiplicity a b = 0 ↔ ¬a ∣ b

Tactic:
simpa [emultiplicity_eq_top.2 hf] using FiniteMultiplicity.not_iff_forall.1 hf 1

Premises used: Iff.mpr, emultiplicity_eq_top, FiniteMultiplicity.not_iff_forall, Iff.mp, OfNat.ofNat
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
R : Type u_3
inst : CommMonoidWithZero R
inst_1 : Subsingleton.{u_3 + 1} Rˣ
a b : R
ha : Irreducible a
hb : Irreducible b
h : a ≠ b
h_1 : Associated a b
u : Rˣ
h_2 : a * (↑u : R) = b
⊢ False

Tactic:
simp_all [Subsingleton.elim u 1]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
⊢ multiplicity a b = 0 ↔ ¬a ∣ b

Tactic:
(emultiplicity_eq_iff_multiplicity_eq_of_ne_one zero_ne_one).symm.trans emultiplicity_eq_zero

Premises used: zero_ne_one, emultiplicity_eq_zero, Iff.trans, emultiplicity_eq_iff_multiplicity_eq_of_ne_one, Iff.symm
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
⊢ emultiplicity a b ≠ 0 ↔ a ∣ b

Tactic:
simp [emultiplicity_eq_zero]

Premises used: emultiplicity_eq_zero
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
⊢ multiplicity a b ≠ 0 ↔ a ∣ b

Tactic:
simp [multiplicity_eq_zero]

Premises used: multiplicity_eq_zero
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hfin : FiniteMultiplicity a b
obtain : ∀ (c : α) (hc : b = a ^ multiplicity a b * c), ∃ (c : α), b = a ^ multiplicity a b * c ∧ ¬a ∣ c
⊢ ∃ (c : α), b = a ^ multiplicity a b * c ∧ ¬a ∣ c

Tactic:
obtain ⟨c, hc⟩ := pow_multiplicity_dvd a b

Premises used: pow_multiplicity_dvd
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c : α
hc : b = a ^ multiplicity a b * c
⊢ ∃ (c : α), b = a ^ multiplicity a b * c ∧ ¬a ∣ c

Tactic:
⟨c, hc, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c : α
hc : b = a ^ multiplicity a b * c
refine : ¬a ∣ c
⊢ ∃ (c : α), b = a ^ multiplicity a b * c ∧ ¬a ∣ c

Tactic:
refine ⟨c, hc, ?_⟩
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c : α
hc : b = a ^ multiplicity a b * c
k : α
hk : c = a * k
⊢ b = a ^ (multiplicity a b + 1) * k

Tactic:
rw [hk, ← mul_assoc, ← _root_.pow_succ] at hc

Premises used: pow_succ, mul_assoc
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c : α
hc : b = a ^ multiplicity a b * c
k : α
hk : c = a * k
hc₁ : b = a ^ (multiplicity a b + 1) * k
⊢ c = a * k

Tactic:
rw [hk, ← mul_assoc, ← _root_.pow_succ] at hc

Premises used: pow_succ, mul_assoc
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c k : α
hc : b = a ^ (multiplicity a b + 1) * k
hk : c = a * k
⊢ a ^ (multiplicity a b + 1) ∣ b

Tactic:
have h₁ : a ^ (multiplicity a b + 1) ∣ b := ⟨k, hc⟩
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c k : α
hc : b = a ^ (multiplicity a b + 1) * k
hk : c = a * k
h₁ : a ^ (multiplicity a b + 1) ∣ b
⊢ multiplicity a b = multiplicity a b

Tactic:
simp
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c k : α
hc : b = a ^ (multiplicity a b + 1) * k
hk : c = a * k
h₁ : a ^ (multiplicity a b + 1) ∣ b
⊢ False

Tactic:
exact (hfin.multiplicity_eq_iff.1 (by simp)).2 h₁

Premises used: And.right, FiniteMultiplicity.multiplicity_eq_iff, Iff.mp
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
a b : α
c d : β
mp : emultiplicity a b ≤ emultiplicity c d → ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
mpr : (∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d) → emultiplicity a b ≤ emultiplicity c d
⊢ emultiplicity a b ≤ emultiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

Tactic:
constructor
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
a b : α
c d : β
⊢ emultiplicity a b ≤ emultiplicity c d → ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

Tactic:
fun h n hab ↦ pow_dvd_of_le_emultiplicity (le_trans (le_emultiplicity_of_pow_dvd hab) h)

Premises used: le_emultiplicity_of_pow_dvd, pow_dvd_of_le_emultiplicity, le_trans
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
a b : α
c d : β
⊢ emultiplicity a b ≤ emultiplicity c d → ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

Tactic:
exact fun h n hab ↦ pow_dvd_of_le_emultiplicity (le_trans (le_emultiplicity_of_pow_dvd hab) h)

Premises used: le_emultiplicity_of_pow_dvd, pow_dvd_of_le_emultiplicity, le_trans
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
mpr :
  ∀ (h : FiniteMultiplicity a b),
    LE.le (α := ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ ¬a ^ (n + 1) ∣ b) h) : ℕ∞)
      (if h : FiniteMultiplicity c d then (↑(Nat.find (p := fun (n : ℕ) ↦ ¬c ^ (n + 1) ∣ d) h) : ℕ∞) else ⊤)
mpr₁ :
  ¬FiniteMultiplicity a b →
    LE.le (α := ℕ∞) ⊤
      (if h : FiniteMultiplicity c d then (↑(Nat.find (p := fun (n : ℕ) ↦ ¬c ^ (n + 1) ∣ d) h) : ℕ∞) else ⊤)
⊢ LE.le (α := ℕ∞) (if h : FiniteMultiplicity a b then (↑(Nat.find (p := fun (n : ℕ) ↦ ¬a ^ (n + 1) ∣ b) h) : ℕ∞) else ⊤)
    (if h : FiniteMultiplicity c d then (↑(Nat.find (p := fun (n : ℕ) ↦ ¬c ^ (n + 1) ∣ d) h) : ℕ∞) else ⊤)

Tactic:
split
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
h_1 : FiniteMultiplicity a b
obtain :
  ∀ (w : ℕ) (h_1 : ¬a ^ (w + 1) ∣ b),
    LE.le (α := ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ ¬a ^ (n + 1) ∣ b) ⋯) : ℕ∞)
      (if h : FiniteMultiplicity c d then (↑(Nat.find (p := fun (n : ℕ) ↦ ¬c ^ (n + 1) ∣ d) h) : ℕ∞) else ⊤)
⊢ LE.le (α := ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ ¬a ^ (n + 1) ∣ b) h_1) : ℕ∞)
    (if h : FiniteMultiplicity c d then (↑(Nat.find (p := fun (n : ℕ) ↦ ¬c ^ (n + 1) ∣ d) h) : ℕ∞) else ⊤)

Tactic:
obtain ⟨w, h_1⟩ := h_1
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
w : ℕ
h_1 : ¬a ^ (w + 1) ∣ b
isTrue :
  ∀ (h : FiniteMultiplicity c d),
    LE.le (α := ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ ¬a ^ (n + 1) ∣ b) ⋯) : ℕ∞)
      (↑(Nat.find (p := fun (n : ℕ) ↦ ¬c ^ (n + 1) ∣ d) h) : ℕ∞)
isFalse : ¬FiniteMultiplicity c d → LE.le (α := ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ ¬a ^ (n + 1) ∣ b) ⋯) : ℕ∞) ⊤
⊢ LE.le (α := ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ ¬a ^ (n + 1) ∣ b) ⋯) : ℕ∞)
    (if h : FiniteMultiplicity c d then (↑(Nat.find (p := fun (n : ℕ) ↦ ¬c ^ (n + 1) ∣ d) h) : ℕ∞) else ⊤)

Tactic:
split
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
w : ℕ
h_1 : ¬a ^ (w + 1) ∣ b
h_2 : FiniteMultiplicity c d
⊢ LE.le (α := ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ ¬a ^ (n + 1) ∣ b) ⋯) : ℕ∞)
    (↑(Nat.find (p := fun (n : ℕ) ↦ ¬c ^ (n + 1) ∣ d) h_2) : ℕ∞)

Tactic:
simp_all only [cast_le, le_find_iff, lt_find_iff, Decidable.not_not, le_refl,
          not_true_eq_false, not_false_eq_true, implies_true]

Premises used: le_refl, not_true_eq_false, Nat.le_find_iff, Decidable.not_not, Nat.lt_find_iff, implies_true, Nat.cast_le, not_false_eq_true
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
w : ℕ
h_1 : ¬a ^ (w + 1) ∣ b
h_2 : FiniteMultiplicity c d
⊢ LE.le (α := ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ ¬a ^ (n + 1) ∣ b) ⋯) : ℕ∞)
    (↑(Nat.find (p := fun (n : ℕ) ↦ ¬c ^ (n + 1) ∣ d) h_2) : ℕ∞)

Tactic:
next h_2 =>
        simp_all only [cast_le, le_find_iff, lt_find_iff, Decidable.not_not, le_refl,
          not_true_eq_false, not_false_eq_true, implies_true]

Premises used: le_refl, not_true_eq_false, Nat.le_find_iff, Decidable.not_not, Nat.lt_find_iff, implies_true, Nat.cast_le, not_false_eq_true
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
w : ℕ
h_1 : ¬a ^ (w + 1) ∣ b
h_2 : ¬FiniteMultiplicity c d
⊢ LE.le (α := ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ ¬a ^ (n + 1) ∣ b) ⋯) : ℕ∞) ⊤

Tactic:
simp_all only [not_exists, Decidable.not_not, le_top]

Premises used: not_exists, le_top, Decidable.not_not
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
h_1 : FiniteMultiplicity a b
⊢ LE.le (α := ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ ¬a ^ (n + 1) ∣ b) h_1) : ℕ∞)
    (if h : FiniteMultiplicity c d then (↑(Nat.find (p := fun (n : ℕ) ↦ ¬c ^ (n + 1) ∣ d) h) : ℕ∞) else ⊤)

Tactic:
next h_1 =>
      obtain ⟨w, h_1⟩ := h_1
      split
      next h_2 =>
        simp_all only [cast_le, le_find_iff, lt_find_iff, Decidable.not_not, le_refl,
          not_true_eq_false, not_false_eq_true, implies_true]
      next h_2 => simp_all only [not_exists, Decidable.not_not, le_top]

Premises used: le_refl, not_exists, not_true_eq_false, Nat.le_find_iff, le_top, Decidable.not_not, Nat.lt_find_iff, implies_true, Nat.cast_le, not_false_eq_true
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
h_1 : ¬FiniteMultiplicity a b
⊢ LE.le (α := ℕ∞) ⊤
    (if h : FiniteMultiplicity c d then (↑(Nat.find (p := fun (n : ℕ) ↦ ¬c ^ (n + 1) ∣ d) h) : ℕ∞) else ⊤)

Tactic:
simp_all only [not_exists, Decidable.not_not, not_true_eq_false, top_le_iff,
        dite_eq_right_iff, ENat.coe_ne_top, imp_false, not_false_eq_true, implies_true]

Premises used: imp_false, not_exists, not_true_eq_false, dite_eq_right_iff, top_le_iff, ENat.coe_ne_top, Decidable.not_not, implies_true, not_false_eq_true
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
a b : α
c d : β
mp : emultiplicity a b ≤ emultiplicity c d → ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
mpr mpr₁ : (∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d) → emultiplicity a b ≤ emultiplicity c d
⊢ emultiplicity a b ≤ emultiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

Tactic:
classical
  constructor
  · exact fun h n hab ↦ pow_dvd_of_le_emultiplicity (le_trans (le_emultiplicity_of_pow_dvd hab) h)
  · intro h
    unfold emultiplicity
    -- aesop? says
    split
    next h_1 =>
      obtain ⟨w, h_1⟩ := h_1
      split
      next h_2 =>
        simp_all only [cast_le, le_find_iff, lt_find_iff, Decidable.not_not, le_refl,
          not_true_eq_false, not_false_eq_true, implies_true]
      next h_2 => simp_all only [not_exists, Decidable.not_not, le_top]
    next h_1 =>
      simp_all only [not_exists, Decidable.not_not, not_true_eq_false, top_le_iff,
        dite_eq_right_iff, ENat.coe_ne_top, imp_false, not_false_eq_true, implies_true]

Premises used: le_refl, imp_false, not_exists, not_true_eq_false, Nat.le_find_iff, dite_eq_right_iff, le_emultiplicity_of_pow_dvd, pow_dvd_of_le_emultiplicity, le_top, top_le_iff, ENat.coe_ne_top, Decidable.not_not, Nat.lt_find_iff, implies_true, Nat.cast_le, not_false_eq_true, emultiplicity, le_trans
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
a b : α
c d : β
hab : FiniteMultiplicity a b
hcd : FiniteMultiplicity c d
rw : emultiplicity a b ≤ emultiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
⊢ multiplicity a b ≤ multiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

Tactic:
rw [← WithTop.coe_le_coe, ENat.some_eq_coe, ← hab.emultiplicity_eq_multiplicity,
    ← hcd.emultiplicity_eq_multiplicity]

Premises used: ENat.some_eq_coe, FiniteMultiplicity.emultiplicity_eq_multiplicity, WithTop.coe_le_coe
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
a b : α
c d : β
hab : FiniteMultiplicity a b
hcd : FiniteMultiplicity c d
⊢ emultiplicity a b ≤ emultiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

Tactic:
apply emultiplicity_le_emultiplicity_iff

Premises used: emultiplicity_le_emultiplicity_iff
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
a b : α
c d : β
⊢ emultiplicity a b = emultiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b ↔ c ^ n ∣ d

Tactic:
⟨fun h n =>
    ⟨emultiplicity_le_emultiplicity_iff.1 h.le n, emultiplicity_le_emultiplicity_iff.1 h.ge n⟩,
    fun h => le_antisymm (emultiplicity_le_emultiplicity_iff.2 fun n => (h n).mp)
      (emultiplicity_le_emultiplicity_iff.2 fun n => (h n).mpr)⟩

Premises used: Iff.mpr, Eq.ge, emultiplicity_le_emultiplicity_iff, Eq.le, le_antisymm, Iff.intro, Iff.mp
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
F : Type u_3
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
f : F
a b : α
n : ℕ
rw : a ^ n ∣ b → Dvd.dvd.{u_2} (α := β) ((f : (a : α) → β) (a ^ n) : β) ((f : (a : α) → β) b : β)
⊢ a ^ n ∣ b → HPow.hPow (α := β) ((f : (a : α) → β) a : β) n ∣ (f : (a : α) → β) b

Tactic:
rw [← map_pow]

Premises used: map_pow
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
F : Type u_3
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
f : F
a b : α
n : ℕ
⊢ a ^ n ∣ b → Dvd.dvd.{u_2} (α := β) ((f : (a : α) → β) (a ^ n) : β) ((f : (a : α) → β) b : β)

Tactic:
map_dvd f

Premises used: map_dvd
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
F : Type u_3
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
f : F
a b : α
n : ℕ
⊢ a ^ n ∣ b → Dvd.dvd.{u_2} (α := β) ((f : (a : α) → β) (a ^ n) : β) ((f : (a : α) → β) b : β)

Tactic:
exact map_dvd f

Premises used: map_dvd