case inl
p : ℕ
pp : Prime p
⊢ Icc 1 (↑(factorization 0) p) = Finset.filter (fun i => p ^ i ∣ 0) (Ico 1 0)

case inr
n p : ℕ
pp : Prime p
hn : n ≠ 0
⊢ Icc 1 (↑(factorization n) p) = Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n)
n p : ℕ
pp : Prime p
⊢ Icc 1 (↑(factorization n) p) = Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n)
rcases eq_or_ne n 0 with (rfl | hn)
case inr.a
n p : ℕ
pp : Prime p
hn : n ≠ 0
x : (fun x => ℕ) p
⊢ x ∈ Icc 1 (↑(factorization n) p) ↔ x ∈ Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n)
case inr
n p : ℕ
pp : Prime p
hn : n ≠ 0
⊢ Icc 1 (↑(factorization n) p) = Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n)
ext x
case inr.a
n p : ℕ
pp : Prime p
hn : n ≠ 0
x : (fun x => ℕ) p
⊢ 1 ≤ x → x ≤ ↑(factorization n) p → x < n
case inr.a
n p : ℕ
pp : Prime p
hn : n ≠ 0
x : (fun x => ℕ) p
⊢ x ∈ Icc 1 (↑(factorization n) p) ↔ x ∈ Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n)
simp only [mem_Icc, Finset.mem_filter, mem_Ico, and_assoc, and_congr_right_iff,
  pp.pow_dvd_iff_le_factorization hn, iff_and_self]
no goals
case inr.a
n p : ℕ
pp : Prime p
hn : n ≠ 0
x : (fun x => ℕ) p
⊢ 1 ≤ x → x ≤ ↑(factorization n) p → x < n
exact fun _ H => lt_of_le_of_lt H (factorization_lt p hn)
no goals
case inl
p : ℕ
pp : Prime p
⊢ Icc 1 (↑(factorization 0) p) = Finset.filter (fun i => p ^ i ∣ 0) (Ico 1 0)
simp