case inl
b p : ℕ
⊢ 0 * b / p ^ ↑(factorization (0 * b)) p = 0 / p ^ ↑(factorization 0) p * (b / p ^ ↑(factorization b) p)

case inr
a b p : ℕ
ha : a ≠ 0
⊢ a * b / p ^ ↑(factorization (a * b)) p = a / p ^ ↑(factorization a) p * (b / p ^ ↑(factorization b) p)
a b p : ℕ
⊢ a * b / p ^ ↑(factorization (a * b)) p = a / p ^ ↑(factorization a) p * (b / p ^ ↑(factorization b) p)
rcases eq_or_ne a 0 with (rfl | ha)
case inr.inl
a p : ℕ
ha : a ≠ 0
⊢ a * 0 / p ^ ↑(factorization (a * 0)) p = a / p ^ ↑(factorization a) p * (0 / p ^ ↑(factorization 0) p)

case inr.inr
a b p : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b / p ^ ↑(factorization (a * b)) p = a / p ^ ↑(factorization a) p * (b / p ^ ↑(factorization b) p)
case inr
a b p : ℕ
ha : a ≠ 0
⊢ a * b / p ^ ↑(factorization (a * b)) p = a / p ^ ↑(factorization a) p * (b / p ^ ↑(factorization b) p)
rcases eq_or_ne b 0 with (rfl | hb)
case inr.inr
a b p : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b / (p ^ ↑(factorization a) p * p ^ ↑(factorization b) p) =
    a / p ^ ↑(factorization a) p * (b / p ^ ↑(factorization b) p)
case inr.inr
a b p : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b / p ^ ↑(factorization (a * b)) p = a / p ^ ↑(factorization a) p * (b / p ^ ↑(factorization b) p)
simp only [ord_proj_mul p ha hb]
no goals
case inr.inr
a b p : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b / (p ^ ↑(factorization a) p * p ^ ↑(factorization b) p) =
    a / p ^ ↑(factorization a) p * (b / p ^ ↑(factorization b) p)
rw [mul_div_mul_comm_of_dvd_dvd (ord_proj_dvd a p) (ord_proj_dvd b p)]
no goals
case inl
b p : ℕ
⊢ 0 * b / p ^ ↑(factorization (0 * b)) p = 0 / p ^ ↑(factorization 0) p * (b / p ^ ↑(factorization b) p)
simp
no goals
case inr.inl
a p : ℕ
ha : a ≠ 0
⊢ a * 0 / p ^ ↑(factorization (a * 0)) p = a / p ^ ↑(factorization a) p * (0 / p ^ ↑(factorization 0) p)
simp