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

State before:
A : Set ℕ
⊢ ∀ ⦃m s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
Tactic:
by_induc
State after:
case Base_Case
A : Set ℕ
⊢ ∀ ⦃s : ℕ⦄, num_elts_below A 0 s → ∀ t < s, ∃ n, enum A t n

case Induction_Step
A : Set ℕ
⊢ ∀ (m : ℕ),
    (∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n) →
      ∀ ⦃s : ℕ⦄, num_elts_below A (m + 1) s → ∀ t < s, ∃ n, enum A t n

State before:
case Base_Case
A : Set ℕ
⊢ ∀ ⦃s : ℕ⦄, num_elts_below A 0 s → ∀ t < s, ∃ n, enum A t n
Tactic:
fix s : Nat
State after:
case Base_Case
A : Set ℕ
s : ℕ
⊢ num_elts_below A 0 s → ∀ t < s, ∃ n, enum A t n

State before:
case Base_Case
A : Set ℕ
s : ℕ
⊢ num_elts_below A 0 s → ∀ t < s, ∃ n, enum A t n
Tactic:
assume h1 : num_elts_below A 0 s
State after:
case Base_Case
A : Set ℕ
s : ℕ
h1 : num_elts_below A 0 s
⊢ ∀ t < s, ∃ n, enum A t n

State before:
case Base_Case
A : Set ℕ
s : ℕ
h1 : num_elts_below A 0 s
⊢ ∀ t < s, ∃ n, enum A t n
Tactic:
define at h1
State after:
case Base_Case
A : Set ℕ
s : ℕ
h1 : s = 0
⊢ ∀ t < s, ∃ n, enum A t n

State before:
case Base_Case
A : Set ℕ
s : ℕ
h1 : s = 0
⊢ ∀ t < s, ∃ n, enum A t n
Tactic:
fix t : Nat
State after:
case Base_Case
A : Set ℕ
s : ℕ
h1 : s = 0
t : ℕ
⊢ t < s → ∃ n, enum A t n

State before:
case Base_Case
A : Set ℕ
s : ℕ
h1 : s = 0
t : ℕ
⊢ t < s → ∃ n, enum A t n
Tactic:
contrapos
State after:
case Base_Case
A : Set ℕ
s : ℕ
h1 : s = 0
t : ℕ
⊢ (¬∃ n, enum A t n) → ¬t < s

State before:
case Base_Case
A : Set ℕ
s : ℕ
h1 : s = 0
t : ℕ
⊢ (¬∃ n, enum A t n) → ¬t < s
Tactic:
assume h2 : ¬∃ (n : Nat), enum A t n
State after:
case Base_Case
A : Set ℕ
s : ℕ
h1 : s = 0
t : ℕ
h2 : ¬∃ n, enum A t n
⊢ ¬t < s

State before:
case Base_Case
A : Set ℕ
s : ℕ
h1 : s = 0
t : ℕ
h2 : ¬∃ n, enum A t n
⊢ ¬t < s
Tactic:
linarith
State after:
no goals

State before:
case Induction_Step
A : Set ℕ
⊢ ∀ (m : ℕ),
    (∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n) →
      ∀ ⦃s : ℕ⦄, num_elts_below A (m + 1) s → ∀ t < s, ∃ n, enum A t n
Tactic:
fix m : Nat
State after:
case Induction_Step
A : Set ℕ
m : ℕ
⊢ (∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n) →
    ∀ ⦃s : ℕ⦄, num_elts_below A (m + 1) s → ∀ t < s, ∃ n, enum A t n

State before:
case Induction_Step
A : Set ℕ
m : ℕ
⊢ (∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n) →
    ∀ ⦃s : ℕ⦄, num_elts_below A (m + 1) s → ∀ t < s, ∃ n, enum A t n
Tactic:
assume ih : ∀ ⦃s : Nat⦄, num_elts_below A m s → ∀ t < s, ∃ (n : Nat), enum A t n
State after:
case Induction_Step
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
⊢ ∀ ⦃s : ℕ⦄, num_elts_below A (m + 1) s → ∀ t < s, ∃ n, enum A t n

State before:
case Induction_Step
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
⊢ ∀ ⦃s : ℕ⦄, num_elts_below A (m + 1) s → ∀ t < s, ∃ n, enum A t n
Tactic:
fix s : Nat
State after:
case Induction_Step
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
⊢ num_elts_below A (m + 1) s → ∀ t < s, ∃ n, enum A t n

