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

State before:
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ matching (enum A) (I s) A
Tactic:
define
State after:
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ rel_within (enum A) (I s) A ∧ fcnl_on (enum A) (I s) ∧ fcnl_on (invRel (enum A)) A

State before:
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ rel_within (enum A) (I s) A ∧ fcnl_on (enum A) (I s) ∧ fcnl_on (invRel (enum A)) A
Tactic:
apply And.intro
State after:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ rel_within (enum A) (I s) A

case right
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ fcnl_on (enum A) (I s) ∧ fcnl_on (invRel (enum A)) A

State before:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ rel_within (enum A) (I s) A
Tactic:
define
State after:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ ∀ ⦃x y : ℕ⦄, enum A x y → x ∈ I s ∧ y ∈ A

State before:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ ∀ ⦃x y : ℕ⦄, enum A x y → x ∈ I s ∧ y ∈ A
Tactic:
fix t : Nat
State after:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t : ℕ
⊢ ∀ ⦃y : ℕ⦄, enum A t y → t ∈ I s ∧ y ∈ A

State before:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t : ℕ
⊢ ∀ ⦃y : ℕ⦄, enum A t y → t ∈ I s ∧ y ∈ A
Tactic:
fix n : Nat
State after:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
⊢ enum A t n → t ∈ I s ∧ n ∈ A

State before:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
⊢ enum A t n → t ∈ I s ∧ n ∈ A
Tactic:
assume h3 : enum A t n
State after:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : enum A t n
⊢ t ∈ I s ∧ n ∈ A

State before:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : enum A t n
⊢ t ∈ I s ∧ n ∈ A
Tactic:
have h4 : ∀ ⦃m : Nat⦄, m ≥ n + 1 → ∀ ⦃t_1 : Nat⦄, num_elts_below A m t_1 → t < t_1 :=
  neb_increase h3
State after:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : enum A t n
h4 : ∀ ⦃m : ℕ⦄, m ≥ n + 1 → ∀ ⦃t_1 : ℕ⦄, num_elts_below A m t_1 → t < t_1
⊢ t ∈ I s ∧ n ∈ A

State before:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : enum A t n
h4 : ∀ ⦃m : ℕ⦄, m ≥ n + 1 → ∀ ⦃t_1 : ℕ⦄, num_elts_below A m t_1 → t < t_1
⊢ t ∈ I s ∧ n ∈ A
Tactic:
define at h3
State after:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : n ∈ A ∧ num_elts_below A n t
h4 : ∀ ⦃m : ℕ⦄, m ≥ n + 1 → ∀ ⦃t_1 : ℕ⦄, num_elts_below A m t_1 → t < t_1
⊢ t ∈ I s ∧ n ∈ A

State before:
case left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : n ∈ A ∧ num_elts_below A n t
h4 : ∀ ⦃m : ℕ⦄, m ≥ n + 1 → ∀ ⦃t_1 : ℕ⦄, num_elts_below A m t_1 → t < t_1
⊢ t ∈ I s ∧ n ∈ A
Tactic:
apply And.intro _ h3.left
State after:
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : n ∈ A ∧ num_elts_below A n t
h4 : ∀ ⦃m : ℕ⦄, m ≥ n + 1 → ∀ ⦃t_1 : ℕ⦄, num_elts_below A m t_1 → t < t_1
⊢ t ∈ I s

State before:
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : n ∈ A ∧ num_elts_below A n t
h4 : ∀ ⦃m : ℕ⦄, m ≥ n + 1 → ∀ ⦃t_1 : ℕ⦄, num_elts_below A m t_1 → t < t_1
⊢ t ∈ I s
Tactic:
define
State after:
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : n ∈ A ∧ num_elts_below A n t
h4 : ∀ ⦃m : ℕ⦄, m ≥ n + 1 → ∀ ⦃t_1 : ℕ⦄, num_elts_below A m t_1 → t < t_1
⊢ t < s

