have h61:= h60 h14 doesn't work as expected

Stream: new members

[Michael Beeson]

In tactic mode I write
have h61:= h60 h14 ,
and I do not get any error message nor do I get a new hypothesis h61. My proof state is below.
Actually, further experimentation shows I can't do ANYTHING in this proof state. Lean is unresponsive.
So I guess the specific proof state below won't be helpful.

solve1 tactic failed, focused goal has not been solved
state:
M : Type,
_inst_1 : Model M,
Y a : M,
h2 : ¬a ∈ Y,
h3 : Y ∈ FINITE M,
h4copy : ∀ (Y_1 : M), Y_1 ⊆ Y → separable_subset M Y_1 Y → Y_1 ∈ FINITE M,
U : M,
h5 : U ⊆ Y ∪ single a,
h4 : U ⊆ Y → separable_subset M U Y → U ∈ FINITE M,
h7 : U ⊆ Y ∪ single a,
h8copy : ∀ (z : M), z ∈ Y ∪ single a → z ∈ U ∨ ¬z ∈ U,
h8 : a ∈ Y ∪ single a → a ∈ U ∨ ¬a ∈ U,
h9 : a ∈ Y ∪ single a,
h11 : a ∈ U,
V : M := U - single a,
h13 : V = U - single a,
h60 : V ⊆ Y → separable_subset M V Y → V ∈ FINITE M,
h14 : V ⊆ Y,
h18 : separable_subset M V Y
⊢ U ∈ FINITE M