case inl
n : ℕ
h : 0 ∣ n
⊢ factorization (n / 0) = factorization n - factorization 0

case inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
⊢ factorization (n / d) = factorization n - factorization d
d n : ℕ
h : d ∣ n
⊢ factorization (n / d) = factorization n - factorization d
rcases eq_or_ne d 0 with (rfl | hd)
case inr.inl
d : ℕ
hd : d ≠ 0
h : d ∣ 0
⊢ factorization (0 / d) = factorization 0 - factorization d

case inr.inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ factorization (n / d) = factorization n - factorization d
case inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
⊢ factorization (n / d) = factorization n - factorization d
rcases eq_or_ne n 0 with (rfl | hn)
case inr.inr.a
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ (fun x => x + factorization d) (factorization (n / d)) =
    (fun x => x + factorization d) (factorization n - factorization d)
case inr.inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ factorization (n / d) = factorization n - factorization d
apply add_left_injective d.factorization
case inr.inr.a
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ factorization (n / d) + factorization d = factorization n - factorization d + factorization d
case inr.inr.a
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ (fun x => x + factorization d) (factorization (n / d)) =
    (fun x => x + factorization d) (factorization n - factorization d)
simp only
no goals
case inr.inr.a
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ factorization (n / d) + factorization d = factorization n - factorization d + factorization d
rw [tsub_add_cancel_of_le <| (Nat.factorization_le_iff_dvd hd hn).mpr h, ←
  Nat.factorization_mul (Nat.div_pos (Nat.le_of_dvd hn.bot_lt h) hd.bot_lt).ne' hd,
  Nat.div_mul_cancel h]
no goals
case inl
n : ℕ
h : 0 ∣ n
⊢ factorization (n / 0) = factorization n - factorization 0
simp [zero_dvd_iff.mp h]
no goals
case inr.inl
d : ℕ
hd : d ≠ 0
h : d ∣ 0
⊢ factorization (0 / d) = factorization 0 - factorization d
simp