Slightly golf proofs although they're already really short

Changes

1 changed files (+3/-5)

• Category.lean
  • @@ -335,7 +335,7 @@ instance [Applicative f] [LawfulApplicative f] [Applicative g] [LawfulApplicativ
    seq_pure := by simp seq_assoc x h h' := by simp [seq_assoc, seq_map_assoc, map_seq] - congr 3 + congr ext simp [seq_assoc]
  • @@ -504,8 +504,7 @@ instance [EndofunctorMonoid m] : Monad m where
    instance [EndofunctorMonoid m] [J : Natural (m ∘ m) m EndofunctorMonoid.join] [P : Natural Id m EndofunctorMonoid.pure] : LawfulMonad m := LawfulMonad.mk' m id_map (pure_bind := fun x f ↦ by - simp [P.naturality, Functor.map] - exact EndofunctorMonoid.join_pure) + simpa [P.naturality, Functor.map] using EndofunctorMonoid.join_pure) (bind_assoc := fun x f g ↦ by have := EndofunctorMonoid.join_join (x := (fun a ↦ Functor.map (f := m) g (f a)) <$> x) simp at this
  • @@ -513,8 +512,7 @@ instance [EndofunctorMonoid m] [J : Natural (m ∘ m) m EndofunctorMonoid.join]
    (map_const := by simp [map_const]) (bind_pure_comp := fun f x ↦ by have := EndofunctorMonoid.join_map_pure (x := f <$> x) - simp at this - exact this) + simpa using this) @[simp] def joinFromBind [Monad m] (bind : {α β : Type u} → m α → (α → m β) → m β) (x : m (m α)) :=