α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : TopologicalSpace α
f✝ : α → G
s : Set α
x✝¹ : α
H : Type u_1
M : Type u_2
inst✝⁵ : CommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : ContinuousMul M
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalGroup H
f : G →* H →* M
hl : ∀ (x : G), Tendsto (↑(↑f x)) (𝓝 1) (𝓝 (↑(↑f x) 1))
hr : ∀ (y : H), Tendsto (fun x => ↑(↑f x) y) (𝓝 1) (𝓝 (↑(↑f 1) y))
x✝ : G × H
x : G
y : H
hf : Tendsto (fun x => ↑(↑f x.fst) x.snd) (𝓝 1 ×ˢ 𝓝 1) (𝓝 (↑(↑f 1) 1))
⊢ 𝓝 (↑(↑f x) y * ↑(↑f 1) y * (↑(↑f x) 1 * ↑(↑f 1) 1)) = 𝓝 (↑(↑f x) y)
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : TopologicalSpace α
f✝ : α → G
s : Set α
x✝¹ : α
H : Type u_1
M : Type u_2
inst✝⁵ : CommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : ContinuousMul M
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalGroup H
f : G →* H →* M
hl : ∀ (x : G), Tendsto (↑(↑f x)) (𝓝 1) (𝓝 (↑(↑f x) 1))
hr : ∀ (y : H), Tendsto (fun x => ↑(↑f x) y) (𝓝 1) (𝓝 (↑(↑f 1) y))
x✝ : G × H
x : G
y : H
hf : Tendsto (fun x => ↑(↑f x.fst) x.snd) (𝓝 1 ×ˢ 𝓝 1) (𝓝 (↑(↑f 1) 1))
⊢ Tendsto (fun x_1 => ↑(↑f x) y * ↑(↑f x_1.fst) y * (↑(↑f x) x_1.snd * ↑(↑f x_1.fst) x_1.snd)) (𝓝 1 ×ˢ 𝓝 1)
    (𝓝 (↑(↑f x) y))
refine ((tendsto_const_nhds.mul ((hr y).comp tendsto_fst)).mul
  (((hl x).comp tendsto_snd).mul hf)).mono_right (le_of_eq ?_)
no goals
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : TopologicalSpace α
f✝ : α → G
s : Set α
x✝¹ : α
H : Type u_1
M : Type u_2
inst✝⁵ : CommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : ContinuousMul M
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalGroup H
f : G →* H →* M
hl : ∀ (x : G), Tendsto (↑(↑f x)) (𝓝 1) (𝓝 (↑(↑f x) 1))
hr : ∀ (y : H), Tendsto (fun x => ↑(↑f x) y) (𝓝 1) (𝓝 (↑(↑f 1) y))
x✝ : G × H
x : G
y : H
hf : Tendsto (fun x => ↑(↑f x.fst) x.snd) (𝓝 1 ×ˢ 𝓝 1) (𝓝 (↑(↑f 1) 1))
⊢ 𝓝 (↑(↑f x) y * ↑(↑f 1) y * (↑(↑f x) 1 * ↑(↑f 1) 1)) = 𝓝 (↑(↑f x) y)
simp only [map_one, mul_one, MonoidHom.one_apply]