simple propositional logic exercises

Stream: new members

[dearoneesama]

Hi everyone! I just picked up Lean a few days ago and now I am staring at one exercise without clue how to go forward.

example : ¬(p → q) → p ∧ ¬q :=
  λ h1,
    or.elim (em p)
      (λ hp,
        suffices hnq : ¬q, from and.intro hp hnq,
        λ hq : q, h1 (λ hp_, hq))
      (λ hnp, sorry)

for the other λ hnp: ¬p, part, I don't know what to do since i think i need p ∧ ¬q to get it working. but i already have ¬p!

i think as long as i use (em p).elim on the Prop which appears in the conclusion, i am stuck, like this:

example : (((p → q) → p) → p) :=
  λ h1 : ((p → q) → p),
    or.elim (em p)
      id
      (λ hnp, sorry)

[Ruben Van de Velde]

No, you're on the right path. You can prove p -> q in that branch, and finish from there