internlm/Lean-Github huggingface dataset:
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
x : U
⊢ x ∈ ⋃₀ F → ∃ n, S n x
Tactic:
assume h4 : x ∈ ⋃₀ F
Proof state after:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : x ∈ ⋃₀ F
⊢ ∃ n, S n x
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : x ∈ ⋃₀ F
⊢ ∃ n, S n x
Tactic:
define at h4
Proof state after:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
⊢ ∃ n, S n x
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
⊢ ∃ n, S n x
Tactic:
obtain (A : Set U) (h5 : A ∈ F ∧ x ∈ A) from h4
Proof state after:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
⊢ ∃ n, S n x
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
⊢ ∃ n, S n x
Tactic:
define at Ronto
Proof state after:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
⊢ ∃ n, S n x
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
⊢ ∃ n, S n x
Tactic:
obtain (i : Nat) (h6 : R i A) from Ronto h5.left
Proof state after:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
i : ℕ
h6 : R i A
⊢ ∃ n, S n x
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
i : ℕ
h6 : R i A
⊢ ∃ n, S n x
Tactic:
have fAfcnlonto : fcnl_onto_from_nat (f A) A := h2 A h5.left
Proof state after:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
i : ℕ
h6 : R i A
fAfcnlonto : fcnl_onto_from_nat (f A) A
⊢ ∃ n, S n x
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
i : ℕ
h6 : R i A
fAfcnlonto : fcnl_onto_from_nat (f A) A
⊢ ∃ n, S n x
Tactic:
define at fAfcnlonto
Proof state after:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
i : ℕ
h6 : R i A
fAfcnlonto : unique_val_on_N (f A) ∧ nat_rel_onto (f A) A
⊢ ∃ n, S n x
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
i : ℕ
h6 : R i A
fAfcnlonto : unique_val_on_N (f A) ∧ nat_rel_onto (f A) A
⊢ ∃ n, S n x
Tactic:
have fAonto : nat_rel_onto (f A) A := fAfcnlonto.right
Proof state after:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
i : ℕ
h6 : R i A
fAfcnlonto : unique_val_on_N (f A) ∧ nat_rel_onto (f A) A
fAonto : nat_rel_onto (f A) A
⊢ ∃ n, S n x
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
i : ℕ
h6 : R i A
fAfcnlonto : unique_val_on_N (f A) ∧ nat_rel_onto (f A) A
fAonto : nat_rel_onto (f A) A
⊢ ∃ n, S n x
Tactic:
define at fAonto
Proof state after:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
i : ℕ
h6 : R i A
fAfcnlonto : unique_val_on_N (f A) ∧ nat_rel_onto (f A) A
fAonto : ∀ ⦃x : U⦄, x ∈ A → ∃ n, f A n x
⊢ ∃ n, S n x
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
i : ℕ
h6 : R i A
fAfcnlonto : unique_val_on_N (f A) ∧ nat_rel_onto (f A) A
fAonto : ∀ ⦃x : U⦄, x ∈ A → ∃ n, f A n x
⊢ ∃ n, S n x
Tactic:
obtain (j : Nat) (h7 : f A j x) from fAonto h5.right
Proof state after:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
i : ℕ
h6 : R i A
fAfcnlonto : unique_val_on_N (f A) ∧ nat_rel_onto (f A) A
fAonto : ∀ ⦃x : U⦄, x ∈ A → ∃ n, f A n x
j : ℕ
h7 : f A j x
⊢ ∃ n, S n x
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
i : ℕ
h6 : R i A
fAfcnlonto : unique_val_on_N (f A) ∧ nat_rel_onto (f A) A
fAonto : ∀ ⦃x : U⦄, x ∈ A → ∃ n, f A n x
j : ℕ
h7 : f A j x
⊢ ∃ n, S n x
Tactic:
apply Exists.intro (fnnn (i, j))
Proof state after:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
i : ℕ
h6 : R i A
fAfcnlonto : unique_val_on_N (f A) ∧ nat_rel_onto (f A) A
fAonto : ∀ ⦃x : U⦄, x ∈ A → ∃ n, f A n x
j : ℕ
h7 : f A j x
⊢ S (fnnn (i, j)) x
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
i : ℕ
h6 : R i A
fAfcnlonto : unique_val_on_N (f A) ∧ nat_rel_onto (f A) A
fAonto : ∀ ⦃x : U⦄, x ∈ A → ∃ n, f A n x
j : ℕ
h7 : f A j x
⊢ S (fnnn (i, j)) x
Tactic:
define
Proof state after:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
i : ℕ
h6 : R i A
fAfcnlonto : unique_val_on_N (f A) ∧ nat_rel_onto (f A) A
fAonto : ∀ ⦃x : U⦄, x ∈ A → ∃ n, f A n x
j : ℕ
h7 : f A j x
⊢ ∃ p, fnnn p = fnnn (i, j) ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 x
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
i : ℕ
h6 : R i A
fAfcnlonto : unique_val_on_N (f A) ∧ nat_rel_onto (f A) A
fAonto : ∀ ⦃x : U⦄, x ∈ A → ∃ n, f A n x
j : ℕ
h7 : f A j x
⊢ ∃ p, fnnn p = fnnn (i, j) ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 x
Tactic:
apply Exists.intro (i, j)
Proof state after:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
i : ℕ
h6 : R i A
fAfcnlonto : unique_val_on_N (f A) ∧ nat_rel_onto (f A) A
fAonto : ∀ ⦃x : U⦄, x ∈ A → ∃ n, f A n x
j : ℕ
h7 : f A j x
⊢ fnnn (i, j) = fnnn (i, j) ∧ ∃ A ∈ F, R (i, j).1 A ∧ f A (i, j).2 x
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
i : ℕ
h6 : R i A
fAfcnlonto : unique_val_on_N (f A) ∧ nat_rel_onto (f A) A
fAonto : ∀ ⦃x : U⦄, x ∈ A → ∃ n, f A n x
j : ℕ
h7 : f A j x
⊢ fnnn (i, j) = fnnn (i, j) ∧ ∃ A ∈ F, R (i, j).1 A ∧ f A (i, j).2 x
Tactic:
apply And.intro
Proof state after:
case right.left
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
i : ℕ
h6 : R i A
fAfcnlonto : unique_val_on_N (f A) ∧ nat_rel_onto (f A) A
fAonto : ∀ ⦃x : U⦄, x ∈ A → ∃ n, f A n x
j : ℕ
h7 : f A j x
⊢ fnnn (i, j) = fnnn (i, j)

