case inl
p : ℕ
⊢ factorization (0 / p ^ ↑(factorization 0) p) = Finsupp.erase p (factorization 0)

case inr
n p : ℕ
hn : n ≠ 0
⊢ factorization (n / p ^ ↑(factorization n) p) = Finsupp.erase p (factorization n)
n p : ℕ
⊢ factorization (n / p ^ ↑(factorization n) p) = Finsupp.erase p (factorization n)
rcases eq_or_ne n 0 with (rfl | hn)
case pos
n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ factorization (n / p ^ ↑(factorization n) p) = Finsupp.erase p (factorization n)

case neg
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ factorization (n / p ^ ↑(factorization n) p) = Finsupp.erase p (factorization n)
case inr
n p : ℕ
hn : n ≠ 0
⊢ factorization (n / p ^ ↑(factorization n) p) = Finsupp.erase p (factorization n)
by_cases pp : p.Prime
case pos.h
n p : ℕ
hn : n ≠ 0
pp : Prime p
q : ℕ
⊢ ↑(factorization (n / p ^ ↑(factorization n) p)) q = ↑(Finsupp.erase p (factorization n)) q
case pos
n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ factorization (n / p ^ ↑(factorization n) p) = Finsupp.erase p (factorization n)
ext q
case pos.h.inl
n : ℕ
hn : n ≠ 0
q : ℕ
pp : Prime q
⊢ ↑(factorization (n / q ^ ↑(factorization n) q)) q = ↑(Finsupp.erase q (factorization n)) q

case pos.h.inr
n p : ℕ
hn : n ≠ 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ ↑(factorization (n / p ^ ↑(factorization n) p)) q = ↑(Finsupp.erase p (factorization n)) q
case pos.h
n p : ℕ
hn : n ≠ 0
pp : Prime p
q : ℕ
⊢ ↑(factorization (n / p ^ ↑(factorization n) p)) q = ↑(Finsupp.erase p (factorization n)) q
rcases eq_or_ne q p with (rfl | hqp)
no goals
case inl
p : ℕ
⊢ factorization (0 / p ^ ↑(factorization 0) p) = Finsupp.erase p (factorization 0)
simp
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ factorization (n / p ^ ↑(factorization n) p) = factorization n

n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ ¬p ∈ (factorization n).support
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ factorization (n / p ^ ↑(factorization n) p) = Finsupp.erase p (factorization n)
rw [Finsupp.erase_of_not_mem_support]
no goals
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ factorization (n / p ^ ↑(factorization n) p) = factorization n
simp [pp]
no goals
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ ¬p ∈ (factorization n).support
simp [mt prime_of_mem_factors pp]
case pos.h.inl
n : ℕ
hn : n ≠ 0
q : ℕ
pp : Prime q
⊢ ¬Prime q ∨ True ∨ n / q ^ ↑(factorization n) q = 0
case pos.h.inl
n : ℕ
hn : n ≠ 0
q : ℕ
pp : Prime q
⊢ ↑(factorization (n / q ^ ↑(factorization n) q)) q = ↑(Finsupp.erase q (factorization n)) q
simp only [Finsupp.erase_same, factorization_eq_zero_iff, not_dvd_ord_compl pp hn]
no goals
case pos.h.inl
n : ℕ
hn : n ≠ 0
q : ℕ
pp : Prime q
⊢ ¬Prime q ∨ True ∨ n / q ^ ↑(factorization n) q = 0
simp
case pos.h.inr
n p : ℕ
hn : n ≠ 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ ↑(factorization n - factorization (p ^ ↑(factorization n) p)) q = ↑(factorization n) q
case pos.h.inr
n p : ℕ
hn : n ≠ 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ ↑(factorization (n / p ^ ↑(factorization n) p)) q = ↑(Finsupp.erase p (factorization n)) q
rw [Finsupp.erase_ne hqp, factorization_div (ord_proj_dvd n p)]
no goals
case pos.h.inr
n p : ℕ
hn : n ≠ 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ ↑(factorization n - factorization (p ^ ↑(factorization n) p)) q = ↑(factorization n) q
simp [pp.factorization, hqp.symm]