[GOAL]
α : Type u_1
inst✝ : Monoid α
a b : ℕ
⊢ multiplicity ↑a ↑b = multiplicity a b
[PROOFSTEP]
apply Part.ext'
[GOAL]
case x
α : Type u_1
inst✝ : Monoid α
a b : ℕ
⊢ (multiplicity ↑a ↑b).Dom ↔ (multiplicity a b).Dom
[PROOFSTEP]
rw [← @finite_iff_dom ℕ, @finite_def ℕ, ← @finite_iff_dom ℤ, @finite_def ℤ]
[GOAL]
case x
α : Type u_1
inst✝ : Monoid α
a b : ℕ
⊢ (∃ n, ¬↑a ^ (n + 1) ∣ ↑b) ↔ ∃ n, ¬a ^ (n + 1) ∣ b
[PROOFSTEP]
norm_cast
[GOAL]
case x
α : Type u_1
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₂
[PROOFSTEP]
intro h1 h2
[GOAL]
case x
α : Type u_1
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
[PROOFSTEP]
apply _root_.le_antisymm
[GOAL]
case x.a
α : Type u_1
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
[PROOFSTEP]
apply Nat.find_mono
[GOAL]
case x.a.h
α : Type u_1
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
[PROOFSTEP]
norm_cast
[GOAL]
case x.a.h
α : Type u_1
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
[PROOFSTEP]
simp
[GOAL]
case x.a
α : Type u_1
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
[PROOFSTEP]
apply Nat.find_mono
[GOAL]
case x.a.h
α : Type u_1
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
[PROOFSTEP]
norm_cast
[GOAL]
case x.a.h
α : Type u_1
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
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬Finite a b
n : ℕ
⊢ a ^ zero ∣ b
[PROOFSTEP]
rw [_root_.pow_zero]
[GOAL]
α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬Finite a b
n : ℕ
⊢ 1 ∣ b
[PROOFSTEP]
exact one_dvd _
[GOAL]
α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬Finite a b
n : ℕ
⊢ ∀ (n : ℕ), a ^ succ n ∣ b
[PROOFSTEP]
simpa [Finite, Classical.not_not] using h
[GOAL]
α : Type u_1
inst✝ : Monoid α
a b : α
⊢ (∀ (n : ℕ), a ^ n ∣ b) → ¬Finite a b
[PROOFSTEP]
simp [Finite, multiplicity, Classical.not_not]
[GOAL]
α : Type u_1
inst✝ : Monoid α
a b : α
⊢ (∀ (n : ℕ), a ^ n ∣ b) → ∀ (x : ℕ), a ^ (x + 1) ∣ b
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
k : ℕ
⊢ ↑k ≤ multiplicity a b → a ^ k ∣ b
[PROOFSTEP]
rw [← PartENat.some_eq_natCast]
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
k : ℕ
⊢ ↑k ≤ multiplicity a b → a ^ k ∣ b
[PROOFSTEP]
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
[GOAL]
α : 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
[PROOFSTEP]
rw [_root_.pow_zero]
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
k : ℕ
x✝ : ↑zero ≤ multiplicity a b
⊢ 1 ∣ b
[PROOFSTEP]
exact one_dvd _
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : Finite a b
⊢ ↑(Part.get (multiplicity a b) h) ≤ multiplicity a b
[PROOFSTEP]
rw [PartENat.natCast_get]
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
m : ℕ
hm : multiplicity a b < ↑m
h : a ^ m ∣ b
⊢ False
[PROOFSTEP]
rw [PartENat.lt_coe_iff] at hm 
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
m : ℕ
hm : ∃ h, Part.get (multiplicity a b) h < m
h : a ^ m ∣ b
⊢ False
[PROOFSTEP]
exact Nat.find_spec hm.fst ((pow_dvd_pow _ hm.snd).trans h)
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
m : ℕ
h : Finite a b
hm : Part.get (multiplicity a b) h < m
⊢ multiplicity a b < ↑m
[PROOFSTEP]
rwa [← PartENat.coe_lt_coe, PartENat.natCast_get] at hm 
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
hfin : Finite a b
hdiv : a ∣ b
⊢ 0 < Part.get (multiplicity a b) hfin
[PROOFSTEP]
refine' zero_lt_iff.2 fun h => _
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
hfin : Finite a b
hdiv : a ∣ b
h : Part.get (multiplicity a b) hfin = 0
⊢ False
[PROOFSTEP]
simpa [hdiv] using is_greatest' hfin (lt_one_iff.mpr h)
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
k : ℕ
hk : a ^ k ∣ b
hsucc : ¬a ^ (k + 1) ∣ b
⊢ multiplicity a b ≤ ↑k
[PROOFSTEP]
have : Finite a b := ⟨k, hsucc⟩
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
k : ℕ
hk : a ^ k ∣ b
hsucc : ¬a ^ (k + 1) ∣ b
this : Finite a b
⊢ multiplicity a b ≤ ↑k
[PROOFSTEP]
rw [PartENat.le_coe_iff]
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
k : ℕ
hk : a ^ k ∣ b
hsucc : ¬a ^ (k + 1) ∣ b
this : Finite a b
⊢ ∃ h, Part.get (multiplicity a b) h ≤ k
[PROOFSTEP]
exact ⟨this, Nat.find_min' _ hsucc⟩
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
k : ℕ
hk : a ^ k ∣ b
hsucc : ¬a ^ (k + 1) ∣ b
⊢ k = Part.get (multiplicity a b) (_ : ∃ n, (fun n => ¬a ^ (n + 1) ∣ b) n)
[PROOFSTEP]
rw [← PartENat.natCast_inj, PartENat.natCast_get, unique hk hsucc]
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
k : ℕ
⊢ multiplicity a b < ↑k ↔ ¬a ^ k ∣ b
[PROOFSTEP]
rw [pow_dvd_iff_le_multiplicity, not_le]
[GOAL]
α : 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
[PROOFSTEP]
rw [← PartENat.some_eq_natCast]
[GOAL]
α : 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
[PROOFSTEP]
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⟩⟩
[GOAL]
α : 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)
[PROOFSTEP]
rw [PartENat.lt_coe_iff]
[GOAL]
α : 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
[PROOFSTEP]
exact ⟨h₁, lt_succ_self _⟩
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
⊢ (∀ (n : ℕ), ¬¬a ^ (n + 1) ∣ b) ↔ ∀ (n : ℕ), a ^ n ∣ b
[PROOFSTEP]
simp only [Classical.not_not]
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
⊢ (∀ (n : ℕ), a ^ (n + 1) ∣ b) ↔ ∀ (n : ℕ), a ^ n ∣ b
[PROOFSTEP]
exact
  ⟨fun h n =>
    Nat.casesOn n
      (by
        rw [_root_.pow_zero]
        exact one_dvd _)
      fun n => h _,
    fun h n => h _⟩
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : ∀ (n : ℕ), a ^ (n + 1) ∣ b
n : ℕ
⊢ a ^ zero ∣ b
[PROOFSTEP]
rw [_root_.pow_zero]
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : ∀ (n : ℕ), a ^ (n + 1) ∣ b
n : ℕ
⊢ 1 ∣ b
[PROOFSTEP]
exact one_dvd _
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : α
ha : Finite a 1
⊢ Part.get (multiplicity a 1) ha = 0
[PROOFSTEP]
rw [PartENat.get_eq_iff_eq_coe, eq_coe_iff, _root_.pow_zero]
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : α
ha : Finite a 1
⊢ 1 ∣ 1 ∧ ¬a ^ (0 + 1) ∣ 1
[PROOFSTEP]
simp [not_dvd_one_of_finite_one_right ha]
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
⊢ multiplicity a b = 0 ↔ ¬a ∣ b
[PROOFSTEP]
rw [← Nat.cast_zero, eq_coe_iff]
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
⊢ a ^ 0 ∣ b ∧ ¬a ^ (0 + 1) ∣ b ↔ ¬a ∣ b
[PROOFSTEP]
simp only [_root_.pow_zero, isUnit_one, IsUnit.dvd, zero_add, pow_one, true_and]
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
⊢ multiplicity a b ≠ ⊤ ↔ Finite a b
[PROOFSTEP]
rw [Ne.def, eq_top_iff_not_finite, Classical.not_not]
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
⊢ multiplicity a b < ⊤ ↔ Finite a b
[PROOFSTEP]
rw [lt_top_iff_ne_top, ne_top_iff_finite]
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
hfin : Finite a b
⊢ ∃ c, b = a ^ Part.get (multiplicity a b) hfin * c ∧ ¬a ∣ c
[PROOFSTEP]
obtain ⟨c, hc⟩ := multiplicity.pow_multiplicity_dvd hfin
[GOAL]
case intro
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
hfin : Finite a b
c : α
hc : b = a ^ Part.get (multiplicity a b) hfin * c
⊢ ∃ c, b = a ^ Part.get (multiplicity a b) hfin * c ∧ ¬a ∣ c
[PROOFSTEP]
refine' ⟨c, hc, _⟩
[GOAL]
case intro
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
hfin : Finite a b
c : α
hc : b = a ^ Part.get (multiplicity a b) hfin * c
⊢ ¬a ∣ c
[PROOFSTEP]
rintro ⟨k, hk⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
hfin : Finite a b
c : α
hc : b = a ^ Part.get (multiplicity a b) hfin * c
k : α
hk : c = a * k
⊢ False
[PROOFSTEP]
rw [hk, ← mul_assoc, ← _root_.pow_succ'] at hc 
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
hfin : Finite a b
c k : α
hc : b = a ^ (Part.get (multiplicity a b) hfin + 1) * k
hk : c = a * k
⊢ False
[PROOFSTEP]
have h₁ : a ^ ((multiplicity a b).get hfin + 1) ∣ b := ⟨k, hc⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
hfin : Finite a b
c k : α
hc : b = a ^ (Part.get (multiplicity a b) hfin + 1) * k
hk : c = a * k
h₁ : a ^ (Part.get (multiplicity a b) hfin + 1) ∣ b
⊢ False
[PROOFSTEP]
exact (multiplicity.eq_coe_iff.1 (by simp)).2 h₁
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
hfin : Finite a b
c k : α
hc : b = a ^ (Part.get (multiplicity a b) hfin + 1) * k
hk : c = a * k
h₁ : a ^ (Part.get (multiplicity a b) hfin + 1) ∣ b
⊢ multiplicity a b = ↑(Part.get (multiplicity a b) hfin)
[PROOFSTEP]
simp
[GOAL]
α : 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
[PROOFSTEP]
rw [← PartENat.natCast_get (finite_iff_dom.1 hab)]
[GOAL]
α : 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
[PROOFSTEP]
exact le_multiplicity_of_pow_dvd (h _ (pow_multiplicity_dvd _))
[GOAL]
α : 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
[PROOFSTEP]
have : ∀ n : ℕ, c ^ n ∣ d := fun n => h n (not_finite_iff_forall.1 hab _)
[GOAL]
α : 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
[PROOFSTEP]
rw [eq_top_iff_not_finite.2 hab, eq_top_iff_not_finite.2 (not_finite_iff_forall.2 this)]
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : 0 < multiplicity a b
⊢ a ∣ b
[PROOFSTEP]
rw [← pow_one a]
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : 0 < multiplicity a b
⊢ a ^ 1 ∣ b
[PROOFSTEP]
apply pow_dvd_of_le_multiplicity
[GOAL]
case a
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : 0 < multiplicity a b
⊢ ↑1 ≤ multiplicity a b
[PROOFSTEP]
simpa only [Nat.cast_one, PartENat.pos_iff_one_le] using h
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
hdvd : a ∣ b
heq : 0 = multiplicity a b
⊢ multiplicity a b < 1
[PROOFSTEP]
simpa only [heq, Nat.cast_zero] using PartENat.coe_lt_coe.mpr zero_lt_one
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
hdvd : a ∣ b
heq : 0 = multiplicity a b
⊢ a ^ 1 ∣ b
[PROOFSTEP]
rwa [pow_one a]
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : ℕ
⊢ Finite a b ↔ a ≠ 1 ∧ 0 < b
[PROOFSTEP]
rw [← not_iff_not, not_finite_iff_forall, not_and_or, Ne.def, Classical.not_not, not_lt, le_zero_iff]
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : ℕ
⊢ (∀ (n : ℕ), a ^ n ∣ b) ↔ a = 1 ∨ b = 0
[PROOFSTEP]
exact
  ⟨fun h =>
    or_iff_not_imp_right.2 fun hb =>
      have ha : a ≠ 0 := fun ha => hb <| zero_dvd_iff.mp <| by rw [ha] at h ; exact h 1
      Classical.by_contradiction fun ha1 : a ≠ 1 =>
        have ha_gt_one : 1 < a :=
          lt_of_not_ge fun _ =>
            match a with
            | 0 => ha rfl
            | 1 => ha1 rfl
            | b + 2 => by linarith
        not_lt_of_ge (le_of_dvd (Nat.pos_of_ne_zero hb) (h b)) (lt_pow_self ha_gt_one b),
    fun h => by cases h <;> simp [*]⟩
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : ℕ
h : ∀ (n : ℕ), a ^ n ∣ b
hb : ¬b = 0
ha : a = 0
⊢ 0 ∣ b
[PROOFSTEP]
rw [ha] at h 
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : ℕ
h : ∀ (n : ℕ), 0 ^ n ∣ b
hb : ¬b = 0
ha : a = 0
⊢ 0 ∣ b
[PROOFSTEP]
exact h 1
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b✝ : ℕ
hb : ¬b✝ = 0
b : ℕ
h : ∀ (n : ℕ), (b + 2) ^ n ∣ b✝
ha : b + 2 ≠ 0
ha1 : b + 2 ≠ 1
x✝ : 1 ≥ b + 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : ℕ
h : a = 1 ∨ b = 0
⊢ ∀ (n : ℕ), a ^ n ∣ b
[PROOFSTEP]
cases h
[GOAL]
case inl
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : ℕ
h✝ : a = 1
⊢ ∀ (n : ℕ), a ^ n ∣ b
[PROOFSTEP]
simp [*]
[GOAL]
case inr
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : ℕ
h✝ : b = 0
⊢ ∀ (n : ℕ), a ^ n ∣ b
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
inst✝ : CommMonoid α
a b c : α
⊢ Finite a (b * c) → Finite a c
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
inst✝ : CommMonoid α
a b c : α
⊢ Finite a (c * b) → Finite a c
[PROOFSTEP]
exact finite_of_finite_mul_right
[GOAL]
α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
ha : ¬IsUnit a
hb : IsUnit b
⊢ a ^ 0 ∣ b
[PROOFSTEP]
simp only [_root_.pow_zero, one_dvd]
[GOAL]
α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
ha : ¬IsUnit a
hb : IsUnit b
⊢ ¬a ^ (0 + 1) ∣ b
[PROOFSTEP]
rw [pow_one]
[GOAL]
α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
ha : ¬IsUnit a
hb : IsUnit b
⊢ ¬a ∣ b
[PROOFSTEP]
exact fun h => mt (isUnit_of_dvd_unit h) ha hb
[GOAL]
α : Type u_1
inst✝ : MonoidWithZero α
a b : α
h : Finite a b
n : ℕ
hn : ¬a ^ (n + 1) ∣ b
hb : b = 0
⊢ False
[PROOFSTEP]
simp [hb] at hn 
[GOAL]
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
⊢ multiplicity (Associates.mk a) (Associates.mk b) = multiplicity a b
[PROOFSTEP]
by_cases h : Finite a b
[GOAL]
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : Finite a b
⊢ multiplicity (Associates.mk a) (Associates.mk b) = multiplicity a b
[PROOFSTEP]
rw [← PartENat.natCast_get (finite_iff_dom.mp h)]
[GOAL]
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : Finite a b
⊢ multiplicity (Associates.mk a) (Associates.mk b) = ↑(Part.get (multiplicity a b) (_ : (multiplicity a b).Dom))
[PROOFSTEP]
refine' (multiplicity.unique (show Associates.mk a ^ (multiplicity a b).get h ∣ Associates.mk b from _) _).symm
[GOAL]
case pos.refine'_1
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : Finite a b
⊢ Associates.mk a ^ Part.get (multiplicity a b) h ∣ Associates.mk b
[PROOFSTEP]
rw [← Associates.mk_pow, Associates.mk_dvd_mk]
[GOAL]
case pos.refine'_2
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : Finite a b
⊢ ¬Associates.mk a ^ (Part.get (multiplicity a b) h + 1) ∣ Associates.mk b
[PROOFSTEP]
rw [← Associates.mk_pow, Associates.mk_dvd_mk]
[GOAL]
case pos.refine'_1
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : Finite a b
⊢ a ^ Part.get (multiplicity a b) h ∣ b
[PROOFSTEP]
exact pow_multiplicity_dvd h
[GOAL]
case pos.refine'_2
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : Finite a b
⊢ ¬a ^ (Part.get (multiplicity a b) h + 1) ∣ b
[PROOFSTEP]
exact is_greatest ((PartENat.lt_coe_iff _ _).mpr (Exists.intro (finite_iff_dom.mp h) (Nat.lt_succ_self _)))
[GOAL]
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : ¬Finite a b
⊢ multiplicity (Associates.mk a) (Associates.mk b) = multiplicity a b
[PROOFSTEP]
suffices ¬Finite (Associates.mk a) (Associates.mk b)
  by
  rw [finite_iff_dom, PartENat.not_dom_iff_eq_top] at h this 
  rw [h, this]
[GOAL]
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : ¬Finite a b
this : ¬Finite (Associates.mk a) (Associates.mk b)
⊢ multiplicity (Associates.mk a) (Associates.mk b) = multiplicity a b
[PROOFSTEP]
rw [finite_iff_dom, PartENat.not_dom_iff_eq_top] at h this 
[GOAL]
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h✝ : ¬Finite a b
h : multiplicity a b = ⊤
this✝ : ¬Finite (Associates.mk a) (Associates.mk b)
this : multiplicity (Associates.mk a) (Associates.mk b) = ⊤
⊢ multiplicity (Associates.mk a) (Associates.mk b) = multiplicity a b
[PROOFSTEP]
rw [h, this]
[GOAL]
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : ¬Finite a b
⊢ ¬Finite (Associates.mk a) (Associates.mk b)
[PROOFSTEP]
refine'
  not_finite_iff_forall.mpr fun n => by
    rw [← Associates.mk_pow, Associates.mk_dvd_mk]
    exact not_finite_iff_forall.mp h n
[GOAL]
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : ¬Finite a b
n : ℕ
⊢ Associates.mk a ^ n ∣ Associates.mk b
[PROOFSTEP]
rw [← Associates.mk_pow, Associates.mk_dvd_mk]
[GOAL]
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : ¬Finite a b
n : ℕ
⊢ a ^ n ∣ b
[PROOFSTEP]
exact not_finite_iff_forall.mp h n
[GOAL]
α : Type u_1
inst✝¹ : Semiring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p a ≤ multiplicity p b
⊢ min (multiplicity p a) (multiplicity p b) ≤ multiplicity p (a + b)
[PROOFSTEP]
rw [min_eq_left h, multiplicity_le_multiplicity_iff]
[GOAL]
α : Type u_1
inst✝¹ : Semiring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p a ≤ multiplicity p b
⊢ ∀ (n : ℕ), p ^ n ∣ a → p ^ n ∣ a + b
[PROOFSTEP]
exact fun n hn => dvd_add hn (multiplicity_le_multiplicity_iff.1 h n hn)
[GOAL]
α : Type u_1
inst✝¹ : Semiring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b ≤ multiplicity p a
⊢ min (multiplicity p a) (multiplicity p b) ≤ multiplicity p (a + b)
[PROOFSTEP]
rw [min_eq_right h, multiplicity_le_multiplicity_iff]
[GOAL]
α : Type u_1
inst✝¹ : Semiring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b ≤ multiplicity p a
⊢ ∀ (n : ℕ), p ^ n ∣ b → p ^ n ∣ a + b
[PROOFSTEP]
exact fun n hn => dvd_add (multiplicity_le_multiplicity_iff.1 h n hn) hn
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
⊢ (multiplicity a (-b)).Dom ↔ (multiplicity a b).Dom
[PROOFSTEP]
simp only [multiplicity, PartENat.find, dvd_neg]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h₁ : (multiplicity a (-b)).Dom
h₂ : (multiplicity a b).Dom
⊢ ↑(Part.get (multiplicity a (-b)) h₁) = ↑(Part.get (multiplicity a b) h₂)
[PROOFSTEP]
rw [PartENat.natCast_get]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h₁ : (multiplicity a (-b)).Dom
h₂ : (multiplicity a b).Dom
⊢ multiplicity a (-b) = ↑(Part.get (multiplicity a b) h₂)
[PROOFSTEP]
exact Eq.symm (unique (pow_multiplicity_dvd _).neg_right (mt dvd_neg.1 (is_greatest' _ (lt_succ_self _))))
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : ℕ
b : ℤ
⊢ multiplicity a (_root_.Int.natAbs b) = multiplicity (↑a) b
[PROOFSTEP]
cases' Int.natAbs_eq b with h h
[GOAL]
case inl
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : ℕ
b : ℤ
h : b = ↑(_root_.Int.natAbs b)
⊢ multiplicity a (_root_.Int.natAbs b) = multiplicity (↑a) b
[PROOFSTEP]
conv_rhs => rw [h]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : ℕ
b : ℤ
h : b = ↑(_root_.Int.natAbs b)
| multiplicity (↑a) b
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : ℕ
b : ℤ
h : b = ↑(_root_.Int.natAbs b)
| multiplicity (↑a) b
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : ℕ
b : ℤ
h : b = ↑(_root_.Int.natAbs b)
| multiplicity (↑a) b
[PROOFSTEP]
rw [h]
[GOAL]
case inr
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : ℕ
b : ℤ
h : b = -↑(_root_.Int.natAbs b)
⊢ multiplicity a (_root_.Int.natAbs b) = multiplicity (↑a) b
[PROOFSTEP]
conv_rhs => rw [h]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : ℕ
b : ℤ
h : b = -↑(_root_.Int.natAbs b)
| multiplicity (↑a) b
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : ℕ
b : ℤ
h : b = -↑(_root_.Int.natAbs b)
| multiplicity (↑a) b
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : ℕ
b : ℤ
h : b = -↑(_root_.Int.natAbs b)
| multiplicity (↑a) b
[PROOFSTEP]
rw [h]
[GOAL]
case inl
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : ℕ
b : ℤ
h : b = ↑(_root_.Int.natAbs b)
⊢ multiplicity a (_root_.Int.natAbs b) = multiplicity ↑a ↑(_root_.Int.natAbs b)
[PROOFSTEP]
rw [Int.coe_nat_multiplicity]
[GOAL]
case inr
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : ℕ
b : ℤ
h : b = -↑(_root_.Int.natAbs b)
⊢ multiplicity a (_root_.Int.natAbs b) = multiplicity (↑a) (-↑(_root_.Int.natAbs b))
[PROOFSTEP]
rw [multiplicity.neg, Int.coe_nat_multiplicity]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) = multiplicity p b
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) ≤ multiplicity p b
[PROOFSTEP]
apply PartENat.le_of_lt_add_one
[GOAL]
case a.h
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) < multiplicity p b + 1
[PROOFSTEP]
cases' PartENat.ne_top_iff.mp (PartENat.ne_top_of_lt h) with k hk
[GOAL]
case a.h.intro
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
⊢ multiplicity p (a + b) < multiplicity p b + 1
[PROOFSTEP]
rw [hk]
[GOAL]
case a.h.intro
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
⊢ multiplicity p (a + b) < ↑k + 1
[PROOFSTEP]
rw_mod_cast [multiplicity_lt_iff_neg_dvd, dvd_add_right]
[GOAL]
case a.h.intro
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
⊢ ¬p ^ (k + 1) ∣ b
case a.h.intro
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
⊢ p ^ (k + 1) ∣ a
[PROOFSTEP]
intro h_dvd
[GOAL]
case a.h.intro
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
h_dvd : p ^ (k + 1) ∣ b
⊢ False
[PROOFSTEP]
apply multiplicity.is_greatest _ h_dvd
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
h_dvd : p ^ (k + 1) ∣ b
⊢ multiplicity p b < ↑(k + 1)
[PROOFSTEP]
rw [hk, ← Nat.succ_eq_add_one]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
h_dvd : p ^ (k + 1) ∣ b
⊢ ↑k < ↑(succ k)
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
h_dvd : p ^ (k + 1) ∣ b
⊢ k < succ k
[PROOFSTEP]
apply Nat.lt_succ_self k
[GOAL]
case a.h.intro
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
⊢ p ^ (k + 1) ∣ a
[PROOFSTEP]
rw [pow_dvd_iff_le_multiplicity, Nat.cast_add, ← hk, Nat.cast_one]
[GOAL]
case a.h.intro
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
k : ℕ
hk : multiplicity p b = ↑k
⊢ multiplicity p b + 1 ≤ multiplicity p a
[PROOFSTEP]
exact PartENat.add_one_le_of_lt h
[GOAL]
case a
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
⊢ multiplicity p b ≤ multiplicity p (a + b)
[PROOFSTEP]
have := @min_le_multiplicity_add α _ _ p a b
[GOAL]
case a
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
this : min (multiplicity p a) (multiplicity p b) ≤ multiplicity p (a + b)
⊢ multiplicity p b ≤ multiplicity p (a + b)
[PROOFSTEP]
rwa [← min_eq_right (le_of_lt h)]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
⊢ multiplicity p (a - b) = multiplicity p b
[PROOFSTEP]
rw [sub_eq_add_neg, multiplicity_add_of_gt]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
⊢ multiplicity p (-b) = multiplicity p b
[PROOFSTEP]
rw [multiplicity.neg]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
⊢ multiplicity p (-b) < multiplicity p a
[PROOFSTEP]
rw [multiplicity.neg]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
⊢ multiplicity p b < multiplicity p a
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p a ≠ multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
[PROOFSTEP]
rcases lt_trichotomy (multiplicity p a) (multiplicity p b) with (hab | hab | hab)
[GOAL]
case inl
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p a < multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
[PROOFSTEP]
rw [add_comm, multiplicity_add_of_gt hab, min_eq_left]
[GOAL]
case inl
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p a < multiplicity p b
⊢ multiplicity p a ≤ multiplicity p b
[PROOFSTEP]
exact le_of_lt hab
[GOAL]
case inr.inl
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p a = multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
[PROOFSTEP]
contradiction
[GOAL]
case inr.inr
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
[PROOFSTEP]
rw [multiplicity_add_of_gt hab, min_eq_right]
[GOAL]
case inr.inr
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p b ≤ multiplicity p a
[PROOFSTEP]
exact le_of_lt hab
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
⊢ a * b = p * (p ^ (n + m) * s)
[PROOFSTEP]
simp [hs, pow_add, mul_comm, mul_assoc, mul_left_comm]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝ : p ∣ a
x : α
hx : a = p * x
hn0 : n = 0
⊢ False
[PROOFSTEP]
simp [hx, hn0] at ha 
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝² : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝¹ : p ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
x✝ : p ^ (n - 1 + 1) ∣ x
y : α
hy : x = p ^ (n - 1 + 1) * y
⊢ p * x * p = p ^ (n + 1) * y * p
[PROOFSTEP]
rw [tsub_add_cancel_of_le (succ_le_of_lt hn0)] at hy 
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝² : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝¹ : p ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
x✝ : p ^ (n - 1 + 1) ∣ x
y : α
hy : x = p ^ n * y
⊢ p * x * p = p ^ (n + 1) * y * p
[PROOFSTEP]
simp [hy, pow_add, mul_comm, mul_assoc, mul_left_comm]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this✝ : p ∣ a * b
x✝ : p ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
hpx : ¬p ^ (n - 1 + 1) ∣ x
this : 1 ≤ n + m
⊢ x * b * p = p ^ (n - 1 + m + 1) * s * p
[PROOFSTEP]
rw [tsub_add_eq_add_tsub (succ_le_of_lt hn0), tsub_add_cancel_of_le this]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this✝ : p ∣ a * b
x✝ : p ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
hpx : ¬p ^ (n - 1 + 1) ∣ x
this : 1 ≤ n + m
⊢ x * b * p = p ^ (n + m) * s * p
[PROOFSTEP]
simp_all [mul_comm, mul_assoc, mul_left_comm, pow_add]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝ : p ∣ b
x : α
hx : b = p * x
hm0 : m = 0
⊢ False
[PROOFSTEP]
simp [hx, hm0] at hb 
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝² : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝¹ : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
x✝ : p ^ (m - 1 + 1) ∣ x
y : α
hy : x = p ^ (m - 1 + 1) * y
⊢ p * x * p = p ^ (m + 1) * y * p
[PROOFSTEP]
rw [tsub_add_cancel_of_le (succ_le_of_lt hm0)] at hy 
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝² : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝¹ : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
x✝ : p ^ (m - 1 + 1) ∣ x
y : α
hy : x = p ^ m * y
⊢ p * x * p = p ^ (m + 1) * y * p
[PROOFSTEP]
simp [hy, pow_add, mul_comm, mul_assoc, mul_left_comm]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝ : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
hpx : ¬p ^ (m - 1 + 1) ∣ x
⊢ a * x * p = p ^ (n + (m - 1) + 1) * s * p
[PROOFSTEP]
rw [add_assoc, tsub_add_cancel_of_le (succ_le_of_lt hm0)]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝ : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
hpx : ¬p ^ (m - 1 + 1) ∣ x
⊢ a * x * p = p ^ (n + m) * s * p
[PROOFSTEP]
simp_all [mul_comm, mul_assoc, mul_left_comm, pow_add]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a : α
hp : Prime p
x✝ : Finite p a
⊢ ¬p ^ (0 + 1) ∣ a ^ 0
[PROOFSTEP]
simp [mt isUnit_iff_dvd_one.2 hp.2.1]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a : α
hp : Prime p
k : ℕ
ha : Finite p a
⊢ Finite p (a ^ (k + 1))
[PROOFSTEP]
rw [_root_.pow_succ]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a : α
hp : Prime p
k : ℕ
ha : Finite p a
⊢ Finite p (a * a ^ k)
[PROOFSTEP]
exact finite_mul hp ha (finite_pow hp ha)
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : α
ha : ¬IsUnit a
ha0 : a ≠ 0
⊢ multiplicity a a = 1
[PROOFSTEP]
rw [← Nat.cast_one]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : α
ha : ¬IsUnit a
ha0 : a ≠ 0
⊢ multiplicity a a = ↑1
[PROOFSTEP]
exact
  eq_coe_iff.2
    ⟨by simp, fun ⟨b, hb⟩ =>
      ha (isUnit_iff_dvd_one.2 ⟨b, mul_left_cancel₀ ha0 <| by simpa [_root_.pow_succ, mul_assoc] using hb⟩)⟩
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : α
ha : ¬IsUnit a
ha0 : a ≠ 0
⊢ a ^ 1 ∣ a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : α
ha : ¬IsUnit a
ha0 : a ≠ 0
x✝ : a ^ (1 + 1) ∣ a
b : α
hb : a = a ^ (1 + 1) * b
⊢ a * 1 = a * (a * b)
[PROOFSTEP]
simpa [_root_.pow_succ, mul_assoc] using hb
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : α
ha : Finite a a
⊢ a ^ 1 ∣ a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : α
ha : Finite a a
x✝ : a ^ (1 + 1) ∣ a
b : α
hb : a = a ^ (1 + 1) * b
⊢ False
[PROOFSTEP]
rw [← mul_one a, pow_add, pow_one, mul_assoc, mul_assoc, mul_right_inj' (ne_zero_of_finite ha)] at hb 
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : α
ha : Finite a a
x✝ : a ^ (1 + 1) ∣ a
b : α
hb : 1 = 1 * (a * 1 * b)
⊢ False
[PROOFSTEP]
exact mt isUnit_iff_dvd_one.2 (not_unit_of_finite ha) ⟨b, by simp_all⟩
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : α
ha : Finite a a
x✝ : a ^ (1 + 1) ∣ a
b : α
hb : 1 = 1 * (a * 1 * b)
⊢ 1 = a * b
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
⊢ Part.get (multiplicity p (a * b)) h =
    Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)
[PROOFSTEP]
have hdiva : p ^ get (multiplicity p a) ((finite_mul_iff hp).1 h).1 ∣ a := pow_multiplicity_dvd _
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
⊢ Part.get (multiplicity p (a * b)) h =
    Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)
