-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem compact_open_separated_mul_right {K U : Set G} (hK : IsCompact K) (hU : IsOpen U)
    (hKU : K ⊆ U) : ∃ V ∈ 𝓝 (1 : G), K * V ⊆ U

Proof state:
case refine_4.intro.intro.intro.intro
G : Type w
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 ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Tactic:
exact ⟨t, mem_nhdsWithin_of_mem_nhds ht, s, hs, h⟩

Result:
no goals

Proof state:
case refine_4
G : Type w
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 ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Tactic:
have := tendsto_mul (show U ∈ 𝓝 (x * 1) by simpa using hU.mem_nhds (hKU hx))

Result:
case refine_4
G : Type w
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.1 * p.2) (𝓝 (x, 1))
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Proof state:
case refine_2
G : Type w
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 ∈ 𝓝 1, t * V ⊆ U) → ∃ V ∈ 𝓝 1, s * V ⊆ U

Tactic:
rintro s t hst ⟨V, hV, hV'⟩

Result:
case refine_2.intro.intro
G : Type w
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 ∈ 𝓝 1, s * V ⊆ U

Proof state:
G : Type w
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)

Tactic:
simpa using hU.mem_nhds (hKU hx)

Result:
no goals

Proof state:
case refine_3.intro.intro.intro.intro
G : Type w
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 ∈ 𝓝 1, (s ∪ t) * V ⊆ U

Tactic:
use V ∩ W, inter_mem V_in W_in

Result:
case right
G : Type w
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

Proof state:
case refine_4.intro.intro.intro.intro
G : Type w
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.1 * p.2) ⁻¹' U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Tactic:
rw [← image_subset_iff, image_mul_prod] at h

Result:
case refine_4.intro.intro.intro.intro
G : Type w
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 ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Proof state:
case refine_1
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∃ V ∈ 𝓝 1, ∅ * V ⊆ U

Tactic:
exact ⟨univ, by simp⟩

Result:
no goals

Proof state:
case refine_2.intro.intro
G : Type w
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 ∈ 𝓝 1, s * V ⊆ U

Tactic:
exact ⟨V, hV, (mul_subset_mul_right hst).trans hV'⟩

Result:
no goals

Proof state:
case refine_4
G : Type w
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₁ ∈ 𝓝 x, ∃ t₂ ∈ 𝓝 1, t₁ ×ˢ t₂ ⊆ (fun p => p.1 * p.2) ⁻¹' U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Tactic:
rcases this with ⟨t, ht, s, hs, h⟩

Result:
case refine_4.intro.intro.intro.intro
G : Type w
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.1 * p.2) ⁻¹' U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Proof state:
case refine_4
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Tactic:
intro x hx

Result:
case refine_4
G : Type w
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 ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Proof state:
case refine_3
G : Type w
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 ∈ 𝓝 1, s * V ⊆ U) → (∃ V ∈ 𝓝 1, t * V ⊆ U) → ∃ V ∈ 𝓝 1, (s ∪ t) * V ⊆ U

Tactic:
rintro s t ⟨V, V_in, hV'⟩ ⟨W, W_in, hW'⟩

Result:
case refine_3.intro.intro.intro.intro
G : Type w
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 ∈ 𝓝 1, (s ∪ t) * V ⊆ U

Proof state:
case right
G : Type w
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

Tactic:
rw [union_mul]

Result:
case right
G : Type w
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

Proof state:
case refine_4
G : Type w
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.1 * p.2) (𝓝 (x, 1))
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Tactic:
rw [nhds_prod_eq, mem_map, mem_prod_iff] at this

Result:
case refine_4
G : Type w
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₁ ∈ 𝓝 x, ∃ t₂ ∈ 𝓝 1, t₁ ×ˢ t₂ ⊆ (fun p => p.1 * p.2) ⁻¹' U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Proof state:
case right
G : Type w
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

Tactic:
exact
  union_subset ((mul_subset_mul_left V.inter_subset_left).trans hV')
    ((mul_subset_mul_left V.inter_subset_right).trans hW')

Result:
no goals

Proof state:
G : Type w
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

Tactic:
simp

Result:
no goals