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

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

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

State before:
A B C : Type
f : A → B
g : B → C
h1 : onto f
h2 : onto g
⊢ onto (g ∘ f)
Tactic:
define at h1
State after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : onto g
⊢ onto (g ∘ f)

State before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : onto g
⊢ onto (g ∘ f)
Tactic:
define at h2
State after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
⊢ onto (g ∘ f)

State before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
⊢ onto (g ∘ f)
Tactic:
define
State after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
⊢ ∀ (y : C), ∃ x, (g ∘ f) x = y

State before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
⊢ ∀ (y : C), ∃ x, (g ∘ f) x = y
Tactic:
fix c : C
State after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
c : C
⊢ ∃ x, (g ∘ f) x = c

State before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
c : C
⊢ ∃ x, (g ∘ f) x = c
Tactic:
obtain (b : B) (h3 : g b = c) from h2 c
State after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
c : C
b : B
h3 : g b = c
⊢ ∃ x, (g ∘ f) x = c

State before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
c : C
b : B
h3 : g b = c
⊢ ∃ x, (g ∘ f) x = c
Tactic:
obtain (a : A) (h4 : f a = b) from h1 b
State after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
c : C
b : B
h3 : g b = c
a : A
h4 : f a = b
⊢ ∃ x, (g ∘ f) x = c

State before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
c : C
b : B
h3 : g b = c
a : A
h4 : f a = b
⊢ ∃ x, (g ∘ f) x = c
Tactic:
apply Exists.intro a
State after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
c : C
b : B
h3 : g b = c
a : A
h4 : f a = b
⊢ (g ∘ f) a = c

State before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
c : C
b : B
h3 : g b = c
a : A
h4 : f a = b
⊢ (g ∘ f) a = c
Tactic:
rewrite [comp_def]
State after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
c : C
b : B
h3 : g b = c
a : A
h4 : f a = b
⊢ g (f a) = c

State before:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
c : C
b : B
h3 : g b = c
a : A
h4 : f a = b
⊢ g (f a) = c
Tactic:
rewrite [←h4] at h3
State after:
A B C : Type
f : A → B
g : B → C
h1 : ∀ (y : B), ∃ x, f x = y
h2 : ∀ (y : C), ∃ x, g x = y
c : C
b : B
a : A
h3 : g (f a) = c
h4 : f a = b
⊢ g (f a) = c

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