Theorem: HTPI.func_from_graph_rtl (HTPILib/Chap5.lean)

State before:
A B : Type
F : Set (A × B)
⊢ is_func_graph F → ∃ f, graph f = F
Tactic:
assume h1 : is_func_graph F
State after:
A B : Type
F : Set (A × B)
h1 : is_func_graph F
⊢ ∃ f, graph f = F

State before:
A B : Type
F : Set (A × B)
h1 : is_func_graph F
⊢ ∃ f, graph f = F
Tactic:
define at h1
State after:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
⊢ ∃ f, graph f = F

State before:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
⊢ ∃ f, graph f = F
Tactic:
have h2 : ∀ (x : A), ∃ (y : B), (x, y) ∈ F := by
  fix x : A
  obtain (y : B) (h3 : (x, y) ∈ F)
    (h4 : ∀ (y1 y2 : B), (x, y1) ∈ F → (x, y2) ∈ F → y1 = y2) from h1 x
  show ∃ (y : B), (x, y) ∈ F from Exists.intro y h3
  done
State after:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
⊢ ∃ f, graph f = F

State before:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
⊢ ∃ f, graph f = F
Tactic:
set f : A → B := fun (x : A) => Classical.choose (h2 x)
State after:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
⊢ ∃ f, graph f = F

State before:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
⊢ ∃ f, graph f = F
Tactic:
apply Exists.intro f
State after:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
⊢ graph f = F

State before:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
⊢ graph f = F
Tactic:
apply Set.ext
State after:
case h
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
⊢ ∀ (x : A × B), x ∈ graph f ↔ x ∈ F

State before:
case h
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
⊢ ∀ (x : A × B), x ∈ graph f ↔ x ∈ F
Tactic:
fix (x, y) : A × B
State after:
case h
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
⊢ (x, y) ∈ graph f ↔ (x, y) ∈ F

State before:
case h
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
⊢ (x, y) ∈ graph f ↔ (x, y) ∈ F
Tactic:
have h3 : (x, f x) ∈ F := Classical.choose_spec (h2 x)
State after:
case h
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
⊢ (x, y) ∈ graph f ↔ (x, y) ∈ F

State before:
case h
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
⊢ (x, y) ∈ graph f ↔ (x, y) ∈ F
Tactic:
apply Iff.intro
State after:
case h.mp
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
⊢ (x, y) ∈ graph f → (x, y) ∈ F

case h.mpr
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
⊢ (x, y) ∈ F → (x, y) ∈ graph f

State before:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
⊢ ∀ (x : A), ∃ y, (x, y) ∈ F
Tactic:
fix x : A
State after:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
x : A
⊢ ∃ y, (x, y) ∈ F

State before:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
x : A
⊢ ∃ y, (x, y) ∈ F
Tactic:
obtain (y : B) (h3 : (x, y) ∈ F)
  (h4 : ∀ (y1 y2 : B), (x, y1) ∈ F → (x, y2) ∈ F → y1 = y2) from h1 x
State after:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
x : A
y : B
h3 : (x, y) ∈ F
h4 : ∀ (y_1 y_2 : B), (x, y_1) ∈ F → (x, y_2) ∈ F → y_1 = y_2
⊢ ∃ y, (x, y) ∈ F

State before:
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
x : A
y : B
h3 : (x, y) ∈ F
h4 : ∀ (y_1 y_2 : B), (x, y_1) ∈ F → (x, y_2) ∈ F → y_1 = y_2
⊢ ∃ y, (x, y) ∈ F
Tactic:
show ∃ (y : B), (x, y) ∈ F from Exists.intro y h3
State after:
no goals

State before:
case h.mp
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
⊢ (x, y) ∈ graph f → (x, y) ∈ F
Tactic:
assume h4 : (x, y) ∈ graph f
State after:
case h.mp
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
h4 : (x, y) ∈ graph f
⊢ (x, y) ∈ F

State before:
case h.mp
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
h4 : (x, y) ∈ graph f
⊢ (x, y) ∈ F
Tactic:
define at h4
State after:
case h.mp
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
h4 : f x = y
⊢ (x, y) ∈ F

State before:
case h.mp
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
h4 : f x = y
⊢ (x, y) ∈ F
Tactic:
rewrite [h4] at h3
State after:
case h.mp
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, y) ∈ F
h4 : f x = y
⊢ (x, y) ∈ F

State before:
case h.mp
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, y) ∈ F
h4 : f x = y
⊢ (x, y) ∈ F
Tactic:
show (x, y) ∈ F from h3
State after:
no goals

State before:
case h.mpr
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
⊢ (x, y) ∈ F → (x, y) ∈ graph f
Tactic:
assume h4 : (x, y) ∈ F
State after:
case h.mpr
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
h4 : (x, y) ∈ F
⊢ (x, y) ∈ graph f

State before:
case h.mpr
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
h4 : (x, y) ∈ F
⊢ (x, y) ∈ graph f
Tactic:
define
State after:
case h.mpr
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
h4 : (x, y) ∈ F
⊢ f x = y

State before:
case h.mpr
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
h4 : (x, y) ∈ F
⊢ f x = y
Tactic:
obtain (z : B) (h5 : (x, z) ∈ F)
  (h6 : ∀ (y1 y2 : B), (x, y1) ∈ F → (x, y2) ∈ F → y1 = y2) from h1 x
State after:
case h.mpr
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
h4 : (x, y) ∈ F
z : B
h5 : (x, z) ∈ F
h6 : ∀ (y_1 y_2 : B), (x, y_1) ∈ F → (x, y_2) ∈ F → y_1 = y_2
⊢ f x = y

State before:
case h.mpr
A B : Type
F : Set (A × B)
h1 : ∀ (x : A), ∃! y, (x, y) ∈ F
h2 : ∀ (x : A), ∃ y, (x, y) ∈ F
f : A → B := fun x => Classical.choose (_ : ∃ y, (x, y) ∈ F)
x : A
y : B
h3 : (x, f x) ∈ F
h4 : (x, y) ∈ F
z : B
h5 : (x, z) ∈ F
h6 : ∀ (y_1 y_2 : B), (x, y_1) ∈ F → (x, y_2) ∈ F → y_1 = y_2
⊢ f x = y
Tactic:
show f x = y from h6 (f x) y h3 h4
State after:
no goals