Section 5 Solutions – Theorem Proving in Lean 4

example (p q r : Prop) (hp : p)
  : (p ∨ q ∨ r) ∧ (q ∨ p ∨ r) ∧ (q ∨ r ∨ p) := by
        apply And.intro
        apply Or.inl
        exact hp
        apply And.intro
        apply Or.inr
        apply Or.inl
        exact hp
        apply Or.inr
        apply Or.inr
        exact hp

Add a comment

You must log in to post a comment.

Site Maintenance

Our platform is currently undergoing maintenance. We apologize for any inconvenience. Please check back later.