case refine_1
n : ℕ
⊢ properDivisors n = {1} → Prime n

case refine_2
n : ℕ
⊢ Prime n → properDivisors n = {1}
n : ℕ
⊢ properDivisors n = {1} ↔ Prime n
refine ⟨?_, ?_⟩
case refine_1
n : ℕ
h : properDivisors n = {1}
⊢ Prime n
case refine_1
n : ℕ
⊢ properDivisors n = {1} → Prime n
intro h
case refine_1.refine'_1
n : ℕ
h : properDivisors n = {1}
⊢ 2 ≤ n

case refine_1.refine'_2
n : ℕ
h : properDivisors n = {1}
m : ℕ
hdvd : m ∣ n
⊢ m = 1 ∨ m = n
case refine_1
n : ℕ
h : properDivisors n = {1}
⊢ Prime n
refine' Nat.prime_def_lt''.mpr ⟨_, fun m hdvd => _⟩
no goals
case refine_1.refine'_1
n : ℕ
h : properDivisors n = {1}
⊢ 2 ≤ n
match n with
| 0 => contradiction
| 1 => contradiction
| Nat.succ (Nat.succ n) => simp [succ_le_succ]
no goals
n : ℕ
h : properDivisors 0 = {1}
⊢ 2 ≤ 0
contradiction
no goals
n : ℕ
h : properDivisors 1 = {1}
⊢ 2 ≤ 1
contradiction
no goals
n✝ n : ℕ
h : properDivisors (succ (succ n)) = {1}
⊢ 2 ≤ succ (succ n)
simp [succ_le_succ]
case refine_1.refine'_2
n : ℕ
h : properDivisors n = {1}
m : ℕ
hdvd : m ∣ n
⊢ m ∣ n ∧ m < n ∨ m = n
case refine_1.refine'_2
n : ℕ
h : properDivisors n = {1}
m : ℕ
hdvd : m ∣ n
⊢ m = 1 ∨ m = n
rw [← mem_singleton, ← h, mem_properDivisors]
case refine_1.refine'_2.refine_2
n : ℕ
h : properDivisors n = {1}
m : ℕ
hdvd : m ∣ n
this : m ≤ n
⊢ m ∣ n ∧ m < n ∨ m = n

case refine_1.refine'_2.refine_1
n : ℕ
h : properDivisors n = {1}
m : ℕ
hdvd : m ∣ n
⊢ 0 < n
case refine_1.refine'_2
n : ℕ
h : properDivisors n = {1}
m : ℕ
hdvd : m ∣ n
⊢ m ∣ n ∧ m < n ∨ m = n
have := Nat.le_of_dvd ?_ hdvd
case refine_1.refine'_2.refine_2
n : ℕ
h : properDivisors n = {1}
m : ℕ
hdvd : m ∣ n
this : m ≤ n
⊢ m < n ∨ m = n
case refine_1.refine'_2.refine_2
n : ℕ
h : properDivisors n = {1}
m : ℕ
hdvd : m ∣ n
this : m ≤ n
⊢ m ∣ n ∧ m < n ∨ m = n
simp [hdvd, this]
no goals
case refine_1.refine'_2.refine_2
n : ℕ
h : properDivisors n = {1}
m : ℕ
hdvd : m ∣ n
this : m ≤ n
⊢ m < n ∨ m = n
exact (le_iff_eq_or_lt.mp this).symm
case refine_1.refine'_2.refine_1
n : ℕ
h : properDivisors n = {1}
m : ℕ
hdvd : m ∣ n
this : n ≤ 0
⊢ False
case refine_1.refine'_2.refine_1
n : ℕ
h : properDivisors n = {1}
m : ℕ
hdvd : m ∣ n
⊢ 0 < n
by_contra'
no goals
case refine_1.refine'_2.refine_1
n : ℕ
h : properDivisors n = {1}
m : ℕ
hdvd : m ∣ n
this : n ≤ 0
⊢ False
simp [nonpos_iff_eq_zero.mp this, this] at h
no goals
case refine_2
n : ℕ
⊢ Prime n → properDivisors n = {1}
exact fun h => Prime.properDivisors h