awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : Membership.mem (γ := Filter M) (𝓝 0) U
x : M
hx : x ∈ K
this : Membership.mem (γ := Filter M) (map (fun (p : M × M) ↦ p.1 * p.2) (𝓝 (x, 0))) U
⊢ ∃ t₁ ∈ 𝓝 x, ∃ (t₂ : Set M), Membership.mem (γ := Filter M) (𝓝 0) t₂ ∧ t₁ ×ˢ t₂ ⊆ (fun (p : M × M) ↦ p.1 * p.2) ⁻¹' U

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

Premises used: nhds_prod_eq, Filter.mem_prod_iff, Filter.mem_map
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : Membership.mem (γ := Filter M) (𝓝 0) U
x : M
hx : x ∈ K
this :
  ∃ t₁ ∈ 𝓝 x, ∃ (t₂ : Set M), Membership.mem (γ := Filter M) (𝓝 0) t₂ ∧ t₁ ×ˢ t₂ ⊆ (fun (p : M × M) ↦ p.1 * p.2) ⁻¹' U
refine_4 :
  ∀ (t : Set M) (ht : t ∈ 𝓝 x) (s : Set M) (hs : Membership.mem (γ := Filter M) (𝓝 0) s)
    (h : t ×ˢ s ⊆ (fun (p : M × M) ↦ p.1 * p.2) ⁻¹' U),
    ∃ t ∈ 𝓝[K] x, ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ t * V ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ t * V ⊆ U

Tactic:
rcases this with ⟨t, ht, s, hs, h⟩
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : Membership.mem (γ := Filter M) (𝓝 0) U
x : M
hx : x ∈ K
t : Set M
ht : t ∈ 𝓝 x
s : Set M
hs : Membership.mem (γ := Filter M) (𝓝 0) s
h : t ×ˢ s ⊆ (fun (p : M × M) ↦ p.1 * p.2) ⁻¹' U
⊢ t * s ⊆ U

Tactic:
rw [← image_subset_iff, image_mul_prod] at h

Premises used: Set.image_mul_prod, Set.image_subset_iff
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : Membership.mem (γ := Filter M) (𝓝 0) U
x : M
hx : x ∈ K
t : Set M
ht : t ∈ 𝓝 x
s : Set M
hs : Membership.mem (γ := Filter M) (𝓝 0) s
h : t * s ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ t * V ⊆ U

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

Premises used: mem_nhdsWithin_of_mem_nhds, And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : Membership.mem (γ := Filter M) (𝓝 0) U
x : M
hx : x ∈ K
t : Set M
ht : t ∈ 𝓝 x
s : Set M
hs : Membership.mem (γ := Filter M) (𝓝 0) s
h : t * s ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ t * V ⊆ U

Tactic:
exact ⟨t, mem_nhdsWithin_of_mem_nhds ht, s, hs, h⟩
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
l : Filter M
hl : Disjoint l (cocompact M)
⊢ Tendsto (β := M) (fun (x : M × M) ↦ x.1 * x.2) (SProd.sprod (α := Filter M) (𝓝 0) l) (𝓝 0)

Tactic:
calc
  map (fun x : M × M ↦ x.1 * x.2) (𝓝 0 ×ˢ l)
  _ ≤ map (fun x : M × M ↦ x.1 * x.2) (𝓝ˢ ({0} ×ˢ Set.univ)) :=
    map_mono <| nhds_prod_le_of_disjoint_cocompact 0 hl
  _ ≤ 𝓝 0 := continuous_mul.tendsto_nhdsSet_nhds fun _ ⟨hx, _⟩ ↦ mul_eq_zero_of_left hx _

Premises used: Continuous.tendsto_nhdsSet_nhds, Filter.map_mono, Trans.trans, HMul.hMul, continuous_mul, nhds_prod_le_of_disjoint_cocompact, mul_eq_zero_of_left, Prod.fst, Filter.Tendsto, _private.0.tendsto_mul_nhds_zero_prod_of_disjoint_cocompact.match_1, OfNat.ofNat, Eq, Prod.snd, rfl
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
l : Filter M
hl : Disjoint l (cocompact M)
⊢ Tendsto (β := M) (fun (x : M × M) ↦ x.1 * x.2) (SProd.sprod (β := Filter M) l (𝓝 0)) (𝓝 0)

Tactic:
calc
  map (fun x : M × M ↦ x.1 * x.2) (l ×ˢ 𝓝 0)
  _ ≤ map (fun x : M × M ↦ x.1 * x.2) (𝓝ˢ (Set.univ ×ˢ {0})) :=
    map_mono <| prod_nhds_le_of_disjoint_cocompact 0 hl
  _ ≤ 𝓝 0 := continuous_mul.tendsto_nhdsSet_nhds fun _ ⟨_, hx⟩ ↦ mul_eq_zero_of_right _ hx

Premises used: Continuous.tendsto_nhdsSet_nhds, prod_nhds_le_of_disjoint_cocompact, Filter.map_mono, Trans.trans, HMul.hMul, continuous_mul, mul_eq_zero_of_right, Prod.fst, Filter.Tendsto, _private.0.tendsto_mul_prod_nhds_zero_of_disjoint_cocompact.match_1, OfNat.ofNat, Eq, Prod.snd, rfl
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
⊢ Filter.coprod (𝓝 0) (𝓝 0) ⊓ l ≤
    SProd.sprod (α := Filter M) (𝓝 0) (map Prod.snd l) ⊔ SProd.sprod (β := Filter M) (map Prod.fst l) (𝓝 0)

Tactic:
have := calc
    (𝓝 0).coprod (𝓝 0) ⊓ l
    _ ≤ (𝓝 0).coprod (𝓝 0) ⊓ map Prod.fst l ×ˢ map Prod.snd l :=
      inf_le_inf_left _ le_prod_map_fst_snd
    _ ≤ 𝓝 0 ×ˢ map Prod.snd l ⊔ map Prod.fst l ×ˢ 𝓝 0 :=
      coprod_inf_prod_le _ _ _ _
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
this :
  Filter.coprod (𝓝 0) (𝓝 0) ⊓ l ≤
    SProd.sprod (α := Filter M) (𝓝 0) (map Prod.snd l) ⊔ SProd.sprod (β := Filter M) (map Prod.fst l) (𝓝 0)
apply : Tendsto (β := M) (fun (x : M × M) ↦ x.1 * x.2) (SProd.sprod (α := Filter M) (𝓝 0) (map Prod.snd l)) (𝓝 0)
apply₁ : Tendsto (β := M) (fun (x : M × M) ↦ x.1 * x.2) (SProd.sprod (β := Filter M) (map Prod.fst l) (𝓝 0)) (𝓝 0)
⊢ Tendsto (β := M) (fun (x : M × M) ↦ x.1 * x.2) (Filter.coprod (𝓝 0) (𝓝 0) ⊓ l) (𝓝 0)

Tactic:
apply (Tendsto.sup _ _).mono_left this

Premises used: Filter.Tendsto.sup, Filter.Tendsto.mono_left
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
this :
  Filter.coprod (𝓝 0) (𝓝 0) ⊓ l ≤
    SProd.sprod (α := Filter M) (𝓝 0) (map Prod.snd l) ⊔ SProd.sprod (β := Filter M) (map Prod.fst l) (𝓝 0)
hl₁ : Disjoint (map Prod.snd l) (cocompact M)
⊢ Tendsto (β := M) (fun (x : M × M) ↦ x.1 * x.2) (SProd.sprod (α := Filter M) (𝓝 0) (map Prod.snd l)) (𝓝 0)

Tactic:
apply tendsto_mul_nhds_zero_prod_of_disjoint_cocompact

Premises used: tendsto_mul_nhds_zero_prod_of_disjoint_cocompact
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
this :
  Filter.coprod (𝓝 0) (𝓝 0) ⊓ l ≤
    SProd.sprod (α := Filter M) (𝓝 0) (map Prod.snd l) ⊔ SProd.sprod (β := Filter M) (map Prod.fst l) (𝓝 0)
⊢ Disjoint (map Prod.snd l) (cocompact M)

Tactic:
disjoint_map_cocompact continuous_snd hl

Premises used: continuous_snd, disjoint_map_cocompact
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
this :
  Filter.coprod (𝓝 0) (𝓝 0) ⊓ l ≤
    SProd.sprod (α := Filter M) (𝓝 0) (map Prod.snd l) ⊔ SProd.sprod (β := Filter M) (map Prod.fst l) (𝓝 0)
⊢ Disjoint (map Prod.snd l) (cocompact M)

Tactic:
exact disjoint_map_cocompact continuous_snd hl

Premises used: continuous_snd, disjoint_map_cocompact
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
this :
  Filter.coprod (𝓝 0) (𝓝 0) ⊓ l ≤
    SProd.sprod (α := Filter M) (𝓝 0) (map Prod.snd l) ⊔ SProd.sprod (β := Filter M) (map Prod.fst l) (𝓝 0)
hl₁ : Disjoint (map Prod.fst l) (cocompact M)
⊢ Tendsto (β := M) (fun (x : M × M) ↦ x.1 * x.2) (SProd.sprod (β := Filter M) (map Prod.fst l) (𝓝 0)) (𝓝 0)

Tactic:
apply tendsto_mul_prod_nhds_zero_of_disjoint_cocompact

Premises used: tendsto_mul_prod_nhds_zero_of_disjoint_cocompact
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
this :
  Filter.coprod (𝓝 0) (𝓝 0) ⊓ l ≤
    SProd.sprod (α := Filter M) (𝓝 0) (map Prod.snd l) ⊔ SProd.sprod (β := Filter M) (map Prod.fst l) (𝓝 0)
⊢ Disjoint (map Prod.fst l) (cocompact M)

Tactic:
disjoint_map_cocompact continuous_fst hl

Premises used: continuous_fst, disjoint_map_cocompact
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
this :
  Filter.coprod (𝓝 0) (𝓝 0) ⊓ l ≤
    SProd.sprod (α := Filter M) (𝓝 0) (map Prod.snd l) ⊔ SProd.sprod (β := Filter M) (map Prod.fst l) (𝓝 0)
⊢ Disjoint (map Prod.fst l) (cocompact M)

Tactic:
exact disjoint_map_cocompact continuous_fst hl

Premises used: continuous_fst, disjoint_map_cocompact
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
h'l : l ≤ Filter.coprod (𝓝 0) (𝓝 0)
⊢ Tendsto (β := M) (fun (x : M × M) ↦ x.1 * x.2) l (𝓝 0)

Tactic:
simpa [inf_eq_right.mpr h'l] using tendsto_mul_coprod_nhds_zero_inf_of_disjoint_cocompact hl

Premises used: Iff.mpr, tendsto_mul_coprod_nhds_zero_inf_of_disjoint_cocompact, inf_eq_right
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
α : Type u_6
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
f g : α → M
l : Filter α
hf : Tendsto f l (𝓝 0)
hg : Disjoint (map g l) (cocompact M)
⊢ Tendsto.{u_6, u_3} (β := M) (fun (x : α) ↦ f x * g x) l (𝓝 0)

Tactic:
tendsto_mul_nhds_zero_prod_of_disjoint_cocompact hg |>.comp (hf.prodMk tendsto_map)

Premises used: Filter.tendsto_map, Filter.Tendsto.prodMk, Filter.Tendsto.comp, tendsto_mul_nhds_zero_prod_of_disjoint_cocompact
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
α : Type u_6
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
f g : α → M
l : Filter α
hf : Disjoint (map f l) (cocompact M)
hg : Tendsto g l (𝓝 0)
⊢ Tendsto.{u_6, u_3} (β := M) (fun (x : α) ↦ f x * g x) l (𝓝 0)

Tactic:
tendsto_mul_prod_nhds_zero_of_disjoint_cocompact hf |>.comp (tendsto_map.prodMk hg)

Premises used: Filter.tendsto_map, tendsto_mul_prod_nhds_zero_of_disjoint_cocompact, Filter.Tendsto.prodMk, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
α : Type u_6
β : Type u_7
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
inst_3 : TopologicalSpace α
inst_4 : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous[inst_3, inst] f
g_cont : Continuous[inst_4, inst] g
hf : Tendsto f (cocompact α) (𝓝 0)
hg : Tendsto g (cocompact β) (𝓝 0)
⊢ let l := map (Prod.map f g) (cocompact (α × β));
  l = map (Prod.map f g) (cocompact (α × β))

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

Premises used: Filter.map, Prod.map, Filter.cocompact, Prod, Filter
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
α : Type u_6
β : Type u_7
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
inst_3 : TopologicalSpace α
inst_4 : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous[inst_3, inst] f
g_cont : Continuous[inst_4, inst] 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)
⊢ IsCompact K

Tactic:
have K_compact : IsCompact K := .prod (hf.isCompact_insert_range_of_cocompact f_cont)
    (hg.isCompact_insert_range_of_cocompact g_cont)
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
α : Type u_6
β : Type u_7
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
inst_3 : TopologicalSpace α
inst_4 : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous[inst_3, inst] f
g_cont : Continuous[inst_4, inst] 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 ∈ l

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 _)⟩
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
α : Type u_6
β : Type u_7
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
inst_3 : TopologicalSpace α
inst_4 : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous[inst_3, inst] f
g_cont : Continuous[inst_4, inst] 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
rw : ∃ K ∈ l, IsCompact K
⊢ Disjoint l (cocompact (M × M))

