Theorem: HTPI.nonempty_of_pos_numElts (HTPILib/Chap8Part1.lean)

State before:
U : Type
A : Set U
n : ℕ
h1 : numElts A n
h2 : n > 0
⊢ ∃ x, x ∈ A
Tactic:
define at h1
State after:
U : Type
A : Set U
n : ℕ
h1 : ∃ R, matching R (I n) A
h2 : n > 0
⊢ ∃ x, x ∈ A

State before:
U : Type
A : Set U
n : ℕ
h1 : ∃ R, matching R (I n) A
h2 : n > 0
⊢ ∃ x, x ∈ A
Tactic:
obtain (R : Rel Nat U) (h3 : matching R (I n) A) from h1
State after:
U : Type
A : Set U
n : ℕ
h1 : ∃ R, matching R (I n) A
h2 : n > 0
R : Rel ℕ U
h3 : matching R (I n) A
⊢ ∃ x, x ∈ A

State before:
U : Type
A : Set U
n : ℕ
h1 : ∃ R, matching R (I n) A
h2 : n > 0
R : Rel ℕ U
h3 : matching R (I n) A
⊢ ∃ x, x ∈ A
Tactic:
define at h3
State after:
U : Type
A : Set U
n : ℕ
h1 : ∃ R, matching R (I n) A
h2 : n > 0
R : Rel ℕ U
h3 : rel_within R (I n) A ∧ fcnl_on R (I n) ∧ fcnl_on (invRel R) A
⊢ ∃ x, x ∈ A

State before:
U : Type
A : Set U
n : ℕ
h1 : ∃ R, matching R (I n) A
h2 : n > 0
R : Rel ℕ U
h3 : rel_within R (I n) A ∧ fcnl_on R (I n) ∧ fcnl_on (invRel R) A
⊢ ∃ x, x ∈ A
Tactic:
have h4 : 0 ∈ I n := h2
State after:
U : Type
A : Set U
n : ℕ
h1 : ∃ R, matching R (I n) A
h2 : n > 0
R : Rel ℕ U
h3 : rel_within R (I n) A ∧ fcnl_on R (I n) ∧ fcnl_on (invRel R) A
h4 : 0 ∈ I n
⊢ ∃ x, x ∈ A

State before:
U : Type
A : Set U
n : ℕ
h1 : ∃ R, matching R (I n) A
h2 : n > 0
R : Rel ℕ U
h3 : rel_within R (I n) A ∧ fcnl_on R (I n) ∧ fcnl_on (invRel R) A
h4 : 0 ∈ I n
⊢ ∃ x, x ∈ A
Tactic:
obtain (x : U) (h5 : R 0 x) from fcnl_exists h3.right.left h4
State after:
U : Type
A : Set U
n : ℕ
h1 : ∃ R, matching R (I n) A
h2 : n > 0
R : Rel ℕ U
h3 : rel_within R (I n) A ∧ fcnl_on R (I n) ∧ fcnl_on (invRel R) A
h4 : 0 ∈ I n
x : U
h5 : R 0 x
⊢ ∃ x, x ∈ A

State before:
U : Type
A : Set U
n : ℕ
h1 : ∃ R, matching R (I n) A
h2 : n > 0
R : Rel ℕ U
h3 : rel_within R (I n) A ∧ fcnl_on R (I n) ∧ fcnl_on (invRel R) A
h4 : 0 ∈ I n
x : U
h5 : R 0 x
⊢ ∃ x, x ∈ A
Tactic:
have h6 : 0 ∈ I n ∧ x ∈ A := h3.left h5
State after:
U : Type
A : Set U
n : ℕ
h1 : ∃ R, matching R (I n) A
h2 : n > 0
R : Rel ℕ U
h3 : rel_within R (I n) A ∧ fcnl_on R (I n) ∧ fcnl_on (invRel R) A
h4 : 0 ∈ I n
x : U
h5 : R 0 x
h6 : 0 ∈ I n ∧ x ∈ A
⊢ ∃ x, x ∈ A

State before:
U : Type
A : Set U
n : ℕ
h1 : ∃ R, matching R (I n) A
h2 : n > 0
R : Rel ℕ U
h3 : rel_within R (I n) A ∧ fcnl_on R (I n) ∧ fcnl_on (invRel R) A
h4 : 0 ∈ I n
x : U
h5 : R 0 x
h6 : 0 ∈ I n ∧ x ∈ A
⊢ ∃ x, x ∈ A
Tactic:
show ∃ (x : U), x ∈ A from Exists.intro x h6.right
State after:
no goals