Pure (theorem prover)

Pure

Paradigm(s)	Functional, Declarative
Designed by	User:Hakerh400
Appeared in	2026
Computational class	Turing complete
Major implementations	Implemented
File extension(s)	.txt

Pure is an interactive theorem prover invented by User:Hakerh400. It is documented in 2026.

Overview

A type can be either Prop (propositions), Set (ZFC sets) and Func (functions, represented as a → b).

A term can be a global identifier, local identifier, lambda abstraction or application. Every term has a type.

A proof can be either a global axiom or theorem, local proof variable, implication introduction/elimination, and universal quantifier introduction/elimination. Every proof has a statement (term whose type is Prop).

Tactics

The prover supports a lot of useful tactics. Tactics include ind for induction, rw for substitution, simp for simplification, etc. All tactics are implemented using a single core tactic: refine, which modifies the proof state continuation in a monadic context that includes access to environment (the collection of all definitions/axioms/theorems introduced so far) and the IO monad.

Example

Here is a proof of the Schröder–Bernstein theorem. It imports some utility library that we developed.

The imported library contains theorems about natural numbers, cardinalities and other set-theoretic constructs.

import data/nat/a/thms

def seq A B f g :=
nat_rec_aux (pair ∅ ∅) # λ n p, let

A' := A \ fst p

B' := B \ snd p

G' := B' \ image f A'

F' := image g G'

in pair (fst p ∪ F') (snd p ∪ G')

def F' A B f g n :=
fst # seq A B f g n

def G' A B f g n :=
snd # seq A B f g n

def F A B f g n :=
ite (n = zero_aux) ∅ # F' A B f g n \ F' A B f g (pred_aux n)

def G A B f g n :=
ite (n = zero_aux) ∅ # G' A B f g n \ G' A B f g (pred_aux n)

def A' A B f g :=
A \ unions (image (F A B f g) Nat_aux)

def B' A B f g :=
B \ unions (image (G A B f g) Nat_aux)

