Lean证明器中如何定义函数证明单射函数存在左逆元

你对Lean的能力存在误解：Lean完全支持分情况形式的函数定义，配合经典逻辑与选择公理，可以直接完成该定理的证明，不存在障碍。
注意该定理成立需要一个隐含前提：定义域类型非空——如果定义域是空类型、陪域非空，单射的空函数不可能存在左逆，这是定理本身的边界，不是证明工具的限制。

你提到的标准分情况证明思路在Lean中可以完全复现，核心依赖三个内置能力：

• 原生支持if条件分支的函数定义，可以直接根据「元素是否在函数像集中」做分支判断
• 经典逻辑下的选择公理算子Classical.choose，可以从存在性证明中提取出满足条件的项
• 非空类型的任意取值算子Classical.arbitrary，可以给不在像集中的陪域元素指定一个默认的定义域返回值

具体构造左逆函数g : β → α的规则就是标准的分情况规则：

1. 对任意y : β，如果存在x : α使得f x = y，就取g y为这个对应的x（因为f是单射，这个x唯一）
2. 如果y不在f的像集中，就随便取一个α中的元素作为g y的返回值（这部分取值不会出现在左逆复合的路径中，不影响证明正确性）

import Mathlib.Logic.Function.Basic

-- 手动实现的证明版本
theorem injective_has_left_inverse {α β : Type*} [Nonempty α] (f : α → β) (hf : Function.Injective f) :
    ∃ (g : β → α), g ∘ f = id := by
  -- 分情况定义左逆g
  let g : β → α := fun y =>
    if h : ∃ x, f x = y then
      Classical.choose h  -- 取出像集中元素对应的原像
    else
      Classical.arbitrary α  -- 非像集元素返回定义域任意默认值
  use g
  -- 证明g和f复合等于恒等函数
  funext x
  have h_img : ∃ (x' : α), f x' = f x := ⟨x, rfl⟩
  simp [g, h_img, hf.eq_iff]
  <;> tauto

-- Mathlib已经内置了该定理，日常使用直接调用即可
example {α β : Type*} [Nonempty α] (f : α → β) (hf : Function.Injective f) :
    ∃ (g : β → α), g ∘ f = id := hf.hasLeftInverse

如果你是在构造性逻辑（不启用排中律、选择公理）的环境下工作，该定理确实无法证明——这不是Lean的限制，是构造性数学本身的结论：没有选择公理的情况下，你无法为所有陪域元素统一选出对应的原像。但Mathlib默认启用经典逻辑，日常证明直接使用内置定理即可，不需要手动重复构造。

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