Apply failed, don't know why and how to proceed

Stream: new members

[fkefjlwejlfk]

Hello guys, I am a noob and I seem to have a very simple problem I don't quite understand (lean 3):

constant x : Prop

def f : string -> bool
| "foo" := tt
| _ := ff

lemma proof_x : (∃ s : string, f s = tt -> x) -> x :=
begin
  intro h,
  apply h, -- error: invalid apply tactic, failed to unify x with ∃ (s : string), f s = tt → x
  sorry
end

In the lemma proof_x I begin by introducing hypothesis h: h : ∃ (s : string), f s = tt → x at this point my goal is x.
To me it seems like I should be able to apply h to get a goal of ∃ (s : string), f s = tt . However, it says the apply tactic failed to unify.
I have two questions:

1. Why is this happening? To me it seems that if I can construct a string such that f s = tt, I have proof of x by h. Why does lean not allow me to do this? Does it have to do with the existential quantifier?
2. What is the correct tactic / workflow to proceed here instead?

[Ruben Van de Velde]

Is your hypothesis (∃ s : string, f s = tt) -> x or ∃ s : string, (f s = tt -> x)?

[fkefjlwejlfk]

Ruben Van de Velde said:

Is your hypothesis (∃ s : string, f s = tt) -> x or ∃ s : string, (f s = tt -> x)?

Actually I think it is (∃ s : string, f s = tt -> x), does this imply the former? If that is the case, is this lemma still proveable?

[Kyle Miller]

∃ s : string, f s = tt -> x is true no matter what x is (for example, s = "" makes the implication vacuously true), so the lemma can't be true since would imply x no matter what x is.