-- Mathlib/Topology/Algebra/Monoid.lean
theorem tendsto_mul_cocompact_nhds_zero [TopologicalSpace α] [TopologicalSpace β]
    {f : α → M} {g : β → M} (f_cont : Continuous f) (g_cont : Continuous g)
    (hf : Tendsto f (cocompact α) (𝓝 0)) (hg : Tendsto g (cocompact β) (𝓝 0)) :
    Tendsto (fun i : α × β ↦ f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)

Proof state:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝⁴ : TopologicalSpace M
inst✝³ : MulZeroClass M
inst✝² : ContinuousMul M
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous f
g_cont : Continuous g
hf : Tendsto f (cocompact α) (𝓝 0)
hg : Tendsto g (cocompact β) (𝓝 0)
l : Filter (M × M) := map (Prod.map f g) (cocompact (α × β))
l_def : l = map (Prod.map f g) (cocompact (α × β))
K : Set (M × M) := insert 0 (range f) ×ˢ insert 0 (range g)
K_compact : IsCompact K
K_mem_l : K ∈ l
⊢ Tendsto (fun i => f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)

Tactic:
have l_compact : Disjoint l (cocompact (M × M)) := by
  rw [disjoint_cocompact_right]
  exact ⟨K, K_mem_l, K_compact⟩

Result:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝⁴ : TopologicalSpace M
inst✝³ : MulZeroClass M
inst✝² : ContinuousMul M
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous f
g_cont : Continuous g
hf : Tendsto f (cocompact α) (𝓝 0)
hg : Tendsto g (cocompact β) (𝓝 0)
l : Filter (M × M) := map (Prod.map f g) (cocompact (α × β))
l_def : l = map (Prod.map f g) (cocompact (α × β))
K : Set (M × M) := insert 0 (range f) ×ˢ insert 0 (range g)
K_compact : IsCompact K
K_mem_l : K ∈ l
l_compact : Disjoint l (cocompact (M × M))
⊢ Tendsto (fun i => f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)

Proof state:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝⁴ : TopologicalSpace M
inst✝³ : MulZeroClass M
inst✝² : ContinuousMul M
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous f
g_cont : Continuous g
hf : Tendsto f (cocompact α) (𝓝 0)
hg : Tendsto g (cocompact β) (𝓝 0)
l : Filter (M × M) := map (Prod.map f g) (cocompact (α × β))
l_def : l = map (Prod.map f g) (cocompact (α × β))
K : Set (M × M) := insert 0 (range f) ×ˢ insert 0 (range g)
K_compact : IsCompact K
⊢ Tendsto (fun i => f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)

Tactic:
have K_mem_l : K ∈ l := eventually_map.mpr <| .of_forall fun ⟨x, y⟩ ↦
  ⟨mem_insert_of_mem _ (mem_range_self _), mem_insert_of_mem _ (mem_range_self _)⟩

Result:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝⁴ : TopologicalSpace M
inst✝³ : MulZeroClass M
inst✝² : ContinuousMul M
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous f
g_cont : Continuous g
hf : Tendsto f (cocompact α) (𝓝 0)
hg : Tendsto g (cocompact β) (𝓝 0)
l : Filter (M × M) := map (Prod.map f g) (cocompact (α × β))
l_def : l = map (Prod.map f g) (cocompact (α × β))
K : Set (M × M) := insert 0 (range f) ×ˢ insert 0 (range g)
K_compact : IsCompact K
K_mem_l : K ∈ l
⊢ Tendsto (fun i => f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)

Proof state:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝⁴ : TopologicalSpace M
inst✝³ : MulZeroClass M
inst✝² : ContinuousMul M
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous f
g_cont : Continuous g
hf : Tendsto f (cocompact α) (𝓝 0)
hg : Tendsto g (cocompact β) (𝓝 0)
l : Filter (M × M) := map (Prod.map f g) (cocompact (α × β))
l_def : l = map (Prod.map f g) (cocompact (α × β))
K : Set (M × M) := insert 0 (range f) ×ˢ insert 0 (range g)
K_compact : IsCompact K
K_mem_l : K ∈ l
l_compact : Disjoint l (cocompact (M × M))
⊢ l ≤ (𝓝 0).coprod (𝓝 0)

Tactic:
rw [l_def, ← coprod_cocompact]

