awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M : Type u
inst : Monoid M
inst_1 : TopologicalSpace M
hmul :
  Tendsto (β := M) (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = Filter.map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = Filter.map (fun (x : M) ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key :
  Eq.{u + 1} (α := (p : M × M) → M) (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀))
    (comp (β := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (uncurry fun (x1 x2 : M) ↦ x1 * x2))
key₂ : Eq.{u + 1} (α := M → M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ y₀ * x) fun (x : M) ↦ x₀ * y₀ * x
map :
  Eq (α := Filter M) (Filter.map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 (x₀, y₀)))
    (Filter.map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 x₀ ×ˢ 𝓝 y₀))
map₁ :
  Eq (α := Filter M) (Filter.map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 x₀ ×ˢ 𝓝 y₀))
    (Filter.map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
⊢ ContinuousAt (Y := M) (fun (p : M × M) ↦ p.1 * p.2) (x₀, y₀)
have map₂ : Eq (α := Filter M)
  (Filter.map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
  (Filter.map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀)
    (Filter.map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1))))
Tactic: calc
      map (uncurry (· * ·)) (𝓝 (x₀, y₀)) = map (uncurry (· * ·)) (𝓝 x₀ ×ˢ 𝓝 y₀) := by
        rw [nhds_prod_eq]
      _ = map (fun p : M × M => x₀ * p.1 * (p.2 * y₀)) (𝓝 1 ×ˢ 𝓝 1) := by
        unfold uncurry
        rw [hleft x₀, hright y₀, prod_map_map_eq, Filter.map_map, Function.comp_def]
      _ = map ((fun x => x₀ * x) ∘ fun x => x * y₀) (map (uncurry (· * ·)) (𝓝 1 ×ˢ 𝓝 1)) := by
        rw [key, ← Filter.map_map]
      _ ≤ map ((fun x : M => x₀ * x) ∘ fun x => x * y₀) (𝓝 1) := map_mono hmul
      _ = 𝓝 (x₀ * y₀) := by
        rw [← Filter.map_map, ← hright, hleft y₀, Filter.map_map, key₂, ← hleft]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M : Type u
inst : Monoid M
inst_1 : TopologicalSpace M
hmul :
  Tendsto (β := M) (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = Filter.map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = Filter.map (fun (x : M) ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key :
  Eq.{u + 1} (α := (p : M × M) → M) (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀))
    (comp (β := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (uncurry fun (x1 x2 : M) ↦ x1 * x2))
key₂ : Eq.{u + 1} (α := M → M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ y₀ * x) fun (x : M) ↦ x₀ * y₀ * x
map :
  Eq (α := Filter M) (Filter.map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 (x₀, y₀)))
    (Filter.map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 x₀ ×ˢ 𝓝 y₀))
map₁ :
  Eq (α := Filter M) (Filter.map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 x₀ ×ˢ 𝓝 y₀))
    (Filter.map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
map₂ :
  Eq (α := Filter M)
    (Filter.map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
    (Filter.map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀)
      (Filter.map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1))))
⊢ ContinuousAt (Y := M) (fun (p : M × M) ↦ p.1 * p.2) (x₀, y₀)
have map₃ : Filter.map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (𝓝 1) = 𝓝 (x₀ * y₀)
Tactic: calc
      map (uncurry (· * ·)) (𝓝 (x₀, y₀)) = map (uncurry (· * ·)) (𝓝 x₀ ×ˢ 𝓝 y₀) := by
        rw [nhds_prod_eq]
      _ = map (fun p : M × M => x₀ * p.1 * (p.2 * y₀)) (𝓝 1 ×ˢ 𝓝 1) := by
        unfold uncurry
        rw [hleft x₀, hright y₀, prod_map_map_eq, Filter.map_map, Function.comp_def]
      _ = map ((fun x => x₀ * x) ∘ fun x => x * y₀) (map (uncurry (· * ·)) (𝓝 1 ×ˢ 𝓝 1)) := by
        rw [key, ← Filter.map_map]
      _ ≤ map ((fun x : M => x₀ * x) ∘ fun x => x * y₀) (𝓝 1) := map_mono hmul
      _ = 𝓝 (x₀ * y₀) := by
        rw [← Filter.map_map, ← hright, hleft y₀, Filter.map_map, key₂, ← hleft]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M : Type u
