internlm/Lean-Github huggingface dataset:
Theorem: HTPI.eq_numElts_of_equinum
Proof state before:
U V : Type
A : Set U
B : Set V
n : ℕ
h1 : A ∼ B
h2 : numElts A n
⊢ numElts B n
Tactic:
rewrite [numElts_def] at h2
Proof state after:
U V : Type
A : Set U
B : Set V
n : ℕ
h1 : A ∼ B
h2 : I n ∼ A
⊢ numElts B n
Theorem: HTPI.eq_numElts_of_equinum
Proof state before:
U V : Type
A : Set U
B : Set V
n : ℕ
h1 : A ∼ B
h2 : I n ∼ A
⊢ numElts B n
Tactic:
rewrite [numElts_def]
Proof state after:
U V : Type
A : Set U
B : Set V
n : ℕ
h1 : A ∼ B
h2 : I n ∼ A
⊢ I n ∼ B
Theorem: HTPI.eq_numElts_of_equinum
Proof state before:
U V : Type
A : Set U
B : Set V
n : ℕ
h1 : A ∼ B
h2 : I n ∼ A
⊢ I n ∼ B
Tactic:
show I n ∼ B from Theorem_8_1_3_3 h2 h1
Proof state after:
no goals
Theorem: HTPI.Theorem_7_4_4
Proof state before:
m n : ℕ
h1 : rel_prime m n
⊢ phi (m * n) = phi m * phi n
Tactic:
have h2 : numElts (Set_rp_below m) (phi m) := phi_is_numElts m
Proof state after:
m n : ℕ
h1 : rel_prime m n
h2 : numElts (Set_rp_below m) (phi m)
⊢ phi (m * n) = phi m * phi n
Theorem: HTPI.Theorem_7_4_4
Proof state before:
m n : ℕ
h1 : rel_prime m n
h2 : numElts (Set_rp_below m) (phi m)
⊢ phi (m * n) = phi m * phi n
Tactic:
have h3 : numElts (Set_rp_below n) (phi n) := phi_is_numElts n
Proof state after:
m n : ℕ
h1 : rel_prime m n
h2 : numElts (Set_rp_below m) (phi m)
h3 : numElts (Set_rp_below n) (phi n)
⊢ phi (m * n) = phi m * phi n
Theorem: HTPI.Theorem_7_4_4
Proof state before:
m n : ℕ
h1 : rel_prime m n
h2 : numElts (Set_rp_below m) (phi m)
h3 : numElts (Set_rp_below n) (phi n)
⊢ phi (m * n) = phi m * phi n
Tactic:
have h4 : numElts (Set_rp_below (m * n)) (phi (m * n)) :=
  phi_is_numElts (m * n)
Proof state after:
m n : ℕ
h1 : rel_prime m n
h2 : numElts (Set_rp_below m) (phi m)
h3 : numElts (Set_rp_below n) (phi n)
h4 : numElts (Set_rp_below (m * n)) (phi (m * n))
⊢ phi (m * n) = phi m * phi n
Theorem: HTPI.Theorem_7_4_4
Proof state before:
m n : ℕ
h1 : rel_prime m n
h2 : numElts (Set_rp_below m) (phi m)
h3 : numElts (Set_rp_below n) (phi n)
h4 : numElts (Set_rp_below (m * n)) (phi (m * n))
⊢ phi (m * n) = phi m * phi n
Tactic:
have h5 : numElts (Set_rp_below m ×ₛ Set_rp_below n) (phi (m * n)) :=
  eq_numElts_of_equinum (Set_rp_below_prod h1) h4
Proof state after:
m n : ℕ
h1 : rel_prime m n
h2 : numElts (Set_rp_below m) (phi m)
h3 : numElts (Set_rp_below n) (phi n)
h4 : numElts (Set_rp_below (m * n)) (phi (m * n))
h5 : numElts (Set_rp_below m ×ₛ Set_rp_below n) (phi (m * n))
⊢ phi (m * n) = phi m * phi n
Theorem: HTPI.Theorem_7_4_4
Proof state before:
m n : ℕ
h1 : rel_prime m n
h2 : numElts (Set_rp_below m) (phi m)
h3 : numElts (Set_rp_below n) (phi n)
h4 : numElts (Set_rp_below (m * n)) (phi (m * n))
h5 : numElts (Set_rp_below m ×ₛ Set_rp_below n) (phi (m * n))
⊢ phi (m * n) = phi m * phi n
Tactic:
have h6 : numElts (Set_rp_below m ×ₛ Set_rp_below n) (phi m * phi n) :=
  numElts_prod h2 h3
