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

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

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

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

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

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

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

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

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

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

State before:
case h.mp
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
b : B
h2 : (a, b) ∈ R ∧ (b, c) ∈ S
⊢ (c, b) ∈ inv S ∧ (b, a) ∈ inv R
Tactic:
rewrite [inv_def, inv_def]
State after:
case h.mp
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (a, x) ∈ R ∧ (x, c) ∈ S
b : B
h2 : (a, b) ∈ R ∧ (b, c) ∈ S
⊢ (b, c) ∈ S ∧ (a, b) ∈ R

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

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

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

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

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

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

State before:
case h.mpr
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (c, x) ∈ inv S ∧ (x, a) ∈ inv R
b : B
h2 : (c, b) ∈ inv S ∧ (b, a) ∈ inv R
⊢ (a, b) ∈ R ∧ (b, c) ∈ S
Tactic:
rewrite [inv_def, inv_def] at h2
State after:
case h.mpr
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (c, x) ∈ inv S ∧ (x, a) ∈ inv R
b : B
h2 : (b, c) ∈ S ∧ (a, b) ∈ R
⊢ (a, b) ∈ R ∧ (b, c) ∈ S

State before:
case h.mpr
A B C : Type
R : Set (A × B)
S : Set (B × C)
c : C
a : A
h1 : ∃ x, (c, x) ∈ inv S ∧ (x, a) ∈ inv R
b : B
h2 : (b, c) ∈ S ∧ (a, b) ∈ R
⊢ (a, b) ∈ R ∧ (b, c) ∈ S
Tactic:
show (a, b) ∈ R ∧ (b, c) ∈ S from And.intro h2.right h2.left
State after:
no goals