lean 4 ac_refl

Stream: Is there code for X?

[Kevin Buzzard]

I'm stuck on this:

import Mathlib

example (A B C D E F G H : Prop) : A ∨ B ∨ C ∨ D ∨ E ∨ F ∨ G ∨ H ↔ (F ∨ G) ∨ (H ∨ B) ∨ (A ∨ E) ∨ (D ∨ C) := by
  simp [or_assoc]
  -- out of ideas
  sorry

In Lean 3, apply iff_of_eq, ac_refl, would do it, but I can't find ac_refl in mathlib4. Is this just annoying in mathlib4 right now?

[Matthew Ballard]

ac_rfl implementation new syntax

[Moritz Doll]

did you check whether ac_refl is still on the list of unported tactics?

[Alex J. Best]

tauto also works for this fwiw

[Kevin Buzzard]

Moritz Doll said:

did you check whether ac_refl is still on the list of unported tactics?

I looked in the Tactic directory of mathlib4 and couldn't find it. I can quite believe that there are better ways to do this!

[Matthew Ballard]

It’s in core now

[Matthew Ballard]

Does aesop also work?

[Kevin Buzzard]

It does in my use case (which is 5 times worse than the example above)!

[Yakov Pechersky]

The assoc, comm, left_comm combination works for any abelian-group-like op:

example (A B C D E F G H : Prop) : A ∨ B ∨ C ∨ D ∨ E ∨ F ∨ G ∨ H ↔ (F ∨ G) ∨ (H ∨ B) ∨ (A ∨ E) ∨ (D ∨ C) := by
  simp [or_assoc, or_comm, or_left_comm]

[Kevin Buzzard]

gaargh I tried this! But I forgot or_left_comm! Thanks! That'll learn me (until the next time I forget it)