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

State before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
⊢ one_to_one f
Tactic:
define
State after:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
⊢ ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2

State before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
⊢ ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
Tactic:
fix a1 : A
State after:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 : A
⊢ ∀ (x2 : A), f a1 = f x2 → a1 = x2

State before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 : A
⊢ ∀ (x2 : A), f a1 = f x2 → a1 = x2
Tactic:
fix a2 : A
State after:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 a2 : A
⊢ f a1 = f a2 → a1 = a2

State before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 a2 : A
⊢ f a1 = f a2 → a1 = a2
Tactic:
assume h2 : f a1 = f a2
State after:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 a2 : A
h2 : f a1 = f a2
⊢ a1 = a2

State before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 a2 : A
h2 : f a1 = f a2
⊢ a1 = a2
Tactic:
show a1 = a2 from
  calc a1
    _ = id a1 := by rfl
    _ = (g ∘ f) a1 := by rw [h1]
    _ = g (f a1) := by rfl
    _ = g (f a2) := by rw [h2]
    _ = (g ∘ f) a2 := by rfl
    _ = id a2 := by rw [h1]
    _ = a2 := by rfl
State after:
no goals

State before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 a2 : A
h2 : f a1 = f a2
⊢ a1 = id a1
Tactic:
rfl
State after:
no goals

State before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 a2 : A
h2 : f a1 = f a2
⊢ id a1 = (g ∘ f) a1
Tactic:
rw [h1]
State after:
no goals

State before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 a2 : A
h2 : f a1 = f a2
⊢ (g ∘ f) a1 = g (f a1)
Tactic:
rfl
State after:
no goals

State before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 a2 : A
h2 : f a1 = f a2
⊢ g (f a1) = g (f a2)
Tactic:
rw [h2]
State after:
no goals

State before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 a2 : A
h2 : f a1 = f a2
⊢ g (f a2) = (g ∘ f) a2
Tactic:
rfl
State after:
no goals

State before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 a2 : A
h2 : f a1 = f a2
⊢ (g ∘ f) a2 = id a2
Tactic:
rw [h1]
State after:
no goals

State before:
A B : Type
f : A → B
g : B → A
h1 : g ∘ f = id
a1 a2 : A
h2 : f a1 = f a2
⊢ id a2 = a2
Tactic:
rfl
State after:
no goals