case mp
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ factorization d ≤ factorization n → d ∣ n

case mpr
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d ∣ n → factorization d ≤ factorization n
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ factorization d ≤ factorization n ↔ d ∣ n
constructor
case mp
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
hdn : factorization d ≤ factorization n
⊢ d ∣ n
case mp
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ factorization d ≤ factorization n → d ∣ n
intro hdn
case mp
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
hdn : factorization d ≤ factorization n
K : ℕ →₀ ℕ := factorization n - factorization d
hK : K = factorization n - factorization d
⊢ d ∣ n
case mp
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
hdn : factorization d ≤ factorization n
⊢ d ∣ n
set K := n.factorization - d.factorization with hK
no goals
case mp
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
hdn : factorization d ≤ factorization n
K : ℕ →₀ ℕ := factorization n - factorization d
hK : K = factorization n - factorization d
⊢ n = d * Finsupp.prod K fun x x_1 => x ^ x_1
rw [← factorization_prod_pow_eq_self hn, ← factorization_prod_pow_eq_self hd,
    ←Finsupp.prod_add_index' pow_zero pow_add, hK, add_tsub_cancel_of_le hdn]
case mpr.intro
d : ℕ
hd : d ≠ 0
c : ℕ
hn : d * c ≠ 0
⊢ factorization d ≤ factorization (d * c)
case mpr
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d ∣ n → factorization d ≤ factorization n
rintro ⟨c, rfl⟩
case mpr.intro
d : ℕ
hd : d ≠ 0
c : ℕ
hn : d * c ≠ 0
⊢ factorization d ≤ factorization d + factorization c
case mpr.intro
d : ℕ
hd : d ≠ 0
c : ℕ
hn : d * c ≠ 0
⊢ factorization d ≤ factorization (d * c)
rw [factorization_mul hd (right_ne_zero_of_mul hn)]
no goals
case mpr.intro
d : ℕ
hd : d ≠ 0
c : ℕ
hn : d * c ≠ 0
⊢ factorization d ≤ factorization d + factorization c
simp