## Stream: new members

### Topic: Associativity of ∨

#### newptcai (Jul 05 2023 at 09:15):

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 (Jul 05 2023 at 10:24):

import Mathlib.Tactic

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


#### Bulhwi Cha (Jul 05 2023 at 10:38):

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 (Jul 05 2023 at 13:00):

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


Last updated: Dec 20 2023 at 11:08 UTC