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

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

State before:
U V : Type
A : Set U
B : Set V
h : A ∼ B
R : Rel U V
h1 : matching R A B
⊢ B ∼ A
Tactic:
apply Exists.intro (invRel R)
State after:
U V : Type
A : Set U
B : Set V
h : A ∼ B
R : Rel U V
h1 : matching R A B
⊢ matching (invRel R) B A

State before:
U V : Type
A : Set U
B : Set V
h : A ∼ B
R : Rel U V
h1 : matching R A B
⊢ matching (invRel R) B A
Tactic:
show matching (invRel R) B A from inv_match h1
State after:
no goals