-- Mathlib/Topology/Algebra/Monoid.lean
theorem ContinuousMul.of_nhds_one {M : Type u} [Monoid M] [TopologicalSpace M]
    (hmul : Tendsto (uncurry ((· * ·) : M → M → M)) (𝓝 1 ×ˢ 𝓝 1) <| 𝓝 1)
    (hleft : ∀ x₀ : M, 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1))
    (hright : ∀ x₀ : M, 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)) : ContinuousMul M :=
  ⟨by
    rw [continuous_iff_continuousAt]
    rintro ⟨x₀, y₀⟩
    have key : (fun p : M × M => x₀ * p.1 * (p.2 * y₀)) =
        ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry (· * ·)

Proof state:
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.1 * (p.2 * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x1 x2 => x1 * x2
key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x
⊢ map (uncurry fun x1 x2 => x1 * x2) (𝓝 (x₀, y₀)) = map (uncurry fun x1 x2 => x1 * x2) (𝓝 x₀ ×ˢ 𝓝 y₀)

Tactic:
rw [nhds_prod_eq]

Result:
no goals

Proof state:
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
⊢ Continuous fun p => p.1 * p.2

Tactic:
rw [continuous_iff_continuousAt]

Result:
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
⊢ ∀ (x : M × M), ContinuousAt (fun p => p.1 * p.2) x

Proof state:
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
⊢ (fun p => x₀ * p.1 * (p.2 * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x1 x2 => x1 * x2

Tactic:
ext p

Result:
case h
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
p : M × M
⊢ x₀ * p.1 * (p.2 * y₀) = (((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x1 x2 => x1 * x2) p

Proof state:
case mk
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.1 * (p.2 * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x1 x2 => x1 * x2
⊢ ContinuousAt (fun p => p.1 * p.2) (x₀, y₀)

Tactic:
have key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x := by
  ext x
  simp [mul_assoc]

Result:
case mk
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.1 * (p.2 * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x1 x2 => x1 * x2
key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x
⊢ ContinuousAt (fun p => p.1 * p.2) (x₀, y₀)

Proof state:
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.1 * (p.2 * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x1 x2 => x1 * x2
key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x
⊢ map (fun a => a.1 * a.2) (𝓝 x₀ ×ˢ 𝓝 y₀) = map (fun p => x₀ * p.1 * (p.2 * y₀)) (𝓝 1 ×ˢ 𝓝 1)

Tactic:
simp_rw [hleft x₀, hright y₀, prod_map_map_eq, Filter.map_map, Function.comp_def]

Result:
no goals

Proof state:
case h
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.1 * (p.2 * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x1 x2 => x1 * x2
x : M
⊢ ((fun x => x₀ * x) ∘ fun x => y₀ * x) x = x₀ * y₀ * x

Tactic:
simp [mul_assoc]

Result:
no goals

Proof state:
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.1 * (p.2 * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x1 x2 => x1 * x2
⊢ ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x

Tactic:
ext x

Result:
case h
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.1 * (p.2 * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x1 x2 => x1 * x2
x : M
⊢ ((fun x => x₀ * x) ∘ fun x => y₀ * x) x = x₀ * y₀ * x

Proof state:
case h
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
p : M × M
⊢ x₀ * p.1 * (p.2 * y₀) = (((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x1 x2 => x1 * x2) p

Tactic:
simp [uncurry, mul_assoc]

Result:
no goals

Proof state:
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.1 * (p.2 * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x1 x2 => x1 * x2
key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x
⊢ map ((fun x => x₀ * x) ∘ fun x => x * y₀) (𝓝 1) = 𝓝 (x₀ * y₀)

Tactic:
rw [← Filter.map_map, ← hright, hleft y₀, Filter.map_map, key₂, ← hleft]

Result:
no goals

Proof state:
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
⊢ ∀ (x : M × M), ContinuousAt (fun p => p.1 * p.2) x

Tactic:
rintro ⟨x₀, y₀⟩

Result:
case mk
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
⊢ ContinuousAt (fun p => p.1 * p.2) (x₀, y₀)

Proof state:
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.1 * (p.2 * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x1 x2 => x1 * x2
key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x
⊢ map (fun p => x₀ * p.1 * (p.2 * y₀)) (𝓝 1 ×ˢ 𝓝 1) =
    map ((fun x => x₀ * x) ∘ fun x => x * y₀) (map (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1))

Tactic:
rw [key, ← Filter.map_map]

Result:
no goals