internlm/Lean-Github huggingface dataset:
Theorem: HTPI.neb_increase
Proof state before:
case Base_Case
A : Set ℕ
n s : ℕ
h1 : n ∈ A ∧ num_elts_below A n s
t : ℕ
h2 : 1 ≤ t ∧ num_elts_below A n (t - 1)
h3 : s = t - 1
⊢ s < t
Tactic:
show s < t from
  calc s
    _ = t - 1 := h3
    _ < t - 1 + 1 := by linarith
    _ = t := Nat.sub_add_cancel h2.left
Proof state after:
no goals
Theorem: HTPI.neb_increase
Proof state before:
A : Set ℕ
n s : ℕ
h1 : n ∈ A ∧ num_elts_below A n s
t : ℕ
h2 : 1 ≤ t ∧ num_elts_below A n (t - 1)
h3 : s = t - 1
⊢ t - 1 < t - 1 + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.neb_increase
Proof state before:
case Induction_Step
A : Set ℕ
n s : ℕ
h1 : enum A s n
⊢ ∀ m ≥ n + 1, (∀ ⦃t : ℕ⦄, num_elts_below A m t → s < t) → ∀ ⦃t : ℕ⦄, num_elts_below A (m + 1) t → s < t
Tactic:
fix m : Nat
Proof state after:
case Induction_Step
A : Set ℕ
n s : ℕ
h1 : enum A s n
m : ℕ
⊢ m ≥ n + 1 → (∀ ⦃t : ℕ⦄, num_elts_below A m t → s < t) → ∀ ⦃t : ℕ⦄, num_elts_below A (m + 1) t → s < t
Theorem: HTPI.neb_increase
Proof state before:
case Induction_Step
A : Set ℕ
n s : ℕ
h1 : enum A s n
m : ℕ
⊢ m ≥ n + 1 → (∀ ⦃t : ℕ⦄, num_elts_below A m t → s < t) → ∀ ⦃t : ℕ⦄, num_elts_below A (m + 1) t → s < t
Tactic:
assume h2 : m ≥ n + 1
Proof state after:
case Induction_Step
A : Set ℕ
n s : ℕ
h1 : enum A s n
m : ℕ
h2 : m ≥ n + 1
⊢ (∀ ⦃t : ℕ⦄, num_elts_below A m t → s < t) → ∀ ⦃t : ℕ⦄, num_elts_below A (m + 1) t → s < t
Theorem: HTPI.neb_increase
Proof state before:
case Induction_Step
A : Set ℕ
n s : ℕ
h1 : enum A s n
m : ℕ
h2 : m ≥ n + 1
⊢ (∀ ⦃t : ℕ⦄, num_elts_below A m t → s < t) → ∀ ⦃t : ℕ⦄, num_elts_below A (m + 1) t → s < t
Tactic:
assume ih : ∀ ⦃t : Nat⦄, num_elts_below A m t → s < t
Proof state after:
case Induction_Step
A : Set ℕ
n s : ℕ
h1 : enum A s n
m : ℕ
h2 : m ≥ n + 1
ih : ∀ ⦃t : ℕ⦄, num_elts_below A m t → s < t
⊢ ∀ ⦃t : ℕ⦄, num_elts_below A (m + 1) t → s < t
Theorem: HTPI.neb_increase
Proof state before:
case Induction_Step
A : Set ℕ
n s : ℕ
h1 : enum A s n
m : ℕ
h2 : m ≥ n + 1
ih : ∀ ⦃t : ℕ⦄, num_elts_below A m t → s < t
⊢ ∀ ⦃t : ℕ⦄, num_elts_below A (m + 1) t → s < t
Tactic:
fix t : Nat
Proof state after:
case Induction_Step
A : Set ℕ
n s : ℕ
h1 : enum A s n
m : ℕ
h2 : m ≥ n + 1
ih : ∀ ⦃t : ℕ⦄, num_elts_below A m t → s < t
t : ℕ
⊢ num_elts_below A (m + 1) t → s < t
Theorem: HTPI.neb_increase
Proof state before:
case Induction_Step
A : Set ℕ
n s : ℕ
h1 : enum A s n
m : ℕ
h2 : m ≥ n + 1
ih : ∀ ⦃t : ℕ⦄, num_elts_below A m t → s < t
t : ℕ
⊢ num_elts_below A (m + 1) t → s < t
Tactic:
assume h3 : num_elts_below A (m + 1) t
Proof state after:
case Induction_Step
A : Set ℕ
n s : ℕ
h1 : enum A s n
m : ℕ
h2 : m ≥ n + 1
ih : ∀ ⦃t : ℕ⦄, num_elts_below A m t → s < t
t : ℕ
h3 : num_elts_below A (m + 1) t
⊢ s < t
Theorem: HTPI.neb_increase
Proof state before:
case Induction_Step
A : Set ℕ
n s : ℕ
h1 : enum A s n
m : ℕ
h2 : m ≥ n + 1
ih : ∀ ⦃t : ℕ⦄, num_elts_below A m t → s < t
t : ℕ
h3 : num_elts_below A (m + 1) t
⊢ s < t
Tactic:
by_cases h4 : m ∈ A
Proof state after:
case pos
A : Set ℕ
n s : ℕ
h1 : enum A s n
m : ℕ
h2 : m ≥ n + 1
ih : ∀ ⦃t : ℕ⦄, num_elts_below A m t → s < t
t : ℕ
h3 : num_elts_below A (m + 1) t
h4 : m ∈ A
⊢ s < t

