internlm/Lean-Github huggingface dataset:
Theorem: HTPI.unbdd_subset_nat_match
Proof state before:
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ rel_within (enum A) (Univ ℕ) A ∧ fcnl_on (enum A) (Univ ℕ) ∧ fcnl_on (invRel (enum A)) A
Tactic:
apply And.intro
Proof state after:
case left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ rel_within (enum A) (Univ ℕ) A

case right
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ fcnl_on (enum A) (Univ ℕ) ∧ fcnl_on (invRel (enum A)) A
Theorem: HTPI.unbdd_subset_nat_match
Proof state before:
case left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ rel_within (enum A) (Univ ℕ) A
Tactic:
define
Proof state after:
case left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ ∀ ⦃x y : ℕ⦄, enum A x y → x ∈ Univ ℕ ∧ y ∈ A
Theorem: HTPI.unbdd_subset_nat_match
Proof state before:
case left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ ∀ ⦃x y : ℕ⦄, enum A x y → x ∈ Univ ℕ ∧ y ∈ A
Tactic:
fix s : Nat
Proof state after:
case left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
⊢ ∀ ⦃y : ℕ⦄, enum A s y → s ∈ Univ ℕ ∧ y ∈ A
Theorem: HTPI.unbdd_subset_nat_match
Proof state before:
case left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
⊢ ∀ ⦃y : ℕ⦄, enum A s y → s ∈ Univ ℕ ∧ y ∈ A
Tactic:
fix n : Nat
Proof state after:
case left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s n : ℕ
⊢ enum A s n → s ∈ Univ ℕ ∧ n ∈ A
Theorem: HTPI.unbdd_subset_nat_match
Proof state before:
case left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s n : ℕ
⊢ enum A s n → s ∈ Univ ℕ ∧ n ∈ A
Tactic:
assume h2 : enum A s n
Proof state after:
case left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s n : ℕ
h2 : enum A s n
⊢ s ∈ Univ ℕ ∧ n ∈ A
Theorem: HTPI.unbdd_subset_nat_match
Proof state before:
case left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s n : ℕ
h2 : enum A s n
⊢ s ∈ Univ ℕ ∧ n ∈ A
Tactic:
define at h2
Proof state after:
case left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s n : ℕ
h2 : n ∈ A ∧ num_elts_below A n s
⊢ s ∈ Univ ℕ ∧ n ∈ A
Theorem: HTPI.unbdd_subset_nat_match
Proof state before:
case left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s n : ℕ
h2 : n ∈ A ∧ num_elts_below A n s
⊢ s ∈ Univ ℕ ∧ n ∈ A
Tactic:
apply And.intro (elt_Univ s) h2.left
Proof state after:
no goals
Theorem: HTPI.unbdd_subset_nat_match
Proof state before:
case right
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ fcnl_on (enum A) (Univ ℕ) ∧ fcnl_on (invRel (enum A)) A
Tactic:
apply And.intro
Proof state after:
case right.left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ fcnl_on (enum A) (Univ ℕ)

case right.right
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ fcnl_on (invRel (enum A)) A
Theorem: HTPI.unbdd_subset_nat_match
Proof state before:
case right.left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ fcnl_on (enum A) (Univ ℕ)
Tactic:
show fcnl_on (enum A) (Univ Nat) from enum_fcnl_of_unbdd h1
Proof state after:
no goals
Theorem: HTPI.unbdd_subset_nat_match
Proof state before:
case right.right
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ fcnl_on (invRel (enum A)) A
Tactic:
show fcnl_on (invRel (enum A)) A from inv_enum_fcnl A
Proof state after:
no goals
Theorem: HTPI.subset_nat_ctble
Proof state before:
A : Set ℕ
⊢ ctble A
Tactic:
define
Proof state after:
A : Set ℕ
⊢ finite A ∨ denum A
Theorem: HTPI.subset_nat_ctble
Proof state before:
A : Set ℕ
⊢ finite A ∨ denum A
Tactic:
by_cases h1 : ∃ (m : Nat), ∀ n ∈ A, n < m
Proof state after:
case pos
A : Set ℕ
h1 : ∃ m, ∀ n ∈ A, n < m
⊢ finite A ∨ denum A

