Theorem: HTPI.comp_match (HTPILib/Chap8Part1.lean)

State before:
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
⊢ matching (compRel S R) A C
Tactic:
define
State after:
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
⊢ rel_within (compRel S R) A C ∧ fcnl_on (compRel S R) A ∧ fcnl_on (invRel (compRel S R)) C

State before:
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
⊢ rel_within (compRel S R) A C ∧ fcnl_on (compRel S R) A ∧ fcnl_on (invRel (compRel S R)) C
Tactic:
apply And.intro
State after:
case left
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
⊢ rel_within (compRel S R) A C

case right
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
⊢ fcnl_on (compRel S R) A ∧ fcnl_on (invRel (compRel S R)) C

State before:
case left
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
⊢ rel_within (compRel S R) A C
Tactic:
define
State after:
case left
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
⊢ ∀ ⦃x : U⦄ ⦃y : W⦄, compRel S R x y → x ∈ A ∧ y ∈ C

State before:
case left
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
⊢ ∀ ⦃x : U⦄ ⦃y : W⦄, compRel S R x y → x ∈ A ∧ y ∈ C
Tactic:
fix a : U
State after:
case left
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
a : U
⊢ ∀ ⦃y : W⦄, compRel S R a y → a ∈ A ∧ y ∈ C

State before:
case left
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
a : U
⊢ ∀ ⦃y : W⦄, compRel S R a y → a ∈ A ∧ y ∈ C
Tactic:
fix c : W
State after:
case left
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
a : U
c : W
⊢ compRel S R a c → a ∈ A ∧ c ∈ C

State before:
case left
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
a : U
c : W
⊢ compRel S R a c → a ∈ A ∧ c ∈ C
Tactic:
assume h3 : compRel S R a c
State after:
case left
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
a : U
c : W
h3 : compRel S R a c
⊢ a ∈ A ∧ c ∈ C

State before:
case left
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
a : U
c : W
h3 : compRel S R a c
⊢ a ∈ A ∧ c ∈ C
Tactic:
rewrite [compRel_def] at h3
State after:
case left
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
a : U
c : W
h3 : ∃ x, R a x ∧ S x c
⊢ a ∈ A ∧ c ∈ C

State before:
case left
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
a : U
c : W
h3 : ∃ x, R a x ∧ S x c
⊢ a ∈ A ∧ c ∈ C
Tactic:
obtain (b : V) (h4 : R a b ∧ S b c) from h3
State after:
case left
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
a : U
c : W
h3 : ∃ x, R a x ∧ S x c
b : V
h4 : R a b ∧ S b c
⊢ a ∈ A ∧ c ∈ C

State before:
case left
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
a : U
c : W
h3 : ∃ x, R a x ∧ S x c
b : V
h4 : R a b ∧ S b c
⊢ a ∈ A ∧ c ∈ C
Tactic:
have h5 : a ∈ A ∧ b ∈ B := h1.left h4.left
State after:
case left
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
a : U
c : W
h3 : ∃ x, R a x ∧ S x c
b : V
h4 : R a b ∧ S b c
h5 : a ∈ A ∧ b ∈ B
⊢ a ∈ A ∧ c ∈ C

State before:
case left
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
a : U
c : W
h3 : ∃ x, R a x ∧ S x c
b : V
h4 : R a b ∧ S b c
h5 : a ∈ A ∧ b ∈ B
⊢ a ∈ A ∧ c ∈ C
Tactic:
have h6 : b ∈ B ∧ c ∈ C := h2.left h4.right
State after:
case left
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
a : U
c : W
h3 : ∃ x, R a x ∧ S x c
b : V
h4 : R a b ∧ S b c
h5 : a ∈ A ∧ b ∈ B
h6 : b ∈ B ∧ c ∈ C
⊢ a ∈ A ∧ c ∈ C

State before:
case left
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
a : U
c : W
h3 : ∃ x, R a x ∧ S x c
b : V
h4 : R a b ∧ S b c
h5 : a ∈ A ∧ b ∈ B
h6 : b ∈ B ∧ c ∈ C
⊢ a ∈ A ∧ c ∈ C
Tactic:
show a ∈ A ∧ c ∈ C from And.intro h5.left h6.right
State after:
no goals

State before:
case right
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
⊢ fcnl_on (compRel S R) A ∧ fcnl_on (invRel (compRel S R)) C
Tactic:
apply And.intro
State after:
case right.left
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
⊢ fcnl_on (compRel S R) A

case right.right
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
⊢ fcnl_on (invRel (compRel S R)) C

State before:
case right.left
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
⊢ fcnl_on (compRel S R) A
Tactic:
show fcnl_on (compRel S R) A from comp_fcnl h1 h2
State after:
no goals

State before:
case right.right
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
⊢ fcnl_on (invRel (compRel S R)) C
Tactic:
rewrite [inv_comp]
State after:
case right.right
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
⊢ fcnl_on (compRel (invRel R) (invRel S)) C

State before:
case right.right
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
⊢ fcnl_on (compRel (invRel R) (invRel S)) C
Tactic:
have h3 : matching (invRel R) B A := inv_match h1
State after:
case right.right
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
h3 : matching (invRel R) B A
⊢ fcnl_on (compRel (invRel R) (invRel S)) C

State before:
case right.right
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
h3 : matching (invRel R) B A
⊢ fcnl_on (compRel (invRel R) (invRel S)) C
Tactic:
have h4 : matching (invRel S) C B := inv_match h2
State after:
case right.right
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
h3 : matching (invRel R) B A
h4 : matching (invRel S) C B
⊢ fcnl_on (compRel (invRel R) (invRel S)) C

State before:
case right.right
U V W : Type
R : Rel U V
S : Rel V W
A : Set U
B : Set V
C : Set W
h1 : matching R A B
h2 : matching S B C
h3 : matching (invRel R) B A
h4 : matching (invRel S) C B
⊢ fcnl_on (compRel (invRel R) (invRel S)) C
Tactic:
show fcnl_on (compRel (invRel R) (invRel S)) C from comp_fcnl h4 h3
State after:
no goals