New Member question about "Theorem Proving in Lean

Stream: lean4

[kvanvels]

Please forgive me if this is an inappropriate spot for this question.

I am working through the "Theorem Proving in Lean" for Lean 4 and I would appreciate hint on how to prove the following example (without using tactics)

variable (p : Prop)
example : p ∨ ¬p :=

I can do this using tactics as follows:

open Classical
variable (p : Prop)
example : p ∨ ¬p := by
  apply Or.elim (em p)
  intro hp
  exact Or.inl hp
  intro hnp
  exact Or.inr hnp

I have attempted to ape this proof as follows

variable (p : Prop)
open Classical
example : p ∨ ¬p :=
    fun ( p : Prop ) =>
      (Or.elim (em p)
        (fun hp : p => Or.inl hp)
        (fun hnp : ¬p => Or.inr hnp)
      )

or

variable (p : Prop)
open Classical
example : p ∨ ¬p :=
      (Or.elim (em p)
        (fun hp : p => Or.inl hp)
        (fun hnp : ¬p => Or.inr hnp)
      )

I appreciate any suggestions/help.

Kent

[Henrik Böving]

first things first there is actually an even easier way^^

example : p ∨ ¬p := by exact em p

or alternatively

example : p ∨ ¬p := em p

which is equivalent

Now the first term mode proof you tried doesn't work because of the fun you only have to do that if you are working with an implication if you have a variable that binds some value you can already pretend that you have automatically written this statement basically. The second proof is correct though and my Lean accepts it, what is wrong about it?

[kvanvels]

Thanks for the fast response. I copied and pasted my second solution into a different file and the error goes away. I need to investigate more. I suspect a different function was messing it up. I was getting the following error on the "Or.elim (em p)" line.

function expected at
  Or.elim (em p) (fun hp => Or.inl hp) fun hnp => Or.inr hnp
term has type
  p ∨ ¬p

[kvanvels]

There was an underscore hiding at the end of the file. The error went away. Thanks again.

[kvanvels]

I am trying to prove the following exercise (trimmed down version) of an exercise in "Theorem proving in Lean". I have posted my best approach. I

open Classical

variable (α : Type) (p q : α → Prop)
variable (r : Prop)

example (a : α) :  ((∀ x, p x) → r)  → (∃ x, p x → r) :=
(fun h : (∀ x, p x) → r =>
  suffices h2 : p a → r from Exists.intro a h2
  fun h3 : p a =>
  suffices h4 : (∀ (x : α), p x) from (h h4)
  fun x => _ --don't know what I should do here.
 )

I need to show (p x) and have (p a) for every a in α. So this should be sufficient. How do I tell lean4 to notice this? Any help will be appreciated.

There is some discussion about this in the tutorial, (there is a paragraph that reads : As was the case for implication, the propositions-as-types interpretation now comes into play. Remember the introduction and elimination rules for dependent arrow types: and then an example but I can't see how to use it)

[Kevin Buzzard]

(this question is now being discussed here)