better rw_assoc

Stream: mathlib4

[Kevin Buzzard]

Apparently rw_assoc isn't ported to Lean 4 yet, but I guess would need simp_assoc for lemmas like this

import Mathlib.Tactic

open CategoryTheory

variable (C : Type) [Category C]

variable (a b c d e f g h i j : C)

example (ab : a ⟶ b) (bc : b ⟶ c) (ad : a ⟶ d) (de : d ⟶ e) (ce : c ⟶ e)
    (comm1 : ab ≫ bc ≫ ce = ad ≫ de)
    (cf : c ⟶ f) (eg : e ⟶ g) (fg : f ⟶ g)
    (comm2 : ce ≫ eg = cf ≫ fg)
    (fh : f ⟶ h) (hj : h ⟶ j) (gi : g ⟶ i) (ij : i ⟶ j)
    (comm3 : fg ≫ gi ≫ ij = fh ≫ hj) :
    ab ≫ bc ≫ cf ≫ fh ≫ hj = ad ≫ de ≫ eg ≫ gi ≫ ij := by
  -- assoc_rw not ported yet
  repeat rw [← Category.assoc]
  rw [← comm1]
  repeat rw [Category.assoc]
  congr 2
  repeat rw [← Category.assoc]
  rw [comm2]
  repeat rw [Category.assoc]
  congr 1
  rw [comm3]

and furthermore in my actual use case I wasn't even using category theory, everything was an R-linear map. Do we have tactics which might solve goals like this?

[Kyle Miller]

I know you said you weren't using category theory, but for category theory there's a conv mode slice tactic for reassociating

[Kyle Miller]

It could be more ergonomic, but it's usable:

example (ab : a ⟶ b) (bc : b ⟶ c) (ad : a ⟶ d) (de : d ⟶ e) (ce : c ⟶ e)
    (comm1 : ab ≫ bc ≫ ce = ad ≫ de)
    (cf : c ⟶ f) (eg : e ⟶ g) (fg : f ⟶ g)
    (comm2 : ce ≫ eg = cf ≫ fg)
    (fh : f ⟶ h) (hj : h ⟶ j) (gi : g ⟶ i) (ij : i ⟶ j)
    (comm3 : fg ≫ gi ≫ ij = fh ≫ hj) :
    ab ≫ bc ≫ cf ≫ fh ≫ hj = ad ≫ de ≫ eg ≫ gi ≫ ij := by
  slice_rhs 0 1 => rw [← comm1]
  slice_rhs 3 4 => rw [comm2]
  slice_rhs 4 7 => rw [comm3]