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

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

State before:
A : Set ℕ
⊢ ∀ ⦃x : ℕ⦄, x ∈ A → ∃! y, invRel (enum A) x y
Tactic:
fix n : Nat
State after:
A : Set ℕ
n : ℕ
⊢ n ∈ A → ∃! y, invRel (enum A) n y

State before:
A : Set ℕ
n : ℕ
⊢ n ∈ A → ∃! y, invRel (enum A) n y
Tactic:
assume h1 : n ∈ A
State after:
A : Set ℕ
n : ℕ
h1 : n ∈ A
⊢ ∃! y, invRel (enum A) n y

State before:
A : Set ℕ
n : ℕ
h1 : n ∈ A
⊢ ∃! y, invRel (enum A) n y
Tactic:
exists_unique
State after:
case Existence
A : Set ℕ
n : ℕ
h1 : n ∈ A
⊢ ∃ y, invRel (enum A) n y

case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
⊢ ∀ (y_1 y_2 : ℕ), invRel (enum A) n y_1 → invRel (enum A) n y_2 → y_1 = y_2

State before:
case Existence
A : Set ℕ
n : ℕ
h1 : n ∈ A
⊢ ∃ y, invRel (enum A) n y
Tactic:
obtain (s : Nat) (h2 : num_elts_below A n s) from neb_exists A n
State after:
case Existence
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
h2 : num_elts_below A n s
⊢ ∃ y, invRel (enum A) n y

State before:
case Existence
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
h2 : num_elts_below A n s
⊢ ∃ y, invRel (enum A) n y
Tactic:
apply Exists.intro s
State after:
case Existence
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
h2 : num_elts_below A n s
⊢ invRel (enum A) n s

State before:
case Existence
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
h2 : num_elts_below A n s
⊢ invRel (enum A) n s
Tactic:
define
State after:
case Existence
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
h2 : num_elts_below A n s
⊢ n ∈ A ∧ num_elts_below A n s

State before:
case Existence
A : Set ℕ
n : ℕ
h1 : n ∈ A
s : ℕ
h2 : num_elts_below A n s
⊢ n ∈ A ∧ num_elts_below A n s
Tactic:
show n ∈ A ∧ num_elts_below A n s from And.intro h1 h2
State after:
no goals

State before:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
⊢ ∀ (y_1 y_2 : ℕ), invRel (enum A) n y_1 → invRel (enum A) n y_2 → y_1 = y_2
Tactic:
fix s1 : Nat
State after:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
s1 : ℕ
⊢ ∀ (y_2 : ℕ), invRel (enum A) n s1 → invRel (enum A) n y_2 → s1 = y_2

State before:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
s1 : ℕ
⊢ ∀ (y_2 : ℕ), invRel (enum A) n s1 → invRel (enum A) n y_2 → s1 = y_2
Tactic:
fix s2 : Nat
State after:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
s1 s2 : ℕ
⊢ invRel (enum A) n s1 → invRel (enum A) n s2 → s1 = s2

State before:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
s1 s2 : ℕ
⊢ invRel (enum A) n s1 → invRel (enum A) n s2 → s1 = s2
Tactic:
assume h2 : invRel (enum A) n s1
State after:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
s1 s2 : ℕ
h2 : invRel (enum A) n s1
⊢ invRel (enum A) n s2 → s1 = s2

State before:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
s1 s2 : ℕ
h2 : invRel (enum A) n s1
⊢ invRel (enum A) n s2 → s1 = s2
Tactic:
assume h3 : invRel (enum A) n s2
State after:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
s1 s2 : ℕ
h2 : invRel (enum A) n s1
h3 : invRel (enum A) n s2
⊢ s1 = s2

State before:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
s1 s2 : ℕ
h2 : invRel (enum A) n s1
h3 : invRel (enum A) n s2
⊢ s1 = s2
Tactic:
define at h2
State after:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
s1 s2 : ℕ
h2 : n ∈ A ∧ num_elts_below A n s1
h3 : invRel (enum A) n s2
⊢ s1 = s2

State before:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
s1 s2 : ℕ
h2 : n ∈ A ∧ num_elts_below A n s1
h3 : invRel (enum A) n s2
⊢ s1 = s2
Tactic:
define at h3
State after:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
s1 s2 : ℕ
h2 : n ∈ A ∧ num_elts_below A n s1
h3 : n ∈ A ∧ num_elts_below A n s2
⊢ s1 = s2

State before:
case Uniqueness
A : Set ℕ
n : ℕ
h1 : n ∈ A
s1 s2 : ℕ
h2 : n ∈ A ∧ num_elts_below A n s1
h3 : n ∈ A ∧ num_elts_below A n s2
⊢ s1 = s2
Tactic:
show s1 = s2 from neb_unique A h2.right h3.right
State after:
no goals