[Merged by Bors] - fix (topology/algebra/basic): fix universe issue with of_nhds_one

[kbuzzard]

Everything had type max{u v} before.

---

Right now on master we have this:

import topology.algebra.group

set_option pp.universes true
/-
topological_group.of_nhds_one.{u_1 u_2} :
  ∀ {G : Type (max u_1 u_2)} [_inst_5 : group.{(max u_1 u_2)} G] [_inst_6 : topological_space.{(max u_1 u_2)} G],
    filter.tendsto.{(max u_1 u_2) (max u_1 u_2)}
      (function.uncurry.{(max u_1 u_2) (max u_1 u_2) (max u_1 u_2)} has_mul.mul.{(max u_1 u_2)})
      ((nhds.{(max u_1 u_2)} 1).prod (nhds.{(max u_1 u_2)} 1))
      (nhds.{(max u_1 u_2)} 1) →
    filter.tendsto.{(max u_1 u_2) (max u_1 u_2)} (λ (x : G), x⁻¹) (nhds.{(max u_1 u_2)} 1)
      (nhds.{(max u_1 u_2)} 1) →
    (∀ (x₀ : G),
       nhds.{(max u_1 u_2)} x₀ =
         filter.map.{(max u_1 u_2) (max u_1 u_2)} (λ (x : G), x₀ * x) (nhds.{(max u_1 u_2)} 1)) →
    (∀ (x₀ : G),
       filter.tendsto.{(max u_1 u_2) (max u_1 u_2)} (λ (x : G), x₀ * x * x₀⁻¹) (nhds.{(max u_1 u_2)} 1)
         (nhds.{(max u_1 u_2)} 1)) →
    topological_group.{(max u_1 u_2)} G
All Messages (1)

-/

These caused a rewrite to fail! This fix to topology.algebra.group fixes the universe problem and enables the rewrite to work. Is this related to this discussion? https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/universe.20issue.20with.20.60Type*.60/near/228074514

[bryangingechen]

Thanks!
bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests