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

State before:
A B C : Type
f : A → B
g : B → C
⊢ one_to_one f → one_to_one g → one_to_one (g ∘ f)
Tactic:
assume h1 : one_to_one f
State after:
A B C : Type
f : A → B
g : B → C
h1 : one_to_one f
⊢ one_to_one g → one_to_one (g ∘ f)

State before:
A B C : Type
f : A → B
g : B → C
h1 : one_to_one f
⊢ one_to_one g → one_to_one (g ∘ f)
Tactic:
assume h2 : one_to_one g
State after:
A B C : Type
f : A → B
g : B → C
h1 : one_to_one f
h2 : one_to_one g
⊢ one_to_one (g ∘ f)

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

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

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

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

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

State before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
a1 a2 : A
⊢ (g ∘ f) a1 = (g ∘ f) a2 → a1 = a2
Tactic:
define : (g ∘ f) a1
State after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
a1 a2 : A
⊢ g (f a1) = (g ∘ f) a2 → a1 = a2

State before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
a1 a2 : A
⊢ g (f a1) = (g ∘ f) a2 → a1 = a2
Tactic:
define : (g ∘ f) a2
State after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
a1 a2 : A
⊢ g (f a1) = g (f a2) → a1 = a2

State before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
a1 a2 : A
⊢ g (f a1) = g (f a2) → a1 = a2
Tactic:
assume h3 : g (f a1) = g (f a2)
State after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
a1 a2 : A
h3 : g (f a1) = g (f a2)
⊢ a1 = a2

State before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
a1 a2 : A
h3 : g (f a1) = g (f a2)
⊢ a1 = a2
Tactic:
have h4 : f a1 = f a2 := h2 (f a1) (f a2) h3
State after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
a1 a2 : A
h3 : g (f a1) = g (f a2)
h4 : f a1 = f a2
⊢ a1 = a2

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