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

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

case inr.inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
ha0 : a ≠ 0
⊢ p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
case inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
⊢ p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
rcases eq_or_ne a 0 with (rfl | ha0)
case inr.inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
ha0 : a ≠ 0
⊢ ↑(factorization a) p ≤ ↑(factorization b) p
case inr.inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
ha0 : a ≠ 0
⊢ p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
rw [pow_dvd_pow_iff_le_right pp.one_lt]
no goals
case inr.inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
ha0 : a ≠ 0
⊢ ↑(factorization a) p ≤ ↑(factorization b) p
exact (factorization_le_iff_dvd ha0 hb0).2 hab p
no goals
case inl
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : ¬Prime p
⊢ p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
simp [pp]
no goals
case inr.inl
b : ℕ
hb0 : b ≠ 0
p : ℕ
pp : Prime p
hab : 0 ∣ b
⊢ p ^ ↑(factorization 0) p ∣ p ^ ↑(factorization b) p
simp