Menu Close

Etiqueta: L.intros

Las funciones de extracción no están acotadas

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión

   uₒ, u₂, u₄, u₆, ...

se ha obtenido con la función de extracción φ tal que φ(n) = 2*n.

En Lean, se puede definir que φ es una función de extracción por

   def extraccion (φ : ℕ → ℕ) :=
     ∀ n m, n < m → φ n < φ m

Demostrar que las funciones de extracción no está acotadas; es decir, que si φ es una función de extracción, entonces

    ∀ N N', ∃ n ≥ N', φ n ≥ N

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

import tactic
open nat
 
variable {φ :   }
 
def extraccion (φ :   ) :=
   n m, n < m  φ n < φ m
 
example
  (h : extraccion φ)
  :  N N',  n  N', φ n  N :=
sorry
Soluciones con Lean
import tactic
open nat
 
variable {φ :   }
 
def extraccion (φ :   ) :=
   n m, n < m  φ n < φ m
 
lemma aux
  (h : extraccion φ)
  :  n, n  φ n :=
begin
  intro n,
  induction n with m HI,
  { exact nat.zero_le (φ 0), },
  { apply nat.succ_le_of_lt,
    calc m  φ m        : HI
       ... < φ (succ m) : h m (m+1) (lt_add_one m), },
end
 
-- 1ª demostración
example
  (h : extraccion φ)
  :  N N',  n  N', φ n  N :=
