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

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

State before:
U V : Type
R : Rel U V
A : Set U
x : U
h1 : ∀ ⦃x : U⦄, x ∈ A → ∃! y, R x y
h2 : x ∈ A
⊢ ∃ y, R x y
Tactic:
obtain (y : V) (h3 : R x y)
  (h4 : ∀ (y_1 y_2 : V), R x y_1 → R x y_2 → y_1 = y_2) from h1 h2
State after:
U V : Type
R : Rel U V
A : Set U
x : U
h1 : ∀ ⦃x : U⦄, x ∈ A → ∃! y, R x y
h2 : x ∈ A
y : V
h3 : R x y
h4 : ∀ (y_1 y_2 : V), R x y_1 → R x y_2 → y_1 = y_2
⊢ ∃ y, R x y

State before:
U V : Type
R : Rel U V
A : Set U
x : U
h1 : ∀ ⦃x : U⦄, x ∈ A → ∃! y, R x y
h2 : x ∈ A
y : V
h3 : R x y
h4 : ∀ (y_1 y_2 : V), R x y_1 → R x y_2 → y_1 = y_2
⊢ ∃ y, R x y
Tactic:
show ∃ (y : V), R x y from Exists.intro y h3
State after:
no goals