Tactic:
rw [disjoint_cocompact_right]

Premises used: Filter.disjoint_cocompact_right
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
α : Type u_6
β : Type u_7
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
inst_3 : TopologicalSpace α
inst_4 : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous[inst_3, inst] f
g_cont : Continuous[inst_4, inst] 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
⊢ ∃ K ∈ l, IsCompact K

Tactic:
⟨K, K_mem_l, K_compact⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
α : Type u_6
β : Type u_7
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
inst_3 : TopologicalSpace α
inst_4 : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous[inst_3, inst] f
g_cont : Continuous[inst_4, inst] 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
⊢ ∃ K ∈ l, IsCompact K

Tactic:
exact ⟨K, K_mem_l, K_compact⟩
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
α : Type u_6
β : Type u_7
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
inst_3 : TopologicalSpace α
inst_4 : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous[inst_3, inst] f
g_cont : Continuous[inst_4, inst] 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
⊢ Disjoint l (cocompact (M × M))

Tactic:
have l_compact : Disjoint l (cocompact (M × M)) := by
    rw [disjoint_cocompact_right]
    exact ⟨K, K_mem_l, K_compact⟩
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
α : Type u_6
β : Type u_7
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
inst_3 : TopologicalSpace α
inst_4 : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous[inst_3, inst] f
g_cont : Continuous[inst_4, inst] 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))
rw : map (Prod.map f g) ((cocompact α).coprod (cocompact β)) ≤ Filter.coprod (𝓝 0) (𝓝 0)
⊢ l ≤ Filter.coprod (𝓝 0) (𝓝 0)

