internlm/Lean-Github huggingface dataset:
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 n2 : ℕ
⊢ R x n1 → R x n2 → n1 = n2
Tactic:
assume h5 : R x n1
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 : ℕ
h5 : R x n1
⊢ R x n2 → n1 = n2
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 n2 : ℕ
h5 : R x n1
⊢ R x n2 → n1 = n2
Tactic:
assume h6 : R x n2
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 : ℕ
h5 : R x n1
h6 : R x n2
⊢ n1 = n2
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 n2 : ℕ
h5 : R x n1
h6 : R x n2
⊢ n1 = n2
Tactic:
define at h5
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 : ℕ
h5 : S n1 x ∧ ∀ (m : ℕ), S m x → n1 ≤ m
h6 : R x n2
⊢ n1 = n2
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 n2 : ℕ
h5 : S n1 x ∧ ∀ (m : ℕ), S m x → n1 ≤ m
h6 : R x n2
⊢ n1 = n2
Tactic:
define at h6
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 : ℕ
h5 : S n1 x ∧ ∀ (m : ℕ), S m x → n1 ≤ m
h6 : S n2 x ∧ ∀ (m : ℕ), S m x → n2 ≤ m
⊢ n1 = n2
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 n2 : ℕ
h5 : S n1 x ∧ ∀ (m : ℕ), S m x → n1 ≤ m
h6 : S n2 x ∧ ∀ (m : ℕ), S m x → n2 ≤ m
⊢ n1 = n2
Tactic:
have h7 : n1 ≤ n2 := h5.right n2 h6.left
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 : ℕ
h5 : S n1 x ∧ ∀ (m : ℕ), S m x → n1 ≤ m
h6 : S n2 x ∧ ∀ (m : ℕ), S m x → n2 ≤ m
h7 : n1 ≤ n2
⊢ n1 = n2
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 n2 : ℕ
h5 : S n1 x ∧ ∀ (m : ℕ), S m x → n1 ≤ m
h6 : S n2 x ∧ ∀ (m : ℕ), S m x → n2 ≤ m
h7 : n1 ≤ n2
⊢ n1 = n2
Tactic:
have h8 : n2 ≤ n1 := h6.right n1 h5.left
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 : ℕ
h5 : S n1 x ∧ ∀ (m : ℕ), S m x → n1 ≤ m
h6 : S n2 x ∧ ∀ (m : ℕ), S m x → n2 ≤ m
h7 : n1 ≤ n2
h8 : n2 ≤ n1
⊢ n1 = n2
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 n2 : ℕ
h5 : S n1 x ∧ ∀ (m : ℕ), S m x → n1 ≤ m
h6 : S n2 x ∧ ∀ (m : ℕ), S m x → n2 ≤ m
h7 : n1 ≤ n2
h8 : n2 ≤ n1
⊢ n1 = n2
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.Theorem_8_1_5_2_to_3
Proof state before:
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
Tactic:
fix x1 : U
Proof state after:
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 : U
⊢ ∀ ⦃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 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 : U
⊢ ∀ ⦃x2 : U⦄ ⦃n : ℕ⦄, x1 ∈ A ∧ R x1 n → x2 ∈ A ∧ R x2 n → x1 = x2
Tactic:
fix x2 : U
Proof state after:
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 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
Tactic:
fix n : Nat
Proof state after:
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 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
Tactic:
assume h4 : x1 ∈ A ∧ R x1 n
Proof state after:
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 : ℕ
h4 : 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 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 : ℕ
h4 : x1 ∈ A ∧ R x1 n
⊢ x2 ∈ A ∧ R x2 n → x1 = x2
Tactic:
assume h5 : x2 ∈ A ∧ R x2 n
Proof state after:
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 : ℕ
h4 : x1 ∈ A ∧ R x1 n
h5 : x2 ∈ A ∧ R x2 n
⊢ x1 = x2
Theorem: HTPI.Theorem_8_1_5_2_to_3
Proof state before:
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 : ℕ
h4 : x1 ∈ A ∧ R x1 n
h5 : x2 ∈ A ∧ R x2 n
⊢ x1 = x2
Tactic:
have h6 : R x1 n := h4.right
Proof state after:
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 : ℕ
h4 : x1 ∈ A ∧ R x1 n
h5 : x2 ∈ A ∧ R x2 n
h6 : R x1 n
⊢ x1 = x2
Theorem: HTPI.Theorem_8_1_5_2_to_3
Proof state before:
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 : ℕ
h4 : x1 ∈ A ∧ R x1 n
h5 : x2 ∈ A ∧ R x2 n
h6 : R x1 n
⊢ x1 = x2
Tactic:
have h7 : R x2 n := h5.right
Proof state after:
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 : ℕ
h4 : x1 ∈ A ∧ R x1 n
h5 : x2 ∈ A ∧ R x2 n
h6 : R x1 n
h7 : R x2 n
⊢ x1 = x2
Theorem: HTPI.Theorem_8_1_5_2_to_3
Proof state before:
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 : ℕ
h4 : x1 ∈ A ∧ R x1 n
h5 : x2 ∈ A ∧ R x2 n
h6 : R x1 n
h7 : R x2 n
⊢ x1 = x2
Tactic:
define at h6
Proof state after:
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 : ℕ
h4 : x1 ∈ A ∧ R x1 n
h5 : x2 ∈ A ∧ R x2 n
h6 : S n x1 ∧ ∀ (m : ℕ), S m x1 → n ≤ m
h7 : R x2 n
⊢ x1 = x2
Theorem: HTPI.Theorem_8_1_5_2_to_3
Proof state before:
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 : ℕ
h4 : x1 ∈ A ∧ R x1 n
h5 : x2 ∈ A ∧ R x2 n
h6 : S n x1 ∧ ∀ (m : ℕ), S m x1 → n ≤ m
h7 : R x2 n
⊢ x1 = x2
Tactic:
define at h7
Proof state after:
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 : ℕ
h4 : x1 ∈ A ∧ R x1 n
h5 : x2 ∈ A ∧ R x2 n
h6 : S n x1 ∧ ∀ (m : ℕ), S m x1 → n ≤ m
h7 : S n x2 ∧ ∀ (m : ℕ), S m x2 → n ≤ m
⊢ x1 = x2
Theorem: HTPI.Theorem_8_1_5_2_to_3
Proof state before:
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 : ℕ
h4 : x1 ∈ A ∧ R x1 n
h5 : x2 ∈ A ∧ R x2 n
h6 : S n x1 ∧ ∀ (m : ℕ), S m x1 → n ≤ m
h7 : S n x2 ∧ ∀ (m : ℕ), S m x2 → n ≤ m
⊢ x1 = x2
Tactic:
show x1 = x2 from h2.left h6.left h7.left
Proof state after:
no goals
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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]
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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)
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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}
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_1_5_3_to_1
Proof 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
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 : 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