[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Mul M
inst✝ : ContinuousMul M
a b : M
⊢ 𝓝 a * 𝓝 b ≤ 𝓝 (a * b)
[PROOFSTEP]
rw [← map₂_mul, ← map_uncurry_prod, ← nhds_prod_eq]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Mul M
inst✝ : ContinuousMul M
a b : M
⊢ map (Function.uncurry fun x x_1 => x * x_1) (𝓝 (a, b)) ≤ 𝓝 (a * b)
[PROOFSTEP]
exact continuous_mul.tendsto _
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Mul M
inst✝⁵ : ContinuousMul M
inst✝⁴ : TopologicalSpace N
inst✝³ : Monoid N
inst✝² : ContinuousMul N
inst✝¹ : T2Space N
f : ι → Nˣ
r₁ r₂ : N
l : Filter ι
inst✝ : NeBot l
h₁ : Tendsto (fun x => ↑(f x)) l (𝓝 r₁)
h₂ : Tendsto (fun x => ↑(f x)⁻¹) l (𝓝 r₂)
⊢ r₁ * r₂ = 1
[PROOFSTEP]
symm
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Mul M
inst✝⁵ : ContinuousMul M
inst✝⁴ : TopologicalSpace N
inst✝³ : Monoid N
inst✝² : ContinuousMul N
inst✝¹ : T2Space N
f : ι → Nˣ
r₁ r₂ : N
l : Filter ι
inst✝ : NeBot l
h₁ : Tendsto (fun x => ↑(f x)) l (𝓝 r₁)
h₂ : Tendsto (fun x => ↑(f x)⁻¹) l (𝓝 r₂)
⊢ 1 = r₁ * r₂
[PROOFSTEP]
simpa using h₁.mul h₂
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Mul M
inst✝⁵ : ContinuousMul M
inst✝⁴ : TopologicalSpace N
inst✝³ : Monoid N
inst✝² : ContinuousMul N
inst✝¹ : T2Space N
f : ι → Nˣ
r₁ r₂ : N
l : Filter ι
inst✝ : NeBot l
h₁ : Tendsto (fun x => ↑(f x)) l (𝓝 r₁)
h₂ : Tendsto (fun x => ↑(f x)⁻¹) l (𝓝 r₂)
⊢ r₂ * r₁ = 1
[PROOFSTEP]
symm
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Mul M
inst✝⁵ : ContinuousMul M
inst✝⁴ : TopologicalSpace N
inst✝³ : Monoid N
inst✝² : ContinuousMul N
inst✝¹ : T2Space N
f : ι → Nˣ
r₁ r₂ : N
l : Filter ι
inst✝ : NeBot l
h₁ : Tendsto (fun x => ↑(f x)) l (𝓝 r₁)
h₂ : Tendsto (fun x => ↑(f x)⁻¹) l (𝓝 r₂)
⊢ 1 = r₂ * r₁
[PROOFSTEP]
simpa using h₂.mul h₁
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid 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)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
⊢ Continuous fun p => p.fst * p.snd
[PROOFSTEP]
rw [continuous_iff_continuousAt]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid 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)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
⊢ ∀ (x : M × M), ContinuousAt (fun p => p.fst * p.snd) x
[PROOFSTEP]
rintro ⟨x₀, y₀⟩
[GOAL]
case mk
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid 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)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
⊢ ContinuousAt (fun p => p.fst * p.snd) (x₀, y₀)
[PROOFSTEP]
have key : (fun p : M × M => x₀ * p.1 * (p.2 * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry (· * ·) :=
  by
  ext p
  simp [uncurry, mul_assoc]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid 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)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
⊢ (fun p => x₀ * p.fst * (p.snd * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x x_1 => x * x_1
[PROOFSTEP]
ext p
[GOAL]
case h
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid 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)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
p : M × M
⊢ x₀ * p.fst * (p.snd * y₀) = (((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x x_1 => x * x_1) p
[PROOFSTEP]
simp [uncurry, mul_assoc]
[GOAL]
case mk
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid 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)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.fst * (p.snd * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x x_1 => x * x_1
⊢ ContinuousAt (fun p => p.fst * p.snd) (x₀, y₀)
[PROOFSTEP]
have key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x :=
  by
  ext x
  simp [mul_assoc]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid 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)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.fst * (p.snd * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x x_1 => x * x_1
⊢ ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid 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)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.fst * (p.snd * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x x_1 => x * x_1
x : M
⊢ ((fun x => x₀ * x) ∘ fun x => y₀ * x) x = x₀ * y₀ * x
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
case mk
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid 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)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.fst * (p.snd * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x x_1 => x * x_1
key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x
⊢ ContinuousAt (fun p => p.fst * p.snd) (x₀, y₀)
[PROOFSTEP]
calc
  map (uncurry (· * ·)) (𝓝 (x₀, y₀)) = map (uncurry (· * ·)) (𝓝 x₀ ×ˢ 𝓝 y₀) := by rw [nhds_prod_eq]
  _ = map (fun p : M × M => x₀ * p.1 * (p.2 * y₀)) (𝓝 1 ×ˢ 𝓝 1) :=
    -- Porting note: `rw` was able to prove this
            -- Now it fails with `failed to rewrite using equation theorems for 'Function.uncurry'`
            -- and `failed to rewrite using equation theorems for 'Function.comp'`.
            -- Removing those two lemmas, the `rw` would succeed, but then needs a `rfl`.by
    simp_rw [uncurry, hleft x₀, hright y₀, prod_map_map_eq, Filter.map_map, Function.comp]
  _ = map ((fun x => x₀ * x) ∘ fun x => x * y₀) (map (uncurry (· * ·)) (𝓝 1 ×ˢ 𝓝 1)) := by rw [key, ← Filter.map_map]
  _ ≤ map ((fun x : M => x₀ * x) ∘ fun x => x * y₀) (𝓝 1) := (map_mono hmul)
  _ = 𝓝 (x₀ * y₀) := by rw [← Filter.map_map, ← hright, hleft y₀, Filter.map_map, key₂, ← hleft]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid 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)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.fst * (p.snd * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x x_1 => x * x_1
key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x
⊢ map (uncurry fun x x_1 => x * x_1) (𝓝 (x₀, y₀)) = map (uncurry fun x x_1 => x * x_1) (𝓝 x₀ ×ˢ 𝓝 y₀)
[PROOFSTEP]
rw [nhds_prod_eq]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid 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)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.fst * (p.snd * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x x_1 => x * x_1
key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x
⊢ map (uncurry fun x x_1 => x * x_1) (𝓝 x₀ ×ˢ 𝓝 y₀) = map (fun p => x₀ * p.fst * (p.snd * y₀)) (𝓝 1 ×ˢ 𝓝 1)
[PROOFSTEP]
simp_rw [uncurry, hleft x₀, hright y₀, prod_map_map_eq, Filter.map_map, Function.comp]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid 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)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.fst * (p.snd * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x x_1 => x * x_1
key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x
⊢ map (fun p => x₀ * p.fst * (p.snd * y₀)) (𝓝 1 ×ˢ 𝓝 1) =
    map ((fun x => x₀ * x) ∘ fun x => x * y₀) (map (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1))
[PROOFSTEP]
rw [key, ← Filter.map_map]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace M✝
inst✝³ : Mul M✝
inst✝² : ContinuousMul M✝
M : Type u
inst✝¹ : Monoid 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)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.fst * (p.snd * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x x_1 => x * x_1
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₀)
[PROOFSTEP]
rw [← Filter.map_map, ← hright, hleft y₀, Filter.map_map, key₂, ← hleft]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
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
[PROOFSTEP]
apply ContinuousMul.of_nhds_one hmul hleft
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
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)
[PROOFSTEP]
intro x₀
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
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)
[PROOFSTEP]
simp_rw [mul_comm, hleft x₀]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
M₁ : Type u_6
M₂ : Type u_7
inst✝⁴ : TopologicalSpace M₂
inst✝³ : T2Space M₂
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : ContinuousMul M₂
⊢ IsClosed {f | ∀ (x y : M₁), f (x * y) = f x * f y}
[PROOFSTEP]
simp only [setOf_forall]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
M₁ : Type u_6
M₂ : Type u_7
inst✝⁴ : TopologicalSpace M₂
inst✝³ : T2Space M₂
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : ContinuousMul M₂
⊢ IsClosed (⋂ (i : M₁) (i_1 : M₁), {x | x (i * i_1) = x i * x i_1})
[PROOFSTEP]
exact
  isClosed_iInter fun x =>
    isClosed_iInter fun y =>
      isClosed_eq
        (continuous_apply _)
          -- Porting note: proof was:
                    -- `((continuous_apply _).mul (continuous_apply _))`
        (by continuity)
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : TopologicalSpace X
M₁ : Type u_6
M₂ : Type u_7
inst✝⁴ : TopologicalSpace M₂
inst✝³ : T2Space M₂
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : ContinuousMul M₂
x y : M₁
⊢ Continuous fun x_1 => x_1 x * x_1 y
[PROOFSTEP]
continuity
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N✝ : Type u_5
inst✝⁶ : TopologicalSpace X
M : Type u_6
N : Type u_7
F : Type u_8
inst✝⁵ : Mul M
inst✝⁴ : Mul N
inst✝³ : MulHomClass F M N
inst✝² : TopologicalSpace M
inst✝¹ : TopologicalSpace N
inst✝ : ContinuousMul N
f : F
hf : Inducing ↑f
⊢ Continuous (↑f ∘ fun p => p.fst * p.snd)
[PROOFSTEP]
simpa only [(· ∘ ·), map_mul f] using hf.continuous.fst'.mul hf.continuous.snd'
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
s : Set M
hs : s ∈ 𝓝 1
⊢ ∃ V, IsOpen V ∧ 1 ∈ V ∧ ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ s
[PROOFSTEP]
have : (fun a : M × M => a.1 * a.2) ⁻¹' s ∈ 𝓝 ((1, 1) : M × M) := tendsto_mul (by simpa only [one_mul] using hs)
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
s : Set M
hs : s ∈ 𝓝 1
⊢ s ∈ 𝓝 (1 * 1)
[PROOFSTEP]
simpa only [one_mul] using hs
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
s : Set M
hs : s ∈ 𝓝 1
this : (fun a => a.fst * a.snd) ⁻¹' s ∈ 𝓝 (1, 1)
⊢ ∃ V, IsOpen V ∧ 1 ∈ V ∧ ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ s
[PROOFSTEP]
simpa only [prod_subset_iff] using exists_nhds_square this
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
⊢ ∃ V, V ∈ 𝓝 1 ∧ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
[PROOFSTEP]
rcases exists_nhds_one_split hu with ⟨W, W1, h⟩
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ (v : M), v ∈ W → ∀ (w : M), w ∈ W → v * w ∈ u
⊢ ∃ V, V ∈ 𝓝 1 ∧ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
[PROOFSTEP]
rcases exists_nhds_one_split W1 with ⟨V, V1, h'⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ (v : M), v ∈ W → ∀ (w : M), w ∈ W → v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ W
⊢ ∃ V, V ∈ 𝓝 1 ∧ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
[PROOFSTEP]
use V, V1
[GOAL]
case right
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ (v : M), v ∈ W → ∀ (w : M), w ∈ W → v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ W
⊢ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
[PROOFSTEP]
intro v w s t v_in w_in s_in t_in
[GOAL]
case right
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ (v : M), v ∈ W → ∀ (w : M), w ∈ W → v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ W
v w s t : M
v_in : v ∈ V
w_in : w ∈ V
s_in : s ∈ V
t_in : t ∈ V
⊢ v * w * s * t ∈ u
[PROOFSTEP]
simpa only [mul_assoc] using h _ (h' v v_in w w_in) _ (h' s s_in t t_in)
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
U : Set M
hU : U ∈ 𝓝 1
⊢ ∃ V, IsOpen V ∧ 1 ∈ V ∧ V * V ⊆ U
[PROOFSTEP]
rcases exists_open_nhds_one_split hU with ⟨V, Vo, V1, hV⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
U : Set M
hU : U ∈ 𝓝 1
V : Set M
Vo : IsOpen V
V1 : 1 ∈ V
hV : ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ U
⊢ ∃ V, IsOpen V ∧ 1 ∈ V ∧ V * V ⊆ U
[PROOFSTEP]
use V, Vo, V1
[GOAL]
case right
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
U : Set M
hU : U ∈ 𝓝 1
V : Set M
Vo : IsOpen V
V1 : 1 ∈ V
hV : ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ U
⊢ V * V ⊆ U
[PROOFSTEP]
rintro _ ⟨x, y, hx, hy, rfl⟩
[GOAL]
case right.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
U : Set M
hU : U ∈ 𝓝 1
V : Set M
Vo : IsOpen V
V1 : 1 ∈ V
hV : ∀ (v : M), v ∈ V → ∀ (w : M), w ∈ V → v * w ∈ U
x y : M
hx : x ∈ V
hy : y ∈ V
⊢ (fun x x_1 => x * x_1) x y ∈ U
[PROOFSTEP]
exact hV _ hx _ hy
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
s t : Set M
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (s * t)
[PROOFSTEP]
rw [← image_mul_prod]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
s t : Set M
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact ((fun x => x.fst * x.snd) '' s ×ˢ t)
[PROOFSTEP]
exact (hs.prod ht).image continuous_mul
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
x✝ : ∀ (i : ι), i ∈ [] → Tendsto (f i) x (𝓝 (a i))
⊢ Tendsto (fun b => List.prod (List.map (fun c => f c b) [])) x (𝓝 (List.prod (List.map a [])))
[PROOFSTEP]
simp [tendsto_const_nhds]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f✝ : ι → α → M
x : Filter α
a : ι → M
f : ι
l : List ι
h : ∀ (i : ι), i ∈ f :: l → Tendsto (f✝ i) x (𝓝 (a i))
⊢ Tendsto (fun b => List.prod (List.map (fun c => f✝ c b) (f :: l))) x (𝓝 (List.prod (List.map a (f :: l))))
[PROOFSTEP]
simp only [List.map_cons, List.prod_cons]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f✝ : ι → α → M
x : Filter α
a : ι → M
f : ι
l : List ι
h : ∀ (i : ι), i ∈ f :: l → Tendsto (f✝ i) x (𝓝 (a i))
⊢ Tendsto (fun b => f✝ f b * List.prod (List.map (fun c => f✝ c b) l)) x (𝓝 (a f * List.prod (List.map a l)))
[PROOFSTEP]
exact (h f (List.mem_cons_self _ _)).mul (tendsto_list_prod l fun c hc => h c (List.mem_cons_of_mem _ hc))
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ (i : ι), i ∈ l → ContinuousOn (f i) t
⊢ ContinuousOn (fun a => List.prod (List.map (fun i => f i a) l)) t
[PROOFSTEP]
intro x hx
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ (i : ι), i ∈ l → ContinuousOn (f i) t
x : X
hx : x ∈ t
⊢ ContinuousWithinAt (fun a => List.prod (List.map (fun i => f i a) l)) t x
[PROOFSTEP]
rw [continuousWithinAt_iff_continuousAt_restrict _ hx]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ (i : ι), i ∈ l → ContinuousOn (f i) t
x : X
hx : x ∈ t
⊢ ContinuousAt (restrict t fun a => List.prod (List.map (fun i => f i a) l)) { val := x, property := hx }
[PROOFSTEP]
refine' tendsto_list_prod _ fun i hi => _
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ (i : ι), i ∈ l → ContinuousOn (f i) t
x : X
hx : x ∈ t
i : ι
hi : i ∈ l
⊢ Tendsto (fun b => f i ↑b) (𝓝 { val := x, property := hx }) (𝓝 (f i ↑{ val := x, property := hx }))
[PROOFSTEP]
specialize h i hi x hx
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
x : X
hx : x ∈ t
i : ι
hi : i ∈ l
h : ContinuousWithinAt (f i) t x
⊢ Tendsto (fun b => f i ↑b) (𝓝 { val := x, property := hx }) (𝓝 (f i ↑{ val := x, property := hx }))
[PROOFSTEP]
rw [continuousWithinAt_iff_continuousAt_restrict _ hx] at h 
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
x : X
hx : x ∈ t
i : ι
hi : i ∈ l
h : ContinuousAt (restrict t (f i)) { val := x, property := hx }
⊢ Tendsto (fun b => f i ↑b) (𝓝 { val := x, property := hx }) (𝓝 (f i ↑{ val := x, property := hx }))
[PROOFSTEP]
exact h
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
⊢ Continuous fun a => a ^ 0
[PROOFSTEP]
simpa using continuous_const
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
k : ℕ
⊢ Continuous fun a => a ^ (k + 1)
[PROOFSTEP]
simp only [pow_succ]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
k : ℕ
⊢ Continuous fun a => a * a ^ k
[PROOFSTEP]
exact continuous_id.mul (continuous_pow _)
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : b * a = 1
⊢ Tendsto (fun x => a * x) (cocompact M) (cocompact M)
[PROOFSTEP]
refine Filter.Tendsto.of_tendsto_comp ?_ (Filter.comap_cocompact_le (continuous_mul_left b))
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : b * a = 1
⊢ Tendsto ((fun b_1 => b * b_1) ∘ fun x => a * x) (cocompact M) (cocompact M)
[PROOFSTEP]
simp only [comp_mul_left, ha, one_mul]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : b * a = 1
⊢ Tendsto (fun x => x) (cocompact M) (cocompact M)
[PROOFSTEP]
exact Filter.tendsto_id
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : a * b = 1
⊢ Tendsto (fun x => x * a) (cocompact M) (cocompact M)
[PROOFSTEP]
refine Filter.Tendsto.of_tendsto_comp ?_ (Filter.comap_cocompact_le (continuous_mul_right b))
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : a * b = 1
⊢ Tendsto ((fun b_1 => b_1 * b) ∘ fun x => x * a) (cocompact M) (cocompact M)
[PROOFSTEP]
simp only [comp_mul_right, ha, mul_one]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : a * b = 1
⊢ Tendsto (fun x => x) (cocompact M) (cocompact M)
[PROOFSTEP]
exact Filter.tendsto_id
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Monoid M
inst✝⁵ : ContinuousMul M
R : Type u_6
A : Type u_7
inst✝⁴ : Monoid A
inst✝³ : SMul R A
inst✝² : IsScalarTower R A A
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousMul A
q : R
⊢ Continuous fun x => q • x
[PROOFSTEP]
simp (config := { singlePass := true }) only [← smul_one_mul q (_ : A)]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Monoid M
inst✝⁵ : ContinuousMul M
R : Type u_6
A : Type u_7
inst✝⁴ : Monoid A
inst✝³ : SMul R A
inst✝² : IsScalarTower R A A
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousMul A
q : R
⊢ Continuous fun x => q • 1 * x
[PROOFSTEP]
exact continuous_const.mul continuous_id
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Monoid M
inst✝⁵ : ContinuousMul M
R : Type u_6
A : Type u_7
inst✝⁴ : Monoid A
inst✝³ : SMul R A
inst✝² : SMulCommClass R A A
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousMul A
q : R
⊢ Continuous fun x => q • x
[PROOFSTEP]
simp (config := { singlePass := true }) only [← mul_smul_one q (_ : A)]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Monoid M
inst✝⁵ : ContinuousMul M
R : Type u_6
A : Type u_7
inst✝⁴ : Monoid A
inst✝³ : SMul R A
inst✝² : SMulCommClass R A A
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousMul A
q : R
⊢ Continuous fun x => x * q • 1
[PROOFSTEP]
exact continuous_id.mul continuous_const
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
s : Multiset ι
⊢ (∀ (i : ι), i ∈ s → Tendsto (f i) x (𝓝 (a i))) →
    Tendsto (fun b => Multiset.prod (Multiset.map (fun c => f c b) s)) x (𝓝 (Multiset.prod (Multiset.map a s)))
[PROOFSTEP]
rcases s with ⟨l⟩
[GOAL]
case mk
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
s : Multiset ι
l : List ι
⊢ (∀ (i : ι), i ∈ Quot.mk Setoid.r l → Tendsto (f i) x (𝓝 (a i))) →
    Tendsto (fun b => Multiset.prod (Multiset.map (fun c => f c b) (Quot.mk Setoid.r l))) x
      (𝓝 (Multiset.prod (Multiset.map a (Quot.mk Setoid.r l))))
[PROOFSTEP]
simpa using tendsto_list_prod l
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
s : Multiset ι
⊢ (∀ (i : ι), i ∈ s → Continuous (f i)) → Continuous fun a => Multiset.prod (Multiset.map (fun i => f i a) s)
[PROOFSTEP]
rcases s with ⟨l⟩
[GOAL]
case mk
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
s : Multiset ι
l : List ι
⊢ (∀ (i : ι), i ∈ Quot.mk Setoid.r l → Continuous (f i)) →
    Continuous fun a => Multiset.prod (Multiset.map (fun i => f i a) (Quot.mk Setoid.r l))
[PROOFSTEP]
simpa using continuous_list_prod l
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
s : Multiset ι
t : Set X
⊢ (∀ (i : ι), i ∈ s → ContinuousOn (f i) t) → ContinuousOn (fun a => Multiset.prod (Multiset.map (fun i => f i a) s)) t
[PROOFSTEP]
rcases s with ⟨l⟩
[GOAL]
case mk
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
s : Multiset ι
t : Set X
l : List ι
⊢ (∀ (i : ι), i ∈ Quot.mk Setoid.r l → ContinuousOn (f i) t) →
    ContinuousOn (fun a => Multiset.prod (Multiset.map (fun i => f i a) (Quot.mk Setoid.r l))) t
[PROOFSTEP]
simpa using continuousOn_list_prod l
[GOAL]
ι : Type u_1
α : Type u_2
X✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
X : Type u_6
M : Type u_7
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ (i : ι), i ∈ s → f i =ᶠ[l] g i
⊢ ∏ i in s, f i =ᶠ[l] ∏ i in s, g i
[PROOFSTEP]
replace hs : ∀ᶠ x in l, ∀ i ∈ s, f i x = g i x
[GOAL]
case hs
ι : Type u_1
α : Type u_2
X✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
X : Type u_6
M : Type u_7
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ (i : ι), i ∈ s → f i =ᶠ[l] g i
⊢ ∀ᶠ (x : X) in l, ∀ (i : ι), i ∈ s → f i x = g i x
[PROOFSTEP]
rwa [eventually_all_finset]
[GOAL]
ι : Type u_1
α : Type u_2
X✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
X : Type u_6
M : Type u_7
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ᶠ (x : X) in l, ∀ (i : ι), i ∈ s → f i x = g i x
⊢ ∏ i in s, f i =ᶠ[l] ∏ i in s, g i
[PROOFSTEP]
filter_upwards [hs] with x hx
[GOAL]
case h
ι : Type u_1
α : Type u_2
X✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
X : Type u_6
M : Type u_7
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ᶠ (x : X) in l, ∀ (i : ι), i ∈ s → f i x = g i x
x : X
hx : ∀ (i : ι), i ∈ s → f i x = g i x
⊢ Finset.prod s (fun i => f i) x = Finset.prod s (fun i => g i) x
[PROOFSTEP]
simp only [Finset.prod_apply, Finset.prod_congr rfl hx]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
M : Type u_6
inst✝ : CommMonoid M
f : ι → X → M
hf : LocallyFinite fun i => mulSupport (f i)
x₀ : X
⊢ ∃ I, ∀ᶠ (x : X) in 𝓝 x₀, (mulSupport fun i => f i x) ⊆ ↑I
[PROOFSTEP]
rcases hf x₀ with ⟨U, hxU, hUf⟩
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
M : Type u_6
inst✝ : CommMonoid M
f : ι → X → M
hf : LocallyFinite fun i => mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ U)}
⊢ ∃ I, ∀ᶠ (x : X) in 𝓝 x₀, (mulSupport fun i => f i x) ⊆ ↑I
[PROOFSTEP]
refine' ⟨hUf.toFinset, mem_of_superset hxU fun y hy i hi => _⟩
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
M : Type u_6
inst✝ : CommMonoid M
f : ι → X → M
hf : LocallyFinite fun i => mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ U)}
y : X
hy : y ∈ U
i : ι
hi : i ∈ mulSupport fun i => f i y
⊢ i ∈ ↑(Finite.toFinset hUf)
[PROOFSTEP]
rw [hUf.coe_toFinset]
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
X : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M✝
inst✝² : CommMonoid M✝
inst✝¹ : ContinuousMul M✝
M : Type u_6
inst✝ : CommMonoid M
f : ι → X → M
hf : LocallyFinite fun i => mulSupport (f i)
x₀ : X
U : Set X
hxU : U ∈ 𝓝 x₀
hUf : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ U)}
y : X
hy : y ∈ U
i : ι
hi : i ∈ mulSupport fun i => f i y
⊢ i ∈ {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ U)}
[PROOFSTEP]
exact ⟨y, hi, hy⟩
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
⊢ Continuous fun x => ∏ᶠ (i : ι), f i x
[PROOFSTEP]
refine' continuous_iff_continuousAt.2 fun x => _
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
x : X
⊢ ContinuousAt (fun x => ∏ᶠ (i : ι), f i x) x
[PROOFSTEP]
rcases finprod_eventually_eq_prod hf x with ⟨s, hs⟩
[GOAL]
case intro
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
x : X
s : Finset ι
hs : ∀ᶠ (y : X) in 𝓝 x, ∏ᶠ (i : ι), f i y = ∏ i in s, f i y
⊢ ContinuousAt (fun x => ∏ᶠ (i : ι), f i x) x
[PROOFSTEP]
refine' ContinuousAt.congr _ (EventuallyEq.symm hs)
[GOAL]
case intro
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
x : X
s : Finset ι
hs : ∀ᶠ (y : X) in 𝓝 x, ∏ᶠ (i : ι), f i y = ∏ i in s, f i y
⊢ ContinuousAt (fun x => ∏ i in s, f i x) x
[PROOFSTEP]
exact tendsto_finset_prod _ fun i _ => (hc i).continuousAt
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
p : ι → Prop
hc : ∀ (i : ι), p i → Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
⊢ Continuous fun x => ∏ᶠ (i : ι) (_ : p i), f i x
[PROOFSTEP]
simp only [← finprod_subtype_eq_finprod_cond]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
p : ι → Prop
hc : ∀ (i : ι), p i → Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
⊢ Continuous fun x => ∏ᶠ (j : { i // p i }), f (↑j) x
[PROOFSTEP]
exact continuous_finprod (fun i => hc i i.2) (hf.comp_injective Subtype.coe_injective)
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : TopologicalSpace X
ι' : Sort u_6
inst✝ : Mul M
ts : ι' → TopologicalSpace M
h' : ∀ (i : ι'), ContinuousMul M
⊢ ContinuousMul M
[PROOFSTEP]
rw [← sInf_range]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : TopologicalSpace X
ι' : Sort u_6
inst✝ : Mul M
ts : ι' → TopologicalSpace M
h' : ∀ (i : ι'), ContinuousMul M
⊢ ContinuousMul M
[PROOFSTEP]
exact continuousMul_sInf (Set.forall_range_iff.mpr h')
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : TopologicalSpace X
ι' : Sort u_6
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul M
[PROOFSTEP]
rw [inf_eq_iInf]
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : TopologicalSpace X
ι' : Sort u_6
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul M
[PROOFSTEP]
refine' continuousMul_iInf fun b => _
[GOAL]
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : TopologicalSpace X
ι' : Sort u_6
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
b : Bool
⊢ ContinuousMul M
[PROOFSTEP]
cases b
[GOAL]
case false
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : TopologicalSpace X
ι' : Sort u_6
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul M
[PROOFSTEP]
assumption
[GOAL]
case true
ι : Type u_1
α : Type u_2
X : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : TopologicalSpace X
ι' : Sort u_6
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul M
[PROOFSTEP]
assumption
