internlm/Lean-Github huggingface dataset:
Theorem: HTPI.equinum_Univ
Proof state before:
case h.mpr
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
h3 : v ∈ Univ V
u : U
h4 : f u = v
⊢ v ∈ image f (Univ U)
Tactic:
apply Exists.intro u
Proof state after:
case h.mpr
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
h3 : v ∈ Univ V
u : U
h4 : f u = v
⊢ u ∈ Univ U ∧ f u = v
Theorem: HTPI.equinum_Univ
Proof state before:
case h.mpr
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
h3 : v ∈ Univ V
u : U
h4 : f u = v
⊢ u ∈ Univ U ∧ f u = v
Tactic:
apply And.intro _ h4
Proof state after:
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
h3 : v ∈ Univ V
u : U
h4 : f u = v
⊢ u ∈ Univ U
Theorem: HTPI.equinum_Univ
Proof state before:
U V : Type
f : U → V
h1 : one_to_one f
h2 : onto f
v : V
h3 : v ∈ Univ V
u : U
h4 : f u = v
⊢ u ∈ Univ U
Tactic:
show u ∈ Univ U from elt_Univ u
Proof state after:
no goals
Theorem: HTPI.neb_step
Proof state before:
A : Set ℕ
n s : ℕ
⊢ num_elts_below A (n + 1) s ↔ n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) ∨ n ∉ A ∧ num_elts_below A n s
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.neb_step_elt
Proof state before:
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
⊢ num_elts_below A (n + 1) s ↔ 1 ≤ s ∧ num_elts_below A n (s - 1)
Tactic:
rewrite [neb_step]
Proof state after:
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
⊢ n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) ∨ n ∉ A ∧ num_elts_below A n s ↔ 1 ≤ s ∧ num_elts_below A n (s - 1)
Theorem: HTPI.neb_step_elt
Proof state before:
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
⊢ n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) ∨ n ∉ A ∧ num_elts_below A n s ↔ 1 ≤ s ∧ num_elts_below A n (s - 1)
Tactic:
apply Iff.intro
Proof state after:
case mp
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
⊢ n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) ∨ n ∉ A ∧ num_elts_below A n s → 1 ≤ s ∧ num_elts_below A n (s - 1)

case mpr
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
⊢ 1 ≤ s ∧ num_elts_below A n (s - 1) → n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) ∨ n ∉ A ∧ num_elts_below A n s
Theorem: HTPI.neb_step_elt
Proof state before:
case mp
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
⊢ n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) ∨ n ∉ A ∧ num_elts_below A n s → 1 ≤ s ∧ num_elts_below A n (s - 1)
Tactic:
assume h2 : n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) ∨
  ¬n ∈ A ∧ num_elts_below A n s
Proof state after:
case mp
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
h2 : n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) ∨ n ∉ A ∧ num_elts_below A n s
⊢ 1 ≤ s ∧ num_elts_below A n (s - 1)
Theorem: HTPI.neb_step_elt
Proof state before:
case mp
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
h2 : n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) ∨ n ∉ A ∧ num_elts_below A n s
⊢ 1 ≤ s ∧ num_elts_below A n (s - 1)
Tactic:
by_cases on h2
Proof state after:
case mp.Case_1
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
h2 : n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1)
⊢ 1 ≤ s ∧ num_elts_below A n (s - 1)

