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

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

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

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

State before:
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : matching R A B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
⊢ ∃! y, remove_one R u v x y
Tactic:
obtain (w : U) (h4 : w ∈ A ∧ ∀ (y : V),
  remove_one R u v x y ↔ R w y) from remove_one_iff h1 h2 v h3
State after:
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : matching R A B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
⊢ ∃! y, remove_one R u v x y

State before:
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : matching R A B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
⊢ ∃! y, remove_one R u v x y
Tactic:
define at h1
State after:
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
⊢ ∃! y, remove_one R u v x y

State before:
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
⊢ ∃! y, remove_one R u v x y
Tactic:
exists_unique
State after:
case Existence
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
⊢ ∃ y, remove_one R u v x y

case Uniqueness
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
⊢ ∀ (y_1 y_2 : V), remove_one R u v x y_1 → remove_one R u v x y_2 → y_1 = y_2

State before:
case Existence
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
⊢ ∃ y, remove_one R u v x y
Tactic:
obtain (y : V) (h5 : R w y) from fcnl_exists h1.right.left h4.left
State after:
case Existence
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y : V
h5 : R w y
⊢ ∃ y, remove_one R u v x y

State before:
case Existence
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y : V
h5 : R w y
⊢ ∃ y, remove_one R u v x y
Tactic:
apply Exists.intro y
State after:
case Existence
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y : V
h5 : R w y
⊢ remove_one R u v x y

State before:
case Existence
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y : V
h5 : R w y
⊢ remove_one R u v x y
Tactic:
rewrite [h4.right]
State after:
case Existence
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y : V
h5 : R w y
⊢ R w y

State before:
case Existence
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y : V
h5 : R w y
⊢ R w y
Tactic:
show R w y from h5
State after:
no goals

State before:
case Uniqueness
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
⊢ ∀ (y_1 y_2 : V), remove_one R u v x y_1 → remove_one R u v x y_2 → y_1 = y_2
Tactic:
fix y1 : V
State after:
case Uniqueness
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y1 : V
⊢ ∀ (y_2 : V), remove_one R u v x y1 → remove_one R u v x y_2 → y1 = y_2

State before:
case Uniqueness
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y1 : V
⊢ ∀ (y_2 : V), remove_one R u v x y1 → remove_one R u v x y_2 → y1 = y_2
Tactic:
fix y2 : V
State after:
case Uniqueness
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y1 y2 : V
⊢ remove_one R u v x y1 → remove_one R u v x y2 → y1 = y2

State before:
case Uniqueness
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y1 y2 : V
⊢ remove_one R u v x y1 → remove_one R u v x y2 → y1 = y2
Tactic:
rewrite [h4.right, h4.right]
State after:
case Uniqueness
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y1 y2 : V
⊢ R w y1 → R w y2 → y1 = y2

State before:
case Uniqueness
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y1 y2 : V
⊢ R w y1 → R w y2 → y1 = y2
Tactic:
assume h5 : R w y1
State after:
case Uniqueness
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y1 y2 : V
h5 : R w y1
⊢ R w y2 → y1 = y2

State before:
case Uniqueness
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y1 y2 : V
h5 : R w y1
⊢ R w y2 → y1 = y2
Tactic:
assume h6 : R w y2
State after:
case Uniqueness
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y1 y2 : V
h5 : R w y1
h6 : R w y2
⊢ y1 = y2

State before:
case Uniqueness
U V : Type
R : Rel U V
A : Set U
B : Set V
u : U
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : u ∈ A
v : V
x : U
h3 : x ∈ A \ {u}
w : U
h4 : w ∈ A ∧ ∀ (y : V), remove_one R u v x y ↔ R w y
y1 y2 : V
h5 : R w y1
h6 : R w y2
⊢ y1 = y2
Tactic:
show y1 = y2 from fcnl_unique h1.right.left h4.left h5 h6
State after:
no goals