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

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

State before:
U V : Type
R : Rel U V
A : Set U
x : U
y1 y2 : V
h1 : ∀ ⦃x : U⦄, x ∈ A → ∃! y, R x y
h2 : x ∈ A
h3 : R x y1
h4 : R x y2
⊢ y1 = y2
Tactic:
obtain (z : V) (h5 : R x z)
  (h6 : ∀ (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
y1 y2 : V
h1 : ∀ ⦃x : U⦄, x ∈ A → ∃! y, R x y
h2 : x ∈ A
h3 : R x y1
h4 : R x y2
z : V
h5 : R x z
h6 : ∀ (y_1 y_2 : V), R x y_1 → R x y_2 → y_1 = y_2
⊢ y1 = y2

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