-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem ordCompl_dvd_ordCompl_of_dvd {a b : ℕ} (hab : a ∣ b) (p : ℕ) :
    ordCompl[p] a ∣ ordCompl[p] b

Proof state:
case inr.inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
q : ℕ
hqp : q ≠ p
⊢ a.factorization q ≤ b.factorization q

Tactic:
exact (factorization_le_iff_dvd ha0 hb0).2 hab q

Result:
no goals

Proof state:
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

Tactic:
have ha := (Nat.div_pos (ordProj_le p ha0) (ordProj_pos a p)).ne'

Result:
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

Proof state:
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

Tactic:
have hb := (Nat.div_pos (ordProj_le p hb0) (ordProj_pos b p)).ne'

Result:
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

Proof state:
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

Tactic:
rw [← factorization_le_iff_dvd ha hb, factorization_ordCompl a p, factorization_ordCompl b p]

Result:
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
⊢ Finsupp.erase p a.factorization ≤ Finsupp.erase p b.factorization

Proof state:
case inr.inr.inl
b p : ℕ
pp : Prime p
hb0 : b ≠ 0
hab : 0 ∣ b
⊢ 0 / p ^ (factorization 0) p ∣ b / p ^ b.factorization p

Tactic:
cases hb0 (zero_dvd_iff.1 hab)

Result:
no goals

Proof state:
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
⊢ Finsupp.erase p a.factorization ≤ Finsupp.erase p b.factorization

Tactic:
intro q

Result:
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
q : ℕ
⊢ (Finsupp.erase p a.factorization) q ≤ (Finsupp.erase p b.factorization) q

Proof state:
case inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

Tactic:
rcases eq_or_ne a 0 with (rfl | ha0)

Result:
case inr.inr.inl
b p : ℕ
pp : Prime p
hb0 : b ≠ 0
hab : 0 ∣ b
⊢ 0 / p ^ (factorization 0) p ∣ b / p ^ b.factorization p

case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

Proof state:
case inr.inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
q : ℕ
hqp : q ≠ p
⊢ (Finsupp.erase p a.factorization) q ≤ (Finsupp.erase p b.factorization) q

Tactic:
simp_rw [erase_ne hqp]

Result:
case inr.inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
q : ℕ
hqp : q ≠ p
⊢ a.factorization q ≤ b.factorization q

Proof state:
case inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

Tactic:
rcases eq_or_ne b 0 with (rfl | hb0)

Result:
case inr.inl
a p : ℕ
pp : Prime p
hab : a ∣ 0
⊢ a / p ^ a.factorization p ∣ 0 / p ^ (factorization 0) p

case inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

Proof state:
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
q : ℕ
⊢ (Finsupp.erase p a.factorization) q ≤ (Finsupp.erase p b.factorization) q

Tactic:
rcases eq_or_ne q p with (rfl | hqp)

Result:
case inr.inr.inr.inl
a b : ℕ
hab : a ∣ b
hb0 : b ≠ 0
ha0 : a ≠ 0
q : ℕ
pp : Prime q
ha : a / q ^ a.factorization q ≠ 0
hb : b / q ^ b.factorization q ≠ 0
⊢ (Finsupp.erase q a.factorization) q ≤ (Finsupp.erase q b.factorization) q

case inr.inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
q : ℕ
hqp : q ≠ p
⊢ (Finsupp.erase p a.factorization) q ≤ (Finsupp.erase p b.factorization) q

Proof state:
case inl
a b : ℕ
hab : a ∣ b
p : ℕ
pp : ¬Prime p
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

Tactic:
simp [pp, hab]

Result:
no goals

Proof state:
case inr.inr.inr.inl
a b : ℕ
hab : a ∣ b
hb0 : b ≠ 0
ha0 : a ≠ 0
q : ℕ
pp : Prime q
ha : a / q ^ a.factorization q ≠ 0
hb : b / q ^ b.factorization q ≠ 0
⊢ (Finsupp.erase q a.factorization) q ≤ (Finsupp.erase q b.factorization) q

Tactic:
simp

Result:
no goals

Proof state:
a b : ℕ
hab : a ∣ b
p : ℕ
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

Tactic:
rcases em' p.Prime with (pp | pp)

Result:
case inl
a b : ℕ
hab : a ∣ b
p : ℕ
pp : ¬Prime p
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

case inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

Proof state:
case inr.inl
a p : ℕ
pp : Prime p
hab : a ∣ 0
⊢ a / p ^ a.factorization p ∣ 0 / p ^ (factorization 0) p

Tactic:
simp

Result:
no goals