case neg
A : Set ℕ
h1 : ¬∃ m, ∀ n ∈ A, n < m
⊢ finite A ∨ denum A
Theorem: HTPI.subset_nat_ctble
Proof state before:
case pos
A : Set ℕ
h1 : ∃ m, ∀ n ∈ A, n < m
⊢ finite A ∨ denum A
Tactic:
apply Or.inl
Proof state after:
case pos.h
A : Set ℕ
h1 : ∃ m, ∀ n ∈ A, n < m
⊢ finite A
Theorem: HTPI.subset_nat_ctble
Proof state before:
case pos.h
A : Set ℕ
h1 : ∃ m, ∀ n ∈ A, n < m
⊢ finite A
Tactic:
obtain (m : Nat) (h2 : ∀ n ∈ A, n < m) from h1
Proof state after:
case pos.h
A : Set ℕ
h1 : ∃ m, ∀ n ∈ A, n < m
m : ℕ
h2 : ∀ n ∈ A, n < m
⊢ finite A
Theorem: HTPI.subset_nat_ctble
Proof state before:
case pos.h
A : Set ℕ
h1 : ∃ m, ∀ n ∈ A, n < m
m : ℕ
h2 : ∀ n ∈ A, n < m
⊢ finite A
Tactic:
obtain (s : Nat) (h3 : num_elts_below A m s) from neb_exists A m
Proof state after:
case pos.h
A : Set ℕ
h1 : ∃ m, ∀ n ∈ A, n < m
m : ℕ
h2 : ∀ n ∈ A, n < m
s : ℕ
h3 : num_elts_below A m s
⊢ finite A
Theorem: HTPI.subset_nat_ctble
Proof state before:
case pos.h
A : Set ℕ
h1 : ∃ m, ∀ n ∈ A, n < m
m : ℕ
h2 : ∀ n ∈ A, n < m
s : ℕ
h3 : num_elts_below A m s
⊢ finite A
Tactic:
apply Exists.intro s
Proof state after:
case pos.h
A : Set ℕ
h1 : ∃ m, ∀ n ∈ A, n < m
m : ℕ
h2 : ∀ n ∈ A, n < m
s : ℕ
h3 : num_elts_below A m s
⊢ I s ∼ A
Theorem: HTPI.subset_nat_ctble
Proof state before:
case pos.h
A : Set ℕ
h1 : ∃ m, ∀ n ∈ A, n < m
m : ℕ
h2 : ∀ n ∈ A, n < m
s : ℕ
h3 : num_elts_below A m s
⊢ I s ∼ A
Tactic:
show I s ∼ A from bdd_subset_nat h2 h3
Proof state after:
no goals
Theorem: HTPI.subset_nat_ctble
Proof state before:
case neg
A : Set ℕ
h1 : ¬∃ m, ∀ n ∈ A, n < m
⊢ finite A ∨ denum A
Tactic:
apply Or.inr
Proof state after:
case neg.h
A : Set ℕ
h1 : ¬∃ m, ∀ n ∈ A, n < m
⊢ denum A
Theorem: HTPI.subset_nat_ctble
Proof state before:
case neg.h
A : Set ℕ
h1 : ¬∃ m, ∀ n ∈ A, n < m
⊢ denum A
Tactic:
push_neg at h1
Proof state after:
case neg.h
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, m ≤ n
⊢ denum A
Theorem: HTPI.subset_nat_ctble
Proof state before:
case neg.h
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, m ≤ n
⊢ denum A
Tactic:
show denum A from unbdd_subset_nat h1
Proof state after:
no goals
Theorem: HTPI.ctble_iff_equinum_set_nat
Proof state before:
U : Type
A : Set U
⊢ ctble A ↔ ∃ I, I ∼ A
Tactic:
apply Iff.intro
Proof state after:
case mp
U : Type
A : Set U
⊢ ctble A → ∃ I, I ∼ A

