Instance names seem unnecessary after all

[ctchou]

In section 6.2 there is the following example:

instance hasMulGroup₂ {α : Type*} [Group₂ α] : Mul α :=
⟨Group₂.mul⟩

instance hasOneGroup₂ {α : Type*} [Group₂ α] : One α :=
⟨Group₂.one⟩

instance hasInvGroup₂ {α : Type*} [Group₂ α] : Inv α :=
⟨Group₂.inv⟩

and the following comment later:

In this case, we have to supply names for the instances, because Lean has a hard time coming up with good defaults.

But after I remove the three names hasMulGroup2, etc, Lean does not complain and nothing bad seems to happen. Perhaps the comment is no longer up-to-date w.r.t. the latest Lean?