case pos
n✝ n : ℕ
hn : n = 0
⊢ image (fun x => n / x) (divisors n) = divisors n

case neg
n✝ n : ℕ
hn : ¬n = 0
⊢ image (fun x => n / x) (divisors n) = divisors n
n✝ n : ℕ
⊢ image (fun x => n / x) (divisors n) = divisors n
by_cases hn : n = 0
case neg.a
n✝ n : ℕ
hn : ¬n = 0
a : ℕ
⊢ a ∈ image (fun x => n / x) (divisors n) ↔ a ∈ divisors n
case neg
n✝ n : ℕ
hn : ¬n = 0
⊢ image (fun x => n / x) (divisors n) = divisors n
ext a
case neg.a.mp
n✝ n : ℕ
hn : ¬n = 0
a : ℕ
⊢ a ∈ image (fun x => n / x) (divisors n) → a ∈ divisors n

case neg.a.mpr
n✝ n : ℕ
hn : ¬n = 0
a : ℕ
⊢ a ∈ divisors n → a ∈ image (fun x => n / x) (divisors n)
case neg.a
n✝ n : ℕ
hn : ¬n = 0
a : ℕ
⊢ a ∈ image (fun x => n / x) (divisors n) ↔ a ∈ divisors n
constructor
no goals
case pos
n✝ n : ℕ
hn : n = 0
⊢ image (fun x => n / x) (divisors n) = divisors n
simp [hn]
case neg.a.mp
n✝ n : ℕ
hn : ¬n = 0
a : ℕ
⊢ (∃ a_1, a_1 ∈ divisors n ∧ n / a_1 = a) → a ∈ divisors n
case neg.a.mp
n✝ n : ℕ
hn : ¬n = 0
a : ℕ
⊢ a ∈ image (fun x => n / x) (divisors n) → a ∈ divisors n
rw [mem_image]
case neg.a.mp.intro.intro
n✝ n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∈ divisors n
hx2 : n / x = a
⊢ a ∈ divisors n
case neg.a.mp
n✝ n : ℕ
hn : ¬n = 0
a : ℕ
⊢ (∃ a_1, a_1 ∈ divisors n ∧ n / a_1 = a) → a ∈ divisors n
rintro ⟨x, hx1, hx2⟩
case neg.a.mp.intro.intro
n✝ n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∣ n ∧ n ≠ 0
hx2 : n / x = a
⊢ a ∣ n ∧ n ≠ 0
case neg.a.mp.intro.intro
n✝ n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∈ divisors n
hx2 : n / x = a
⊢ a ∈ divisors n
rw [mem_divisors] at *
case neg.a.mp.intro.intro
n✝ n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∣ n ∧ n ≠ 0
hx2 : n / x = a
⊢ a ∣ n
case neg.a.mp.intro.intro
n✝ n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∣ n ∧ n ≠ 0
hx2 : n / x = a
⊢ a ∣ n ∧ n ≠ 0
refine' ⟨_, hn⟩
case neg.a.mp.intro.intro
n✝ n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∣ n ∧ n ≠ 0
hx2 : n / x = a
⊢ n / x ∣ n
case neg.a.mp.intro.intro
n✝ n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∣ n ∧ n ≠ 0
hx2 : n / x = a
⊢ a ∣ n
rw [← hx2]
no goals
case neg.a.mp.intro.intro
n✝ n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∣ n ∧ n ≠ 0
hx2 : n / x = a
⊢ n / x ∣ n
exact div_dvd_of_dvd hx1.1
case neg.a.mpr
n✝ n : ℕ
hn : ¬n = 0
a : ℕ
⊢ a ∣ n ∧ n ≠ 0 → ∃ a_2, a_2 ∈ divisors n ∧ n / a_2 = a
case neg.a.mpr
n✝ n : ℕ
hn : ¬n = 0
a : ℕ
⊢ a ∈ divisors n → a ∈ image (fun x => n / x) (divisors n)
rw [mem_divisors, mem_image]
case neg.a.mpr.intro
n✝ n : ℕ
hn : ¬n = 0
a : ℕ
h1 : a ∣ n
⊢ ∃ a_1, a_1 ∈ divisors n ∧ n / a_1 = a
case neg.a.mpr
n✝ n : ℕ
hn : ¬n = 0
a : ℕ
⊢ a ∣ n ∧ n ≠ 0 → ∃ a_2, a_2 ∈ divisors n ∧ n / a_2 = a
rintro ⟨h1, -⟩
no goals
case neg.a.mpr.intro
n✝ n : ℕ
hn : ¬n = 0
a : ℕ
h1 : a ∣ n
⊢ ∃ a_1, a_1 ∈ divisors n ∧ n / a_1 = a
exact ⟨n / a, mem_divisors.mpr ⟨div_dvd_of_dvd h1, hn⟩, Nat.div_div_self h1 hn⟩