问如何在精益验证程序中定义函数？(在"A函数是内射的，则有左逆“中)

EN

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