[PROOFSTEP]
have hdivb : p ^ get (multiplicity p b) ((finite_mul_iff hp).1 h).2 ∣ b := pow_multiplicity_dvd _
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
hdivb : p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
⊢ Part.get (multiplicity p (a * b)) h =
    Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)
[PROOFSTEP]
have hpoweq :
  p ^ (get (multiplicity p a) ((finite_mul_iff hp).1 h).1 + get (multiplicity p b) ((finite_mul_iff hp).1 h).2) =
    p ^ get (multiplicity p a) ((finite_mul_iff hp).1 h).1 * p ^ get (multiplicity p b) ((finite_mul_iff hp).1 h).2 :=
  by simp [pow_add]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
hdivb : p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
⊢ p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) =
    p ^ Part.get (multiplicity p a) (_ : Finite p a) * p ^ Part.get (multiplicity p b) (_ : Finite p b)
[PROOFSTEP]
simp [pow_add]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
hdivb : p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
hpoweq :
  p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) =
    p ^ Part.get (multiplicity p a) (_ : Finite p a) * p ^ Part.get (multiplicity p b) (_ : Finite p b)
⊢ Part.get (multiplicity p (a * b)) h =
    Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)
[PROOFSTEP]
have hdiv :
  p ^ (get (multiplicity p a) ((finite_mul_iff hp).1 h).1 + get (multiplicity p b) ((finite_mul_iff hp).1 h).2) ∣
    a * b :=
  by rw [hpoweq]; apply mul_dvd_mul <;> assumption
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
hdivb : p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
hpoweq :
  p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) =
    p ^ Part.get (multiplicity p a) (_ : Finite p a) * p ^ Part.get (multiplicity p b) (_ : Finite p b)
