internlm/Lean-Github huggingface dataset:
Theorem: HTPI.inv_enum_fcnl
Proof state before:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
s1 s2 : ℕ
h2 : n ∈ A ∧ num_elts_below A n s1
h3 : invRel (enum A) n s2
⊢ s1 = s2
Tactic:
define at h3
Proof state after:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
s1 s2 : ℕ
h2 : n ∈ A ∧ num_elts_below A n s1
h3 : n ∈ A ∧ num_elts_below A n s2
⊢ s1 = s2
Theorem: HTPI.inv_enum_fcnl
Proof state before:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
s1 s2 : ℕ
h2 : n ∈ A ∧ num_elts_below A n s1
h3 : n ∈ A ∧ num_elts_below A n s2
⊢ s1 = s2
Tactic:
show s1 = s2 from neb_unique A h2.right h3.right
Proof state after:
no goals
Theorem: HTPI.bdd_subset_nat_match
Proof state before:
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ matching (enum A) (I s) A
Tactic:
define
Proof state after:
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ rel_within (enum A) (I s) A ∧ fcnl_on (enum A) (I s) ∧ fcnl_on (invRel (enum A)) A
Theorem: HTPI.bdd_subset_nat_match
Proof state before:
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ rel_within (enum A) (I s) A ∧ fcnl_on (enum A) (I s) ∧ fcnl_on (invRel (enum A)) A
Tactic:
apply And.intro
Proof state after:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ rel_within (enum A) (I s) A

case right
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ fcnl_on (enum A) (I s) ∧ fcnl_on (invRel (enum A)) A
Theorem: HTPI.bdd_subset_nat_match
Proof state before:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ rel_within (enum A) (I s) A
Tactic:
define
Proof state after:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ ∀ ⦃x y : ℕ⦄, enum A x y → x ∈ I s ∧ y ∈ A
Theorem: HTPI.bdd_subset_nat_match
Proof state before:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ ∀ ⦃x y : ℕ⦄, enum A x y → x ∈ I s ∧ y ∈ A
Tactic:
fix t : Nat
Proof state after:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t : ℕ
⊢ ∀ ⦃y : ℕ⦄, enum A t y → t ∈ I s ∧ y ∈ A
Theorem: HTPI.bdd_subset_nat_match
Proof state before:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t : ℕ
⊢ ∀ ⦃y : ℕ⦄, enum A t y → t ∈ I s ∧ y ∈ A
Tactic:
fix n : Nat
Proof state after:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
⊢ enum A t n → t ∈ I s ∧ n ∈ A
Theorem: HTPI.bdd_subset_nat_match
Proof state before:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
⊢ enum A t n → t ∈ I s ∧ n ∈ A
Tactic:
assume h3 : enum A t n
Proof state after:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : enum A t n
⊢ t ∈ I s ∧ n ∈ A
Theorem: HTPI.bdd_subset_nat_match
Proof state before:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : enum A t n
⊢ t ∈ I s ∧ n ∈ A
Tactic:
have h4 : ∀ ⦃m : Nat⦄, m ≥ n + 1 → ∀ ⦃t_1 : Nat⦄, num_elts_below A m t_1 → t < t_1 :=
  neb_increase h3
