assoc_rw_test.lean

universes u v

class category (Obj : Type u) : Type (max u (v+1)) :=
  (Hom : Obj → Obj → Type v)
  (identity : Π X : Obj, Hom X X)
  (compose  : Π {X Y Z : Obj}, Hom X Y → Hom Y Z → Hom X Z)
  (left_identity  : ∀ {X Y : Obj} (f : Hom X Y), compose (identity X) f = f)
  (right_identity : ∀ {X Y : Obj} (f : Hom X Y), compose f (identity Y) = f)
  (associativity  : ∀ {W X Y Z : Obj} (f : Hom W X) (g : Hom X Y) (h : Hom Y Z), compose (compose f g) h = compose f (compose g h))

infixr ` ≫ `:80 := category.compose -- type as \gg
infixr ` ⟶ `:10  := category.Hom     -- type as \h
local notation f ` ∘ `:80 g:80 := g ≫ f

section

parameters {C : Type u} [cat : category.{u v} C]
include cat

parameters {a b : C} {i : a ⟶ b}
parameters {x : C} {f : a ⟶ x} (h : b ⟶ x) (e : h ∘ i = f)
parameters {y : C} (g : x ⟶ y)
include e
def gh : b ⟶ y := g ∘ h
example : gh ∘ i = g ∘ f := begin
  dsimp [gh],
  -- assoc_rw [e]
  rw [←category.associativity, e]
end

end