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

State before:
A B C : Type
f : A → B
g : B → C
⊢ ∃ h, graph h = comp (graph g) (graph f)
Tactic:
set h : A → C := fun (x : A) => g (f x)
State after:
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
⊢ ∃ h, graph h = comp (graph g) (graph f)

State before:
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
⊢ ∃ h, graph h = comp (graph g) (graph f)
Tactic:
apply Exists.intro h
State after:
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
⊢ graph h = comp (graph g) (graph f)

State before:
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
⊢ graph h = comp (graph g) (graph f)
Tactic:
apply Set.ext
State after:
case h
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
⊢ ∀ (x : A × C), x ∈ graph h ↔ x ∈ comp (graph g) (graph f)

State before:
case h
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
⊢ ∀ (x : A × C), x ∈ graph h ↔ x ∈ comp (graph g) (graph f)
Tactic:
fix (a, c) : A × C
State after:
case h
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
⊢ (a, c) ∈ graph h ↔ (a, c) ∈ comp (graph g) (graph f)

State before:
case h
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
⊢ (a, c) ∈ graph h ↔ (a, c) ∈ comp (graph g) (graph f)
Tactic:
apply Iff.intro
State after:
case h.mp
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
⊢ (a, c) ∈ graph h → (a, c) ∈ comp (graph g) (graph f)

case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
⊢ (a, c) ∈ comp (graph g) (graph f) → (a, c) ∈ graph h

State before:
case h.mp
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
⊢ (a, c) ∈ graph h → (a, c) ∈ comp (graph g) (graph f)
Tactic:
assume h1 : (a, c) ∈ graph h
State after:
case h.mp
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : (a, c) ∈ graph h
⊢ (a, c) ∈ comp (graph g) (graph f)

State before:
case h.mp
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : (a, c) ∈ graph h
⊢ (a, c) ∈ comp (graph g) (graph f)
Tactic:
define at h1
State after:
case h.mp
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ (a, c) ∈ comp (graph g) (graph f)

State before:
case h.mp
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ (a, c) ∈ comp (graph g) (graph f)
Tactic:
define
State after:
case h.mp
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g

State before:
case h.mp
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
Tactic:
apply Exists.intro (f a)
State after:
case h.mp
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ (a, f a) ∈ graph f ∧ (f a, c) ∈ graph g

State before:
case h.mp
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ (a, f a) ∈ graph f ∧ (f a, c) ∈ graph g
Tactic:
apply And.intro
State after:
case h.mp.left
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ (a, f a) ∈ graph f

case h.mp.right
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ (f a, c) ∈ graph g

State before:
case h.mp.left
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ (a, f a) ∈ graph f
Tactic:
define
State after:
case h.mp.left
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ f a = f a

State before:
case h.mp.left
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ f a = f a
Tactic:
rfl
State after:
no goals

State before:
case h.mp.right
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ (f a, c) ∈ graph g
Tactic:
define
State after:
case h.mp.right
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ g (f a) = c

State before:
case h.mp.right
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : h a = c
⊢ g (f a) = c
Tactic:
show g (f a) = c from h1
State after:
no goals

State before:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
⊢ (a, c) ∈ comp (graph g) (graph f) → (a, c) ∈ graph h
Tactic:
assume h1 : (a, c) ∈ comp (graph g) (graph f)
State after:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : (a, c) ∈ comp (graph g) (graph f)
⊢ (a, c) ∈ graph h

State before:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : (a, c) ∈ comp (graph g) (graph f)
⊢ (a, c) ∈ graph h
Tactic:
define
State after:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : (a, c) ∈ comp (graph g) (graph f)
⊢ h a = c

State before:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : (a, c) ∈ comp (graph g) (graph f)
⊢ h a = c
Tactic:
define at h1
State after:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
⊢ h a = c

State before:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
⊢ h a = c
Tactic:
obtain (b : B) (h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g) from h1
State after:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
b : B
h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g
⊢ h a = c

State before:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
b : B
h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g
⊢ h a = c
Tactic:
have h3 : (a, b) ∈ graph f := h2.left
State after:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
b : B
h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g
h3 : (a, b) ∈ graph f
⊢ h a = c

State before:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
b : B
h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g
h3 : (a, b) ∈ graph f
⊢ h a = c
Tactic:
have h4 : (b, c) ∈ graph g := h2.right
State after:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
b : B
h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g
h3 : (a, b) ∈ graph f
h4 : (b, c) ∈ graph g
⊢ h a = c

State before:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
b : B
h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g
h3 : (a, b) ∈ graph f
h4 : (b, c) ∈ graph g
⊢ h a = c
Tactic:
define at h3
State after:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
b : B
h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g
h3 : f a = b
h4 : (b, c) ∈ graph g
⊢ h a = c

State before:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
b : B
h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g
h3 : f a = b
h4 : (b, c) ∈ graph g
⊢ h a = c
Tactic:
define at h4
State after:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
b : B
h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g
h3 : f a = b
h4 : g b = c
⊢ h a = c

State before:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
b : B
h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g
h3 : f a = b
h4 : g b = c
⊢ h a = c
Tactic:
rewrite [←h3] at h4
State after:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
b : B
h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g
h3 : f a = b
h4 : g (f a) = c
⊢ h a = c

State before:
case h.mpr
A B C : Type
f : A → B
g : B → C
h : A → C := fun x => g (f x)
a : A
c : C
h1 : ∃ x, (a, x) ∈ graph f ∧ (x, c) ∈ graph g
b : B
h2 : (a, b) ∈ graph f ∧ (b, c) ∈ graph g
h3 : f a = b
h4 : g (f a) = c
⊢ h a = c
Tactic:
show h a = c from h4
State after:
no goals