case inl
p d : ℕ
hpd : ¬p ∣ d
hdn : d ∣ 0
⊢ d ∣ 0 / p ^ ↑(factorization 0) p

case inr
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : n ≠ 0
⊢ d ∣ n / p ^ ↑(factorization n) p
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
⊢ d ∣ n / p ^ ↑(factorization n) p
rcases eq_or_ne n 0 with (rfl | hn0)
case inr.inl
p n : ℕ
hn0 : n ≠ 0
hdn : 0 ∣ n
hpd : ¬p ∣ 0
⊢ 0 ∣ n / p ^ ↑(factorization n) p

case inr.inr
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : n ≠ 0
hd0 : d ≠ 0
⊢ d ∣ n / p ^ ↑(factorization n) p
case inr
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : n ≠ 0
⊢ d ∣ n / p ^ ↑(factorization n) p
rcases eq_or_ne d 0 with (rfl | hd0)
case inr.inr
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : n ≠ 0
hd0 : d ≠ 0
⊢ factorization d ≤ Finsupp.erase p (factorization n)
case inr.inr
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : n ≠ 0
hd0 : d ≠ 0
⊢ d ∣ n / p ^ ↑(factorization n) p
rw [← factorization_le_iff_dvd hd0 (ord_compl_pos p hn0).ne', factorization_ord_compl]
case inr.inr
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : n ≠ 0
hd0 : d ≠ 0
q : ℕ
⊢ ↑(factorization d) q ≤ ↑(Finsupp.erase p (factorization n)) q
case inr.inr
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : n ≠ 0
hd0 : d ≠ 0
⊢ factorization d ≤ Finsupp.erase p (factorization n)
intro q
case inr.inr.inl
d n : ℕ
hdn : d ∣ n
hn0 : n ≠ 0
hd0 : d ≠ 0
q : ℕ
hpd : ¬q ∣ d
⊢ ↑(factorization d) q ≤ ↑(Finsupp.erase q (factorization n)) q

case inr.inr.inr
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : n ≠ 0
hd0 : d ≠ 0
q : ℕ
hqp : q ≠ p
⊢ ↑(factorization d) q ≤ ↑(Finsupp.erase p (factorization n)) q
case inr.inr
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : n ≠ 0
hd0 : d ≠ 0
q : ℕ
⊢ ↑(factorization d) q ≤ ↑(Finsupp.erase p (factorization n)) q
rcases eq_or_ne q p with (rfl | hqp)
no goals
case inl
p d : ℕ
hpd : ¬p ∣ d
hdn : d ∣ 0
⊢ d ∣ 0 / p ^ ↑(factorization 0) p
simp
no goals
case inr.inl
p n : ℕ
hn0 : n ≠ 0
hdn : 0 ∣ n
hpd : ¬p ∣ 0
⊢ 0 ∣ n / p ^ ↑(factorization n) p
simp at hpd
no goals
case inr.inr.inl
d n : ℕ
hdn : d ∣ n
hn0 : n ≠ 0
hd0 : d ≠ 0
q : ℕ
hpd : ¬q ∣ d
⊢ ↑(factorization d) q ≤ ↑(Finsupp.erase q (factorization n)) q
simp [factorization_eq_zero_iff, hpd]
no goals
case inr.inr.inr
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : n ≠ 0
hd0 : d ≠ 0
q : ℕ
hqp : q ≠ p
⊢ ↑(factorization d) q ≤ ↑(Finsupp.erase p (factorization n)) q
simp [hqp, (factorization_le_iff_dvd hd0 hn0).2 hdn q]