awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Group G
u : UniformSpace G
inst_1 : IsTopologicalGroup G
F : ι → α → G
p : Filter ι
s : Set α
hu : rightUniformSpace G = u
⊢ UniformCauchySeqOn F p s ↔
    ∀ (u_1 : Set G),
      Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ a ∈ s, F m.2 a * (F m.1 a)⁻¹ ∈ u_1

Tactic:
exact hu ▸ ⟨fun h u hu ↦ h _ ⟨u, hu, fun _ ↦ id⟩,
    fun h _ ⟨u, hu, hv⟩ => mem_of_superset (h u hu) fun _ hi a ha => hv (hi a ha)⟩
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Group G
u : UniformSpace G
inst_1 : IsTopologicalGroup G
F : ι → α → G
f : α → G
p : Filter ι
hu : rightUniformSpace G = u
simp :
  TendstoUniformly F f p ↔
    ∀ (u_1 : Set G), Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ᶠ (i : ι) in p, ∀ (a : α), F i a * (f a)⁻¹ ∈ u_1
⊢ TendstoUniformly F f p ↔
    ∀ (u_1 : Set G), Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ᶠ (i : ι) in p, ∀ (a : α), F i a / f a ∈ u_1

Tactic:
simp only [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Group G
u : UniformSpace G
inst_1 : IsTopologicalGroup G
F : ι → α → G
f : α → G
p : Filter ι
hu : rightUniformSpace G = u
⊢ TendstoUniformly F f p ↔
    ∀ (u_1 : Set G), Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ᶠ (i : ι) in p, ∀ (a : α), F i a * (f a)⁻¹ ∈ u_1

Tactic:
hu ▸ ⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩,
    fun h _ ⟨u, hu, hv⟩ => mem_of_superset (h u hu) fun _ hi a => hv (hi a)⟩

Premises used: HMul.hMul, Filter.Eventually, Eq.rec, id, Prod.fst, Inv.inv, Set.preimage, And.intro, Iff.intro, Exists.intro, _private.0.IsTopologicalGroup.uniformCauchySeqOn_iff.match_1, Prod.snd, Filter.mem_of_superset
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Group G
u : UniformSpace G
inst_1 : IsTopologicalGroup G
F : ι → α → G
f : α → G
p : Filter ι
hu : rightUniformSpace G = u
⊢ TendstoUniformly F f p ↔
    ∀ (u_1 : Set G), Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ᶠ (i : ι) in p, ∀ (a : α), F i a * (f a)⁻¹ ∈ u_1

Tactic:
exact hu ▸ ⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩,
    fun h _ ⟨u, hu, hv⟩ => mem_of_superset (h u hu) fun _ hi a => hv (hi a)⟩
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Group G
u : UniformSpace G
inst_1 : IsTopologicalGroup G
F : ι → α → G
f : α → G
p : Filter ι
s : Set α
hu : rightUniformSpace G = u
simp :
  TendstoUniformlyOn F f p s ↔
    ∀ (u_1 : Set G), Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ᶠ (i : ι) in p, ∀ a ∈ s, F i a * (f a)⁻¹ ∈ u_1
⊢ TendstoUniformlyOn F f p s ↔
    ∀ (u_1 : Set G), Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ᶠ (i : ι) in p, ∀ a ∈ s, F i a / f a ∈ u_1

Tactic:
simp only [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Group G
u : UniformSpace G
inst_1 : IsTopologicalGroup G
F : ι → α → G
f : α → G
p : Filter ι
s : Set α
hu : rightUniformSpace G = u
⊢ TendstoUniformlyOn F f p s ↔
    ∀ (u_1 : Set G), Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ᶠ (i : ι) in p, ∀ a ∈ s, F i a * (f a)⁻¹ ∈ u_1

Tactic:
hu ▸ ⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩,
    fun h _ ⟨u, hu, hv⟩ => mem_of_superset (h u hu) fun _ hi a ha => hv (hi a ha)⟩

Premises used: HMul.hMul, Filter.Eventually, Eq.rec, id, Prod.fst, Inv.inv, Set.preimage, And.intro, Iff.intro, Exists.intro, _private.0.IsTopologicalGroup.uniformCauchySeqOn_iff.match_1, Prod.snd, Filter.mem_of_superset
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Group G
u : UniformSpace G
inst_1 : IsTopologicalGroup G
F : ι → α → G
f : α → G
p : Filter ι
s : Set α
hu : rightUniformSpace G = u
⊢ TendstoUniformlyOn F f p s ↔
    ∀ (u_1 : Set G), Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ᶠ (i : ι) in p, ∀ a ∈ s, F i a * (f a)⁻¹ ∈ u_1

Tactic:
exact hu ▸ ⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩,
    fun h _ ⟨u, hu, hv⟩ => mem_of_superset (h u hu) fun _ hi a ha => hv (hi a ha)⟩
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Group G
u : UniformSpace G
inst_1 : IsTopologicalGroup G
inst_2 : TopologicalSpace α
F : ι → α → G
f : α → G
p : Filter ι
hu : rightUniformSpace G = u
simp :
  TendstoLocallyUniformly F f p ↔
    ∀ (u_1 : Set G),
      Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ (x : α), ∃ t ∈ 𝓝 x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a * (f a)⁻¹ ∈ u_1
⊢ TendstoLocallyUniformly F f p ↔
    ∀ (u_1 : Set G),
      Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ (x : α), ∃ t ∈ 𝓝 x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a / f a ∈ u_1

Tactic:
simp only [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Group G
u : UniformSpace G
inst_1 : IsTopologicalGroup G
inst_2 : TopologicalSpace α
F : ι → α → G
f : α → G
p : Filter ι
hu : rightUniformSpace G = u
⊢ TendstoLocallyUniformly F f p ↔
    ∀ (u_1 : Set G),
      Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ (x : α), ∃ t ∈ 𝓝 x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a * (f a)⁻¹ ∈ u_1

Tactic:
hu ▸ ⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩, fun h _ ⟨u, hu, hv⟩ x =>
    Exists.imp (fun _ ⟨h, hp⟩ => ⟨h, mem_of_superset hp fun _ hi a ha => hv (hi a ha)⟩)
      (h u hu x)⟩

Premises used: HMul.hMul, Filter.Eventually, Membership.mem, Exists, nhds, Eq.rec, id, Exists.imp, Prod.fst, And, Inv.inv, Set.preimage, And.intro, Iff.intro, Exists.intro, _private.0.IsTopologicalGroup.uniformCauchySeqOn_iff.match_1, Prod.snd
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Group G
u : UniformSpace G
inst_1 : IsTopologicalGroup G
inst_2 : TopologicalSpace α
F : ι → α → G
f : α → G
p : Filter ι
hu : rightUniformSpace G = u
⊢ TendstoLocallyUniformly F f p ↔
    ∀ (u_1 : Set G),
      Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ (x : α), ∃ t ∈ 𝓝 x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a * (f a)⁻¹ ∈ u_1

Tactic:
exact hu ▸ ⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩, fun h _ ⟨u, hu, hv⟩ x =>
    Exists.imp (fun _ ⟨h, hp⟩ => ⟨h, mem_of_superset hp fun _ hi a ha => hv (hi a ha)⟩)
      (h u hu x)⟩
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Group G
u : UniformSpace G
inst_1 : IsTopologicalGroup G
inst_2 : TopologicalSpace α
F : ι → α → G
f : α → G
p : Filter ι
s : Set α
hu : rightUniformSpace G = u
simp :
  TendstoLocallyUniformlyOn F f p s ↔
    ∀ (u_1 : Set G),
      Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a * (f a)⁻¹ ∈ u_1
⊢ TendstoLocallyUniformlyOn F f p s ↔
    ∀ (u_1 : Set G),
      Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a / f a ∈ u_1

Tactic:
simp only [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Group G
u : UniformSpace G
inst_1 : IsTopologicalGroup G
inst_2 : TopologicalSpace α
F : ι → α → G
f : α → G
p : Filter ι
s : Set α
hu : rightUniformSpace G = u
⊢ TendstoLocallyUniformlyOn F f p s ↔
    ∀ (u_1 : Set G),
      Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a * (f a)⁻¹ ∈ u_1

Tactic:
hu ▸ ⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩, fun h _ ⟨u, hu, hv⟩ x =>
    (Exists.imp fun _ ⟨h, hp⟩ => ⟨h, mem_of_superset hp fun _ hi a ha => hv (hi a ha)⟩) ∘
      h u hu x⟩

Premises used: HMul.hMul, Function.comp, Eq.rec, id, Exists.imp, Prod.fst, Inv.inv, Set.preimage, And.intro, Iff.intro, Exists.intro, _private.0.IsTopologicalGroup.uniformCauchySeqOn_iff.match_1, Prod.snd
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Group G
u : UniformSpace G
inst_1 : IsTopologicalGroup G
inst_2 : TopologicalSpace α
F : ι → α → G
f : α → G
p : Filter ι
s : Set α
hu : rightUniformSpace G = u
⊢ TendstoLocallyUniformlyOn F f p s ↔
    ∀ (u_1 : Set G),
      Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a * (f a)⁻¹ ∈ u_1

Tactic:
exact hu ▸ ⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩, fun h _ ⟨u, hu, hv⟩ x =>
    (Exists.imp fun _ ⟨h, hp⟩ => ⟨h, mem_of_superset hp fun _ hi a ha => hv (hi a ha)⟩) ∘
      h u hu x⟩
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
hom : Type u_3
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : IsTopologicalGroup α
inst_3 : TopologicalSpace β
inst_4 : Group β
inst_5 : FunLike hom β α
inst_6 : MonoidHomClass hom β α
e : hom
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
x₀ : α
h :
  ∀ (t : β × β),
    Eq.{u_1 + 1} (α := α)
      (((fun (x : α × α) ↦ x.2 / x.1) ∘ fun (t : β × β) ↦ ((e : (a : β) → α) t.1, (e : (a : β) → α) t.2)) t)
      (comp (β := β) (⇑e : (a : β) → α) (fun (t : β × β) ↦ t.2 / t.1) t)
⊢ Eq (α := β × β → α) ((fun (x : α × α) ↦ x.2 / x.1) ∘ fun (t : β × β) ↦ ((e : (a : β) → α) t.1, (e : (a : β) → α) t.2))
    (comp (β := β) (⇑e : (a : β) → α) fun (t : β × β) ↦ t.2 / t.1)

Tactic:
ext t
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
hom : Type u_3
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : IsTopologicalGroup α
inst_3 : TopologicalSpace β
inst_4 : Group β
inst_5 : FunLike hom β α
inst_6 : MonoidHomClass hom β α
e : hom
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
x₀ : α
t : β × β
⊢ Eq.{u_1 + 1} (α := α)
    (((fun (x : α × α) ↦ x.2 / x.1) ∘ fun (t : β × β) ↦ ((e : (a : β) → α) t.1, (e : (a : β) → α) t.2)) t)
    (comp (β := β) (⇑e : (a : β) → α) (fun (t : β × β) ↦ t.2 / t.1) t)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
hom : Type u_3
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : IsTopologicalGroup α
inst_3 : TopologicalSpace β
inst_4 : Group β
inst_5 : FunLike hom β α
inst_6 : MonoidHomClass hom β α
e : hom
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
x₀ : α
⊢ Eq (α := β × β → α) ((fun (x : α × α) ↦ x.2 / x.1) ∘ fun (t : β × β) ↦ ((e : (a : β) → α) t.1, (e : (a : β) → α) t.2))
    (comp (β := β) (⇑e : (a : β) → α) fun (t : β × β) ↦ t.2 / t.1)

Tactic:
have comm : ((fun x : α × α => x.2 / x.1) ∘ fun t : β × β => (e t.1, e t.2)) =
      e ∘ fun t : β × β => t.2 / t.1 := by
    ext t
    simp
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
hom : Type u_3
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : IsTopologicalGroup α
inst_3 : TopologicalSpace β
inst_4 : Group β
inst_5 : FunLike hom β α
inst_6 : MonoidHomClass hom β α
e : hom
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
x₀ : α
comm :
  Eq (α := β × β → α) ((fun (x : α × α) ↦ x.2 / x.1) ∘ fun (t : β × β) ↦ ((e : (a : β) → α) t.1, (e : (a : β) → α) t.2))
    (comp (β := β) (⇑e : (a : β) → α) fun (t : β × β) ↦ t.2 / t.1)
⊢ Tendsto (β := α) (fun (x : α × α) ↦ x.2 / x.1) (𝓝 (x₀, x₀)) (𝓝 ((e : (a : β) → α) 1) : Filter α)

Tactic:
simpa using (continuous_div'.comp (@continuous_swap α α _ _)).tendsto (x₀, x₀)

Premises used: Continuous.comp, continuous_swap, Prod.mk, ContinuousDiv.continuous_div', Continuous.tendsto
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
hom : Type u_3
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : IsTopologicalGroup α
inst_3 : TopologicalSpace β
inst_4 : Group β
inst_5 : FunLike hom β α
inst_6 : MonoidHomClass hom β α
e : hom
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
x₀ : α
comm :
  Eq (α := β × β → α) ((fun (x : α × α) ↦ x.2 / x.1) ∘ fun (t : β × β) ↦ ((e : (a : β) → α) t.1, (e : (a : β) → α) t.2))
    (comp (β := β) (⇑e : (a : β) → α) fun (t : β × β) ↦ t.2 / t.1)
⊢ Tendsto (β := α) (fun (x : α × α) ↦ x.2 / x.1) (𝓝 (x₀, x₀)) (𝓝 ((e : (a : β) → α) 1) : Filter α)

Tactic:
have lim : Tendsto (fun x : α × α => x.2 / x.1) (𝓝 (x₀, x₀)) (𝓝 (e 1)) := by
    simpa using (continuous_div'.comp (@continuous_swap α α _ _)).tendsto (x₀, x₀)
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
hom : Type u_3
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : IsTopologicalGroup α
inst_3 : TopologicalSpace β
inst_4 : Group β
inst_5 : FunLike hom β α
inst_6 : MonoidHomClass hom β α
e : hom
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
x₀ : α
comm :
  Eq (α := β × β → α) ((fun (x : α × α) ↦ x.2 / x.1) ∘ fun (t : β × β) ↦ ((e : (a : β) → α) t.1, (e : (a : β) → α) t.2))
    (comp (β := β) (⇑e : (a : β) → α) fun (t : β × β) ↦ t.2 / t.1)
lim : Tendsto (β := α) (fun (x : α × α) ↦ x.2 / x.1) (𝓝 (x₀, x₀)) (𝓝 ((e : (a : β) → α) 1) : Filter α)
⊢ Tendsto (β := β) (fun (t : β × β) ↦ t.2 / t.1)
    (comap (fun (p : β × β) ↦ ((e : (a : β) → α) p.1, (e : (a : β) → α) p.2)) (𝓝 (x₀, x₀))) (𝓝 1)

Tactic:
simpa using de.tendsto_comap_nhds_nhds lim comm

Premises used: IsDenseInducing.tendsto_comap_nhds_nhds
-- 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)
⊢ Tendsto (fun (x : β × β) ↦ (x.2 - x.1, y₁))
    (comap (fun (p : β × β) ↦ ((e : (a : β) → α) p.1, (e : (a : β) → α) p.2)) (𝓝 (x₀, x₀)))
    (SProd.sprod (α := Filter β) (𝓝 0) (𝓝 y₁))

Tactic:
have := Tendsto.prodMk (tendsto_sub_comap_self de x₀)
      (tendsto_const_nhds : Tendsto (fun _ : β × β => y₁) (comap ee <| 𝓝 (x₀, x₀)) (𝓝 y₁))
-- 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)
this :
  Tendsto (fun (x : β × β) ↦ (x.2 - x.1, y₁))
    (comap (fun (p : β × β) ↦ ((e : (a : β) → α) p.1, (e : (a : β) → α) p.2)) (𝓝 (x₀, x₀)))
    (SProd.sprod (α := Filter β) (𝓝 0) (𝓝 y₁))
rw :
  Tendsto (fun (a : β × β) ↦ (a.2 - a.1, y₁))
    (comap (fun (p : β × β) ↦ ((e : (a : β) → α) p.1, (e : (a : β) → α) p.2)) (𝓝 (x₀, x₀)))
    (SProd.sprod (α := Filter β) (𝓝 0) (𝓝 y₁))
⊢ Tendsto (β := β × δ) (fun (a : β × β) ↦ (a.2 - a.1, y₁))
    (SProd.sprod (α := Filter β) (β := Filter β) (comap (⇑e : (a : β) → α) Nx) (comap (⇑e : (a : β) → α) Nx))
    (𝓝 (0, y₁))

Tactic:
rw [nhds_prod_eq, prod_comap_comap_eq, ← nhds_prod_eq]

Premises used: Filter.prod_comap_comap_eq, nhds_prod_eq
-- 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)
this :
  Tendsto (fun (x : β × β) ↦ (x.2 - x.1, y₁))
    (comap (fun (p : β × β) ↦ ((e : (a : β) → α) p.1, (e : (a : β) → α) p.2)) (𝓝 (x₀, x₀)))
    (SProd.sprod (α := Filter β) (𝓝 0) (𝓝 y₁))
⊢ Tendsto (fun (a : β × β) ↦ (a.2 - a.1, y₁))
    (comap (fun (p : β × β) ↦ ((e : (a : β) → α) p.1, (e : (a : β) → α) p.2)) (𝓝 (x₀, x₀)))
    (SProd.sprod (α := Filter β) (𝓝 0) (𝓝 y₁))

Tactic:
(this :)

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)
this :
  Tendsto (fun (x : β × β) ↦ (x.2 - x.1, y₁))
    (comap (fun (p : β × β) ↦ ((e : (a : β) → α) p.1, (e : (a : β) → α) p.2)) (𝓝 (x₀, x₀)))
    (SProd.sprod (α := Filter β) (𝓝 0) (𝓝 y₁))
⊢ Tendsto (fun (a : β × β) ↦ (a.2 - a.1, y₁))
    (comap (fun (p : β × β) ↦ ((e : (a : β) → α) p.1, (e : (a : β) → α) p.2)) (𝓝 (x₀, x₀)))
    (SProd.sprod (α := Filter β) (𝓝 0) (𝓝 y₁))

Tactic:
exact (this :)
-- 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)
⊢ Tendsto (β := β × δ) (fun (a : β × β) ↦ (a.2 - a.1, y₁))
    (SProd.sprod (α := Filter β) (β := Filter β) (comap (⇑e : (a : β) → α) Nx) (comap (⇑e : (a : β) → α) Nx))
    (𝓝 (0, y₁))

Tactic:
have lim1 : Tendsto (fun a : β × β => (a.2 - a.1, y₁))
      (comap e Nx ×ˢ comap e Nx) (𝓝 (0, y₁)) := by
    have := Tendsto.prodMk (tendsto_sub_comap_self de x₀)
      (tendsto_const_nhds : Tendsto (fun _ : β × β => y₁) (comap ee <| 𝓝 (x₀, x₀)) (𝓝 y₁))
    rw [nhds_prod_eq, prod_comap_comap_eq, ← nhds_prod_eq]
    exact (this :)
-- 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₁))
⊢ Tendsto (β := G) (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2) (𝓝 (0, y₁)) (𝓝 0)

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

Premises used: Prod.mk, Continuous.tendsto, OfNat.ofNat
-- 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₁))
⊢ Tendsto (β := G) (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2) (𝓝 (0, y₁)) (𝓝 0)

Tactic:
have lim2 : Tendsto (fun p : β × δ => φ p.1 p.2) (𝓝 (0, y₁)) (𝓝 0) := by
    simpa using hφ.tendsto (0, y₁)
-- 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)
⊢ 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)

Tactic:
have lim := lim2.comp lim1