Proof state after:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : enum A t n
h4 : ∀ ⦃m : ℕ⦄, m ≥ n + 1 → ∀ ⦃t_1 : ℕ⦄, num_elts_below A m t_1 → t < t_1
⊢ t ∈ I s ∧ n ∈ A
Theorem: HTPI.bdd_subset_nat_match
Proof state before:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : enum A t n
h4 : ∀ ⦃m : ℕ⦄, m ≥ n + 1 → ∀ ⦃t_1 : ℕ⦄, num_elts_below A m t_1 → t < t_1
⊢ t ∈ I s ∧ n ∈ A
Tactic:
define at h3
Proof state after:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : n ∈ A ∧ num_elts_below A n t
h4 : ∀ ⦃m : ℕ⦄, m ≥ n + 1 → ∀ ⦃t_1 : ℕ⦄, num_elts_below A m t_1 → t < t_1
⊢ t ∈ I s ∧ n ∈ A
Theorem: HTPI.bdd_subset_nat_match
Proof state before:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : n ∈ A ∧ num_elts_below A n t
h4 : ∀ ⦃m : ℕ⦄, m ≥ n + 1 → ∀ ⦃t_1 : ℕ⦄, num_elts_below A m t_1 → t < t_1
⊢ t ∈ I s ∧ n ∈ A
Tactic:
apply And.intro _ h3.left
Proof state after:
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : n ∈ A ∧ num_elts_below A n t
h4 : ∀ ⦃m : ℕ⦄, m ≥ n + 1 → ∀ ⦃t_1 : ℕ⦄, num_elts_below A m t_1 → t < t_1
⊢ t ∈ I s
Theorem: HTPI.bdd_subset_nat_match
Proof state before:
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : n ∈ A ∧ num_elts_below A n t
h4 : ∀ ⦃m : ℕ⦄, m ≥ n + 1 → ∀ ⦃t_1 : ℕ⦄, num_elts_below A m t_1 → t < t_1
⊢ t ∈ I s
Tactic:
define
Proof state after:
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : n ∈ A ∧ num_elts_below A n t
h4 : ∀ ⦃m : ℕ⦄, m ≥ n + 1 → ∀ ⦃t_1 : ℕ⦄, num_elts_below A m t_1 → t < t_1
⊢ t < s
Theorem: HTPI.bdd_subset_nat_match
Proof state before:
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : n ∈ A ∧ num_elts_below A n t
h4 : ∀ ⦃m : ℕ⦄, m ≥ n + 1 → ∀ ⦃t_1 : ℕ⦄, num_elts_below A m t_1 → t < t_1
⊢ t < s
Tactic:
have h5 : n < m := h1 n h3.left
Proof state after:
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : n ∈ A ∧ num_elts_below A n t
h4 : ∀ ⦃m : ℕ⦄, m ≥ n + 1 → ∀ ⦃t_1 : ℕ⦄, num_elts_below A m t_1 → t < t_1
h5 : n < m
⊢ t < s
Theorem: HTPI.bdd_subset_nat_match
Proof state before:
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : n ∈ A ∧ num_elts_below A n t
h4 : ∀ ⦃m : ℕ⦄, m ≥ n + 1 → ∀ ⦃t_1 : ℕ⦄, num_elts_below A m t_1 → t < t_1
h5 : n < m
⊢ t < s
Tactic:
have h6 : m ≥ n + 1 := h5
Proof state after:
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : n ∈ A ∧ num_elts_below A n t
h4 : ∀ ⦃m : ℕ⦄, m ≥ n + 1 → ∀ ⦃t_1 : ℕ⦄, num_elts_below A m t_1 → t < t_1
h5 : n < m
h6 : m ≥ n + 1
⊢ t < s
Theorem: HTPI.bdd_subset_nat_match
Proof state before:
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : n ∈ A ∧ num_elts_below A n t
h4 : ∀ ⦃m : ℕ⦄, m ≥ n + 1 → ∀ ⦃t_1 : ℕ⦄, num_elts_below A m t_1 → t < t_1
h5 : n < m
h6 : m ≥ n + 1
⊢ t < s
Tactic:
show t < s from h4 h6 h2
Proof state after:
no goals
Theorem: HTPI.bdd_subset_nat_match
Proof state before:
case right
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ fcnl_on (enum A) (I s) ∧ fcnl_on (invRel (enum A)) A
Tactic:
apply And.intro
Proof state after:
case right.left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ fcnl_on (enum A) (I s)