case mp.Case_2
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
h2 : n ∉ A ∧ num_elts_below A n s
⊢ 1 ≤ s ∧ num_elts_below A n (s - 1)
Theorem: HTPI.neb_step_elt
Proof state before:
case mp.Case_1
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
h2 : n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1)
⊢ 1 ≤ s ∧ num_elts_below A n (s - 1)
Tactic:
show 1 ≤ s ∧ num_elts_below A n (s - 1) from h2.right
Proof state after:
no goals
Theorem: HTPI.neb_step_elt
Proof state before:
case mp.Case_2
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
h2 : n ∉ A ∧ num_elts_below A n s
⊢ 1 ≤ s ∧ num_elts_below A n (s - 1)
Tactic:
show 1 ≤ s ∧ num_elts_below A n (s - 1) from absurd h1 h2.left
Proof state after:
no goals
Theorem: HTPI.neb_step_elt
Proof state before:
case mpr
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
⊢ 1 ≤ s ∧ num_elts_below A n (s - 1) → n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) ∨ n ∉ A ∧ num_elts_below A n s
Tactic:
assume h2 : 1 ≤ s ∧ num_elts_below A n (s - 1)
Proof state after:
case mpr
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
h2 : 1 ≤ s ∧ num_elts_below A n (s - 1)
⊢ n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) ∨ n ∉ A ∧ num_elts_below A n s
Theorem: HTPI.neb_step_elt
Proof state before:
case mpr
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
h2 : 1 ≤ s ∧ num_elts_below A n (s - 1)
⊢ n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) ∨ n ∉ A ∧ num_elts_below A n s
Tactic:
apply Or.inl
Proof state after:
case mpr.h
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
h2 : 1 ≤ s ∧ num_elts_below A n (s - 1)
⊢ n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1)
Theorem: HTPI.neb_step_elt
Proof state before:
case mpr.h
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
h2 : 1 ≤ s ∧ num_elts_below A n (s - 1)
⊢ n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1)
Tactic:
show n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) from And.intro h1 h2
Proof state after:
no goals
Theorem: HTPI.neb_step_not_elt
Proof state before:
A : Set ℕ
n : ℕ
h1 : n ∉ A
s : ℕ
⊢ num_elts_below A (n + 1) s ↔ num_elts_below A n s
Tactic:
rewrite [neb_step]
Proof state after:
A : Set ℕ
n : ℕ
h1 : n ∉ A
s : ℕ
⊢ n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) ∨ n ∉ A ∧ num_elts_below A n s ↔ num_elts_below A n s
Theorem: HTPI.neb_step_not_elt
Proof state before:
A : Set ℕ
n : ℕ
h1 : n ∉ A
s : ℕ
⊢ n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) ∨ n ∉ A ∧ num_elts_below A n s ↔ num_elts_below A n s
Tactic:
apply Iff.intro
Proof state after:
case mp
A : Set ℕ
n : ℕ
h1 : n ∉ A
s : ℕ
⊢ n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) ∨ n ∉ A ∧ num_elts_below A n s → num_elts_below A n s

case mpr
A : Set ℕ
n : ℕ
h1 : n ∉ A
s : ℕ
⊢ num_elts_below A n s → n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) ∨ n ∉ A ∧ num_elts_below A n s
Theorem: HTPI.neb_step_not_elt
Proof state before:
case mp
A : Set ℕ
n : ℕ
h1 : n ∉ A
s : ℕ
⊢ n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) ∨ n ∉ A ∧ num_elts_below A n s → num_elts_below A n s
Tactic:
assume h2 : n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) ∨
  ¬n ∈ A ∧ num_elts_below A n s
Proof state after:
case mp
A : Set ℕ
n : ℕ
h1 : n ∉ A
s : ℕ
h2 : n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) ∨ n ∉ A ∧ num_elts_below A n s
⊢ num_elts_below A n s
Theorem: HTPI.neb_step_not_elt
Proof state before:
case mp
A : Set ℕ
n : ℕ
h1 : n ∉ A
s : ℕ
h2 : n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) ∨ n ∉ A ∧ num_elts_below A n s
⊢ num_elts_below A n s
Tactic:
by_cases on h2
Proof state after:
case mp.Case_1
A : Set ℕ
n : ℕ
h1 : n ∉ A
s : ℕ
h2 : n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1)
⊢ num_elts_below A n s

