Beware hearbeats

Stream: general

[Kevin Buzzard]

This pauses for a long time...

import Mathlib.RepresentationTheory.Rep

count_hearbeats in
theorem Rep.ihom_coev_app_hom' : ∀ {k G : Type} [CommRing k] [Group G] (A B : Rep k G),
  (CategoryTheory.NatTrans.app (CategoryTheory.ihom.coev A) B).hom =
    LinearMap.flip (TensorProduct.mk k (CoeSort.coe A) ↑((CategoryTheory.Functor.id (Rep k G)).obj B).V) :=
fun {k G} [CommRing k] [Group G] A B ↦ LinearMap.ext fun x ↦ LinearMap.ext fun x_1 ↦ rfl

and then says expected command because you missed out a letter of hearTbeats :-/

OK so now I learnt my lesson, I should use auto-complete. So I change the first line to count_, press ctrl-tab, and off we go again with the heavy rfl while it just says loading... :-/

[Eric Wieser]

I had this typo just now too!