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

State before:
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ matching (emptyRel U V) A B
Tactic:
define
State after:
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ rel_within (emptyRel U V) A B ∧ fcnl_on (emptyRel U V) A ∧ fcnl_on (invRel (emptyRel U V)) B

State before:
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ rel_within (emptyRel U V) A B ∧ fcnl_on (emptyRel U V) A ∧ fcnl_on (invRel (emptyRel U V)) B
Tactic:
apply And.intro
State after:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ rel_within (emptyRel U V) A B

case right
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ fcnl_on (emptyRel U V) A ∧ fcnl_on (invRel (emptyRel U V)) B

State before:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ rel_within (emptyRel U V) A B
Tactic:
define
State after:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ ∀ ⦃x : U⦄ ⦃y : V⦄, emptyRel U V x y → x ∈ A ∧ y ∈ B

State before:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ ∀ ⦃x : U⦄ ⦃y : V⦄, emptyRel U V x y → x ∈ A ∧ y ∈ B
Tactic:
fix a : U
State after:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
a : U
⊢ ∀ ⦃y : V⦄, emptyRel U V a y → a ∈ A ∧ y ∈ B

State before:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
a : U
⊢ ∀ ⦃y : V⦄, emptyRel U V a y → a ∈ A ∧ y ∈ B
Tactic:
fix b : V
State after:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
a : U
b : V
⊢ emptyRel U V a b → a ∈ A ∧ b ∈ B

State before:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
a : U
b : V
⊢ emptyRel U V a b → a ∈ A ∧ b ∈ B
Tactic:
assume h3 : emptyRel U V a b
State after:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
a : U
b : V
h3 : emptyRel U V a b
⊢ a ∈ A ∧ b ∈ B

State before:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
a : U
b : V
h3 : emptyRel U V a b
⊢ a ∈ A ∧ b ∈ B
Tactic:
by_contra h4
State after:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
a : U
b : V
h3 : emptyRel U V a b
h4 : ¬(a ∈ A ∧ b ∈ B)
⊢ False

State before:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
a : U
b : V
h3 : emptyRel U V a b
h4 : ¬(a ∈ A ∧ b ∈ B)
⊢ False
Tactic:
define at h3
State after:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
a : U
b : V
h3 : False
h4 : ¬(a ∈ A ∧ b ∈ B)
⊢ False

State before:
case left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
a : U
b : V
h3 : False
h4 : ¬(a ∈ A ∧ b ∈ B)
⊢ False
Tactic:
show False from h3
State after:
no goals

State before:
case right
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ fcnl_on (emptyRel U V) A ∧ fcnl_on (invRel (emptyRel U V)) B
Tactic:
apply And.intro
State after:
case right.left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ fcnl_on (emptyRel U V) A

case right.right
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ fcnl_on (invRel (emptyRel U V)) B

State before:
case right.left
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ fcnl_on (emptyRel U V) A
Tactic:
show fcnl_on (emptyRel U V) A from fcnl_on_empty (emptyRel U V) h1
State after:
no goals

State before:
case right.right
U V : Type
A : Set U
B : Set V
h1 : empty A
h2 : empty B
⊢ fcnl_on (invRel (emptyRel U V)) B
Tactic:
show fcnl_on (invRel (emptyRel U V)) B from
  fcnl_on_empty (invRel (emptyRel U V)) h2
State after:
no goals