How to properly Type Functions for Lean4?

Stream: general

[Mason McBride]

Screenshot-2023-11-13-at-8.34.08-PM.png
In this screenshot, my Ex1 does not successfully parse and all the variables are of type ?m.218 etc and not X, Y, etc. Why is this?

[Yury G. Kudryashov]

This is not an #mwe UPD: I was wrong.

[Yury G. Kudryashov]

Also, please use #backticks instead of screenshots.

[Mason McBride]

This is my entire file so the fact it's not an MWE is a good answer

[Yury G. Kudryashov]

Don't you have some imports? UPD: I see, you don't.

[Mason McBride]

/-- `LeftInverse g f` means that g is a left inverse to f. That is, `g ∘ f = id`. -/
def LeftInverse (g : β → α) (f : α → β) : Prop :=
  ∀ x, g (f x) = x

/-- `HasLeftInverse f` means that `f` has an unspecified left inverse. -/
def HasLeftInverse (f : α → β) : Prop :=
  ∃ finv : β → α, LeftInverse finv f

/-- `RightInverse g f` means that g is a right inverse to f. That is, `f ∘ g = id`. -/
def RightInverse (g : β → α) (f : α → β) : Prop :=
  LeftInverse f g

/-- `HasRightInverse f` means that `f` has an unspecified right inverse. -/
def HasRightInverse (f : α → β) : Prop :=
  ∃ finv : β → α, RightInverse finv f

variable (X : α) (Y : Β )
variable (g : Y → X) (f : X → Y) (h : X → Y)
def Ex1 (LeftInverse g f) (RightInverse h f) : g = h := by sorry

[Mason McBride]

I copy and pasted from Function.lean but I'm trying to start from the ground up

[Yury G. Kudryashov]

You defined (X : α) and (Y : B) instead of making them types.

[Yury G. Kudryashov]

I guess, in your setup, Lean uses autoimplicits for α and β but not for X and Y.

[Mason McBride]

universe u

variable (X Y: Type u)

/-- `LeftInverse g f` means that g is a left inverse to f. That is, `g ∘ f = id`. -/
def LeftInverse (g : β → α) (f : α → β) : Prop :=
  ∀ x, g (f x) = x

/-- `HasLeftInverse f` means that `f` has an unspecified left inverse. -/
def HasLeftInverse (f : α → β) : Prop :=
  ∃ finv : β → α, LeftInverse finv f

/-- `RightInverse g f` means that g is a right inverse to f. That is, `f ∘ g = id`. -/
def RightInverse (g : β → α) (f : α → β) : Prop :=
  LeftInverse f g

/-- `HasRightInverse f` means that `f` has an unspecified right inverse. -/
def HasRightInverse (f : α → β) : Prop :=
  ∃ finv : β → α, RightInverse finv f

variable (g : Y → X) (f : X → Y) (h : X → Y)
def Ex1 (LeftInverse g f) (RightInverse h f) : g = h := by sorry

Here is my MWE.
Screenshot-2023-11-13-at-8.44.06-PM.png
This is my infoview. I want it to be clean and clear without all the underneath typing that Lean is doing

[Yury G. Kudryashov]

You should name your assumptions

lemma ex1 (h1 : LeftInverse g f) (h2 : RightInverse h f) : g = h := sorry

[Mason McBride]

Did yousee my infoview?

[Yury G. Kudryashov]

universe u

variable {α β : Type _} (X Y: Type u)

/-- `LeftInverse g f` means that g is a left inverse to f. That is, `g ∘ f = id`. -/
def LeftInverse (g : β → α) (f : α → β) : Prop :=
  ∀ x, g (f x) = x

/-- `HasLeftInverse f` means that `f` has an unspecified left inverse. -/
def HasLeftInverse (f : α → β) : Prop :=
  ∃ finv : β → α, LeftInverse finv f

/-- `RightInverse g f` means that g is a right inverse to f. That is, `f ∘ g = id`. -/
def RightInverse (g : β → α) (f : α → β) : Prop :=
  LeftInverse f g

/-- `HasRightInverse f` means that `f` has an unspecified right inverse. -/
def HasRightInverse (f : α → β) : Prop :=
  ∃ finv : β → α, RightInverse finv f

variable (g : Y → X) (f : X → Y) (h : Y → X)

theorem ex1 (h1 : LeftInverse g f) (h2 : RightInverse h f) : g = h := by sorry

[Mason McBride]

Thanks I appreciate it. Everything has the types I want but \alpha and \beta are type ?u.192 and ?u.195. Maybe I can do add the hidden attribute to them?

[Yury G. Kudryashov]

You can use Type u instead of Type _

[Mason McBride]

universe u

variable {α β : Type _} (X Y: Type u)

/-- g is a left inverse to f. That is, `g ∘ f = id`. -/
def LeftInverse (g : β → α) (f : α → β) : Prop :=
  g ∘ f = id

/-- g is a right inverse to f. That is, `f ∘ g = id`. -/
def RightInverse (g : β → α) (f : α → β) : Prop :=
  LeftInverse f g

/-- `f` has an unspecified left inverse. -/
def HasLeftInverse (f : α → β) : Prop :=
  ∃ finv : β → α, LeftInverse finv f

/-- `f` has an unspecified right inverse. -/
def HasRightInverse (f : α → β) : Prop :=
  ∃ finv : β → α, RightInverse finv f

variable (g : Y → X) (f : X → Y) (h : Y → X)
def Ex1 (h₁ : LeftInverse g f) (h₂ : RightInverse h f) : g = h := by
  calc g = g ∘ id      := rfl
  _      = g ∘ f ∘ h   := by rw [<- h₂]
  _      = (g ∘ f) ∘ h := rfl
  _      = id ∘ h      := by rw [h₁]
  _      = h           := by rfl