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

State before:
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ fcnl_on (enum A) (Univ ℕ)
Tactic:
define
State after:
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ ∀ ⦃x : ℕ⦄, x ∈ Univ ℕ → ∃! y, enum A x y

State before:
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ ∀ ⦃x : ℕ⦄, x ∈ Univ ℕ → ∃! y, enum A x y
Tactic:
by_induc
State after:
case Base_Case
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ 0 ∈ Univ ℕ → ∃! y, enum A 0 y

case Induction_Step
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ ∀ (x : ℕ), (x ∈ Univ ℕ → ∃! y, enum A x y) → x + 1 ∈ Univ ℕ → ∃! y, enum A (x + 1) y

State before:
case Base_Case
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ 0 ∈ Univ ℕ → ∃! y, enum A 0 y
Tactic:
assume h2 : 0 ∈ Univ Nat
State after:
case Base_Case
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
⊢ ∃! y, enum A 0 y

State before:
case Base_Case
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
⊢ ∃! y, enum A 0 y
Tactic:
exists_unique
State after:
case Base_Case.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
⊢ ∃ y, enum A 0 y

case Base_Case.Uniqueness
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
⊢ ∀ (y_1 y_2 : ℕ), enum A 0 y_1 → enum A 0 y_2 → y_1 = y_2

State before:
case Base_Case.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
⊢ ∃ y, enum A 0 y
Tactic:
obtain (n : Nat) (h3 : n ∈ A ∧ n ≥0) from h1 0
State after:
case Base_Case.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
n : ℕ
h3 : n ∈ A ∧ n ≥ 0
⊢ ∃ y, enum A 0 y

State before:
case Base_Case.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
n : ℕ
h3 : n ∈ A ∧ n ≥ 0
⊢ ∃ y, enum A 0 y
Tactic:
obtain (s : Nat) (h4 : num_elts_below A (n + 1) s) from neb_exists A (n + 1)
State after:
case Base_Case.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
n : ℕ
h3 : n ∈ A ∧ n ≥ 0
s : ℕ
h4 : num_elts_below A (n + 1) s
⊢ ∃ y, enum A 0 y

State before:
case Base_Case.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
n : ℕ
h3 : n ∈ A ∧ n ≥ 0
s : ℕ
h4 : num_elts_below A (n + 1) s
⊢ ∃ y, enum A 0 y
Tactic:
have h5 : ∀ (t : Nat), t < s → ∃ (n : Nat), enum A t n := enum_not_skip h4
State after:
case Base_Case.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
n : ℕ
h3 : n ∈ A ∧ n ≥ 0
s : ℕ
h4 : num_elts_below A (n + 1) s
h5 : ∀ t < s, ∃ n, enum A t n
⊢ ∃ y, enum A 0 y

State before:
case Base_Case.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
n : ℕ
h3 : n ∈ A ∧ n ≥ 0
s : ℕ
h4 : num_elts_below A (n + 1) s
h5 : ∀ t < s, ∃ n, enum A t n
⊢ ∃ y, enum A 0 y
Tactic:
rewrite [neb_step_elt h3.left] at h4
State after:
case Base_Case.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
n : ℕ
h3 : n ∈ A ∧ n ≥ 0
s : ℕ
h4 : 1 ≤ s ∧ num_elts_below A n (s - 1)
h5 : ∀ t < s, ∃ n, enum A t n
⊢ ∃ y, enum A 0 y

State before:
case Base_Case.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
n : ℕ
h3 : n ∈ A ∧ n ≥ 0
s : ℕ
h4 : 1 ≤ s ∧ num_elts_below A n (s - 1)
h5 : ∀ t < s, ∃ n, enum A t n
⊢ ∃ y, enum A 0 y
Tactic:
show ∃ (y : Nat), enum A 0 y from h5 0 h4.left
State after:
no goals

State before:
case Base_Case.Uniqueness
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
h2 : 0 ∈ Univ ℕ
⊢ ∀ (y_1 y_2 : ℕ), enum A 0 y_1 → enum A 0 y_2 → y_1 = y_2
Tactic:
show ∀ (y_1 y_2 : Nat), enum A 0 y_1 → enum A 0 y_2 → y_1 = y_2 from enum_unique A 0
State after:
no goals

State before:
case Induction_Step
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ ∀ (x : ℕ), (x ∈ Univ ℕ → ∃! y, enum A x y) → x + 1 ∈ Univ ℕ → ∃! y, enum A (x + 1) y
Tactic:
fix s : Nat
State after:
case Induction_Step
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
⊢ (s ∈ Univ ℕ → ∃! y, enum A s y) → s + 1 ∈ Univ ℕ → ∃! y, enum A (s + 1) y

State before:
case Induction_Step
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
⊢ (s ∈ Univ ℕ → ∃! y, enum A s y) → s + 1 ∈ Univ ℕ → ∃! y, enum A (s + 1) y
Tactic:
assume ih : s ∈ Univ Nat → ∃! (y : Nat), enum A s y
State after:
case Induction_Step
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
⊢ s + 1 ∈ Univ ℕ → ∃! y, enum A (s + 1) y

