no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
x y : G
⊢ 𝓝 (x * y) = map ((fun x x_1 => x * x_1) x) (map (fun a => a * y) (𝓝 1 * 𝓝 1))
simp
no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
x y : G
⊢ map ((fun x x_1 => x * x_1) x) (map (fun a => a * y) (𝓝 1 * 𝓝 1)) = map₂ (fun a b => x * (a * b * y)) (𝓝 1) (𝓝 1)
rw [← map₂_mul, map_map₂, map_map₂]
no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
x y : G
⊢ map₂ (fun a b => x * (a * b * y)) (𝓝 1) (𝓝 1) = map₂ (fun a b => x * a * (b * y)) (𝓝 1) (𝓝 1)
simp only [mul_assoc]
no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
x y : G
⊢ map₂ (fun a b => x * a * (b * y)) (𝓝 1) (𝓝 1) = 𝓝 x * 𝓝 y
rw [← map_mul_left_nhds_one x, ← map_mul_right_nhds_one y, ← map₂_mul, map₂_map_left,
 map₂_map_right]