awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
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)
⊢ ∃ (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'
have lim1 : 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 :)
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
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₁))
⊢ ∃ (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'
have lim2 : 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₁)
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
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)
⊢ ∃ (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'
have 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)
Tactic: have lim := lim2.comp lim1
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
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)
⊢ ∃ (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'
have 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
Tactic: rw [tendsto_prod_self_iff] at lim
Cleared hypotheses: lim
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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₂ ∧
      ∀ x ∈ U₂,
        ∀ x' ∈ U₂, (fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G)) (x' - x, y₁) ∈ W'
have 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)
Tactic: simp_rw [forall_mem_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
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)
⊢ ∃ (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'
have lim_φ : 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)
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
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))
have 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)
Tactic: have := Filter.prod_mono (tendsto_sub_comap_self de x₀) (tendsto_sub_comap_self df y₀)
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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)
⊢ 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))
have 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))
Tactic: rwa [prod_map_map_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
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)
have 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))
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
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
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 (β := 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)
have 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))
Tactic: rw [← nhds_prod_eq] at lim_sub_sub
Cleared hypotheses: lim_sub_sub
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
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)
⊢ ∃ (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'
have 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)
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