What import links or_assoc with simp

Stream: new members

[Lars Ericson]

As an exercise in Lean 4 I did this proof:

variable (p q r : Prop)

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

I wondered if a shorter proof were possible, so I asked Google Bard "What is the most compact Lean 4 proof of (p ∨ q) ∨ r ↔ p ∨ (q ∨ r)" and it said

variable (p q r : Prop)

theorem or_assoc : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
  by simp -- simp made no progress

but Lean says "simp made no progress". However, there is an or_assoc in Mathlib. Is there an import that links simp and or_assoc which would make Bard's proof work?

[Newell Jensen]

by tauto would make it even simpler if that is what you are going for...

[Lars Ericson]

@Newell Jensen this has a similar problem unknown tactic. I am missing a crucial import to get the tactics filled up:

variable (p q r : Prop)

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

[Newell Jensen]

Yes, something like this (you can refine if you don't want to import as much):

import Mathlib

variable (p q r : Prop)

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