Tactic:
rw [l_def, ← coprod_cocompact]

Premises used: Filter.coprod_cocompact
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
α : Type u_6
β : Type u_7
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
inst_3 : TopologicalSpace α
inst_4 : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous[inst_3, inst] f
g_cont : Continuous[inst_4, inst] 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 β)) ≤ Filter.coprod (𝓝 0) (𝓝 0)

Tactic:
hf.prodMap_coprod hg

Premises used: Filter.Tendsto.prodMap_coprod, Filter.Tendsto
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
α : Type u_6
β : Type u_7
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
inst_3 : TopologicalSpace α
inst_4 : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous[inst_3, inst] f
g_cont : Continuous[inst_4, inst] 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 β)) ≤ Filter.coprod (𝓝 0) (𝓝 0)

Tactic:
exact hf.prodMap_coprod hg

Premises used: Filter.Tendsto.prodMap_coprod
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
α : Type u_6
β : Type u_7
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
inst_3 : TopologicalSpace α
inst_4 : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous[inst_3, inst] f
g_cont : Continuous[inst_4, inst] 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 ≤ Filter.coprod (𝓝 0) (𝓝 0)

Tactic:
have l_le_coprod : l ≤ (𝓝 0).coprod (𝓝 0) := by
    rw [l_def, ← coprod_cocompact]
    exact hf.prodMap_coprod hg
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
α : Type u_6
β : Type u_7
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
inst_3 : TopologicalSpace α
inst_4 : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous[inst_3, inst] f
g_cont : Continuous[inst_4, inst] 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 ≤ Filter.coprod (𝓝 0) (𝓝 0)
⊢ Tendsto (β := M) (fun (i : α × β) ↦ f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)

