internlm/Lean-Github huggingface dataset:
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case 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 : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
h4 : fnnn (i1, j1) = n ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
⊢ a1 = a2
Tactic:
obtain (A1 : Set U) (Aija1 : A1 ∈ F ∧ R i1 A1 ∧ f A1 j1 a1)
  from h4.right
Proof state after:
case 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 : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
h4 : fnnn (i1, j1) = n ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
A1 : Set U
Aija1 : A1 ∈ F ∧ R i1 A1 ∧ f A1 j1 a1
⊢ a1 = a2
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case 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 : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
h4 : fnnn (i1, j1) = n ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
A1 : Set U
Aija1 : A1 ∈ F ∧ R i1 A1 ∧ f A1 j1 a1
⊢ a1 = a2
Tactic:
obtain ((i2, j2) : Nat × Nat) (h5 : fnnn (i2, j2) = n ∧
  ∃ A ∈ F, R i2 A ∧ f A j2 a2) from Sna2
Proof state after:
case 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 : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
h4 : fnnn (i1, j1) = n ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
A1 : Set U
Aija1 : A1 ∈ F ∧ R i1 A1 ∧ f A1 j1 a1
i2 j2 : ℕ
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
⊢ a1 = a2
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case 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 : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
h4 : fnnn (i1, j1) = n ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
A1 : Set U
Aija1 : A1 ∈ F ∧ R i1 A1 ∧ f A1 j1 a1
i2 j2 : ℕ
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
⊢ a1 = a2
Tactic:
obtain (A2 : Set U) (Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2)
  from h5.right
Proof state after:
case 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 : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
h4 : fnnn (i1, j1) = n ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
A1 : Set U
Aija1 : A1 ∈ F ∧ R i1 A1 ∧ f A1 j1 a1
i2 j2 : ℕ
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
A2 : Set U
Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2
⊢ a1 = a2
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case 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 : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
h4 : fnnn (i1, j1) = n ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
A1 : Set U
Aija1 : A1 ∈ F ∧ R i1 A1 ∧ f A1 j1 a1
i2 j2 : ℕ
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
A2 : Set U
Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2
⊢ a1 = a2
Tactic:
rewrite [←h5.left] at h4
Proof state after:
case 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 : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
A1 : Set U
Aija1 : A1 ∈ F ∧ R i1 A1 ∧ f A1 j1 a1
i2 j2 : ℕ
h4 : fnnn (i1, j1) = fnnn (i2, j2) ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
A2 : Set U
Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2
⊢ a1 = a2
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case 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 : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
A1 : Set U
Aija1 : A1 ∈ F ∧ R i1 A1 ∧ f A1 j1 a1
i2 j2 : ℕ
h4 : fnnn (i1, j1) = fnnn (i2, j2) ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
A2 : Set U
Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2
⊢ a1 = a2
Tactic:
have h6 : (i1, j1) = (i2, j2) :=
  fnnn_one_one (i1, j1) (i2, j2) h4.left
