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)
rcases :
  ∀ (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 β),
      Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U ∧
        ∃ (V : Set δ),
          Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V ∧
            ∀ x ∈ U,
              ∀ x' ∈ U,
                ∀ y ∈ V,
                  ∀ y' ∈ V,
                    HSub.hSub (α := G)
                        ((fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G)) (x', y'))
                        ((fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G)) (x, y)) ∈
                      W'
⊢ ∃ (U : Set β),
    Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U ∧
      ∃ (V : Set δ),
        Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V ∧
          ∀ x ∈ U,
            ∀ x' ∈ U,
              ∀ y ∈ V,
                ∀ y' ∈ V,
                  HSub.hSub (α := G)
                      ((fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G)) (x', y'))
                      ((fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G)) (x, y)) ∈
                    W'

Tactic:
rcases exists_nhds_zero_quarter W'_nhds with ⟨W, W_nhds, W4⟩

Premises used: exists_nhds_zero_quarter
-- 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'
rcases :
  ∀ (U : Set (β × β)) (U_in : U ∈ comap ee (𝓝 (x₀, x₀))) (V : Set (δ × δ)) (V_in : V ∈ comap ff (𝓝 (y₀, y₀)))
    (H :
      ∀ (x : β × β) (y : δ × δ),
        x ∈ U →
          y ∈ V →
            (fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G))
                ((x, y).1.2 - (x, y).1.1, (x, y).2.2 - (x, y).2.1) ∈
              W),
    ∃ (U₁ : Set β),
      Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U₁ ∧
        ∃ (V₁ : Set δ),
          Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V₁ ∧
            ∀ 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
⊢ ∃ (U₁ : Set β),
    Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U₁ ∧
      ∃ (V₁ : Set δ),
        Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V₁ ∧
          ∀ 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

Tactic:
rcases tendsto_prod_iff.1 lim_φ_sub_sub W W_nhds with ⟨U, U_in, V, V_in, H⟩

Premises used: Filter.tendsto_prod_iff, Iff.mp
-- 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_in : ∃ (t : Set β), Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) t ∧ t ×ˢ t ⊆ U
V : Set (δ × δ)
V_in : ∃ (t : Set δ), Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) t ∧ t ×ˢ t ⊆ V
H :
  ∀ (x : β × β) (y : δ × δ),
    x ∈ U →
      y ∈ V →
        (fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G))
            ((x, y).1.2 - (x, y).1.1, (x, y).2.2 - (x, y).2.1) ∈
          W
rcases :
  ∀ (U₁ : Set β) (U₁_in : Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U₁) (HU₁ : U₁ ×ˢ U₁ ⊆ U),
    ∃ (U₁ : Set β),
      Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U₁ ∧
        ∃ (V₁ : Set δ),
          Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V₁ ∧
            ∀ 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
⊢ ∃ (U₁ : Set β),
    Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U₁ ∧
      ∃ (V₁ : Set δ),
        Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V₁ ∧
          ∀ 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

Tactic:
rcases U_in with ⟨U₁, U₁_in, HU₁⟩
-- 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 (β × β)
V : Set (δ × δ)
V_in : ∃ (t : Set δ), Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) t ∧ t ×ˢ t ⊆ V
H :
  ∀ (x : β × β) (y : δ × δ),
    x ∈ U →
      y ∈ V →
        (fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G))
            ((x, y).1.2 - (x, y).1.1, (x, y).2.2 - (x, y).2.1) ∈
          W
U₁ : Set β
U₁_in : Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U₁
HU₁ : U₁ ×ˢ U₁ ⊆ U
rcases :
  ∀ (V₁ : Set δ) (V₁_in : Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V₁) (HV₁ : V₁ ×ˢ V₁ ⊆ V),
    ∃ (U₁ : Set β),
      Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U₁ ∧
        ∃ (V₁ : Set δ),
          Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V₁ ∧
            ∀ 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
⊢ ∃ (U₁ : Set β),
    Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U₁ ∧
      ∃ (V₁ : Set δ),
        Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V₁ ∧
          ∀ 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

