Theorem: HTPI.Theorem_4_2_5_4 (HTPILib/Chap4.lean)

State before:
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
⊢ comp T (comp S R) = comp (comp T S) R
Tactic:
apply Set.ext
State after:
case h
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
⊢ ∀ (x : A × D), x ∈ comp T (comp S R) ↔ x ∈ comp (comp T S) R

State before:
case h
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
⊢ ∀ (x : A × D), x ∈ comp T (comp S R) ↔ x ∈ comp (comp T S) R
Tactic:
fix (a, d) : A × D
State after:
case h
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
⊢ (a, d) ∈ comp T (comp S R) ↔ (a, d) ∈ comp (comp T S) R

State before:
case h
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
⊢ (a, d) ∈ comp T (comp S R) ↔ (a, d) ∈ comp (comp T S) R
Tactic:
apply Iff.intro
State after:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
⊢ (a, d) ∈ comp T (comp S R) → (a, d) ∈ comp (comp T S) R

case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
⊢ (a, d) ∈ comp (comp T S) R → (a, d) ∈ comp T (comp S R)

State before:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
⊢ (a, d) ∈ comp T (comp S R) → (a, d) ∈ comp (comp T S) R
Tactic:
assume h1 : (a, d) ∈ comp T (comp S R)
State after:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : (a, d) ∈ comp T (comp S R)
⊢ (a, d) ∈ comp (comp T S) R

State before:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : (a, d) ∈ comp T (comp S R)
⊢ (a, d) ∈ comp (comp T S) R
Tactic:
define
State after:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : (a, d) ∈ comp T (comp S R)
⊢ ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S

State before:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : (a, d) ∈ comp T (comp S R)
⊢ ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
Tactic:
define at h1
State after:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
⊢ ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S

State before:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
⊢ ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
Tactic:
obtain (c : C) (h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T) from h1
State after:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
⊢ ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S

State before:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
⊢ ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
Tactic:
have h3 : (a, c) ∈ comp S R := h2.left
State after:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
h3 : (a, c) ∈ comp S R
⊢ ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S

State before:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
h3 : (a, c) ∈ comp S R
⊢ ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
Tactic:
define at h3
State after:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
h3 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
⊢ ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S

State before:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
h3 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
⊢ ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
Tactic:
obtain (b : B) (h4 : (a, b) ∈ R ∧ (b, c) ∈ S) from h3
State after:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
h3 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
b : B
h4 : (a, b) ∈ R ∧ (b, c) ∈ S
⊢ ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S

State before:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
h3 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
b : B
h4 : (a, b) ∈ R ∧ (b, c) ∈ S
⊢ ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
Tactic:
apply Exists.intro b
State after:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
h3 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
b : B
h4 : (a, b) ∈ R ∧ (b, c) ∈ S
⊢ (a, b) ∈ R ∧ (b, d) ∈ comp T S

State before:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
h3 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
b : B
h4 : (a, b) ∈ R ∧ (b, c) ∈ S
⊢ (a, b) ∈ R ∧ (b, d) ∈ comp T S
Tactic:
apply And.intro h4.left
State after:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
h3 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
b : B
h4 : (a, b) ∈ R ∧ (b, c) ∈ S
⊢ (b, d) ∈ comp T S

State before:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
h3 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
b : B
h4 : (a, b) ∈ R ∧ (b, c) ∈ S
⊢ (b, d) ∈ comp T S
Tactic:
define
State after:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
h3 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
b : B
h4 : (a, b) ∈ R ∧ (b, c) ∈ S
⊢ ∃ x, (b, x) ∈ S ∧ (x, d) ∈ T

State before:
case h.mp
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
c : C
h2 : (a, c) ∈ comp S R ∧ (c, d) ∈ T
h3 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
b : B
h4 : (a, b) ∈ R ∧ (b, c) ∈ S
⊢ ∃ x, (b, x) ∈ S ∧ (x, d) ∈ T
Tactic:
show ∃ (x : C), (b, x) ∈ S ∧ (x, d) ∈ T from
  Exists.intro c (And.intro h4.right h2.right)