case neg
A : Set ℕ
n s : ℕ
h1 : enum A s n
m : ℕ
h2 : m ≥ n + 1
ih : ∀ ⦃t : ℕ⦄, num_elts_below A m t → s < t
t : ℕ
h3 : num_elts_below A (m + 1) t
h4 : m ∉ A
⊢ s < t
Theorem: HTPI.neb_increase
Proof state before:
case pos
A : Set ℕ
n s : ℕ
h1 : enum A s n
m : ℕ
h2 : m ≥ n + 1
ih : ∀ ⦃t : ℕ⦄, num_elts_below A m t → s < t
t : ℕ
h3 : num_elts_below A (m + 1) t
h4 : m ∈ A
⊢ s < t
Tactic:
rewrite [neb_step_elt h4] at h3
Proof state after:
case pos
A : Set ℕ
n s : ℕ
h1 : enum A s n
m : ℕ
h2 : m ≥ n + 1
ih : ∀ ⦃t : ℕ⦄, num_elts_below A m t → s < t
t : ℕ
h3 : 1 ≤ t ∧ num_elts_below A m (t - 1)
h4 : m ∈ A
⊢ s < t
Theorem: HTPI.neb_increase
Proof state before:
case pos
A : Set ℕ
n s : ℕ
h1 : enum A s n
m : ℕ
h2 : m ≥ n + 1
ih : ∀ ⦃t : ℕ⦄, num_elts_below A m t → s < t
t : ℕ
h3 : 1 ≤ t ∧ num_elts_below A m (t - 1)
h4 : m ∈ A
⊢ s < t
Tactic:
have h5 : s < t - 1 := ih h3.right
Proof state after:
case pos
A : Set ℕ
n s : ℕ
h1 : enum A s n
m : ℕ
h2 : m ≥ n + 1
ih : ∀ ⦃t : ℕ⦄, num_elts_below A m t → s < t
t : ℕ
h3 : 1 ≤ t ∧ num_elts_below A m (t - 1)
h4 : m ∈ A
h5 : s < t - 1
⊢ s < t
Theorem: HTPI.neb_increase
Proof state before:
case pos
A : Set ℕ
n s : ℕ
h1 : enum A s n
m : ℕ
h2 : m ≥ n + 1
ih : ∀ ⦃t : ℕ⦄, num_elts_below A m t → s < t
t : ℕ
h3 : 1 ≤ t ∧ num_elts_below A m (t - 1)
h4 : m ∈ A
h5 : s < t - 1
⊢ s < t
Tactic:
show s < t from
  calc s
    _ < t - 1 := h5
    _ ≤ t := Nat.sub_le _ _
