awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (β := 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)
W : Set G
W_nhds : Membership.mem (γ := Filter G) (𝓝 0) W
W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'
U₁ : Set β
U₁_nhds : Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U₁
V₁ : Set δ
V₁_nhds : Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V₁
H :
  ∀ x ∈ U₁,
    ∀ x' ∈ U₁,
      ∀ y ∈ V₁,
        ∀ y' ∈ V₁,
          (fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G)) (x' - x, y' - y) ∈ W
x₁ : β
x₁_in : x₁ ∈ U₁
⊢ V₁.Nonempty

Tactic:
(df.comap_nhds_neBot _).nonempty_of_mem V₁_nhds

Premises used: IsDenseInducing.comap_nhds_neBot, Filter.NeBot.nonempty_of_mem
-- 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 (β := 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)
W : Set G
W_nhds : Membership.mem (γ := Filter G) (𝓝 0) W
W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'
U₁ : Set β
U₁_nhds : Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U₁
V₁ : Set δ
V₁_nhds : Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V₁
H :
  ∀ x ∈ U₁,
    ∀ x' ∈ U₁,
      ∀ y ∈ V₁,
        ∀ y' ∈ V₁,
          (fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G)) (x' - x, y' - y) ∈ W
x₁ : β
x₁_in : x₁ ∈ U₁
y₁ : δ
y₁_in : y₁ ∈ V₁
change :
  Continuous[instTopologicalSpaceProd, inst_10.toTopologicalSpace]
    ((fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2) ∘ Prod.swap)
⊢ Continuous[instTopologicalSpaceProd, inst_10.toTopologicalSpace] fun (p : δ × β) ↦
    (((φ.flip : (a : δ) → β →+ G) p.1 : β →+ G) : (a : β) → G) p.2

Tactic:
change Continuous ((fun p : β × δ => φ p.1 p.2) ∘ Prod.swap)

Premises used: Continuous, Function.comp, Prod.fst, Prod.swap, Prod.snd, DFunLike.coe
-- 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 (β := 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)
W : Set G
W_nhds : Membership.mem (γ := Filter G) (𝓝 0) W
W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'
U₁ : Set β
U₁_nhds : Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U₁
V₁ : Set δ
V₁_nhds : Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V₁
H :
  ∀ x ∈ U₁,
    ∀ x' ∈ U₁,
      ∀ y ∈ V₁,
        ∀ y' ∈ V₁,
          (fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G)) (x' - x, y' - y) ∈ W
x₁ : β
x₁_in : x₁ ∈ U₁
y₁ : δ
y₁_in : y₁ ∈ V₁
⊢ Continuous[instTopologicalSpaceProd, inst_10.toTopologicalSpace]
    ((fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2) ∘ Prod.swap)

Tactic:
hφ.comp continuous_swap

Premises used: Continuous.comp, continuous_swap
-- 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 (β := 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)
W : Set G
W_nhds : Membership.mem (γ := Filter G) (𝓝 0) W
W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'
U₁ : Set β
U₁_nhds : Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U₁
V₁ : Set δ
V₁_nhds : Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V₁
H :
  ∀ x ∈ U₁,
    ∀ x' ∈ U₁,
      ∀ y ∈ V₁,
        ∀ y' ∈ V₁,
          (fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G)) (x' - x, y' - y) ∈ W
x₁ : β
x₁_in : x₁ ∈ U₁
y₁ : δ
y₁_in : y₁ ∈ V₁
⊢ Continuous[instTopologicalSpaceProd, inst_10.toTopologicalSpace]
    ((fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2) ∘ Prod.swap)

Tactic:
exact hφ.comp continuous_swap

Premises used: Continuous.comp, continuous_swap
-- 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 (β := 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)
W : Set G
W_nhds : Membership.mem (γ := Filter G) (𝓝 0) W
W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'
U₁ : Set β
U₁_nhds : Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U₁
V₁ : Set δ
V₁_nhds : Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V₁
H :
  ∀ x ∈ U₁,
    ∀ x' ∈ U₁,
      ∀ y ∈ V₁,
        ∀ y' ∈ V₁,
          (fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G)) (x' - x, y' - y) ∈ W
x₁ : β
x₁_in : x₁ ∈ U₁
y₁ : δ
y₁_in : y₁ ∈ V₁
⊢ Continuous[instTopologicalSpaceProd, inst_10.toTopologicalSpace] fun (p : δ × β) ↦
    (((φ.flip : (a : δ) → β →+ G) p.1 : β →+ G) : (a : β) → G) p.2

Tactic:
have cont_flip : Continuous fun p : δ × β => φ.flip p.1 p.2 := by
    change Continuous ((fun p : β × δ => φ p.1 p.2) ∘ Prod.swap)
    exact hφ.comp continuous_swap
-- 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
inst_12 : IsUniformAddGroup G
inst_13 : T0Space G
inst_14 : CompleteSpace G
⊢ Continuous[instTopologicalSpaceProd, inst_10.toTopologicalSpace]
    (⋯.extend fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)