⊢ p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) ∣ a * b
[PROOFSTEP]
rw [hpoweq]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
hdivb : p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
hpoweq :
  p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) =
    p ^ Part.get (multiplicity p a) (_ : Finite p a) * p ^ Part.get (multiplicity p b) (_ : Finite p b)
⊢ p ^ Part.get (multiplicity p a) (_ : Finite p a) * p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ a * b
[PROOFSTEP]
apply mul_dvd_mul
[GOAL]
case a
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
hdivb : p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
hpoweq :
  p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) =
    p ^ Part.get (multiplicity p a) (_ : Finite p a) * p ^ Part.get (multiplicity p b) (_ : Finite p b)
⊢ p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
[PROOFSTEP]
assumption
[GOAL]
case a
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
hdivb : p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
hpoweq :
  p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) =
    p ^ Part.get (multiplicity p a) (_ : Finite p a) * p ^ Part.get (multiplicity p b) (_ : Finite p b)
⊢ p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
hdivb : p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
hpoweq :
  p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) =
    p ^ Part.get (multiplicity p a) (_ : Finite p a) * p ^ Part.get (multiplicity p b) (_ : Finite p b)
hdiv : p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) ∣ a * b
⊢ Part.get (multiplicity p (a * b)) h =
    Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)
[PROOFSTEP]
have hsucc :
  ¬p ^ (get (multiplicity p a) ((finite_mul_iff hp).1 h).1 + get (multiplicity p b) ((finite_mul_iff hp).1 h).2 + 1) ∣
      a * b :=
  fun h =>
  not_or_of_not (is_greatest' _ (lt_succ_self _)) (is_greatest' _ (lt_succ_self _))
    (_root_.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul hp hdiva hdivb h)
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
hdivb : p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
hpoweq :
  p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) =
    p ^ Part.get (multiplicity p a) (_ : Finite p a) * p ^ Part.get (multiplicity p b) (_ : Finite p b)