Tactic:
tendsto_mul_nhds_zero_of_disjoint_cocompact l_compact l_le_coprod |>.comp tendsto_map

Premises used: Filter.tendsto_map, tendsto_mul_nhds_zero_of_disjoint_cocompact, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
α : Type u_6
β : Type u_7
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
inst_3 : TopologicalSpace α
inst_4 : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous[inst_3, inst] f
g_cont : Continuous[inst_4, inst] 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 ≤ Filter.coprod (𝓝 0) (𝓝 0)
⊢ Tendsto (β := M) (fun (i : α × β) ↦ f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)

Tactic:
exact tendsto_mul_nhds_zero_of_disjoint_cocompact l_compact l_le_coprod |>.comp tendsto_map

Premises used: Filter.tendsto_map, tendsto_mul_nhds_zero_of_disjoint_cocompact, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
α : Type u_6
β : Type u_7
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
f : α → M
g : β → M
hf : Tendsto f cofinite (𝓝 0)
hg : Tendsto g cofinite (𝓝 0)
this : TopologicalSpace α := ⊥
⊢ DiscreteTopology α

Tactic:
haveI : DiscreteTopology α := discreteTopology_bot α
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
α : Type u_6
β : Type u_7
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
f : α → M
g : β → M
hf : Tendsto f cofinite (𝓝 0)
hg : Tendsto g cofinite (𝓝 0)
this_1 : TopologicalSpace α := ⊥
this_2 : DiscreteTopology α
this : TopologicalSpace β := ⊥
⊢ DiscreteTopology β

