-- Mathlib/Topology/Algebra/Monoid.lean
theorem exists_mem_nhds_zero_mul_subset
    {K U : Set M} (hK : IsCompact K) (hU : U ∈ 𝓝 0) : ∃ V ∈ 𝓝 0, K * V ⊆ U

Proof state:
case refine_4
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
x : M
hx : x ∈ K
this : U ∈ map (fun p => p.1 * p.2) (𝓝 (x, 0))
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U

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

Result:
case refine_4
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
x : M
hx : x ∈ K
this : ∃ t₁ ∈ 𝓝 x, ∃ t₂ ∈ 𝓝 0, t₁ ×ˢ t₂ ⊆ (fun p => p.1 * p.2) ⁻¹' U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U

Proof state:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
x : M
hx : x ∈ K
⊢ U ∈ 𝓝 (x * 0)

Tactic:
simpa using hU

Result:
no goals

Proof state:
case refine_2
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∀ ⦃s t : Set M⦄, s ⊆ t → (∃ V ∈ 𝓝 0, t * V ⊆ U) → ∃ V ∈ 𝓝 0, s * V ⊆ U

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

Result:
case refine_2.intro.intro
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
s t : Set M
hst : s ⊆ t
V : Set M
hV : V ∈ 𝓝 0
hV' : t * V ⊆ U
⊢ ∃ V ∈ 𝓝 0, s * V ⊆ U

Proof state:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∃ V ∈ 𝓝 0, K * V ⊆ U

Tactic:
refine hK.induction_on ?_ ?_ ?_ ?_

Result:
case refine_1
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∃ V ∈ 𝓝 0, ∅ * V ⊆ U

case refine_2
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∀ ⦃s t : Set M⦄, s ⊆ t → (∃ V ∈ 𝓝 0, t * V ⊆ U) → ∃ V ∈ 𝓝 0, s * V ⊆ U

case refine_3
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∀ ⦃s t : Set M⦄, (∃ V ∈ 𝓝 0, s * V ⊆ U) → (∃ V ∈ 𝓝 0, t * V ⊆ U) → ∃ V ∈ 𝓝 0, (s ∪ t) * V ⊆ U

case refine_4
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U

Proof state:
case right
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
s t V : Set M
V_in : V ∈ 𝓝 0
hV' : s * V ⊆ U
W : Set M
W_in : W ∈ 𝓝 0
hW' : t * W ⊆ U
⊢ (s ∪ t) * (V ∩ W) ⊆ U

Tactic:
rw [union_mul]

Result:
case right
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
s t V : Set M
V_in : V ∈ 𝓝 0
hV' : s * V ⊆ U
W : Set M
W_in : W ∈ 𝓝 0
hW' : t * W ⊆ U
⊢ s * (V ∩ W) ∪ t * (V ∩ W) ⊆ U

Proof state:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ univ ∈ 𝓝 0 ∧ ∅ * univ ⊆ U

Tactic:
simp

Result:
no goals

Proof state:
case refine_4.intro.intro.intro.intro
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
x : M
hx : x ∈ K
t : Set M
ht : t ∈ 𝓝 x
s : Set M
hs : s ∈ 𝓝 0
h : t ×ˢ s ⊆ (fun p => p.1 * p.2) ⁻¹' U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U

Tactic:
rw [← image_subset_iff, image_mul_prod] at h

Result:
case refine_4.intro.intro.intro.intro
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
x : M
hx : x ∈ K
t : Set M
ht : t ∈ 𝓝 x
s : Set M
hs : s ∈ 𝓝 0
h : t * s ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U

Proof state:
case refine_4
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
x : M
hx : x ∈ K
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U

Tactic:
have := tendsto_mul (show U ∈ 𝓝 (x * 0) by simpa using hU)

Result:
case refine_4
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
x : M
hx : x ∈ K
this : U ∈ map (fun p => p.1 * p.2) (𝓝 (x, 0))
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U

Proof state:
case refine_3
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∀ ⦃s t : Set M⦄, (∃ V ∈ 𝓝 0, s * V ⊆ U) → (∃ V ∈ 𝓝 0, t * V ⊆ U) → ∃ V ∈ 𝓝 0, (s ∪ t) * V ⊆ U

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

Result:
case refine_3.intro.intro.intro.intro
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
s t V : Set M
V_in : V ∈ 𝓝 0
hV' : s * V ⊆ U
W : Set M
W_in : W ∈ 𝓝 0
hW' : t * W ⊆ U
⊢ ∃ V ∈ 𝓝 0, (s ∪ t) * V ⊆ U

Proof state:
case right
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
s t V : Set M
V_in : V ∈ 𝓝 0
hV' : s * V ⊆ U
W : Set M
W_in : W ∈ 𝓝 0
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:
case refine_2.intro.intro
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
s t : Set M
hst : s ⊆ t
V : Set M
hV : V ∈ 𝓝 0
hV' : t * V ⊆ U
⊢ ∃ V ∈ 𝓝 0, s * V ⊆ U

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

Result:
no goals

Proof state:
case refine_4
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
x : M
hx : x ∈ K
this : ∃ t₁ ∈ 𝓝 x, ∃ t₂ ∈ 𝓝 0, t₁ ×ˢ t₂ ⊆ (fun p => p.1 * p.2) ⁻¹' U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U

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

Result:
case refine_4.intro.intro.intro.intro
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
x : M
hx : x ∈ K
t : Set M
ht : t ∈ 𝓝 x
s : Set M
hs : s ∈ 𝓝 0
h : t ×ˢ s ⊆ (fun p => p.1 * p.2) ⁻¹' U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U

Proof state:
case refine_1
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∃ V ∈ 𝓝 0, ∅ * V ⊆ U

Tactic:
exact ⟨univ, by simp⟩

Result:
no goals

Proof state:
case refine_4
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U

Tactic:
intro x hx

Result:
case refine_4
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
x : M
hx : x ∈ K
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U

Proof state:
case refine_4.intro.intro.intro.intro
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
x : M
hx : x ∈ K
t : Set M
ht : t ∈ 𝓝 x
s : Set M
hs : s ∈ 𝓝 0
h : t * s ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U

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

Result:
no goals