case right.right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
i : ℕ
h6 : R i A
fAfcnlonto : unique_val_on_N (f A) ∧ nat_rel_onto (f A) A
fAonto : ∀ ⦃x : U⦄, x ∈ A → ∃ n, f A n x
j : ℕ
h7 : f A j x
⊢ ∃ A ∈ F, R (i, j).1 A ∧ f A (i, j).2 x
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case right.left
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
i : ℕ
h6 : R i A
fAfcnlonto : unique_val_on_N (f A) ∧ nat_rel_onto (f A) A
fAonto : ∀ ⦃x : U⦄, x ∈ A → ∃ n, f A n x
j : ℕ
h7 : f A j x
⊢ fnnn (i, j) = fnnn (i, j)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case right.right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
i : ℕ
h6 : R i A
fAfcnlonto : unique_val_on_N (f A) ∧ nat_rel_onto (f A) A
fAonto : ∀ ⦃x : U⦄, x ∈ A → ∃ n, f A n x
j : ℕ
h7 : f A j x
⊢ ∃ A ∈ F, R (i, j).1 A ∧ f A (i, j).2 x
Tactic:
apply Exists.intro A
Proof state after:
case right.right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
i : ℕ
h6 : R i A
fAfcnlonto : unique_val_on_N (f A) ∧ nat_rel_onto (f A) A
fAonto : ∀ ⦃x : U⦄, x ∈ A → ∃ n, f A n x
j : ℕ
h7 : f A j x
⊢ A ∈ F ∧ R (i, j).1 A ∧ f A (i, j).2 x
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case right.right
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ∃ R, fcnl_onto_from_nat R F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
R : Rel ℕ (Set U)
h3 : unique_val_on_N R ∧ nat_rel_onto R F
Runiqueval : unique_val_on_N R
Ronto : ∀ ⦃x : Set U⦄, x ∈ F → ∃ n, R n x
S : Rel ℕ U := enum_union_fam F f R
x : U
h4 : ∃ t ∈ F, x ∈ t
A : Set U
h5 : A ∈ F ∧ x ∈ A
i : ℕ
h6 : R i A
fAfcnlonto : unique_val_on_N (f A) ∧ nat_rel_onto (f A) A
fAonto : ∀ ⦃x : U⦄, x ∈ A → ∃ n, f A n x
j : ℕ
h7 : f A j x
⊢ A ∈ F ∧ R (i, j).1 A ∧ f A (i, j).2 x
Tactic:
show A ∈ F ∧ R (i, j).1 A ∧ f A (i, j).2 x from
  And.intro h5.left (And.intro h6 h7)
