continuity attr on classes ineffectual

Stream: mathlib4

[Yakov Pechersky]

In Mathlib/Topology/Algebra/Group/Basic.lean, we have

@[to_additive (attr := continuity)]
class ContinuousInv (G : Type u) [TopologicalSpace G] [Inv G] : Prop where
  continuous_inv : Continuous fun a : G => a⁻¹
#align has_continuous_inv ContinuousInv

However, it doesn't seem like that continuity attribute does anything. Consider:

import Mathlib.Topology.Algebra.Group.Basic

variable {G : Type _} [TopologicalSpace G] [Group G] [ContinuousMul G] [ContinuousInv G]

theorem continuous_inv : Continuous (Inv.inv (α := G)) :=
  Continuous.inv continuous_id

theorem continuous_inv' : Continuous (Inv.inv (α := G)) :=
  ContinuousInv.continuous_inv

theorem continuous_inv'' : Continuous (Inv.inv (α := G)) := by
  continuity -- fails

attribute [local continuity] ContinuousInv.continuous_inv

theorem continuous_inv''' : Continuous (Inv.inv (α := G)) := by
  continuity -- works

[Scott Morrison]

It is slightly weird that it ever worked on classes. How about we just switch to adding the attribute to the field afterwards?