Theorem: HTPI.Theorem_8_1_5_1_to_2 (HTPILib/Chap8Part2.lean)

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
State after:
U : Type
A : Set U
h1 : ∃ I, I ∼ A
⊢ ∃ R, fcnl_onto_from_nat R A

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
State after:
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
⊢ ∃ R, fcnl_onto_from_nat R A

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
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

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
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

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
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

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
State after:
no goals