Associativity of ∨

Stream: new members

[newptcai]

I tried to prove (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) using the following code

example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
  Iff.intro
  (fun h =>
    Or.elim h
    (fun hpq =>
      Or.elim hpq
      (fun hp => Or.inl hp)
      (fun hq => Or.inr (Or.inl hq))
      )
    (fun hr => Or.inr (Or.inr hr)))
  (fun h =>
    Or.elim h
    (fun hp => Or.inl (Or.inl hp))
    (fun hqr =>
      Or.elim hqr
      (fun hq => Or.inl (Or.inr hq))
      (fun hr => Or.inr hr)
    ))

It is possible to make this code more concise?

[Kevin Buzzard]

import Mathlib.Tactic

example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := by
  tauto

[Bulhwi Cha]

example (p q r : Prop) : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := by
  apply Iff.intro <;> intro h
  · match h with
    | Or.inl (Or.inl hp) => exact Or.inl hp
    | Or.inl (Or.inr hq) => exact Or.inr (Or.inl hq)
    | Or.inr hr => exact Or.inr (Or.inr hr)
  · match h with
    | Or.inl hp => exact Or.inl (Or.inl hp)
    | Or.inr (Or.inl hq) => exact Or.inl (Or.inr hq)
    | Or.inr (Or.inr hr) => exact Or.inr hr

[Yuyang Zhao]

example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
  .intro
    (·.elim (·.elim (.inl ·) (.inr <| .inl ·)) (.inr <| .inr ·))
    (·.elim (.inl <| .inl ·) (·.elim (.inl <| .inr ·) (.inr ·)))