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

State before:
U V : Type
A : Set U
B : Set V
u : U
v : V
h1 : A ∼ B
h2 : u ∈ A
h3 : v ∈ B
⊢ A \ {u} ∼ B \ {v}
Tactic:
define
State after:
U V : Type
A : Set U
B : Set V
u : U
v : V
h1 : A ∼ B
h2 : u ∈ A
h3 : v ∈ B
⊢ ∃ R, matching R (A \ {u}) (B \ {v})

State before:
U V : Type
A : Set U
B : Set V
u : U
v : V
h1 : A ∼ B
h2 : u ∈ A
h3 : v ∈ B
⊢ ∃ R, matching R (A \ {u}) (B \ {v})
Tactic:
obtain (R : Rel U V) (h4 : matching R A B) from h1
State after:
U V : Type
A : Set U
B : Set V
u : U
v : V
h1 : A ∼ B
h2 : u ∈ A
h3 : v ∈ B
R : Rel U V
h4 : matching R A B
⊢ ∃ R, matching R (A \ {u}) (B \ {v})

State before:
U V : Type
A : Set U
B : Set V
u : U
v : V
h1 : A ∼ B
h2 : u ∈ A
h3 : v ∈ B
R : Rel U V
h4 : matching R A B
⊢ ∃ R, matching R (A \ {u}) (B \ {v})
Tactic:
apply Exists.intro (remove_one R u v)
State after:
U V : Type
A : Set U
B : Set V
u : U
v : V
h1 : A ∼ B
h2 : u ∈ A
h3 : v ∈ B
R : Rel U V
h4 : matching R A B
⊢ matching (remove_one R u v) (A \ {u}) (B \ {v})

State before:
U V : Type
A : Set U
B : Set V
u : U
v : V
h1 : A ∼ B
h2 : u ∈ A
h3 : v ∈ B
R : Rel U V
h4 : matching R A B
⊢ matching (remove_one R u v) (A \ {u}) (B \ {v})
Tactic:
show matching (remove_one R u v) (A \ {u}) (B \ {v}) from
  remove_one_match h4 h2 h3
State after:
no goals