a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
⊢ a ∣ b
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ (∀ (p : ℕ), p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p) ↔ a ∣ b
refine' ⟨fun h => _, fun hab p => ord_proj_dvd_ord_proj_of_dvd hb0 hab p⟩
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
⊢ factorization a ≤ factorization b
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
⊢ a ∣ b
rw [← factorization_le_iff_dvd ha0 hb0]
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
q : ℕ
⊢ ↑(factorization a) q ≤ ↑(factorization b) q
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
⊢ factorization a ≤ factorization b
intro q
case inl
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
q : ℕ
hq_le : q ≤ 1
⊢ ↑(factorization a) q ≤ ↑(factorization b) q

case inr
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
q : ℕ
hq1 : 1 < q
⊢ ↑(factorization a) q ≤ ↑(factorization b) q
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
q : ℕ
⊢ ↑(factorization a) q ≤ ↑(factorization b) q
rcases le_or_lt q 1 with (hq_le | hq1)
no goals
case inr
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
q : ℕ
hq1 : 1 < q
⊢ ↑(factorization a) q ≤ ↑(factorization b) q
exact (pow_dvd_pow_iff_le_right hq1).1 (h q)
no goals
case inl
a b : ℕ
ha0 : a ≠ 0
hb0 : b ≠ 0
h : ∀ (p : ℕ), p ^ ↑(factorization a) p ∣ p ^ ↑(factorization b) p
q : ℕ
hq_le : q ≤ 1
⊢ ↑(factorization a) q ≤ ↑(factorization b) q
interval_cases q <;> simp