awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst : TopologicalSpace α
inst_1 : AddCommGroup α
inst_2 : IsTopologicalAddGroup α
inst_3 : TopologicalSpace β
inst_4 : AddCommGroup β
inst_5 : TopologicalSpace δ
inst_6 : AddCommGroup δ
inst_7 : UniformSpace G
inst_8 : AddCommGroup G
e : β →+ α
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
φ : β →+ δ →+ G
hφ :
  Continuous[instTopologicalSpaceProd, inst_7.toTopologicalSpace] fun (p : β × δ) ↦
    (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2
W' : Set G
W'_nhds : Membership.mem (γ := Filter G) (𝓝 0) W'
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : (u : β × β) → α × α := fun (u : β × β) ↦ ((e : (a : β) → α) u.1, (e : (a : β) → α) u.2)
lim1 :
  Tendsto (β := β × δ) (fun (a : β × β) ↦ (a.2 - a.1, y₁))
    (SProd.sprod (α := Filter β) (β := Filter β) (comap (⇑e : (a : β) → α) Nx) (comap (⇑e : (a : β) → α) Nx))
    (𝓝 (0, y₁))
lim2 : Tendsto (β := G) (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2) (𝓝 (0, y₁)) (𝓝 0)
lim :
  Tendsto.{u_2, u_5} (β := G)
    ((fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2) ∘ fun (a : β × β) ↦ (a.2 - a.1, y₁))
    (SProd.sprod (α := Filter β) (β := Filter β) (comap (⇑e : (a : β) → α) Nx) (comap (⇑e : (a : β) → α) Nx)) (𝓝 0)
⊢ ∀ (W : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) W →
      ∃ (U : Set β),
        Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) Nx) U ∧
          ∀ (x x' : β),
            x ∈ U →
              x' ∈ U →
                ((fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2) ∘ fun (a : β × β) ↦
                      (a.2 - a.1, y₁))
                    (x, x') ∈
                  W

Tactic:
rw [tendsto_prod_self_iff] at lim

Premises used: Filter.tendsto_prod_self_iff
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst : TopologicalSpace α
inst_1 : AddCommGroup α
inst_2 : IsTopologicalAddGroup α
inst_3 : TopologicalSpace β
inst_4 : AddCommGroup β
inst_5 : TopologicalSpace δ
inst_6 : AddCommGroup δ
inst_7 : UniformSpace G
inst_8 : AddCommGroup G
e : β →+ α
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
φ : β →+ δ →+ G
hφ :
  Continuous[instTopologicalSpaceProd, inst_7.toTopologicalSpace] fun (p : β × δ) ↦
    (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2
W' : Set G
W'_nhds : Membership.mem (γ := Filter G) (𝓝 0) W'
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : (u : β × β) → α × α := fun (u : β × β) ↦ ((e : (a : β) → α) u.1, (e : (a : β) → α) u.2)
lim1 :
  Tendsto (β := β × δ) (fun (a : β × β) ↦ (a.2 - a.1, y₁))
    (SProd.sprod (α := Filter β) (β := Filter β) (comap (⇑e : (a : β) → α) Nx) (comap (⇑e : (a : β) → α) Nx))
    (𝓝 (0, y₁))
lim2 : Tendsto (β := G) (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2) (𝓝 (0, y₁)) (𝓝 0)
lim :
  ∀ (W : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) W →
      ∃ (U : Set β),
        Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) Nx) U ∧
          ∀ (x x' : β),
            x ∈ U →
              x' ∈ U →
                ((fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2) ∘ fun (a : β × β) ↦
                      (a.2 - a.1, y₁))
                    (x, x') ∈
                  W
simp_rw :
  ∃ (U₂ : Set β),
    Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U₂ ∧
      ∀ (a b : β),
        a ∈ U₂ → b ∈ U₂ → Membership.mem (α := G) W' ((((φ : (a : β) → δ →+ G) (b - a) : δ →+ G) : (a : δ) → G) y₁ : G)
⊢ ∃ (U₂ : Set β),
    Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U₂ ∧
      ∀ x ∈ U₂,
        ∀ x' ∈ U₂, (fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G)) (x' - x, y₁) ∈ W'

Tactic:
simp_rw [forall_mem_comm]

Premises used: forall_mem_comm
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst : TopologicalSpace α
inst_1 : AddCommGroup α
inst_2 : IsTopologicalAddGroup α
inst_3 : TopologicalSpace β
inst_4 : AddCommGroup β
inst_5 : TopologicalSpace δ
inst_6 : AddCommGroup δ
inst_7 : UniformSpace G
inst_8 : AddCommGroup G
e : β →+ α
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
φ : β →+ δ →+ G
hφ :
  Continuous[instTopologicalSpaceProd, inst_7.toTopologicalSpace] fun (p : β × δ) ↦
    (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2
W' : Set G
W'_nhds : Membership.mem (γ := Filter G) (𝓝 0) W'
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : (u : β × β) → α × α := fun (u : β × β) ↦ ((e : (a : β) → α) u.1, (e : (a : β) → α) u.2)
lim1 :
  Tendsto (β := β × δ) (fun (a : β × β) ↦ (a.2 - a.1, y₁))
    (SProd.sprod (α := Filter β) (β := Filter β) (comap (⇑e : (a : β) → α) Nx) (comap (⇑e : (a : β) → α) Nx))
    (𝓝 (0, y₁))
lim2 : Tendsto (β := G) (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2) (𝓝 (0, y₁)) (𝓝 0)
lim :
  ∀ (W : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) W →
      ∃ (U : Set β),
        Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) Nx) U ∧
          ∀ (x x' : β),
            x ∈ U →
              x' ∈ U →
                ((fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2) ∘ fun (a : β × β) ↦
                      (a.2 - a.1, y₁))
                    (x, x') ∈
                  W
⊢ ∃ (U₂ : Set β),
    Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U₂ ∧
      ∀ (a b : β),
        a ∈ U₂ → b ∈ U₂ → Membership.mem (α := G) W' ((((φ : (a : β) → δ →+ G) (b - a) : δ →+ G) : (a : δ) → G) y₁ : G)

Tactic:
lim W' W'_nhds

Premises used: Set.Mem, setOf
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst : TopologicalSpace α
inst_1 : AddCommGroup α
inst_2 : IsTopologicalAddGroup α
inst_3 : TopologicalSpace β
inst_4 : AddCommGroup β
inst_5 : TopologicalSpace δ
inst_6 : AddCommGroup δ
inst_7 : UniformSpace G
inst_8 : AddCommGroup G
e : β →+ α
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
φ : β →+ δ →+ G
hφ :
  Continuous[instTopologicalSpaceProd, inst_7.toTopologicalSpace] fun (p : β × δ) ↦
    (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2
W' : Set G
W'_nhds : Membership.mem (γ := Filter G) (𝓝 0) W'
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : (u : β × β) → α × α := fun (u : β × β) ↦ ((e : (a : β) → α) u.1, (e : (a : β) → α) u.2)
lim1 :
  Tendsto (β := β × δ) (fun (a : β × β) ↦ (a.2 - a.1, y₁))
    (SProd.sprod (α := Filter β) (β := Filter β) (comap (⇑e : (a : β) → α) Nx) (comap (⇑e : (a : β) → α) Nx))
    (𝓝 (0, y₁))
lim2 : Tendsto (β := G) (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2) (𝓝 (0, y₁)) (𝓝 0)
lim :
  ∀ (W : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) W →
      ∃ (U : Set β),
        Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) Nx) U ∧
          ∀ (x x' : β),
            x ∈ U →
              x' ∈ U →
                ((fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2) ∘ fun (a : β × β) ↦
                      (a.2 - a.1, y₁))
                    (x, x') ∈
                  W
⊢ ∃ (U₂ : Set β),
    Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U₂ ∧
      ∀ (a b : β),
        a ∈ U₂ → b ∈ U₂ → Membership.mem (α := G) W' ((((φ : (a : β) → δ →+ G) (b - a) : δ →+ G) : (a : δ) → G) y₁ : G)

Tactic:
exact lim W' W'_nhds
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst : TopologicalSpace α
inst_1 : AddCommGroup α
inst_2 : IsTopologicalAddGroup α
inst_3 : TopologicalSpace β
inst_4 : AddCommGroup β
inst_5 : TopologicalSpace γ
inst_6 : AddCommGroup γ
inst_7 : IsTopologicalAddGroup γ
inst_8 : TopologicalSpace δ
inst_9 : AddCommGroup δ
inst_10 : UniformSpace G
inst_11 : AddCommGroup G
e : β →+ α
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
f : δ →+ γ
df : IsDenseInducing.{u_4, u_3} (α := δ) (β := γ) (⇑f : (a : δ) → γ)
φ : β →+ δ →+ G
hφ :
  Continuous[instTopologicalSpaceProd, inst_10.toTopologicalSpace] fun (p : β × δ) ↦
    (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2
W' : Set G
W'_nhds : Membership.mem (γ := Filter G) (𝓝 0) W'
inst_12 : IsUniformAddGroup G
x₀ : α
y₀ : γ
ee : (u : β × β) → α × α := fun (u : β × β) ↦ ((e : (a : β) → α) u.1, (e : (a : β) → α) u.2)
ff : (u : δ × δ) → γ × γ := fun (u : δ × δ) ↦ ((f : (a : δ) → γ) u.1, (f : (a : δ) → γ) u.2)
⊢ Tendsto (β := G) (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2) (𝓝 (0, 0)) (𝓝 0)

Tactic:
simpa using hφ.tendsto (0, 0)

Premises used: Prod.mk, Continuous.tendsto, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst : TopologicalSpace α
inst_1 : AddCommGroup α
inst_2 : IsTopologicalAddGroup α
inst_3 : TopologicalSpace β
inst_4 : AddCommGroup β
inst_5 : TopologicalSpace γ
inst_6 : AddCommGroup γ
inst_7 : IsTopologicalAddGroup γ
inst_8 : TopologicalSpace δ
inst_9 : AddCommGroup δ
inst_10 : UniformSpace G
inst_11 : AddCommGroup G
e : β →+ α
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
f : δ →+ γ
df : IsDenseInducing.{u_4, u_3} (α := δ) (β := γ) (⇑f : (a : δ) → γ)
φ : β →+ δ →+ G
hφ :
  Continuous[instTopologicalSpaceProd, inst_10.toTopologicalSpace] fun (p : β × δ) ↦
    (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2
W' : Set G
W'_nhds : Membership.mem (γ := Filter G) (𝓝 0) W'
inst_12 : IsUniformAddGroup G
x₀ : α
y₀ : γ
ee : (u : β × β) → α × α := fun (u : β × β) ↦ ((e : (a : β) → α) u.1, (e : (a : β) → α) u.2)
ff : (u : δ × δ) → γ × γ := fun (u : δ × δ) ↦ ((f : (a : δ) → γ) u.1, (f : (a : δ) → γ) u.2)
⊢ Tendsto (β := G) (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2) (𝓝 (0, 0)) (𝓝 0)

Tactic:
have lim_φ : Filter.Tendsto (fun p : β × δ => φ p.1 p.2) (𝓝 (0, 0)) (𝓝 0) := by
    simpa using hφ.tendsto (0, 0)
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst : TopologicalSpace α
inst_1 : AddCommGroup α
inst_2 : IsTopologicalAddGroup α
inst_3 : TopologicalSpace β
inst_4 : AddCommGroup β
inst_5 : TopologicalSpace γ
inst_6 : AddCommGroup γ
inst_7 : IsTopologicalAddGroup γ
inst_8 : TopologicalSpace δ
inst_9 : AddCommGroup δ
inst_10 : UniformSpace G
inst_11 : AddCommGroup G
e : β →+ α
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
f : δ →+ γ
df : IsDenseInducing.{u_4, u_3} (α := δ) (β := γ) (⇑f : (a : δ) → γ)
φ : β →+ δ →+ G
hφ :
  Continuous[instTopologicalSpaceProd, inst_10.toTopologicalSpace] fun (p : β × δ) ↦
    (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2
W' : Set G
W'_nhds : Membership.mem (γ := Filter G) (𝓝 0) W'
inst_12 : IsUniformAddGroup G
x₀ : α
y₀ : γ
ee : (u : β × β) → α × α := fun (u : β × β) ↦ ((e : (a : β) → α) u.1, (e : (a : β) → α) u.2)
ff : (u : δ × δ) → γ × γ := fun (u : δ × δ) ↦ ((f : (a : δ) → γ) u.1, (f : (a : δ) → γ) u.2)
lim_φ : Tendsto (β := G) (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2) (𝓝 (0, 0)) (𝓝 0)
⊢ SProd.sprod (α := Filter β) (β := Filter δ)
      (map (fun (t : β × β) ↦ t.2 - t.1)
        (comap (fun (p : β × β) ↦ ((e : (a : β) → α) p.1, (e : (a : β) → α) p.2)) (𝓝 (x₀, x₀))))
      (map (fun (t : δ × δ) ↦ t.2 - t.1)
        (comap (fun (p : δ × δ) ↦ ((f : (a : δ) → γ) p.1, (f : (a : δ) → γ) p.2)) (𝓝 (y₀, y₀)))) ≤
    SProd.sprod (α := Filter β) (β := Filter δ) (𝓝 0) (𝓝 0)

Tactic:
have := Filter.prod_mono (tendsto_sub_comap_self de x₀) (tendsto_sub_comap_self df y₀)
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst : TopologicalSpace α
inst_1 : AddCommGroup α
inst_2 : IsTopologicalAddGroup α
inst_3 : TopologicalSpace β
inst_4 : AddCommGroup β
inst_5 : TopologicalSpace γ
inst_6 : AddCommGroup γ
inst_7 : IsTopologicalAddGroup γ
inst_8 : TopologicalSpace δ
inst_9 : AddCommGroup δ
inst_10 : UniformSpace G
inst_11 : AddCommGroup G
e : β →+ α
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
f : δ →+ γ
df : IsDenseInducing.{u_4, u_3} (α := δ) (β := γ) (⇑f : (a : δ) → γ)
φ : β →+ δ →+ G
hφ :
  Continuous[instTopologicalSpaceProd, inst_10.toTopologicalSpace] fun (p : β × δ) ↦
    (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2
W' : Set G
W'_nhds : Membership.mem (γ := Filter G) (𝓝 0) W'
inst_12 : IsUniformAddGroup G
x₀ : α
y₀ : γ
ee : (u : β × β) → α × α := fun (u : β × β) ↦ ((e : (a : β) → α) u.1, (e : (a : β) → α) u.2)
ff : (u : δ × δ) → γ × γ := fun (u : δ × δ) ↦ ((f : (a : δ) → γ) u.1, (f : (a : δ) → γ) u.2)
lim_φ : Tendsto (β := G) (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2) (𝓝 (0, 0)) (𝓝 0)
this :
  SProd.sprod (α := Filter β) (β := Filter δ)
      (map (fun (t : β × β) ↦ t.2 - t.1)
        (comap (fun (p : β × β) ↦ ((e : (a : β) → α) p.1, (e : (a : β) → α) p.2)) (𝓝 (x₀, x₀))))
      (map (fun (t : δ × δ) ↦ t.2 - t.1)
        (comap (fun (p : δ × δ) ↦ ((f : (a : δ) → γ) p.1, (f : (a : δ) → γ) p.2)) (𝓝 (y₀, y₀)))) ≤
    SProd.sprod (α := Filter β) (β := Filter δ) (𝓝 0) (𝓝 0)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (this :
      map (fun (p : Prod.{u_2, u_4} (β × β) (δ × δ)) ↦ (p.1.2 - p.1.1, p.2.2 - p.2.1))
          (SProd.sprod (α := Filter (β × β)) (β := Filter (δ × δ))
            (comap (fun (p : β × β) ↦ ((e : (a : β) → α) p.1, (e : (a : β) → α) p.2)) (𝓝 (x₀, x₀)))
            (comap (fun (p : δ × δ) ↦ ((f : (a : δ) → γ) p.1, (f : (a : δ) → γ) p.2)) (𝓝 (y₀, y₀)))) ≤
        SProd.sprod (α := Filter β) (β := Filter δ) (𝓝 0) (𝓝 0)),
    Tendsto (fun (p : Prod.{u_2, u_4} (β × β) (δ × δ)) ↦ (p.1.2 - p.1.1, p.2.2 - p.2.1))
      (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (SProd.sprod (α := Filter β) (β := Filter δ) (𝓝 0) (𝓝 0))
⊢ Tendsto (fun (p : Prod.{u_2, u_4} (β × β) (δ × δ)) ↦ (p.1.2 - p.1.1, p.2.2 - p.2.1))
    (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (SProd.sprod (α := Filter β) (β := Filter δ) (𝓝 0) (𝓝 0))

Tactic:
rwa [prod_map_map_eq] at this

Premises used: Filter.prod_map_map_eq
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst : TopologicalSpace α
inst_1 : AddCommGroup α
inst_2 : IsTopologicalAddGroup α
inst_3 : TopologicalSpace β
inst_4 : AddCommGroup β
inst_5 : TopologicalSpace γ
inst_6 : AddCommGroup γ
inst_7 : IsTopologicalAddGroup γ
inst_8 : TopologicalSpace δ
inst_9 : AddCommGroup δ
inst_10 : UniformSpace G
inst_11 : AddCommGroup G
e : β →+ α
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
f : δ →+ γ
df : IsDenseInducing.{u_4, u_3} (α := δ) (β := γ) (⇑f : (a : δ) → γ)
φ : β →+ δ →+ G
hφ :
  Continuous[instTopologicalSpaceProd, inst_10.toTopologicalSpace] fun (p : β × δ) ↦
    (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2
W' : Set G
W'_nhds : Membership.mem (γ := Filter G) (𝓝 0) W'
inst_12 : IsUniformAddGroup G
x₀ : α
y₀ : γ
ee : (u : β × β) → α × α := fun (u : β × β) ↦ ((e : (a : β) → α) u.1, (e : (a : β) → α) u.2)
ff : (u : δ × δ) → γ × γ := fun (u : δ × δ) ↦ ((f : (a : δ) → γ) u.1, (f : (a : δ) → γ) u.2)
lim_φ : Tendsto (β := G) (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2) (𝓝 (0, 0)) (𝓝 0)
⊢ Tendsto (fun (p : Prod.{u_2, u_4} (β × β) (δ × δ)) ↦ (p.1.2 - p.1.1, p.2.2 - p.2.1))
    (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (SProd.sprod (α := Filter β) (β := Filter δ) (𝓝 0) (𝓝 0))

Tactic:
have lim_sub_sub :
      Tendsto (fun p : (β × β) × δ × δ => (p.1.2 - p.1.1, p.2.2 - p.2.1))
        (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0 ×ˢ 𝓝 0) := by
      have := Filter.prod_mono (tendsto_sub_comap_self de x₀) (tendsto_sub_comap_self df y₀)
      rwa [prod_map_map_eq] at this
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst : TopologicalSpace α
inst_1 : AddCommGroup α
inst_2 : IsTopologicalAddGroup α
inst_3 : TopologicalSpace β
inst_4 : AddCommGroup β
inst_5 : TopologicalSpace γ
inst_6 : AddCommGroup γ
inst_7 : IsTopologicalAddGroup γ
inst_8 : TopologicalSpace δ
inst_9 : AddCommGroup δ
inst_10 : UniformSpace G
inst_11 : AddCommGroup G
e : β →+ α
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
f : δ →+ γ
df : IsDenseInducing.{u_4, u_3} (α := δ) (β := γ) (⇑f : (a : δ) → γ)
φ : β →+ δ →+ G
hφ :
  Continuous[instTopologicalSpaceProd, inst_10.toTopologicalSpace] fun (p : β × δ) ↦
    (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2
W' : Set G
W'_nhds : Membership.mem (γ := Filter G) (𝓝 0) W'
inst_12 : IsUniformAddGroup G
x₀ : α
y₀ : γ
ee : (u : β × β) → α × α := fun (u : β × β) ↦ ((e : (a : β) → α) u.1, (e : (a : β) → α) u.2)
ff : (u : δ × δ) → γ × γ := fun (u : δ × δ) ↦ ((f : (a : δ) → γ) u.1, (f : (a : δ) → γ) u.2)
lim_φ : Tendsto (β := G) (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2) (𝓝 (0, 0)) (𝓝 0)
lim_sub_sub :
  Tendsto (fun (p : Prod.{u_2, u_4} (β × β) (δ × δ)) ↦ (p.1.2 - p.1.1, p.2.2 - p.2.1))
    (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (SProd.sprod (α := Filter β) (β := Filter δ) (𝓝 0) (𝓝 0))
⊢ Tendsto (β := β × δ) (fun (p : Prod.{u_2, u_4} (β × β) (δ × δ)) ↦ (p.1.2 - p.1.1, p.2.2 - p.2.1))
    (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 (0, 0))

Tactic:
rw [← nhds_prod_eq] at lim_sub_sub

Premises used: nhds_prod_eq
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst : TopologicalSpace α
inst_1 : AddCommGroup α
inst_2 : IsTopologicalAddGroup α
inst_3 : TopologicalSpace β
inst_4 : AddCommGroup β
inst_5 : TopologicalSpace γ
inst_6 : AddCommGroup γ
inst_7 : IsTopologicalAddGroup γ
inst_8 : TopologicalSpace δ
inst_9 : AddCommGroup δ
inst_10 : UniformSpace G
inst_11 : AddCommGroup G
e : β →+ α
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
f : δ →+ γ
df : IsDenseInducing.{u_4, u_3} (α := δ) (β := γ) (⇑f : (a : δ) → γ)
φ : β →+ δ →+ G
hφ :
  Continuous[instTopologicalSpaceProd, inst_10.toTopologicalSpace] fun (p : β × δ) ↦
    (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2
W' : Set G
W'_nhds : Membership.mem (γ := Filter G) (𝓝 0) W'
inst_12 : IsUniformAddGroup G
x₀ : α
y₀ : γ
ee : (u : β × β) → α × α := fun (u : β × β) ↦ ((e : (a : β) → α) u.1, (e : (a : β) → α) u.2)
ff : (u : δ × δ) → γ × γ := fun (u : δ × δ) ↦ ((f : (a : δ) → γ) u.1, (f : (a : δ) → γ) u.2)
lim_φ : Tendsto (β := G) (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2) (𝓝 (0, 0)) (𝓝 0)
lim_sub_sub :
  Tendsto (β := β × δ) (fun (p : Prod.{u_2, u_4} (β × β) (δ × δ)) ↦ (p.1.2 - p.1.1, p.2.2 - p.2.1))
    (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 (0, 0))
⊢ Tendsto (β := G)
    (fun (p : Prod.{u_2, u_4} (β × β) (δ × δ)) ↦
      (fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G))
        (p.1.2 - p.1.1, p.2.2 - p.2.1))
    (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)

Tactic:
Tendsto.comp lim_φ lim_sub_sub

Premises used: Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst : TopologicalSpace α
inst_1 : AddCommGroup α
inst_2 : IsTopologicalAddGroup α
inst_3 : TopologicalSpace β
inst_4 : AddCommGroup β
inst_5 : TopologicalSpace γ
inst_6 : AddCommGroup γ
inst_7 : IsTopologicalAddGroup γ
inst_8 : TopologicalSpace δ
inst_9 : AddCommGroup δ
inst_10 : UniformSpace G
inst_11 : AddCommGroup G
e : β →+ α
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
f : δ →+ γ
df : IsDenseInducing.{u_4, u_3} (α := δ) (β := γ) (⇑f : (a : δ) → γ)
φ : β →+ δ →+ G
hφ :
  Continuous[instTopologicalSpaceProd, inst_10.toTopologicalSpace] fun (p : β × δ) ↦
    (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2
W' : Set G
W'_nhds : Membership.mem (γ := Filter G) (𝓝 0) W'
inst_12 : IsUniformAddGroup G
x₀ : α
y₀ : γ
ee : (u : β × β) → α × α := fun (u : β × β) ↦ ((e : (a : β) → α) u.1, (e : (a : β) → α) u.2)
ff : (u : δ × δ) → γ × γ := fun (u : δ × δ) ↦ ((f : (a : δ) → γ) u.1, (f : (a : δ) → γ) u.2)
lim_φ : Tendsto (β := G) (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2) (𝓝 (0, 0)) (𝓝 0)
lim_sub_sub :
  Tendsto (β := β × δ) (fun (p : Prod.{u_2, u_4} (β × β) (δ × δ)) ↦ (p.1.2 - p.1.1, p.2.2 - p.2.1))
    (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 (0, 0))
⊢ Tendsto (β := G)
    (fun (p : Prod.{u_2, u_4} (β × β) (δ × δ)) ↦
      (fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G))
        (p.1.2 - p.1.1, p.2.2 - p.2.1))
    (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)

Tactic:
exact Tendsto.comp lim_φ lim_sub_sub

Premises used: Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst : TopologicalSpace α
inst_1 : AddCommGroup α
inst_2 : IsTopologicalAddGroup α
inst_3 : TopologicalSpace β
inst_4 : AddCommGroup β
inst_5 : TopologicalSpace γ
inst_6 : AddCommGroup γ
inst_7 : IsTopologicalAddGroup γ
inst_8 : TopologicalSpace δ
inst_9 : AddCommGroup δ
inst_10 : UniformSpace G
inst_11 : AddCommGroup G
e : β →+ α
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
f : δ →+ γ
df : IsDenseInducing.{u_4, u_3} (α := δ) (β := γ) (⇑f : (a : δ) → γ)
φ : β →+ δ →+ G
hφ :
  Continuous[instTopologicalSpaceProd, inst_10.toTopologicalSpace] fun (p : β × δ) ↦
    (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2
W' : Set G
W'_nhds : Membership.mem (γ := Filter G) (𝓝 0) W'
inst_12 : IsUniformAddGroup G
x₀ : α
y₀ : γ
ee : (u : β × β) → α × α := fun (u : β × β) ↦ ((e : (a : β) → α) u.1, (e : (a : β) → α) u.2)
ff : (u : δ × δ) → γ × γ := fun (u : δ × δ) ↦ ((f : (a : δ) → γ) u.1, (f : (a : δ) → γ) u.2)
lim_φ : Tendsto (β := G) (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2) (𝓝 (0, 0)) (𝓝 0)
⊢ Tendsto (β := G)
    (fun (p : Prod.{u_2, u_4} (β × β) (δ × δ)) ↦
      (fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G))
        (p.1.2 - p.1.1, p.2.2 - p.2.1))
    (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)

Tactic:
have lim_φ_sub_sub :
    Tendsto (fun p : (β × β) × δ × δ => (fun p : β × δ => φ p.1 p.2) (p.1.2 - p.1.1, p.2.2 - p.2.1))
      ((comap ee <| 𝓝 (x₀, x₀)) ×ˢ (comap ff <| 𝓝 (y₀, y₀))) (𝓝 0) := by
    have lim_sub_sub :
      Tendsto (fun p : (β × β) × δ × δ => (p.1.2 - p.1.1, p.2.2 - p.2.1))
        (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0 ×ˢ 𝓝 0) := by
      have := Filter.prod_mono (tendsto_sub_comap_self de x₀) (tendsto_sub_comap_self df y₀)
      rwa [prod_map_map_eq] at this
    rw [← nhds_prod_eq] at lim_sub_sub
    exact Tendsto.comp lim_φ lim_sub_sub