case mp.Case_2
A : Set ℕ
n : ℕ
h1 : n ∉ A
s : ℕ
h2 : n ∉ A ∧ num_elts_below A n s
⊢ num_elts_below A n s
Theorem: HTPI.neb_step_not_elt
Proof state before:
case mp.Case_1
A : Set ℕ
n : ℕ
h1 : n ∉ A
s : ℕ
h2 : n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1)
⊢ num_elts_below A n s
Tactic:
show num_elts_below A n s from absurd h2.left h1
Proof state after:
no goals
Theorem: HTPI.neb_step_not_elt
Proof state before:
case mp.Case_2
A : Set ℕ
n : ℕ
h1 : n ∉ A
s : ℕ
h2 : n ∉ A ∧ num_elts_below A n s
⊢ num_elts_below A n s
Tactic:
show num_elts_below A n s from h2.right
Proof state after:
no goals
Theorem: HTPI.neb_step_not_elt
Proof state before:
case mpr
A : Set ℕ
n : ℕ
h1 : n ∉ A
s : ℕ
⊢ num_elts_below A n s → n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) ∨ n ∉ A ∧ num_elts_below A n s
Tactic:
assume h2 : num_elts_below A n s
Proof state after:
case mpr
A : Set ℕ
n : ℕ
h1 : n ∉ A
s : ℕ
h2 : num_elts_below A n s
⊢ n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) ∨ n ∉ A ∧ num_elts_below A n s
Theorem: HTPI.neb_step_not_elt
Proof state before:
case mpr
A : Set ℕ
n : ℕ
h1 : n ∉ A
s : ℕ
h2 : num_elts_below A n s
⊢ n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) ∨ n ∉ A ∧ num_elts_below A n s
Tactic:
apply Or.inr
Proof state after:
case mpr.h
A : Set ℕ
n : ℕ
h1 : n ∉ A
s : ℕ
h2 : num_elts_below A n s
⊢ n ∉ A ∧ num_elts_below A n s
Theorem: HTPI.neb_step_not_elt
Proof state before:
case mpr.h
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.neb_exists
Proof state before:
A : Set ℕ
⊢ ∀ (n : ℕ), ∃ s, num_elts_below A n s
Tactic:
by_induc
Proof state after:
case Base_Case
A : Set ℕ
⊢ ∃ s, num_elts_below A 0 s

case Induction_Step
A : Set ℕ
⊢ ∀ (n : ℕ), (∃ s, num_elts_below A n s) → ∃ s, num_elts_below A (n + 1) s
Theorem: HTPI.neb_exists
Proof state before:
case Base_Case
A : Set ℕ
⊢ ∃ s, num_elts_below A 0 s
Tactic:
apply Exists.intro 0
Proof state after:
case Base_Case
A : Set ℕ
⊢ num_elts_below A 0 0
Theorem: HTPI.neb_exists
Proof state before:
case Base_Case
A : Set ℕ
⊢ num_elts_below A 0 0
Tactic:
define
Proof state after:
case Base_Case
A : Set ℕ
⊢ 0 = 0
Theorem: HTPI.neb_exists
Proof state before:
case Base_Case
A : Set ℕ
⊢ 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.neb_exists
Proof state before:
case Induction_Step
A : Set ℕ
⊢ ∀ (n : ℕ), (∃ s, num_elts_below A n s) → ∃ s, num_elts_below A (n + 1) s
Tactic:
fix n : Nat
Proof state after:
case Induction_Step
A : Set ℕ
n : ℕ
⊢ (∃ s, num_elts_below A n s) → ∃ s, num_elts_below A (n + 1) s
Theorem: HTPI.neb_exists
Proof state before:
case Induction_Step
A : Set ℕ
n : ℕ
⊢ (∃ s, num_elts_below A n s) → ∃ s, num_elts_below A (n + 1) s
Tactic:
assume ih : ∃ (s : Nat), num_elts_below A n s
Proof state after:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∃ s, num_elts_below A n s
⊢ ∃ s, num_elts_below A (n + 1) s
Theorem: HTPI.neb_exists
Proof state before:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∃ s, num_elts_below A n s
⊢ ∃ s, num_elts_below A (n + 1) s
Tactic:
obtain (t : Nat) (h1 : num_elts_below A n t) from ih
Proof state after:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∃ s, num_elts_below A n s
t : ℕ
h1 : num_elts_below A n t
⊢ ∃ s, num_elts_below A (n + 1) s
Theorem: HTPI.neb_exists
Proof state before:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∃ s, num_elts_below A n s
t : ℕ
h1 : num_elts_below A n t
⊢ ∃ s, num_elts_below A (n + 1) s
Tactic:
by_cases h2 : n ∈ A
Proof state after:
case pos
A : Set ℕ
n : ℕ
ih : ∃ s, num_elts_below A n s
t : ℕ
h1 : num_elts_below A n t
h2 : n ∈ A
⊢ ∃ s, num_elts_below A (n + 1) s

