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

State before:
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
⊢ ctble A
Tactic:
obtain (S : Rel U Nat) (h2 : fcnl_one_one_to_nat S A) from h1
State after:
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_one_one_to_nat S A
⊢ ctble A

State before:
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_one_one_to_nat S A
⊢ ctble A
Tactic:
define at h2
State after:
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
⊢ ctble A

State before:
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
⊢ ctble A
Tactic:
rewrite [ctble_iff_equinum_set_nat]
State after:
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
⊢ ∃ I, I ∼ A

State before:
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
⊢ ∃ I, I ∼ A
Tactic:
set R : Rel Nat U := invRel (restrict_to S A)
State after:
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
⊢ ∃ I, I ∼ A

State before:
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
⊢ ∃ I, I ∼ A
Tactic:
set I : Set Nat := {n : Nat | ∃ (x : U), R n x}
State after:
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
⊢ ∃ I, I ∼ A

State before:
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
⊢ ∃ I, I ∼ A
Tactic:
apply Exists.intro I
State after:
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
⊢ I ∼ A

State before:
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
⊢ I ∼ A
Tactic:
define
State after:
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
⊢ ∃ R, matching R I A

State before:
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
⊢ ∃ R, matching R I A
Tactic:
apply Exists.intro R
State after:
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
⊢ matching R I A

State before:
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
⊢ matching R I A
Tactic:
define
State after:
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
⊢ rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A

State before:
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
⊢ rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
Tactic:
apply And.intro
State after:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
⊢ rel_within R I A

case right
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
⊢ fcnl_on R I ∧ fcnl_on (invRel R) A

State before:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
⊢ rel_within R I A
Tactic:
define
State after:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
⊢ ∀ ⦃x : ℕ⦄ ⦃y : U⦄, R x y → x ∈ I ∧ y ∈ A

State before:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
⊢ ∀ ⦃x : ℕ⦄ ⦃y : U⦄, R x y → x ∈ I ∧ y ∈ A
Tactic:
fix n : Nat
State after:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
⊢ ∀ ⦃y : U⦄, R n y → n ∈ I ∧ y ∈ A

State before:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
⊢ ∀ ⦃y : U⦄, R n y → n ∈ I ∧ y ∈ A
Tactic:
fix x : U
State after:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
x : U
⊢ R n x → n ∈ I ∧ x ∈ A

State before:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
x : U
⊢ R n x → n ∈ I ∧ x ∈ A
Tactic:
assume h3 : R n x
State after:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
x : U
h3 : R n x
⊢ n ∈ I ∧ x ∈ A

State before:
case left
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
x : U
h3 : R n x
⊢ n ∈ I ∧ x ∈ A
Tactic:
apply And.intro
State after:
case left.left
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
x : U
h3 : R n x
⊢ n ∈ I

case left.right
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
x : U
h3 : R n x
⊢ x ∈ A

State before:
case left.left
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
x : U
h3 : R n x
⊢ n ∈ I
Tactic:
define
State after:
case left.left
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
x : U
h3 : R n x
⊢ ∃ x, R n x

State before:
case left.left
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
x : U
h3 : R n x
⊢ ∃ x, R n x
Tactic:
show ∃ (x : U), R n x from Exists.intro x h3
State after:
no goals

State before:
case left.right
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
x : U
h3 : R n x
⊢ x ∈ A
Tactic:
define at h3
State after:
case left.right
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
x : U
h3 : x ∈ A ∧ S x n
⊢ x ∈ A

State before:
case left.right
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
x : U
h3 : x ∈ A ∧ S x n
⊢ x ∈ A
Tactic:
show x ∈ A from h3.left
State after:
no goals

State before:
case right
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
⊢ fcnl_on R I ∧ fcnl_on (invRel R) A
Tactic:
apply And.intro
State after:
case right.left
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
⊢ fcnl_on R I

case right.right
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
⊢ fcnl_on (invRel R) A

State before:
case right.left
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
⊢ fcnl_on R I
Tactic:
define
State after:
case right.left
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
⊢ ∀ ⦃x : ℕ⦄, x ∈ I → ∃! y, R x y

State before:
case right.left
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
⊢ ∀ ⦃x : ℕ⦄, x ∈ I → ∃! y, R x y
Tactic:
fix n : Nat
State after:
case right.left
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
⊢ n ∈ I → ∃! y, R n y

