How to do it proprely in lean

Stream: new members

[T.X. XIA]

Hi. I'm new to lean and am recently reading Theorem Proving in Lean 4.

I was trying to solve the problem in the exercise of Quantifiers and Equality and ended up using three 'byContradiction' in a row.
So I'm wondering is it the right way to do it?

And by the way, I would like to know how can we check out the standard library so as to learn how to use it? I know that there is a manual but, for example, when I wanted to look at what's in the Classical, I couldn't find it in the manual or in VS Code.

example : (∃ x, p x) ↔ ¬ (∀ x, ¬ p x) :=
  Iff.intro
    (fun ⟨x, hpx⟩ h => h x hpx)
    (fun h => byContradiction (fun hne : ¬(∃ x, p x) =>
      have := (fun x => byContradiction (fun hh : ¬¬ p x =>
        have := byContradiction (fun hnpx : ¬ p x => hh hnpx)
        show False from hne ⟨x, this⟩
        ))
      absurd this h
    ))