case a
n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∈ filter (fun x => x ∣ n) (range (succ n)) ↔ a✝ ∈ divisors n
n : ℕ
h : n ≠ 0
⊢ filter (fun x => x ∣ n) (range (succ n)) = divisors n
ext
case a
n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∣ n → a✝ < succ n → 1 ≤ a✝
case a
n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∈ filter (fun x => x ∣ n) (range (succ n)) ↔ a✝ ∈ divisors n
simp only [divisors, mem_filter, mem_range, mem_Ico, and_congr_left_iff, iff_and_self]
no goals
case a
n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∣ n → a✝ < succ n → 1 ≤ a✝
exact fun ha _ => succ_le_iff.mpr (pos_of_dvd_of_pos ha h.bot_lt)