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

State before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
⊢ graph g = inv (graph f)
Tactic:
have h3 : one_to_one f := Theorem_5_3_3_1 f g h1
State after:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
⊢ graph g = inv (graph f)

State before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
⊢ graph g = inv (graph f)
Tactic:
have h4 : onto f := Theorem_5_3_3_2 f g h2
State after:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
⊢ graph g = inv (graph f)

State before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
⊢ graph g = inv (graph f)
Tactic:
obtain (g' : B → A) (h5 : graph g' = inv (graph f))
  from Theorem_5_3_1 f h3 h4
State after:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g' = inv (graph f)
⊢ graph g = inv (graph f)

State before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g' = inv (graph f)
⊢ graph g = inv (graph f)
Tactic:
have h6 : g' ∘ f = id := Theorem_5_3_2_1 f g' h5
State after:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g' = inv (graph f)
h6 : g' ∘ f = id
⊢ graph g = inv (graph f)

State before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g' = inv (graph f)
h6 : g' ∘ f = id
⊢ graph g = inv (graph f)
Tactic:
have h7 : g = g' :=
  calc g
    _ = id ∘ g := by rfl
    _ = (g' ∘ f) ∘ g := by rw [h6]
    _ = g' ∘ (f ∘ g) := by rfl
    _ = g' ∘ id := by rw [h2]
    _ = g' := by rfl
State after:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g' = inv (graph f)
h6 : g' ∘ f = id
h7 : g = g'
⊢ graph g = inv (graph f)

State before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g' = inv (graph f)
h6 : g' ∘ f = id
h7 : g = g'
⊢ graph g = inv (graph f)
Tactic:
rewrite [←h7] at h5
State after:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g = inv (graph f)
h6 : g' ∘ f = id
h7 : g = g'
⊢ graph g = inv (graph f)

State before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g = inv (graph f)
h6 : g' ∘ f = id
h7 : g = g'
⊢ graph g = inv (graph f)
Tactic:
show graph g = inv (graph f) from h5
State after:
no goals

State before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g' = inv (graph f)
h6 : g' ∘ f = id
⊢ g = id ∘ g
Tactic:
rfl
State after:
no goals

State before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g' = inv (graph f)
h6 : g' ∘ f = id
⊢ id ∘ g = (g' ∘ f) ∘ g
Tactic:
rw [h6]
State after:
no goals

State before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g' = inv (graph f)
h6 : g' ∘ f = id
⊢ (g' ∘ f) ∘ g = g' ∘ f ∘ g
Tactic:
rfl
State after:
no goals

State before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g' = inv (graph f)
h6 : g' ∘ f = id
⊢ g' ∘ f ∘ g = g' ∘ id
Tactic:
rw [h2]
State after:
no goals

State before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
h2 : f ∘ g = id
h3 : one_to_one f
h4 : onto f
g' : B → A
h5 : graph g' = inv (graph f)
h6 : g' ∘ f = id
⊢ g' ∘ id = g'
Tactic:
rfl
State after:
no goals