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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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