R : Type ?u.553341
n : ℕ
h : ↑Ω n = 1
⊢ Prime n
R : Type ?u.553341
n : ℕ
⊢ ↑Ω n = 1 ↔ Prime n
refine' ⟨fun h => _, fun h => List.length_eq_one.2 ⟨n, factors_prime h⟩⟩
case zero
R : Type ?u.553341
h : ↑Ω Nat.zero = 1
⊢ Prime Nat.zero

case succ
R : Type ?u.553341
n✝ : ℕ
h : ↑Ω (succ n✝) = 1
⊢ Prime (succ n✝)
R : Type ?u.553341
n : ℕ
h : ↑Ω n = 1
⊢ Prime n
cases n
case succ
R : Type ?u.553341
n : ℕ
h : ↑Ω (succ n) = 1
⊢ Prime (succ n)
case succ
R : Type ?u.553341
n✝ : ℕ
h : ↑Ω (succ n✝) = 1
⊢ Prime (succ n✝)
rename_i n
case succ.intro
R : Type ?u.553341
n : ℕ
h : ↑Ω (succ n) = 1
x : ℕ
hx : factors (succ n) = [x]
⊢ Prime (succ n)
case succ
R : Type ?u.553341
n : ℕ
h : ↑Ω (succ n) = 1
⊢ Prime (succ n)
rcases List.length_eq_one.1 h with ⟨x, hx⟩
case succ.intro
R : Type ?u.553341
n : ℕ
h : ↑Ω (succ n) = 1
x : ℕ
hx : factors (succ n) = [x]
⊢ Prime x
case succ.intro
R : Type ?u.553341
n : ℕ
h : ↑Ω (succ n) = 1
x : ℕ
hx : factors (succ n) = [x]
⊢ Prime (succ n)
rw [← prod_factors n.succ_ne_zero, hx, List.prod_singleton]
case succ.intro.h
R : Type ?u.553341
n : ℕ
h : ↑Ω (succ n) = 1
x : ℕ
hx : factors (succ n) = [x]
⊢ x ∈ factors ?succ.intro.n

case succ.intro.n
R : Type ?u.553341
n : ℕ
h : ↑Ω (succ n) = 1
x : ℕ
hx : factors (succ n) = [x]
⊢ ℕ
case succ.intro
R : Type ?u.553341
n : ℕ
h : ↑Ω (succ n) = 1
x : ℕ
hx : factors (succ n) = [x]
⊢ Prime x
apply prime_of_mem_factors
no goals
case succ.intro.h
R : Type ?u.553341
n : ℕ
h : ↑Ω (succ n) = 1
x : ℕ
hx : factors (succ n) = [x]
⊢ x ∈ factors ?succ.intro.n

case succ.intro.n
R : Type ?u.553341
n : ℕ
h : ↑Ω (succ n) = 1
x : ℕ
hx : factors (succ n) = [x]
⊢ ℕ
rw [hx, List.mem_singleton]
case zero
R : Type ?u.553341
h : ¬Prime Nat.zero
⊢ ↑Ω Nat.zero ≠ 1
case zero
R : Type ?u.553341
h : ↑Ω Nat.zero = 1
⊢ Prime Nat.zero
contrapose! h
no goals
case zero
R : Type ?u.553341
h : ¬Prime Nat.zero
⊢ ↑Ω Nat.zero ≠ 1
simp