case mpr
U : Type
A : Set U
⊢ (∃ I, I ∼ A) → ctble A
Theorem: HTPI.ctble_iff_equinum_set_nat
Proof state before:
case mp
U : Type
A : Set U
⊢ ctble A → ∃ I, I ∼ A
Tactic:
assume h1 : ctble A
Proof state after:
case mp
U : Type
A : Set U
h1 : ctble A
⊢ ∃ I, I ∼ A
Theorem: HTPI.ctble_iff_equinum_set_nat
Proof state before:
case mp
U : Type
A : Set U
h1 : ctble A
⊢ ∃ I, I ∼ A
Tactic:
define at h1
Proof state after:
case mp
U : Type
A : Set U
h1 : finite A ∨ denum A
⊢ ∃ I, I ∼ A
Theorem: HTPI.ctble_iff_equinum_set_nat
Proof state before:
case mp
U : Type
A : Set U
h1 : finite A ∨ denum A
⊢ ∃ I, I ∼ A
Tactic:
by_cases on h1
Proof state after:
case mp.Case_1
U : Type
A : Set U
h1 : finite A
⊢ ∃ I, I ∼ A

case mp.Case_2
U : Type
A : Set U
h1 : denum A
⊢ ∃ I, I ∼ A
Theorem: HTPI.ctble_iff_equinum_set_nat
Proof state before:
case mp.Case_1
U : Type
A : Set U
h1 : finite A
⊢ ∃ I, I ∼ A
Tactic:
define at h1
Proof state after:
case mp.Case_1
U : Type
A : Set U
h1 : ∃ n, I n ∼ A
⊢ ∃ I, I ∼ A
Theorem: HTPI.ctble_iff_equinum_set_nat
Proof state before:
case mp.Case_1
U : Type
A : Set U
h1 : ∃ n, I n ∼ A
⊢ ∃ I, I ∼ A
Tactic:
obtain (n : Nat) (h2 : I n ∼ A) from h1
Proof state after:
case mp.Case_1
U : Type
A : Set U
h1 : ∃ n, I n ∼ A
n : ℕ
h2 : I n ∼ A
⊢ ∃ I, I ∼ A
Theorem: HTPI.ctble_iff_equinum_set_nat
Proof state before:
case mp.Case_1
U : Type
A : Set U
h1 : ∃ n, I n ∼ A
n : ℕ
h2 : I n ∼ A
⊢ ∃ I, I ∼ A
Tactic:
show ∃ (I : Set Nat), I ∼ A from Exists.intro (I n) h2
Proof state after:
no goals
Theorem: HTPI.ctble_iff_equinum_set_nat
Proof state before:
case mp.Case_2
U : Type
A : Set U
h1 : denum A
⊢ ∃ I, I ∼ A
Tactic:
rewrite [denum_def] at h1
Proof state after:
case mp.Case_2
U : Type
A : Set U
h1 : Univ ℕ ∼ A
⊢ ∃ I, I ∼ A
Theorem: HTPI.ctble_iff_equinum_set_nat
Proof state before:
case mp.Case_2
U : Type
A : Set U
h1 : Univ ℕ ∼ A
⊢ ∃ I, I ∼ A
Tactic:
show ∃ (I : Set Nat), I ∼ A from Exists.intro (Univ Nat) h1
Proof state after:
no goals
Theorem: HTPI.ctble_iff_equinum_set_nat
Proof state before:
case mpr
U : Type
A : Set U
⊢ (∃ I, I ∼ A) → ctble A
Tactic:
assume h1 : ∃ (I : Set Nat), I ∼ A
Proof state after:
case mpr
U : Type
A : Set U
h1 : ∃ I, I ∼ A
⊢ ctble A
Theorem: HTPI.ctble_iff_equinum_set_nat
Proof state before:
case mpr
U : Type
A : Set U
h1 : ∃ I, I ∼ A
⊢ ctble A
Tactic:
obtain (I : Set Nat) (h2 : I ∼ A) from h1
Proof state after:
case mpr
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
⊢ ctble A
Theorem: HTPI.ctble_iff_equinum_set_nat
Proof state before:
case mpr
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
⊢ ctble A
Tactic:
have h3 : ctble I := subset_nat_ctble I
Proof state after:
case mpr
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
h3 : ctble I
⊢ ctble A
Theorem: HTPI.ctble_iff_equinum_set_nat
Proof state before:
case mpr
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
h3 : ctble I
⊢ ctble A
Tactic:
show ctble A from ctble_of_equinum_ctble h2 h3
Proof state after:
no goals
Theorem: HTPI.Theorem_8_1_5_1_to_2
Proof state before:
U : Type
A : Set U
h1 : ctble A
⊢ ∃ R, fcnl_onto_from_nat R A
Tactic:
rewrite [ctble_iff_equinum_set_nat] at h1
Proof state after:
U : Type
A : Set U
h1 : ∃ I, I ∼ A
⊢ ∃ R, fcnl_onto_from_nat R A
Theorem: HTPI.Theorem_8_1_5_1_to_2
Proof state before:
U : Type
A : Set U
h1 : ∃ I, I ∼ A
⊢ ∃ R, fcnl_onto_from_nat R A
Tactic:
obtain (I : Set Nat) (h2 : I ∼ A) from h1
Proof state after:
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
⊢ ∃ R, fcnl_onto_from_nat R A
Theorem: HTPI.Theorem_8_1_5_1_to_2
Proof state before:
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
⊢ ∃ R, fcnl_onto_from_nat R A
Tactic:
obtain (R : Rel Nat U) (h3 : matching R I A) from h2
Proof state after:
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : matching R I A
⊢ ∃ R, fcnl_onto_from_nat R A
Theorem: HTPI.Theorem_8_1_5_1_to_2
Proof state before:
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : matching R I A
⊢ ∃ R, fcnl_onto_from_nat R A
Tactic:
define at h3
Proof state after:
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
⊢ ∃ R, fcnl_onto_from_nat R A
Theorem: HTPI.Theorem_8_1_5_1_to_2
Proof state before:
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
⊢ ∃ R, fcnl_onto_from_nat R A
Tactic:
apply Exists.intro R
Proof state after:
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
⊢ fcnl_onto_from_nat R A
Theorem: HTPI.Theorem_8_1_5_1_to_2
Proof state before:
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
⊢ fcnl_onto_from_nat R A
Tactic:
define
Proof state after:
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
⊢ unique_val_on_N R ∧ nat_rel_onto R A
Theorem: HTPI.Theorem_8_1_5_1_to_2
Proof state before:
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
⊢ unique_val_on_N R ∧ nat_rel_onto R A
Tactic:
apply And.intro
Proof state after:
case left
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
⊢ unique_val_on_N R

