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

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

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

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

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

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

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

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

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