Proof state after:
no goals
Theorem: HTPI.neb_increase
Proof state before:
case neg
A : Set ℕ
n s : ℕ
h1 : enum A s n
m : ℕ
h2 : m ≥ n + 1
ih : ∀ ⦃t : ℕ⦄, num_elts_below A m t → s < t
t : ℕ
h3 : num_elts_below A (m + 1) t
h4 : m ∉ A
⊢ s < t
Tactic:
rewrite [neb_step_not_elt h4] at h3
Proof state after:
case neg
A : Set ℕ
n s : ℕ
h1 : enum A s n
m : ℕ
h2 : m ≥ n + 1
ih : ∀ ⦃t : ℕ⦄, num_elts_below A m t → s < t
t : ℕ
h3 : num_elts_below A m t
h4 : m ∉ A
⊢ s < t
Theorem: HTPI.neb_increase
Proof state before:
case neg
A : Set ℕ
n s : ℕ
h1 : enum A s n
m : ℕ
h2 : m ≥ n + 1
ih : ∀ ⦃t : ℕ⦄, num_elts_below A m t → s < t
t : ℕ
h3 : num_elts_below A m t
h4 : m ∉ A
⊢ s < t
Tactic:
show s < t from ih h3
Proof state after:
no goals
Theorem: HTPI.enum_not_skip
Proof state before:
A : Set ℕ
⊢ ∀ ⦃m s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
Tactic:
by_induc
Proof state after:
case Base_Case
A : Set ℕ
⊢ ∀ ⦃s : ℕ⦄, num_elts_below A 0 s → ∀ t < s, ∃ n, enum A t n

case Induction_Step
A : Set ℕ
⊢ ∀ (m : ℕ),
    (∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n) →
      ∀ ⦃s : ℕ⦄, num_elts_below A (m + 1) s → ∀ t < s, ∃ n, enum A t n
Theorem: HTPI.enum_not_skip
Proof state before:
case Base_Case
A : Set ℕ
⊢ ∀ ⦃s : ℕ⦄, num_elts_below A 0 s → ∀ t < s, ∃ n, enum A t n
Tactic:
fix s : Nat
Proof state after:
case Base_Case
A : Set ℕ
s : ℕ
⊢ num_elts_below A 0 s → ∀ t < s, ∃ n, enum A t n
Theorem: HTPI.enum_not_skip
Proof state before:
case Base_Case
A : Set ℕ
s : ℕ
⊢ num_elts_below A 0 s → ∀ t < s, ∃ n, enum A t n
Tactic:
assume h1 : num_elts_below A 0 s
Proof state after:
case Base_Case
A : Set ℕ
s : ℕ
h1 : num_elts_below A 0 s
⊢ ∀ t < s, ∃ n, enum A t n
Theorem: HTPI.enum_not_skip
Proof state before:
case Base_Case
A : Set ℕ
s : ℕ
h1 : num_elts_below A 0 s
⊢ ∀ t < s, ∃ n, enum A t n
Tactic:
define at h1
Proof state after:
case Base_Case
A : Set ℕ
s : ℕ
h1 : s = 0
⊢ ∀ t < s, ∃ n, enum A t n
Theorem: HTPI.enum_not_skip
Proof state before:
case Base_Case
A : Set ℕ
s : ℕ
h1 : s = 0
⊢ ∀ t < s, ∃ n, enum A t n
Tactic:
fix t : Nat
Proof state after:
case Base_Case
A : Set ℕ
s : ℕ
h1 : s = 0
t : ℕ
⊢ t < s → ∃ n, enum A t n
Theorem: HTPI.enum_not_skip
Proof state before:
case Base_Case
A : Set ℕ
s : ℕ
h1 : s = 0
t : ℕ
⊢ t < s → ∃ n, enum A t n
Tactic:
contrapos
Proof state after:
case Base_Case
A : Set ℕ
s : ℕ
h1 : s = 0
t : ℕ
⊢ (¬∃ n, enum A t n) → ¬t < s
Theorem: HTPI.enum_not_skip
Proof state before:
case Base_Case
A : Set ℕ
s : ℕ
h1 : s = 0
t : ℕ
⊢ (¬∃ n, enum A t n) → ¬t < s
Tactic:
assume h2 : ¬∃ (n : Nat), enum A t n
Proof state after:
case Base_Case
A : Set ℕ
s : ℕ
h1 : s = 0
t : ℕ
h2 : ¬∃ n, enum A t n
⊢ ¬t < s
Theorem: HTPI.enum_not_skip
Proof state before:
case Base_Case
A : Set ℕ
s : ℕ
h1 : s = 0
t : ℕ
h2 : ¬∃ n, enum A t n
⊢ ¬t < s
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.enum_not_skip
Proof state before:
case Induction_Step
A : Set ℕ
⊢ ∀ (m : ℕ),
    (∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n) →
      ∀ ⦃s : ℕ⦄, num_elts_below A (m + 1) s → ∀ t < s, ∃ n, enum A t n