def R A B f g x :=
ite (x ∈ A' A B f g) f (fn_inv g B) x

-----

@[simp]
thm seq_zero : ∀ A B f g, seq A B f g zero_aux = pair ∅ ∅ :=
{ simp seq }

@[simp]
thm F'_zero : ∀ A B f g, F' A B f g zero_aux = ∅ :=
{ simp F' }

thm F'_succ : ∀ A B f g (n ∈ Nat_aux), F' A B f g (succ_aux n) = F' A B f g n ∪

image g (B \ G' A B f g n \ image f (A \ F' A B f g n)) :=

{ simp [F', G', seq] }

@[simp]
thm G'_zero : ∀ A B f g, G' A B f g zero_aux = ∅ :=
{ simp G' }

thm G'_succ : ∀ A B f g (n ∈ Nat_aux), G' A B f g (succ_aux n) = G' A B f g n ∪

(B \ G' A B f g n \ image f (A \ F' A B f g n)) :=

{ simp [F', G', seq] }

thm F'_subset_A : ∀ A B f g [maps_to g B A] (n ∈ Nat_aux), F' A B f g n ⊆ A :=
{ ind n, simp, in x, simp F'_succ at h₃, cs h₃, ap h₁, asm, csr h₃ → y, subst' h₆, ap h₀ }

thm G'_subset_B : ∀ A B f g (n ∈ Nat_aux), G' A B f g n ⊆ B :=
{ ind n, simp, in x, simp G'_succ at h₂, cs h₂, ap h₀, asm, csr h₂, asm }

@[simp]
thm F'_subset_F'_succ : ∀ A B f g (n ∈ Nat_aux), F' A B f g n ⊆ F' A B f g (succ_aux n) :=
{ simp F'_succ }

@[simp]
thm G'_subset_G'_succ : ∀ A B f g (n ∈ Nat_aux), G' A B f g n ⊆ G' A B f g (succ_aux n) :=
{ simp G'_succ }

thm F'_subset_F'_of_le : ∀ A B f g (k n ∈ Nat_aux), nat_le_aux k n → F' A B f g k ⊆ F' A B f g n :=
{ revert k, ind n → k, simp at h₀, simp h₀, in n k, rw nat_le_aux_iff at h₃, cs h₃,

subst h₃, rw nat_lt_aux_succ_iff at h₃, spec h₁ h₃, trans h₁, simp }

thm F'_subset_F'_of_lt : ∀ A B f g (k n ∈ Nat_aux), nat_lt_aux k n → F' A B f g k ⊆ F' A B f g n :=
{ rw nat_lt_aux_iff at h₂, cs h₂, ap F'_subset_F'_of_le h₃ }

thm G'_subset_G'_of_le : ∀ A B f g (k n ∈ Nat_aux), nat_le_aux k n → G' A B f g k ⊆ G' A B f g n :=
{ revert k, ind n → k, simp at h₀, simp h₀, in n k, rw nat_le_aux_iff at h₃, cs h₃,

subst h₃, rw nat_lt_aux_succ_iff at h₃, spec h₁ h₃, trans h₁, simp }

thm G'_subset_G'_of_lt : ∀ A B f g (k n ∈ Nat_aux), nat_lt_aux k n → G' A B f g k ⊆ G' A B f g n :=
{ rw nat_lt_aux_iff at h₂, cs h₂, ap G'_subset_G'_of_le h₃ }

@[simp, tc]
thm A'_subset_A : ∀ A B f g, A' A B f g ⊆ A :=
{ simp A' }

@[simp, tc]
thm B'_subset_B : ∀ A B f g, B' A B f g ⊆ B :=
{ simp B' }

@[simp]
thm G_zero : ∀ A B f g, G A B f g zero_aux = ∅ :=
{ simp G }

@[simp]
thm G_succ : ∀ A B f g (n ∈ Nat_aux), G A B f g (succ_aux n) =

B \ G' A B f g n \ image f (A \ F' A B f g n) :=

{ simp [G, G'_succ], rw union_comm, ap union_dif_eq_of_disjoint, in x, simp at h₁, csr h₁, asm }

@[simp]
thm F_zero : ∀ A B f g, F A B f g zero_aux = ∅ :=
{ simp F }

@[simp, tc]
thm G_subset_B : ∀ A B f g (n ∈ Nat_aux), G A B f g n ⊆ B :=
{ ind n; simp, ap dif_subset_of_subset, simp }

thm F'_eq_image : ∀ A B f g (n ∈ Nat_aux), F' A B f g n = image g (G' A B f g n) :=
{ ind n, simp, simp [F'_succ, G'_succ, h₀] }

thm image_mem_F'_of_mem_G' : ∀ A B f g y (n ∈ Nat_aux), y ∈ G' A B f g n → g y ∈ F' A B f g n :=
{ rw F'_eq_image, ap app_mem_image h₁ }

thm image_mem_F'_iff_mem_G' : ∀ A B f g [inj g B A] (n ∈ Nat_aux) (y ∈ B),

g y ∈ F' A B f g n ↔ y ∈ G' A B f g n :=

{ hv h₁, clear h₁, symm, split, ap image_mem_F'_of_mem_G' h₂ h₃, ind n,

simpa at h₂ ⊢, simp [F'_succ, G'_succ] at h₃ ⊢, cs h₃, left, ex h₂ h₃,

right, csr h₃ → z, cs h₀, spec h₁ h₇, subst h₁, clear h₁ h₂ h₆, simpa [h₁, h₂] }

thm mem_G'_iff_image_mem_F' : ∀ A B f g [inj g B A] (n ∈ Nat_aux) (y ∈ B),

y ∈ G' A B f g n ↔ g y ∈ F' A B f g n :=

{ rw image_mem_F'_iff_mem_G' }

thm mem_G'_of_mem_G : ∀ A B f g (n ∈ Nat_aux) y, y ∈ G A B f g n → y ∈ G' A B f g n :=
{ cs n, simpa at *, simp G'_succ at h₁ ⊢, right h₁ }

thm mem_F'_of_mem_F : ∀ A B f g (n ∈ Nat_aux) x, x ∈ F A B f g n → x ∈ F' A B f g n :=
{ cs n, simpa at *, simp [F, F'_succ] at h₁ ⊢, cs h₁, simp h₂ at h₁, clear h₂, right h₁ }

thm not_lt_mem_G'_of_mem_G : ∀ A B f [inj f A B] g [inj g B A] (n k ∈ Nat_aux) y,

nat_lt_aux k n → y ∈ G A B f g n → ¬(y ∈ G' A B f g k) :=

{ cs n, simp at h₄, elim h₄, simp at h₄ h₅ ⊢, csr h₅, cpos h₆,

hv G'_subset_G'_of_le, rw subset at h₈, ap h₈ h₄, asm }

thm not_lt_mem_F'_of_mem_F : ∀ A B f [inj f A B] g [inj g B A] (n k ∈ Nat_aux) x,

nat_lt_aux k n → x ∈ F A B f g n → ¬(x ∈ F' A B f g k) :=

{ cs n, simp at h₄, elim h₄, simp at h₄, simp F at h₅, cs h₅, cpos h₆,

hv F'_subset_F'_of_le, rw subset at h₇, ap h₇ h₄, asm }

thm mem_G_iff_mem_G'_least : ∀ A B f [inj f A B] g [inj g B A] (n ∈ Nat_aux) y,

y ∈ G A B f g n ↔ y ∈ G' A B f g n ∧ ∀ (k ∈ Nat_aux), nat_lt_aux k n → ¬(y ∈ G' A B f g k) :=

{ symm, split, { cs h₃, cs n, simpa at h₂ ⊢, spec h₄ h₂ _; simp [G'_succ, G, h₄],

simpa [G'_succ, h₄] at h₃ }, use mem_G'_of_mem_G h₃, in k, ap not_lt_mem_G'_of_mem_G h₅ h₃ }

thm mem_F_iff_mem_F'_least : ∀ A B f [inj f A B] g [inj g B A] (n ∈ Nat_aux) x,

x ∈ F A B f g n ↔ x ∈ F' A B f g n ∧ ∀ (k ∈ Nat_aux), nat_lt_aux k n → ¬(x ∈ F' A B f g k) :=

{ symm, split, { cs h₃, cs n, simpa at h₂ ⊢, spec h₄ h₂ _, simp, simp [F'_succ, F, h₄],

simp F'_succ at h₃, simpa h₄ at h₃ }, use mem_F'_of_mem_F h₃, in k, ap not_lt_mem_F'_of_mem_F h₅ h₃ }

thm disjoint_G : ∀ A B f [inj f A B] g [inj g B A] (m n ∈ Nat_aux),

¬(m = n) → disjoint (G A B f g m) (G A B f g n) :=

{ revert n, revert m, iter 2 rw ←tc_univ, ex nat_lt_aux_wlog ⊢|01011 _ _,

{ rw disjoint_comm, simp tc_univ }, in m n y, in, rw mem_G_iff_mem_G'_least at h₆,

cs h₆, ap h₇ h₄, ap mem_G'_of_mem_G h₅ }

thm disjoint_F : ∀ A B f [inj f A B] g [inj g B A] (m n ∈ Nat_aux),

¬(m = n) → disjoint (F A B f g m) (F A B f g n) :=

{ revert n, revert m, iter 2 rw ←tc_univ, ex nat_lt_aux_wlog ⊢|01011 _ _,

{ rw disjoint_comm, simp tc_univ }, in m n x, in, rw mem_F_iff_mem_F'_least at h₆,

cs h₆, ap h₇ h₄, ap mem_F'_of_mem_F h₅ }

thm mem_G'_succ_of_mem_G' : ∀ A B f g (n ∈ Nat_aux) y,

y ∈ G' A B f g n → y ∈ G' A B f g (succ_aux n) :=

{ hv G'_subset_G'_of_le, rw subset at h₂, ap h₂, simp, asm }

thm mem_F'_succ_of_mem_F' : ∀ A B f g (n ∈ Nat_aux) x,

x ∈ F' A B f g n → x ∈ F' A B f g (succ_aux n) :=

{ hv F'_subset_F'_of_le, rw subset at h₂, ap h₂, simp, asm }

thm exi_mem_G'_of_mem_F' : ∀ A B f [inj f A B] g [inj g B A] (n ∈ Nat_aux) x,

x ∈ F' A B f g n → ∃ y, y ∈ G' A B f g n ∧ g y = x :=

{ ind n, simp at h₂, elim h₂, simp F'_succ at h₃, cs h₃,

{ spec h₂ h₃, csr h₂ → y, use y, symm, use h₃, ap mem_G'_succ_of_mem_G' h₂ },

csr h₃ → y, use y, symm, use h₆, simpa [G'_succ, h₄, h₃] }

@[simp]
thm F_eq_image : ∀ A B f [inj f A B] g [inj g B A] (n ∈ Nat_aux), F A B f g n = image g (G A B f g n) :=
{ cs n, simp, rw [F, succ_aux_ne_zero_aux, ite_false, pred_aux_succ_aux], ext x,

rw mem_dif, split, { cs h₃, simp, simpa [F'_succ, h₄] at h₃ }, simp at h₃, split,

simp F'_succ, right h₃, cpos h₃, simp, in y, in, subst' h₇, csr' exi_mem_G'_of_mem_F' h₃ → y',

cs h₁, hv G'_subset_B, rw subset at h₁₀, spec h₁₀ h₈, spec h₂ h₉, subst h₂, contra h₅ h₇ }

@[simp, tc]
thm F_subset_A : ∀ A B f [inj f A B] g [inj g B A] (n ∈ Nat_aux), F A B f g n ⊆ A :=
{ in x, simp at h₃, csr h₃ → y, subst' h₄, hv G_subset_B, rw subset at h₄, spec h₄ h₃, cs h₁, ap h₁ }

thm G'_eq_rec : ∀ A B f g (n ∈ Nat_aux), G' A B f g n =

nat_rec_aux ∅ (λ k a, a ∪ G A B f g k) (succ_aux n) :=

{ ind n, simp, simp G'_succ at h₀ ⊢, rw h₀ }

thm F'_eq_rec : ∀ A B f [inj f A B] g [inj g B A] (n ∈ Nat_aux), F' A B f g n =

nat_rec_aux ∅ (λ k a, a ∪ F A B f g k) (succ_aux n) :=

{ ind n, simp, simp F'_succ at h₂ ⊢, rw h₂ }

thm G'_succ_eq_rec : ∀ A B f g (n ∈ Nat_aux), G' A B f g (succ_aux n) =

G' A B f g n ∪ G A B f g (succ_aux n) :=

{ simp G'_succ }

thm F'_succ_eq_rec : ∀ A B f [inj f A B] g [inj g B A] (n ∈ Nat_aux), F' A B f g (succ_aux n) =

F' A B f g n ∪ F A B f g (succ_aux n) :=

{ simp F'_succ }

@[simp]
thm mem_A' : ∀ A B f g (x ∈ A), x ∈ A' A B f g ↔ ∀ (n ∈ Nat_aux), ¬(x ∈ F A B f g n) :=
{ simp A', split, { cs h₁, in n, ap h₂, use n, simp h₃ },

use h₀, in s, csr h₂ → n, subst' h₃, ap h₁ }

@[simp]
thm mem_B' : ∀ A B f g (x ∈ B), x ∈ B' A B f g ↔ ∀ (n ∈ Nat_aux), ¬(x ∈ G A B f g n) :=
{ simp B', split, { cs h₁, in n, ap h₂, use n, simp h₃ },

use h₀, in s, csr h₂ → n, subst' h₃, ap h₁ }

@[tc]
thm bij_G_F : ∀ A B f [inj f A B] g [inj g B A] (n ∈ Nat_aux),

bij g (G A B f g n) (F A B f g n) :=

{ hv inj g (G A B f g n) A, ap inj_of_subset_dom h₁, simp, ap bij_image_of_inj }

thm G_succ_eq_dif : ∀ A B f g (n ∈ Nat_aux),

G A B f g (succ_aux n) = G' A B f g (succ_aux n) \ G' A B f g n :=

{ rw G, simp }

thm F_succ_eq_dif : ∀ A B f g (n ∈ Nat_aux),

F A B f g (succ_aux n) = F' A B f g (succ_aux n) \ F' A B f g n :=

{ rw F, simp }

@[tc]
thm disjoint_G'_G_succ : ∀ A B f g (n ∈ Nat_aux), disjoint (G' A B f g n) (G A B f g (succ_aux n)) :=
{ rw G_succ_eq_dif, tc }

@[tc]
thm disjoint_F'_F_succ : ∀ A B f g (n ∈ Nat_aux), disjoint (F' A B f g n) (F A B f g (succ_aux n)) :=
{ rw F_succ_eq_dif, tc }

thm bij_A'_B'_aux₁ : ∀ A B f [inj f A B] g [inj g B A] (x ∈ A),

(∀ (n ∈ Nat_aux), ¬(f x ∈ G A B f g n)) → x ∈ A' A B f g :=

{ rw mem_A', cpos h₃, simp at h₃ ⊢, csr h₃ → n, byc, simp at h₅, hv f x ∈ B,

{ cs h₀, spec h₀ h₃, asm }, hv f x ∈ G A B f g (succ_aux n),

{ simp h₆, split,

{ cpos h₅, csr' nat_aux_exi_least (λ n, f x ∈ G' A B f g n) h₅ → m,

simp, use m, rw mem_G_iff_mem_G'_least, split; asm },

in x', cs h₀, spec h₁ h₉, subst h₁, ap mem_F'_of_mem_F h₄ }, contra h₅ h₇ }

@[tc]
thm bij_A'_B' : ∀ A B f [inj f A B] g [inj g B A], bij f (A' A B f g) (B' A B f g) :=
{ split,

{ in x, hv x ∈ A, { hv A'_subset_A, rw subset at h₃, ex h₃ h₂ },

hv f x ∈ B, { cs h₀, spec h₀ h₄, asm }, simp at h₂ ⊢, cpos h₂, simp at h₂ ⊢,

csr h₂ → n, cs n, simp at h₄, elim h₄, simp at h₃, csr h₃, spec h₅ h₆ rfl*,

csr' nat_aux_exi_least (λ n, x ∈ F' A B f g n) h₅ → m, use m,

rw mem_F_iff_mem_F'_least, split; asm }, split,

{ in x y, hv A'_subset_A, rw subset at h₅, hv h₅ h₂, hv h₅ h₃, cs h₀, spec h₁ h₅, asm },

in y, hv y ∈ B, { hv B'_subset_B, rw subset at h₃, ex h₃ h₂ },

rw mem_B' at h₂, by_cases ∃ (x ∈ A), f x = y,

{ csr h₄ → x, subst' h₅, hv @bij_A'_B'_aux₁ A B f h₀ g h₁ x h₄ @h₂, use x },

push_neg at h₄, spec @h₂ (succ_aux zero_aux) _, simp at h₂,

spec h₂ h₃, csr h₂ → x, contra h₃ h₅ }

@[tc]
thm bij_R_A'_B' : ∀ A B f [inj f A B] g [inj g B A], bij (R A B f g) (A' A B f g) (B' A B f g) :=
{ csr' bij_A'_B' h₀ h₁, split, { in x, simp [R, h₅], ap h₂ }, split,

{ in x y,simp [R, h₅, h₆] at h₇, ap h₃, asm },

in y, spec h₄ h₅, csr h₄ → x, use x, simpa [R, h₄] }

@[tc]
thm bij_fn_inv_g_F_G : ∀ A B f [inj f A B] g [inj g B A] (n ∈ Nat_aux),

bij (fn_inv g B) (F A B f g n) (G A B f g n) :=

{ hv bij_G_F h₀ h₁ h₂, csr h₃, hv ∀ (x ∈ F A B f g n), fn_inv g B x ∈ G A B f g n,

{ in x, rw fn_inv, spec h₅ h₆, csr h₅ → y, subst' h₆, tau y, simp, hv G_subset_B,

rw subset at h₇, ap h₇ h₅, cs h₇, let x := h₇|0, subst' h₉, hv G_subset_B,

rw subset at h₉, spec h₉ h₅, cs h₁, spec h₂ h₉, rwa h₂ },

hv ∀ (y ∈ G A B f g n), fn_inv g B (g y) = y,

{ in y, rw fn_inv, tau y, simp, hv G_subset_B, rw subset at h₈, ap h₈ h₇,

cs h₈, spec h₃ h₇, spec h₆ h₃, rw fn_inv at h₆, spec h₄ h₉, asm },

split, in x, tc, split,

{ in x₁ x₂, hv h₅, spec h₅ h₈, spec h₁₁ h₉, csr h₅ → y₁,

csr h₁₂ → y₂, subst' h₆ h₁₃, simp h₇ at h₁₀, rw h₁₀ },

in y, use g y, split, ap h₃, asm }

@[tc]
thm bij_R_F_G : ∀ A B f [inj f A B] g [inj g B A] (n ∈ Nat_aux),

bij (R A B f g) (F A B f g n) (G A B f g n) :=

{ hv bij_fn_inv_g_F_G h₀ h₁ h₂, csr h₃,

hv ∀ (x ∈ F A B f g n), R A B f g x = fn_inv g B x,

{ in x, rw R, ap @cong_fn (ite ⊢|00 ⊢|01 ⊢|02) ⊢|02, ap ite_neg,

hv F_subset_A, rw subset at h₇, spec h₇ h₆, simp, use n, asm },

split, in x, rw h₆, ap h₃, split, { in x₁ x₂, simp only h₆ at h₉, ap h₄, asm },

in y, spec h₅ h₇, csr h₅ → x, use x, rwa h₇ }

thm mem_dif_A' : ∀ A B f [inj f A B] g [inj g B A] x,

x ∈ A \ A' A B f g ↔ ∃ (n ∈ Nat_aux), x ∈ F A B f g n :=

{ simp, split, cs h₂, simpa at h₃, csr h₂ → n, hv x ∈ A,

hv F_subset_A, rw subset at h₄, ap h₄ h₃, use h₄, simp, use n, asm }

thm mem_dif_B' : ∀ A B f [inj f A B] g [inj g B A] y,

y ∈ B \ B' A B f g ↔ ∃ (n ∈ Nat_aux), y ∈ G A B f g n :=

{ simp, split, cs h₂, simpa at h₃, csr h₂ → n, hv y ∈ B,

hv G_subset_B, rw subset at h₄, ap h₄ h₃, use h₄, simp, use n, asm }

thm bij_R_dif_A'_dif_B'_aux₁ : ∀ A B f [inj f A B] g [inj g B A] (n₁ n₂ ∈ Nat_aux)

(x₁ ∈ F A B f g n₁) (x₂ ∈ F A B f g n₂), R A B f g x₁ = R A B f g x₂ → n₁ = n₂ :=

{ hv F_subset_A h₀ h₁, rw subset at h₇, hv h₇ h₄, hv h₇ h₅, hv ¬(x₁ ∈ A' A B f g),

simp, use n₁, asm, hv ¬(x₂ ∈ A' A B f g), simp, use n₂, asm,

simp only [R, h₁₀, h₁₁] at h₆, simp at h₆, hv bij_fn_inv_g_F_G h₀ h₁,

csr' h₁₂ h₂, csr' h₁₂ h₃, spec h₁₃ h₄, spec h₁₆ h₅, rw ←h₆ at h₁₆,

byc, hv disjoint_G h₁₉, spec h₂₀ h₁₃, contra h₁₆ h₂₀ }

@[tc]
thm bij_R_dif_A'_dif_B' : ∀ A B f [inj f A B] g [inj g B A],

bij (R A B f g) (A \ A' A B f g) (B \ B' A B f g) :=

{ hv bij_R_F_G h₀ h₁, split,

{ in x, rw mem_dif_A' at h₃, csr h₃ → n, spec h₂ h₃,

csr h₂, rw mem_dif_B', use n, ap h₂ }, split,

{ in x₁ x₂, rw mem_dif_A' at h₃ h₄, csr h₃ → n, csr h₅ → n', hv n = n',

ap bij_R_dif_A'_dif_B'_aux₁ h₇, subst' h₈, spec h₂ h₃, csr h₂, spec h₃ h₉, asm },

in y, rw mem_dif_B' at h₃, csr h₃ → n, spec h₂ h₃, csr h₂, spec h₄ h₆,

csr h₄ → x, use x, split, rw mem_dif_A', use n, asm, asm }

@[tc]
thm bij_R_A_B : ∀ A B f [inj f A B] g [inj g B A], bij (R A B f g) A B :=
{ let A₁ := A' A B f g, let B₁ := B' A B f g, let A₂ := A \ A₁, let B₂ := B \ B₁,

hv bij_R_A'_B' h₀ h₁, hv bij_R_dif_A'_dif_B' h₀ h₁, clear h₀ h₁,

simp [←h₀, ←h₁, ←h₂, ←h₃] at h₄ h₅, let r := R A B f g, subst' h₆,

hv ∀ (x ∈ A), x ∈ A₁ ∨ x ∈ A₂, { in x, simp [h₂, h₆] },

hv ∀ (y ∈ B), y ∈ B₁ ∨ y ∈ B₂, { in y, simp [h₃, h₇] },

hv disjoint A₁ A₂, { simp [h₀, h₂] }, hv disjoint B₁ B₂, { simp [h₁, h₃] },

hv A₁ ⊆ A, simp h₀, hv B₁ ⊆ B, simp h₁, hv A₂ ⊆ A, simp h₂, hv B₂ ⊆ B, simp h₃,

clear h₀ h₁ h₂ h₃, rw [subset, ←tc_univ] at h₆ h₇ h₈ h₉, csr h₀, csr h₃, split,

{ in x, cs' h₆ h₁₄; clear h₁₄, spec h₀ h₁₄, asm, spec h₃ h₁₄, asm }, split,

{ in x y, cs' h₆ h₁₄; clear h₁₄,

{ cs' h₆ h₁₄; clear h₁₄, spec h₁ h₁₄, asm, spec h₀ h₁₅, spec h₃ h₁₆,

subst h₁₄, spec h₉ h₀, contra h₃ h₉ }, cs' h₆ h₁₄; clear h₁₄,

{ spec h₃ h₁₅, spec h₀ h₁₆, subst h₁₄, spec h₉ h₀, contra h₃ h₉ },

spec h₄ h₁₄, asm }, in y, cs' h₇ h₁₄; clear h₁₄,

{ spec h₂ h₁₄, csr h₂ → x, use x, asm }, spec h₅ h₁₄, csr h₅ → x, use x, asm }

thm exi_bij_of_exi_inj : ∀ A B, exi_inj A B → exi_inj B A → exi_bij A B :=
{ cs h₀ → f, cs h₁ → g, use R A B f g,

hv A' A B f g ∪ (A \ A' A B f g) = A, ap union_dif_self, ap A'_subset_A,

hv B' A B f g ∪ (B \ B' A B f g) = B, ap union_dif_self, ap B'_subset_B,

rw 1 ←h₂, rw 3 ←h₃, ap bij_union_union_of }

External resources

• Implementation