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

State before:
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
⊢ g ∘ f = id
Tactic:
apply funext
State after:
case h
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
⊢ ∀ (x : A), (g ∘ f) x = id x

State before:
case h
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
⊢ ∀ (x : A), (g ∘ f) x = id x
Tactic:
fix a : A
State after:
case h
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
a : A
⊢ (g ∘ f) a = id a

State before:
case h
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
a : A
⊢ (g ∘ f) a = id a
Tactic:
have h2 : (f a, a) ∈ graph g := by
  rewrite [h1]         define               rfl
  done
State after:
case h
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
a : A
h2 : (f a, a) ∈ graph g
⊢ (g ∘ f) a = id a

State before:
case h
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
a : A
h2 : (f a, a) ∈ graph g
⊢ (g ∘ f) a = id a
Tactic:
define at h2
State after:
case h
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
a : A
h2 : g (f a) = a
⊢ (g ∘ f) a = id a

State before:
case h
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
a : A
h2 : g (f a) = a
⊢ (g ∘ f) a = id a
Tactic:
show (g ∘ f) a = id a from h2
State after:
no goals

State before:
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
a : A
⊢ (f a, a) ∈ graph g
Tactic:
rewrite [h1]
State after:
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
a : A
⊢ (f a, a) ∈ inv (graph f)

State before:
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
a : A
⊢ (f a, a) ∈ inv (graph f)
Tactic:
define
State after:
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
a : A
⊢ f a = f a

State before:
A B : Type
f : A → B
g : B → A
h1 : graph g = inv (graph f)
a : A
⊢ f a = f a
Tactic:
rfl
State after:
no goals