-- Mathlib/Topology/Algebra/Monoid.lean
theorem tendsto_mul_cofinite_nhds_zero {f : α → M} {g : β → M}
    (hf : Tendsto f cofinite (𝓝 0)) (hg : Tendsto g cofinite (𝓝 0)) :
    Tendsto (fun i : α × β ↦ f i.1 * g i.2) cofinite (𝓝 0)

Proof state:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
f : α → M
g : β → M
hf : Tendsto f cofinite (𝓝 0)
hg : Tendsto g cofinite (𝓝 0)
this : TopologicalSpace α := ⊥
⊢ Tendsto (fun i => f i.1 * g i.2) cofinite (𝓝 0)

Tactic:
haveI : DiscreteTopology α := discreteTopology_bot α

Result:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
f : α → M
g : β → M
hf : Tendsto f cofinite (𝓝 0)
hg : Tendsto g cofinite (𝓝 0)
this✝ : TopologicalSpace α := ⊥
this : DiscreteTopology α
⊢ Tendsto (fun i => f i.1 * g i.2) cofinite (𝓝 0)

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

Tactic:
exact tendsto_mul_cocompact_nhds_zero
  continuous_of_discreteTopology continuous_of_discreteTopology hf hg

Result:
no goals

Proof state:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
f : α → M
g : β → M
hf : Tendsto f cofinite (𝓝 0)
hg : Tendsto g cofinite (𝓝 0)
this✝ : TopologicalSpace α := ⊥
this : DiscreteTopology α
⊢ Tendsto (fun i => f i.1 * g i.2) cofinite (𝓝 0)

Tactic:
letI : TopologicalSpace β := ⊥

Result:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
f : α → M
g : β → M
hf : Tendsto f cofinite (𝓝 0)
hg : Tendsto g cofinite (𝓝 0)
this✝¹ : TopologicalSpace α := ⊥
this✝ : DiscreteTopology α
this : TopologicalSpace β := ⊥
⊢ Tendsto (fun i => f i.1 * g i.2) cofinite (𝓝 0)

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

Tactic:
letI : TopologicalSpace α := ⊥

Result:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
f : α → M
g : β → M
hf : Tendsto f cofinite (𝓝 0)
hg : Tendsto g cofinite (𝓝 0)
this : TopologicalSpace α := ⊥
⊢ Tendsto (fun i => f i.1 * g i.2) cofinite (𝓝 0)

Proof state:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
f : α → M
g : β → M
hf : Tendsto f cofinite (𝓝 0)
hg : Tendsto g cofinite (𝓝 0)
this✝² : TopologicalSpace α := ⊥
this✝¹ : DiscreteTopology α
this✝ : TopologicalSpace β := ⊥
this : DiscreteTopology β
⊢ Tendsto (fun i => f i.1 * g i.2) cofinite (𝓝 0)

Tactic:
rw [← cocompact_eq_cofinite] at *

Result:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
f : α → M
g : β → M
this✝² : TopologicalSpace α := ⊥
hf : Tendsto f (cocompact α) (𝓝 0)
this✝¹ : DiscreteTopology α
this✝ : TopologicalSpace β := ⊥
hg : Tendsto g (cocompact β) (𝓝 0)
this : DiscreteTopology β
⊢ 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
f : α → M
g : β → M
hf : Tendsto f cofinite (𝓝 0)
hg : Tendsto g cofinite (𝓝 0)
this✝¹ : TopologicalSpace α := ⊥
this✝ : DiscreteTopology α
this : TopologicalSpace β := ⊥
⊢ Tendsto (fun i => f i.1 * g i.2) cofinite (𝓝 0)

Tactic:
haveI : DiscreteTopology β := discreteTopology_bot β

Result:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
f : α → M
g : β → M
hf : Tendsto f cofinite (𝓝 0)
hg : Tendsto g cofinite (𝓝 0)
this✝² : TopologicalSpace α := ⊥
this✝¹ : DiscreteTopology α
this✝ : TopologicalSpace β := ⊥
this : DiscreteTopology β
⊢ Tendsto (fun i => f i.1 * g i.2) cofinite (𝓝 0)