Result:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝⁴ : TopologicalSpace M
inst✝³ : MulZeroClass M
inst✝² : ContinuousMul M
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous f
g_cont : Continuous g
hf : Tendsto f (cocompact α) (𝓝 0)
hg : Tendsto g (cocompact β) (𝓝 0)
l : Filter (M × M) := map (Prod.map f g) (cocompact (α × β))
l_def : l = map (Prod.map f g) (cocompact (α × β))
K : Set (M × M) := insert 0 (range f) ×ˢ insert 0 (range g)
K_compact : IsCompact K
K_mem_l : K ∈ l
l_compact : Disjoint l (cocompact (M × M))
⊢ map (Prod.map f g) ((cocompact α).coprod (cocompact β)) ≤ (𝓝 0).coprod (𝓝 0)

Proof state:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝⁴ : TopologicalSpace M
inst✝³ : MulZeroClass M
inst✝² : ContinuousMul M
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous f
g_cont : Continuous g
hf : Tendsto f (cocompact α) (𝓝 0)
hg : Tendsto g (cocompact β) (𝓝 0)
⊢ Tendsto (fun i => f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)

Tactic:
set l : Filter (M × M) := map (Prod.map f g) (cocompact (α × β)) with l_def

Result:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝⁴ : TopologicalSpace M
inst✝³ : MulZeroClass M
inst✝² : ContinuousMul M
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous f
g_cont : Continuous g
hf : Tendsto f (cocompact α) (𝓝 0)
hg : Tendsto g (cocompact β) (𝓝 0)
l : Filter (M × M) := map (Prod.map f g) (cocompact (α × β))
l_def : l = map (Prod.map f g) (cocompact (α × β))
⊢ Tendsto (fun i => f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)

Proof state:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝⁴ : TopologicalSpace M
inst✝³ : MulZeroClass M
inst✝² : ContinuousMul M
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous f
g_cont : Continuous g
hf : Tendsto f (cocompact α) (𝓝 0)
hg : Tendsto g (cocompact β) (𝓝 0)
l : Filter (M × M) := map (Prod.map f g) (cocompact (α × β))
l_def : l = map (Prod.map f g) (cocompact (α × β))
K : Set (M × M) := insert 0 (range f) ×ˢ insert 0 (range g)
⊢ Tendsto (fun i => f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)

Tactic:
have K_compact : IsCompact K := .prod (hf.isCompact_insert_range_of_cocompact f_cont)
  (hg.isCompact_insert_range_of_cocompact g_cont)

Result:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝⁴ : TopologicalSpace M
inst✝³ : MulZeroClass M
inst✝² : ContinuousMul M
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous f
g_cont : Continuous g
hf : Tendsto f (cocompact α) (𝓝 0)
hg : Tendsto g (cocompact β) (𝓝 0)
l : Filter (M × M) := map (Prod.map f g) (cocompact (α × β))
l_def : l = map (Prod.map f g) (cocompact (α × β))
K : Set (M × M) := insert 0 (range f) ×ˢ insert 0 (range g)
K_compact : IsCompact K
⊢ Tendsto (fun i => f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)

Proof state:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝⁴ : TopologicalSpace M
inst✝³ : MulZeroClass M
inst✝² : ContinuousMul M
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous f
g_cont : Continuous g
hf : Tendsto f (cocompact α) (𝓝 0)
hg : Tendsto g (cocompact β) (𝓝 0)
l : Filter (M × M) := map (Prod.map f g) (cocompact (α × β))
l_def : l = map (Prod.map f g) (cocompact (α × β))
K : Set (M × M) := insert 0 (range f) ×ˢ insert 0 (range g)
K_compact : IsCompact K
K_mem_l : K ∈ l
l_compact : Disjoint l (cocompact (M × M))
⊢ Tendsto (fun i => f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)

Tactic:
have l_le_coprod : l ≤ (𝓝 0).coprod (𝓝 0) := by
  rw [l_def, ← coprod_cocompact]
  exact hf.prod_map_coprod hg

Result:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝⁴ : TopologicalSpace M
inst✝³ : MulZeroClass M
inst✝² : ContinuousMul M
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous f
g_cont : Continuous g
hf : Tendsto f (cocompact α) (𝓝 0)
hg : Tendsto g (cocompact β) (𝓝 0)
l : Filter (M × M) := map (Prod.map f g) (cocompact (α × β))
l_def : l = map (Prod.map f g) (cocompact (α × β))
K : Set (M × M) := insert 0 (range f) ×ˢ insert 0 (range g)
K_compact : IsCompact K
K_mem_l : K ∈ l
l_compact : Disjoint l (cocompact (M × M))
l_le_coprod : l ≤ (𝓝 0).coprod (𝓝 0)
⊢ Tendsto (fun i => f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)