inst : CommMonoid M
inst_1 : TopologicalSpace M
hmul :
  Tendsto (β := M) (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
⊢ ContinuousMul M
have apply : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x * x₀) (𝓝 1)
Tactic: apply ContinuousMul.of_nhds_one hmul hleft
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M : Type u
inst : CommMonoid M
inst_1 : TopologicalSpace M
hmul :
  Tendsto (β := M) (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
x₀ : M
⊢ 𝓝 x₀ = map (fun (x : M) ↦ x * x₀) (𝓝 1)
have simp_rw : 𝓝 x₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
Tactic: simp_rw [mul_comm, hleft x₀]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M₁ : Type u_6
M₂ : Type u_7
inst : TopologicalSpace M₂
inst_1 : T2Space M₂
inst_2 : Mul M₁
inst_3 : Mul M₂
inst_4 : ContinuousMul M₂
⊢ IsClosed[Pi.topologicalSpace] {f : M₁ → M₂ | ∀ (x y : M₁), f (x * y) = f x * f y}
have simp : IsClosed[Pi.topologicalSpace] (⋂ (i : M₁), ⋂ (i_1 : M₁), {x : M₁ → M₂ | x (i * i_1) = x i * x i_1})
Tactic: simp only [setOf_forall]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
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
⊢ ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ K * V ⊆ U
have refine_1 : ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ ∅ * V ⊆ U
Tactic: refine hK.induction_on ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
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
refine_1 : ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ ∅ * V ⊆ U
⊢ ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ K * V ⊆ U
have refine_2 : ∀ ⦃s t : Set M⦄,
  s ⊆ t →
    (∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ t * V ⊆ U) →
      ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ s * V ⊆ U
Tactic: refine hK.induction_on ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
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
refine_1 : ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ ∅ * V ⊆ U
refine_2 :
  ∀ ⦃s t : Set M⦄,
    s ⊆ t →
      (∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ t * V ⊆ U) →
        ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ s * V ⊆ U
⊢ ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ K * V ⊆ U
have refine_3 : ∀ ⦃s t : Set M⦄,
  (∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ s * V ⊆ U) →
    (∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ t * V ⊆ U) →
      ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ (s ∪ t) * V ⊆ U
Tactic: refine hK.induction_on ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
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
refine_1 : ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ ∅ * V ⊆ U
refine_2 :
  ∀ ⦃s t : Set M⦄,
    s ⊆ t →
      (∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ t * V ⊆ U) →
        ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ s * V ⊆ U
refine_3 :
  ∀ ⦃s t : Set M⦄,
    (∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ s * V ⊆ U) →
      (∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ t * V ⊆ U) →
        ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ (s ∪ t) * V ⊆ U
⊢ ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ K * V ⊆ U
have refine_4 : ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ t * V ⊆ U
Tactic: refine hK.induction_on ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
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
s t V : Set M
V_in : Membership.mem (γ := Filter M) (𝓝 0) V
hV' : s * V ⊆ U
W : Set M
W_in : Membership.mem (γ := Filter M) (𝓝 0) W
hW' : t * W ⊆ U
⊢ ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ (s ∪ t) * V ⊆ U
have right : (s ∪ t) * (V ∩ W) ⊆ U
Tactic: use V ∩ W, inter_mem V_in W_in
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
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
s t V : Set M
V_in : Membership.mem (γ := Filter M) (𝓝 0) V
hV' : s * V ⊆ U
W : Set M
W_in : Membership.mem (γ := Filter M) (𝓝 0) W
hW' : t * W ⊆ U
⊢ (s ∪ t) * (V ∩ W) ⊆ U
have right : s * (V ∩ W) ∪ t * (V ∩ W) ⊆ U
Tactic: rw [union_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (hypothesis)
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 ∈ 𝓝[K] x, ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ t * V ⊆ U
have this : Membership.mem (γ := Filter M) (map (fun (p : M × M) ↦ p.1 * p.2) (𝓝 (x, 0))) U
Tactic: have := tendsto_mul (show U ∈ 𝓝 (x * 0) by simpa using hU)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (hypothesis)
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 ∈ 𝓝[K] x, ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ t * V ⊆ U
have this₁ : ∃ 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
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
⊢ ∃ t ∈ 𝓝[K] x, ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ t * V ⊆ U
have 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
Tactic: rcases this with ⟨t, ht, s, hs, h⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (hypothesis)
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 ∈ 𝓝[K] x, ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 0) V ∧ t * V ⊆ U
have h₁ : t * s ⊆ U
Tactic: rw [← image_subset_iff, image_mul_prod] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (hypothesis)
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))
⊢ Tendsto (β := M) (fun (x : M × M) ↦ x.1 * x.2) (Filter.coprod (𝓝 0) (𝓝 0) ⊓ l) (𝓝 0)
have this : 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 _ _ _ _
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
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)
⊢ Tendsto (β := M) (fun (x : M × M) ↦ x.1 * x.2) (Filter.coprod (𝓝 0) (𝓝 0) ⊓ l) (𝓝 0)
have apply : Tendsto (β := M) (fun (x : M × M) ↦ x.1 * x.2) (SProd.sprod (α := Filter M) (𝓝 0) (map Prod.snd l)) (𝓝 0)
Tactic: apply (Tendsto.sup _ _).mono_left this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
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)
⊢ Tendsto (β := M) (fun (x : M × M) ↦ x.1 * x.2) (Filter.coprod (𝓝 0) (𝓝 0) ⊓ l) (𝓝 0)
have apply₁ : Tendsto (β := M) (fun (x : M × M) ↦ x.1 * x.2) (SProd.sprod (β := Filter M) (map Prod.fst l) (𝓝 0)) (𝓝 0)
Tactic: apply (Tendsto.sup _ _).mono_left this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
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)
⊢ Tendsto (β := M) (fun (x : M × M) ↦ x.1 * x.2) (SProd.sprod (α := Filter M) (𝓝 0) (map Prod.snd l)) (𝓝 0)
have hl₁ : Disjoint (map Prod.snd l) (cocompact M)
Tactic: apply tendsto_mul_nhds_zero_prod_of_disjoint_cocompact
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
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)
⊢ Tendsto (β := M) (fun (x : M × M) ↦ x.1 * x.2) (SProd.sprod (β := Filter M) (map Prod.fst l) (𝓝 0)) (𝓝 0)
have hl₁ : Disjoint (map Prod.fst l) (cocompact M)
Tactic: apply tendsto_mul_prod_nhds_zero_of_disjoint_cocompact
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (hypothesis)
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)
⊢ Tendsto (β := M) (fun (i : α × β) ↦ f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)
have l_def : 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (hypothesis)
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)
⊢ Tendsto (β := M) (fun (i : α × β) ↦ f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)
have K_compact : 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)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (hypothesis)
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
⊢ Tendsto (β := M) (fun (i : α × β) ↦ f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)
have K_mem_l : 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 _)⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
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))
have rw : ∃ K ∈ l, IsCompact K
Tactic: rw [disjoint_cocompact_right]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (hypothesis)
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
⊢ Tendsto (β := M) (fun (i : α × β) ↦ f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)
have l_compact : 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⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
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)
have rw : map (Prod.map f g) ((cocompact α).coprod (cocompact β)) ≤ Filter.coprod (𝓝 0) (𝓝 0)
Tactic: rw [l_def, ← coprod_cocompact]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (hypothesis)
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))
⊢ Tendsto (β := M) (fun (i : α × β) ↦ f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)
have l_le_coprod : 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (hypothesis)
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 α := ⊥
⊢ Tendsto (β := M) (fun (i : α × β) ↦ f i.1 * g i.2) cofinite (𝓝 0)
have this₁ : DiscreteTopology α
Tactic: haveI : DiscreteTopology α := discreteTopology_bot α
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (hypothesis)
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 β := ⊥
⊢ Tendsto (β := M) (fun (i : α × β) ↦ f i.1 * g i.2) cofinite (𝓝 0)
have this₁ : DiscreteTopology β
Tactic: haveI : DiscreteTopology β := discreteTopology_bot β
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
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 β
⊢ Tendsto (β := M) (fun (i : α × β) ↦ f i.1 * g i.2) cofinite (𝓝 0)
have 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)
Tactic: rw [← cocompact_eq_cofinite] at *
Cleared hypotheses: hf, hg, this_2, this_3, this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M : Type u_3
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
inst_3 : CompactSpace M
inst_4 : T1Space M
⊢ IsOpen[inst_1] {0}
have obtain : ∀ (U : Set M) (hU : IsOpen[inst_1] U) (h0U : 0 ∈ U) (h1U : 1 ∉ U), IsOpen[inst_1] {0}
Tactic: obtain ⟨U, hU, h0U, h1U⟩ := t1Space_iff_exists_open.mp ‹_› zero_ne_one
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
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
⊢ IsOpen[inst_1] {0}
have obtain : ∀ (W : Set M) (hW : Membership.mem (γ := Filter M) (𝓝 0) W) (hW' : univ * W ⊆ U), IsOpen[inst_1] {0}
Tactic: obtain ⟨W, hW, hW'⟩ := exists_mem_nhds_zero_mul_subset isCompact_univ (hU.mem_nhds h0U)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
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
W : Set M
hW : Membership.mem (γ := Filter M) (𝓝 0) W
hW' : univ * W ⊆ U
⊢ IsOpen[inst_1] {0}
have pos : ∀ (H : ∃ (x : M), x ≠ 0 ∧ x ∈ W), IsOpen[inst_1] {0}
Tactic: by_cases H : ∃ x ≠ 0, x ∈ W