-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem continuous_of_continuousAt_one₂ {H M : Type*} [CommMonoid M] [TopologicalSpace M]
    [ContinuousMul M] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H →* M)
    (hf : ContinuousAt (fun x : G × H ↦ f x.1 x.2) (1, 1))
    (hl : ∀ x, ContinuousAt (f x) 1) (hr : ∀ y, ContinuousAt (f · y) 1) :
    Continuous (fun x : G × H ↦ f x.1 x.2) := continuous_iff_continuousAt.2 fun (x, y) => by
  simp only [ContinuousAt, nhds_prod_eq, ← map_mul_left_nhds_one x, ← map_mul_left_nhds_one y,
    prod_map_map_eq, tendsto_map'_iff, Function.comp_def, map_mul, MonoidHom.mul_apply] at *
  refine ((tendsto_const_nhds.mul ((hr y).comp tendsto_fst)).mul
    (((hl x).comp tendsto_snd).mul hf)).mono_right (le_of_eq ?_)
  simp only [map_one, mul_one, MonoidHom.one_apply]

Proof state:
G : Type w
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
H : Type u_1
M : Type u_2
inst✝⁵ : CommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : ContinuousMul M
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
f : G →* H →* M
hf : ContinuousAt (fun x => (f x.1) x.2) (1, 1)
hl : ∀ (x : G), ContinuousAt (⇑(f x)) 1
hr : ∀ (y : H), ContinuousAt (fun x => (f x) y) 1
x✝ : G × H
x : G
y : H
⊢ ContinuousAt (fun x => (f x.1) x.2) (x, y)

Tactic:
simp only [ContinuousAt, nhds_prod_eq, ← map_mul_left_nhds_one x, ← map_mul_left_nhds_one y,
  prod_map_map_eq, tendsto_map'_iff, Function.comp_def, map_mul, MonoidHom.mul_apply] at *

Result:
G : Type w
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
H : Type u_1
M : Type u_2
inst✝⁵ : CommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : ContinuousMul M
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup 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.1) x.2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 ((f 1) 1))
⊢ Tendsto (fun x_1 => (f x) y * (f x_1.1) y * ((f x) x_1.2 * (f x_1.1) x_1.2)) (𝓝 1 ×ˢ 𝓝 1) (𝓝 ((f x) y))

Proof state:
G : Type w
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
H : Type u_1
M : Type u_2
inst✝⁵ : CommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : ContinuousMul M
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup 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.1) x.2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 ((f 1) 1))
⊢ 𝓝 ((f x) y * (f 1) y * ((f x) 1 * (f 1) 1)) = 𝓝 ((f x) y)

Tactic:
simp only [map_one, mul_one, MonoidHom.one_apply]

Result:
no goals

Proof state:
G : Type w
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
H : Type u_1
M : Type u_2
inst✝⁵ : CommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : ContinuousMul M
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup 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.1) x.2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 ((f 1) 1))
⊢ Tendsto (fun x_1 => (f x) y * (f x_1.1) y * ((f x) x_1.2 * (f x_1.1) x_1.2)) (𝓝 1 ×ˢ 𝓝 1) (𝓝 ((f x) y))

Tactic:
refine ((tendsto_const_nhds.mul ((hr y).comp tendsto_fst)).mul
  (((hl x).comp tendsto_snd).mul hf)).mono_right (le_of_eq ?_)

Result:
G : Type w
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
H : Type u_1
M : Type u_2
inst✝⁵ : CommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : ContinuousMul M
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup 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.1) x.2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 ((f 1) 1))
⊢ 𝓝 ((f x) y * (f 1) y * ((f x) 1 * (f 1) 1)) = 𝓝 ((f x) y)