Tactic:
continuous_extend_of_cauchy _ ?_

Premises used: IsDenseInducing.continuous_extend_of_cauchy
-- 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
inst_12 : IsUniformAddGroup G
inst_13 : T0Space G
inst_14 : CompleteSpace G
refine :
  ∀ (b : α × γ),
    Cauchy.{u_5} (α := G)
      (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
        (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 b)))
⊢ Continuous[instTopologicalSpaceProd, inst_10.toTopologicalSpace]
    (⋯.extend fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)

Tactic:
refine continuous_extend_of_cauchy _ ?_

Premises used: IsDenseInducing.continuous_extend_of_cauchy
-- 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
inst_12 : IsUniformAddGroup G
inst_13 : T0Space G
inst_14 : CompleteSpace G
x₀ : α
y₀ : γ
left :
  NeBot.{u_5} (α := G)
    (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
      (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀))))
right :
  SProd.sprod (α := Filter G) (β := Filter G)
      (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
        (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀))))
      (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
        (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀)))) ≤
    𝓤 G
⊢ Cauchy.{u_5} (α := G)
    (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
      (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀))))

Tactic:
constructor
-- 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
inst_12 : IsUniformAddGroup G
inst_13 : T0Space G
inst_14 : CompleteSpace G
x₀ : α
y₀ : γ
left : NeBot (α := β × δ) (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀)))
⊢ NeBot.{u_5} (α := G)
    (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
      (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀))))

Tactic:
apply NeBot.map

Premises used: Filter.NeBot.map
-- 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
inst_12 : IsUniformAddGroup G
inst_13 : T0Space G
inst_14 : CompleteSpace G
x₀ : α
y₀ : γ
left : ∀ t ∈ 𝓝 (x₀, y₀), ∃ (a : β × δ), Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ) a ∈ t
⊢ NeBot (α := β × δ) (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀)))

Tactic:
apply comap_neBot

Premises used: Filter.comap_neBot
-- 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
inst_12 : IsUniformAddGroup G
inst_13 : T0Space G
inst_14 : CompleteSpace G
x₀ : α
y₀ : γ
U : Set (α × γ)
h : U ∈ 𝓝 (x₀, y₀)
left :
  ∀ (x : α × γ) (x_in : x ∈ U) (z : β × δ) (z_x : Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ) z = x),
    ∃ (a : β × δ), Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ) a ∈ U
⊢ ∃ (a : β × δ), Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ) a ∈ U

Tactic:
rcases mem_closure_iff_nhds.1 ((de.prodMap df).dense (x₀, y₀)) U h with ⟨x, x_in, ⟨z, z_x⟩⟩

Premises used: mem_closure_iff_nhds, Prod.mk, IsDenseInducing.dense, Iff.mp, IsDenseInducing.prodMap
-- 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
inst_12 : IsUniformAddGroup G
inst_13 : T0Space G
inst_14 : CompleteSpace G
x₀ : α
y₀ : γ
U : Set (α × γ)
h : U ∈ 𝓝 (x₀, y₀)
x : α × γ
x_in : x ∈ U
z : β × δ
z_x : Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ) z = x
left : Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ) z ∈ U
⊢ ∃ (a : β × δ), Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ) a ∈ U

Tactic:
exists z
-- 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
inst_12 : IsUniformAddGroup G
inst_13 : T0Space G
inst_14 : CompleteSpace G
x₀ : α
y₀ : γ
U : Set (α × γ)
h : U ∈ 𝓝 (x₀, y₀)
x : α × γ
x_in : x ∈ U
z : β × δ
z_x : Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ) z = x
⊢ Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ) z ∈ U

Tactic:
simp_all
-- 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
inst_12 : IsUniformAddGroup G
inst_13 : T0Space G
inst_14 : CompleteSpace G
x₀ : α
y₀ : γ
right :
  LE.le.{u_5} (α := Filter G)
    (map
      (fun (p : (β × δ) × β × δ) ↦
        HSub.hSub (α := G) ((fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G)) p.2)
          ((fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G)) p.1))
      (comap
        (fun (p : (β × δ) × β × δ) ↦
          (((e : (a : β) → α) p.1.1, (f : (a : δ) → γ) p.1.2), (e : (a : β) → α) p.2.1, (f : (a : δ) → γ) p.2.2))
        (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀))))
    (𝓝 0)
⊢ SProd.sprod (α := Filter G) (β := Filter G)
      (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
        (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀))))
      (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
        (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀)))) ≤
    𝓤 G

Tactic:
suffices map (fun p : (β × δ) × β × δ => (fun p : β × δ => φ p.1 p.2) p.2 -
      (fun p : β × δ => φ p.1 p.2) p.1)
        (comap (fun p : (β × δ) × β × δ => ((e p.1.1, f p.1.2), (e p.2.1, f p.2.2)))
        (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀))) ≤ 𝓝 0 by
      rwa [uniformity_eq_comap_nhds_zero G, prod_map_map_eq, ← map_le_iff_le_comap, Filter.map_map,
        prod_comap_comap_eq]