internlm/Lean-Github huggingface dataset:
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_8_1_5_2
Proof state before:
U : Type
A : Set U
⊢ ctble A ↔ ∃ R, fcnl_onto_from_nat R A
Tactic:
apply Iff.intro
Proof state after:
case mp
U : Type
A : Set U
⊢ ctble A → ∃ R, fcnl_onto_from_nat R A

case mpr
U : Type
A : Set U
⊢ (∃ R, fcnl_onto_from_nat R A) → ctble A
Theorem: HTPI.Theorem_8_1_5_2
Proof state before:
case mp
U : Type
A : Set U
⊢ ctble A → ∃ R, fcnl_onto_from_nat R A
Tactic:
assume h1 : ctble A
Proof state after:
case mp
U : Type
A : Set U
h1 : ctble A
⊢ ∃ R, fcnl_onto_from_nat R A
Theorem: HTPI.Theorem_8_1_5_2
Proof state before:
case mp
U : Type
A : Set U
h1 : ctble A
⊢ ∃ R, fcnl_onto_from_nat R A
Tactic:
show ∃ (R : Rel Nat U), fcnl_onto_from_nat R A from
  Theorem_8_1_5_1_to_2 h1
Proof state after:
no goals
Theorem: HTPI.Theorem_8_1_5_2
Proof state before:
case mpr
U : Type
A : Set U
⊢ (∃ R, fcnl_onto_from_nat R A) → ctble A
Tactic:
assume h1 : ∃ (R : Rel Nat U), fcnl_onto_from_nat R A
Proof state after:
case mpr
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
⊢ ctble A
Theorem: HTPI.Theorem_8_1_5_2
Proof state before:
case mpr
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
⊢ ctble A
Tactic:
have h2 : ∃ (R : Rel U Nat), fcnl_one_one_to_nat R A :=
  Theorem_8_1_5_2_to_3 h1
Proof state after:
case mpr
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
h2 : ∃ R, fcnl_one_one_to_nat R A
⊢ ctble A
Theorem: HTPI.Theorem_8_1_5_2
Proof state before:
case mpr
U : Type
A : Set U
h1 : ∃ R, fcnl_onto_from_nat R A
h2 : ∃ R, fcnl_one_one_to_nat R A
⊢ ctble A
Tactic:
show ctble A from Theorem_8_1_5_3_to_1 h2
Proof state after:
no goals
Theorem: HTPI.Theorem_8_1_5_3
Proof state before:
U : Type
A : Set U
⊢ ctble A ↔ ∃ R, fcnl_one_one_to_nat R A
Tactic:
apply Iff.intro
Proof state after:
case mp
U : Type
A : Set U
⊢ ctble A → ∃ R, fcnl_one_one_to_nat R A

case mpr
U : Type
A : Set U
⊢ (∃ R, fcnl_one_one_to_nat R A) → ctble A
Theorem: HTPI.Theorem_8_1_5_3
Proof state before:
case mp
U : Type
A : Set U
⊢ ctble A → ∃ R, fcnl_one_one_to_nat R A
Tactic:
assume h1 : ctble A
Proof state after:
case mp
U : Type
A : Set U
h1 : ctble A
⊢ ∃ R, fcnl_one_one_to_nat R A
Theorem: HTPI.Theorem_8_1_5_3
Proof state before:
case mp
U : Type
A : Set U
h1 : ctble A
⊢ ∃ R, fcnl_one_one_to_nat R A
Tactic:
have h2 : ∃ (R : Rel Nat U), fcnl_onto_from_nat R A :=
  Theorem_8_1_5_1_to_2 h1
Proof state after:
case mp
U : Type
A : Set U
h1 : ctble A
h2 : ∃ R, fcnl_onto_from_nat R A
⊢ ∃ R, fcnl_one_one_to_nat R A
Theorem: HTPI.Theorem_8_1_5_3
Proof state before:
case mp
U : Type
A : Set U
h1 : ctble A
h2 : ∃ R, fcnl_onto_from_nat R A
⊢ ∃ R, fcnl_one_one_to_nat R A
Tactic:
show ∃ (R : Rel U Nat), fcnl_one_one_to_nat R A from
  Theorem_8_1_5_2_to_3 h2
