case refine_1
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∃ V, V ∈ 𝓝 1 ∧ ∅ * V ⊆ U

case refine_2
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∀ ⦃s t : Set G⦄, s ⊆ t → (∃ V, V ∈ 𝓝 1 ∧ t * V ⊆ U) → ∃ V, V ∈ 𝓝 1 ∧ s * V ⊆ U

case refine_3
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∀ ⦃s t : Set G⦄, (∃ V, V ∈ 𝓝 1 ∧ s * V ⊆ U) → (∃ V, V ∈ 𝓝 1 ∧ t * V ⊆ U) → ∃ V, V ∈ 𝓝 1 ∧ (s ∪ t) * V ⊆ U

case refine_4
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∀ (x : G), x ∈ K → ∃ t, t ∈ 𝓝[K] x ∧ ∃ V, V ∈ 𝓝 1 ∧ t * V ⊆ U
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∃ V, V ∈ 𝓝 1 ∧ K * V ⊆ U
refine hK.induction_on ?_ ?_ ?_ ?_
no goals
case refine_1
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∃ V, V ∈ 𝓝 1 ∧ ∅ * V ⊆ U
exact ⟨univ, by simp⟩
no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ univ ∈ 𝓝 1 ∧ ∅ * univ ⊆ U
simp
case refine_2.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
s t : Set G
hst : s ⊆ t
V : Set G
hV : V ∈ 𝓝 1
hV' : t * V ⊆ U
⊢ ∃ V, V ∈ 𝓝 1 ∧ s * V ⊆ U
case refine_2
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∀ ⦃s t : Set G⦄, s ⊆ t → (∃ V, V ∈ 𝓝 1 ∧ t * V ⊆ U) → ∃ V, V ∈ 𝓝 1 ∧ s * V ⊆ U
rintro s t hst ⟨V, hV, hV'⟩
no goals
case refine_2.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
s t : Set G
hst : s ⊆ t
V : Set G
hV : V ∈ 𝓝 1
hV' : t * V ⊆ U
⊢ ∃ V, V ∈ 𝓝 1 ∧ s * V ⊆ U
exact ⟨V, hV, (mul_subset_mul_right hst).trans hV'⟩
case refine_3.intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
s t V : Set G
V_in : V ∈ 𝓝 1
hV' : s * V ⊆ U
W : Set G
W_in : W ∈ 𝓝 1
hW' : t * W ⊆ U
⊢ ∃ V, V ∈ 𝓝 1 ∧ (s ∪ t) * V ⊆ U
case refine_3
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∀ ⦃s t : Set G⦄, (∃ V, V ∈ 𝓝 1 ∧ s * V ⊆ U) → (∃ V, V ∈ 𝓝 1 ∧ t * V ⊆ U) → ∃ V, V ∈ 𝓝 1 ∧ (s ∪ t) * V ⊆ U
rintro s t ⟨V, V_in, hV'⟩ ⟨W, W_in, hW'⟩
case refine_3.intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
s t V : Set G
V_in : V ∈ 𝓝 1
hV' : s * V ⊆ U
W : Set G
W_in : W ∈ 𝓝 1
hW' : t * W ⊆ U
⊢ (s ∪ t) * (V ∩ W) ⊆ U
case refine_3.intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
s t V : Set G
V_in : V ∈ 𝓝 1
hV' : s * V ⊆ U
W : Set G
W_in : W ∈ 𝓝 1
hW' : t * W ⊆ U
⊢ ∃ V, V ∈ 𝓝 1 ∧ (s ∪ t) * V ⊆ U
use V ∩ W, inter_mem V_in W_in
case refine_3.intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
s t V : Set G
V_in : V ∈ 𝓝 1
hV' : s * V ⊆ U
W : Set G
W_in : W ∈ 𝓝 1
hW' : t * W ⊆ U
⊢ s * (V ∩ W) ∪ t * (V ∩ W) ⊆ U
case refine_3.intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
s t V : Set G
V_in : V ∈ 𝓝 1
hV' : s * V ⊆ U
W : Set G
W_in : W ∈ 𝓝 1
hW' : t * W ⊆ U
⊢ (s ∪ t) * (V ∩ W) ⊆ U
rw [union_mul]
no goals
case refine_3.intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
s t V : Set G
V_in : V ∈ 𝓝 1
hV' : s * V ⊆ U
W : Set G
W_in : W ∈ 𝓝 1
hW' : t * W ⊆ U
⊢ s * (V ∩ W) ∪ t * (V ∩ W) ⊆ U
exact
  union_subset ((mul_subset_mul_left (V.inter_subset_left W)).trans hV')
    ((mul_subset_mul_left (V.inter_subset_right W)).trans hW')
case refine_4
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
x : G
hx : x ∈ K
⊢ ∃ t, t ∈ 𝓝[K] x ∧ ∃ V, V ∈ 𝓝 1 ∧ t * V ⊆ U
case refine_4
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∀ (x : G), x ∈ K → ∃ t, t ∈ 𝓝[K] x ∧ ∃ V, V ∈ 𝓝 1 ∧ t * V ⊆ U
intro x hx
case refine_4
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
x : G
hx : x ∈ K
this : U ∈ map (fun p => p.fst * p.snd) (𝓝 (x, 1))
⊢ ∃ t, t ∈ 𝓝[K] x ∧ ∃ V, V ∈ 𝓝 1 ∧ t * V ⊆ U
case refine_4
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
x : G
hx : x ∈ K
⊢ ∃ t, t ∈ 𝓝[K] x ∧ ∃ V, V ∈ 𝓝 1 ∧ t * V ⊆ U
have := tendsto_mul (show U ∈ 𝓝 (x * 1) by simpa using hU.mem_nhds (hKU hx))
case refine_4
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
x : G
hx : x ∈ K
this : ∃ t₁, t₁ ∈ 𝓝 x ∧ ∃ t₂, t₂ ∈ 𝓝 1 ∧ t₁ ×ˢ t₂ ⊆ (fun p => p.fst * p.snd) ⁻¹' U
⊢ ∃ t, t ∈ 𝓝[K] x ∧ ∃ V, V ∈ 𝓝 1 ∧ t * V ⊆ U
case refine_4
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
x : G
hx : x ∈ K
this : U ∈ map (fun p => p.fst * p.snd) (𝓝 (x, 1))
⊢ ∃ t, t ∈ 𝓝[K] x ∧ ∃ V, V ∈ 𝓝 1 ∧ t * V ⊆ U
rw [nhds_prod_eq, mem_map, mem_prod_iff] at this
case refine_4.intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
x : G
hx : x ∈ K
t : Set G
ht : t ∈ 𝓝 x
s : Set G
hs : s ∈ 𝓝 1
h : t ×ˢ s ⊆ (fun p => p.fst * p.snd) ⁻¹' U
⊢ ∃ t, t ∈ 𝓝[K] x ∧ ∃ V, V ∈ 𝓝 1 ∧ t * V ⊆ U
case refine_4
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
x : G
hx : x ∈ K
this : ∃ t₁, t₁ ∈ 𝓝 x ∧ ∃ t₂, t₂ ∈ 𝓝 1 ∧ t₁ ×ˢ t₂ ⊆ (fun p => p.fst * p.snd) ⁻¹' U
⊢ ∃ t, t ∈ 𝓝[K] x ∧ ∃ V, V ∈ 𝓝 1 ∧ t * V ⊆ U
rcases this with ⟨t, ht, s, hs, h⟩
case refine_4.intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
x : G
hx : x ∈ K
t : Set G
ht : t ∈ 𝓝 x
s : Set G
hs : s ∈ 𝓝 1
h : t * s ⊆ U
⊢ ∃ t, t ∈ 𝓝[K] x ∧ ∃ V, V ∈ 𝓝 1 ∧ t * V ⊆ U
case refine_4.intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
x : G
hx : x ∈ K
t : Set G
ht : t ∈ 𝓝 x
s : Set G
hs : s ∈ 𝓝 1
h : t ×ˢ s ⊆ (fun p => p.fst * p.snd) ⁻¹' U
⊢ ∃ t, t ∈ 𝓝[K] x ∧ ∃ V, V ∈ 𝓝 1 ∧ t * V ⊆ U
rw [← image_subset_iff, image_mul_prod] at h
no goals
case refine_4.intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
x : G
hx : x ∈ K
t : Set G
ht : t ∈ 𝓝 x
s : Set G
hs : s ∈ 𝓝 1
h : t * s ⊆ U
⊢ ∃ t, t ∈ 𝓝[K] x ∧ ∃ V, V ∈ 𝓝 1 ∧ t * V ⊆ U
exact ⟨t, mem_nhdsWithin_of_mem_nhds ht, s, hs, h⟩
no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
x : G
hx : x ∈ K
⊢ U ∈ 𝓝 (x * 1)
simpa using hU.mem_nhds (hKU hx)