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

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

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

State before:
U V : Type
R : Rel U V
A : Set U
B : Set V
x u : U
y v : V
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y)
h3 : x ∈ A ∧ y ∈ B
⊢ x ∈ A \ {u} ∧ y ∈ B \ {v}
Tactic:
show x ∈ A \ {u} ∧ y ∈ B \ {v} from
  And.intro (And.intro h3.left h2.left) (And.intro h3.right h2.right.left)
State after:
no goals

State before:
U V : Type
R : Rel U V
A : Set U
B : Set V
x u : U
y v : V
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y)
⊢ x ∈ A ∧ y ∈ B
Tactic:
by_cases on h2.right.right with h3
State after:
case Case_1
U V : Type
R : Rel U V
A : Set U
B : Set V
x u : U
y v : V
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y)
h3 : R x y
⊢ x ∈ A ∧ y ∈ B

case Case_2
U V : Type
R : Rel U V
A : Set U
B : Set V
x u : U
y v : V
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y)
h3 : R x v ∧ R u y
⊢ x ∈ A ∧ y ∈ B

State before:
case Case_1
U V : Type
R : Rel U V
A : Set U
B : Set V
x u : U
y v : V
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y)
h3 : R x y
⊢ x ∈ A ∧ y ∈ B
Tactic:
show x ∈ A ∧ y ∈ B from h1.left h3
State after:
no goals

State before:
case Case_2
U V : Type
R : Rel U V
A : Set U
B : Set V
x u : U
y v : V
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y)
h3 : R x v ∧ R u y
⊢ x ∈ A ∧ y ∈ B
Tactic:
have h4 : x ∈ A ∧ v ∈ B := h1.left h3.left
State after:
case Case_2
U V : Type
R : Rel U V
A : Set U
B : Set V
x u : U
y v : V
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y)
h3 : R x v ∧ R u y
h4 : x ∈ A ∧ v ∈ B
⊢ x ∈ A ∧ y ∈ B

State before:
case Case_2
U V : Type
R : Rel U V
A : Set U
B : Set V
x u : U
y v : V
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y)
h3 : R x v ∧ R u y
h4 : x ∈ A ∧ v ∈ B
⊢ x ∈ A ∧ y ∈ B
Tactic:
have h5 : u ∈ A ∧ y ∈ B := h1.left h3.right
State after:
case Case_2
U V : Type
R : Rel U V
A : Set U
B : Set V
x u : U
y v : V
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y)
h3 : R x v ∧ R u y
h4 : x ∈ A ∧ v ∈ B
h5 : u ∈ A ∧ y ∈ B
⊢ x ∈ A ∧ y ∈ B

State before:
case Case_2
U V : Type
R : Rel U V
A : Set U
B : Set V
x u : U
y v : V
h1 : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
h2 : x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y)
h3 : R x v ∧ R u y
h4 : x ∈ A ∧ v ∈ B
h5 : u ∈ A ∧ y ∈ B
⊢ x ∈ A ∧ y ∈ B
Tactic:
show x ∈ A ∧ y ∈ B from And.intro h4.left h5.right
State after:
no goals