[GOAL]
⊢ ∀ (a : PrimeMultiset), ⊥ ≤ a
[PROOFSTEP]
simp only [bot_le, forall_const]
[GOAL]
⊢ Repr PrimeMultiset
[PROOFSTEP]
delta PrimeMultiset
[GOAL]
⊢ Repr (Multiset Nat.Primes)
[PROOFSTEP]
infer_instance
[GOAL]
v : PrimeMultiset
p : ℕ
h : p ∈ toNatMultiset v
⊢ Nat.Prime p
[PROOFSTEP]
rcases Multiset.mem_map.mp h with ⟨⟨_, hp'⟩, ⟨_, h_eq⟩⟩
[GOAL]
case intro.mk.intro
v : PrimeMultiset
p : ℕ
h : p ∈ toNatMultiset v
val✝ : ℕ
hp' : Nat.Prime val✝
left✝ : { val := val✝, property := hp' } ∈ v
h_eq : Coe.coe { val := val✝, property := hp' } = p
⊢ Nat.Prime p
[PROOFSTEP]
exact h_eq ▸ hp'
[GOAL]
v : PrimeMultiset
p : ℕ+
h : p ∈ toPNatMultiset v
⊢ PNat.Prime p
[PROOFSTEP]
rcases Multiset.mem_map.mp h with ⟨⟨_, hp'⟩, ⟨_, h_eq⟩⟩
[GOAL]
case intro.mk.intro
v : PrimeMultiset
p : ℕ+
h : p ∈ toPNatMultiset v
val✝ : ℕ
hp' : Nat.Prime val✝
left✝ : { val := val✝, property := hp' } ∈ v
h_eq : Coe.coe { val := val✝, property := hp' } = p
⊢ PNat.Prime p
[PROOFSTEP]
exact h_eq ▸ hp'
[GOAL]
v : PrimeMultiset
⊢ Multiset.map PNat.val (toPNatMultiset v) = toNatMultiset v
[PROOFSTEP]
change (v.map (Coe.coe : Nat.Primes → ℕ+)).map Subtype.val = v.map Subtype.val
[GOAL]
v : PrimeMultiset
⊢ Multiset.map Subtype.val (Multiset.map Coe.coe v) = Multiset.map Subtype.val v
[PROOFSTEP]
rw [Multiset.map_map]
[GOAL]
v : PrimeMultiset
⊢ Multiset.map (Subtype.val ∘ Coe.coe) v = Multiset.map Subtype.val v
[PROOFSTEP]
congr
[GOAL]
v : PrimeMultiset
⊢ ↑(prod v) = Multiset.prod (toNatMultiset v)
[PROOFSTEP]
let h : (v.prod : ℕ) = ((v.map Coe.coe).map Coe.coe).prod := PNat.coeMonoidHom.map_multiset_prod v.toPNatMultiset
[GOAL]
v : PrimeMultiset
h : ↑(prod v) = Multiset.prod (Multiset.map Coe.coe (Multiset.map Coe.coe v)) :=
  MonoidHom.map_multiset_prod PNat.coeMonoidHom (toPNatMultiset v)
⊢ ↑(prod v) = Multiset.prod (toNatMultiset v)
[PROOFSTEP]
rw [Multiset.map_map] at h 
[GOAL]
v : PrimeMultiset
h : ↑(prod v) = Multiset.prod (Multiset.map (Coe.coe ∘ Coe.coe) v)
⊢ ↑(prod v) = Multiset.prod (toNatMultiset v)
[PROOFSTEP]
have : (Coe.coe : ℕ+ → ℕ) ∘ (Coe.coe : Nat.Primes → ℕ+) = Coe.coe := funext fun p => rfl
[GOAL]
v : PrimeMultiset
h : ↑(prod v) = Multiset.prod (Multiset.map (Coe.coe ∘ Coe.coe) v)
this : Coe.coe ∘ Coe.coe = Coe.coe
⊢ ↑(prod v) = Multiset.prod (toNatMultiset v)
[PROOFSTEP]
rw [this] at h 
[GOAL]
v : PrimeMultiset
h : ↑(prod v) = Multiset.prod (Multiset.map Coe.coe v)
this : Coe.coe ∘ Coe.coe = Coe.coe
⊢ ↑(prod v) = Multiset.prod (toNatMultiset v)
[PROOFSTEP]
exact h
[GOAL]
v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
⊢ toNatMultiset (ofNatMultiset v h) = v
[PROOFSTEP]
dsimp [ofNatMultiset, toNatMultiset]
[GOAL]
v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
⊢ Multiset.map Coe.coe (Multiset.pmap (fun p hp => { val := p, property := hp }) v h) = v
[PROOFSTEP]
have : (fun p h => (Coe.coe : Nat.Primes → ℕ) ⟨p, h⟩) = fun p _ => id p :=
  by
  funext p h
  rfl
[GOAL]
v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
⊢ (fun p h => Coe.coe { val := p, property := h }) = fun p x => id p
[PROOFSTEP]
funext p h
[GOAL]
case h.h
v : Multiset ℕ
h✝ : ∀ (p : ℕ), p ∈ v → Nat.Prime p
p : ℕ
h : Nat.Prime p
⊢ Coe.coe { val := p, property := h } = id p
[PROOFSTEP]
rfl
[GOAL]
v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
this : (fun p h => Coe.coe { val := p, property := h }) = fun p x => id p
⊢ Multiset.map Coe.coe (Multiset.pmap (fun p hp => { val := p, property := hp }) v h) = v
[PROOFSTEP]
rw [Multiset.map_pmap, this, Multiset.pmap_eq_map, Multiset.map_id]
[GOAL]
v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
⊢ ↑(prod (ofNatMultiset v h)) = Multiset.prod v
[PROOFSTEP]
rw [coe_prod, to_ofNatMultiset]
[GOAL]
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
⊢ toPNatMultiset (ofPNatMultiset v h) = v
[PROOFSTEP]
dsimp [ofPNatMultiset, toPNatMultiset]
[GOAL]
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
⊢ Multiset.map Coe.coe (Multiset.pmap (fun p hp => { val := ↑p, property := hp }) v h) = v
[PROOFSTEP]
have : (fun (p : ℕ+) (h : p.Prime) => (Coe.coe : Nat.Primes → ℕ+) ⟨p, h⟩) = fun p _ => id p :=
  by
  funext p h
  apply Subtype.eq
  rfl
[GOAL]
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
⊢ (fun p h => Coe.coe { val := ↑p, property := h }) = fun p x => id p
[PROOFSTEP]
funext p h
[GOAL]
case h.h
v : Multiset ℕ+
h✝ : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
p : ℕ+
h : PNat.Prime p
⊢ Coe.coe { val := ↑p, property := h } = id p
[PROOFSTEP]
apply Subtype.eq
[GOAL]
case h.h.a
v : Multiset ℕ+
h✝ : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
p : ℕ+
h : PNat.Prime p
⊢ ↑(Coe.coe { val := ↑p, property := h }) = ↑(id p)
[PROOFSTEP]
rfl
[GOAL]
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
this : (fun p h => Coe.coe { val := ↑p, property := h }) = fun p x => id p
⊢ Multiset.map Coe.coe (Multiset.pmap (fun p hp => { val := ↑p, property := hp }) v h) = v
[PROOFSTEP]
rw [Multiset.map_pmap, this, Multiset.pmap_eq_map, Multiset.map_id]
[GOAL]
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
⊢ prod (ofPNatMultiset v h) = Multiset.prod v
[PROOFSTEP]
dsimp [prod]
[GOAL]
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → PNat.Prime p
⊢ Multiset.prod (toPNatMultiset (ofPNatMultiset v h)) = Multiset.prod v
[PROOFSTEP]
rw [to_ofPNatMultiset]
[GOAL]
l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
⊢ ↑(prod (ofNatList l h)) = List.prod l
[PROOFSTEP]
have := prod_ofNatMultiset (l : Multiset ℕ) h
[GOAL]
l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
this : ↑(prod (ofNatMultiset (↑l) h)) = Multiset.prod ↑l
⊢ ↑(prod (ofNatList l h)) = List.prod l
[PROOFSTEP]
rw [Multiset.coe_prod] at this 
[GOAL]
l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
this : ↑(prod (ofNatMultiset (↑l) h)) = List.prod l
⊢ ↑(prod (ofNatList l h)) = List.prod l
[PROOFSTEP]
exact this
[GOAL]
l : List ℕ+
h : ∀ (p : ℕ+), p ∈ l → PNat.Prime p
⊢ prod (ofPNatList l h) = List.prod l
[PROOFSTEP]
have := prod_ofPNatMultiset (l : Multiset ℕ+) h
[GOAL]
l : List ℕ+
h : ∀ (p : ℕ+), p ∈ l → PNat.Prime p
this : prod (ofPNatMultiset (↑l) h) = Multiset.prod ↑l
⊢ prod (ofPNatList l h) = List.prod l
[PROOFSTEP]
rw [Multiset.coe_prod] at this 
[GOAL]
l : List ℕ+
h : ∀ (p : ℕ+), p ∈ l → PNat.Prime p
this : prod (ofPNatMultiset (↑l) h) = List.prod l
⊢ prod (ofPNatList l h) = List.prod l
[PROOFSTEP]
exact this
[GOAL]
⊢ prod 0 = 1
[PROOFSTEP]
exact Multiset.prod_zero
[GOAL]
u v : PrimeMultiset
⊢ prod (u + v) = prod u * prod v
[PROOFSTEP]
change (coePNatMonoidHom (u + v)).prod = _
[GOAL]
u v : PrimeMultiset
⊢ Multiset.prod (↑coePNatMonoidHom (u + v)) = prod u * prod v
[PROOFSTEP]
rw [coePNatMonoidHom.map_add]
[GOAL]
u v : PrimeMultiset
⊢ Multiset.prod (↑coePNatMonoidHom u + ↑coePNatMonoidHom v) = prod u * prod v
[PROOFSTEP]
exact Multiset.prod_add _ _
[GOAL]
d : ℕ
u : PrimeMultiset
⊢ prod (d • u) = Pow.pow (prod u) d
[PROOFSTEP]
induction' d with n ih
[GOAL]
case zero
u : PrimeMultiset
⊢ prod (Nat.zero • u) = Pow.pow (prod u) Nat.zero
[PROOFSTEP]
rfl
[GOAL]
case succ
u : PrimeMultiset
n : ℕ
ih : prod (n • u) = Pow.pow (prod u) n
⊢ prod (Nat.succ n • u) = Pow.pow (prod u) (Nat.succ n)
[PROOFSTEP]
have : ∀ n' : ℕ, Pow.pow (prod u) n' = Monoid.npow n' (prod u) := fun _ ↦ rfl
[GOAL]
case succ
u : PrimeMultiset
n : ℕ
ih : prod (n • u) = Pow.pow (prod u) n
this : ∀ (n' : ℕ), Pow.pow (prod u) n' = Monoid.npow n' (prod u)
⊢ prod (Nat.succ n • u) = Pow.pow (prod u) (Nat.succ n)
[PROOFSTEP]
rw [succ_nsmul, prod_add, ih, this, this, Monoid.npow_succ, mul_comm]
[GOAL]
n : ℕ+
⊢ ↑(PrimeMultiset.prod (factorMultiset n)) = ↑n
[PROOFSTEP]
dsimp [factorMultiset]
[GOAL]
n : ℕ+
⊢ ↑(PrimeMultiset.prod (PrimeMultiset.ofNatList (Nat.factors ↑n) (_ : ∀ {p : ℕ}, p ∈ Nat.factors ↑n → Nat.Prime p))) =
    ↑n
[PROOFSTEP]
rw [PrimeMultiset.prod_ofNatList]
[GOAL]
n : ℕ+
⊢ List.prod (Nat.factors ↑n) = ↑n
[PROOFSTEP]
exact Nat.prod_factors n.ne_zero
[GOAL]
v : PrimeMultiset
⊢ PNat.factorMultiset (prod v) = v
[PROOFSTEP]
apply PrimeMultiset.coeNat_injective
[GOAL]
case a
v : PrimeMultiset
⊢ Coe.coe (PNat.factorMultiset (prod v)) = Coe.coe v
[PROOFSTEP]
suffices toNatMultiset (PNat.factorMultiset (prod v)) = toNatMultiset v by exact this
[GOAL]
v : PrimeMultiset
this : toNatMultiset (PNat.factorMultiset (prod v)) = toNatMultiset v
⊢ Coe.coe (PNat.factorMultiset (prod v)) = Coe.coe v
[PROOFSTEP]
exact this
[GOAL]
case a
v : PrimeMultiset
⊢ toNatMultiset (PNat.factorMultiset (prod v)) = toNatMultiset v
[PROOFSTEP]
rw [v.prod.coeNat_factorMultiset, PrimeMultiset.coe_prod]
[GOAL]
case a
v : PrimeMultiset
⊢ ↑(Nat.factors (Multiset.prod (toNatMultiset v))) = toNatMultiset v
[PROOFSTEP]
rcases v with
  ⟨l⟩
    --unfold_coes
[GOAL]
case a.mk
v : PrimeMultiset
l : List Nat.Primes
⊢ ↑(Nat.factors (Multiset.prod (toNatMultiset (Quot.mk Setoid.r l)))) = toNatMultiset (Quot.mk Setoid.r l)
[PROOFSTEP]
dsimp [PrimeMultiset.toNatMultiset]
[GOAL]
case a.mk
v : PrimeMultiset
l : List Nat.Primes
⊢ ↑(Nat.factors (Multiset.prod ↑(List.map Coe.coe l))) = ↑(List.map Coe.coe l)
[PROOFSTEP]
rw [Multiset.coe_prod]
[GOAL]
case a.mk
v : PrimeMultiset
l : List Nat.Primes
⊢ ↑(Nat.factors (List.prod (List.map Coe.coe l))) = ↑(List.map Coe.coe l)
[PROOFSTEP]
let l' := l.map (Coe.coe : Nat.Primes → ℕ)
[GOAL]
case a.mk
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map Coe.coe l
⊢ ↑(Nat.factors (List.prod (List.map Coe.coe l))) = ↑(List.map Coe.coe l)
[PROOFSTEP]
have : ∀ p : ℕ, p ∈ l' → p.Prime := fun p hp =>
  by
  rcases List.mem_map.mp hp with ⟨⟨_, hp'⟩, ⟨_, h_eq⟩⟩
  exact h_eq ▸ hp'
[GOAL]
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map Coe.coe l
p : ℕ
hp : p ∈ l'
⊢ Nat.Prime p
[PROOFSTEP]
rcases List.mem_map.mp hp with ⟨⟨_, hp'⟩, ⟨_, h_eq⟩⟩
[GOAL]
case intro.mk.intro
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map Coe.coe l
p : ℕ
hp : p ∈ l'
val✝ : ℕ
hp' : Nat.Prime val✝
left✝ : { val := val✝, property := hp' } ∈ l
h_eq : Coe.coe { val := val✝, property := hp' } = p
⊢ Nat.Prime p
[PROOFSTEP]
exact h_eq ▸ hp'
[GOAL]
case a.mk
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map Coe.coe l
this : ∀ (p : ℕ), p ∈ l' → Nat.Prime p
⊢ ↑(Nat.factors (List.prod (List.map Coe.coe l))) = ↑(List.map Coe.coe l)
[PROOFSTEP]
exact Multiset.coe_eq_coe.mpr (@Nat.factors_unique _ l' rfl this).symm
[GOAL]
⊢ factorMultiset 1 = 0
[PROOFSTEP]
simp [factorMultiset, PrimeMultiset.ofNatList, PrimeMultiset.ofNatMultiset]
[GOAL]
n m : ℕ+
⊢ factorMultiset (n * m) = factorMultiset n + factorMultiset m
[PROOFSTEP]
let u := factorMultiset n
[GOAL]
n m : ℕ+
u : PrimeMultiset := factorMultiset n
⊢ factorMultiset (n * m) = factorMultiset n + factorMultiset m
[PROOFSTEP]
let v := factorMultiset m
[GOAL]
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
⊢ factorMultiset (n * m) = factorMultiset n + factorMultiset m
[PROOFSTEP]
have : n = u.prod := (prod_factorMultiset n).symm
[GOAL]
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this : n = PrimeMultiset.prod u
⊢ factorMultiset (n * m) = factorMultiset n + factorMultiset m
[PROOFSTEP]
rw [this]
[GOAL]
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this : n = PrimeMultiset.prod u
⊢ factorMultiset (PrimeMultiset.prod u * m) = factorMultiset (PrimeMultiset.prod u) + factorMultiset m
[PROOFSTEP]
have : m = v.prod := (prod_factorMultiset m).symm
[GOAL]
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this✝ : n = PrimeMultiset.prod u
this : m = PrimeMultiset.prod v
⊢ factorMultiset (PrimeMultiset.prod u * m) = factorMultiset (PrimeMultiset.prod u) + factorMultiset m
[PROOFSTEP]
rw [this]
[GOAL]
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this✝ : n = PrimeMultiset.prod u
this : m = PrimeMultiset.prod v
⊢ factorMultiset (PrimeMultiset.prod u * PrimeMultiset.prod v) =
    factorMultiset (PrimeMultiset.prod u) + factorMultiset (PrimeMultiset.prod v)
[PROOFSTEP]
rw [← PrimeMultiset.prod_add]
[GOAL]
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this✝ : n = PrimeMultiset.prod u
this : m = PrimeMultiset.prod v
⊢ factorMultiset (PrimeMultiset.prod (u + v)) =
    factorMultiset (PrimeMultiset.prod u) + factorMultiset (PrimeMultiset.prod v)
[PROOFSTEP]
repeat' rw [PrimeMultiset.factorMultiset_prod]
[GOAL]
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this✝ : n = PrimeMultiset.prod u
this : m = PrimeMultiset.prod v
⊢ factorMultiset (PrimeMultiset.prod (u + v)) =
    factorMultiset (PrimeMultiset.prod u) + factorMultiset (PrimeMultiset.prod v)
[PROOFSTEP]
rw [PrimeMultiset.factorMultiset_prod]
[GOAL]
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this✝ : n = PrimeMultiset.prod u
this : m = PrimeMultiset.prod v
⊢ u + v = factorMultiset (PrimeMultiset.prod u) + factorMultiset (PrimeMultiset.prod v)
[PROOFSTEP]
rw [PrimeMultiset.factorMultiset_prod]
[GOAL]
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this✝ : n = PrimeMultiset.prod u
this : m = PrimeMultiset.prod v
⊢ u + v = u + factorMultiset (PrimeMultiset.prod v)
[PROOFSTEP]
rw [PrimeMultiset.factorMultiset_prod]
[GOAL]
n : ℕ+
m : ℕ
⊢ factorMultiset (Pow.pow n m) = m • factorMultiset n
[PROOFSTEP]
let u := factorMultiset n
[GOAL]
n : ℕ+
m : ℕ
u : PrimeMultiset := factorMultiset n
⊢ factorMultiset (Pow.pow n m) = m • factorMultiset n
[PROOFSTEP]
have : n = u.prod := (prod_factorMultiset n).symm
[GOAL]
n : ℕ+
m : ℕ
u : PrimeMultiset := factorMultiset n
this : n = PrimeMultiset.prod u
⊢ factorMultiset (Pow.pow n m) = m • factorMultiset n
[PROOFSTEP]
rw [this, ← PrimeMultiset.prod_smul]
[GOAL]
n : ℕ+
m : ℕ
u : PrimeMultiset := factorMultiset n
this : n = PrimeMultiset.prod u
⊢ factorMultiset (PrimeMultiset.prod (m • u)) = m • factorMultiset (PrimeMultiset.prod u)
[PROOFSTEP]
repeat' rw [PrimeMultiset.factorMultiset_prod]
[GOAL]
n : ℕ+
m : ℕ
u : PrimeMultiset := factorMultiset n
this : n = PrimeMultiset.prod u
⊢ factorMultiset (PrimeMultiset.prod (m • u)) = m • factorMultiset (PrimeMultiset.prod u)
[PROOFSTEP]
rw [PrimeMultiset.factorMultiset_prod]
[GOAL]
n : ℕ+
m : ℕ
u : PrimeMultiset := factorMultiset n
this : n = PrimeMultiset.prod u
⊢ m • u = m • factorMultiset (PrimeMultiset.prod u)
[PROOFSTEP]
rw [PrimeMultiset.factorMultiset_prod]
[GOAL]
p : Nat.Primes
⊢ factorMultiset ↑p = PrimeMultiset.ofPrime p
[PROOFSTEP]
apply factorMultisetEquiv.symm.injective
[GOAL]
case a
p : Nat.Primes
⊢ ↑factorMultisetEquiv.symm (factorMultiset ↑p) = ↑factorMultisetEquiv.symm (PrimeMultiset.ofPrime p)
[PROOFSTEP]
change (p : ℕ+).factorMultiset.prod = (PrimeMultiset.ofPrime p).prod
[GOAL]
case a
p : Nat.Primes
⊢ PrimeMultiset.prod (factorMultiset ↑p) = PrimeMultiset.prod (PrimeMultiset.ofPrime p)
[PROOFSTEP]
rw [(p : ℕ+).prod_factorMultiset, PrimeMultiset.prod_ofPrime]
[GOAL]
m n : ℕ+
⊢ factorMultiset m ≤ factorMultiset n ↔ m ∣ n
[PROOFSTEP]
constructor
[GOAL]
case mp
m n : ℕ+
⊢ factorMultiset m ≤ factorMultiset n → m ∣ n
[PROOFSTEP]
intro h
[GOAL]
case mp
m n : ℕ+
h : factorMultiset m ≤ factorMultiset n
⊢ m ∣ n
[PROOFSTEP]
rw [← prod_factorMultiset m, ← prod_factorMultiset m]
[GOAL]
case mp
m n : ℕ+
h : factorMultiset m ≤ factorMultiset n
⊢ PrimeMultiset.prod (factorMultiset (PrimeMultiset.prod (factorMultiset m))) ∣ n
[PROOFSTEP]
apply Dvd.intro (n.factorMultiset - m.factorMultiset).prod
[GOAL]
case mp
m n : ℕ+
h : factorMultiset m ≤ factorMultiset n
⊢ PrimeMultiset.prod (factorMultiset (PrimeMultiset.prod (factorMultiset m))) *
      PrimeMultiset.prod (factorMultiset n - factorMultiset m) =
    n
[PROOFSTEP]
rw [← PrimeMultiset.prod_add, PrimeMultiset.factorMultiset_prod, add_tsub_cancel_of_le h, prod_factorMultiset]
[GOAL]
case mpr
m n : ℕ+
⊢ m ∣ n → factorMultiset m ≤ factorMultiset n
[PROOFSTEP]
intro h
[GOAL]
case mpr
m n : ℕ+
h : m ∣ n
⊢ factorMultiset m ≤ factorMultiset n
[PROOFSTEP]
rw [← mul_div_exact h, factorMultiset_mul]
[GOAL]
case mpr
m n : ℕ+
h : m ∣ n
⊢ factorMultiset m ≤ factorMultiset m + factorMultiset (divExact n m)
[PROOFSTEP]
exact le_self_add
[GOAL]
m : ℕ+
v : PrimeMultiset
⊢ factorMultiset m ≤ v ↔ m ∣ PrimeMultiset.prod v
[PROOFSTEP]
let h := @factorMultiset_le_iff m v.prod
[GOAL]
m : ℕ+
v : PrimeMultiset
h : factorMultiset m ≤ factorMultiset (PrimeMultiset.prod v) ↔ m ∣ PrimeMultiset.prod v := factorMultiset_le_iff
⊢ factorMultiset m ≤ v ↔ m ∣ PrimeMultiset.prod v
[PROOFSTEP]
rw [v.factorMultiset_prod] at h 
[GOAL]
m : ℕ+
v : PrimeMultiset
h : factorMultiset m ≤ v ↔ m ∣ PrimeMultiset.prod v
⊢ factorMultiset m ≤ v ↔ m ∣ PrimeMultiset.prod v
[PROOFSTEP]
exact h
[GOAL]
u v : PrimeMultiset
⊢ prod u ∣ prod v ↔ u ≤ v
[PROOFSTEP]
let h := @PNat.factorMultiset_le_iff' u.prod v
[GOAL]
u v : PrimeMultiset
h : PNat.factorMultiset (prod u) ≤ v ↔ prod u ∣ prod v := PNat.factorMultiset_le_iff'
⊢ prod u ∣ prod v ↔ u ≤ v
[PROOFSTEP]
rw [u.factorMultiset_prod] at h 
[GOAL]
u v : PrimeMultiset
h : u ≤ v ↔ prod u ∣ prod v
⊢ prod u ∣ prod v ↔ u ≤ v
[PROOFSTEP]
exact h.symm
[GOAL]
u : PrimeMultiset
n : ℕ+
⊢ prod u ∣ n ↔ u ≤ PNat.factorMultiset n
[PROOFSTEP]
let h := @prod_dvd_iff u n.factorMultiset
[GOAL]
u : PrimeMultiset
n : ℕ+
h : prod u ∣ prod (PNat.factorMultiset n) ↔ u ≤ PNat.factorMultiset n := prod_dvd_iff
⊢ prod u ∣ n ↔ u ≤ PNat.factorMultiset n
[PROOFSTEP]
rw [n.prod_factorMultiset] at h 
[GOAL]
u : PrimeMultiset
n : ℕ+
h : prod u ∣ n ↔ u ≤ PNat.factorMultiset n
⊢ prod u ∣ n ↔ u ≤ PNat.factorMultiset n
[PROOFSTEP]
exact h
[GOAL]
m n : ℕ+
⊢ factorMultiset (gcd m n) = factorMultiset m ⊓ factorMultiset n
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
m n : ℕ+
⊢ factorMultiset (gcd m n) ≤ factorMultiset m ⊓ factorMultiset n
[PROOFSTEP]
apply le_inf_iff.mpr
[GOAL]
case a
m n : ℕ+
⊢ factorMultiset (gcd m n) ≤ factorMultiset m ∧ factorMultiset (gcd m n) ≤ factorMultiset n
[PROOFSTEP]
constructor
[GOAL]
case a.left
m n : ℕ+
⊢ factorMultiset (gcd m n) ≤ factorMultiset m
[PROOFSTEP]
apply factorMultiset_le_iff.mpr
[GOAL]
case a.right
m n : ℕ+
⊢ factorMultiset (gcd m n) ≤ factorMultiset n
[PROOFSTEP]
apply factorMultiset_le_iff.mpr
[GOAL]
case a.left
m n : ℕ+
⊢ gcd m n ∣ m
case a.right m n : ℕ+ ⊢ gcd m n ∣ n
[PROOFSTEP]
exact gcd_dvd_left m n
[GOAL]
case a.right
m n : ℕ+
⊢ gcd m n ∣ n
[PROOFSTEP]
exact gcd_dvd_right m n
[GOAL]
case a
m n : ℕ+
⊢ factorMultiset m ⊓ factorMultiset n ≤ factorMultiset (gcd m n)
[PROOFSTEP]
rw [← PrimeMultiset.prod_dvd_iff, prod_factorMultiset]
[GOAL]
case a
m n : ℕ+
⊢ PrimeMultiset.prod (factorMultiset m ⊓ factorMultiset n) ∣ gcd m n
[PROOFSTEP]
apply dvd_gcd
[GOAL]
case a.hm
m n : ℕ+
⊢ PrimeMultiset.prod (factorMultiset m ⊓ factorMultiset n) ∣ m
[PROOFSTEP]
rw [PrimeMultiset.prod_dvd_iff']
[GOAL]
case a.hn
m n : ℕ+
⊢ PrimeMultiset.prod (factorMultiset m ⊓ factorMultiset n) ∣ n
[PROOFSTEP]
rw [PrimeMultiset.prod_dvd_iff']
[GOAL]
case a.hm
m n : ℕ+
⊢ factorMultiset m ⊓ factorMultiset n ≤ factorMultiset m
case a.hn m n : ℕ+ ⊢ factorMultiset m ⊓ factorMultiset n ≤ factorMultiset n
[PROOFSTEP]
exact inf_le_left
[GOAL]
case a.hn
m n : ℕ+
⊢ factorMultiset m ⊓ factorMultiset n ≤ factorMultiset n
[PROOFSTEP]
exact inf_le_right
[GOAL]
m n : ℕ+
⊢ factorMultiset (lcm m n) = factorMultiset m ⊔ factorMultiset n
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
m n : ℕ+
⊢ factorMultiset (lcm m n) ≤ factorMultiset m ⊔ factorMultiset n
[PROOFSTEP]
rw [← PrimeMultiset.prod_dvd_iff, prod_factorMultiset]
[GOAL]
case a
m n : ℕ+
⊢ lcm m n ∣ PrimeMultiset.prod (factorMultiset m ⊔ factorMultiset n)
[PROOFSTEP]
apply lcm_dvd
[GOAL]
case a.hm
m n : ℕ+
⊢ m ∣ PrimeMultiset.prod (factorMultiset m ⊔ factorMultiset n)
[PROOFSTEP]
rw [← factorMultiset_le_iff']
[GOAL]
case a.hn
m n : ℕ+
⊢ n ∣ PrimeMultiset.prod (factorMultiset m ⊔ factorMultiset n)
[PROOFSTEP]
rw [← factorMultiset_le_iff']
[GOAL]
case a.hm
m n : ℕ+
⊢ factorMultiset m ≤ factorMultiset m ⊔ factorMultiset n
case a.hn m n : ℕ+ ⊢ factorMultiset n ≤ factorMultiset m ⊔ factorMultiset n
[PROOFSTEP]
exact le_sup_left
[GOAL]
case a.hn
m n : ℕ+
⊢ factorMultiset n ≤ factorMultiset m ⊔ factorMultiset n
[PROOFSTEP]
exact le_sup_right
[GOAL]
case a
m n : ℕ+
⊢ factorMultiset m ⊔ factorMultiset n ≤ factorMultiset (lcm m n)
[PROOFSTEP]
apply sup_le_iff.mpr
[GOAL]
case a
m n : ℕ+
⊢ factorMultiset m ≤ factorMultiset (lcm m n) ∧ factorMultiset n ≤ factorMultiset (lcm m n)
[PROOFSTEP]
constructor
[GOAL]
case a.left
m n : ℕ+
⊢ factorMultiset m ≤ factorMultiset (lcm m n)
[PROOFSTEP]
apply factorMultiset_le_iff.mpr
[GOAL]
case a.right
m n : ℕ+
⊢ factorMultiset n ≤ factorMultiset (lcm m n)
[PROOFSTEP]
apply factorMultiset_le_iff.mpr
[GOAL]
case a.left
m n : ℕ+
⊢ m ∣ lcm m n
case a.right m n : ℕ+ ⊢ n ∣ lcm m n
[PROOFSTEP]
exact dvd_lcm_left m n
[GOAL]
case a.right
m n : ℕ+
⊢ n ∣ lcm m n
[PROOFSTEP]
exact dvd_lcm_right m n
[GOAL]
m : ℕ+
p : Nat.Primes
k : ℕ
⊢ Pow.pow (↑p) k ∣ m ↔ k ≤ Multiset.count p (factorMultiset m)
[PROOFSTEP]
intros
[GOAL]
m : ℕ+
p : Nat.Primes
k : ℕ
⊢ Pow.pow (↑p) k ∣ m ↔ k ≤ Multiset.count p (factorMultiset m)
[PROOFSTEP]
rw [Multiset.le_count_iff_replicate_le, ← factorMultiset_le_iff, factorMultiset_pow, factorMultiset_ofPrime]
[GOAL]
m : ℕ+
p : Nat.Primes
k : ℕ
⊢ k • PrimeMultiset.ofPrime p ≤ factorMultiset m ↔ Multiset.replicate k p ≤ factorMultiset m
[PROOFSTEP]
congr! 2
[GOAL]
case a.h.e'_3.h
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ k • PrimeMultiset.ofPrime p = Multiset.replicate k p
[PROOFSTEP]
apply Multiset.eq_replicate.mpr
[GOAL]
case a.h.e'_3.h
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ ↑Multiset.card (k • PrimeMultiset.ofPrime p) = k ∧ ∀ (b : Nat.Primes), b ∈ k • PrimeMultiset.ofPrime p → b = p
[PROOFSTEP]
constructor
[GOAL]
case a.h.e'_3.h.left
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ ↑Multiset.card (k • PrimeMultiset.ofPrime p) = k
[PROOFSTEP]
rw [Multiset.card_nsmul, PrimeMultiset.card_ofPrime, mul_one]
[GOAL]
case a.h.e'_3.h.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
⊢ ∀ (b : Nat.Primes), b ∈ k • PrimeMultiset.ofPrime p → b = p
[PROOFSTEP]
intro q h
[GOAL]
case a.h.e'_3.h.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
q : Nat.Primes
h : q ∈ k • PrimeMultiset.ofPrime p
⊢ q = p
[PROOFSTEP]
rw [PrimeMultiset.ofPrime, Multiset.nsmul_singleton _ k] at h 
[GOAL]
case a.h.e'_3.h.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
q : Nat.Primes
h : q ∈ Multiset.replicate k p
⊢ q = p
[PROOFSTEP]
exact Multiset.eq_of_mem_replicate h
[GOAL]
u v : PrimeMultiset
⊢ prod (u ⊓ v) = PNat.gcd (prod u) (prod v)
[PROOFSTEP]
let n := u.prod
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
⊢ prod (u ⊓ v) = PNat.gcd (prod u) (prod v)
[PROOFSTEP]
let m := v.prod
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
⊢ prod (u ⊓ v) = PNat.gcd (prod u) (prod v)
[PROOFSTEP]
change (u ⊓ v).prod = PNat.gcd n m
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
⊢ prod (u ⊓ v) = PNat.gcd n m
[PROOFSTEP]
have : u = n.factorMultiset := u.factorMultiset_prod.symm
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
this : u = PNat.factorMultiset n
⊢ prod (u ⊓ v) = PNat.gcd n m
[PROOFSTEP]
rw [this]
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
this : u = PNat.factorMultiset n
⊢ prod (PNat.factorMultiset n ⊓ v) = PNat.gcd n m
[PROOFSTEP]
have : v = m.factorMultiset := v.factorMultiset_prod.symm
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
this✝ : u = PNat.factorMultiset n
this : v = PNat.factorMultiset m
⊢ prod (PNat.factorMultiset n ⊓ v) = PNat.gcd n m
[PROOFSTEP]
rw [this]
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
this✝ : u = PNat.factorMultiset n
this : v = PNat.factorMultiset m
⊢ prod (PNat.factorMultiset n ⊓ PNat.factorMultiset m) = PNat.gcd n m
[PROOFSTEP]
rw [← PNat.factorMultiset_gcd n m, PNat.prod_factorMultiset]
[GOAL]
u v : PrimeMultiset
⊢ prod (u ⊔ v) = PNat.lcm (prod u) (prod v)
[PROOFSTEP]
let n := u.prod
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
⊢ prod (u ⊔ v) = PNat.lcm (prod u) (prod v)
[PROOFSTEP]
let m := v.prod
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
⊢ prod (u ⊔ v) = PNat.lcm (prod u) (prod v)
[PROOFSTEP]
change (u ⊔ v).prod = PNat.lcm n m
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
⊢ prod (u ⊔ v) = PNat.lcm n m
[PROOFSTEP]
have : u = n.factorMultiset := u.factorMultiset_prod.symm
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
this : u = PNat.factorMultiset n
⊢ prod (u ⊔ v) = PNat.lcm n m
[PROOFSTEP]
rw [this]
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
this : u = PNat.factorMultiset n
⊢ prod (PNat.factorMultiset n ⊔ v) = PNat.lcm n m
[PROOFSTEP]
have : v = m.factorMultiset := v.factorMultiset_prod.symm
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
this✝ : u = PNat.factorMultiset n
this : v = PNat.factorMultiset m
⊢ prod (PNat.factorMultiset n ⊔ v) = PNat.lcm n m
[PROOFSTEP]
rw [this]
[GOAL]
u v : PrimeMultiset
n : ℕ+ := prod u
m : ℕ+ := prod v
this✝ : u = PNat.factorMultiset n
this : v = PNat.factorMultiset m
⊢ prod (PNat.factorMultiset n ⊔ PNat.factorMultiset m) = PNat.lcm n m
[PROOFSTEP]
rw [← PNat.factorMultiset_lcm n m, PNat.prod_factorMultiset]
