case inl
a b : ℕ
hab : a ∣ b
p : ℕ
pp : ¬Prime p
⊢ a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p

case inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
⊢ a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
a b : ℕ
hab : a ∣ b
p : ℕ
⊢ a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
rcases em' p.Prime with (pp | pp)
case inr.inl
a p : ℕ
pp : Prime p
hab : a ∣ 0
⊢ a / p ^ ↑(factorization a) p ∣ 0 / p ^ ↑(factorization 0) p

case inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
⊢ a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
case inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
⊢ a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
rcases eq_or_ne b 0 with (rfl | hb0)
case inr.inr.inl
b p : ℕ
pp : Prime p
hb0 : b ≠ 0
hab : 0 ∣ b
⊢ 0 / p ^ ↑(factorization 0) p ∣ b / p ^ ↑(factorization b) p

case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
⊢ a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
case inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
⊢ a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
rcases eq_or_ne a 0 with (rfl | ha0)
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ ↑(factorization a) p ≠ 0
⊢ a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
⊢ a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
have ha := (Nat.div_pos (ord_proj_le p ha0) (ord_proj_pos a p)).ne'
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ ↑(factorization a) p ≠ 0
hb : b / p ^ ↑(factorization b) p ≠ 0
⊢ a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ ↑(factorization a) p ≠ 0
⊢ a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
have hb := (Nat.div_pos (ord_proj_le p hb0) (ord_proj_pos b p)).ne'
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ ↑(factorization a) p ≠ 0
hb : b / p ^ ↑(factorization b) p ≠ 0
⊢ Finsupp.erase p (factorization a) ≤ Finsupp.erase p (factorization b)
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ ↑(factorization a) p ≠ 0
hb : b / p ^ ↑(factorization b) p ≠ 0
⊢ a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
rw [← factorization_le_iff_dvd ha hb, factorization_ord_compl a p, factorization_ord_compl b p]
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ ↑(factorization a) p ≠ 0
hb : b / p ^ ↑(factorization b) p ≠ 0
q : ℕ
⊢ ↑(Finsupp.erase p (factorization a)) q ≤ ↑(Finsupp.erase p (factorization b)) q
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ ↑(factorization a) p ≠ 0
hb : b / p ^ ↑(factorization b) p ≠ 0
⊢ Finsupp.erase p (factorization a) ≤ Finsupp.erase p (factorization b)
intro q
case inr.inr.inr.inl
a b : ℕ
hab : a ∣ b
hb0 : b ≠ 0
ha0 : a ≠ 0
q : ℕ
pp : Prime q
ha : a / q ^ ↑(factorization a) q ≠ 0
hb : b / q ^ ↑(factorization b) q ≠ 0
⊢ ↑(Finsupp.erase q (factorization a)) q ≤ ↑(Finsupp.erase q (factorization b)) q

case inr.inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ ↑(factorization a) p ≠ 0
hb : b / p ^ ↑(factorization b) p ≠ 0
q : ℕ
hqp : q ≠ p
⊢ ↑(Finsupp.erase p (factorization a)) q ≤ ↑(Finsupp.erase p (factorization b)) q
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ ↑(factorization a) p ≠ 0
hb : b / p ^ ↑(factorization b) p ≠ 0
q : ℕ
⊢ ↑(Finsupp.erase p (factorization a)) q ≤ ↑(Finsupp.erase p (factorization b)) q
rcases eq_or_ne q p with (rfl | hqp)
case inr.inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ ↑(factorization a) p ≠ 0
hb : b / p ^ ↑(factorization b) p ≠ 0
q : ℕ
hqp : q ≠ p
⊢ ↑(factorization a) q ≤ ↑(factorization b) q
case inr.inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ ↑(factorization a) p ≠ 0
hb : b / p ^ ↑(factorization b) p ≠ 0
q : ℕ
hqp : q ≠ p
⊢ ↑(Finsupp.erase p (factorization a)) q ≤ ↑(Finsupp.erase p (factorization b)) q
simp_rw [erase_ne hqp]
no goals
case inr.inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ ↑(factorization a) p ≠ 0
hb : b / p ^ ↑(factorization b) p ≠ 0
q : ℕ
hqp : q ≠ p
⊢ ↑(factorization a) q ≤ ↑(factorization b) q
exact (factorization_le_iff_dvd ha0 hb0).2 hab q
no goals
case inl
a b : ℕ
hab : a ∣ b
p : ℕ
pp : ¬Prime p
⊢ a / p ^ ↑(factorization a) p ∣ b / p ^ ↑(factorization b) p
simp [pp, hab]
no goals
case inr.inl
a p : ℕ
pp : Prime p
hab : a ∣ 0
⊢ a / p ^ ↑(factorization a) p ∣ 0 / p ^ ↑(factorization 0) p
simp
no goals
case inr.inr.inl
b p : ℕ
pp : Prime p
hb0 : b ≠ 0
hab : 0 ∣ b
⊢ 0 / p ^ ↑(factorization 0) p ∣ b / p ^ ↑(factorization b) p
cases hb0 (zero_dvd_iff.1 hab)
no goals
case inr.inr.inr.inl
a b : ℕ
hab : a ∣ b
hb0 : b ≠ 0
ha0 : a ≠ 0
q : ℕ
pp : Prime q
ha : a / q ^ ↑(factorization a) q ≠ 0
hb : b / q ^ ↑(factorization b) q ≠ 0
⊢ ↑(Finsupp.erase q (factorization a)) q ≤ ↑(Finsupp.erase q (factorization b)) q
simp