How can I define a function in Lean prover? (In "A function is injective then has left inverse")

I want to prove the fact "A function is injective, then it has left-inverse." in Lean Prover.

As you know, in standard proof of this theorem, ( https://math.stackexchange.com/questions/2099699/left-inverse-in-f-a-iff-injective-proof ), we should define a function which is defined by case-by-case form. But I think that there is no way to define case-by-case form function in lean prover.

How can I prove it in Lean Prover?

Solution

Use if...then...else to make a case by case definition.

import tactic

open function

open_locale classical

-- Theorem: if A is nonempty then an injective function from it
-- has a one-sided inverse
example (A B : Type) [inhabited A] (f : A → B) (hf : injective f) :
  ∃ g : B → A, g ∘ f = id :=
-- Proof:
begin
  -- define the function in the obvious way; it's the inverse on the image
  -- and a random element of A otherwise (works because A is inhabited)
  let g : B → A := λ b, if h : ∃ a, f a = b then h.some else arbitrary A,
  -- claim g works
  use g,
  -- let's take an arbitrary element a of A
  ext a,
  -- and let's note that there exists an element of a whose image
  -- under f is f(a), namely a itself!
  have ha : ∃ a' : A, f a' = f a := ⟨a, rfl⟩,
  -- Now unravel the definition of g and follow your nose.
  simp [g],
  -- We now need to prove that the "random" element g chose
  -- must be the a we started with, but how do we rule out lots of
  -- different a's mapping to the same b? We use injectivity of f.
  apply hf,
  -- and now we're done
  exact ha.some_spec,
end