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

State before:
U : Type
A : Set U
⊢ numElts A 0 ↔ empty A
Tactic:
apply Iff.intro
State after:
case mp
U : Type
A : Set U
⊢ numElts A 0 → empty A

case mpr
U : Type
A : Set U
⊢ empty A → numElts A 0

State before:
case mp
U : Type
A : Set U
⊢ numElts A 0 → empty A
Tactic:
assume h1 : numElts A 0
State after:
case mp
U : Type
A : Set U
h1 : numElts A 0
⊢ empty A

State before:
case mp
U : Type
A : Set U
h1 : numElts A 0
⊢ empty A
Tactic:
define
State after:
case mp
U : Type
A : Set U
h1 : numElts A 0
⊢ ¬∃ x, x ∈ A

State before:
case mp
U : Type
A : Set U
h1 : numElts A 0
⊢ ¬∃ x, x ∈ A
Tactic:
by_contra h2
State after:
case mp
U : Type
A : Set U
h1 : numElts A 0
h2 : ∃ x, x ∈ A
⊢ False

State before:
case mp
U : Type
A : Set U
h1 : numElts A 0
h2 : ∃ x, x ∈ A
⊢ False
Tactic:
obtain (x : U) (h3 : x ∈ A) from h2
State after:
case mp
U : Type
A : Set U
h1 : numElts A 0
h2 : ∃ x, x ∈ A
x : U
h3 : x ∈ A
⊢ False

State before:
case mp
U : Type
A : Set U
h1 : numElts A 0
h2 : ∃ x, x ∈ A
x : U
h3 : x ∈ A
⊢ False
Tactic:
define at h1
State after:
case mp
U : Type
A : Set U
h1 : ∃ R, matching R (I 0) A
h2 : ∃ x, x ∈ A
x : U
h3 : x ∈ A
⊢ False

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

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

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

State before:
case mp
U : Type
A : Set U
h1 : ∃ R, matching R (I 0) A
h2 : ∃ x, x ∈ A
x : U
h3 : x ∈ A
R : Rel ℕ U
h4 : rel_within R (I 0) A ∧ fcnl_on R (I 0) ∧ fcnl_on (invRel R) A
j : ℕ
h5 : invRel R x j
⊢ False
Tactic:
define at h5
State after:
case mp
U : Type
A : Set U
h1 : ∃ R, matching R (I 0) A
h2 : ∃ x, x ∈ A
x : U
h3 : x ∈ A
R : Rel ℕ U
h4 : rel_within R (I 0) A ∧ fcnl_on R (I 0) ∧ fcnl_on (invRel R) A
j : ℕ
h5 : R j x
⊢ False

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

State before:
case mp
U : Type
A : Set U
h1 : ∃ R, matching R (I 0) A
h2 : ∃ x, x ∈ A
x : U
h3 : x ∈ A
R : Rel ℕ U
h4 : rel_within R (I 0) A ∧ fcnl_on R (I 0) ∧ fcnl_on (invRel R) A
j : ℕ
h5 : R j x
h6 : j ∈ I 0 ∧ x ∈ A
⊢ False
Tactic:
contradict I_0_empty
State after:
case mp
U : Type
A : Set U
h1 : ∃ R, matching R (I 0) A
h2 : ∃ x, x ∈ A
x : U
h3 : x ∈ A
R : Rel ℕ U
h4 : rel_within R (I 0) A ∧ fcnl_on R (I 0) ∧ fcnl_on (invRel R) A
j : ℕ
h5 : R j x
h6 : j ∈ I 0 ∧ x ∈ A
⊢ ∃ x, x ∈ I 0

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

State before:
case mpr
U : Type
A : Set U
⊢ empty A → numElts A 0
Tactic:
assume h1 : empty A
State after:
case mpr
U : Type
A : Set U
h1 : empty A
⊢ numElts A 0

State before:
case mpr
U : Type
A : Set U
h1 : empty A
⊢ numElts A 0
Tactic:
show ∃ (R : Rel Nat U), matching R (I 0) A from
  Exists.intro (emptyRel Nat U) (empty_match I_0_empty h1)
State after:
no goals