Theorem Proving in Lean 4, Exercise 4.6.2

Stream: new members

[Nathan]

variable (α : Type) (p q : α → Prop) variable (r : Prop) example : α → ((∀ x : α, r) ↔ r) := sorry

How do I solve this? λ h => ⟨λ hax => hax h, λ hr => λ _ => hr⟩ works, but I get an "unused variable" warning. Also, I don't understand the mathematical interpretation of this statement. If we were to say (∀ x ∈ S, r) ↔ r, this could be false if S were empty.

[Ruben Van de Velde]

The meaning is: "given some element of alpha, 'r is true for all elements of alpha' is equivalent to just 'r'"

[Nathan]

I guess my proof is correct then, but how do I avoid the warning?

[Ruben Van de Velde]

You can write a _ like you did at the end there

[Ruben Van de Velde]

Wait, where is the warning?

[Nathan]

Screenshot 2025-09-22 at 2.34.43 PM.png

[Ruben Van de Velde]

Oh, not in the proof. Yeah, you can replace the x by _

[Nathan]

thanks :)