p : ℕ+
pp : Prime p
⊢ p ≠ 1
p : ℕ+
⊢ Prime p → p ≠ 1
intro pp
p : ℕ+
pp : Prime p
contra : p = 1
⊢ False
p : ℕ+
pp : Prime p
⊢ p ≠ 1
intro contra
p : ℕ+
pp : Prime p
contra : p = 1
⊢ ↑p = 1
p : ℕ+
pp : Prime p
contra : p = 1
⊢ False
apply Nat.Prime.ne_one pp
p : ℕ+
pp : Prime p
contra : p = 1
⊢ p = 1
p : ℕ+
pp : Prime p
contra : p = 1
⊢ ↑p = 1
rw [PNat.coe_eq_one_iff]
no goals
p : ℕ+
pp : Prime p
contra : p = 1
⊢ p = 1
apply contra