case right.right
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ fcnl_on (invRel (enum A)) A
Theorem: HTPI.bdd_subset_nat_match
Proof state before:
case right.left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ fcnl_on (enum A) (I s)
Tactic:
define
Proof state after:
case right.left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ ∀ ⦃x : ℕ⦄, x ∈ I s → ∃! y, enum A x y
Theorem: HTPI.bdd_subset_nat_match
Proof state before:
case right.left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ ∀ ⦃x : ℕ⦄, x ∈ I s → ∃! y, enum A x y
Tactic:
fix t : Nat
Proof state after:
case right.left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t : ℕ
⊢ t ∈ I s → ∃! y, enum A t y
Theorem: HTPI.bdd_subset_nat_match
Proof state before:
case right.left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t : ℕ
⊢ t ∈ I s → ∃! y, enum A t y
Tactic:
assume h3 : t ∈ I s
Proof state after:
case right.left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t : ℕ
h3 : t ∈ I s
⊢ ∃! y, enum A t y
Theorem: HTPI.bdd_subset_nat_match
Proof state before:
case right.left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t : ℕ
h3 : t ∈ I s
⊢ ∃! y, enum A t y
Tactic:
define at h3
Proof state after:
case right.left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t : ℕ
h3 : t < s
⊢ ∃! y, enum A t y
Theorem: HTPI.bdd_subset_nat_match
Proof state before:
case right.left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t : ℕ
h3 : t < s
⊢ ∃! y, enum A t y
Tactic:
exists_unique
Proof state after:
case right.left.Existence
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t : ℕ
h3 : t < s
⊢ ∃ y, enum A t y

case right.left.Uniqueness
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t : ℕ
h3 : t < s
⊢ ∀ (y_1 y_2 : ℕ), enum A t y_1 → enum A t y_2 → y_1 = y_2
Theorem: HTPI.bdd_subset_nat_match
Proof state before:
case right.left.Existence
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t : ℕ
h3 : t < s
⊢ ∃ y, enum A t y
Tactic:
show ∃ (y : Nat), enum A t y from enum_not_skip h2 t h3
Proof state after:
no goals
Theorem: HTPI.bdd_subset_nat_match
Proof state before:
case right.left.Uniqueness
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t : ℕ
h3 : t < s
⊢ ∀ (y_1 y_2 : ℕ), enum A t y_1 → enum A t y_2 → y_1 = y_2
Tactic:
show ∀ (y_1 y_2 : Nat), enum A t y_1 → enum A t y_2 → y_1 = y_2 from
  enum_unique A t
Proof state after:
no goals
Theorem: HTPI.bdd_subset_nat_match
Proof state before:
case right.right
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ fcnl_on (invRel (enum A)) A
Tactic:
show fcnl_on (invRel (enum A)) A from inv_enum_fcnl A
Proof state after:
no goals
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ fcnl_on (enum A) (Univ ℕ)
Tactic:
define
Proof state after:
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ ∀ ⦃x : ℕ⦄, x ∈ Univ ℕ → ∃! y, enum A x y
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ ∀ ⦃x : ℕ⦄, x ∈ Univ ℕ → ∃! y, enum A x y
Tactic:
by_induc
Proof state after:
case Base_Case
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ 0 ∈ Univ ℕ → ∃! y, enum A 0 y

case Induction_Step
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ ∀ (x : ℕ), (x ∈ Univ ℕ → ∃! y, enum A x y) → x + 1 ∈ Univ ℕ → ∃! y, enum A (x + 1) y
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Base_Case
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ 0 ∈ Univ ℕ → ∃! y, enum A 0 y
Tactic:
assume h2 : 0 ∈ Univ Nat
Proof state after:
case Base_Case
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
⊢ ∃! y, enum A 0 y
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Base_Case
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
⊢ ∃! y, enum A 0 y
Tactic:
exists_unique
Proof state after:
case Base_Case.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
⊢ ∃ y, enum A 0 y

