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₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = 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
⊢ Eq (α := Filter M) (map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 (x₀, y₀)))
    (map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 x₀ ×ˢ 𝓝 y₀))
have rw : Eq (α := Filter M) (map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 x₀ ×ˢ 𝓝 y₀))
  (map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 x₀ ×ˢ 𝓝 y₀))
Tactic: rw [nhds_prod_eq]
-- 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₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = 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
⊢ Eq (α := Filter M) (map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 x₀ ×ˢ 𝓝 y₀))
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
have unfold : Eq (α := Filter M) (map (fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2) (𝓝 x₀ ×ˢ 𝓝 y₀))
  (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
Tactic: unfold uncurry
-- 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₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = 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
⊢ Eq (α := Filter M) (map (fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2) (𝓝 x₀ ×ˢ 𝓝 y₀))
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
have rw : Eq (α := Filter M)
  (map (fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2)
    (SProd.sprod (α := Filter M) (map (fun (x : M) ↦ x₀ * x) (𝓝 1)) (𝓝 y₀)))
  (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
Tactic: rw [hleft x₀, hright y₀, prod_map_map_eq, Filter.map_map, Function.comp_def]
-- 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₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = 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
rw :
  Eq (α := Filter M)
    (map (fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2)
      (SProd.sprod (α := Filter M) (map (fun (x : M) ↦ x₀ * x) (𝓝 1)) (𝓝 y₀)))
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
⊢ Eq (α := Filter M) (map (fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2) (𝓝 x₀ ×ˢ 𝓝 y₀))
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
have rw₁ : Eq (α := Filter M)
  (map (fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2)
    (SProd.sprod (α := Filter M) (β := Filter M) (map (fun (x : M) ↦ x₀ * x) (𝓝 1)) (map (fun (x : M) ↦ x * y₀) (𝓝 1))))
  (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
Tactic: rw [hleft x₀, hright y₀, prod_map_map_eq, Filter.map_map, Function.comp_def]
-- 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₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = 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
rw :
  Eq (α := Filter M)
    (map (fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2)
      (SProd.sprod (α := Filter M) (map (fun (x : M) ↦ x₀ * x) (𝓝 1)) (𝓝 y₀)))
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
rw₁ :
  Eq (α := Filter M)
    (map (fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2)
      (SProd.sprod (α := Filter M) (β := Filter M) (map (fun (x : M) ↦ x₀ * x) (𝓝 1))
        (map (fun (x : M) ↦ x * y₀) (𝓝 1))))
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
⊢ Eq (α := Filter M) (map (fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2) (𝓝 x₀ ×ˢ 𝓝 y₀))
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
have rw₂ : Eq (α := Filter M)
  (map (fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2)
    (map (fun (p : M × M) ↦ (x₀ * p.1, p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1))))
  (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
Tactic: rw [hleft x₀, hright y₀, prod_map_map_eq, Filter.map_map, Function.comp_def]
-- 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₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = 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
rw :
  Eq (α := Filter M)
    (map (fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2)
      (SProd.sprod (α := Filter M) (map (fun (x : M) ↦ x₀ * x) (𝓝 1)) (𝓝 y₀)))
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
rw₁ :
  Eq (α := Filter M)
    (map (fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2)
      (SProd.sprod (α := Filter M) (β := Filter M) (map (fun (x : M) ↦ x₀ * x) (𝓝 1))
        (map (fun (x : M) ↦ x * y₀) (𝓝 1))))
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
rw₂ :
  Eq (α := Filter M)
    (map (fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2)
      (map (fun (p : M × M) ↦ (x₀ * p.1, p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1))))
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
⊢ Eq (α := Filter M) (map (fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2) (𝓝 x₀ ×ˢ 𝓝 y₀))
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
have rw₃ : Eq (α := Filter M)
  (map ((fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2) ∘ fun (p : M × M) ↦ (x₀ * p.1, p.2 * y₀))
    (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
  (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
Tactic: rw [hleft x₀, hright y₀, prod_map_map_eq, Filter.map_map, Function.comp_def]
-- 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₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = 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
rw :
  Eq (α := Filter M)
    (map (fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2)
      (SProd.sprod (α := Filter M) (map (fun (x : M) ↦ x₀ * x) (𝓝 1)) (𝓝 y₀)))
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
rw₁ :
  Eq (α := Filter M)
    (map (fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2)
      (SProd.sprod (α := Filter M) (β := Filter M) (map (fun (x : M) ↦ x₀ * x) (𝓝 1))
        (map (fun (x : M) ↦ x * y₀) (𝓝 1))))
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
rw₂ :
  Eq (α := Filter M)
    (map (fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2)
      (map (fun (p : M × M) ↦ (x₀ * p.1, p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1))))
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
rw₃ :
  Eq (α := Filter M)
    (map ((fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2) ∘ fun (p : M × M) ↦ (x₀ * p.1, p.2 * y₀))
      (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
⊢ Eq (α := Filter M) (map (fun (a : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) a.1 a.2) (𝓝 x₀ ×ˢ 𝓝 y₀))
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
have rw₄ : Eq (α := Filter M)
  (map (fun (x : M × M) ↦ (fun (x1 x2 : M) ↦ x1 * x2) (x₀ * x.1, x.2 * y₀).1 (x₀ * x.1, x.2 * y₀).2)
    (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
  (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
Tactic: rw [hleft x₀, hright y₀, prod_map_map_eq, Filter.map_map, Function.comp_def]
-- 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₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = 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
⊢ Eq (α := Filter M)
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
    (map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀)
      (map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1))))
have rw : Eq (α := Filter M)
  (map (comp (β := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (uncurry fun (x1 x2 : M) ↦ x1 * x2))
    (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
  (map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀)
    (map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1))))
Tactic: rw [key, ← Filter.map_map]
-- 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₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = 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
rw :
  Eq (α := Filter M)
    (map (comp (β := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (uncurry fun (x1 x2 : M) ↦ x1 * x2))
      (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
    (map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀)
      (map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1))))
⊢ Eq (α := Filter M)
    (map (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀)) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
    (map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀)
      (map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1))))
have rw₁ : Eq (α := Filter M)
  (map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀)
    (map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1))))
  (map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀)
    (map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1))))
