case 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
V : Set Gᵐᵒᵖ
hV : V ∈ 𝓝 (op 1)
hV' : op '' K * V ⊆ op '' U
⊢ ∃ V, V ∈ 𝓝 1 ∧ V * K ⊆ 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 ∧ V * K ⊆ U
rcases compact_open_separated_mul_right (hK.image continuous_op) (opHomeomorph.isOpenMap U hU)
    (image_subset op hKU) with
  ⟨V, hV : V ∈ 𝓝 (op (1 : G)), hV' : op '' K * V ⊆ op '' U⟩
case 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
V : Set Gᵐᵒᵖ
hV : V ∈ 𝓝 (op 1)
hV' : op '' K * V ⊆ op '' U
⊢ op ⁻¹' V * K ⊆ U
case 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
V : Set Gᵐᵒᵖ
hV : V ∈ 𝓝 (op 1)
hV' : op '' K * V ⊆ op '' U
⊢ ∃ V, V ∈ 𝓝 1 ∧ V * K ⊆ U
refine' ⟨op ⁻¹' V, continuous_op.continuousAt hV, _⟩
no goals
case 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
V : Set Gᵐᵒᵖ
hV : V ∈ 𝓝 (op 1)
hV' : op '' K * V ⊆ op '' U
⊢ op ⁻¹' V * K ⊆ U
rwa [← image_preimage_eq V op_surjective, ← image_op_mul, image_subset_iff,
  preimage_image_eq _ op_injective] at hV'