Oh wait I can just directly simpa without the this

Changes

1 changed files (+1/-2)

• Category.lean
  • @@ -540,8 +540,7 @@ instance [EndofunctorMonoid m] [J : Natural (m ∘ m) m EndofunctorMonoid.join]
    simp [J.naturality, ← this]) (map_const := by simp [map_const]) (bind_pure_comp := fun f x ↦ by - have := EndofunctorMonoid.join_map_pure (x := f <$> x) - simpa using this) + simpa using EndofunctorMonoid.join_map_pure (x := f <$> x)) @[simp] def joinFromBind [Monad m] (bind : {α β : Type u} → m α → (α → m β) → m β) (x : m (m α)) :=