Proof state after:
no goals
Theorem: HTPI.Lemma_8_2_2_2
Proof state before:
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
h1 : ∀ (A : Set U), ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
⊢ ∃ f, ∀ A ∈ F, fcnl_onto_from_nat (f A) A
Tactic:
set f : Set U → Rel Nat U := fun (A : Set U) => Classical.choose (h1 A)
Proof state after:
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
h1 : ∀ (A : Set U), ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
f : Set U → Rel ℕ U := fun A => Classical.choose (_ : ∃ SA, A ∈ F → fcnl_onto_from_nat SA A)
⊢ ∃ f, ∀ A ∈ F, fcnl_onto_from_nat (f A) A
Theorem: HTPI.Lemma_8_2_2_2
Proof state before:
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
h1 : ∀ (A : Set U), ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
f : Set U → Rel ℕ U := fun A => Classical.choose (_ : ∃ SA, A ∈ F → fcnl_onto_from_nat SA A)
⊢ ∃ f, ∀ A ∈ F, fcnl_onto_from_nat (f A) A
Tactic:
apply Exists.intro f
Proof state after:
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
h1 : ∀ (A : Set U), ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
f : Set U → Rel ℕ U := fun A => Classical.choose (_ : ∃ SA, A ∈ F → fcnl_onto_from_nat SA A)
⊢ ∀ A ∈ F, fcnl_onto_from_nat (f A) A
Theorem: HTPI.Lemma_8_2_2_2
Proof state before:
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
h1 : ∀ (A : Set U), ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
f : Set U → Rel ℕ U := fun A => Classical.choose (_ : ∃ SA, A ∈ F → fcnl_onto_from_nat SA A)
⊢ ∀ A ∈ F, fcnl_onto_from_nat (f A) A
Tactic:
fix A : Set U
Proof state after:
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
h1 : ∀ (A : Set U), ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
f : Set U → Rel ℕ U := fun A => Classical.choose (_ : ∃ SA, A ∈ F → fcnl_onto_from_nat SA A)
A : Set U
⊢ A ∈ F → fcnl_onto_from_nat (f A) A
Theorem: HTPI.Lemma_8_2_2_2
Proof state before:
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
h1 : ∀ (A : Set U), ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
f : Set U → Rel ℕ U := fun A => Classical.choose (_ : ∃ SA, A ∈ F → fcnl_onto_from_nat SA A)
A : Set U
⊢ A ∈ F → fcnl_onto_from_nat (f A) A
Tactic:
show A ∈ F → fcnl_onto_from_nat (f A) A from Classical.choose_spec (h1 A)
Proof state after:
no goals
Theorem: HTPI.Lemma_8_2_2_2
Proof state before:
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
⊢ ∀ (A : Set U), ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
Tactic:
fix A : Set U
Proof state after:
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
⊢ ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
Theorem: HTPI.Lemma_8_2_2_2
Proof state before:
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
⊢ ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
Tactic:
by_cases h2 : A ∈ F
Proof state after:
case pos
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∈ F
⊢ ∃ SA, A ∈ F → fcnl_onto_from_nat SA A