Proof state after:
no goals
Theorem: HTPI.Theorem_8_1_5_3
Proof state before:
case mpr
U : Type
A : Set U
⊢ (∃ R, fcnl_one_one_to_nat R A) → ctble A
Tactic:
assume h1 : ∃ (R : Rel U Nat), fcnl_one_one_to_nat R A
Proof state after:
case mpr
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
⊢ ctble A
Theorem: HTPI.Theorem_8_1_5_3
Proof state before:
case mpr
U : Type
A : Set U
h1 : ∃ R, fcnl_one_one_to_nat R A
⊢ ctble A
Tactic:
show ctble A from Theorem_8_1_5_3_to_1 h1
Proof state after:
no goals
Theorem: HTPI.fqn_def
Proof state before:
q : ℚ
⊢ fqn q = fnnn (fzn q.num, q.den)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.fqn_one_one
Proof state before:
⊢ one_to_one fqn
Tactic:
define
Proof state after:
⊢ ∀ (x1 x2 : ℚ), fqn x1 = fqn x2 → x1 = x2
Theorem: HTPI.fqn_one_one
Proof state before:
⊢ ∀ (x1 x2 : ℚ), fqn x1 = fqn x2 → x1 = x2
Tactic:
fix q1 : Rat
Proof state after:
q1 : ℚ
⊢ ∀ (x2 : ℚ), fqn q1 = fqn x2 → q1 = x2
Theorem: HTPI.fqn_one_one
Proof state before:
q1 : ℚ
⊢ ∀ (x2 : ℚ), fqn q1 = fqn x2 → q1 = x2
Tactic:
fix q2 : Rat
Proof state after:
q1 q2 : ℚ
⊢ fqn q1 = fqn q2 → q1 = q2
Theorem: HTPI.fqn_one_one
Proof state before:
q1 q2 : ℚ
⊢ fqn q1 = fqn q2 → q1 = q2
Tactic:
assume h1 : fqn q1 = fqn q2
Proof state after:
q1 q2 : ℚ
h1 : fqn q1 = fqn q2
⊢ q1 = q2
Theorem: HTPI.fqn_one_one
Proof state before:
q1 q2 : ℚ
h1 : fqn q1 = fqn q2
⊢ q1 = q2
Tactic:
rewrite [fqn_def, fqn_def] at h1
Proof state after:
q1 q2 : ℚ
h1 : fnnn (fzn q1.num, q1.den) = fnnn (fzn q2.num, q2.den)
⊢ q1 = q2
Theorem: HTPI.fqn_one_one
Proof state before:
q1 q2 : ℚ
h1 : fnnn (fzn q1.num, q1.den) = fnnn (fzn q2.num, q2.den)
⊢ q1 = q2
Tactic:
have h2 : (fzn q1.num, q1.den) = (fzn q2.num, q2.den) :=
  fnnn_one_one _ _ h1
Proof state after:
q1 q2 : ℚ
h1 : fnnn (fzn q1.num, q1.den) = fnnn (fzn q2.num, q2.den)
h2 : (fzn q1.num, q1.den) = (fzn q2.num, q2.den)
⊢ q1 = q2
Theorem: HTPI.fqn_one_one
Proof state before:
q1 q2 : ℚ
h1 : fnnn (fzn q1.num, q1.den) = fnnn (fzn q2.num, q2.den)
h2 : (fzn q1.num, q1.den) = (fzn q2.num, q2.den)
⊢ q1 = q2
Tactic:
have h3 : fzn q1.num = fzn q2.num ∧ q1.den = q2.den :=
  Prod.mk.inj h2
