case a
v : PrimeMultiset
⊢ Coe.coe (PNat.factorMultiset (prod v)) = Coe.coe v
v : PrimeMultiset
⊢ PNat.factorMultiset (prod v) = v
apply PrimeMultiset.coeNat_injective
case a
v : PrimeMultiset
⊢ toNatMultiset (PNat.factorMultiset (prod v)) = toNatMultiset v
case a
v : PrimeMultiset
⊢ Coe.coe (PNat.factorMultiset (prod v)) = Coe.coe v
suffices toNatMultiset (PNat.factorMultiset (prod v)) = toNatMultiset v by exact this
case a
v : PrimeMultiset
⊢ ↑(Nat.factors (Multiset.prod (toNatMultiset v))) = toNatMultiset v
case a
v : PrimeMultiset
⊢ toNatMultiset (PNat.factorMultiset (prod v)) = toNatMultiset v
rw [v.prod.coeNat_factorMultiset, PrimeMultiset.coe_prod]
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)
case a
v : PrimeMultiset
⊢ ↑(Nat.factors (Multiset.prod (toNatMultiset v))) = toNatMultiset v
rcases v with ⟨l⟩
case a.mk
v : PrimeMultiset
l : List Nat.Primes
⊢ ↑(Nat.factors (Multiset.prod ↑(List.map Coe.coe l))) = ↑(List.map Coe.coe l)
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)
dsimp [PrimeMultiset.toNatMultiset]
case a.mk
v : PrimeMultiset
l : List Nat.Primes
⊢ ↑(Nat.factors (List.prod (List.map Coe.coe l))) = ↑(List.map Coe.coe l)
case a.mk
v : PrimeMultiset
l : List Nat.Primes
⊢ ↑(Nat.factors (Multiset.prod ↑(List.map Coe.coe l))) = ↑(List.map Coe.coe l)
rw [Multiset.coe_prod]
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)
case a.mk
v : PrimeMultiset
l : List Nat.Primes
⊢ ↑(Nat.factors (List.prod (List.map Coe.coe l))) = ↑(List.map Coe.coe l)
let l' := l.map (Coe.coe : Nat.Primes → ℕ)
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)
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)
have : ∀ p : ℕ, p ∈ l' → p.Prime := fun p hp => by
  rcases List.mem_map.mp hp with ⟨⟨_, hp'⟩, ⟨_, h_eq⟩⟩
  exact h_eq ▸ hp'
no goals
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)
exact Multiset.coe_eq_coe.mpr (@Nat.factors_unique _ l' rfl this).symm
no goals
v : PrimeMultiset
this : toNatMultiset (PNat.factorMultiset (prod v)) = toNatMultiset v
⊢ Coe.coe (PNat.factorMultiset (prod v)) = Coe.coe v
exact this
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
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map Coe.coe l
p : ℕ
hp : p ∈ l'
⊢ Nat.Prime p
rcases List.mem_map.mp hp with ⟨⟨_, hp'⟩, ⟨_, h_eq⟩⟩
no goals
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
exact h_eq ▸ hp'