State after:
no goals

State before:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
⊢ (a, d) ∈ comp (comp T S) R → (a, d) ∈ comp T (comp S R)
Tactic:
assume h1 : (a, d) ∈ comp (comp T S) R
State after:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : (a, d) ∈ comp (comp T S) R
⊢ (a, d) ∈ comp T (comp S R)

State before:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : (a, d) ∈ comp (comp T S) R
⊢ (a, d) ∈ comp T (comp S R)
Tactic:
define
State after:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : (a, d) ∈ comp (comp T S) R
⊢ ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T

State before:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : (a, d) ∈ comp (comp T S) R
⊢ ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
Tactic:
define at h1
State after:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
⊢ ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T

State before:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
⊢ ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
Tactic:
obtain (b : B) (h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S) from h1
State after:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
⊢ ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T

State before:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
⊢ ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
Tactic:
have h3 : (b, d) ∈ comp T S := h2.right
State after:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
h3 : (b, d) ∈ comp T S
⊢ ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T

State before:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
h3 : (b, d) ∈ comp T S
⊢ ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
Tactic:
define at h3
State after:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
h3 : ∃ x, (b, x) ∈ S ∧ (x, d) ∈ T
⊢ ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T

State before:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
h3 : ∃ x, (b, x) ∈ S ∧ (x, d) ∈ T
⊢ ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
Tactic:
obtain (c : C) (h4 : (b, c) ∈ S ∧ (c, d) ∈ T) from h3
State after:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
h3 : ∃ x, (b, x) ∈ S ∧ (x, d) ∈ T
c : C
h4 : (b, c) ∈ S ∧ (c, d) ∈ T
⊢ ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T

State before:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
h3 : ∃ x, (b, x) ∈ S ∧ (x, d) ∈ T
c : C
h4 : (b, c) ∈ S ∧ (c, d) ∈ T
⊢ ∃ x, (a, x) ∈ comp S R ∧ (x, d) ∈ T
Tactic:
apply Exists.intro c
State after:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
h3 : ∃ x, (b, x) ∈ S ∧ (x, d) ∈ T
c : C
h4 : (b, c) ∈ S ∧ (c, d) ∈ T
⊢ (a, c) ∈ comp S R ∧ (c, d) ∈ T

State before:
case h.mpr
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
h3 : ∃ x, (b, x) ∈ S ∧ (x, d) ∈ T
c : C
h4 : (b, c) ∈ S ∧ (c, d) ∈ T
⊢ (a, c) ∈ comp S R ∧ (c, d) ∈ T
Tactic:
apply And.intro _ h4.right
State after:
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
h3 : ∃ x, (b, x) ∈ S ∧ (x, d) ∈ T
c : C
h4 : (b, c) ∈ S ∧ (c, d) ∈ T
⊢ (a, c) ∈ comp S R

State before:
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
h3 : ∃ x, (b, x) ∈ S ∧ (x, d) ∈ T
c : C
h4 : (b, c) ∈ S ∧ (c, d) ∈ T
⊢ (a, c) ∈ comp S R
Tactic:
define
State after:
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
h3 : ∃ x, (b, x) ∈ S ∧ (x, d) ∈ T
c : C
h4 : (b, c) ∈ S ∧ (c, d) ∈ T
⊢ ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S

State before:
A B C D : Type
R : Set (A × B)
S : Set (B × C)
T : Set (C × D)
a : A
d : D
h1 : ∃ x, (a, x) ∈ R ∧ (x, d) ∈ comp T S
b : B
h2 : (a, b) ∈ R ∧ (b, d) ∈ comp T S
h3 : ∃ x, (b, x) ∈ S ∧ (x, d) ∈ T
c : C
h4 : (b, c) ∈ S ∧ (c, d) ∈ T
⊢ ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
Tactic:
show ∃ (x : B), (a, x) ∈ R ∧ (x, c) ∈ S from
  Exists.intro b (And.intro h2.left h4.left)
State after:
no goals