An implementation of finite choice, see https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Theorem.20for.20.22finite.20choice.22.3F/with/529925010

theorem finite_choice {X : Type u_1} {f : X → ℕ} {N : ℕ} (h : ∀ n < N, ∃ (x : X), f x = n) : ∃ (g : Fin N → X), ∀ (n : Fin N), f (g n) = ↑n

theorem sec_ex {α : Type u_1} {β : Type u_2} [Fintype β] [DecidableEq β] (f : α → β) (h : ∀ (b : β), ∃ (a : α), f a = b) : ∃ (s : β → α), f ∘ s = id

def finite_choice_trunc {X : Type u_1} {f : X → ℕ} {N : ℕ} (h : (n : ℕ) → n < N → Trunc { x : X // f x = n }) : Trunc { g : Fin N → X // ∀ (n : Fin N), f (g n) = ↑n }

Variants of the above that use Trunc in place of ∃. Roughly speaking, this means that if the hypotheses are constructive, we can guarantee that the conclusion is constructive

Equations

• One or more equations did not get rendered due to their size.

def sec_ex_trunc {α : Type u_1} {β : Type u_2} [Fintype β] [DecidableEq β] (f : α → β) (h : (b : β) → Trunc { a : α // f a = b }) : Trunc { s : β → α // f ∘ s = id }

Equations

• One or more equations did not get rendered due to their size.