# How can I instantiate a variable in an existential quantifier in apply style

From Isabelle Community Wiki

Sometimes, it is necessary to instantiate an existentially quantified variable in by hand.

Using `rule_tac`

, it is possible to specify the desired instantiation by hand.

lemma "∃ x. x = 3" apply(rule_tac x="3" in exI) apply simp done

## Hints

Using apply style is considered deprecated and should be avoided. Using Isar, the `obtain`

keyword is available.

lemma "∃ x. x = 3" proof - obtain y :: nat where "y = 3" by simp hence "∃ x. x = 3" using exI[where x="y"] by simp thus ?thesis . qed

The `using exI[where x="y"]`

can be omitted.