Proof approach guidance?

Stream: general

[Dominic Farolino]

I'm working on completing example: (∃ x, r → p x) ↔ (r → ∃ x, p x) := sorry, from Chapter 4, section 4, in the Theorem Proving in Lean book. So far what I have is:

example: (∃ x, r → p x) ↔ (r → ∃ x, p x) :=
  iff.intro
    (assume h: (∃ x, r → p x),
      assume hr: r,
      show ∃ x, p x, from
      exists.elim h
        (assume y: α,
          assume hinner: r → p y,
          have hpy: p y, from hinner hr,
          exists.intro y hpy
        )
    )
    (assume h: (r → ∃ x, p x),
      show (∃ x, r → p x), from
      by_cases
        (assume hc: r,
          exists.elim (h hc)
          (assume y: α,
            assume hinner: p y,
            have hcom: r → p y, from sorry,
            show (∃ x, r → p x), from exists.intro y hcom
          )
        )
        (assume hc: ¬ r, sorry)
    )

But I cannot figure out what to put in place of the first sorry (I haven't even looked at how to prove this with a proof of not r, which worries me a bit). Thoughts/suggested direction?

[Mario Carneiro]

there is a (a : \alpha) assumption in the book

[Mario Carneiro]

you have to know that the quantification domain is nonempty to prove this one

[Mario Carneiro]

for the first sorry, you can assume r, ignore the assumption and then use hinner

[Dominic Farolino]

Thanks for taking a look. Ok, your advice worked for the first sorry. It kind of confuses me why I have to re-assume r, since I have already assumed it in the form of hc, and I believe I have not "used" it at the the first sorry is evaluated.

For the second sorry, my intuition tells me that I can get r from not r, by somehow using the fact that the quantification domain is non-empty, and then just basically repeating the exists.elim (...)

[Dominic Farolino]

that is proving difficult though..

[Mario Carneiro]

we have to assume r because that's how you prove an implication

[Dominic Farolino]

Oh, duh, thanks

[Mario Carneiro]

for the second sorry, you are trying to prove ∃ x, r → p x assuming not r, and so any x will do, since not r and r imply p x

[Mario Carneiro]

so you use that the quantification domain is nonempty to take some x and use that

[Dominic Farolino]

Wow, I got it :) My assume block ended up like

(assume hc: ¬ r,
          show (∃ x, r → p x), from
            exists.intro a (assume hr: r, absurd hr hc)
)

[Dominic Farolino]

(minus the weird spacing that didn't translate well). Still a little funny to me why it works, I feel like we're assuming that r somehow "for free", but the overall bit makes sense to me

[Mario Carneiro]

it's a bit of a weird theorem. It says that there is an element such that either r is false or p x holds

[Mario Carneiro]

when r is false that's easy to prove