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

State before:
U V W : Type
A : Set U
B : Set V
C : Set W
h1 : A ∼ B
h2 : B ∼ C
⊢ A ∼ C
Tactic:
obtain (R : Rel U V) (h3 : matching R A B) from h1
State after:
U V W : Type
A : Set U
B : Set V
C : Set W
h1 : A ∼ B
h2 : B ∼ C
R : Rel U V
h3 : matching R A B
⊢ A ∼ C

State before:
U V W : Type
A : Set U
B : Set V
C : Set W
h1 : A ∼ B
h2 : B ∼ C
R : Rel U V
h3 : matching R A B
⊢ A ∼ C
Tactic:
obtain (S : Rel V W) (h4 : matching S B C) from h2
State after:
U V W : Type
A : Set U
B : Set V
C : Set W
h1 : A ∼ B
h2 : B ∼ C
R : Rel U V
h3 : matching R A B
S : Rel V W
h4 : matching S B C
⊢ A ∼ C

State before:
U V W : Type
A : Set U
B : Set V
C : Set W
h1 : A ∼ B
h2 : B ∼ C
R : Rel U V
h3 : matching R A B
S : Rel V W
h4 : matching S B C
⊢ A ∼ C
Tactic:
apply Exists.intro (compRel S R)
State after:
U V W : Type
A : Set U
B : Set V
C : Set W
h1 : A ∼ B
h2 : B ∼ C
R : Rel U V
h3 : matching R A B
S : Rel V W
h4 : matching S B C
⊢ matching (compRel S R) A C

State before:
U V W : Type
A : Set U
B : Set V
C : Set W
h1 : A ∼ B
h2 : B ∼ C
R : Rel U V
h3 : matching R A B
S : Rel V W
h4 : matching S B C
⊢ matching (compRel S R) A C
Tactic:
show matching (compRel S R) A C from comp_match h3 h4
State after:
no goals