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

State before:
U : Type
F : Set (Set U)
f : Set U → Rel ℕ U
h1 : ctble F
h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A
⊢ ctble (⋃₀ F)
Tactic:
rewrite [Theorem_8_1_5_2] at h1
State after:
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
⊢ ctble (⋃₀ F)

State before:
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
⊢ ctble (⋃₀ F)
Tactic:
rewrite [Theorem_8_1_5_2]
State after:
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, fcnl_onto_from_nat R (⋃₀ F)

State before:
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, fcnl_onto_from_nat R (⋃₀ F)
Tactic:
obtain (R : Rel Nat (Set U)) (h3 : fcnl_onto_from_nat R F) from h1
State after:
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 : fcnl_onto_from_nat R F
⊢ ∃ R, fcnl_onto_from_nat R (⋃₀ F)

State before:
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 : fcnl_onto_from_nat R F
⊢ ∃ R, fcnl_onto_from_nat R (⋃₀ F)
Tactic:
define at h3
State after:
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
⊢ ∃ R, fcnl_onto_from_nat R (⋃₀ F)

State before:
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
⊢ ∃ R, fcnl_onto_from_nat R (⋃₀ F)
Tactic:
have Runiqueval : unique_val_on_N R := h3.left
State after:
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
⊢ ∃ R, fcnl_onto_from_nat R (⋃₀ F)

State before:
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
⊢ ∃ R, fcnl_onto_from_nat R (⋃₀ F)
Tactic:
have Ronto : nat_rel_onto R F := h3.right
State after:
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
⊢ ∃ R, fcnl_onto_from_nat R (⋃₀ F)

State before:
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
⊢ ∃ R, fcnl_onto_from_nat R (⋃₀ F)
Tactic:
set S : Rel Nat U := enum_union_fam F f R
State after:
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
⊢ ∃ R, fcnl_onto_from_nat R (⋃₀ F)

State before:
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
⊢ ∃ R, fcnl_onto_from_nat R (⋃₀ F)
Tactic:
apply Exists.intro S
State after:
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
⊢ fcnl_onto_from_nat S (⋃₀ F)

State before:
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
⊢ fcnl_onto_from_nat S (⋃₀ F)
Tactic:
define
State after:
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
⊢ unique_val_on_N S ∧ nat_rel_onto S (⋃₀ F)

State before:
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
⊢ unique_val_on_N S ∧ nat_rel_onto S (⋃₀ F)
Tactic:
apply And.intro
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
⊢ unique_val_on_N S

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)

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
⊢ unique_val_on_N S
Tactic:
define
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 : ℕ⦄ ⦃x1 x2 : U⦄, S n x1 → S n x2 → x1 = x2

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 : ℕ⦄ ⦃x1 x2 : U⦄, S n x1 → S n x2 → x1 = x2
Tactic:
fix n : Nat
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 : ℕ
⊢ ∀ ⦃x1 x2 : U⦄, S n x1 → S n x2 → x1 = x2

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 : ℕ
⊢ ∀ ⦃x1 x2 : U⦄, S n x1 → S n x2 → x1 = x2
Tactic:
fix a1 : U
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 : U
⊢ ∀ ⦃x2 : U⦄, S n a1 → S n x2 → a1 = x2

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 : U
⊢ ∀ ⦃x2 : U⦄, S n a1 → S n x2 → a1 = x2
Tactic:
fix a2 : U
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
⊢ S n a1 → S n a2 → a1 = a2

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
⊢ S n a1 → S n a2 → a1 = a2
Tactic:
assume Sna1 : S n a1
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 : S n a1
⊢ S n a2 → a1 = a2

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 : S n a1
⊢ S n a2 → a1 = a2
Tactic:
assume Sna2 : S n a2
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 : S n a1
Sna2 : S n a2
⊢ a1 = a2

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 : S n a1
Sna2 : S n a2
⊢ a1 = a2
Tactic:
define at Sna1
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 : S n a2
⊢ a1 = a2

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 : S n a2
⊢ a1 = a2
Tactic:
define at Sna2
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
⊢ a1 = a2

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
⊢ a1 = a2
Tactic:
obtain ((i1, j1) : Nat × Nat) (h4 : fnnn (i1, j1) = n ∧
  ∃ A ∈ F, R i1 A ∧ f A j1 a1) from Sna1
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 = a2

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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))
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

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
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

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)
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

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
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

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
State after:
no goals

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
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

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)
State after:
no goals