Tactic:
haveI : DiscreteTopology β := discreteTopology_bot β
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
α : Type u_6
β : Type u_7
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
f : α → M
g : β → M
hf : Tendsto f cofinite (𝓝 0)
hg : Tendsto g cofinite (𝓝 0)
this_1 : TopologicalSpace α := ⊥
this_2 : DiscreteTopology α
this_3 : TopologicalSpace β := ⊥
this : DiscreteTopology β
rw :
  ∀ (hf : Tendsto f (cocompact α) (𝓝 0)) (this : DiscreteTopology α),
    let this : TopologicalSpace β := ⊥;
    ∀ (hg : Tendsto g (cocompact β) (𝓝 0)) (this_4 : DiscreteTopology β),
      Tendsto (β := M) (fun (i : α × β) ↦ f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)
⊢ Tendsto (β := M) (fun (i : α × β) ↦ f i.1 * g i.2) cofinite (𝓝 0)

Tactic:
rw [← cocompact_eq_cofinite] at *

Premises used: Filter.cocompact_eq_cofinite
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
α : Type u_6
β : Type u_7
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
f : α → M
g : β → M
this_1 : TopologicalSpace α := ⊥
hf : Tendsto f (cocompact α) (𝓝 0)
this_2 : DiscreteTopology α
this_3 : TopologicalSpace β := ⊥
hg : Tendsto g (cocompact β) (𝓝 0)
this : DiscreteTopology β
⊢ Tendsto (β := M) (fun (i : α × β) ↦ f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)

Tactic:
tendsto_mul_cocompact_nhds_zero
    continuous_of_discreteTopology continuous_of_discreteTopology hf hg

Premises used: tendsto_mul_cocompact_nhds_zero, continuous_of_discreteTopology
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
α : Type u_6
β : Type u_7
inst : TopologicalSpace M
inst_1 : MulZeroClass M
inst_2 : ContinuousMul M
f : α → M
g : β → M
this_1 : TopologicalSpace α := ⊥
hf : Tendsto f (cocompact α) (𝓝 0)
this_2 : DiscreteTopology α
this_3 : TopologicalSpace β := ⊥
hg : Tendsto g (cocompact β) (𝓝 0)
this : DiscreteTopology β
⊢ Tendsto (β := M) (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

Premises used: tendsto_mul_cocompact_nhds_zero, continuous_of_discreteTopology
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
inst_3 : CompactSpace M
inst_4 : T1Space M
obtain : ∀ (U : Set M) (hU : IsOpen[inst_1] U) (h0U : 0 ∈ U) (h1U : 1 ∉ U), IsOpen[inst_1] {0}
⊢ IsOpen[inst_1] {0}

Tactic:
obtain ⟨U, hU, h0U, h1U⟩ := t1Space_iff_exists_open.mp ‹_› zero_ne_one

Premises used: t1Space_iff_exists_open, zero_ne_one, Iff.mp
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
inst_3 : CompactSpace M
inst_4 : T1Space M
U : Set M
hU : IsOpen[inst_1] U
h0U : 0 ∈ U
h1U : 1 ∉ U
obtain : ∀ (W : Set M) (hW : Membership.mem (γ := Filter M) (𝓝 0) W) (hW' : univ * W ⊆ U), IsOpen[inst_1] {0}
⊢ IsOpen[inst_1] {0}

Tactic:
obtain ⟨W, hW, hW'⟩ := exists_mem_nhds_zero_mul_subset isCompact_univ (hU.mem_nhds h0U)

Premises used: isCompact_univ, IsOpen.mem_nhds, exists_mem_nhds_zero_mul_subset