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

State before:
U V : Type
R : Rel U V
A : Set U
B : Set V
h : matching R A B
⊢ matching (invRel R) B A
Tactic:
define
State after:
U V : Type
R : Rel U V
A : Set U
B : Set V
h : matching R A B
⊢ rel_within (invRel R) B A ∧ fcnl_on (invRel R) B ∧ fcnl_on (invRel (invRel R)) A

State before:
U V : Type
R : Rel U V
A : Set U
B : Set V
h : matching R A B
⊢ rel_within (invRel R) B A ∧ fcnl_on (invRel R) B ∧ fcnl_on (invRel (invRel R)) A
Tactic:
define at h
State after:
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
⊢ rel_within (invRel R) B A ∧ fcnl_on (invRel R) B ∧ fcnl_on (invRel (invRel R)) A

State before:
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
⊢ rel_within (invRel R) B A ∧ fcnl_on (invRel R) B ∧ fcnl_on (invRel (invRel R)) A
Tactic:
apply And.intro
State after:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
⊢ rel_within (invRel R) B A

case right
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
⊢ fcnl_on (invRel R) B ∧ fcnl_on (invRel (invRel R)) A

State before:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
⊢ rel_within (invRel R) B A
Tactic:
define
State after:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
⊢ ∀ ⦃x : V⦄ ⦃y : U⦄, invRel R x y → x ∈ B ∧ y ∈ A

State before:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
⊢ ∀ ⦃x : V⦄ ⦃y : U⦄, invRel R x y → x ∈ B ∧ y ∈ A
Tactic:
fix y : V
State after:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
y : V
⊢ ∀ ⦃y_1 : U⦄, invRel R y y_1 → y ∈ B ∧ y_1 ∈ A

State before:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
y : V
⊢ ∀ ⦃y_1 : U⦄, invRel R y y_1 → y ∈ B ∧ y_1 ∈ A
Tactic:
fix x : U
State after:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
y : V
x : U
⊢ invRel R y x → y ∈ B ∧ x ∈ A

State before:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
y : V
x : U
⊢ invRel R y x → y ∈ B ∧ x ∈ A
Tactic:
assume h1 : invRel R y x
State after:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
y : V
x : U
h1 : invRel R y x
⊢ y ∈ B ∧ x ∈ A

State before:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
y : V
x : U
h1 : invRel R y x
⊢ y ∈ B ∧ x ∈ A
Tactic:
define at h1
State after:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
y : V
x : U
h1 : R x y
⊢ y ∈ B ∧ x ∈ A

State before:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
y : V
x : U
h1 : R x y
⊢ y ∈ B ∧ x ∈ A
Tactic:
have h2 : x ∈ A ∧ y ∈ B := h.left h1
State after:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
y : V
x : U
h1 : R x y
h2 : x ∈ A ∧ y ∈ B
⊢ y ∈ B ∧ x ∈ A

State before:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
y : V
x : U
h1 : R x y
h2 : x ∈ A ∧ y ∈ B
⊢ y ∈ B ∧ x ∈ A
Tactic:
show y ∈ B ∧ x ∈ A from And.intro h2.right h2.left
State after:
no goals

State before:
case right
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
⊢ fcnl_on (invRel R) B ∧ fcnl_on (invRel (invRel R)) A
Tactic:
rewrite [inv_inv]
State after:
case right
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
⊢ fcnl_on (invRel R) B ∧ fcnl_on R A

State before:
case right
U V : Type
R : Rel U V
A : Set U
B : Set V
h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
⊢ fcnl_on (invRel R) B ∧ fcnl_on R A
Tactic:
show fcnl_on (invRel R) B ∧ fcnl_on R A from
  And.intro h.right.right h.right.left
State after:
no goals