case Base_Case.Uniqueness
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
⊢ ∀ (y_1 y_2 : ℕ), enum A 0 y_1 → enum A 0 y_2 → y_1 = y_2
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Base_Case.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
⊢ ∃ y, enum A 0 y
Tactic:
obtain (n : Nat) (h3 : n ∈ A ∧ n ≥0) from h1 0
Proof state after:
case Base_Case.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
n : ℕ
h3 : n ∈ A ∧ n ≥ 0
⊢ ∃ y, enum A 0 y
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Base_Case.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
n : ℕ
h3 : n ∈ A ∧ n ≥ 0
⊢ ∃ y, enum A 0 y
Tactic:
obtain (s : Nat) (h4 : num_elts_below A (n + 1) s) from neb_exists A (n + 1)
Proof state after:
case Base_Case.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
n : ℕ
h3 : n ∈ A ∧ n ≥ 0
s : ℕ
h4 : num_elts_below A (n + 1) s
⊢ ∃ y, enum A 0 y
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Base_Case.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
n : ℕ
h3 : n ∈ A ∧ n ≥ 0
s : ℕ
h4 : num_elts_below A (n + 1) s
⊢ ∃ y, enum A 0 y
Tactic:
have h5 : ∀ (t : Nat), t < s → ∃ (n : Nat), enum A t n := enum_not_skip h4
Proof state after:
case Base_Case.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
n : ℕ
h3 : n ∈ A ∧ n ≥ 0
s : ℕ
h4 : num_elts_below A (n + 1) s
h5 : ∀ t < s, ∃ n, enum A t n
⊢ ∃ y, enum A 0 y
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Base_Case.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
n : ℕ
h3 : n ∈ A ∧ n ≥ 0
s : ℕ
h4 : num_elts_below A (n + 1) s
h5 : ∀ t < s, ∃ n, enum A t n
⊢ ∃ y, enum A 0 y
Tactic:
rewrite [neb_step_elt h3.left] at h4
Proof state after:
case Base_Case.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
n : ℕ
h3 : n ∈ A ∧ n ≥ 0
s : ℕ
h4 : 1 ≤ s ∧ num_elts_below A n (s - 1)
h5 : ∀ t < s, ∃ n, enum A t n
⊢ ∃ y, enum A 0 y
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Base_Case.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
n : ℕ
h3 : n ∈ A ∧ n ≥ 0
s : ℕ
h4 : 1 ≤ s ∧ num_elts_below A n (s - 1)
h5 : ∀ t < s, ∃ n, enum A t n
⊢ ∃ y, enum A 0 y
Tactic:
show ∃ (y : Nat), enum A 0 y from h5 0 h4.left
Proof state after:
no goals
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Base_Case.Uniqueness
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
⊢ ∀ (y_1 y_2 : ℕ), enum A 0 y_1 → enum A 0 y_2 → y_1 = y_2
Tactic:
show ∀ (y_1 y_2 : Nat), enum A 0 y_1 → enum A 0 y_2 → y_1 = y_2 from enum_unique A 0
Proof state after:
no goals
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Induction_Step
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ ∀ (x : ℕ), (x ∈ Univ ℕ → ∃! y, enum A x y) → x + 1 ∈ Univ ℕ → ∃! y, enum A (x + 1) y
Tactic:
fix s : Nat
Proof state after:
case Induction_Step
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
⊢ (s ∈ Univ ℕ → ∃! y, enum A s y) → s + 1 ∈ Univ ℕ → ∃! y, enum A (s + 1) y
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Induction_Step
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
⊢ (s ∈ Univ ℕ → ∃! y, enum A s y) → s + 1 ∈ Univ ℕ → ∃! y, enum A (s + 1) y
Tactic:
assume ih : s ∈ Univ Nat → ∃! (y : Nat), enum A s y
Proof state after:
case Induction_Step
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
⊢ s + 1 ∈ Univ ℕ → ∃! y, enum A (s + 1) y
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Induction_Step
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
⊢ s + 1 ∈ Univ ℕ → ∃! y, enum A (s + 1) y
Tactic:
assume h2 : s + 1 ∈ Univ Nat
Proof state after:
case Induction_Step
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
⊢ ∃! y, enum A (s + 1) y
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Induction_Step
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
⊢ ∃! y, enum A (s + 1) y
Tactic:
exists_unique
Proof state after:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
⊢ ∃ y, enum A (s + 1) y