case neg
A : Set ℕ
n : ℕ
ih : ∃ s, num_elts_below A n s
t : ℕ
h1 : num_elts_below A n t
h2 : n ∉ A
⊢ ∃ s, num_elts_below A (n + 1) s
Theorem: HTPI.neb_exists
Proof state before:
case pos
A : Set ℕ
n : ℕ
ih : ∃ s, num_elts_below A n s
t : ℕ
h1 : num_elts_below A n t
h2 : n ∈ A
⊢ ∃ s, num_elts_below A (n + 1) s
Tactic:
apply Exists.intro (t + 1)
Proof state after:
case pos
A : Set ℕ
n : ℕ
ih : ∃ s, num_elts_below A n s
t : ℕ
h1 : num_elts_below A n t
h2 : n ∈ A
⊢ num_elts_below A (n + 1) (t + 1)
Theorem: HTPI.neb_exists
Proof state before:
case pos
A : Set ℕ
n : ℕ
ih : ∃ s, num_elts_below A n s
t : ℕ
h1 : num_elts_below A n t
h2 : n ∈ A
⊢ num_elts_below A (n + 1) (t + 1)
Tactic:
rewrite [neb_step_elt h2, Nat.add_sub_cancel]
Proof state after:
case pos
A : Set ℕ
n : ℕ
ih : ∃ s, num_elts_below A n s
t : ℕ
h1 : num_elts_below A n t
h2 : n ∈ A
⊢ 1 ≤ t + 1 ∧ num_elts_below A n t
Theorem: HTPI.neb_exists
Proof state before:
case pos
A : Set ℕ
n : ℕ
ih : ∃ s, num_elts_below A n s
t : ℕ
h1 : num_elts_below A n t
h2 : n ∈ A
⊢ 1 ≤ t + 1 ∧ num_elts_below A n t
Tactic:
apply And.intro _ h1
Proof state after:
A : Set ℕ
n : ℕ
ih : ∃ s, num_elts_below A n s
t : ℕ
h1 : num_elts_below A n t
h2 : n ∈ A
⊢ 1 ≤ t + 1
Theorem: HTPI.neb_exists
Proof state before:
A : Set ℕ
n : ℕ
ih : ∃ s, num_elts_below A n s
t : ℕ
h1 : num_elts_below A n t
h2 : n ∈ A
⊢ 1 ≤ t + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.neb_exists
Proof state before:
case neg
A : Set ℕ
n : ℕ
ih : ∃ s, num_elts_below A n s
t : ℕ
h1 : num_elts_below A n t
h2 : n ∉ A
⊢ ∃ s, num_elts_below A (n + 1) s
Tactic:
apply Exists.intro t
Proof state after:
case neg
A : Set ℕ
n : ℕ
ih : ∃ s, num_elts_below A n s
t : ℕ
h1 : num_elts_below A n t
h2 : n ∉ A
⊢ num_elts_below A (n + 1) t
Theorem: HTPI.neb_exists
Proof state before:
case neg
A : Set ℕ
n : ℕ
ih : ∃ s, num_elts_below A n s
t : ℕ
h1 : num_elts_below A n t
h2 : n ∉ A
⊢ num_elts_below A (n + 1) t
Tactic:
rewrite [neb_step_not_elt h2]
Proof state after:
case neg
A : Set ℕ
n : ℕ
ih : ∃ s, num_elts_below A n s
t : ℕ
h1 : num_elts_below A n t
h2 : n ∉ A
⊢ num_elts_below A n t
Theorem: HTPI.neb_exists
Proof state before:
case neg
A : Set ℕ
n : ℕ
ih : ∃ s, num_elts_below A n s
t : ℕ
h1 : num_elts_below A n t
h2 : n ∉ A
⊢ num_elts_below A n t
Tactic:
show num_elts_below A n t from h1
Proof state after:
no goals
Theorem: HTPI.neb_unique
Proof state before:
A : Set ℕ
⊢ ∀ ⦃n s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
Tactic:
by_induc
Proof state after:
case Base_Case
A : Set ℕ
⊢ ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A 0 s1 → num_elts_below A 0 s2 → s1 = s2

case Induction_Step
A : Set ℕ
⊢ ∀ (n : ℕ),
    (∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2) →
      ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A (n + 1) s1 → num_elts_below A (n + 1) s2 → s1 = s2
