La semana en Calculemus (15 de junio de 2024)

José A. Alonso

16-06-2024

Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:

1. Si g ∘ f es suprayectiva, entonces g es suprayectiva
2. Las funciones inyectivas tienen inversa por la izquierda
3. Las funciones con inversa por la derecha son suprayectivas
4. Las funciones suprayectivas tienen inversa por la derecha
5. Las funciones con inversa son biyectivas

A continuación se muestran las soluciones.

1. Si g ∘ f es suprayectiva, entonces g es suprayectiva

Sean \(f: X → Y\) y \(g: Y → Z\). Demostrar que si \(g ∘ f\) es suprayectiva, entonces \(g\) es suprayectiva.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic

open Function

variable {X Y Z : Type}
variable {f : X → Y}
variable {g : Y → Z}

example
  (h : Surjective (g ∘ f))
  : Surjective g :=
by sorry

1.1. Demostración en lenguaje natural

Se \(z ∈ Z\). Entonces, por ser \(g ∘ f\) suprayectiva, existe un \(x ∈ X\) tal que \[ (g ∘ f)(x) = z \tag{1} \] Por tanto, existe \(y = f(x) ∈ Y\) tal que \begin{align} g(y) &= g(f(x)) \newline &= (g ∘ f)(x) \newline &= z &&\text{[por (1)]} \end{align}

1.2. Demostraciones con Lean4

import Mathlib.Tactic

open Function

variable {X Y Z : Type}
variable {f : X → Y}
variable {g : Y → Z}

-- 1ª demostración
-- ===============

example
  (h : Surjective (g ∘ f))
  : Surjective g :=
by
  intro z
  -- z : Z
  -- ⊢ ∃ a, g a = z
  cases' h z with x hx
  -- x : X
  -- hx : (g ∘ f) x = z
  use f x
  -- ⊢ g (f x) = z
  exact hx

-- 2ª demostración
-- ===============

example
  (h : Surjective (g ∘ f))
  : Surjective g :=
by
  intro z
  -- z : Z
  -- ⊢ ∃ a, g a = z
  cases' h z with x hx
  -- x : X
  -- hx : (g ∘ f) x = z
  exact ⟨f x, hx⟩

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

1.3. Demostraciones con Isabelle/HOL

theory Suprayectiva_si_lo_es_la_composicion
imports Main
begin

(* 1ª demostración *)

lemma
  assumes "surj (g ∘ f)"
  shows "surj g"
proof (unfold Fun.surj_def, rule)
  fix z
  have "∃x. z = (g ∘ f) x"
    using assms
    by (rule surjD)
  then obtain x where "z = (g ∘ f) x"
    by (rule exE)
  then have "z = g (f x)"
    by (simp only: Fun.comp_apply)
  then show "∃y. z = g y"
    by (rule exI)
qed

(* 2 demostración *)

lemma
  assumes "surj (g ∘ f)"
  shows "surj g"
using assms
by auto

end

2. Las funciones inyectivas tienen inversa por la izquierda

En Lean4, que \(g\) es una inversa por la izquierda de \(f\) está definido por

   LeftInverse (g : β → α) (f : α → β) : Prop :=
      ∀ x, g (f x) = x

y que \(f\) tenga inversa por la izquierda está definido por

   HasLeftInverse (f : α → β) : Prop :=
      ∃ finv : β → α, LeftInverse finv f

Finalmente, que \(f\) es inyectiva está definido por

   Injective (f : α → β) : Prop :=
      ∀ ⦃x y⦄, f x = f y → x = y

Demostrar con Lean4 que si \(f\) es una función inyectiva con dominio no vacío, entonces \(f\) tiene inversa por la izquierda.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic

open Function Classical

variable {α β: Type _}
variable {f : α → β}

example
  [hα : Nonempty α]
  (hf : Injective f)
  : HasLeftInverse f :=
by sorry

2.1. Demostración en lenguaje natural