State before:
case Induction_Step
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
⊢ s + 1 ∈ Univ ℕ → ∃! y, enum A (s + 1) y
Tactic:
assume h2 : s + 1 ∈ Univ Nat
State after:
case Induction_Step
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
⊢ ∃! y, enum A (s + 1) y

State before:
case Induction_Step
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
⊢ ∃! y, enum A (s + 1) y
Tactic:
exists_unique
State after:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
⊢ ∃ y, enum A (s + 1) y

case Induction_Step.Uniqueness
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
⊢ ∀ (y_1 y_2 : ℕ), enum A (s + 1) y_1 → enum A (s + 1) y_2 → y_1 = y_2

State before:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
⊢ ∃ y, enum A (s + 1) y
Tactic:
have h3 : s ∈ Univ Nat := elt_Univ s
State after:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
⊢ ∃ y, enum A (s + 1) y

State before:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
⊢ ∃ y, enum A (s + 1) y
Tactic:
obtain (m : Nat) (h4 : enum A s m)
  (h5 : ∀ (y_1 y_2 : Nat), enum A s y_1 → enum A s y_2 → y_1 = y_2) from ih h3
State after:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
⊢ ∃ y, enum A (s + 1) y

State before:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
⊢ ∃ y, enum A (s + 1) y
Tactic:
obtain (n : Nat) (h6 : n ∈ A ∧ n ≥ m + 1) from h1 (m + 1)
State after:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
⊢ ∃ y, enum A (s + 1) y

State before:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
⊢ ∃ y, enum A (s + 1) y
Tactic:
obtain (t : Nat) (h7 : num_elts_below A n t) from neb_exists A n
State after:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
⊢ ∃ y, enum A (s + 1) y

State before:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
⊢ ∃ y, enum A (s + 1) y
Tactic:
have h8 : s < t := neb_increase h4 h6.right h7
State after:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
⊢ ∃ y, enum A (s + 1) y

State before:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
⊢ ∃ y, enum A (s + 1) y
Tactic:
have h9 : s + 1 < t ∨ s + 1 = t := Nat.lt_or_eq_of_le h8
State after:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
h9 : s + 1 < t ∨ s + 1 = t
⊢ ∃ y, enum A (s + 1) y

State before:
case Induction_Step.Existence
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
h9 : s + 1 < t ∨ s + 1 = t
⊢ ∃ y, enum A (s + 1) y
Tactic:
by_cases on h9
State after:
case Induction_Step.Existence.Case_1
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
h9 : s + 1 < t
⊢ ∃ y, enum A (s + 1) y

case Induction_Step.Existence.Case_2
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
h9 : s + 1 = t
⊢ ∃ y, enum A (s + 1) y

State before:
case Induction_Step.Existence.Case_1
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
h9 : s + 1 < t
⊢ ∃ y, enum A (s + 1) y
Tactic:
show ∃ (y : Nat), enum A (s + 1) y from enum_not_skip h7 (s + 1) h9
State after:
no goals

State before:
case Induction_Step.Existence.Case_2
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
h9 : s + 1 = t
⊢ ∃ y, enum A (s + 1) y
Tactic:
rewrite [h9]
State after:
case Induction_Step.Existence.Case_2
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
h9 : s + 1 = t
⊢ ∃ y, enum A t y

State before:
case Induction_Step.Existence.Case_2
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
h9 : s + 1 = t
⊢ ∃ y, enum A t y
Tactic:
apply Exists.intro n
State after:
case Induction_Step.Existence.Case_2
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
h9 : s + 1 = t
⊢ enum A t n

State before:
case Induction_Step.Existence.Case_2
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
h9 : s + 1 = t
⊢ enum A t n
Tactic:
define
State after:
case Induction_Step.Existence.Case_2
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
h9 : s + 1 = t
⊢ n ∈ A ∧ num_elts_below A n t

State before:
case Induction_Step.Existence.Case_2
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
h3 : s ∈ Univ ℕ
m : ℕ
h4 : enum A s m
h5 : ∀ (y_1 y_2 : ℕ), enum A s y_1 → enum A s y_2 → y_1 = y_2
n : ℕ
h6 : n ∈ A ∧ n ≥ m + 1
t : ℕ
h7 : num_elts_below A n t
h8 : s < t
h9 : s + 1 = t
⊢ n ∈ A ∧ num_elts_below A n t
Tactic:
show n ∈ A ∧ num_elts_below A n t from And.intro h6.left h7
State after:
no goals

State before:
case Induction_Step.Uniqueness
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
ih : s ∈ Univ ℕ → ∃! y, enum A s y
h2 : s + 1 ∈ Univ ℕ
⊢ ∀ (y_1 y_2 : ℕ), enum A (s + 1) y_1 → enum A (s + 1) y_2 → y_1 = y_2
Tactic:
show ∀ (y_1 y_2 : Nat), enum A (s + 1) y_1 → enum A (s + 1) y_2 → y_1 = y_2
  from enum_unique A (s + 1)
State after:
no goals