Theorem: HTPI.neb_unique
Proof state before:
case Base_Case
A : Set ℕ
⊢ ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A 0 s1 → num_elts_below A 0 s2 → s1 = s2
Tactic:
fix s1 : Nat
Proof state after:
case Base_Case
A : Set ℕ
s1 : ℕ
⊢ ∀ ⦃s2 : ℕ⦄, num_elts_below A 0 s1 → num_elts_below A 0 s2 → s1 = s2
Theorem: HTPI.neb_unique
Proof state before:
case Base_Case
A : Set ℕ
s1 : ℕ
⊢ ∀ ⦃s2 : ℕ⦄, num_elts_below A 0 s1 → num_elts_below A 0 s2 → s1 = s2
Tactic:
fix s2 : Nat
Proof state after:
case Base_Case
A : Set ℕ
s1 s2 : ℕ
⊢ num_elts_below A 0 s1 → num_elts_below A 0 s2 → s1 = s2
Theorem: HTPI.neb_unique
Proof state before:
case Base_Case
A : Set ℕ
s1 s2 : ℕ
⊢ num_elts_below A 0 s1 → num_elts_below A 0 s2 → s1 = s2
Tactic:
assume h1 : num_elts_below A 0 s1
Proof state after:
case Base_Case
A : Set ℕ
s1 s2 : ℕ
h1 : num_elts_below A 0 s1
⊢ num_elts_below A 0 s2 → s1 = s2
Theorem: HTPI.neb_unique
Proof state before:
case Base_Case
A : Set ℕ
s1 s2 : ℕ
h1 : num_elts_below A 0 s1
⊢ num_elts_below A 0 s2 → s1 = s2
Tactic:
assume h2 : num_elts_below A 0 s2
Proof state after:
case Base_Case
A : Set ℕ
s1 s2 : ℕ
h1 : num_elts_below A 0 s1
h2 : num_elts_below A 0 s2
⊢ s1 = s2
Theorem: HTPI.neb_unique
Proof state before:
case Base_Case
A : Set ℕ
s1 s2 : ℕ
h1 : num_elts_below A 0 s1
h2 : num_elts_below A 0 s2
⊢ s1 = s2
Tactic:
define at h1
Proof state after:
case Base_Case
A : Set ℕ
s1 s2 : ℕ
h1 : s1 = 0
h2 : num_elts_below A 0 s2
⊢ s1 = s2
Theorem: HTPI.neb_unique
Proof state before:
case Base_Case
A : Set ℕ
s1 s2 : ℕ
h1 : s1 = 0
h2 : num_elts_below A 0 s2
⊢ s1 = s2
Tactic:
define at h2
Proof state after:
case Base_Case
A : Set ℕ
s1 s2 : ℕ
h1 : s1 = 0
h2 : s2 = 0
⊢ s1 = s2
Theorem: HTPI.neb_unique
Proof state before:
case Base_Case
A : Set ℕ
s1 s2 : ℕ
h1 : s1 = 0
h2 : s2 = 0
⊢ s1 = s2
Tactic:
rewrite [h1, h2]
Proof state after:
case Base_Case
A : Set ℕ
s1 s2 : ℕ
h1 : s1 = 0
h2 : s2 = 0
⊢ 0 = 0
Theorem: HTPI.neb_unique
Proof state before:
case Base_Case
A : Set ℕ
s1 s2 : ℕ
h1 : s1 = 0
h2 : s2 = 0
⊢ 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.neb_unique
Proof state before:
case Induction_Step
A : Set ℕ
⊢ ∀ (n : ℕ),
    (∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2) →
      ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A (n + 1) s1 → num_elts_below A (n + 1) s2 → s1 = s2
Tactic:
fix n : Nat
Proof state after:
case Induction_Step
A : Set ℕ
n : ℕ
⊢ (∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2) →
    ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A (n + 1) s1 → num_elts_below A (n + 1) s2 → s1 = s2
Theorem: HTPI.neb_unique
Proof state before:
case Induction_Step
A : Set ℕ
n : ℕ
⊢ (∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2) →
    ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A (n + 1) s1 → num_elts_below A (n + 1) s2 → s1 = s2
Tactic:
assume ih : ∀ ⦃s1 s2 : Nat⦄,
  num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