Proof state after:
m n : ℕ
h1 : rel_prime m n
h2 : numElts (Set_rp_below m) (phi m)
h3 : numElts (Set_rp_below n) (phi n)
h4 : numElts (Set_rp_below (m * n)) (phi (m * n))
h5 : numElts (Set_rp_below m ×ₛ Set_rp_below n) (phi (m * n))
h6 : numElts (Set_rp_below m ×ₛ Set_rp_below n) (phi m * phi n)
⊢ phi (m * n) = phi m * phi n
Theorem: HTPI.Theorem_7_4_4
Proof state before:
m n : ℕ
h1 : rel_prime m n
h2 : numElts (Set_rp_below m) (phi m)
h3 : numElts (Set_rp_below n) (phi n)
h4 : numElts (Set_rp_below (m * n)) (phi (m * n))
h5 : numElts (Set_rp_below m ×ₛ Set_rp_below n) (phi (m * n))
h6 : numElts (Set_rp_below m ×ₛ Set_rp_below n) (phi m * phi n)
⊢ phi (m * n) = phi m * phi n
Tactic:
show phi (m * n) = phi m * phi n from numElts_unique h5 h6
Proof state after:
no goals
Theorem: HTPI.Theorem_8_2_1_1
Proof state before:
U V : Type
A : Set U
B : Set V
h1 : ctble A
h2 : ctble B
⊢ ctble (A ×ₛ B)
Tactic:
rewrite [ctble_iff_equinum_set_nat] at h1
Proof state after:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ctble B
⊢ ctble (A ×ₛ B)
Theorem: HTPI.Theorem_8_2_1_1
Proof state before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ctble B
⊢ ctble (A ×ₛ B)
Tactic:
rewrite [ctble_iff_equinum_set_nat] at h2
Proof state after:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
⊢ ctble (A ×ₛ B)
Theorem: HTPI.Theorem_8_2_1_1
Proof state before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
⊢ ctble (A ×ₛ B)
Tactic:
obtain (I : Set Nat) (h3 : I ∼ A) from h1
Proof state after:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
⊢ ctble (A ×ₛ B)
Theorem: HTPI.Theorem_8_2_1_1
Proof state before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
⊢ ctble (A ×ₛ B)
Tactic:
obtain (J : Set Nat) (h4 : J ∼ B) from h2
Proof state after:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
⊢ ctble (A ×ₛ B)
Theorem: HTPI.Theorem_8_2_1_1
Proof state before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
⊢ ctble (A ×ₛ B)
Tactic:
have h5 : I ×ₛ J ∼ A ×ₛ B := Theorem_8_1_2_1 h3 h4
Proof state after:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
⊢ ctble (A ×ₛ B)
Theorem: HTPI.Theorem_8_2_1_1
Proof state before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
⊢ ctble (A ×ₛ B)
Tactic:
have h6 : I ×ₛ J ⊆ Univ (Nat × Nat) := by
  fix p : Nat × Nat
  assume h6 : p ∈ I ×ₛ J
  show p ∈ Univ (Nat × Nat) from elt_Univ p
  done
Proof state after:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
⊢ ctble (A ×ₛ B)
Theorem: HTPI.Theorem_8_2_1_1
Proof state before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
⊢ ctble (A ×ₛ B)
Tactic:
have h7 : ctble (Univ (Nat × Nat)) := by
  define   apply Or.inr
  rewrite [denum_def]
  show Univ Nat ∼ Univ (Nat × Nat) from Theorem_8_1_3_2 NxN_equinum_N
  done
