Comm Group no compact automorphisms

@[to_additive]theorem CommGroup.no_compact_automorphisms    {A : Type*} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A]    [ConnectedSpace A] [CompactSpace A] [T2Space A] (K : Subgroup (ContinuousMonoidHom A A))    (hK : IsCompact (K : Set (ContinuousMonoidHom A A))) :    K = ⊥ := by  have A_rootable : RootableBy A ℕ := Group.rootable A  rw [eq_bot_iff]  intro f hf  ext a  rw [ContinuousMonoidHom.one_toFun]  by_contra! ha  let U : Set A := {f a}ᶜ  have hU : IsOpen U := isOpen_compl_singleton  have hU1 : 1 ∈ U := ha.symm  let W : Set (A →ₜ* A) := {f | Set.MapsTo f Set.univ U}  have hW : IsOpen W :=    (ContinuousMonoidHom.isInducing_toContinuousMap A A).continuous.isOpen_preimage _      (ContinuousMap.isOpen_setOf_mapsTo isCompact_univ hU)  have hW1 : 1 ∈ W := by simpa [W]  replace hW1 : W ∈ nhds 1 := hW.mem_nhds hW1  have : CompactSpace K := isCompact_iff_compactSpace.mp hK  obtain ⟨n, hn0, hnf⟩ :=    (mapClusterPt_iff_frequently.mp (mapClusterPt_one_atTop_pow ⟨f, hf⟩) (Subtype.val ⁻¹' W)    (continuousAt_subtype_val.preimage_mem_nhds (by exact hW1))).forall_exists_of_atTop 1  replace hn0 : n ≠ 0 := by grind  rw [Set.mem_preimage, Subgroup.coe_pow, Subtype.coe_mk,    Set.mem_setOf_eq, Set.mapsTo_univ_iff, ← Set.range_subset_iff] at hnf  change (f ^ n).range ≤ U at hnf  suffices f.range ≤ (f ^ n).range by    exact (Set.Subset.trans this hnf) ⟨a, rfl⟩ rfl  rintro - ⟨b, rfl⟩  use RootableBy.root b n  simp [ContinuousMonoidHom.pow_apply, ← map_pow, RootableBy.root_cancel b hn0]