Proof state after:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
⊢ ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A (n + 1) s1 → num_elts_below A (n + 1) s2 → s1 = s2
Theorem: HTPI.neb_unique
Proof state before:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
⊢ ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A (n + 1) s1 → num_elts_below A (n + 1) s2 → s1 = s2
Tactic:
fix s1 : Nat
Proof state after:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 : ℕ
⊢ ∀ ⦃s2 : ℕ⦄, num_elts_below A (n + 1) s1 → num_elts_below A (n + 1) s2 → s1 = s2
Theorem: HTPI.neb_unique
Proof state before:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 : ℕ
⊢ ∀ ⦃s2 : ℕ⦄, num_elts_below A (n + 1) s1 → num_elts_below A (n + 1) s2 → s1 = s2
Tactic:
fix s2 : Nat
Proof state after:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
⊢ num_elts_below A (n + 1) s1 → num_elts_below A (n + 1) s2 → s1 = s2
Theorem: HTPI.neb_unique
Proof state before:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
⊢ num_elts_below A (n + 1) s1 → num_elts_below A (n + 1) s2 → s1 = s2
Tactic:
assume h1 : num_elts_below A (n + 1) s1
Proof state after:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
h1 : num_elts_below A (n + 1) s1
⊢ num_elts_below A (n + 1) s2 → s1 = s2
Theorem: HTPI.neb_unique
Proof state before:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
h1 : num_elts_below A (n + 1) s1
⊢ num_elts_below A (n + 1) s2 → s1 = s2
Tactic:
assume h2 : num_elts_below A (n + 1) s2
Proof state after:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
h1 : num_elts_below A (n + 1) s1
h2 : num_elts_below A (n + 1) s2
⊢ s1 = s2
Theorem: HTPI.neb_unique
Proof state before:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
h1 : num_elts_below A (n + 1) s1
h2 : num_elts_below A (n + 1) s2
⊢ s1 = s2
Tactic:
by_cases h3 : n ∈ A
Proof state after:
case pos
A : Set ℕ
n : ℕ
ih : ∀ ⦃s1 s2 : ℕ⦄, num_elts_below A n s1 → num_elts_below A n s2 → s1 = s2
s1 s2 : ℕ
h1 : num_elts_below A (n + 1) s1
h2 : num_elts_below A (n + 1) s2
h3 : n ∈ A
⊢ s1 = s2

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

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
Theorem: HTPI.neb_increase
Proof state before:
case Base_Case
A : Set ℕ
n s : ℕ
h1 : enum A s n
⊢ ∀ ⦃t : ℕ⦄, num_elts_below A (n + 1) t → s < t
Tactic:
define at h1
Proof state after:
case Base_Case
A : Set ℕ
n s : ℕ
h1 : n ∈ A ∧ num_elts_below A n s
⊢ ∀ ⦃t : ℕ⦄, num_elts_below A (n + 1) t → s < t
Theorem: HTPI.neb_increase
Proof state before:
case Base_Case
A : Set ℕ
n s : ℕ
h1 : n ∈ A ∧ num_elts_below A n s
⊢ ∀ ⦃t : ℕ⦄, num_elts_below A (n + 1) t → s < t
Tactic:
fix t : Nat
Proof state after:
case Base_Case
A : Set ℕ
n s : ℕ
h1 : n ∈ A ∧ num_elts_below A n s
t : ℕ
⊢ num_elts_below A (n + 1) t → s < t
Theorem: HTPI.neb_increase
Proof state before:
case Base_Case
A : Set ℕ
n s : ℕ
h1 : n ∈ A ∧ num_elts_below A n s
t : ℕ
⊢ num_elts_below A (n + 1) t → s < t
Tactic:
assume h2 : num_elts_below A (n + 1) t
Proof state after:
case Base_Case
A : Set ℕ
n s : ℕ
h1 : n ∈ A ∧ num_elts_below A n s
t : ℕ
h2 : num_elts_below A (n + 1) t
⊢ s < t
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 : num_elts_below A (n + 1) t
⊢ s < t
Tactic:
rewrite [neb_step_elt h1.left] at h2
Proof state after:
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)
⊢ s < t
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)
⊢ s < t
Tactic:
have h3 : s = t - 1 := neb_unique A h1.right h2.right
Proof state after:
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