ι : Type ?u.60957
α : Type ?u.60960
X : Type ?u.60963
M✝ : Type ?u.60966
N : Type ?u.60969
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
⊢ ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
ι : Type ?u.60957
α : Type ?u.60960
X : Type ?u.60963
M✝ : Type ?u.60966
N : Type ?u.60969
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
⊢ ContinuousMul M
apply ContinuousMul.of_nhds_one hmul hleft
ι : Type ?u.60957
α : Type ?u.60960
X : Type ?u.60963
M✝ : Type ?u.60966
N : Type ?u.60969
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
x₀ : M
⊢ 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
ι : Type ?u.60957
α : Type ?u.60960
X : Type ?u.60963
M✝ : Type ?u.60966
N : Type ?u.60969
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
⊢ ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
intro x₀
no goals
ι : Type ?u.60957
α : Type ?u.60960
X : Type ?u.60963
M✝ : Type ?u.60966
N : Type ?u.60969
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
x₀ : M
⊢ 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
simp_rw [mul_comm, hleft x₀]