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

State before:
U V : Type
R : Rel U V
A : Set U
h1 : empty A
⊢ fcnl_on R A
Tactic:
define
State after:
U V : Type
R : Rel U V
A : Set U
h1 : empty A
⊢ ∀ ⦃x : U⦄, x ∈ A → ∃! y, R x y

State before:
U V : Type
R : Rel U V
A : Set U
h1 : empty A
⊢ ∀ ⦃x : U⦄, x ∈ A → ∃! y, R x y
Tactic:
fix a : U
State after:
U V : Type
R : Rel U V
A : Set U
h1 : empty A
a : U
⊢ a ∈ A → ∃! y, R a y

State before:
U V : Type
R : Rel U V
A : Set U
h1 : empty A
a : U
⊢ a ∈ A → ∃! y, R a y
Tactic:
assume h2 : a ∈ A
State after:
U V : Type
R : Rel U V
A : Set U
h1 : empty A
a : U
h2 : a ∈ A
⊢ ∃! y, R a y

State before:
U V : Type
R : Rel U V
A : Set U
h1 : empty A
a : U
h2 : a ∈ A
⊢ ∃! y, R a y
Tactic:
contradict h1 with h3
State after:
U V : Type
R : Rel U V
A : Set U
h1 : empty A
a : U
h2 : a ∈ A
h3 : ¬∃! y, R a y
⊢ ∃ x, x ∈ A

State before:
U V : Type
R : Rel U V
A : Set U
h1 : empty A
a : U
h2 : a ∈ A
h3 : ¬∃! y, R a y
⊢ ∃ x, x ∈ A
Tactic:
show ∃ (x : U), x ∈ A from Exists.intro a h2
State after:
no goals