Tactic:
fix m : Nat
Proof state after:
case Induction_Step
A : Set ℕ
m : ℕ
⊢ (∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n) →
    ∀ ⦃s : ℕ⦄, num_elts_below A (m + 1) s → ∀ t < s, ∃ n, enum A t n
Theorem: HTPI.enum_not_skip
Proof state before:
case Induction_Step
A : Set ℕ
m : ℕ
⊢ (∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n) →
    ∀ ⦃s : ℕ⦄, num_elts_below A (m + 1) s → ∀ t < s, ∃ n, enum A t n
Tactic:
assume ih : ∀ ⦃s : Nat⦄, num_elts_below A m s → ∀ t < s, ∃ (n : Nat), enum A t n
Proof state after:
case Induction_Step
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
⊢ ∀ ⦃s : ℕ⦄, num_elts_below A (m + 1) s → ∀ t < s, ∃ n, enum A t n
Theorem: HTPI.enum_not_skip
Proof state before:
case Induction_Step
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
⊢ ∀ ⦃s : ℕ⦄, num_elts_below A (m + 1) s → ∀ t < s, ∃ n, enum A t n
Tactic:
fix s : Nat
Proof state after:
case Induction_Step
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
⊢ num_elts_below A (m + 1) s → ∀ t < s, ∃ n, enum A t n
Theorem: HTPI.enum_not_skip
Proof state before:
case Induction_Step
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
⊢ num_elts_below A (m + 1) s → ∀ t < s, ∃ n, enum A t n
Tactic:
assume h1 : num_elts_below A (m + 1) s
Proof state after:
case Induction_Step
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : num_elts_below A (m + 1) s
⊢ ∀ t < s, ∃ n, enum A t n
Theorem: HTPI.enum_not_skip
Proof state before:
case Induction_Step
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : num_elts_below A (m + 1) s
⊢ ∀ t < s, ∃ n, enum A t n
Tactic:
by_cases h2 : m ∈ A
Proof state after:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : num_elts_below A (m + 1) s
h2 : m ∈ A
⊢ ∀ t < s, ∃ n, enum A t n

case neg
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : num_elts_below A (m + 1) s
h2 : m ∉ A
⊢ ∀ t < s, ∃ n, enum A t n
Theorem: HTPI.enum_not_skip
Proof state before:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : num_elts_below A (m + 1) s
h2 : m ∈ A
⊢ ∀ t < s, ∃ n, enum A t n
Tactic:
rewrite [neb_step_elt h2] at h1
Proof state after:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
⊢ ∀ t < s, ∃ n, enum A t n
Theorem: HTPI.enum_not_skip
Proof state before:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
⊢ ∀ t < s, ∃ n, enum A t n
Tactic:
have h3 : ∀ t < s - 1, ∃ (n : Nat), enum A t n := ih h1.right
Proof state after:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
⊢ ∀ t < s, ∃ n, enum A t n
Theorem: HTPI.enum_not_skip
Proof state before:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
⊢ ∀ t < s, ∃ n, enum A t n
Tactic:
fix t : Nat
Proof state after:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
⊢ t < s → ∃ n, enum A t n
Theorem: HTPI.enum_not_skip
Proof state before:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
⊢ t < s → ∃ n, enum A t n
Tactic:
assume h4 : t < s
Proof state after:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
⊢ ∃ n, enum A t n
Theorem: HTPI.enum_not_skip
Proof state before:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
⊢ ∃ n, enum A t n
Tactic:
by_cases h5 : t = s - 1
Proof state after:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : t = s - 1
⊢ ∃ n, enum A t n