Sea \(f: A → B\) inyectiva con \(A ≠ ∅\). Entonces, existe un \(a ∈ A\). Sea \(g: B → A\) definida por \[g(y) = \begin{cases} \text{un \(x\) tal que \(f(x) = y\)}, & \text{si \((∃x)[f(x) = y]\)} \newline a, & \text{en caso contrario.} \end{cases} \] Vamos a demostrar que \(g\) es una inversa por la izquierda de \(f\); es decir, \[ (∀x)[g(f(x)) = x] \] Para ello, sea \(x ∈ A\). Entonces, \[ (∃x)[f(x) = f(x)] \] Por la definición de \(g\), \[ g(f(x)) = z \tag{1} \] donde \[ f(z) = f(x). \] Como \(f\) es inyectiva, \[ z = x \] Y, por (1), \[ g(f(x)) = x \]

2.2. Demostraciones con Lean4

import Mathlib.Tactic

open Function Classical

variable {α β: Type _}
variable {f : α → β}

-- 1ª demostración
-- ===============

example
  [hα : Nonempty α]
  (hf : Injective f)
  : HasLeftInverse f :=
by
  unfold HasLeftInverse
  -- ⊢ ∃ finv, LeftInverse finv f
  set g := fun y ↦ if h : ∃ x, f x = y then h.choose else Classical.arbitrary α
  use g
  unfold LeftInverse
  -- ⊢ ∀ (x : α), g (f x) = x
  intro a
  -- ⊢ g (f a) = a
  have h1 : ∃ x : α, f x = f a := Exists.intro a rfl
  dsimp at *
  -- ⊢ (if h : ∃ x, f x = f a then Exists.choose h else Classical.arbitrary α) = a
  simp [h1]
  -- ⊢ Exists.choose (_ : ∃ x, f x = f a) = a
  apply hf
  -- ⊢ f (Exists.choose (_ : ∃ x, f x = f a)) = f a
  exact Classical.choose_spec h1

-- 2ª demostración
-- ===============

example
  [hα : Nonempty α]
  (hf : Injective f)
  : HasLeftInverse f :=
by
  set g := fun y ↦ if h : ∃ x, f x = y then h.choose else Classical.arbitrary α
  use g
  -- ⊢ LeftInverse g f
  intro a
  -- a : α
  -- ⊢ g (f a) = a
  have h1 : ∃ x : α, f x = f a := Exists.intro a rfl
  dsimp at *
  -- ⊢ (if h : ∃ x, f x = f a then Exists.choose h else Classical.arbitrary α) = a
  simp [h1]
  -- ⊢ Exists.choose (_ : ∃ x, f x = f a) = a
  exact hf (Classical.choose_spec h1)

-- 3ª demostración
-- ===============

example
  [hα : Nonempty α]
  (hf : Injective f)
  : HasLeftInverse f :=
by
  unfold HasLeftInverse
  -- ⊢ ∃ finv, LeftInverse finv f
  use invFun f
  -- ⊢ LeftInverse (invFun f) f
  unfold LeftInverse
  -- ⊢ ∀ (x : α), invFun f (f x) = x
  intro x
  -- x : α
  -- ⊢ invFun f (f x) = x
  apply hf
  -- ⊢ f (invFun f (f x)) = f x
  apply invFun_eq
  -- ⊢ ∃ a, f a = f x
  use x

-- 4ª demostración
-- ===============

example
  [hα : Nonempty α]
  (hf : Injective f)
  : HasLeftInverse f :=
by
  use invFun f
  -- ⊢ LeftInverse (invFun f) f
  intro x
  -- x : α
  -- ⊢ invFun f (f x) = x
  apply hf
  -- ⊢ f (invFun f (f x)) = f x
  apply invFun_eq
  -- ⊢ ∃ a, f a = f x
  use x

-- 5ª demostración
-- ===============

example
  [_hα : Nonempty α]
  (hf : Injective f)
  : HasLeftInverse f :=
⟨invFun f, leftInverse_invFun hf⟩

-- 6ª demostración
-- ===============

example
  [_hα : Nonempty α]
  (hf : Injective f)
  : HasLeftInverse f :=
Injective.hasLeftInverse hf

-- Lemas usados
-- ============

