-- Mathlib/Data/PNat/Factors.lean
theorem factorMultiset_prod (v : PrimeMultiset) : v.prod.factorMultiset = v

Proof state:
case a.mk
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map Coe.coe l
⊢ ↑(List.map Coe.coe l).prod.primeFactorsList = ↑(List.map Coe.coe l)

Tactic:
have : ∀ p : ℕ, p ∈ l' → p.Prime := fun p hp => by
  rcases List.mem_map.mp hp with ⟨⟨_, hp'⟩, ⟨_, h_eq⟩⟩
  exact h_eq ▸ hp'

Result:
case a.mk
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map Coe.coe l
this : ∀ p ∈ l', Nat.Prime p
⊢ ↑(List.map Coe.coe l).prod.primeFactorsList = ↑(List.map Coe.coe l)

Proof state:
case a
v : PrimeMultiset
⊢ v.prod.factorMultiset.toNatMultiset = v.toNatMultiset

Tactic:
rw [v.prod.coeNat_factorMultiset, PrimeMultiset.coe_prod]

Result:
case a
v : PrimeMultiset
⊢ ↑v.toNatMultiset.prod.primeFactorsList = v.toNatMultiset

Proof state:
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map Coe.coe l
p : ℕ
hp : p ∈ l'
⊢ Nat.Prime p

Tactic:
rcases List.mem_map.mp hp with ⟨⟨_, hp'⟩, ⟨_, h_eq⟩⟩

Result:
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✝, hp'⟩ ∈ l
h_eq : Coe.coe ⟨val✝, hp'⟩ = p
⊢ Nat.Prime p

Proof state:
case a.mk
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map Coe.coe l
this : ∀ p ∈ l', Nat.Prime p
⊢ ↑(List.map Coe.coe l).prod.primeFactorsList = ↑(List.map Coe.coe l)

Tactic:
exact Multiset.coe_eq_coe.mpr (@Nat.primeFactorsList_unique _ l' rfl this).symm

Result:
no goals

Proof state:
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✝, hp'⟩ ∈ l
h_eq : Coe.coe ⟨val✝, hp'⟩ = p
⊢ Nat.Prime p

Tactic:
exact h_eq ▸ hp'

Result:
no goals

Proof state:
case a.mk
v : PrimeMultiset
l : List Nat.Primes
⊢ ↑(toNatMultiset (Quot.mk (⇑(List.isSetoid Nat.Primes)) l)).prod.primeFactorsList =
    toNatMultiset (Quot.mk (⇑(List.isSetoid Nat.Primes)) l)

Tactic:
dsimp [PrimeMultiset.toNatMultiset]

Result:
case a.mk
v : PrimeMultiset
l : List Nat.Primes
⊢ ↑(List.map Coe.coe l).prod.primeFactorsList = ↑(List.map Coe.coe l)

Proof state:
v : PrimeMultiset
this : v.prod.factorMultiset.toNatMultiset = v.toNatMultiset
⊢ Coe.coe v.prod.factorMultiset = Coe.coe v

Tactic:
exact this

Result:
no goals

Proof state:
case a
v : PrimeMultiset
⊢ ↑v.toNatMultiset.prod.primeFactorsList = v.toNatMultiset

Tactic:
rcases v with ⟨l⟩

Result:
case a.mk
v : PrimeMultiset
l : List Nat.Primes
⊢ ↑(toNatMultiset (Quot.mk (⇑(List.isSetoid Nat.Primes)) l)).prod.primeFactorsList =
    toNatMultiset (Quot.mk (⇑(List.isSetoid Nat.Primes)) l)

Proof state:
case a
v : PrimeMultiset
⊢ Coe.coe v.prod.factorMultiset = Coe.coe v

Tactic:
suffices toNatMultiset (PNat.factorMultiset (prod v)) = toNatMultiset v by exact this

Result:
case a
v : PrimeMultiset
⊢ v.prod.factorMultiset.toNatMultiset = v.toNatMultiset

Proof state:
v : PrimeMultiset
⊢ v.prod.factorMultiset = v

Tactic:
apply PrimeMultiset.coeNat_injective

Result:
case a
v : PrimeMultiset
⊢ Coe.coe v.prod.factorMultiset = Coe.coe v

Proof state:
case a.mk
v : PrimeMultiset
l : List Nat.Primes
⊢ ↑(List.map Coe.coe l).prod.primeFactorsList = ↑(List.map Coe.coe l)

Tactic:
let l' := l.map (Coe.coe : Nat.Primes → ℕ)

Result:
case a.mk
v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map Coe.coe l
⊢ ↑(List.map Coe.coe l).prod.primeFactorsList = ↑(List.map Coe.coe l)