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

State before:
A : Set ℕ
⊢ ∀ (n : ℕ), ∃ s, num_elts_below A n s
Tactic:
by_induc
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

State before:
case Base_Case
A : Set ℕ
⊢ ∃ s, num_elts_below A 0 s
Tactic:
apply Exists.intro 0
State after:
case Base_Case
A : Set ℕ
⊢ num_elts_below A 0 0

State before:
case Base_Case
A : Set ℕ
⊢ num_elts_below A 0 0
Tactic:
define
State after:
case Base_Case
A : Set ℕ
⊢ 0 = 0

State before:
case Base_Case
A : Set ℕ
⊢ 0 = 0
Tactic:
rfl
State after:
no goals

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
State after:
case Induction_Step
A : Set ℕ
n : ℕ
⊢ (∃ s, num_elts_below A n s) → ∃ s, num_elts_below A (n + 1) s

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
State after:
case Induction_Step
A : Set ℕ
n : ℕ
ih : ∃ s, num_elts_below A n s
⊢ ∃ s, num_elts_below A (n + 1) s

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

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

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

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

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

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

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

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

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