case right
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
⊢ nat_rel_onto R A
Theorem: HTPI.Theorem_8_1_5_1_to_2
Proof state before:
case left
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
⊢ unique_val_on_N R
Tactic:
define
Proof state after:
case left
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
⊢ ∀ ⦃n : ℕ⦄ ⦃x1 x2 : U⦄, R n x1 → R n x2 → x1 = x2
Theorem: HTPI.Theorem_8_1_5_1_to_2
Proof state before:
case left
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
⊢ ∀ ⦃n : ℕ⦄ ⦃x1 x2 : U⦄, R n x1 → R n x2 → x1 = x2
Tactic:
fix n : Nat
Proof state after:
case left
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
n : ℕ
⊢ ∀ ⦃x1 x2 : U⦄, R n x1 → R n x2 → x1 = x2
Theorem: HTPI.Theorem_8_1_5_1_to_2
Proof state before:
case left
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
n : ℕ
⊢ ∀ ⦃x1 x2 : U⦄, R n x1 → R n x2 → x1 = x2
Tactic:
fix x1 : U
Proof state after:
case left
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
n : ℕ
x1 : U
⊢ ∀ ⦃x2 : U⦄, R n x1 → R n x2 → x1 = x2
Theorem: HTPI.Theorem_8_1_5_1_to_2
Proof state before:
case left
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
n : ℕ
x1 : U
⊢ ∀ ⦃x2 : U⦄, R n x1 → R n x2 → x1 = x2
Tactic:
fix x2 : U
Proof state after:
case left
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
n : ℕ
x1 x2 : U
⊢ R n x1 → R n x2 → x1 = x2
Theorem: HTPI.Theorem_8_1_5_1_to_2
Proof state before:
case left
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
n : ℕ
x1 x2 : U
⊢ R n x1 → R n x2 → x1 = x2
Tactic:
assume h4 : R n x1
Proof state after:
case left
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
n : ℕ
x1 x2 : U
h4 : R n x1
⊢ R n x2 → x1 = x2
Theorem: HTPI.Theorem_8_1_5_1_to_2
Proof state before:
case left
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
n : ℕ
x1 x2 : U
h4 : R n x1
⊢ R n x2 → x1 = x2
Tactic:
assume h5 : R n x2
Proof state after:
case left
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
n : ℕ
x1 x2 : U
h4 : R n x1
h5 : R n x2
⊢ x1 = x2
Theorem: HTPI.Theorem_8_1_5_1_to_2
Proof state before:
case left
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
n : ℕ
x1 x2 : U
h4 : R n x1
h5 : R n x2
⊢ x1 = x2
Tactic:
have h6 : n ∈ I ∧ x1 ∈ A := h3.left h4
Proof state after:
case left
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
n : ℕ
x1 x2 : U
h4 : R n x1
h5 : R n x2
h6 : n ∈ I ∧ x1 ∈ A
⊢ x1 = x2
Theorem: HTPI.Theorem_8_1_5_1_to_2
Proof state before:
case left
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
n : ℕ
x1 x2 : U
h4 : R n x1
h5 : R n x2
h6 : n ∈ I ∧ x1 ∈ A
⊢ x1 = x2
Tactic:
show x1 = x2 from fcnl_unique h3.right.left h6.left h4 h5
Proof state after:
no goals
Theorem: HTPI.Theorem_8_1_5_1_to_2
Proof state before:
case right
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
⊢ nat_rel_onto R A
Tactic:
define
Proof state after:
case right
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
⊢ ∀ ⦃x : U⦄, x ∈ A → ∃ n, R n x
Theorem: HTPI.Theorem_8_1_5_1_to_2
Proof state before:
case right
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
⊢ ∀ ⦃x : U⦄, x ∈ A → ∃ n, R n x
Tactic:
fix x : U
Proof state after:
case right
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
x : U
⊢ x ∈ A → ∃ n, R n x
Theorem: HTPI.Theorem_8_1_5_1_to_2
Proof state before:
case right
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
x : U
⊢ x ∈ A → ∃ n, R n x
Tactic:
assume h4 : x ∈ A
Proof state after:
case right
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
x : U
h4 : x ∈ A
⊢ ∃ n, R n x
Theorem: HTPI.Theorem_8_1_5_1_to_2
Proof state before:
case right
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
R : Rel ℕ U
h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
x : U
h4 : x ∈ A
⊢ ∃ n, R n x
Tactic:
show ∃ (n : Nat), R n x from fcnl_exists h3.right.right h4
Proof state after:
no goals
Theorem: HTPI.exists_least_rel_to
Proof state before:
U : Type
S : Rel ℕ U
x : U
h1 : ∃ n, S n x
⊢ ∃ n, least_rel_to S x n
Tactic:
set W : Set Nat := {n : Nat | S n x}
Proof state after:
U : Type
S : Rel ℕ U
x : U
h1 : ∃ n, S n x
W : Set ℕ := {n | S n x}
⊢ ∃ n, least_rel_to S x n
Theorem: HTPI.exists_least_rel_to
Proof state before:
U : Type
S : Rel ℕ U
x : U
h1 : ∃ n, S n x
W : Set ℕ := {n | S n x}
⊢ ∃ n, least_rel_to S x n
Tactic:
have h2 : ∃ (n : Nat), n ∈ W := h1
Proof state after:
U : Type
S : Rel ℕ U
x : U
h1 : ∃ n, S n x
W : Set ℕ := {n | S n x}
h2 : ∃ n, n ∈ W
⊢ ∃ n, least_rel_to S x n
Theorem: HTPI.exists_least_rel_to
Proof state before:
U : Type
S : Rel ℕ U
x : U
h1 : ∃ n, S n x
W : Set ℕ := {n | S n x}
h2 : ∃ n, n ∈ W
⊢ ∃ n, least_rel_to S x n
Tactic:
show ∃ (n : Nat), least_rel_to S x n from well_ord_princ W h2
Proof state after:
no goals
Theorem: HTPI.Theorem_8_1_5_2_to_3
Proof state before:
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
⊢ ∃ R, fcnl_one_one_to_nat R A
Tactic:
obtain (S : Rel Nat U) (h2 : fcnl_onto_from_nat S A) from h1
Proof state after:
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : fcnl_onto_from_nat S A
⊢ ∃ R, fcnl_one_one_to_nat R A
Theorem: HTPI.Theorem_8_1_5_2_to_3
Proof state before:
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : fcnl_onto_from_nat S A
⊢ ∃ R, fcnl_one_one_to_nat R A
Tactic:
define at h2
Proof state after:
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
⊢ ∃ R, fcnl_one_one_to_nat R A
Theorem: HTPI.Theorem_8_1_5_2_to_3
Proof state before:
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
⊢ ∃ R, fcnl_one_one_to_nat R A
Tactic:
set R : Rel U Nat := least_rel_to S
Proof state after:
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
⊢ ∃ R, fcnl_one_one_to_nat R A
Theorem: HTPI.Theorem_8_1_5_2_to_3
Proof state before:
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
⊢ ∃ R, fcnl_one_one_to_nat R A
Tactic:
apply Exists.intro R
Proof state after:
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
⊢ fcnl_one_one_to_nat R A
Theorem: HTPI.Theorem_8_1_5_2_to_3
Proof state before:
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
⊢ fcnl_one_one_to_nat R A
Tactic:
define
Proof state after:
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
⊢ fcnl_on R A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ R x1 n → x2 ∈ A ∧ R x2 n → x1 = x2
Theorem: HTPI.Theorem_8_1_5_2_to_3
Proof state before:
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
⊢ fcnl_on R A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ R x1 n → x2 ∈ A ∧ R x2 n → x1 = x2
Tactic:
apply And.intro
Proof state after:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
⊢ fcnl_on R A