begin
  intros N N',
  let n := max N N',
  use n,
  split,
  { exact le_max_right N N', },
  { calc N  n   : le_max_left N N'
       ...  φ n : aux h n, },
end
 
-- 2ª demostración
example
  (h : extraccion φ)
  :  N N',  n  N', φ n  N :=
begin
  intros N N',
  let n := max N N',
  use n,
  split,
  { exact le_max_right N N', },
  { exact le_trans (le_max_left N N')
                   (aux h n), },
end
 
-- 3ª demostración
example
  (h : extraccion φ)
  :  N N',  n  N', φ n  N :=
begin
  intros N N',
  use max N N',
  split,
  { exact le_max_right N N', },
  { exact le_trans (le_max_left N N')
                   (aux h (max N N')), },
end
 
-- 4ª demostración
example
  (h : extraccion φ)
  :  N N',  n  N', φ n  N :=
begin
  intros N N',
  use max N N',
  exact ⟨le_max_right N N',
         le_trans (le_max_left N N')
                  (aux h (max N N'))⟩,
end
 
-- 5ª demostración
example
  (h : extraccion φ)
  :  N N',  n  N', φ n  N :=
λ N N',
  ⟨max N N', ⟨le_max_right N N',
              le_trans (le_max_left N N')
                       (aux h (max N N'))⟩⟩
 
-- 6ª demostración
example
  (h : extraccion φ)
  :  N N',  n  N', φ n  N :=
assume N N',
let n := max N N' in
have h1 : n  N',
  from le_max_right N N',
show  n  N', φ n  N, from
exists.intro n
  (exists.intro h1
    (show φ n  N, from
       calc N  n   : le_max_left N N'
          ...  φ n : aux h n))
 
-- 7ª demostración
example
  (h : extraccion φ)
  :  N N',  n  N', φ n  N :=
assume N N',
let n := max N N' in
have h1 : n  N',
  from le_max_right N N',
show  n  N', φ n  N, from
⟨n, h1, calc N  n   : le_max_left N N'
          ...   φ n : aux h n⟩
 
-- 8ª demostración
example
  (h : extraccion φ)
  :  N N',  n  N', φ n  N :=
assume N N',
let n := max N N' in
have h1 : n  N',
  from le_max_right N N',
show  n  N', φ n  N, from
⟨n, h1, le_trans (le_max_left N N')
                 (aux h (max N N'))⟩
 
-- 9ª demostración
example
  (h : extraccion φ)
  :  N N',  n  N', φ n  N :=
assume N N',
let n := max N N' in
have h1 : n  N',
  from le_max_right N N',
⟨n, h1, le_trans (le_max_left N N')
                 (aux h n)⟩
 
-- 10ª demostración
example
  (h : extraccion φ)
  :  N N',  n  N', φ n  N :=
assume N N',
⟨max N N', le_max_right N N',
           le_trans (le_max_left N N')
                    (aux h (max N N'))⟩
 
-- 11ª demostración
lemma extraccion_mye
  (h : extraccion φ)
  :  N N',  n  N', φ n  N :=
λ N N',
  ⟨max N N', le_max_right N N',
             le_trans (le_max_left N N')
             (aux h (max N N'))

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
theory Las_funciones_de_extraccion_no_estan_acotadas
imports Main
begin
 
definition extraccion :: "(nat ⇒ nat) ⇒ bool" where
  "extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"
 
(* En la demostración se usará el siguiente lema *)
lemma aux :
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0"
    by simp
next
  fix n
  assume HI : "n ≤ φ n"
  also have "φ n < φ (Suc n)"
    using assms extraccion_def by blast
  finally show "Suc n ≤ φ (Suc n)"
    by simp
qed
 
(* 1ª demostración *)
lemma
  assumes "extraccion φ"
  shows   "∀ N N'. ∃ k ≥ N'. φ k ≥ N"
proof (intro allI)
  fix N N' :: nat
  let ?k = "max N N'"
  have "max N N' ≤ ?k"
    by (rule le_refl)
  then have hk : "N ≤ ?k ∧ N' ≤ ?k"
    by (simp only: max.bounded_iff)
  then have "?k ≥ N'"
    by (rule conjunct2)
  moreover
  have "N ≤ φ ?k"
  proof -
    have "N ≤ ?k"
      using hk by (rule conjunct1)
    also have "… ≤ φ ?k"
      using assms by (rule aux)
    finally show "N ≤ φ ?k"
      by this
  qed
  ultimately have "?k ≥ N' ∧ φ ?k ≥ N"
    by (rule conjI)
  then show "∃k ≥ N'. φ k ≥ N"
    by (rule exI)
qed
 
(* 2ª demostración *)
lemma
  assumes "extraccion φ"
  shows   "∀ N N'. ∃ k ≥ N'. φ k ≥ N"
proof (intro allI)
  fix N N' :: nat
  let ?k = "max N N'"
  have "?k ≥ N'"
    by simp
  moreover
  have "N ≤ φ ?k"
  proof -
    have "N ≤ ?k"
      by simp
    also have "… ≤ φ ?k"
      using assms by (rule aux)
    finally show "N ≤ φ ?k"
      by this
  qed
  ultimately show "∃k ≥ N'. φ k ≥ N"
    by blast
qed
 
end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>

Relación entre los índices de las subsucesiones y los de la sucesión

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión

   uₒ, u₂, u₄, u₆, ...

se ha obtenido con la función de extracción φ tal que φ(n) = 2*n.

En Lean, se puede definir que φ es una función de extracción por

   def extraccion (φ : ℕ → ℕ) :=
     ∀ {n m}, n < m → φ n < φ m

Demostrar que si φ es una función de extracción, entonces

   ∀ n, n ≤ φ n

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

import tactic
open nat
 
variable {φ :   }
 
def extraccion (φ :   ) :=
   {n m}, n < m  φ n < φ m
 
example :
  extraccion φ   n, n  φ n :=
sorry
Soluciones con Lean
import tactic
open nat
 
variable {φ :   }
 
set_option pp.structure_projections false
 
def extraccion (φ :   ) :=
   {n m}, n < m  φ n < φ m
 
-- 1ª demostración
example :
  extraccion φ   n, n  φ n :=
begin
  intros h n,
  induction n with m HI,
  { exact nat.zero_le (φ 0), },
  { apply nat.succ_le_of_lt,
    have h1 : m < succ m := lt_add_one m,
    calc m  φ m        : HI
       ... < φ (succ m) : h h1, },
end
 
-- 2ª demostración
example :
  extraccion φ   n, n  φ n :=
begin
  intros h n,
  induction n with m HI,
  { exact nat.zero_le (φ 0), },
  { apply nat.succ_le_of_lt,
    calc m  φ m        : HI
       ... < φ (succ m) : h (lt_add_one m), },
end
 
-- 3ª demostración
example :
  extraccion φ   n, n  φ n :=
assume h : extraccion φ,
assume n,
nat.rec_on n
  ( show 0  φ 0,
      from nat.zero_le (φ 0) )
  ( assume m,
    assume HI : m  φ m,
    have h1 : m < succ m,
      from lt_add_one m,
    have h2 : m < φ (succ m), from
      calc m  φ m        : HI
         ... < φ (succ m) : h h1,
    show succ m  φ (succ m),
      from nat.succ_le_of_lt h2)

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
theory Relacion_entre_los_indices_de_las_subsucesiones_y_de_la_sucesion
imports Main
begin
 
definition extraccion :: "(nat ⇒ nat) ⇒ bool" where
  "extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"
 
(* En la demostración se usará el siguiente lema *)
lemma extraccionE:
  assumes "extraccion φ"
          "n < m"
  shows   "φ n < φ m"
proof -
  have "∀ n m. n < m ⟶ φ n < φ m"
    using assms(1) by (unfold extraccion_def)
  then have "n < m ⟶ φ n < φ m"
    by (elim allE)
  then show "φ n < φ m"
    using assms(2) by (rule mp)
qed
 
(* 1ª demostración *)
lemma
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0"
    by (rule le0)
next
  fix n
  assume "n ≤ φ n"
  also have "φ n < φ (Suc n)"
  proof -
    have "n < Suc n"
      by (rule lessI)
    with assms show "φ n < φ (Suc n)"
      by (rule extraccionE)
  qed
  finally show "Suc n ≤ φ (Suc n)"
    by (rule Suc_leI)
qed
 
(* 2ª demostración *)
lemma
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0"
    by (rule le0)
next
  fix n
  assume "n ≤ φ n"
  also have "… < φ (Suc n)"
  using assms
  proof (rule extraccionE)
    show "n < Suc n"
      by (rule lessI)
  qed
  finally show "Suc n ≤ φ (Suc n)"
    by (rule Suc_leI)
qed
 
(* 3ª demostración *)
lemma
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0"
    by (rule le0)
next
  fix n
  assume "n ≤ φ n"
  also have "… < φ (Suc n)"
    by (rule extraccionE [OF assms lessI])
  finally show "Suc n ≤ φ (Suc n)"
    by (rule Suc_leI)
qed
 
(* 4ª demostración *)
lemma
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0"
    by simp
next
  fix n
  assume HI : "n ≤ φ n"
  also have "φ n < φ (Suc n)"
    using assms extraccion_def by blast
  finally show "Suc n ≤ φ (Suc n)"
    by simp
qed
 
end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>

Las particiones definen relaciones transitivas

Cada familia de conjuntos P define una relación de forma que dos elementos están relacionados si algún conjunto de P contiene a ambos elementos. Se puede definir en Lean por

   def relacion (P : set (set X)) (x y : X) :=
     ∃ A ∈ P, x ∈ A ∧ y ∈ A

Una familia de subconjuntos de X es una partición de X si cada de X pertenece a un único conjunto de P y todos los elementos de P son no vacíos. Se puede definir en Lean por

   def particion (P : set (set X)) : Prop :=
     (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

Demostrar que si P es una partición de X, entonces la relación definida por P es transitiva.

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

import tactic
 
variable {X : Type}
variable (P : set (set X))
 
def relacion (P : set (set X)) (x y : X) :=
   A ∈ P, x ∈ A  y ∈ A
 
def particion (P : set (set X)) : Prop :=
  ( x, ( B ∈ P, x ∈ B   C ∈ P, x ∈ C  B = C))  ∅ ∉ P
 
example
  (h : particion P)
  : transitive (relacion P) :=
sorry
Soluciones con Lean
import tactic
 
variable {X : Type}
variable (P : set (set X))
 
def relacion (P : set (set X)) (x y : X) :=
   A ∈ P, x ∈ A  y ∈ A
 
def particion (P : set (set X)) : Prop :=
  ( x, ( B ∈ P, x ∈ B   C ∈ P, x ∈ C  B = C))  ∅ ∉ P
 
-- 1ª demostración
example
  (h : particion P)
  : transitive (relacion P) :=
begin
  unfold transitive,
  intros x y z h1 h2,
  unfold relacion at *,
  rcases h1 with ⟨B1, hB1P, hxB1, hyB1⟩,
  rcases h2 with ⟨B2, hB2P, hyB2, hzB2⟩,
  use B1,
  repeat { split },
  { exact hB1P, },
  { exact hxB1, },
  { convert hzB2,
    rcases (h.1 y) with ⟨B, -, -, hB⟩,
    have hBB1 : B = B1 := hB B1 hB1P hyB1,
    have hBB2 : B = B2 := hB B2 hB2P hyB2,
    exact eq.trans hBB1.symm hBB2, },
end
 
-- 2ª demostración
example
  (h : particion P)
  : transitive (relacion P) :=
begin
  rintros x y z ⟨B1,hB1P,hxB1,hyB1⟩ ⟨B2,hB2P,hyB2,hzB2⟩,
  use B1,
  repeat { split },
  { exact hB1P, },
  { exact hxB1, },
  { convert hzB2,
    rcases (h.1 y) with ⟨B, -, -, hB⟩,
    exact eq.trans (hB B1 hB1P hyB1).symm (hB B2 hB2P hyB2), },
end
 
-- 3ª demostración
example
  (h : particion P)
  : transitive (relacion P) :=
begin
  rintros x y z ⟨B1,hB1P,hxB1,hyB1⟩ ⟨B2,hB2P,hyB2,hzB2⟩,
  use [B1, ⟨hB1P,
            hxB1,
            by { convert hzB2,
                 rcases (h.1 y) with ⟨B, -, -, hB⟩,
                 exact eq.trans (hB B1 hB1P hyB1).symm
                                (hB B2 hB2P hyB2), }],
end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
theory Las_particiones_definen_relaciones_transitivas
imports Main
begin
 
definition relacion :: "('a set) set ⇒ 'a ⇒ 'a ⇒ bool" where
  "relacion P x y ⟷ (∃A∈P. x ∈ A ∧ y ∈ A)"
 
definition particion :: "('a set) set ⇒ bool" where
  "particion P ⟷ (∀x. (∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))) ∧ {} ∉ P"
 
(* 1ª demostración *)
lemma
  assumes "particion P"
  shows   "transp (relacion P)"
proof (rule transpI)
  fix x y z
  assume "relacion P x y" and "relacion P y z"
  have "∃A∈P. x ∈ A ∧ y ∈ A"
    using ‹relacion P x y›
    by (simp only: relacion_def)
  then obtain A where "A ∈ P" and hA : "x ∈ A ∧ y ∈ A"
    by (rule bexE)
  have "∃B∈P. y ∈ B ∧ z ∈ B"
    using ‹relacion P y z›
    by (simp only: relacion_def)
  then obtain B where "B ∈ P" and hB : "y ∈ B ∧ z ∈ B"
    by (rule bexE)
  have "A = B"
  proof -
    have "∃C ∈ P. y ∈ C ∧ (∀D∈P. y ∈ D ⟶ C = D)"
      using assms
      by (simp only: particion_def)
    then obtain C where "C ∈ P"
                    and hC : "y ∈ C ∧ (∀D∈P. y ∈ D ⟶ C = D)"
      by (rule bexE)
    have hC' : "∀D∈P. y ∈ D ⟶ C = D"
      using hC by (rule conjunct2)
    have "C = A"
      using ‹A ∈ P› hA hC' by simp
    moreover have "C = B"
      using ‹B ∈ P› hB hC by simp
    ultimately show "A = B"
      by (rule subst)
  qed
  then have "x ∈ A ∧ z ∈ A"
    using hA hB by simp
  then have "∃A∈P. x ∈ A ∧ z ∈ A"
    using ‹A ∈ P› by (rule bexI)
  then show "relacion P x z"
    using ‹A = B› ‹A ∈ P›
    by (unfold relacion_def)
qed
 
(* 2ª demostración *)
lemma
  assumes "particion P"
  shows   "transp (relacion P)"
proof (rule transpI)
  fix x y z
  assume "relacion P x y" and "relacion P y z"
  obtain A where "A ∈ P" and hA : "x ∈ A ∧ y ∈ A"
    using ‹relacion P x y›
    by (meson relacion_def)
  obtain B where "B ∈ P" and hB : "y ∈ B ∧ z ∈ B"
    using ‹relacion P y z›
    by (meson relacion_def)
  have "A = B"
  proof -
    obtain C where "C ∈ P" and hC : "y ∈ C ∧ (∀D∈P. y ∈ D ⟶ C = D)"
      using assms particion_def
      by metis
    have "C = A"
      using ‹A ∈ P› hA hC by auto
    moreover have "C = B"
      using ‹B ∈ P› hB hC by auto
    ultimately show "A = B"
      by simp
  qed
  then have "x ∈ A ∧ z ∈ A"
    using hA hB by auto
  then show "relacion P x z"
    using ‹A = B› ‹A ∈ P› relacion_def
    by metis
qed
 
(* 3ª demostración *)
lemma
  assumes "particion P"
  shows   "transp (relacion P)"
  using assms particion_def relacion_def
  by (smt (verit) transpI)
 
end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>

Las familias de conjuntos definen relaciones simétricas

Cada familia de conjuntos P define una relación de forma que dos elementos están relacionados si algún conjunto de P contiene a ambos elementos. Se puede definir en Lean por

   def relacion (P : set (set X)) (x y : X) :=
     ∃ A ∈ P, x ∈ A ∧ y ∈ A

Demostrar que si P es una familia de subconjunt❙os de X, entonces la relación definida por P es simétrica.

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

import tactic
 
variable {X : Type}
variable (P : set (set X))
 
def relacion (P : set (set X)) (x y : X) :=
   A ∈ P, x ∈ A  y ∈ A
 
example : symmetric (relacion P) :=
sorry
Soluciones con Lean
import tactic
 
variable {X : Type}
variable (P : set (set X))
 
def relacion (P : set (set X)) (x y : X) :=
   A ∈ P, x ∈ A  y ∈ A
 
-- 1ª demostración
example : symmetric (relacion P) :=
begin
  unfold symmetric,
  intros x y hxy,
  unfold relacion at *,
  rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩,
  use B,
  repeat { split },
  { exact hBP, },
  { exact hyB, },
  { exact hxB, },
end
 
-- 2ª demostración
example : symmetric (relacion P) :=
begin
  intros x y hxy,
  rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩,
  use B,
  repeat { split } ;
  assumption,
end
 
-- 3ª demostración
example : symmetric (relacion P) :=
begin
  intros x y hxy,
  rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩,
  use [B, ⟨hBP, hyB, hxB⟩],
end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
theory Las_familias_de_conjuntos_definen_relaciones_simetricas
imports Main
begin
 
definition relacion :: "('a set) set ⇒ 'a ⇒ 'a ⇒ bool" where
  "relacion P x y ⟷ (∃A∈P. x ∈ A ∧ y ∈ A)"
 
(* 1ª demostración *)
lemma "symp (relacion P)"
proof (rule sympI)
  fix x y
  assume "relacion P x y"
  then have "∃A∈P. x ∈ A ∧ y ∈ A"
    by (unfold relacion_def)
  then have "∃A∈P. y ∈ A ∧ x ∈ A"
  proof (rule bexE)
    fix A
    assume hA1 : "A ∈ P" and hA2 : "x ∈ A ∧ y ∈ A"
    have "y ∈ A ∧ x ∈ A"
      using hA2 by (simp only: conj_commute)
    then show "∃A∈P. y ∈ A ∧ x ∈ A"
      using hA1 by (rule bexI)
  qed
  then show "relacion P y x"
    by (unfold relacion_def)
qed
 
(* 2ª demostración *)
lemma "symp (relacion P)"
proof (rule sympI)
  fix x y
  assume "relacion P x y"
  then obtain A where "A ∈ P ∧ x ∈ A ∧ y ∈ A"
    using relacion_def
    by metis
  then show "relacion P y x"
    using relacion_def
    by metis
qed
 
(* 3ª demostración *)
lemma "symp (relacion P)"
  using relacion_def
  by (metis sympI)
 
end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>

El conjunto de las clases de equivalencia es una partición

Demostrar que si R es una relación de equivalencia en X, entonces las clases de equivalencia de R es una partición de X.

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

import tactic
 
variable  {X : Type}
variables {x y: X}
variable  {R : X  X  Prop}
 
def clase (R : X  X  Prop) (x : X) :=
  {y : X | R x y}
 
def particion (A : set (set X)) : Prop :=
  ( x, ( B ∈ A, x ∈ B   C ∈ A, x ∈ C  B = C))  ∅ ∉ A
 
example
  (h : equivalence R)
  : particion {a : set X |  s : X, a = clase R s} :=
sorry
Soluciones con Lean
import tactic
 
variable  {X : Type}
variables {x y: X}
variable  {R : X  X  Prop}
 
def clase (R : X  X  Prop) (x : X) :=
  {y : X | R x y}
 
def particion (A : set (set X)) : Prop :=
  ( x, ( B ∈ A, x ∈ B   C ∈ A, x ∈ C  B = C))  ∅ ∉ A
 
lemma aux
  (h : equivalence R)
  (hxy : R x y)
  : clase R y ⊆ clase R x :=
λ z hz, h.2.2 hxy hz
 
-- 1ª demostración
example
  (h : equivalence R)
  : particion {a : set X |  s : X, a = clase R s} :=
begin
  split,
  { simp,
    intro y,
    use (clase R y),
    split,
    { use y, },
    { split,
      { exact h.1 y, },
      { intros x hx,
        apply le_antisymm,
        { exact aux h hx, },
        { exact aux h (h.2.1 hx), }}}},
  { simp,
    intros x hx,
    have h1 : x ∈ clase R x := h.1 x,
    rw ← hx at h1,
    exact set.not_mem_empty x h1, },
end
 
-- 2ª demostración
example
  (h : equivalence R)
  : particion {a : set X |  s : X, a = clase R s} :=
begin
  split,
  { simp,
    intro y,
    use (clase R y),
    split,
    { use y, },
    { split,
      { exact h.1 y, },
      { intros x hx,
        exact le_antisymm (aux h hx) (aux h (h.2.1 hx)), }}},
  { simp,
    intros x hx,
    have h1 : x ∈ clase R x := h.1 x,
    rw ← hx at h1,
    exact set.not_mem_empty x h1, },
end
 
-- 3ª demostración
example
  (h : equivalence R)
  : particion {a : set X |  s : X, a = clase R s} :=
begin
  split,
  { simp,
    intro y,
    use [clase R y,
         ⟨by use y,
          ⟨h.1 y, λ x hx, le_antisymm (aux h hx) (aux h (h.2.1 hx))⟩⟩], },
  { simp,
    intros x hx,
    have h1 : x ∈ clase R x := h.1 x,
    rw ← hx at h1,
    exact set.not_mem_empty x h1, },
end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
theory El_conjunto_de_las_clases_de_equivalencia_es_una_particion
imports Main
begin
 
definition clase :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a set"
  where "clase R x = {y. R x y}"
 
definition particion :: "('a set) set ⇒ bool" where
  "particion P ⟷ (∀x. (∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))) ∧ {} ∉ P"
 
lemma
  fixes   R :: "'a ⇒ 'a ⇒ bool"
  assumes "equivp R"
  shows   "particion (⋃x. {clase R x})" (is "particion ?P")
proof (unfold particion_def; intro conjI)
  show "(∀x. ∃B∈?P. x ∈ B ∧ (∀C∈?P. x ∈ C ⟶ B = C))"
  proof (intro allI)
    fix x
    have "clase R x ∈ ?P"
      by auto
    moreover have "x ∈ clase R x"
      using assms clase_def equivp_def
      by (metis CollectI)
    moreover have "∀C∈?P. x ∈ C ⟶ clase R x = C"
    proof
      fix C
      assume "C ∈ ?P"
      then obtain y where "C = clase R y"
        by auto
      show "x ∈ C ⟶ clase R x = C"
      proof
        assume "x ∈ C"
        then have "R y x"
          using ‹C = clase R y› assms clase_def
          by (metis CollectD)
        then show "clase R x = C"
          using assms ‹C = clase R y› clase_def equivp_def
          by metis
      qed
    qed
    ultimately show "∃B∈?P. x ∈ B ∧ (∀C∈?P. x ∈ C ⟶ B = C)"
      by blast
  qed
next
  show "{} ∉ ?P"
  proof
    assume "{} ∈ ?P"
    then obtain x where "{} = clase R x"
      by auto
    moreover have "x ∈ clase R x"
      using assms clase_def equivp_def
      by (metis CollectI)
    ultimately show False
      by simp
  qed
qed
 
end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>