State before:
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : n ∈ A ∧ num_elts_below A n t
h4 : ∀ ⦃m : ℕ⦄, m ≥ n + 1 → ∀ ⦃t_1 : ℕ⦄, num_elts_below A m t_1 → t < t_1
⊢ t < s
Tactic:
have h5 : n < m := h1 n h3.left
State after:
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : n ∈ A ∧ num_elts_below A n t
h4 : ∀ ⦃m : ℕ⦄, m ≥ n + 1 → ∀ ⦃t_1 : ℕ⦄, num_elts_below A m t_1 → t < t_1
h5 : n < m
⊢ t < s

State before:
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : n ∈ A ∧ num_elts_below A n t
h4 : ∀ ⦃m : ℕ⦄, m ≥ n + 1 → ∀ ⦃t_1 : ℕ⦄, num_elts_below A m t_1 → t < t_1
h5 : n < m
⊢ t < s
Tactic:
have h6 : m ≥ n + 1 := h5
State after:
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : n ∈ A ∧ num_elts_below A n t
h4 : ∀ ⦃m : ℕ⦄, m ≥ n + 1 → ∀ ⦃t_1 : ℕ⦄, num_elts_below A m t_1 → t < t_1
h5 : n < m
h6 : m ≥ n + 1
⊢ t < s

State before:
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t n : ℕ
h3 : n ∈ A ∧ num_elts_below A n t
h4 : ∀ ⦃m : ℕ⦄, m ≥ n + 1 → ∀ ⦃t_1 : ℕ⦄, num_elts_below A m t_1 → t < t_1
h5 : n < m
h6 : m ≥ n + 1
⊢ t < s
Tactic:
show t < s from h4 h6 h2
State after:
no goals

State before:
case right
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ fcnl_on (enum A) (I s) ∧ fcnl_on (invRel (enum A)) A
Tactic:
apply And.intro
State after:
case right.left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ fcnl_on (enum A) (I s)

case right.right
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ fcnl_on (invRel (enum A)) A

State before:
case right.left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ fcnl_on (enum A) (I s)
Tactic:
define
State after:
case right.left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ ∀ ⦃x : ℕ⦄, x ∈ I s → ∃! y, enum A x y

State before:
case right.left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
⊢ ∀ ⦃x : ℕ⦄, x ∈ I s → ∃! y, enum A x y
Tactic:
fix t : Nat
State after:
case right.left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t : ℕ
⊢ t ∈ I s → ∃! y, enum A t y

State before:
case right.left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t : ℕ
⊢ t ∈ I s → ∃! y, enum A t y
Tactic:
assume h3 : t ∈ I s
State after:
case right.left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t : ℕ
h3 : t ∈ I s
⊢ ∃! y, enum A t y

State before:
case right.left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t : ℕ
h3 : t ∈ I s
⊢ ∃! y, enum A t y
Tactic:
define at h3
State after:
case right.left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t : ℕ
h3 : t < s
⊢ ∃! y, enum A t y

State before:
case right.left
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t : ℕ
h3 : t < s
⊢ ∃! y, enum A t y
Tactic:
exists_unique
State after:
case right.left.Existence
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t : ℕ
h3 : t < s
⊢ ∃ y, enum A t y

case right.left.Uniqueness
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t : ℕ
h3 : t < s
⊢ ∀ (y_1 y_2 : ℕ), enum A t y_1 → enum A t y_2 → y_1 = y_2

State before:
case right.left.Existence
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t : ℕ
h3 : t < s
⊢ ∃ y, enum A t y
Tactic:
show ∃ (y : Nat), enum A t y from enum_not_skip h2 t h3
State after:
no goals

State before:
case right.left.Uniqueness
A : Set ℕ
m s : ℕ
h1 : ∀ n ∈ A, n < m
h2 : num_elts_below A m s
t : ℕ
h3 : t < s
⊢ ∀ (y_1 y_2 : ℕ), enum A t y_1 → enum A t y_2 → y_1 = y_2
Tactic:
show ∀ (y_1 y_2 : Nat), enum A t y_1 → enum A t y_2 → y_1 = y_2 from
  enum_unique A t
State after:
no goals

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