case right
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
⊢ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ R x1 n → x2 ∈ A ∧ R x2 n → x1 = x2
Theorem: HTPI.Theorem_8_1_5_2_to_3
Proof state before:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
⊢ fcnl_on R A
Tactic:
define
Proof state after:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
⊢ ∀ ⦃x : U⦄, x ∈ A → ∃! y, R x y
Theorem: HTPI.Theorem_8_1_5_2_to_3
Proof state before:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
⊢ ∀ ⦃x : U⦄, x ∈ A → ∃! y, R x y
Tactic:
fix x : U
Proof state after:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
⊢ x ∈ A → ∃! y, R x y
Theorem: HTPI.Theorem_8_1_5_2_to_3
Proof state before:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
⊢ x ∈ A → ∃! y, R x y
Tactic:
assume h4 : x ∈ A
Proof state after:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
⊢ ∃! y, R x y
Theorem: HTPI.Theorem_8_1_5_2_to_3
Proof state before:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
⊢ ∃! y, R x y
Tactic:
exists_unique
Proof state after:
case left.Existence
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
⊢ ∃ y, R x y

case left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
⊢ ∀ (y_1 y_2 : ℕ), R x y_1 → R x y_2 → y_1 = y_2
Theorem: HTPI.Theorem_8_1_5_2_to_3
Proof state before:
case left.Existence
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
⊢ ∃ y, R x y
Tactic:
have h5 : ∃ (n : Nat), S n x := h2.right h4
Proof state after:
case left.Existence
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
h5 : ∃ n, S n x
⊢ ∃ y, R x y
Theorem: HTPI.Theorem_8_1_5_2_to_3
Proof state before:
case left.Existence
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
h5 : ∃ n, S n x
⊢ ∃ y, R x y
Tactic:
show ∃ (n : Nat), R x n from exists_least_rel_to h5
Proof state after:
no goals
Theorem: HTPI.Theorem_8_1_5_2_to_3
Proof state before:
case left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
⊢ ∀ (y_1 y_2 : ℕ), R x y_1 → R x y_2 → y_1 = y_2
Tactic:
fix n1 : Nat
Proof state after:
case left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
n1 : ℕ
⊢ ∀ (y_2 : ℕ), R x n1 → R x y_2 → n1 = y_2
Theorem: HTPI.Theorem_8_1_5_2_to_3
Proof state before:
case left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
n1 : ℕ
⊢ ∀ (y_2 : ℕ), R x n1 → R x y_2 → n1 = y_2
Tactic:
fix n2 : Nat
Proof state after:
case left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
S : Rel ℕ U
h2 : unique_val_on_N S ∧ nat_rel_onto S A
R : Rel U ℕ := least_rel_to S
x : U
h4 : x ∈ A
n1 n2 : ℕ
⊢ R x n1 → R x n2 → n1 = n2