-- variable (p : α → Prop)
-- variable (x : α)
-- variable (b : β)
-- variable (γ : Type _) [Nonempty γ]
-- variable (f1 : γ → β)
-- #check (Classical.choose_spec : (h : ∃ x, p x) → p (Classical.choose h))
-- #check (Exists.intro x: p x → ∃ y, p y)
-- #check (Injective.hasLeftInverse : Injective f1 → HasLeftInverse f1)
-- #check (invFun_eq : (∃ a, f1 a = b) → f1 (invFun f1 b) = b)
-- #check (leftInverse_invFun : Function.Injective f1 → LeftInverse (Function.invFun f1) f1)

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

2.3. Demostraciones con Isabelle/HOL

theory Las_funciones_inyectivas_tienen_inversa_por_la_izquierda
imports Main
begin

definition tiene_inversa_izq :: "('a ⇒ 'b) ⇒ bool" where
  "tiene_inversa_izq f ⟷ (∃g. ∀x. g (f x) = x)"

(* 1ª demostración *)

lemma
  assumes "inj f"
  shows   "tiene_inversa_izq f"
proof (unfold tiene_inversa_izq_def)
  let ?g = "(λy. SOME x. f x = y)"
  have "∀x. ?g (f x) = x"
  proof (rule allI)
    fix a
    have "∃x. f x = f a"
      by auto
    then have "f (?g (f a)) = f a"
      by (rule someI_ex)
    then show "?g (f a) = a"
      using assms
      by (simp only: injD)
  qed
  then show "(∃g. ∀x. g (f x) = x)"
    by (simp only: exI)
qed

(* 2ª demostración *)

lemma
  assumes "inj f"
  shows   "tiene_inversa_izq f"
proof (unfold tiene_inversa_izq_def)
  have "∀x. inv f (f x) = x"
  proof (rule allI)
    fix x
    show "inv f (f x) = x"
      using assms by (simp only: inv_f_f)
  qed
  then show "(∃g. ∀x. g (f x) = x)"
    by (simp only: exI)
qed

(* 3ª demostración *)

lemma
  assumes "inj f"
  shows   "tiene_inversa_izq f"
proof (unfold tiene_inversa_izq_def)
  have "∀x. inv f (f x) = x"
    by (simp add: assms)
  then show "(∃g. ∀x. g (f x) = x)"
    by (simp only: exI)
qed

end

3. Las funciones con inversa por la derecha son suprayectivas

En Lean4, que \(g\) es una inversa por la izquierda de \(f\) está definido por

   LeftInverse (g : β → α) (f : α → β) : Prop :=
      ∀ x, g (f x) = x

que \(g\) es una inversa por la derecha de \(f\) está definido por

   RightInverse (g : β → α) (f : α → β) : Prop :=
      LeftInverse f g

y que \(f\) tenga inversa por la derecha está definido por

   HasRightInverse (f : α → β) : Prop :=
      ∃ g : β → α, RightInverse g f

Finalmente, que \(f\) es suprayectiva está definido por

   def Surjective (f : α → β) : Prop :=
      ∀ b, ∃ a, f a = b

Demostrar con Lean4 que si la función \(f\) tiene inversa por la derecha, entonces \(f\) es suprayectiva.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
open Function

variable {α β: Type _}
variable {f : α → β}

example
  (hf : HasRightInverse f)
  : Surjective f :=
by sorry

3.1. Demostración en lenguaje natural

Sea \(f: A → B\) y \(g: B → A\) una inversa por la derecha de \(f\). Entonces, \[ (∀y ∈ B)[f(g(y)) = y] \tag{1} \]