Tactic: rw [key, ← Filter.map_map]
-- 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₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = 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 (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (𝓝 1) = 𝓝 (x₀ * y₀)
have rw : map (fun (x : M) ↦ x₀ * x) (map (fun (x : M) ↦ x * y₀) (𝓝 1)) = 𝓝 (x₀ * y₀)
Tactic: 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₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = 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
rw : map (fun (x : M) ↦ x₀ * x) (map (fun (x : M) ↦ x * y₀) (𝓝 1)) = 𝓝 (x₀ * y₀)
⊢ map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (𝓝 1) = 𝓝 (x₀ * y₀)
have rw₁ : map (fun (x : M) ↦ x₀ * x) (𝓝 y₀) = 𝓝 (x₀ * y₀)
Tactic: 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₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = 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
rw : map (fun (x : M) ↦ x₀ * x) (map (fun (x : M) ↦ x * y₀) (𝓝 1)) = 𝓝 (x₀ * y₀)
rw₁ : map (fun (x : M) ↦ x₀ * x) (𝓝 y₀) = 𝓝 (x₀ * y₀)
⊢ map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (𝓝 1) = 𝓝 (x₀ * y₀)
have rw₂ : map (fun (x : M) ↦ x₀ * x) (map (fun (x : M) ↦ y₀ * x) (𝓝 1)) = 𝓝 (x₀ * y₀)
Tactic: 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₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = 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
rw : map (fun (x : M) ↦ x₀ * x) (map (fun (x : M) ↦ x * y₀) (𝓝 1)) = 𝓝 (x₀ * y₀)
rw₁ : map (fun (x : M) ↦ x₀ * x) (𝓝 y₀) = 𝓝 (x₀ * y₀)
rw₂ : map (fun (x : M) ↦ x₀ * x) (map (fun (x : M) ↦ y₀ * x) (𝓝 1)) = 𝓝 (x₀ * y₀)
⊢ map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (𝓝 1) = 𝓝 (x₀ * y₀)
have rw₃ : map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ y₀ * x) (𝓝 1) = 𝓝 (x₀ * y₀)
Tactic: 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₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = 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
rw : map (fun (x : M) ↦ x₀ * x) (map (fun (x : M) ↦ x * y₀) (𝓝 1)) = 𝓝 (x₀ * y₀)
rw₁ : map (fun (x : M) ↦ x₀ * x) (𝓝 y₀) = 𝓝 (x₀ * y₀)
rw₂ : map (fun (x : M) ↦ x₀ * x) (map (fun (x : M) ↦ y₀ * x) (𝓝 1)) = 𝓝 (x₀ * y₀)
rw₃ : map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ y₀ * x) (𝓝 1) = 𝓝 (x₀ * y₀)
⊢ map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (𝓝 1) = 𝓝 (x₀ * y₀)
have rw₄ : map (fun (x : M) ↦ x₀ * y₀ * x) (𝓝 1) = 𝓝 (x₀ * y₀)
Tactic: 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₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = 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
rw : map (fun (x : M) ↦ x₀ * x) (map (fun (x : M) ↦ x * y₀) (𝓝 1)) = 𝓝 (x₀ * y₀)
rw₁ : map (fun (x : M) ↦ x₀ * x) (𝓝 y₀) = 𝓝 (x₀ * y₀)
rw₂ : map (fun (x : M) ↦ x₀ * x) (map (fun (x : M) ↦ y₀ * x) (𝓝 1)) = 𝓝 (x₀ * y₀)
rw₃ : map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ y₀ * x) (𝓝 1) = 𝓝 (x₀ * y₀)
rw₄ : map (fun (x : M) ↦ x₀ * y₀ * x) (𝓝 1) = 𝓝 (x₀ * y₀)
⊢ map (α := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (𝓝 1) = 𝓝 (x₀ * y₀)
have rw₅ : 𝓝 (x₀ * y₀) = 𝓝 (x₀ * y₀)
Tactic: 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₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = 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
⊢ ContinuousAt (Y := M) (fun (p : M × M) ↦ p.1 * p.2) (x₀, y₀)
have map : Eq (α := Filter M) (map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 (x₀, y₀)))
  (map (uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 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 : 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₀))
⊢ ContinuousAt (Y := M) (fun (p : M × M) ↦ p.1 * p.2) (x₀, y₀)
have 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)))
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]