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

State before:
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ matching (enum A) (Univ ℕ) A
Tactic:
define
State after:
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ rel_within (enum A) (Univ ℕ) A ∧ fcnl_on (enum A) (Univ ℕ) ∧ fcnl_on (invRel (enum A)) A

State before:
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ rel_within (enum A) (Univ ℕ) A ∧ fcnl_on (enum A) (Univ ℕ) ∧ fcnl_on (invRel (enum A)) A
Tactic:
apply And.intro
State after:
case left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ rel_within (enum A) (Univ ℕ) A

case right
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ fcnl_on (enum A) (Univ ℕ) ∧ fcnl_on (invRel (enum A)) A

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

State before:
case left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ ∀ ⦃x y : ℕ⦄, enum A x y → x ∈ Univ ℕ ∧ y ∈ A
Tactic:
fix s : Nat
State after:
case left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
⊢ ∀ ⦃y : ℕ⦄, enum A s y → s ∈ Univ ℕ ∧ y ∈ A

State before:
case left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s : ℕ
⊢ ∀ ⦃y : ℕ⦄, enum A s y → s ∈ Univ ℕ ∧ y ∈ A
Tactic:
fix n : Nat
State after:
case left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s n : ℕ
⊢ enum A s n → s ∈ Univ ℕ ∧ n ∈ A

State before:
case left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s n : ℕ
⊢ enum A s n → s ∈ Univ ℕ ∧ n ∈ A
Tactic:
assume h2 : enum A s n
State after:
case left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s n : ℕ
h2 : enum A s n
⊢ s ∈ Univ ℕ ∧ n ∈ A

State before:
case left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s n : ℕ
h2 : enum A s n
⊢ s ∈ Univ ℕ ∧ n ∈ A
Tactic:
define at h2
State after:
case left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s n : ℕ
h2 : n ∈ A ∧ num_elts_below A n s
⊢ s ∈ Univ ℕ ∧ n ∈ A

State before:
case left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
s n : ℕ
h2 : n ∈ A ∧ num_elts_below A n s
⊢ s ∈ Univ ℕ ∧ n ∈ A
Tactic:
apply And.intro (elt_Univ s) h2.left
State after:
no goals

State before:
case right
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ fcnl_on (enum A) (Univ ℕ) ∧ fcnl_on (invRel (enum A)) A
Tactic:
apply And.intro
State after:
case right.left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ fcnl_on (enum A) (Univ ℕ)

case right.right
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ fcnl_on (invRel (enum A)) A

State before:
case right.left
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ fcnl_on (enum A) (Univ ℕ)
Tactic:
show fcnl_on (enum A) (Univ Nat) from enum_fcnl_of_unbdd h1
State after:
no goals

State before:
case right.right
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, n ≥ m
⊢ fcnl_on (invRel (enum A)) A
Tactic:
show fcnl_on (invRel (enum A)) A from inv_enum_fcnl A
State after:
no goals