case Induction_Step.Uniqueness
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
⊢ ∀ (y_1 y_2 : ℕ), enum A (s + 1) y_1 → enum A (s + 1) y_2 → y_1 = y_2
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
⊢ ∃ y, enum A (s + 1) y
Tactic:
have h3 : s ∈ Univ Nat := elt_Univ s
Proof state after:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
⊢ ∃ y, enum A (s + 1) y
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
⊢ ∃ y, enum A (s + 1) y
Tactic:
obtain (m : Nat) (h4 : enum A s m)
  (h5 : ∀ (y_1 y_2 : Nat), enum A s y_1 → enum A s y_2 → y_1 = y_2) from ih h3
Proof state after:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
⊢ ∃ y, enum A (s + 1) y
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
⊢ ∃ y, enum A (s + 1) y
Tactic:
obtain (n : Nat) (h6 : n ∈ A ∧ n ≥ m + 1) from h1 (m + 1)
Proof state after:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
⊢ ∃ y, enum A (s + 1) y
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
⊢ ∃ y, enum A (s + 1) y
Tactic:
obtain (t : Nat) (h7 : num_elts_below A n t) from neb_exists A n
Proof state after:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
⊢ ∃ y, enum A (s + 1) y
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
⊢ ∃ y, enum A (s + 1) y
Tactic:
have h8 : s < t := neb_increase h4 h6.right h7
Proof state after:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
⊢ ∃ y, enum A (s + 1) y
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
⊢ ∃ y, enum A (s + 1) y
Tactic:
have h9 : s + 1 < t ∨ s + 1 = t := Nat.lt_or_eq_of_le h8
Proof state after:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
h9 : s + 1 < t ∨ s + 1 = t
⊢ ∃ y, enum A (s + 1) y
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
h9 : s + 1 < t ∨ s + 1 = t
⊢ ∃ y, enum A (s + 1) y
Tactic:
by_cases on h9
Proof state after:
case Induction_Step.Existence.Case_1
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
h9 : s + 1 < t
⊢ ∃ y, enum A (s + 1) y

case Induction_Step.Existence.Case_2
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
h9 : s + 1 = t
⊢ ∃ y, enum A (s + 1) y
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Induction_Step.Existence.Case_1
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
h9 : s + 1 < t
⊢ ∃ y, enum A (s + 1) y
Tactic:
show ∃ (y : Nat), enum A (s + 1) y from enum_not_skip h7 (s + 1) h9
Proof state after:
no goals
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Induction_Step.Existence.Case_2
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
h9 : s + 1 = t
⊢ ∃ y, enum A (s + 1) y
Tactic:
rewrite [h9]
Proof state after:
case Induction_Step.Existence.Case_2
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
h9 : s + 1 = t
⊢ ∃ y, enum A t y
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Induction_Step.Existence.Case_2
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
h9 : s + 1 = t
⊢ ∃ y, enum A t y
Tactic:
apply Exists.intro n
Proof state after:
case Induction_Step.Existence.Case_2
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
h9 : s + 1 = t
⊢ enum A t n
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Induction_Step.Existence.Case_2
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
h9 : s + 1 = t
⊢ enum A t n
Tactic:
define
Proof state after:
case Induction_Step.Existence.Case_2
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
h9 : s + 1 = t
⊢ n ∈ A ∧ num_elts_below A n t
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Induction_Step.Existence.Case_2
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
h9 : s + 1 = t
⊢ n ∈ A ∧ num_elts_below A n t
Tactic:
show n ∈ A ∧ num_elts_below A n t from And.intro h6.left h7
Proof state after:
no goals
Theorem: HTPI.enum_fcnl_of_unbdd
Proof state before:
case Induction_Step.Uniqueness
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
⊢ ∀ (y_1 y_2 : ℕ), enum A (s + 1) y_1 → enum A (s + 1) y_2 → y_1 = y_2
Tactic:
show ∀ (y_1 y_2 : Nat), enum A (s + 1) y_1 → enum A (s + 1) y_2 → y_1 = y_2
  from enum_unique A (s + 1)
Proof state after:
no goals
Theorem: HTPI.unbdd_subset_nat_match
Proof state before:
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ matching (enum A) (Univ ℕ) A
Tactic:
define
Proof state after:
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ rel_within (enum A) (Univ ℕ) A ∧ fcnl_on (enum A) (Univ ℕ) ∧ fcnl_on (invRel (enum A)) A