hdiv : p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) ∣ a * b
hsucc : ¬p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b) + 1) ∣ a * b
⊢ Part.get (multiplicity p (a * b)) h =
    Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)
[PROOFSTEP]
rw [← PartENat.natCast_inj, PartENat.natCast_get, eq_coe_iff]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
hdivb : p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
hpoweq :
  p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) =
    p ^ Part.get (multiplicity p a) (_ : Finite p a) * p ^ Part.get (multiplicity p b) (_ : Finite p b)
hdiv : p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) ∣ a * b
hsucc : ¬p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b) + 1) ∣ a * b
⊢ p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) ∣ a * b ∧
    ¬p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b) + 1) ∣ a * b
[PROOFSTEP]
exact ⟨hdiv, hsucc⟩
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : Finite p a ∧ Finite p b
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b
[PROOFSTEP]
rw [← PartENat.natCast_get (finite_iff_dom.1 h.1), ← PartENat.natCast_get (finite_iff_dom.1 h.2), ←
  PartENat.natCast_get (finite_iff_dom.1 (finite_mul hp h.1 h.2)), ← Nat.cast_add, PartENat.natCast_inj,
  multiplicity.mul' hp]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : ¬(Finite p a ∧ Finite p b)
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b
[PROOFSTEP]
rw [eq_top_iff_not_finite.2 (mt (finite_mul_iff hp).1 h)]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : ¬(Finite p a ∧ Finite p b)
⊢ ⊤ = multiplicity p a + multiplicity p b
[PROOFSTEP]
cases' not_and_or.1 h with h h
[GOAL]
case inl
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h✝ : ¬(Finite p a ∧ Finite p b)
h : ¬Finite p a
⊢ ⊤ = multiplicity p a + multiplicity p b
[PROOFSTEP]
simp [eq_top_iff_not_finite.2 h]
[GOAL]
case inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h✝ : ¬(Finite p a ∧ Finite p b)
h : ¬Finite p b
⊢ ⊤ = multiplicity p a + multiplicity p b
[PROOFSTEP]
simp [eq_top_iff_not_finite.2 h]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
β : Type u_2
p : α
hp : Prime p
s : Finset β
f : β → α
⊢ multiplicity p (∏ x in s, f x) = ∑ x in s, multiplicity p (f x)
[PROOFSTEP]
classical
induction' s using Finset.induction with a s has ih h
· simp only [Finset.sum_empty, Finset.prod_empty]
  convert one_right hp.not_unit
· simp [has, ← ih]
  convert multiplicity.mul hp
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
β : Type u_2
p : α
hp : Prime p
s : Finset β
f : β → α
⊢ multiplicity p (∏ x in s, f x) = ∑ x in s, multiplicity p (f x)
[PROOFSTEP]
induction' s using Finset.induction with a s has ih h
[GOAL]
case empty
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
β : Type u_2
p : α
hp : Prime p
f : β → α
⊢ multiplicity p (∏ x in ∅, f x) = ∑ x in ∅, multiplicity p (f x)
[PROOFSTEP]
simp only [Finset.sum_empty, Finset.prod_empty]
[GOAL]
case empty
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
β : Type u_2
p : α
hp : Prime p
f : β → α
⊢ multiplicity p 1 = 0
[PROOFSTEP]
convert one_right hp.not_unit
[GOAL]
case insert
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
β : Type u_2
p : α
hp : Prime p
f : β → α
a : β
s : Finset β
has : ¬a ∈ s
ih : multiplicity p (∏ x in s, f x) = ∑ x in s, multiplicity p (f x)
⊢ multiplicity p (∏ x in insert a s, f x) = ∑ x in insert a s, multiplicity p (f x)
[PROOFSTEP]
simp [has, ← ih]
[GOAL]
case insert
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
β : Type u_2
p : α
hp : Prime p
f : β → α
a : β
s : Finset β
has : ¬a ∈ s
ih : multiplicity p (∏ x in s, f x) = ∑ x in s, multiplicity p (f x)
⊢ multiplicity p (f a * ∏ x in s, f x) = multiplicity p (f a) + multiplicity p (∏ x in s, f x)
[PROOFSTEP]
convert multiplicity.mul hp
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a : α
hp : Prime p
ha : Finite p a
⊢ ∀ {k : ℕ}, Part.get (multiplicity p (a ^ k)) (_ : Finite p (a ^ k)) = k * Part.get (multiplicity p a) ha
[PROOFSTEP]
intro k
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a : α
hp : Prime p
ha : Finite p a
k : ℕ
⊢ Part.get (multiplicity p (a ^ k)) (_ : Finite p (a ^ k)) = k * Part.get (multiplicity p a) ha
[PROOFSTEP]
induction' k with k hk
[GOAL]
case zero
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a : α
hp : Prime p
ha : Finite p a
⊢ Part.get (multiplicity p (a ^ zero)) (_ : Finite p (a ^ zero)) = zero * Part.get (multiplicity p a) ha
[PROOFSTEP]
simp [one_right hp.not_unit]
[GOAL]
case succ
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a : α
hp : Prime p
ha : Finite p a
k : ℕ
hk : Part.get (multiplicity p (a ^ k)) (_ : Finite p (a ^ k)) = k * Part.get (multiplicity p a) ha
⊢ Part.get (multiplicity p (a ^ succ k)) (_ : Finite p (a ^ succ k)) = succ k * Part.get (multiplicity p a) ha
[PROOFSTEP]
have : multiplicity p (a ^ (k + 1)) = multiplicity p (a * a ^ k) := by rw [_root_.pow_succ]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a : α
hp : Prime p
ha : Finite p a
k : ℕ
hk : Part.get (multiplicity p (a ^ k)) (_ : Finite p (a ^ k)) = k * Part.get (multiplicity p a) ha
⊢ multiplicity p (a ^ (k + 1)) = multiplicity p (a * a ^ k)
[PROOFSTEP]
rw [_root_.pow_succ]
[GOAL]
case succ
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a : α
hp : Prime p
ha : Finite p a
k : ℕ
hk : Part.get (multiplicity p (a ^ k)) (_ : Finite p (a ^ k)) = k * Part.get (multiplicity p a) ha
this : multiplicity p (a ^ (k + 1)) = multiplicity p (a * a ^ k)
⊢ Part.get (multiplicity p (a ^ succ k)) (_ : Finite p (a ^ succ k)) = succ k * Part.get (multiplicity p a) ha
[PROOFSTEP]
rw [succ_eq_add_one, get_eq_get_of_eq _ _ this, multiplicity.mul' hp, hk, add_mul, one_mul, add_comm]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a : α
hp : Prime p
⊢ multiplicity p (a ^ 0) = 0 • multiplicity p a
[PROOFSTEP]
simp [one_right hp.not_unit]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a : α
hp : Prime p
k : ℕ
⊢ multiplicity p (a ^ succ k) = succ k • multiplicity p a
[PROOFSTEP]
simp [_root_.pow_succ, succ_nsmul, pow hp, multiplicity.mul hp]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ multiplicity p (p ^ n) = ↑n
[PROOFSTEP]
rw [eq_coe_iff]
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ p ^ n ∣ p ^ n ∧ ¬p ^ (n + 1) ∣ p ^ n
[PROOFSTEP]
use dvd_rfl
[GOAL]
case right
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ ¬p ^ (n + 1) ∣ p ^ n
[PROOFSTEP]
rw [pow_dvd_pow_iff h0 hu]
[GOAL]
case right
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ ¬n + 1 ≤ n
[PROOFSTEP]
apply Nat.not_succ_le_self
[GOAL]
α : Type u_1
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : coprime a b
⊢ multiplicity p a = 0
[PROOFSTEP]
rw [multiplicity_le_multiplicity_iff] at hle 
[GOAL]
α : Type u_1
p a b : ℕ
hp : p ≠ 1
hle : ∀ (n : ℕ), p ^ n ∣ a → p ^ n ∣ b
hab : coprime a b
⊢ multiplicity p a = 0
[PROOFSTEP]
rw [← nonpos_iff_eq_zero, ← not_lt, PartENat.pos_iff_one_le, ← Nat.cast_one, ← pow_dvd_iff_le_multiplicity]
[GOAL]
α : Type u_1
p a b : ℕ
hp : p ≠ 1
hle : ∀ (n : ℕ), p ^ n ∣ a → p ^ n ∣ b
hab : coprime a b
⊢ ¬p ^ 1 ∣ a
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
p a b : ℕ
hp : p ≠ 1
hle : ∀ (n : ℕ), p ^ n ∣ a → p ^ n ∣ b
hab : coprime a b
h : p ^ 1 ∣ a
⊢ False
[PROOFSTEP]
have := Nat.dvd_gcd h (hle _ h)
[GOAL]
α : Type u_1
p a b : ℕ
hp : p ≠ 1
hle : ∀ (n : ℕ), p ^ n ∣ a → p ^ n ∣ b
hab : coprime a b
h : p ^ 1 ∣ a
this : p ^ 1 ∣ Nat.gcd a b
⊢ False
[PROOFSTEP]
rw [coprime.gcd_eq_one hab, Nat.dvd_one, pow_one] at this 
[GOAL]
α : Type u_1
p a b : ℕ
hp : p ≠ 1
hle : ∀ (n : ℕ), p ^ n ∣ a → p ^ n ∣ b
hab : coprime a b
h : p ^ 1 ∣ a
this : p = 1
⊢ False
[PROOFSTEP]
exact hp this