State before:
case Induction_Step
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
⊢ num_elts_below A (m + 1) s → ∀ t < s, ∃ n, enum A t n
Tactic:
assume h1 : num_elts_below A (m + 1) s
State after:
case Induction_Step
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : num_elts_below A (m + 1) s
⊢ ∀ t < s, ∃ n, enum A t n

State before:
case Induction_Step
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : num_elts_below A (m + 1) s
⊢ ∀ t < s, ∃ n, enum A t n
Tactic:
by_cases h2 : m ∈ A
State after:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : num_elts_below A (m + 1) s
h2 : m ∈ A
⊢ ∀ t < s, ∃ n, enum A t n

case neg
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : num_elts_below A (m + 1) s
h2 : m ∉ A
⊢ ∀ t < s, ∃ n, enum A t n

State before:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : num_elts_below A (m + 1) s
h2 : m ∈ A
⊢ ∀ t < s, ∃ n, enum A t n
Tactic:
rewrite [neb_step_elt h2] at h1
State after:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
⊢ ∀ t < s, ∃ n, enum A t n

State before:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
⊢ ∀ t < s, ∃ n, enum A t n
Tactic:
have h3 : ∀ t < s - 1, ∃ (n : Nat), enum A t n := ih h1.right
State after:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
⊢ ∀ t < s, ∃ n, enum A t n

State before:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
⊢ ∀ t < s, ∃ n, enum A t n
Tactic:
fix t : Nat
State after:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
⊢ t < s → ∃ n, enum A t n

State before:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
⊢ t < s → ∃ n, enum A t n
Tactic:
assume h4 : t < s
State after:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
⊢ ∃ n, enum A t n

State before:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
⊢ ∃ n, enum A t n
Tactic:
by_cases h5 : t = s - 1
State after:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : t = s - 1
⊢ ∃ n, enum A t n

case neg
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : ¬t = s - 1
⊢ ∃ n, enum A t n

State before:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : t = s - 1
⊢ ∃ n, enum A t n
Tactic:
apply Exists.intro m
State after:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : t = s - 1
⊢ enum A t m

State before:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : t = s - 1
⊢ enum A t m
Tactic:
define
State after:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : t = s - 1
⊢ m ∈ A ∧ num_elts_below A m t

State before:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : t = s - 1
⊢ m ∈ A ∧ num_elts_below A m t
Tactic:
apply And.intro h2
State after:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : t = s - 1
⊢ num_elts_below A m t

State before:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : t = s - 1
⊢ num_elts_below A m t
Tactic:
rewrite [h5]
State after:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : t = s - 1
⊢ num_elts_below A m (s - 1)

State before:
case pos
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : t = s - 1
⊢ num_elts_below A m (s - 1)
Tactic:
show num_elts_below A m (s - 1) from h1.right
State after:
no goals

State before:
case neg
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : ¬t = s - 1
⊢ ∃ n, enum A t n
Tactic:
have h6 : t ≤ s - 1 := Nat.le_pred_of_lt h4
State after:
case neg
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : ¬t = s - 1
h6 : t ≤ s - 1
⊢ ∃ n, enum A t n

State before:
case neg
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : ¬t = s - 1
h6 : t ≤ s - 1
⊢ ∃ n, enum A t n
Tactic:
have h7 : t < s - 1 := Nat.lt_of_le_of_ne h6 h5
State after:
case neg
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : ¬t = s - 1
h6 : t ≤ s - 1
h7 : t < s - 1
⊢ ∃ n, enum A t n

State before:
case neg
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : 1 ≤ s ∧ num_elts_below A m (s - 1)
h2 : m ∈ A
h3 : ∀ t < s - 1, ∃ n, enum A t n
t : ℕ
h4 : t < s
h5 : ¬t = s - 1
h6 : t ≤ s - 1
h7 : t < s - 1
⊢ ∃ n, enum A t n
Tactic:
show ∃ (n : Nat), enum A t n from ih h1.right t h7
State after:
no goals

State before:
case neg
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : num_elts_below A (m + 1) s
h2 : m ∉ A
⊢ ∀ t < s, ∃ n, enum A t n
Tactic:
rewrite [neb_step_not_elt h2] at h1
State after:
case neg
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : num_elts_below A m s
h2 : m ∉ A
⊢ ∀ t < s, ∃ n, enum A t n

State before:
case neg
A : Set ℕ
m : ℕ
ih : ∀ ⦃s : ℕ⦄, num_elts_below A m s → ∀ t < s, ∃ n, enum A t n
s : ℕ
h1 : num_elts_below A m s
h2 : m ∉ A
⊢ ∀ t < s, ∃ n, enum A t n
Tactic:
show ∀ t < s, ∃ (n : Nat), enum A t n from ih h1
State after:
no goals