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

State before:
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
⊢ matching (remove_one R u v) (A \ {u}) (B \ {v})
Tactic:
define
State after:
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
⊢ rel_within (remove_one R u v) (A \ {u}) (B \ {v}) ∧
    fcnl_on (remove_one R u v) (A \ {u}) ∧ fcnl_on (invRel (remove_one R u v)) (B \ {v})

State before:
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
⊢ rel_within (remove_one R u v) (A \ {u}) (B \ {v}) ∧
    fcnl_on (remove_one R u v) (A \ {u}) ∧ fcnl_on (invRel (remove_one R u v)) (B \ {v})
Tactic:
apply And.intro
State after:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
⊢ rel_within (remove_one R u v) (A \ {u}) (B \ {v})

case right
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
⊢ fcnl_on (remove_one R u v) (A \ {u}) ∧ fcnl_on (invRel (remove_one R u v)) (B \ {v})

State before:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
⊢ rel_within (remove_one R u v) (A \ {u}) (B \ {v})
Tactic:
define
State after:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
⊢ ∀ ⦃x : U⦄ ⦃y : V⦄, remove_one R u v x y → x ∈ A \ {u} ∧ y ∈ B \ {v}

State before:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
⊢ ∀ ⦃x : U⦄ ⦃y : V⦄, remove_one R u v x y → x ∈ A \ {u} ∧ y ∈ B \ {v}
Tactic:
fix x : U
State after:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
x : U
⊢ ∀ ⦃y : V⦄, remove_one R u v x y → x ∈ A \ {u} ∧ y ∈ B \ {v}

State before:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
x : U
⊢ ∀ ⦃y : V⦄, remove_one R u v x y → x ∈ A \ {u} ∧ y ∈ B \ {v}
Tactic:
fix y : V
State after:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
x : U
y : V
⊢ remove_one R u v x y → x ∈ A \ {u} ∧ y ∈ B \ {v}

State before:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
x : U
y : V
⊢ remove_one R u v x y → x ∈ A \ {u} ∧ y ∈ B \ {v}
Tactic:
assume h4 : remove_one R u v x y
State after:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
x : U
y : V
h4 : remove_one R u v x y
⊢ x ∈ A \ {u} ∧ y ∈ B \ {v}

State before:
case left
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
x : U
y : V
h4 : remove_one R u v x y
⊢ x ∈ A \ {u} ∧ y ∈ B \ {v}
Tactic:
show x ∈ A \ {u} ∧ y ∈ B \ {v} from remove_one_rel_within h1 h4
State after:
no goals

State before:
case right
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
⊢ fcnl_on (remove_one R u v) (A \ {u}) ∧ fcnl_on (invRel (remove_one R u v)) (B \ {v})
Tactic:
apply And.intro (remove_one_fcnl h1 h2 v)
State after:
case right
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
⊢ fcnl_on (invRel (remove_one R u v)) (B \ {v})

State before:
case right
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
⊢ fcnl_on (invRel (remove_one R u v)) (B \ {v})
Tactic:
rewrite [remove_one_inv]
State after:
case right
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
⊢ fcnl_on (remove_one (invRel R) v u) (B \ {v})

State before:
case right
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
v : V
h1 : matching R A B
h2 : u ∈ A
h3 : v ∈ B
⊢ fcnl_on (remove_one (invRel R) v u) (B \ {v})
Tactic:
show fcnl_on (remove_one (invRel R) v u) (B \ {v}) from
  remove_one_fcnl (inv_match h1) h3 u
State after:
no goals