Theorem: HTPI.Theorem_8_1_2_1 (HTPILib/Chap8Part2.lean)

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

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

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

State before:
U V W X : Type
A : Set U
B : Set V
C : Set W
D : Set X
h1 : A ∼ B
h2 : C ∼ D
R : Rel U V
h3 : matching R A B
S : Rel W X
h4 : matching S C D
⊢ matching (R ×ᵣ S) (A ×ₛ C) (B ×ₛ D)
Tactic:
show matching (R ×ᵣ S) (A ×ₛ C) (B ×ₛ D) from prod_match h3 h4
State after:
no goals