awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst_1 : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
q : Filter ι'
q' : Filter α'
h : TendstoUniformlyOnFilter F f p p'
h' : TendstoUniformlyOnFilter F' f' q q'
⊢ TendstoUniformlyOnFilter (fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ q) (p' ×ˢ q')
have rw : ∀ (h : Tendsto (fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β))
  (h' : Tendsto (fun (q : ι' × α') ↦ (f' q.2, F' q.1 q.2)) (q ×ˢ q') (𝓤 β')),
  Tendsto (β := (β × β') × β × β')
    (fun (q : (ι × ι') × α × α') ↦ (Prod.map f f' q.2, Prod.map (F q.1.1) (F' q.1.2) q.2)) ((p ×ˢ q) ×ˢ p' ×ˢ q')
    (𝓤 (β × β'))
Tactic: rw [tendstoUniformlyOnFilter_iff_tendsto] at h h' ⊢
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst_1 : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
q : Filter ι'
q' : Filter α'
h : Tendsto (fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β)
h' : Tendsto (fun (q : ι' × α') ↦ (f' q.2, F' q.1 q.2)) (q ×ˢ q') (𝓤 β')
⊢ Tendsto (β := (β × β') × β × β')
    (fun (q : (ι × ι') × α × α') ↦ (Prod.map f f' q.2, Prod.map (F q.1.1) (F' q.1.2) q.2)) ((p ×ˢ q) ×ˢ p' ×ˢ q')
    (𝓤 (β × β'))
have rw : Tendsto
  (Function.comp (β := (ι × ι') × α × α')
    ((fun (p : (β × β') × β × β') ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ∘ fun (q : (ι × ι') × α × α') ↦
      (Prod.map f f' q.2, Prod.map (F q.1.1) (F' q.1.2) q.2))
    fun (p : (ι × α) × ι' × α') ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
  ((p ×ˢ p') ×ˢ q ×ˢ q') (𝓤 β ×ˢ 𝓤 β')
Tactic: rw [uniformity_prod_eq_comap_prod, tendsto_comap_iff, ← map_swap4_prod, tendsto_map'_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst_1 : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
p' : Filter ι'
s' : Set α'
h : TendstoUniformlyOn F f p s
h' : TendstoUniformlyOn F' f' p' s'
⊢ TendstoUniformlyOn (fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') (s ×ˢ s')
have rw : ∀ (h : TendstoUniformlyOnFilter F f p (𝓟 s)) (h' : TendstoUniformlyOnFilter F' f' p' (𝓟 s')),
  TendstoUniformlyOnFilter (fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') (𝓟 (s ×ˢ s'))
Tactic: rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter] at h h' ⊢
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst_1 : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
p' : Filter ι'
h : TendstoUniformly F f p
h' : TendstoUniformly F' f' p'
⊢ TendstoUniformly (fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p')
have rw : ∀ (h : TendstoUniformlyOn F f p univ) (h' : TendstoUniformlyOn F' f' p' univ),
  TendstoUniformlyOn (fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p')
    (SProd.sprod (α := Set α) (β := Set α') univ univ)
Tactic: rw [← tendstoUniformlyOn_univ, ← univ_prod_univ] at *
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
c : β
⊢ Tendsto (↿F) (p ×ˢ p') (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun (x : α) ↦ c) p p'
have simp_rw : Tendsto (Prod.mk c ∘ ↿F) (p ×ˢ p') (𝓤 β) ↔ TendstoUniformlyOnFilter F (fun (x : α) ↦ c) p p'
Tactic: simp_rw [nhds_eq_comap_uniformity, tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
c : β
⊢ Tendsto (↿F) (p ×ˢ 𝓟 s) (𝓝 c) ↔ TendstoUniformlyOn F (fun (x : α) ↦ c) p s
have rw : Tendsto (↿F) (p ×ˢ 𝓟 s) (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun (x : α) ↦ c) p (𝓟 s)
Tactic: rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
p : Filter ι
c : β
⊢ Tendsto (↿F) (SProd.sprod (β := Filter α) p ⊤) (𝓝 c) ↔ TendstoUniformly F (fun (x : α) ↦ c) p
have rw : Tendsto (↿F) (SProd.sprod (β := Filter α) p ⊤) (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun (x : α) ↦ c) p ⊤
Tactic: rw [tendstoUniformly_iff_tendstoUniformlyOnFilter]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
⊢ TendstoUniformlyOn F f p {x} ↔ Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))
have simp_rw : (∀ s ∈ 𝓤 β, (fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) ⁻¹' s ∈ SProd.sprod (β := Filter α) p (𝓟 {x})) ↔
  ∀ s ∈ 𝓤 β, (fun (x_1 : ι) ↦ (f x, F x_1 x)) ⁻¹' s ∈ p
Tactic: simp_rw [tendstoUniformlyOn_iff_tendsto, Uniform.tendsto_nhds_right, tendsto_def]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
x : α
inst_1 : UniformSpace α
inst_2 : UniformSpace γ
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : (q : α × β) → (α × β) × α × β := fun (q : α × β) ↦ ((x, q.2), q)
⊢ TendstoUniformlyOn F (F x) (𝓝[U] x) V
have rw : Tendsto (fun (q : α × β) ↦ (F x q.2, F q.1 q.2)) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)
Tactic: rw [tendstoUniformlyOn_iff_tendsto]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
x : α
inst_1 : UniformSpace α
inst_2 : UniformSpace γ
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : (q : α × β) → (α × β) × α × β := fun (q : α × β) ↦ ((x, q.2), q)
⊢ Tendsto (fun (q : α × β) ↦ (F x q.2, F q.1 q.2)) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)
have change : Tendsto (Prod.map ↿F ↿F ∘ φ) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)
Tactic: change Tendsto (Prod.map ↿F ↿F ∘ φ) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
x : α
inst_1 : UniformSpace α
inst_2 : UniformSpace γ
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : (q : α × β) → (α × β) × α × β := fun (q : α × β) ↦ ((x, q.2), q)
⊢ Tendsto (Prod.map ↿F ↿F ∘ φ) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)
have simp : Tendsto (Prod.map ↿F ↿F ∘ φ) (comap Prod.fst (𝓝 x) ⊓ 𝓟 (Prod.fst ⁻¹' U ∩ Prod.snd ⁻¹' V)) (𝓤 γ)
Tactic: simp only [nhdsWithin, Filter.prod_eq_inf, comap_inf, inf_assoc, comap_principal, inf_principal]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
x : α
inst_1 : UniformSpace α
inst_2 : UniformSpace γ
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : (q : α × β) → (α × β) × α × β := fun (q : α × β) ↦ ((x, q.2), q)
⊢ Tendsto (Prod.map ↿F ↿F ∘ φ) (comap Prod.fst (𝓝 x) ⊓ 𝓟 (Prod.fst ⁻¹' U ∩ Prod.snd ⁻¹' V)) (𝓤 γ)
have refine : Tendsto φ (comap Prod.fst (𝓝 x)) (𝓤 (α × β))
Tactic: refine Tendsto.comp hF
    (Tendsto.inf ?_ <| tendsto_principal_principal.2 fun x hx => ⟨⟨hU, hx.2⟩, hx⟩)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
x : α
inst_1 : UniformSpace α
inst_2 : UniformSpace γ
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : (q : α × β) → (α × β) × α × β := fun (q : α × β) ↦ ((x, q.2), q)
⊢ Tendsto φ (comap Prod.fst (𝓝 x)) (𝓤 (α × β))
have simp : Tendsto ((fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ∘ φ) (comap (Prod.mk x ∘ Prod.fst) (𝓤 α))
  (𝓤 α ×ˢ 𝓤 β)
Tactic: simp only [uniformity_prod_eq_comap_prod, tendsto_comap_iff,
    nhds_eq_comap_uniformity, comap_comap]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
x : α
inst_1 : UniformSpace α
inst_2 : UniformSpace γ
f : α → β → γ
h : UniformContinuous₂ f
⊢ UniformContinuousOn (↿f) (SProd.sprod (α := Set α) (β := Set β) univ univ)
have rwa : UniformContinuousOn (↿f) univ
Tactic: rwa [univ_prod_univ, uniformContinuousOn_univ]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
x : α
inst_1 : UniformSpace α
inst_2 : UniformSpace γ
f : α → β → γ
h : UniformContinuous₂ f
rwa : UniformContinuousOn (↿f) univ
⊢ UniformContinuousOn (↿f) (SProd.sprod (α := Set α) (β := Set β) univ univ)
have rwa₁ : UniformContinuous ↿f
Tactic: rwa [univ_prod_univ, uniformContinuousOn_univ]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
l' : Filter α
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
⊢ TendstoUniformlyOnFilter F f l l' ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X × α) in l ×ˢ l', (f n.2, F n.1 n.2) ∈ sβ i
have rw : Tendsto (fun (q : X × α) ↦ (f q.2, F q.1 q.2)) (l ×ˢ l') (𝓤 β) ↔
  ∀ (i : ιβ), pβ i → ∀ᶠ (n : X × α) in l ×ˢ l', (f n.2, F n.1 n.2) ∈ sβ i
Tactic: rw [tendstoUniformlyOnFilter_iff_tendsto, hβ.tendsto_right_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
l' : Filter α
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
rw :
  Tendsto (fun (q : X × α) ↦ (f q.2, F q.1 q.2)) (l ×ˢ l') (𝓤 β) ↔
    ∀ (i : ιβ), pβ i → ∀ᶠ (n : X × α) in l ×ˢ l', (f n.2, F n.1 n.2) ∈ sβ i
⊢ TendstoUniformlyOnFilter F f l l' ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X × α) in l ×ˢ l', (f n.2, F n.1 n.2) ∈ sβ i
have rw₁ : (∀ (i : ιβ), pβ i → ∀ᶠ (x : X × α) in l ×ˢ l', (f x.2, F x.1 x.2) ∈ sβ i) ↔
  ∀ (i : ιβ), pβ i → ∀ᶠ (n : X × α) in l ×ˢ l', (f n.2, F n.1 n.2) ∈ sβ i
Tactic: rw [tendstoUniformlyOnFilter_iff_tendsto, hβ.tendsto_right_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
s : Set α
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
⊢ TendstoUniformlyOn F f l s ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ x ∈ s, (f x, F n x) ∈ sβ i
have simp_rw : Tendsto (fun (q : X × α) ↦ (f q.2, F q.1 q.2)) (l ×ˢ 𝓟 s) (𝓤 β) ↔
  ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ x ∈ s, (f x, F n x) ∈ sβ i
Tactic: simp_rw [tendstoUniformlyOn_iff_tendsto, hβ.tendsto_right_iff, eventually_prod_principal_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
s : Set α
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
simp_rw :
  Tendsto (fun (q : X × α) ↦ (f q.2, F q.1 q.2)) (l ×ˢ 𝓟 s) (𝓤 β) ↔
    ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ x ∈ s, (f x, F n x) ∈ sβ i
⊢ TendstoUniformlyOn F f l s ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ x ∈ s, (f x, F n x) ∈ sβ i
have simp_rw₁ : (∀ (i : ιβ), pβ i → ∀ᶠ (x : X × α) in l ×ˢ 𝓟 s, (f x.2, F x.1 x.2) ∈ sβ i) ↔
  ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ x ∈ s, (f x, F n x) ∈ sβ i
Tactic: simp_rw [tendstoUniformlyOn_iff_tendsto, hβ.tendsto_right_iff, eventually_prod_principal_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
⊢ TendstoUniformly F f l ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), (f x, F n x) ∈ sβ i
have simp_rw : TendstoUniformlyOn F f l univ ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), (f x, F n x) ∈ sβ i
Tactic: simp_rw [← tendstoUniformlyOn_univ, hβ.tendstoUniformlyOn_iff_of_uniformity, mem_univ,
    true_imp_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
simp_rw : TendstoUniformlyOn F f l univ ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), (f x, F n x) ∈ sβ i
⊢ TendstoUniformly F f l ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), (f x, F n x) ∈ sβ i
have simp_rw₁ : (∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), Membership.mem (γ := Set α) univ x → (f x, F n x) ∈ sβ i) ↔
  ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), (f x, F n x) ∈ sβ i
Tactic: simp_rw [← tendstoUniformlyOn_univ, hβ.tendstoUniformlyOn_iff_of_uniformity, mem_univ,
    true_imp_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
simp_rw : TendstoUniformlyOn F f l univ ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), (f x, F n x) ∈ sβ i
simp_rw₁ :
  (∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), Membership.mem (γ := Set α) univ x → (f x, F n x) ∈ sβ i) ↔
    ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), (f x, F n x) ∈ sβ i
⊢ TendstoUniformly F f l ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), (f x, F n x) ∈ sβ i
have simp_rw₂ : (∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), True → (f x, F n x) ∈ sβ i) ↔
  ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), (f x, F n x) ∈ sβ i
Tactic: simp_rw [← tendstoUniformlyOn_univ, hβ.tendstoUniformlyOn_iff_of_uniformity, mem_univ,
    true_imp_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
⊢ (∀ u ∈ 𝓤 β, ∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u) ↔
    ∀ u ∈ 𝓤 β, ∀ᶠ (m : Prod.{u_4, u_1} (ι × ι) α) in (p ×ˢ p) ×ˢ 𝓟 s, (F m.1.1 m.2, F m.1.2 m.2) ∈ u
have refine : ∀ (u : Set (β × β)) (hu : u ∈ 𝓤 β),
  (∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u) ↔
    ∀ᶠ (m : Prod.{u_4, u_1} (ι × ι) α) in (p ×ˢ p) ×ˢ 𝓟 s, (F m.1.1 m.2, F m.1.2 m.2) ∈ u
Tactic: refine forall₂_congr fun u hu => ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ (∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u) ↔
    ∀ᶠ (m : Prod.{u_4, u_1} (ι × ι) α) in (p ×ˢ p) ×ˢ 𝓟 s, (F m.1.1 m.2, F m.1.2 m.2) ∈ u
have rw : (∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u) ↔
  ∀ᶠ (x : ι × ι) in p ×ˢ p, ∀ y ∈ s, (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u
Tactic: rw [eventually_prod_principal_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∀ᶠ (m : Prod.{u_4, u_1} (ι × ι) α) in (p ×ˢ p) ×ˢ p', (F m.1.1 m.2, F m.1.2 m.2) ∈ u
have rcases : ∀ (t : Set (β × β)) (ht : t ∈ 𝓤 β) (htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t) (htmem : SetRel.comp t t ⊆ u),
  ∀ᶠ (m : Prod.{u_4, u_1} (ι × ι) α) in (p ×ˢ p) ×ˢ p', (F m.1.1 m.2, F m.1.2 m.2) ∈ u
Tactic: rcases comp_symm_of_uniformity hu with ⟨t, ht, htsymm, htmem⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
⊢ ∀ᶠ (m : Prod.{u_4, u_1} (ι × ι) α) in (p ×ˢ p) ×ˢ p', (F m.1.1 m.2, F m.1.2 m.2) ∈ u
have this : ∀ᶠ (x : Prod.{u_4, u_1} (ι × ι) (α × α)) in (p ×ˢ p) ×ˢ p' ×ˢ p',
  (f ((x.1.1, x.2.1), x.1.2, x.2.2).1.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 ((x.1.1, x.2.1), x.1.2, x.2.2).1.2) ∈ t ∧
    (f ((x.1.1, x.2.1), x.1.2, x.2.2).2.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 ((x.1.1, x.2.1), x.1.2, x.2.2).2.2) ∈ t
Tactic: have := tendsto_swap4_prod.eventually ((hF t ht).prod_mk (hF t ht))
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
this :
  ∀ᶠ (x : Prod.{u_4, u_1} (ι × ι) (α × α)) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.1.1, x.2.1), x.1.2, x.2.2).1.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 ((x.1.1, x.2.1), x.1.2, x.2.2).1.2) ∈
        t ∧
      (f ((x.1.1, x.2.1), x.1.2, x.2.2).2.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 ((x.1.1, x.2.1), x.1.2, x.2.2).2.2) ∈
        t
⊢ ∀ᶠ (m : Prod.{u_4, u_1} (ι × ι) α) in (p ×ˢ p) ×ˢ p', (F m.1.1 m.2, F m.1.2 m.2) ∈ u
have apply : ∀ (x : Prod.{u_4, u_1} (ι × ι) α),
  (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2,
          F (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.1
            (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2) ∈
        t ∧
      (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2,
          F (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.1
            (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2) ∈
        t →
    (F x.1.1 x.2, F x.1.2 x.2) ∈ u
Tactic: apply this.diag_of_prod_right.mono
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
this :
  ∀ᶠ (x : Prod.{u_4, u_1} (ι × ι) (α × α)) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.1.1, x.2.1), x.1.2, x.2.2).1.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 ((x.1.1, x.2.1), x.1.2, x.2.2).1.2) ∈
        t ∧
      (f ((x.1.1, x.2.1), x.1.2, x.2.2).2.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 ((x.1.1, x.2.1), x.1.2, x.2.2).2.2) ∈
        t
⊢ ∀ (x : Prod.{u_4, u_1} (ι × ι) α),
    (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2,
            F (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.1
              (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2) ∈
          t ∧
        (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2,
            F (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.1
              (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2) ∈
          t →
      (F x.1.1 x.2, F x.1.2 x.2) ∈ u
have simp : ∀ (a b : ι) (b_1 : α), (f b_1, F a b_1) ∈ t → (f b_1, F b b_1) ∈ t → (F a b_1, F b b_1) ∈ u
Tactic: simp only [and_imp, Prod.forall]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))
⊢ TendstoUniformlyOnFilter F f p p'
have inl : ∀ (hF : UniformCauchySeqOnFilter F ⊥ p') (hF' : ∀ᶠ (x : α) in p', Tendsto (fun (n : ι) ↦ F n x) ⊥ (𝓝 (f x))),
  TendstoUniformlyOnFilter F f ⊥ p'
Tactic: rcases p.eq_or_neBot with rfl | _
Cleared hypotheses: p, hF, hF'
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))
inl :
  ∀ (hF : UniformCauchySeqOnFilter F ⊥ p') (hF' : ∀ᶠ (x : α) in p', Tendsto (fun (n : ι) ↦ F n x) ⊥ (𝓝 (f x))),
    TendstoUniformlyOnFilter F f ⊥ p'
⊢ TendstoUniformlyOnFilter F f p p'
have inr : p.NeBot → TendstoUniformlyOnFilter F f p p'
Tactic: rcases p.eq_or_neBot with rfl | _
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))
h : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∀ᶠ (n : ι × α) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u
have inr : ∀ (t : Set (β × β)) (ht : t ∈ 𝓤 β) (htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t) (htmem : SetRel.comp t t ⊆ u),
  ∀ᶠ (n : ι × α) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u
Tactic: rcases comp_symm_of_uniformity hu with ⟨t, ht, htsymm, htmem⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))
h : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
⊢ ∀ᶠ (x : Prod.{u_4, u_1} (ι × ι) α) in (p ×ˢ p) ×ˢ p', Tendsto (fun (n : ι) ↦ F n x.2) p (𝓝 (f x.2))
have rw : ∃ (pa : ι × ι → Prop),
  (∀ᶠ (x : ι × ι) in p ×ˢ p, pa x) ∧
    ∃ (pb : α → Prop),
      (∀ᶠ (y : α) in p', pb y) ∧
        ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → Tendsto (fun (n : ι) ↦ F n (x, y).2) p (𝓝 (f (x, y).2))
Tactic: rw [eventually_prod_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))
h : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
⊢ ∀ᶠ (n : ι × α) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u
have hmc : ∀ᶠ (x : Prod.{u_4, u_1} (ι × ι) α) in (p ×ˢ p) ×ˢ p', Tendsto (fun (n : ι) ↦ F n x.2) p (𝓝 (f x.2))
Tactic: have hmc : ∀ᶠ x in (p ×ˢ p) ×ˢ p', Tendsto (fun n : ι => F n x.snd) p (𝓝 (f x.snd)) := by
    rw [eventually_prod_iff]
    exact ⟨fun _ => True, by simp, _, hF', by simp⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))
h : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
hmc : ∀ᶠ (x : Prod.{u_4, u_1} (ι × ι) α) in (p ×ˢ p) ×ˢ p', Tendsto (fun (n : ι) ↦ F n x.2) p (𝓝 (f x.2))
⊢ ∀ᶠ (n : ι × α) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u
have inr : ∀ᶠ (y : α × ι) in p' ×ˢ p, (f y.swap.2, F y.swap.1 y.swap.2) ∈ u
Tactic: rw [Filter.eventually_swap_iff]