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

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

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

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

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

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

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

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

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

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