case mk
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
g : GroupTopology α
toTopologicalSpace✝ : TopologicalSpace α
toTopologicalGroup✝ : TopologicalGroup α
h :
  { toTopologicalSpace := toTopologicalSpace✝, toTopologicalGroup := toTopologicalGroup✝ }.toTopologicalSpace =
    g.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝, toTopologicalGroup := toTopologicalGroup✝ } = g
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
f g : GroupTopology α
h : f.toTopologicalSpace = g.toTopologicalSpace
⊢ f = g
cases f
case mk.mk
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
toTopologicalSpace✝¹ : TopologicalSpace α
toTopologicalGroup✝¹ : TopologicalGroup α
toTopologicalSpace✝ : TopologicalSpace α
toTopologicalGroup✝ : TopologicalGroup α
h :
  { toTopologicalSpace := toTopologicalSpace✝¹, toTopologicalGroup := toTopologicalGroup✝¹ }.toTopologicalSpace =
    { toTopologicalSpace := toTopologicalSpace✝, toTopologicalGroup := toTopologicalGroup✝ }.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝¹, toTopologicalGroup := toTopologicalGroup✝¹ } =
    { toTopologicalSpace := toTopologicalSpace✝, toTopologicalGroup := toTopologicalGroup✝ }
case mk
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
g : GroupTopology α
toTopologicalSpace✝ : TopologicalSpace α
toTopologicalGroup✝ : TopologicalGroup α
h :
  { toTopologicalSpace := toTopologicalSpace✝, toTopologicalGroup := toTopologicalGroup✝ }.toTopologicalSpace =
    g.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝, toTopologicalGroup := toTopologicalGroup✝ } = g
cases g
no goals
case mk.mk
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
toTopologicalSpace✝¹ : TopologicalSpace α
toTopologicalGroup✝¹ : TopologicalGroup α
toTopologicalSpace✝ : TopologicalSpace α
toTopologicalGroup✝ : TopologicalGroup α
h :
  { toTopologicalSpace := toTopologicalSpace✝¹, toTopologicalGroup := toTopologicalGroup✝¹ }.toTopologicalSpace =
    { toTopologicalSpace := toTopologicalSpace✝, toTopologicalGroup := toTopologicalGroup✝ }.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝¹, toTopologicalGroup := toTopologicalGroup✝¹ } =
    { toTopologicalSpace := toTopologicalSpace✝, toTopologicalGroup := toTopologicalGroup✝ }
congr