State before:
case right.left
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
⊢ n ∈ I → ∃! y, R n y
Tactic:
assume h3 : n ∈ I
State after:
case right.left
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
h3 : n ∈ I
⊢ ∃! y, R n y

State before:
case right.left
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
h3 : n ∈ I
⊢ ∃! y, R n y
Tactic:
exists_unique
State after:
case right.left.Existence
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
h3 : n ∈ I
⊢ ∃ y, R n y

case right.left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
h3 : n ∈ I
⊢ ∀ (y_1 y_2 : U), R n y_1 → R n y_2 → y_1 = y_2

State before:
case right.left.Existence
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
h3 : n ∈ I
⊢ ∃ y, R n y
Tactic:
define at h3
State after:
case right.left.Existence
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
h3 : ∃ x, R n x
⊢ ∃ y, R n y

State before:
case right.left.Existence
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
h3 : ∃ x, R n x
⊢ ∃ y, R n y
Tactic:
show ∃ (y : U), R n y from h3
State after:
no goals

State before:
case right.left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
h3 : n ∈ I
⊢ ∀ (y_1 y_2 : U), R n y_1 → R n y_2 → y_1 = y_2
Tactic:
fix x1 : U
State after:
case right.left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
h3 : n ∈ I
x1 : U
⊢ ∀ (y_2 : U), R n x1 → R n y_2 → x1 = y_2

State before:
case right.left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
h3 : n ∈ I
x1 : U
⊢ ∀ (y_2 : U), R n x1 → R n y_2 → x1 = y_2
Tactic:
fix x2 : U
State after:
case right.left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
h3 : n ∈ I
x1 x2 : U
⊢ R n x1 → R n x2 → x1 = x2

State before:
case right.left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
h3 : n ∈ I
x1 x2 : U
⊢ R n x1 → R n x2 → x1 = x2
Tactic:
assume h4 : R n x1
State after:
case right.left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
h3 : n ∈ I
x1 x2 : U
h4 : R n x1
⊢ R n x2 → x1 = x2

State before:
case right.left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
h3 : n ∈ I
x1 x2 : U
h4 : R n x1
⊢ R n x2 → x1 = x2
Tactic:
assume h5 : R n x2
State after:
case right.left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
h3 : n ∈ I
x1 x2 : U
h4 : R n x1
h5 : R n x2
⊢ x1 = x2

State before:
case right.left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
h3 : n ∈ I
x1 x2 : U
h4 : R n x1
h5 : R n x2
⊢ x1 = x2
Tactic:
define at h4
State after:
case right.left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
h3 : n ∈ I
x1 x2 : U
h4 : x1 ∈ A ∧ S x1 n
h5 : R n x2
⊢ x1 = x2

State before:
case right.left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
h3 : n ∈ I
x1 x2 : U
h4 : x1 ∈ A ∧ S x1 n
h5 : R n x2
⊢ x1 = x2
Tactic:
define at h5
State after:
case right.left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
h3 : n ∈ I
x1 x2 : U
h4 : x1 ∈ A ∧ S x1 n
h5 : x2 ∈ A ∧ S x2 n
⊢ x1 = x2

State before:
case right.left.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
n : ℕ
h3 : n ∈ I
x1 x2 : U
h4 : x1 ∈ A ∧ S x1 n
h5 : x2 ∈ A ∧ S x2 n
⊢ x1 = x2
Tactic:
show x1 = x2 from h2.right h4 h5
State after:
no goals

State before:
case right.right
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
⊢ fcnl_on (invRel R) A
Tactic:
define
State after:
case right.right
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
⊢ ∀ ⦃x : U⦄, x ∈ A → ∃! y, invRel R x y

State before:
case right.right
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
⊢ ∀ ⦃x : U⦄, x ∈ A → ∃! y, invRel R x y
Tactic:
fix x : U
State after:
case right.right
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
⊢ x ∈ A → ∃! y, invRel R x y

State before:
case right.right
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
⊢ x ∈ A → ∃! y, invRel R x y
Tactic:
assume h3 : x ∈ A
State after:
case right.right
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
h3 : x ∈ A
⊢ ∃! y, invRel R x y

State before:
case right.right
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
h3 : x ∈ A
⊢ ∃! y, invRel R x y
Tactic:
exists_unique
State after:
case right.right.Existence
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
h3 : x ∈ A
⊢ ∃ y, invRel R x y

case right.right.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
h3 : x ∈ A
⊢ ∀ (y_1 y_2 : ℕ), invRel R x y_1 → invRel R x y_2 → y_1 = y_2

State before:
case right.right.Existence
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
h3 : x ∈ A
⊢ ∃ y, invRel R x y
Tactic:
obtain (y : Nat) (h4 : S x y) from fcnl_exists h2.left h3
State after:
case right.right.Existence
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
h3 : x ∈ A
y : ℕ
h4 : S x y
⊢ ∃ y, invRel R x y

State before:
case right.right.Existence
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
h3 : x ∈ A
y : ℕ
h4 : S x y
⊢ ∃ y, invRel R x y
Tactic:
apply Exists.intro y
State after:
case right.right.Existence
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
h3 : x ∈ A
y : ℕ
h4 : S x y
⊢ invRel R x y

State before:
case right.right.Existence
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
h3 : x ∈ A
y : ℕ
h4 : S x y
⊢ invRel R x y
Tactic:
define
State after:
case right.right.Existence
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
h3 : x ∈ A
y : ℕ
h4 : S x y
⊢ x ∈ A ∧ S x y

State before:
case right.right.Existence
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
h3 : x ∈ A
y : ℕ
h4 : S x y
⊢ x ∈ A ∧ S x y
Tactic:
show x ∈ A ∧ S x y from And.intro h3 h4
State after:
no goals

State before:
case right.right.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
h3 : x ∈ A
⊢ ∀ (y_1 y_2 : ℕ), invRel R x y_1 → invRel R x y_2 → y_1 = y_2
Tactic:
fix n1 : Nat
State after:
case right.right.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
h3 : x ∈ A
n1 : ℕ
⊢ ∀ (y_2 : ℕ), invRel R x n1 → invRel R x y_2 → n1 = y_2

State before:
case right.right.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
h3 : x ∈ A
n1 : ℕ
⊢ ∀ (y_2 : ℕ), invRel R x n1 → invRel R x y_2 → n1 = y_2
Tactic:
fix n2 : Nat
State after:
case right.right.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
h3 : x ∈ A
n1 n2 : ℕ
⊢ invRel R x n1 → invRel R x n2 → n1 = n2

State before:
case right.right.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
h3 : x ∈ A
n1 n2 : ℕ
⊢ invRel R x n1 → invRel R x n2 → n1 = n2
Tactic:
assume h4 : invRel R x n1
State after:
case right.right.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
h3 : x ∈ A
n1 n2 : ℕ
h4 : invRel R x n1
⊢ invRel R x n2 → n1 = n2

State before:
case right.right.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
h3 : x ∈ A
n1 n2 : ℕ
h4 : invRel R x n1
⊢ invRel R x n2 → n1 = n2
Tactic:
assume h5 : invRel R x n2
State after:
case right.right.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
h3 : x ∈ A
n1 n2 : ℕ
h4 : invRel R x n1
h5 : invRel R x n2
⊢ n1 = n2

State before:
case right.right.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
h3 : x ∈ A
n1 n2 : ℕ
h4 : invRel R x n1
h5 : invRel R x n2
⊢ n1 = n2
Tactic:
define at h4
State after:
case right.right.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
h3 : x ∈ A
n1 n2 : ℕ
h4 : x ∈ A ∧ S x n1
h5 : invRel R x n2
⊢ n1 = n2

State before:
case right.right.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
h3 : x ∈ A
n1 n2 : ℕ
h4 : x ∈ A ∧ S x n1
h5 : invRel R x n2
⊢ n1 = n2
Tactic:
define at h5
State after:
case right.right.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
h3 : x ∈ A
n1 n2 : ℕ
h4 : x ∈ A ∧ S x n1
h5 : x ∈ A ∧ S x n2
⊢ n1 = n2

State before:
case right.right.Uniqueness
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
S : Rel U ℕ
h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
R : Rel ℕ U := invRel (restrict_to S A)
I : Set ℕ := {n | ∃ x, R n x}
x : U
h3 : x ∈ A
n1 n2 : ℕ
h4 : x ∈ A ∧ S x n1
h5 : x ∈ A ∧ S x n2
⊢ n1 = n2
Tactic:
show n1 = n2 from fcnl_unique h2.left h3 h4.right h5.right
State after:
no goals