Proof state after:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
h7 : ctble (Univ (ℕ × ℕ))
⊢ ctble (A ×ₛ B)
Theorem: HTPI.Theorem_8_2_1_1
Proof state before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
h7 : ctble (Univ (ℕ × ℕ))
⊢ ctble (A ×ₛ B)
Tactic:
have h8 : ctble (I ×ₛ J) := Exercise_8_1_17 h6 h7
Proof state after:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
h7 : ctble (Univ (ℕ × ℕ))
h8 : ctble (I ×ₛ J)
⊢ ctble (A ×ₛ B)
Theorem: HTPI.Theorem_8_2_1_1
Proof state before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
h7 : ctble (Univ (ℕ × ℕ))
h8 : ctble (I ×ₛ J)
⊢ ctble (A ×ₛ B)
Tactic:
show ctble (A ×ₛ B) from ctble_of_equinum_ctble h5 h8
Proof state after:
no goals
Theorem: HTPI.Theorem_8_2_1_1
Proof state before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
⊢ I ×ₛ J ⊆ Univ (ℕ × ℕ)
Tactic:
fix p : Nat × Nat
Proof state after:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
p : ℕ × ℕ
⊢ p ∈ I ×ₛ J → p ∈ Univ (ℕ × ℕ)
Theorem: HTPI.Theorem_8_2_1_1
Proof state before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
p : ℕ × ℕ
⊢ p ∈ I ×ₛ J → p ∈ Univ (ℕ × ℕ)
Tactic:
assume h6 : p ∈ I ×ₛ J
Proof state after:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
p : ℕ × ℕ
h6 : p ∈ I ×ₛ J
⊢ p ∈ Univ (ℕ × ℕ)
Theorem: HTPI.Theorem_8_2_1_1
Proof state before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
p : ℕ × ℕ
h6 : p ∈ I ×ₛ J
⊢ p ∈ Univ (ℕ × ℕ)
Tactic:
show p ∈ Univ (Nat × Nat) from elt_Univ p
Proof state after:
no goals
Theorem: HTPI.Theorem_8_2_1_1
Proof state before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
⊢ ctble (Univ (ℕ × ℕ))
Tactic:
define
Proof state after:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
⊢ finite (Univ (ℕ × ℕ)) ∨ denum (Univ (ℕ × ℕ))
Theorem: HTPI.Theorem_8_2_1_1
Proof state before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
⊢ finite (Univ (ℕ × ℕ)) ∨ denum (Univ (ℕ × ℕ))
Tactic:
apply Or.inr
Proof state after:
case h
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
⊢ denum (Univ (ℕ × ℕ))
Theorem: HTPI.Theorem_8_2_1_1
Proof state before:
case h
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
⊢ denum (Univ (ℕ × ℕ))
Tactic:
rewrite [denum_def]
Proof state after:
case h
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
⊢ Univ ℕ ∼ Univ (ℕ × ℕ)
Theorem: HTPI.Theorem_8_2_1_1
Proof state before:
case h
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
⊢ Univ ℕ ∼ Univ (ℕ × ℕ)
Tactic:
show Univ Nat ∼ Univ (Nat × Nat) from Theorem_8_1_3_2 NxN_equinum_N
Proof state after:
no goals
Theorem: HTPI.Lemma_8_2_2_1
Proof 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
Proof 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)
Theorem: HTPI.Lemma_8_2_2_1
Proof 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]
Proof 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)
Theorem: HTPI.Lemma_8_2_2_1
Proof 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
Proof 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)
Theorem: HTPI.Lemma_8_2_2_1
Proof 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
Proof 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)
Theorem: HTPI.Lemma_8_2_2_1
Proof 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
Proof 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)
Theorem: HTPI.Lemma_8_2_2_1
Proof 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
Proof 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)
Theorem: HTPI.Lemma_8_2_2_1
Proof 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
Proof 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)
Theorem: HTPI.Lemma_8_2_2_1
Proof 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
Proof 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)
Theorem: HTPI.Lemma_8_2_2_1
Proof 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
Proof 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)
Theorem: HTPI.Lemma_8_2_2_1
Proof 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
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
⊢ 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)
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
⊢ unique_val_on_N S
Tactic:
define
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 : ℕ⦄ ⦃x1 x2 : U⦄, S n x1 → S n x2 → x1 = x2
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 : ℕ⦄ ⦃x1 x2 : U⦄, S n x1 → S n x2 → x1 = x2
Tactic:
fix n : Nat
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 : ℕ
⊢ ∀ ⦃x1 x2 : U⦄, S n x1 → S n x2 → x1 = x2
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 : ℕ
⊢ ∀ ⦃x1 x2 : U⦄, S n x1 → S n x2 → x1 = x2
Tactic:
fix a1 : U
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 : U
⊢ ∀ ⦃x2 : U⦄, S n a1 → S n x2 → a1 = x2
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 : U
⊢ ∀ ⦃x2 : U⦄, S n a1 → S n x2 → a1 = x2
Tactic:
fix a2 : U
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
⊢ S n a1 → S n 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
⊢ S n a1 → S n a2 → a1 = a2
Tactic:
assume Sna1 : S n a1
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 : S n a1
⊢ S n 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 : S n a1
⊢ S n a2 → a1 = a2
Tactic:
assume Sna2 : S n a2
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 : S n a1
Sna2 : S n 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 : S n a1
Sna2 : S n a2
⊢ a1 = a2
Tactic:
define at Sna1
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 : S n 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 : S n a2
⊢ a1 = a2
Tactic:
define at 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
⊢ 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
⊢ a1 = a2
Tactic:
obtain ((i1, j1) : Nat × Nat) (h4 : fnnn (i1, j1) = n ∧
  ∃ A ∈ F, R i1 A ∧ f A j1 a1) from Sna1
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 = a2