Why am I getting this error?

Stream: new members

[Abdullah Uyu]

I tried to specify ell explicitly, but it did not change anything.

import Mathlib.Data.Set.Card

open Set

namespace Basic

variable {G : Type*}
variable {ell : G → G → G → Prop}
variable [DecidableEq G]

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}

class CentralProjectionQuadruple
  (a b c : G)
  (z : star ell a b) where
  abc_ncol : ¬ ell a b c
  az_neq : a ≠ z
  bz_neq : b ≠ z

variable (a b c : G)
variable (z : star ell a b)
variable [CPQ : CentralProjectionQuadruple a b c z]

def central_projection
  (a b c z : G)
  (x : star ell a c) :
    Set (star ell b c) :=
  Subtype.val ⁻¹' (star ell x z ∩ star ell b c)

variable (x : star ell a c)

theorem cen_proj_sing :
    ∃ y, central_projection a b c z x = {y} := by
  sorry

noncomputable def cen_proj_map :
    star ell b c :=
  Exists.choose (cen_proj_sing a b c z x)

theorem zp_sym
  {a b : G}
  {z : star ell a b} :
    z.val ∈ star ell b a := by
  sorry

instance cpq_symmetry :
    CentralProjectionQuadruple b a c ⟨z.val, zp_sym⟩ where
  abc_ncol := by sorry
  az_neq := by exact CentralProjectionQuadruple.bz_neq c
  bz_neq := by exact CentralProjectionQuadruple.az_neq c

noncomputable def φ : star ell a c → star ell b c := cen_proj_map a b c z
noncomputable def ψ : star ell b c → star ell a c := cen_proj_map b a c ⟨z, zp_sym⟩

theorem cen_proj_left :
    Function.LeftInverse ψ φ := by sorry
/- Application type mismatch: In the application
  Function.LeftInverse ?m.7795 φ
the argument
  φ
has type
  (a b c : ?m.7797) →
    (z : ↑(star ?m.7798 a b)) →
      [CPQ : CentralProjectionQuadruple a b c z] → ↑(star ?m.7798 a c) → ↑(star ?m.7798 b c) : Type ?u.7796
but is expected to have type
  ?m.7554 → ?m.7555 : Sort (imax ?u.7553 ?u.7552)
 -/

[Aaron Liu]

Try doing Function.LeftInverse (ψ a b c z) (φ a b c z) instead

[Kevin Buzzard]

$\phi$ is a function which takes many inputs (e.g. a, b, c) before outputs the function star ell a c → star ell b c. In other words, $\phi$ is a function which takes many inputs. The error means "I was expecting a function which takes one input but you gave me a function which takes many inputs". You should probably write something like (\phi a b c z) instead of just \phi.

[Kenny Lau]

The error message also tells you that φ doesn't have the type that you think it should have

[Abdullah Uyu]

Ohhh I see, I am dumb!

[Abdullah Uyu]

How should I modify the code so that I don't have to provide those arguments?

[Abdullah Uyu]

I can do something like this:

theorem cen_proj_left :
    let phi := φ a b c z
    let psi := ψ a b c z
    Function.LeftInverse psi phi := by

but this is just a workaround

[Abdullah Uyu]

When I define it outside, it wants me to provide the arguments, I think I can see why this makes sense. This is like a scope thing, I guess.

[Kenny Lau]

@Abdullah Uyu you can use {} instead of () for the arguments to make them implicit, but it is not recommended here because Lean won't be able to figure them out automatically.

[Abdullah Uyu]

Yeah I see. I said workaround above, but I guess that's the best I can do to keep it tidy.

[Kyle Miller]

One technique people sometimes use is local notation. E.g.

local notation "φ" => φ a b c z
local notation "ψ" => ψ a b c z

theorem cen_proj_left :
    Function.LeftInverse ψ φ := by sorry

[Abdullah Uyu]

That's great!