Para demostrar que \(f\) es subprayectiva, sea \(b ∈ B\). Entonces, \(g(b) ∈ A\) y, por (1), \[ f(g(b) = b \]

3.2. Demostraciones con Lean4

import Mathlib.Tactic
open Function

variable {α β: Type _}
variable {f : α → β}

-- 1ª demostración
-- ===============

example
  (hf : HasRightInverse f)
  : Surjective f :=
by
  unfold Surjective
  -- ⊢ ∀ (b : β), ∃ a, f a = b
  unfold HasRightInverse at hf
  -- hf : ∃ finv, Function.RightInverse finv f
  cases' hf with g hg
  -- g : β → α
  -- hg : Function.RightInverse g f
  intro b
  -- b : β
  -- ⊢ ∃ a, f a = b
  use g b
  -- ⊢ f (g b) = b
  exact hg b

-- 2ª demostración
-- ===============

example
  (hf : HasRightInverse f)
  : Surjective f :=
by
  intro b
  -- b : β
  -- ⊢ ∃ a, f a = b
  cases' hf with g hg
  -- g : β → α
  -- hg : Function.RightInverse g f
  use g b
  -- ⊢ f (g b) = b
  exact hg b

-- 3ª demostración
-- ===============

example
  (hf : HasRightInverse f)
  : Surjective f :=
by
  intro b
  -- b : β
  -- ⊢ ∃ a, f a = b
  cases' hf with g hg
  -- g : β → α
  -- hg : Function.RightInverse g f
  exact ⟨g b, hg b⟩

-- 4ª demostración
-- ===============

example
  (hf : HasRightInverse f)
  : Surjective f :=
HasRightInverse.surjective hf

-- Lemas usados
-- ============

-- #check (HasRightInverse.surjective : HasRightInverse f → Surjective f)

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

3.3. Demostraciones con Isabelle/HOL

theory Las_funciones_con_inversa_por_la_derecha_son_suprayectivas
imports Main
begin

definition tiene_inversa_dcha :: "('a ⇒ 'b) ⇒ bool" where
  "tiene_inversa_dcha f ⟷ (∃g. ∀y. f (g y) = y)"

(* 1ª demostración *)

lemma
  assumes "tiene_inversa_dcha f"
  shows   "surj f"
proof (unfold surj_def; intro allI)
  fix y
  obtain g where "∀y. f (g y) = y"
    using assms tiene_inversa_dcha_def by auto
  then have "f (g y) = y"
    by (rule allE)
  then have "y = f (g y)"
    by (rule sym)
  then show "∃x. y = f x"
    by (rule exI)
qed

(* 2ª demostración *)
lemma
  assumes "tiene_inversa_dcha f"
  shows   "surj f"
proof (unfold surj_def; intro allI)
  fix y
  obtain g where "∀y. f (g y) = y"
    using assms tiene_inversa_dcha_def by auto
  then have "y = f (g y)"
    by simp
  then show "∃x. y = f x"
    by (rule exI)
qed

(* 3ª demostración *)

lemma
  assumes "tiene_inversa_dcha f"
  shows   "surj f"
proof (unfold surj_def; intro allI)
  fix y
  obtain g where "∀y. f (g y) = y"
    using assms tiene_inversa_dcha_def by auto
  then show "∃x. y = f x"
    by metis
qed

(* 4ª demostración *)

lemma
  assumes "tiene_inversa_dcha f"
  shows   "surj f"
proof (unfold surj_def; intro allI)
  fix y
  show "∃x. y = f x"
    using assms tiene_inversa_dcha_def
    by metis
qed

(* 5ª demostración *)

lemma
  assumes "tiene_inversa_dcha f"
  shows   "surj f"
using assms tiene_inversa_dcha_def surj_def
by metis

end

4. Las funciones suprayectivas tienen inversa por la derecha

En Lean4, que \(g\) es una inversa por la izquierda de \(f\) está definido por

   LeftInverse (g : β → α) (f : α → β) : Prop :=
      ∀ x, g (f x) = x

que \(g\) es una inversa por la derecha de \(f\) está definido por

   RightInverse (g : β → α) (f : α → β) : Prop :=
      LeftInverse f g

y que \(f\) tenga inversa por la derecha está definido por

   HasRightInverse (f : α → β) : Prop :=
      ∃ g : β → α, RightInverse g f

Finalmente, que \(f\) es suprayectiva está definido por

   def Surjective (f : α → β) : Prop :=
      ∀ b, ∃ a, f a = b

Demostrar con Lean4 que si \(f\) es una función suprayectiva, entonces \(f\) tiene inversa por la derecha.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
open Function Classical

variable {α β: Type _}
variable {f : α → β}

example
  (hf : Surjective f)
  : HasRightInverse f :=
by sorry

4.1. Demostración en lenguaje natural

Sea \(f: A → B\) una función suprayectiva. Sea \(g: B → A\) la función definida por \[ g(y) = x, \text{donde \(x\) es un elemento tal que \(f(x) = y\)} \]

Veamos que \(g\) es una inversa por la derecha de \(f\); es decir, \[ (∀y ∈ B)[f(g(y)) = y] \] Para ello, sea \(b ∈ B\). Entonces, \[ f(g(b)) = f(a) \] donde \(a\) es un elemento tal que \[ f(a) = b \] Por tanto, \[ f(g(b)) = b \]

4.2. Demostraciones con Lean4

import Mathlib.Tactic
open Function Classical

variable {α β: Type _}
variable {f : α → β}

-- 1ª demostración
-- ===============

example
  (hf : Surjective f)
  : HasRightInverse f :=
by
  unfold HasRightInverse
  -- ⊢ ∃ finv, Function.RightInverse finv f
  let g := fun y ↦ Classical.choose (hf y)
  use g
  -- ⊢ Function.RightInverse g f
  unfold Function.RightInverse
  -- ⊢ LeftInverse f g
  unfold Function.LeftInverse
  -- ⊢ ∀ (x : β), f (g x) = x
  intro b
  -- ⊢ f (g b) = b
  exact Classical.choose_spec (hf b)

-- 2ª demostración
-- ===============

example
  (hf : Surjective f)
  : HasRightInverse f :=
by
  let g := fun y ↦ Classical.choose (hf y)
  use g
  -- ⊢ Function.RightInverse g f
  intro b
  -- ⊢ f (g b) = b
  exact Classical.choose_spec (hf b)

-- 3ª demostración
-- ===============

example
  (hf : Surjective f)
  : HasRightInverse f :=
by
  use surjInv hf
  -- ⊢ Function.RightInverse (surjInv hf) f
  intro b
  -- ⊢ f (surjInv hf b) = b
  exact surjInv_eq hf b

-- 4ª demostración
-- ===============

example
  (hf : Surjective f)
  : HasRightInverse f :=
by
  use surjInv hf
  -- ⊢ Function.RightInverse (surjInv hf) f
  exact surjInv_eq hf

-- 5ª demostración
-- ===============

example
  (hf : Surjective f)
  : HasRightInverse f :=
⟨surjInv hf, surjInv_eq hf⟩

-- 6ª demostración
-- ===============

example
  (hf : Surjective f)
  : HasRightInverse f :=
⟨_, rightInverse_surjInv hf⟩

-- 7ª demostración
-- ===============

example
  (hf : Surjective f)
  : HasRightInverse f :=
Surjective.hasRightInverse hf

-- Lemas usados
-- ============

-- variable (p : α -> Prop)
-- #check (Classical.choose_spec : (h : ∃ x, p x) → p (Classical.choose h))
--
-- variable (h : Surjective f)
-- variable (b : β)
-- #check (surjInv_eq h b : f (surjInv h b) = b)
-- #check (rightInverse_surjInv h : RightInverse (surjInv h) f)
--
-- #check (Surjective.hasRightInverse : Surjective f → HasRightInverse f)

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

4.3. Demostraciones con Isabelle/HOL

theory Las_funciones_suprayectivas_tienen_inversa_por_la_derecha
imports Main
begin

definition tiene_inversa_dcha :: "('a ⇒ 'b) ⇒ bool" where
  "tiene_inversa_dcha f ⟷ (∃g. ∀y. f (g y) = y)"

(* 1ª demostración *)

lemma
  assumes "surj f"
  shows   "tiene_inversa_dcha f"
proof (unfold tiene_inversa_dcha_def)
  let ?g = "λy. SOME x. f x = y"
  have "∀y. f (?g y) = y"
  proof (rule allI)
    fix y
    have "∃x. y = f x"
      using assms by (rule surjD)
    then have "∃x. f x = y"
      by auto
    then show "f (?g y) = y"
      by (rule someI_ex)
  qed
  then show "∃g. ∀y. f (g y) = y"
    by auto
qed

(* 2ª demostración *)

lemma
  assumes "surj f"
  shows   "tiene_inversa_dcha f"
proof (unfold tiene_inversa_dcha_def)
  let ?g = "λy. SOME x. f x = y"
  have "∀y. f (?g y) = y"
  proof (rule allI)
    fix y
    have "∃x. f x = y"
      by (metis assms surjD)
    then show "f (?g y) = y"
      by (rule someI_ex)
  qed
  then show "∃g. ∀y. f (g y) = y"
    by auto
qed

(* 3ª demostración *)

lemma
  assumes "surj f"
  shows   "tiene_inversa_dcha f"
proof (unfold tiene_inversa_dcha_def)
  have "∀y. f (inv f y) = y"
    by (simp add: assms surj_f_inv_f)
  then show "∃g. ∀y. f (g y) = y"
    by auto
qed

(* 4ª demostración *)

lemma
  assumes "surj f"
  shows   "tiene_inversa_dcha f"
  by (metis assms surjD tiene_inversa_dcha_def)

end

5. Las funciones con inversa son biyectivas

En Lean4 se puede definir que \(g\) es una inversa de \(f\) por

   def inversa (f : X → Y) (g : Y → X) :=
     (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

y que \(f\) tiene inversa por

   def tiene_inversa (f : X → Y) :=
     ∃ g, inversa g f

Demostrar con Lean4 que si la función \(f\) tiene inversa, entonces \(f\) es biyectiva.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
open Function

variable {X Y : Type _}
variable (f : X → Y)

def inversa (f : X → Y) (g : Y → X) :=
  (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

def tiene_inversa (f : X → Y) :=
  ∃ g, inversa g f

example
  (hf : tiene_inversa f)
  : Bijective f :=
by sorry

5.1. Demostración en lenguaje natural

Puesto que \(f: X → Y\) tiene inversa, existe una \(g: Y → X\) tal que \begin{align} &(∀x)[(g ∘ f)(x) = x] \tag{1} \newline &(∀y)[(f ∘ g)(y) = y] \tag{2} \end{align}

Para demostrar que \(f\) es inyectiva, sean \(a, b ∈ X\) tales que \[ f(a) = f(b) \tag{3} \] entonces \begin{align} a &= g(f(a)) &&\text{[por (1)]} \newline &= g(f(b)) &&\text{[por (3)]} \newline &= b &&\text{[por (1)]} \end{align}

Para demostrar que \(f\) es suprayectiva, sea \(y ∈ Y\). Entonces, existe \(a = g(y) ∈ X\) tal que \begin{align} f(a) &= f(g(y)) \newline &= y &&\text{[por (2)]} \end{align}

Como \(f\) es inyectiva y suprayectiva, entonces \(f\) es biyectiva.

5.2. Demostraciones con Lean4

import Mathlib.Tactic
open Function

variable {X Y : Type _}
variable (f : X → Y)

def inversa (f : X → Y) (g : Y → X) :=
  (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

def tiene_inversa (f : X → Y) :=
  ∃ g, inversa g f

-- 1ª demostración
-- ===============

example
  (hf : tiene_inversa f)
  : Bijective f :=
by
  rcases hf with ⟨g, ⟨h1, h2⟩⟩
  -- g : Y → X
  -- h1 : ∀ (x : Y), (f ∘ g) x = x
  -- h2 : ∀ (y : X), (g ∘ f) y = y
  constructor
  . -- ⊢ Injective f
    intros a b hab
    -- a b : X
    -- hab : f a = f b
    -- ⊢ a = b
    calc a = g (f a) := (h2 a).symm
         _ = g (f b) := congr_arg g hab
         _ = b       := h2 b
  . -- ⊢ Surjective f
    intro y
    -- y : Y
    -- ⊢ ∃ a, f a = y
    use g y
    -- ⊢ f (g y) = y
    exact h1 y

-- 2ª demostración
-- ===============

example
  (hf : tiene_inversa f)
  : Bijective f :=
by
  rcases hf with ⟨g, ⟨h1, h2⟩⟩
  -- g : Y → X
  -- h1 : ∀ (x : Y), (f ∘ g) x = x
  -- h2 : ∀ (y : X), (g ∘ f) y = y
  constructor
  . -- ⊢ Injective f
    intros a b hab
    -- a b : X
    -- hab : f a = f b
    -- ⊢ a = b
    calc a = g (f a) := (h2 a).symm
         _ = g (f b) := congr_arg g hab
         _ = b       := h2 b
  . -- ⊢ Surjective f
    intro y
    -- y : Y
    -- ⊢ ∃ a, f a = y
    exact ⟨g y, h1 y⟩

-- 3ª demostración
-- ===============

example
  (hf : tiene_inversa f)
  : Bijective f :=
by
  rcases hf with ⟨g, ⟨h1, h2⟩⟩
  constructor
  . exact LeftInverse.injective h2
  . exact RightInverse.surjective h1

-- 4ª demostración
-- ===============

example
  (hf : tiene_inversa f)
  : Bijective f :=
by
  rcases hf with ⟨g, ⟨h1, h2⟩⟩
  exact ⟨LeftInverse.injective h2,
         RightInverse.surjective h1⟩

-- 5ª demostración
-- ===============

example :
  tiene_inversa f → Bijective f :=
by
  rintro ⟨g, ⟨h1, h2⟩⟩
  exact ⟨LeftInverse.injective h2,
         RightInverse.surjective h1⟩

-- 6ª demostración
-- ===============

example :
  tiene_inversa f → Bijective f :=
fun ⟨_, ⟨h1, h2⟩⟩ ↦ ⟨LeftInverse.injective h2,
                     RightInverse.surjective h1⟩

-- Lemas usados
-- ============

-- variable (x y : X)
-- variable (g : Y → X)
-- #check (congr_arg f : x = y → f x = f y)
-- #check (LeftInverse.injective : LeftInverse g f → Injective f)
-- #check (RightInverse.surjective : RightInverse g f → Surjective f)

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

5.3. Demostraciones con Isabelle/HOL

theory Las_funciones_con_inversa_son_biyectivas
imports Main
begin

definition inversa :: "('a ⇒ 'b) ⇒ ('b ⇒ 'a) ⇒ bool" where
  "inversa f g ⟷ (∀ x. (g ∘ f) x = x) ∧ (∀ y. (f ∘ g) y = y)"

definition tiene_inversa :: "('a ⇒ 'b) ⇒ bool" where
  "tiene_inversa f ⟷ (∃ g. inversa f g)"

(* 1ª demostración *)

lemma
  fixes f :: "'a ⇒ 'b"
  assumes "tiene_inversa f"
  shows   "bij f"
proof -
  obtain g where h1 : "∀ x. (g ∘ f) x = x" and
                 h2 : "∀ y. (f ∘ g) y = y"
    by (meson assms inversa_def tiene_inversa_def)
  show "bij f"
  proof (rule bijI)
    show "inj f"
    proof (rule injI)
      fix x y
      assume "f x = f y"
      then have "g (f x) = g (f y)"
        by simp
      then show "x = y"
        using h1 by simp
    qed
  next
    show "surj f"
    proof (rule surjI)
      fix y
      show "f (g y) = y"
        using h2 by simp
    qed
  qed
qed

(* 2ª demostración *)

lemma
  fixes f :: "'a ⇒ 'b"
  assumes "tiene_inversa f"
  shows   "bij f"
proof -
  obtain g where h1 : "∀ x. (g ∘ f) x = x" and
                 h2 : "∀ y. (f ∘ g) y = y"
    by (meson assms inversa_def tiene_inversa_def)
  show "bij f"
  proof (rule bijI)
    show "inj f"
    proof (rule injI)
      fix x y
      assume "f x = f y"
      then have "g (f x) = g (f y)"
        by simp
      then show "x = y"
        using h1 by simp
    qed
  next
    show "surj f"
    proof (rule surjI)
      fix y
      show "f (g y) = y"
        using h2 by simp
    qed
  qed
qed

end