case neg
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : ¬t = s - 1
⊢ ∃ n, enum A t n
Theorem: HTPI.enum_not_skip
Proof state before:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : t = s - 1
⊢ ∃ n, enum A t n
Tactic:
apply Exists.intro m
Proof state after:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : t = s - 1
⊢ enum A t m
Theorem: HTPI.enum_not_skip
Proof state before:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : t = s - 1
⊢ enum A t m
Tactic:
define
Proof state after:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : t = s - 1
⊢ m ∈ A ∧ num_elts_below A m t
Theorem: HTPI.enum_not_skip
Proof state before:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : t = s - 1
⊢ m ∈ A ∧ num_elts_below A m t
Tactic:
apply And.intro h2
Proof state after:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : t = s - 1
⊢ num_elts_below A m t
Theorem: HTPI.enum_not_skip
Proof state before:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : t = s - 1
⊢ num_elts_below A m t
Tactic:
rewrite [h5]
Proof state after:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : t = s - 1
⊢ num_elts_below A m (s - 1)
Theorem: HTPI.enum_not_skip
Proof state before:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : t = s - 1
⊢ num_elts_below A m (s - 1)
Tactic:
show num_elts_below A m (s - 1) from h1.right
Proof state after:
no goals
Theorem: HTPI.enum_not_skip
Proof state before:
case neg
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : ¬t = s - 1
⊢ ∃ n, enum A t n
Tactic:
have h6 : t ≤ s - 1 := Nat.le_pred_of_lt h4
Proof state after:
case neg
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : ¬t = s - 1
h6 : t ≤ s - 1
⊢ ∃ n, enum A t n
Theorem: HTPI.enum_not_skip
Proof state before:
case neg
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : ¬t = s - 1
h6 : t ≤ s - 1
⊢ ∃ n, enum A t n
Tactic:
have h7 : t < s - 1 := Nat.lt_of_le_of_ne h6 h5
Proof state after:
case neg
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : ¬t = s - 1
h6 : t ≤ s - 1
h7 : t < s - 1
⊢ ∃ n, enum A t n
Theorem: HTPI.enum_not_skip
Proof state before:
case neg
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : ¬t = s - 1
h6 : t ≤ s - 1
h7 : t < s - 1
⊢ ∃ n, enum A t n
Tactic:
show ∃ (n : Nat), enum A t n from ih h1.right t h7
Proof state after:
no goals
Theorem: HTPI.enum_not_skip
Proof state before:
case neg
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : num_elts_below A (m + 1) s
h2 : m ∉ A
⊢ ∀ t < s, ∃ n, enum A t n
Tactic:
rewrite [neb_step_not_elt h2] at h1
Proof state after:
case neg
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : num_elts_below A m s
h2 : m ∉ A
⊢ ∀ t < s, ∃ n, enum A t n
Theorem: HTPI.enum_not_skip
Proof state before:
case neg
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : num_elts_below A m s
h2 : m ∉ A
⊢ ∀ t < s, ∃ n, enum A t n
Tactic:
show ∀ t < s, ∃ (n : Nat), enum A t n from ih h1
Proof state after:
no goals
Theorem: HTPI.enum_le
Proof state before:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
h2 : enum A t n2
⊢ n1 ≤ n2
Tactic:
by_contra h3
Proof state after:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
h2 : enum A t n2
h3 : ¬n1 ≤ n2
⊢ False
Theorem: HTPI.enum_le
Proof state before:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
h2 : enum A t n2
h3 : ¬n1 ≤ n2
⊢ False
Tactic:
have h4 : n2 + 1 ≤ n1 := by linarith
Proof state after:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
h2 : enum A t n2
h3 : ¬n1 ≤ n2
h4 : n2 + 1 ≤ n1
⊢ False
Theorem: HTPI.enum_le
Proof state before:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
h2 : enum A t n2
h3 : ¬n1 ≤ n2
h4 : n2 + 1 ≤ n1
⊢ False
Tactic:
define at h1
Proof state after:
A : Set ℕ
t n1 n2 : ℕ
h1 : n1 ∈ A ∧ num_elts_below A n1 t
h2 : enum A t n2
h3 : ¬n1 ≤ n2
h4 : n2 + 1 ≤ n1
⊢ False
Theorem: HTPI.enum_le
Proof state before:
A : Set ℕ
t n1 n2 : ℕ
h1 : n1 ∈ A ∧ num_elts_below A n1 t
h2 : enum A t n2
h3 : ¬n1 ≤ n2
h4 : n2 + 1 ≤ n1
⊢ False
Tactic:
have h5 : t < t := neb_increase h2 h4 h1.right
Proof state after:
A : Set ℕ
t n1 n2 : ℕ
h1 : n1 ∈ A ∧ num_elts_below A n1 t
h2 : enum A t n2
h3 : ¬n1 ≤ n2
h4 : n2 + 1 ≤ n1
h5 : t < t
⊢ False
Theorem: HTPI.enum_le
Proof state before:
A : Set ℕ
t n1 n2 : ℕ
h1 : n1 ∈ A ∧ num_elts_below A n1 t
h2 : enum A t n2
h3 : ¬n1 ≤ n2
h4 : n2 + 1 ≤ n1
h5 : t < t
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.enum_le
Proof state before:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
h2 : enum A t n2
h3 : ¬n1 ≤ n2
⊢ n2 + 1 ≤ n1
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.enum_unique
Proof state before:
A : Set ℕ
t : ℕ
⊢ ∀ ⦃n1 n2 : ℕ⦄, enum A t n1 → enum A t n2 → n1 = n2
Tactic:
fix n1 : Nat
Proof state after:
A : Set ℕ
t n1 : ℕ
⊢ ∀ ⦃n2 : ℕ⦄, enum A t n1 → enum A t n2 → n1 = n2
Theorem: HTPI.enum_unique
Proof state before:
A : Set ℕ
t n1 : ℕ
⊢ ∀ ⦃n2 : ℕ⦄, enum A t n1 → enum A t n2 → n1 = n2
Tactic:
fix n2 : Nat
Proof state after:
A : Set ℕ
t n1 n2 : ℕ
⊢ enum A t n1 → enum A t n2 → n1 = n2
Theorem: HTPI.enum_unique
Proof state before:
A : Set ℕ
t n1 n2 : ℕ
⊢ enum A t n1 → enum A t n2 → n1 = n2
Tactic:
assume h1 : enum A t n1
Proof state after:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
⊢ enum A t n2 → n1 = n2
Theorem: HTPI.enum_unique
Proof state before:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
⊢ enum A t n2 → n1 = n2
Tactic:
assume h2 : enum A t n2
Proof state after:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
h2 : enum A t n2
⊢ n1 = n2
Theorem: HTPI.enum_unique
Proof state before:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
h2 : enum A t n2
⊢ n1 = n2
Tactic:
have h3 : n1 ≤ n2 := enum_le h1 h2
Proof state after:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
h2 : enum A t n2
h3 : n1 ≤ n2
⊢ n1 = n2
Theorem: HTPI.enum_unique
Proof state before:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
h2 : enum A t n2
h3 : n1 ≤ n2
⊢ n1 = n2
Tactic:
have h4 : n2 ≤ n1 := enum_le h2 h1
Proof state after:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
h2 : enum A t n2
h3 : n1 ≤ n2
h4 : n2 ≤ n1
⊢ n1 = n2
Theorem: HTPI.enum_unique
Proof state before:
A : Set ℕ
t n1 n2 : ℕ
h1 : enum A t n1
h2 : enum A t n2
h3 : n1 ≤ n2
h4 : n2 ≤ n1
⊢ n1 = n2
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.inv_enum_fcnl
Proof state before:
A : Set ℕ
⊢ fcnl_on (invRel (enum A)) A
Tactic:
define
Proof state after:
A : Set ℕ
⊢ ∀ ⦃x : ℕ⦄, x ∈ A → ∃! y, invRel (enum A) x y
Theorem: HTPI.inv_enum_fcnl
Proof state before:
A : Set ℕ
⊢ ∀ ⦃x : ℕ⦄, x ∈ A → ∃! y, invRel (enum A) x y
Tactic:
fix n : Nat
Proof state after:
A : Set ℕ
n : ℕ
⊢ n ∈ A → ∃! y, invRel (enum A) n y
Theorem: HTPI.inv_enum_fcnl
Proof state before:
A : Set ℕ
n : ℕ
⊢ n ∈ A → ∃! y, invRel (enum A) n y
Tactic:
assume h1 : n ∈ A
Proof state after:
A : Set ℕ
n : ℕ
h1 : n ∈ A
⊢ ∃! y, invRel (enum A) n y
Theorem: HTPI.inv_enum_fcnl
Proof state before:
A : Set ℕ
n : ℕ
h1 : n ∈ A
⊢ ∃! y, invRel (enum A) n y
Tactic:
exists_unique
Proof state after:
case Existence
A : Set ℕ
n : ℕ
h1 : n ∈ A
⊢ ∃ y, invRel (enum A) n y

