-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem ordCompl_dvd_ordCompl_iff_dvd (a b : ℕ) :
    (∀ p : ℕ, ordCompl[p] a ∣ ordCompl[p] b) ↔ a ∣ b

Proof state:
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : ¬Prime a
⊢ a ∣ b

Tactic:
simpa [pa] using h a

Result:
no goals

Proof state:
case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ b * a ∣ b

Tactic:
simpa [Prime.factorization_self pb, Prime.factorization pa, hab] using h b

Result:
no goals

Proof state:
case inl
a : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ 0 / p ^ (factorization 0) p
⊢ a ∣ 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
⊢ a = b

Tactic:
by_contra hab

Result:
case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ False

Proof state:
case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
⊢ a ∣ b

Tactic:
if pb : b.Prime then ?_ else simpa [pb] using h b

Result:
case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
⊢ a ∣ b

Proof state:
case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ False

Tactic:
apply pa.ne_one

Result:
case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ a = 1

Proof state:
case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
⊢ a ∣ b

Tactic:
if pa : a.Prime then ?_ else simpa [pa] using h a

Result:
case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
⊢ a ∣ b

Proof state:
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : ¬Prime b
⊢ a ∣ b

Tactic:
simpa [pb] using h b

Result:
no goals

Proof state:
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
⊢ a ∣ b

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

Result:
case inl
a : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ 0 / p ^ (factorization 0) p
⊢ a ∣ 0

case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
⊢ a ∣ b

Proof state:
case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
⊢ a ∣ b

Tactic:
rw [prime_dvd_prime_iff_eq pa pb]

Result:
case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
⊢ a = b

Proof state:
case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ a = 1

Tactic:
rw [← Nat.dvd_one, ← Nat.mul_dvd_mul_iff_left hb0.bot_lt, mul_one]

Result:
case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ b * a ∣ b

Proof state:
a b : ℕ
⊢ (∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p) ↔ a ∣ b

Tactic:
refine ⟨fun h => ?_, fun hab p => ordCompl_dvd_ordCompl_of_dvd hab p⟩

Result:
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
⊢ a ∣ b