Tactic:
rcases V_in with ⟨V₁, V₁_in, HV₁⟩
-- 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 (β × β)
V : Set (δ × δ)
H :
  ∀ (x : β × β) (y : δ × δ),
    x ∈ U →
      y ∈ V →
        (fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G))
            ((x, y).1.2 - (x, y).1.1, (x, y).2.2 - (x, y).2.1) ∈
          W
U₁ : Set β
U₁_in : Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U₁
HU₁ : U₁ ×ˢ U₁ ⊆ U
V₁ : Set δ
V₁_in : Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V₁
HV₁ : V₁ ×ˢ V₁ ⊆ V
exists :
  ∀ 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
⊢ ∃ (U₁ : Set β),
    Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U₁ ∧
      ∃ (V₁ : Set δ),
        Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V₁ ∧
          ∀ 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

Tactic:
exists U₁, U₁_in, V₁, V₁_in
-- 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 (β × β)
V : Set (δ × δ)
H :
  ∀ (x : β × β) (y : δ × δ),
    x ∈ U →
      y ∈ V →
        (fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G))
            ((x, y).1.2 - (x, y).1.1, (x, y).2.2 - (x, y).2.1) ∈
          W
U₁ : Set β
U₁_in : Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U₁
HU₁ : U₁ ×ˢ U₁ ⊆ U
V₁ : Set δ
V₁_in : Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V₁
HV₁ : V₁ ×ˢ V₁ ⊆ V
x : β
x_in : x ∈ U₁
x' : β
x'_in : x' ∈ U₁
y : δ
y_in : y ∈ V₁
y' : δ
y'_in : y' ∈ V₁
⊢ (fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G)) (x' - x, y' - y) ∈ W

Tactic:
H _ _ (HU₁ (mk_mem_prod x_in x'_in)) (HV₁ (mk_mem_prod y_in y'_in))

Premises used: Set.Mem, Set.mk_mem_prod
-- 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 (β × β)
V : Set (δ × δ)
H :
  ∀ (x : β × β) (y : δ × δ),
    x ∈ U →
      y ∈ V →
        (fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G))
            ((x, y).1.2 - (x, y).1.1, (x, y).2.2 - (x, y).2.1) ∈
          W
U₁ : Set β
U₁_in : Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U₁
HU₁ : U₁ ×ˢ U₁ ⊆ U
V₁ : Set δ
V₁_in : Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V₁
HV₁ : V₁ ×ˢ V₁ ⊆ V
x : β
x_in : x ∈ U₁
x' : β
x'_in : x' ∈ U₁
y : δ
y_in : y ∈ V₁
y' : δ
y'_in : y' ∈ V₁
⊢ (fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G)) (x' - x, y' - y) ∈ W

Tactic:
exact H _ _ (HU₁ (mk_mem_prod x_in x'_in)) (HV₁ (mk_mem_prod y_in y'_in))

Premises used: Set.mk_mem_prod
-- 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 β),
    Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U₁ ∧
      ∃ (V₁ : Set δ),
        Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V₁ ∧
          ∀ 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

Tactic:
have :
    ∃ U₁ ∈ comap e (𝓝 x₀), ∃ V₁ ∈ comap f (𝓝 y₀), ∀ (x) (_ : x ∈ U₁) (x') (_ : x' ∈ U₁),
      ∀ (y) (_ : y ∈ V₁) (y') (_ : y' ∈ V₁), (fun p : β × δ => φ p.1 p.2) (x' - x, y' - y) ∈ W := by
    rcases tendsto_prod_iff.1 lim_φ_sub_sub W W_nhds with ⟨U, U_in, V, V_in, H⟩
    rw [nhds_prod_eq, ← prod_comap_comap_eq, mem_prod_same_iff] at U_in V_in
    rcases U_in with ⟨U₁, U₁_in, HU₁⟩
    rcases V_in with ⟨V₁, V₁_in, HV₁⟩
    exists U₁, U₁_in, V₁, V₁_in
    intro x x_in x' x'_in y y_in y' y'_in
    exact H _ _ (HU₁ (mk_mem_prod x_in x'_in)) (HV₁ (mk_mem_prod y_in y'_in))
-- 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
⊢ U₁.Nonempty

Tactic:
(de.comap_nhds_neBot _).nonempty_of_mem U₁_nhds

Premises used: IsDenseInducing.comap_nhds_neBot, Filter.NeBot.nonempty_of_mem