case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
⊢ ∀ (y_1 y_2 : ℕ), invRel (enum A) n y_1 → invRel (enum A) n y_2 → y_1 = y_2
Theorem: HTPI.inv_enum_fcnl
Proof state before:
case Existence
A : Set ℕ
n : ℕ
h1 : n ∈ A
⊢ ∃ y, invRel (enum A) n y
Tactic:
obtain (s : Nat) (h2 : num_elts_below A n s) from neb_exists A n
Proof state after:
case Existence
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
h2 : num_elts_below A n s
⊢ ∃ y, invRel (enum A) n y
Theorem: HTPI.inv_enum_fcnl
Proof state before:
case Existence
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
h2 : num_elts_below A n s
⊢ ∃ y, invRel (enum A) n y
Tactic:
apply Exists.intro s
Proof state after:
case Existence
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
h2 : num_elts_below A n s
⊢ invRel (enum A) n s
Theorem: HTPI.inv_enum_fcnl
Proof state before:
case Existence
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
h2 : num_elts_below A n s
⊢ invRel (enum A) n s
Tactic:
define
Proof state after:
case Existence
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
h2 : num_elts_below A n s
⊢ n ∈ A ∧ num_elts_below A n s
Theorem: HTPI.inv_enum_fcnl
Proof state before:
case Existence
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
h2 : num_elts_below A n s
⊢ n ∈ A ∧ num_elts_below A n s
Tactic:
show n ∈ A ∧ num_elts_below A n s from And.intro h1 h2
Proof state after:
no goals
Theorem: HTPI.inv_enum_fcnl
Proof state before:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
⊢ ∀ (y_1 y_2 : ℕ), invRel (enum A) n y_1 → invRel (enum A) n y_2 → y_1 = y_2
Tactic:
fix s1 : Nat
Proof state after:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
s1 : ℕ
⊢ ∀ (y_2 : ℕ), invRel (enum A) n s1 → invRel (enum A) n y_2 → s1 = y_2
Theorem: HTPI.inv_enum_fcnl
Proof state before:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
s1 : ℕ
⊢ ∀ (y_2 : ℕ), invRel (enum A) n s1 → invRel (enum A) n y_2 → s1 = y_2
Tactic:
fix s2 : Nat
Proof state after:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
s1 s2 : ℕ
⊢ invRel (enum A) n s1 → invRel (enum A) n s2 → s1 = s2
Theorem: HTPI.inv_enum_fcnl
Proof state before:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
s1 s2 : ℕ
⊢ invRel (enum A) n s1 → invRel (enum A) n s2 → s1 = s2
Tactic:
assume h2 : invRel (enum A) n s1
Proof state after:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
s1 s2 : ℕ
h2 : invRel (enum A) n s1
⊢ invRel (enum A) n s2 → s1 = s2
Theorem: HTPI.inv_enum_fcnl
Proof state before:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
s1 s2 : ℕ
h2 : invRel (enum A) n s1
⊢ invRel (enum A) n s2 → s1 = s2
Tactic:
assume h3 : invRel (enum A) n s2
Proof state after:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
s1 s2 : ℕ
h2 : invRel (enum A) n s1
h3 : invRel (enum A) n s2
⊢ s1 = s2
Theorem: HTPI.inv_enum_fcnl
Proof state before:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
s1 s2 : ℕ
h2 : invRel (enum A) n s1
h3 : invRel (enum A) n s2
⊢ s1 = s2
Tactic:
define at h2
Proof state after:
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