case neg
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∉ F
⊢ ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
Theorem: HTPI.Lemma_8_2_2_2
Proof state before:
case pos
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∈ F
⊢ ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
Tactic:
have h3 : ctble A := h A h2
Proof state after:
case pos
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∈ F
h3 : ctble A
⊢ ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
Theorem: HTPI.Lemma_8_2_2_2
Proof state before:
case pos
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∈ F
h3 : ctble A
⊢ ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
Tactic:
rewrite [Theorem_8_1_5_2] at h3
Proof state after:
case pos
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∈ F
h3 : ∃ R, fcnl_onto_from_nat R A
⊢ ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
Theorem: HTPI.Lemma_8_2_2_2
Proof state before:
case pos
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∈ F
h3 : ∃ R, fcnl_onto_from_nat R A
⊢ ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
Tactic:
obtain (SA : Rel Nat U) (h4 : fcnl_onto_from_nat SA A) from h3
Proof state after:
case pos
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∈ F
h3 : ∃ R, fcnl_onto_from_nat R A
SA : Rel ℕ U
h4 : fcnl_onto_from_nat SA A
⊢ ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
Theorem: HTPI.Lemma_8_2_2_2
Proof state before:
case pos
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∈ F
h3 : ∃ R, fcnl_onto_from_nat R A
SA : Rel ℕ U
h4 : fcnl_onto_from_nat SA A
⊢ ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
Tactic:
apply Exists.intro SA
Proof state after:
case pos
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∈ F
h3 : ∃ R, fcnl_onto_from_nat R A
SA : Rel ℕ U
h4 : fcnl_onto_from_nat SA A
⊢ A ∈ F → fcnl_onto_from_nat SA A
Theorem: HTPI.Lemma_8_2_2_2
Proof state before:
case pos
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∈ F
h3 : ∃ R, fcnl_onto_from_nat R A
SA : Rel ℕ U
h4 : fcnl_onto_from_nat SA A
⊢ A ∈ F → fcnl_onto_from_nat SA A
Tactic:
assume h5 : A ∈ F
Proof state after:
case pos
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∈ F
h3 : ∃ R, fcnl_onto_from_nat R A
SA : Rel ℕ U
h4 : fcnl_onto_from_nat SA A
h5 : A ∈ F
⊢ fcnl_onto_from_nat SA A
Theorem: HTPI.Lemma_8_2_2_2
Proof state before:
case pos
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∈ F
h3 : ∃ R, fcnl_onto_from_nat R A
SA : Rel ℕ U
h4 : fcnl_onto_from_nat SA A
h5 : A ∈ F
⊢ fcnl_onto_from_nat SA A
Tactic:
show fcnl_onto_from_nat SA A from h4
Proof state after:
no goals
Theorem: HTPI.Lemma_8_2_2_2
Proof state before:
case neg
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∉ F
⊢ ∃ SA, A ∈ F → fcnl_onto_from_nat SA A
Tactic:
apply Exists.intro (emptyRel Nat U)
Proof state after:
case neg
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∉ F
⊢ A ∈ F → fcnl_onto_from_nat (emptyRel ℕ U) A
Theorem: HTPI.Lemma_8_2_2_2
Proof state before:
case neg
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∉ F
⊢ A ∈ F → fcnl_onto_from_nat (emptyRel ℕ U) A
Tactic:
assume h3 : A ∈ F
Proof state after:
case neg
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∉ F
h3 : A ∈ F
⊢ fcnl_onto_from_nat (emptyRel ℕ U) A
Theorem: HTPI.Lemma_8_2_2_2
Proof state before:
case neg
U : Type
F : Set (Set U)
h : ∀ A ∈ F, ctble A
A : Set U
h2 : A ∉ F
h3 : A ∈ F
⊢ fcnl_onto_from_nat (emptyRel ℕ U) A
Tactic:
show fcnl_onto_from_nat (emptyRel Nat U) A from absurd h3 h2
Proof state after:
no goals
Theorem: HTPI.Theorem_8_2_2
Proof state before:
U : Type
F : Set (Set U)
h1 : ctble F
h2 : ∀ A ∈ F, ctble A
⊢ ctble (⋃₀ F)
Tactic:
obtain (f : Set U → Rel Nat U) (h3 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A)
  from Lemma_8_2_2_2 h2
Proof state after:
U : Type
F : Set (Set U)
h1 : ctble F
h2 : ∀ A ∈ F, ctble A
f : Set U → Rel ℕ U
h3 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
⊢ ctble (⋃₀ F)
Theorem: HTPI.Theorem_8_2_2
Proof state before:
U : Type
F : Set (Set U)
h1 : ctble F
h2 : ∀ A ∈ F, ctble A
f : Set U → Rel ℕ U
h3 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
⊢ ctble (⋃₀ F)
Tactic:
show ctble (⋃₀ F) from Lemma_8_2_2_1 h1 h3
Proof state after:
no goals
Theorem: HTPI.seq_def
Proof state before:
U : Type
A : Set U
l : List U
⊢ l ∈ seq A ↔ ∀ x ∈ l, x ∈ A
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.sbl_base
Proof state before:
U : Type
A : Set U
⊢ seq_by_length A 0 = {[]}
Tactic:
apply Set.ext
Proof state after:
case h
U : Type
A : Set U
⊢ ∀ (x : List U), x ∈ seq_by_length A 0 ↔ x ∈ {[]}
Theorem: HTPI.sbl_base
Proof state before:
case h
U : Type
A : Set U
⊢ ∀ (x : List U), x ∈ seq_by_length A 0 ↔ x ∈ {[]}
Tactic:
fix l : List U
Proof state after:
case h
U : Type
A : Set U
l : List U
⊢ l ∈ seq_by_length A 0 ↔ l ∈ {[]}
Theorem: HTPI.sbl_base
Proof state before:
case h
U : Type
A : Set U
l : List U
⊢ l ∈ seq_by_length A 0 ↔ l ∈ {[]}
Tactic:
apply Iff.intro
Proof state after:
case h.mp
U : Type
A : Set U
l : List U
⊢ l ∈ seq_by_length A 0 → l ∈ {[]}

case h.mpr
U : Type
A : Set U
l : List U
⊢ l ∈ {[]} → l ∈ seq_by_length A 0