Lean4代码报错排查：质数集合至少两元素证明问题

问题描述 #

编写Lean4代码完成集合定义与证明任务时，证明质数集合至少有两个不同元素的示例报错，需排查并修正语法或逻辑问题。

原始代码中的语法错误 #

你提供的代码里，example语句末尾多了冗余的中文文字的内容，这是直接导致编译报错的核心语法错误。

修正后的完整代码 #

/- 
## 问题2 
-/ 

/- 
1. 在Lean中定义自然数子集至少含两个元素的含义。

2. 在Lean中定义任意类型`X`的子集恰好含两个元素的含义。

3. 在Lean中定义自然数子集含无穷多元素的含义。

**上述1-3中请勿借用Mathlib中的任何定义**。定义方式可能有多种，请选择你认为最自然的方式。

随后通过证明以下测试用例验证你的定义是否符合要求：

1. 证明质数集合至少有两个不同元素。
2. 证明闭区间`Icc (0 : ℕ) 1`恰好有两个元素。
3. 证明从`Bool`到`Bool`的单射函数集合恰好有两个元素。
4. 证明奇数自然数集合含无穷多元素。
-/ 

noncomputable section
open Classical 
open Set 

-- 自然数子集至少含两个不同元素的定义
def at_least_two_elems (A : Set ℕ) : Prop :=
  ∃ a b, a ∈ A ∧ b ∈ A ∧ a ≠ b 

-- 任意类型`X`的子集恰好含两个不同元素的定义
def exactly_two_elems {X : Type} (A : Set X) : Prop :=
  ∃ a b, a ∈ A ∧ b ∈ A ∧ a ≠ b ∧ ∀ c, c ∈ A → (c = a ∨ c = b)

-- 自然数子集含无穷多元素的定义
def inf_elems (A : Set ℕ) : Prop :=
  ∀ n : ℕ, ∃ m, m ∈ A ∧ m > n

-- 证明质数集合至少有两个不同元素
example : at_least_two_elems {p : ℕ | Nat.Prime p} :=
  ⟨2, 3, Nat.Prime.two, Nat.Prime.three, ne_of_gt (by decide)⟩

额外说明 #

• 若你的Lean环境未自动导入质数相关定理，需手动添加import Mathlib.NumberTheory.Prime，确保Nat.Prime.two和Nat.Prime.three可被识别。
• 逻辑层面你的定义与证明思路完全正确：通过构造2和3这两个不同的质数，满足at_least_two_elems的存在性要求。

内容的提问来源于stack exchange，提问作者pop123_123