d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
⊢ factorization (n / d) = factorization n - factorization d → d ∣ n
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
⊢ d ∣ n ↔ factorization (n / d) = factorization n - factorization d
refine' ⟨factorization_div, _⟩
case inl
d : ℕ
hd : d ≠ 0
hdn : d ≤ d
⊢ factorization (d / d) = factorization d - factorization d → d ∣ d

case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
⊢ factorization (n / d) = factorization n - factorization d → d ∣ n
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
⊢ factorization (n / d) = factorization n - factorization d → d ∣ n
rcases eq_or_lt_of_le hdn with (rfl | hd_lt_n)
case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
⊢ factorization (n / d) = factorization n - factorization d → d ∣ n
case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
⊢ factorization (n / d) = factorization n - factorization d → d ∣ n
have h1 : n / d ≠ 0 := fun H => Nat.lt_asymm hd_lt_n ((Nat.div_eq_zero_iff hd.bot_lt).mp H)
case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
h : factorization (n / d) = factorization n - factorization d
⊢ d ∣ n
case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
⊢ factorization (n / d) = factorization n - factorization d → d ∣ n
intro h
case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
h : factorization (n / d) = factorization n - factorization d
⊢ n ≤ n / d * d
case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
h : factorization (n / d) = factorization n - factorization d
⊢ d ∣ n
rw [dvd_iff_le_div_mul n d]
case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
h : factorization (n / d) = factorization n - factorization d
h2 : ¬n ≤ n / d * d
⊢ False
case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
h : factorization (n / d) = factorization n - factorization d
⊢ n ≤ n / d * d
by_contra h2
case inr.intro
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
h : factorization (n / d) = factorization n - factorization d
h2 : ¬n ≤ n / d * d
p : ℕ
hp : ↑(factorization (n / d * d)) p < ↑(factorization n) p
⊢ False
case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
h : factorization (n / d) = factorization n - factorization d
h2 : ¬n ≤ n / d * d
⊢ False
cases' exists_factorization_lt_of_lt (mul_ne_zero h1 hd) (not_le.mp h2) with p hp
no goals
case inr.intro
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
h : factorization (n / d) = factorization n - factorization d
h2 : ¬n ≤ n / d * d
p : ℕ
hp : ↑(factorization (n / d * d)) p < ↑(factorization n) p
⊢ False
rwa [factorization_mul h1 hd, add_apply, ← lt_tsub_iff_right, h, tsub_apply,
 lt_self_iff_false] at hp
no goals
case inl
d : ℕ
hd : d ≠ 0
hdn : d ≤ d
⊢ factorization (d / d) = factorization d - factorization d → d ∣ d
simp