Extract singleton to define function

Stream: new members

[Abdullah Uyu]

I proved central_projection maps to singletons under some assumptions. Now, I want to really define central projection as a function out of this fact. But I get this error:

import Mathlib.Data.Set.Card

variable [DecidableEq G]

class ProjectiveGeometry
  (G : Type u)
  (ell : G → G → G → Prop) where
  l1  : ∀ a b , ell a b a
  l2  : ∀ a b p q , ell a p q → ell b p q → p ≠ q → ell a b p
  l3  : ∀ a b c d p, ell p a b → ell p c d → ∃ q, ell q a c ∧ ell q b d

def star
  (ell : G → G → G → Prop)
  (a b : G) :
    Set G :=
  {c : G | if a = b then c = a else ell a b c}

def central_projection
  (a b c z: G)
  (ell : G → G → G → Prop)
  (x : star (ell := ell) a c) :
    Set G :=
  star (ell := ell) x z ∩ star (ell := ell) b c

theorem cen_proj_sing
  [PG : ProjectiveGeometry G ell]
  (a b c : G)
  (z : star (ell := ell) a b)
  (x : star (ell := ell) a c)
  (abc_ncol : ¬ ell a b c)
  (az_neq : a ≠ z)
  (bz_neq : b ≠ z) :
    ∃ y, central_projection (ell := ell) a b c z x = {y}  := by
  -- lengthy proof
  sorry

def central_projection_map
  [PG : ProjectiveGeometry G ell]
  (a b c : G)
  (z : star (ell := ell) a b)
  (x : star (ell := ell) a c)
  (abc_ncol : ¬ ell a b c)
  (az_neq : a ≠ z)
  (bz_neq : b ≠ z) :
    G :=
  have ex :
      ∃ y, central_projection (ell := ell) a b c z x = {y} := by
    apply cen_proj_sing a b c z x abc_ncol az_neq bz_neq
  let ⟨y, _⟩ := ex
  /-
  tactic 'cases' failed, nested error:
  tactic 'induction' failed, recursor 'Exists.casesOn' can only eliminate into Prop

  G: Type ?u.1228
  inst✝: DecidableEq G
  ell: G → G → G → Prop
  abc: G
  z: ↑(star ell a b)
  x: ↑(star ell a c)
  motive: (∃ y, central_projection a b c (↑z) ell x = {y}) → Sort ?u.1850
  h_1: (y : G) → (h : central_projection a b c (↑z) ell x = {y}) → motive ⋯
  ex✝: ∃ y, central_projection a b c (↑z) ell x = {y}
  ⊢ motive ex✝
   after processing
    _
  the dependent pattern matcher can solve the following kinds of equations
  - <var> = <term> and <term> = <var>
  - <term> = <term> where the terms are definitionally equal
  - <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil
  -/
  y

[Etienne Marion]

This is because pattern matching invokes existential recursor, which as indicated can only provide Prop (no data), but as a def can produce data, this is not possible.
You have to use docs#Exists.choose, which uses the axiom of choice to build data.

[Abdullah Uyu]

Ah, I see. That resolves it, thank you!