Proof state after:
q1 q2 : ℚ
h1 : fnnn (fzn q1.num, q1.den) = fnnn (fzn q2.num, q2.den)
h2 : (fzn q1.num, q1.den) = (fzn q2.num, q2.den)
h3 : fzn q1.num = fzn q2.num ∧ q1.den = q2.den
⊢ q1 = q2
Theorem: HTPI.fqn_one_one
Proof state before:
q1 q2 : ℚ
h1 : fnnn (fzn q1.num, q1.den) = fnnn (fzn q2.num, q2.den)
h2 : (fzn q1.num, q1.den) = (fzn q2.num, q2.den)
h3 : fzn q1.num = fzn q2.num ∧ q1.den = q2.den
⊢ q1 = q2
Tactic:
have h4 : q1.num = q2.num := fzn_one_one _ _ h3.left
Proof state after:
q1 q2 : ℚ
h1 : fnnn (fzn q1.num, q1.den) = fnnn (fzn q2.num, q2.den)
h2 : (fzn q1.num, q1.den) = (fzn q2.num, q2.den)
h3 : fzn q1.num = fzn q2.num ∧ q1.den = q2.den
h4 : q1.num = q2.num
⊢ q1 = q2
Theorem: HTPI.fqn_one_one
Proof state before:
q1 q2 : ℚ
h1 : fnnn (fzn q1.num, q1.den) = fnnn (fzn q2.num, q2.den)
h2 : (fzn q1.num, q1.den) = (fzn q2.num, q2.den)
h3 : fzn q1.num = fzn q2.num ∧ q1.den = q2.den
h4 : q1.num = q2.num
⊢ q1 = q2
Tactic:
show q1 = q2 from Rat.ext q1 q2 h4 h3.right
Proof state after:
no goals
Theorem: HTPI.image_fqn_unbdd
Proof state before:
⊢ ∀ (m : ℕ), ∃ n ∈ image fqn (Univ ℚ), n ≥ m
Tactic:
fix m : Nat
Proof state after:
m : ℕ
⊢ ∃ n ∈ image fqn (Univ ℚ), n ≥ m
Theorem: HTPI.image_fqn_unbdd
Proof state before:
m : ℕ
⊢ ∃ n ∈ image fqn (Univ ℚ), n ≥ m
Tactic:
set n : Nat := fqn ↑m
Proof state after:
m : ℕ
n : ℕ := fqn ↑m
⊢ ∃ n ∈ image fqn (Univ ℚ), n ≥ m
Theorem: HTPI.image_fqn_unbdd
Proof state before:
m : ℕ
n : ℕ := fqn ↑m
⊢ ∃ n ∈ image fqn (Univ ℚ), n ≥ m
Tactic:
apply Exists.intro n
Proof state after:
m : ℕ
n : ℕ := fqn ↑m
⊢ n ∈ image fqn (Univ ℚ) ∧ n ≥ m
Theorem: HTPI.image_fqn_unbdd
Proof state before:
m : ℕ
n : ℕ := fqn ↑m
⊢ n ∈ image fqn (Univ ℚ) ∧ n ≥ m
Tactic:
apply And.intro
Proof state after:
case left
m : ℕ
n : ℕ := fqn ↑m
⊢ n ∈ image fqn (Univ ℚ)

case right
m : ℕ
n : ℕ := fqn ↑m
⊢ n ≥ m
Theorem: HTPI.image_fqn_unbdd
Proof state before:
case left
m : ℕ
n : ℕ := fqn ↑m
⊢ n ∈ image fqn (Univ ℚ)
Tactic:
define
Proof state after:
case left
m : ℕ
n : ℕ := fqn ↑m
⊢ ∃ x ∈ Univ ℚ, fqn x = n
Theorem: HTPI.image_fqn_unbdd
Proof state before:
case left
m : ℕ
n : ℕ := fqn ↑m
⊢ ∃ x ∈ Univ ℚ, fqn x = n
Tactic:
apply Exists.intro ↑m
Proof state after:
case left
m : ℕ
n : ℕ := fqn ↑m
⊢ ↑m ∈ Univ ℚ ∧ fqn ↑m = n
Theorem: HTPI.image_fqn_unbdd
Proof state before:
case left
m : ℕ
n : ℕ := fqn ↑m
⊢ ↑m ∈ Univ ℚ ∧ fqn ↑m = n
Tactic:
apply And.intro (elt_Univ (↑m : Rat))
Proof state after:
case left
m : ℕ
n : ℕ := fqn ↑m
⊢ fqn ↑m = n
Theorem: HTPI.image_fqn_unbdd
Proof state before:
case left
m : ℕ
n : ℕ := fqn ↑m
⊢ fqn ↑m = n
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.image_fqn_unbdd
Proof state before:
case right
m : ℕ
n : ℕ := fqn ↑m
⊢ n ≥ m
Tactic:
show n ≥ m from
  calc n
    _ = tri (2 * m + 1) + 2 * m := by rfl
    _ ≥ m := by linarith
Proof state after:
no goals
Theorem: HTPI.image_fqn_unbdd
Proof state before:
m : ℕ
n : ℕ := fqn ↑m
⊢ n = tri (2 * m + 1) + 2 * m
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.image_fqn_unbdd
Proof state before:
m : ℕ
n : ℕ := fqn ↑m
⊢ tri (2 * m + 1) + 2 * m ≥ m
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.Theorem_8_1_6
Proof state before:
⊢ denum (Univ ℚ)
Tactic:
set I : Set Nat := image fqn (Univ Rat)
Proof state after:
I : Set ℕ := image fqn (Univ ℚ)
⊢ denum (Univ ℚ)