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

State before:
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
⊢ ∃ g, graph g = inv (graph f)
Tactic:
rewrite [func_from_graph]
State after:
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
⊢ is_func_graph (inv (graph f))

State before:
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
⊢ is_func_graph (inv (graph f))
Tactic:
define
State after:
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
⊢ ∀ (x : B), ∃! y, (x, y) ∈ inv (graph f)

State before:
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
⊢ ∀ (x : B), ∃! y, (x, y) ∈ inv (graph f)
Tactic:
fix b : B
State after:
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
⊢ ∃! y, (b, y) ∈ inv (graph f)

State before:
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
⊢ ∃! y, (b, y) ∈ inv (graph f)
Tactic:
exists_unique
State after:
case Existence
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
⊢ ∃ y, (b, y) ∈ inv (graph f)

case Uniqueness
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
⊢ ∀ (y_1 y_2 : A), (b, y_1) ∈ inv (graph f) → (b, y_2) ∈ inv (graph f) → y_1 = y_2

State before:
case Existence
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
⊢ ∃ y, (b, y) ∈ inv (graph f)
Tactic:
define at h2
State after:
case Existence
A B : Type
f : A → B
h1 : one_to_one f
h2 : ∀ (y : B), ∃ x, f x = y
b : B
⊢ ∃ y, (b, y) ∈ inv (graph f)

State before:
case Existence
A B : Type
f : A → B
h1 : one_to_one f
h2 : ∀ (y : B), ∃ x, f x = y
b : B
⊢ ∃ y, (b, y) ∈ inv (graph f)
Tactic:
obtain (a : A) (h4 : f a = b) from h2 b
State after:
case Existence
A B : Type
f : A → B
h1 : one_to_one f
h2 : ∀ (y : B), ∃ x, f x = y
b : B
a : A
h4 : f a = b
⊢ ∃ y, (b, y) ∈ inv (graph f)

State before:
case Existence
A B : Type
f : A → B
h1 : one_to_one f
h2 : ∀ (y : B), ∃ x, f x = y
b : B
a : A
h4 : f a = b
⊢ ∃ y, (b, y) ∈ inv (graph f)
Tactic:
apply Exists.intro a
State after:
case Existence
A B : Type
f : A → B
h1 : one_to_one f
h2 : ∀ (y : B), ∃ x, f x = y
b : B
a : A
h4 : f a = b
⊢ (b, a) ∈ inv (graph f)

State before:
case Existence
A B : Type
f : A → B
h1 : one_to_one f
h2 : ∀ (y : B), ∃ x, f x = y
b : B
a : A
h4 : f a = b
⊢ (b, a) ∈ inv (graph f)
Tactic:
define
State after:
case Existence
A B : Type
f : A → B
h1 : one_to_one f
h2 : ∀ (y : B), ∃ x, f x = y
b : B
a : A
h4 : f a = b
⊢ f a = b

State before:
case Existence
A B : Type
f : A → B
h1 : one_to_one f
h2 : ∀ (y : B), ∃ x, f x = y
b : B
a : A
h4 : f a = b
⊢ f a = b
Tactic:
show f a = b from h4
State after:
no goals

State before:
case Uniqueness
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
⊢ ∀ (y_1 y_2 : A), (b, y_1) ∈ inv (graph f) → (b, y_2) ∈ inv (graph f) → y_1 = y_2
Tactic:
fix a1 : A
State after:
case Uniqueness
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
a1 : A
⊢ ∀ (y_2 : A), (b, a1) ∈ inv (graph f) → (b, y_2) ∈ inv (graph f) → a1 = y_2

State before:
case Uniqueness
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
a1 : A
⊢ ∀ (y_2 : A), (b, a1) ∈ inv (graph f) → (b, y_2) ∈ inv (graph f) → a1 = y_2
Tactic:
fix a2 : A
State after:
case Uniqueness
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
a1 a2 : A
⊢ (b, a1) ∈ inv (graph f) → (b, a2) ∈ inv (graph f) → a1 = a2

State before:
case Uniqueness
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
a1 a2 : A
⊢ (b, a1) ∈ inv (graph f) → (b, a2) ∈ inv (graph f) → a1 = a2
Tactic:
assume h3 : (b, a1) ∈ inv (graph f)
State after:
case Uniqueness
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
a1 a2 : A
h3 : (b, a1) ∈ inv (graph f)
⊢ (b, a2) ∈ inv (graph f) → a1 = a2

State before:
case Uniqueness
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
a1 a2 : A
h3 : (b, a1) ∈ inv (graph f)
⊢ (b, a2) ∈ inv (graph f) → a1 = a2
Tactic:
assume h4 : (b, a2) ∈ inv (graph f)
State after:
case Uniqueness
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
a1 a2 : A
h3 : (b, a1) ∈ inv (graph f)
h4 : (b, a2) ∈ inv (graph f)
⊢ a1 = a2

State before:
case Uniqueness
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
a1 a2 : A
h3 : (b, a1) ∈ inv (graph f)
h4 : (b, a2) ∈ inv (graph f)
⊢ a1 = a2
Tactic:
define at h3
State after:
case Uniqueness
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
a1 a2 : A
h3 : f a1 = b
h4 : (b, a2) ∈ inv (graph f)
⊢ a1 = a2

State before:
case Uniqueness
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
a1 a2 : A
h3 : f a1 = b
h4 : (b, a2) ∈ inv (graph f)
⊢ a1 = a2
Tactic:
define at h4
State after:
case Uniqueness
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
a1 a2 : A
h3 : f a1 = b
h4 : f a2 = b
⊢ a1 = a2

State before:
case Uniqueness
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
a1 a2 : A
h3 : f a1 = b
h4 : f a2 = b
⊢ a1 = a2
Tactic:
rewrite [←h4] at h3
State after:
case Uniqueness
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
a1 a2 : A
h3 : f a1 = f a2
h4 : f a2 = b
⊢ a1 = a2

State before:
case Uniqueness
A B : Type
f : A → B
h1 : one_to_one f
h2 : onto f
b : B
a1 a2 : A
h3 : f a1 = f a2
h4 : f a2 = b
⊢ a1 = a2
Tactic:
define at h1
State after:
case Uniqueness
A B : Type
f : A → B
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : onto f
b : B
a1 a2 : A
h3 : f a1 = f a2
h4 : f a2 = b
⊢ a1 = a2

State before:
case Uniqueness
A B : Type
f : A → B
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : onto f
b : B
a1 a2 : A
h3 : f a1 = f a2
h4 : f a2 = b
⊢ a1 = a2
Tactic:
show a1 = a2 from h1 a1 a2 h3
State after:
no goals