Proof state after:
case 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 : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
A1 : Set U
Aija1 : A1 ∈ F ∧ R i1 A1 ∧ f A1 j1 a1
i2 j2 : ℕ
h4 : fnnn (i1, j1) = fnnn (i2, j2) ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
A2 : Set U
Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2
h6 : (i1, j1) = (i2, j2)
⊢ a1 = a2
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case 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 : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
A1 : Set U
Aija1 : A1 ∈ F ∧ R i1 A1 ∧ f A1 j1 a1
i2 j2 : ℕ
h4 : fnnn (i1, j1) = fnnn (i2, j2) ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
A2 : Set U
Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2
h6 : (i1, j1) = (i2, j2)
⊢ a1 = a2
Tactic:
have h7 : i1 = i2 ∧ j1 = j2 := Prod.mk.inj h6
Proof state after:
case 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 : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
A1 : Set U
Aija1 : A1 ∈ F ∧ R i1 A1 ∧ f A1 j1 a1
i2 j2 : ℕ
h4 : fnnn (i1, j1) = fnnn (i2, j2) ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
A2 : Set U
Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2
h6 : (i1, j1) = (i2, j2)
h7 : i1 = i2 ∧ j1 = j2
⊢ a1 = a2
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case 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 : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
A1 : Set U
Aija1 : A1 ∈ F ∧ R i1 A1 ∧ f A1 j1 a1
i2 j2 : ℕ
h4 : fnnn (i1, j1) = fnnn (i2, j2) ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
A2 : Set U
Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2
h6 : (i1, j1) = (i2, j2)
h7 : i1 = i2 ∧ j1 = j2
⊢ a1 = a2
Tactic:
rewrite [h7.left, h7.right] at Aija1
Proof state after:
case 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 : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
A1 : Set U
i2 j2 : ℕ
Aija1 : A1 ∈ F ∧ R i2 A1 ∧ f A1 j2 a1
h4 : fnnn (i1, j1) = fnnn (i2, j2) ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
A2 : Set U
Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2
h6 : (i1, j1) = (i2, j2)
h7 : i1 = i2 ∧ j1 = j2
⊢ a1 = a2
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case 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 : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
A1 : Set U
i2 j2 : ℕ
Aija1 : A1 ∈ F ∧ R i2 A1 ∧ f A1 j2 a1
h4 : fnnn (i1, j1) = fnnn (i2, j2) ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
A2 : Set U
Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2
h6 : (i1, j1) = (i2, j2)
h7 : i1 = i2 ∧ j1 = j2
⊢ a1 = a2
Tactic:
define at Runiqueval
Proof state after:
case 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 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set U⦄, R n x1 → R n x2 → x1 = x2
Ronto : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
A1 : Set U
i2 j2 : ℕ
Aija1 : A1 ∈ F ∧ R i2 A1 ∧ f A1 j2 a1
h4 : fnnn (i1, j1) = fnnn (i2, j2) ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
A2 : Set U
Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2
h6 : (i1, j1) = (i2, j2)
h7 : i1 = i2 ∧ j1 = j2
⊢ a1 = a2
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case 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 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set U⦄, R n x1 → R n x2 → x1 = x2
Ronto : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
A1 : Set U
i2 j2 : ℕ
Aija1 : A1 ∈ F ∧ R i2 A1 ∧ f A1 j2 a1
h4 : fnnn (i1, j1) = fnnn (i2, j2) ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
A2 : Set U
Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2
h6 : (i1, j1) = (i2, j2)
h7 : i1 = i2 ∧ j1 = j2
⊢ a1 = a2
Tactic:
have h8 : A1 = A2 := Runiqueval Aija1.right.left Aija2.right.left
Proof state after:
case 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 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set U⦄, R n x1 → R n x2 → x1 = x2
Ronto : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
A1 : Set U
i2 j2 : ℕ
Aija1 : A1 ∈ F ∧ R i2 A1 ∧ f A1 j2 a1
h4 : fnnn (i1, j1) = fnnn (i2, j2) ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
A2 : Set U
Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2
h6 : (i1, j1) = (i2, j2)
h7 : i1 = i2 ∧ j1 = j2
h8 : A1 = A2
⊢ a1 = a2
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case 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 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set U⦄, R n x1 → R n x2 → x1 = x2
Ronto : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
A1 : Set U
i2 j2 : ℕ
Aija1 : A1 ∈ F ∧ R i2 A1 ∧ f A1 j2 a1
h4 : fnnn (i1, j1) = fnnn (i2, j2) ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
A2 : Set U
Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2
h6 : (i1, j1) = (i2, j2)
h7 : i1 = i2 ∧ j1 = j2
h8 : A1 = A2
⊢ a1 = a2
Tactic:
rewrite [h8] at Aija1
Proof state after:
case 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 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set U⦄, R n x1 → R n x2 → x1 = x2
Ronto : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
A1 : Set U
i2 j2 : ℕ
h4 : fnnn (i1, j1) = fnnn (i2, j2) ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
A2 : Set U
Aija1 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a1
Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2
h6 : (i1, j1) = (i2, j2)
h7 : i1 = i2 ∧ j1 = j2
h8 : A1 = A2
⊢ a1 = a2
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case 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 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set U⦄, R n x1 → R n x2 → x1 = x2
Ronto : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
A1 : Set U
i2 j2 : ℕ
h4 : fnnn (i1, j1) = fnnn (i2, j2) ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
A2 : Set U
Aija1 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a1
Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2
h6 : (i1, j1) = (i2, j2)
h7 : i1 = i2 ∧ j1 = j2
h8 : A1 = A2
⊢ a1 = a2
Tactic:
have fA2fcnlonto : fcnl_onto_from_nat (f A2) A2 := h2 A2 Aija2.left
Proof state after:
case 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 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set U⦄, R n x1 → R n x2 → x1 = x2
Ronto : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
A1 : Set U
i2 j2 : ℕ
h4 : fnnn (i1, j1) = fnnn (i2, j2) ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
A2 : Set U
Aija1 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a1
Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2
h6 : (i1, j1) = (i2, j2)
h7 : i1 = i2 ∧ j1 = j2
h8 : A1 = A2
fA2fcnlonto : fcnl_onto_from_nat (f A2) A2
⊢ a1 = a2
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case 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 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set U⦄, R n x1 → R n x2 → x1 = x2
Ronto : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
A1 : Set U
i2 j2 : ℕ
h4 : fnnn (i1, j1) = fnnn (i2, j2) ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
A2 : Set U
Aija1 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a1
Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2
h6 : (i1, j1) = (i2, j2)
h7 : i1 = i2 ∧ j1 = j2
h8 : A1 = A2
fA2fcnlonto : fcnl_onto_from_nat (f A2) A2
⊢ a1 = a2
Tactic:
define at fA2fcnlonto
Proof state after:
case 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 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set U⦄, R n x1 → R n x2 → x1 = x2
Ronto : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
A1 : Set U
i2 j2 : ℕ
h4 : fnnn (i1, j1) = fnnn (i2, j2) ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
A2 : Set U
Aija1 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a1
Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2
h6 : (i1, j1) = (i2, j2)
h7 : i1 = i2 ∧ j1 = j2
h8 : A1 = A2
fA2fcnlonto : unique_val_on_N (f A2) ∧ nat_rel_onto (f A2) A2
⊢ a1 = a2
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case 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 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set U⦄, R n x1 → R n x2 → x1 = x2
Ronto : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
A1 : Set U
i2 j2 : ℕ
h4 : fnnn (i1, j1) = fnnn (i2, j2) ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
A2 : Set U
Aija1 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a1
Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2
h6 : (i1, j1) = (i2, j2)
h7 : i1 = i2 ∧ j1 = j2
h8 : A1 = A2
fA2fcnlonto : unique_val_on_N (f A2) ∧ nat_rel_onto (f A2) A2
⊢ a1 = a2
Tactic:
have fA2uniqueval : unique_val_on_N (f A2) := fA2fcnlonto.left
Proof state after:
case 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 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set U⦄, R n x1 → R n x2 → x1 = x2
Ronto : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
A1 : Set U
i2 j2 : ℕ
h4 : fnnn (i1, j1) = fnnn (i2, j2) ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
A2 : Set U
Aija1 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a1
Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2
h6 : (i1, j1) = (i2, j2)
h7 : i1 = i2 ∧ j1 = j2
h8 : A1 = A2
fA2fcnlonto : unique_val_on_N (f A2) ∧ nat_rel_onto (f A2) A2
fA2uniqueval : unique_val_on_N (f A2)
⊢ a1 = a2
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case 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 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set U⦄, R n x1 → R n x2 → x1 = x2
Ronto : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
A1 : Set U
i2 j2 : ℕ
h4 : fnnn (i1, j1) = fnnn (i2, j2) ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
A2 : Set U
Aija1 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a1
Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2
h6 : (i1, j1) = (i2, j2)
h7 : i1 = i2 ∧ j1 = j2
h8 : A1 = A2
fA2fcnlonto : unique_val_on_N (f A2) ∧ nat_rel_onto (f A2) A2
fA2uniqueval : unique_val_on_N (f A2)
⊢ a1 = a2
Tactic:
define at fA2uniqueval
Proof state after:
case 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 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set U⦄, R n x1 → R n x2 → x1 = x2
Ronto : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
A1 : Set U
i2 j2 : ℕ
h4 : fnnn (i1, j1) = fnnn (i2, j2) ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
A2 : Set U
Aija1 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a1
Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2
h6 : (i1, j1) = (i2, j2)
h7 : i1 = i2 ∧ j1 = j2
h8 : A1 = A2
fA2fcnlonto : unique_val_on_N (f A2) ∧ nat_rel_onto (f A2) A2
fA2uniqueval : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : U⦄, f A2 n x1 → f A2 n x2 → x1 = x2
⊢ a1 = a2
Theorem: HTPI.Lemma_8_2_2_1
Proof state before:
case 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 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set U⦄, R n x1 → R n x2 → x1 = x2
Ronto : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
n : ℕ
a1 a2 : U
Sna1 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a1
Sna2 : ∃ p, fnnn p = n ∧ ∃ A ∈ F, R p.1 A ∧ f A p.2 a2
i1 j1 : ℕ
A1 : Set U
i2 j2 : ℕ
h4 : fnnn (i1, j1) = fnnn (i2, j2) ∧ ∃ A ∈ F, R i1 A ∧ f A j1 a1
h5 : fnnn (i2, j2) = n ∧ ∃ A ∈ F, R i2 A ∧ f A j2 a2
A2 : Set U
Aija1 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a1
Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2
h6 : (i1, j1) = (i2, j2)
h7 : i1 = i2 ∧ j1 = j2
h8 : A1 = A2
fA2fcnlonto : unique_val_on_N (f A2) ∧ nat_rel_onto (f A2) A2
fA2uniqueval : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : U⦄, f A2 n x1 → f A2 n x2 → x1 = x2
⊢ a1 = a2
Tactic:
show a1 = a2 from fA2uniqueval Aija1.right.right Aija2.right.right
Proof state after:
no goals
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
⊢ nat_rel_onto S (⋃₀ F)
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 : nat_rel_onto R F
S : Rel ℕ U := enum_union_fam F f R
⊢ ∀ ⦃x : U⦄, 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⦄, x ∈ ⋃₀ F → ∃ n, S n x
Tactic:
fix x : U
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
⊢ x ∈ ⋃₀ F → ∃ n, S n x