awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hmc : ∀ᶠ (x : Prod.{u_4, u_1} (ι × ι) α) in (p ×ˢ p) ×ˢ p', Tendsto (fun (n : ι) ↦ F n x.2) p (𝓝 (f x.2))
⊢ ∀ᶠ (y : α × ι) in p' ×ˢ p, (f y.swap.2, F y.swap.1 y.swap.2) ∈ u
have this : ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
  (F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.1
          (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2,
        F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.2
          (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) ∈
      t ∧
    Tendsto (fun (n : ι) ↦ F n (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) p
      (𝓝 (f (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2))
Tactic: have := tendsto_prodAssoc.eventually (tendsto_prod_swap.eventually ((hF t ht).and hmc))
-- 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))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.1
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2,
          F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.2
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) ∈
        t ∧
      Tendsto (fun (n : ι) ↦ F n (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) p
        (𝓝 (f (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2))
⊢ ∀ᶠ (y : α × ι) in p' ×ˢ p, (f y.swap.2, F y.swap.1 y.swap.2) ∈ u
have inr : ∀ (x : α × ι),
  (∀ᶠ (y : ι) in p,
      (F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) (x, y))).1.1
              (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) (x, y))).2,
            F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) (x, y))).1.2
              (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) (x, y))).2) ∈
          t ∧
        Tendsto (fun (n : ι) ↦ F n (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) (x, y))).2) p
          (𝓝 (f (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) (x, y))).2))) →
    (f x.swap.2, F x.swap.1 x.swap.2) ∈ u
Tactic: apply this.curry.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 : 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))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.1
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2,
          F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.2
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) ∈
        t ∧
      Tendsto (fun (n : ι) ↦ F n (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) p
        (𝓝 (f (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2))
⊢ ∀ (x : α × ι),
    (∀ᶠ (y : ι) in p,
        (F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) (x, y))).1.1
                (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) (x, y))).2,
              F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) (x, y))).1.2
                (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) (x, y))).2) ∈
            t ∧
          Tendsto (fun (n : ι) ↦ F n (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) (x, y))).2) p
            (𝓝 (f (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) (x, y))).2))) →
      (f x.swap.2, F x.swap.1 x.swap.2) ∈ u
have inr : ∀ (a : α) (b : ι), (∀ᶠ (x : ι) in p, (F b a, F x a) ∈ t) → Tendsto (fun (n : ι) ↦ F n a) p (𝓝 (f a)) → (f a, F b a) ∈ u
Tactic: simp only [Equiv.prodAssoc_apply, eventually_and, eventually_const, Prod.snd_swap, Prod.fst_swap,
    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))
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))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.1
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2,
          F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.2
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) ∈
        t ∧
      Tendsto (fun (n : ι) ↦ F n (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) p
        (𝓝 (f (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))
⊢ (f x, F n x) ∈ u
have inr : (f x, F n x) ∈ SetRel.comp t t
Tactic: refine Set.mem_of_mem_of_subset ?_ 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 : 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))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.1
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2,
          F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.2
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) ∈
        t ∧
      Tendsto (fun (n : ι) ↦ F n (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) p
        (𝓝 (f (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))
⊢ (f x, F n x) ∈ SetRel.comp t t
have hm'₁ : Tendsto (fun (x_1 : ι) ↦ (f x, F x_1 x)) p (𝓤 β)
Tactic: rw [Uniform.tendsto_nhds_right] at hm'
Cleared hypotheses: hm'
-- 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
hmc : ∀ᶠ (x : Prod.{u_4, u_1} (ι × ι) α) in (p ×ˢ p) ×ˢ p', Tendsto (fun (n : ι) ↦ F n x.2) p (𝓝 (f x.2))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.1
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2,
          F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.2
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) ∈
        t ∧
      Tendsto (fun (n : ι) ↦ F n (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) p
        (𝓝 (f (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun (x_1 : ι) ↦ (f x, F x_1 x)) p (𝓤 β)
⊢ (f x, F n x) ∈ SetRel.comp t t
have this₁ : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t ∧ (fun (x_2 : ι) ↦ (f x, F x_2 x)) x_1 ∈ t
Tactic: have := hx.and (hm' 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 : 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))
this_1 :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.1
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2,
          F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.2
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) ∈
        t ∧
      Tendsto (fun (n : ι) ↦ F n (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) p
        (𝓝 (f (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun (x_1 : ι) ↦ (f x, F x_1 x)) p (𝓤 β)
this : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t ∧ (fun (x_2 : ι) ↦ (f x, F x_2 x)) x_1 ∈ t
⊢ (f x, F n x) ∈ SetRel.comp t t
have inr : ∀ (m : ι) (hm : (F n x, F m x) ∈ t ∧ (fun (x_1 : ι) ↦ (f x, F x_1 x)) m ∈ t), (f x, F n x) ∈ SetRel.comp t t
Tactic: obtain ⟨m, hm⟩ := this.exists
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s s' : Set α
p : Filter ι
hf : UniformCauchySeqOn F p s
hss' : s' ⊆ s
⊢ UniformCauchySeqOn F p s'
have rw : ∀ (hf : UniformCauchySeqOnFilter F p (𝓟 s)) (hss' : s' ⊆ s), UniformCauchySeqOnFilter F p (𝓟 s')
Tactic: rw [uniformCauchySeqOn_iff_uniformCauchySeqOnFilter] at hf ⊢
Cleared hypotheses: hf, hss'
-- 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 α
γ : Type u_5
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∀ᶠ (m : Prod.{u_4, u_5} (ι × ι) γ) in (p ×ˢ p) ×ˢ comap g p',
    ((fun (n : ι) ↦ F n ∘ g) m.1.1 m.2, (fun (n : ι) ↦ F n ∘ g) m.1.2 m.2) ∈ u
have obtain : ∀ (pa : ι × ι → Prop) (hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x) (pb : α → Prop) (hpb : ∀ᶠ (y : α) in p', pb y)
  (hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u),
  ∀ᶠ (m : Prod.{u_4, u_5} (ι × ι) γ) in (p ×ˢ p) ×ˢ comap g p',
    ((fun (n : ι) ↦ F n ∘ g) m.1.1 m.2, (fun (n : ι) ↦ F n ∘ g) m.1.2 m.2) ∈ u
Tactic: obtain ⟨pa, hpa, pb, hpb, hpapb⟩ := eventually_prod_iff.mp (hf 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 : ι → α → β
p : Filter ι
p' : Filter α
γ : Type u_5
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
pa : ι × ι → Prop
hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in p', pb y
hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u
⊢ ∀ᶠ (m : Prod.{u_4, u_5} (ι × ι) γ) in (p ×ˢ p) ×ˢ comap g p',
    ((fun (n : ι) ↦ F n ∘ g) m.1.1 m.2, (fun (n : ι) ↦ F n ∘ g) m.1.2 m.2) ∈ u
have rw : ∃ (pa : ι × ι → Prop),
  (∀ᶠ (x : ι × ι) in p ×ˢ p, pa x) ∧
    ∃ (pb : γ → Prop),
      (∀ᶠ (y : γ) in comap g p', pb y) ∧
        ∀ {x : ι × ι},
          pa x →
            ∀ {y : γ},
              pb y → ((fun (n : ι) ↦ F n ∘ g) (x, y).1.1 (x, y).2, (fun (n : ι) ↦ F n ∘ g) (x, y).1.2 (x, y).2) ∈ u
Tactic: rw [eventually_prod_iff]
-- 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 α
γ : Type u_5
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
pa : ι × ι → Prop
hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in p', pb y
hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u
⊢ ∃ (pa : ι × ι → Prop),
    (∀ᶠ (x : ι × ι) in p ×ˢ p, pa x) ∧
      ∃ (pb : γ → Prop),
        (∀ᶠ (y : γ) in comap g p', pb y) ∧
          ∀ {x : ι × ι},
            pa x →
              ∀ {y : γ},
                pb y → ((fun (n : ι) ↦ F n ∘ g) (x, y).1.1 (x, y).2, (fun (n : ι) ↦ F n ∘ g) (x, y).1.2 (x, y).2) ∈ u
have refine : ∀ᶠ (y : γ) in comap g p', (pb ∘ g) y
Tactic: refine ⟨pa, hpa, pb ∘ g, ?_, fun hx _ hy => hpapb hx hy⟩
-- 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 ι
γ : Type u_5
hf : UniformCauchySeqOn F p s
g : γ → α
⊢ UniformCauchySeqOn.{u_5, u_2, u_4} (β := β) (fun (n : ι) ↦ F n ∘ g) p (g ⁻¹' s)
have rw : ∀ (hf : UniformCauchySeqOnFilter F p (𝓟 s)) (g : γ → α),
  UniformCauchySeqOnFilter.{u_5, u_2, u_4} (β := β) (fun (n : ι) ↦ F n ∘ g) p (𝓟 (g ⁻¹' s))
Tactic: rw [uniformCauchySeqOn_iff_uniformCauchySeqOnFilter] at hf ⊢
Cleared hypotheses: hf, g
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst_1 : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
hu : Membership.mem (γ := Filter ((β × β') × β × β')) (𝓤 (β × β')) u
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ x ∈ s ×ˢ s',
      ((fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) m.1 x, (fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) m.2 x) ∈ u
have hu₁ : ∃ t₁ ∈ 𝓤 β, ∃ t₂ ∈ 𝓤 β', t₁ ×ˢ t₂ ⊆ (fun (p : Prod.{u_2, u_7} (β × β) (β' × β')) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' u
Tactic: rw [uniformity_prod_eq_prod, mem_map, mem_prod_iff] at hu
Cleared hypotheses: 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 ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst_1 : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
hu :
  ∃ t₁ ∈ 𝓤 β,
    ∃ t₂ ∈ 𝓤 β', t₁ ×ˢ t₂ ⊆ (fun (p : Prod.{u_2, u_7} (β × β) (β' × β')) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' u
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ x ∈ s ×ˢ s',
      ((fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) m.1 x, (fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) m.2 x) ∈ u
have obtain : ∀ (v : Set (β × β)) (hv : v ∈ 𝓤 β) (w : Set (β' × β')) (hw : w ∈ 𝓤 β')
  (hvw : v ×ˢ w ⊆ (fun (p : Prod.{u_2, u_7} (β × β) (β' × β')) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' u),
  ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ x ∈ s ×ˢ s',
      ((fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) m.1 x, (fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) m.2 x) ∈ u
Tactic: obtain ⟨v, hv, w, hw, hvw⟩ := hu
Cleared hypotheses: 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 ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst_1 : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : v ×ˢ w ⊆ (fun (p : Prod.{u_2, u_7} (β × β) (β' × β')) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' u
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ x ∈ s ×ˢ s',
      ((fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) m.1 x, (fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) m.2 x) ∈ u
have simp_rw : ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
  ∀ (a : α) (b : α'), a ∈ s → b ∈ s' → ((F m.1.1 a, F' m.1.2 b), F m.2.1 a, F' m.2.2 b) ∈ u
Tactic: simp_rw [mem_prod, and_imp, Prod.forall, Prod.map_apply]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst_1 : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : v ×ˢ w ⊆ (fun (p : Prod.{u_2, u_7} (β × β) (β' × β')) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' u
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ (a : α) (b : α'), a ∈ s → b ∈ s' → ((F m.1.1 a, F' m.1.2 b), F m.2.1 a, F' m.2.2 b) ∈ u
have hvw₁ : (fun (p : Prod.{u_2, u_7} (β × β) (β' × β')) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) '' v ×ˢ w ⊆ u
Tactic: rw [← Set.image_subset_iff] at hvw
Cleared hypotheses: hvw
-- 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 ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst_1 : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : (fun (p : Prod.{u_2, u_7} (β × β) (β' × β')) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) '' v ×ˢ w ⊆ u
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ (a : α) (b : α'), a ∈ s → b ∈ s' → ((F m.1.1 a, F' m.1.2 b), F m.2.1 a, F' m.2.2 b) ∈ u
have apply : ∀ (x : (ι × ι') × ι × ι'),
  ((∀ x_1 ∈ s, (F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 x_1, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.2 x_1) ∈ v) ∧
      ∀ x_1 ∈ s', (F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 x_1, F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.2 x_1) ∈ w) →
    ∀ (a : α) (b : α'), a ∈ s → b ∈ s' → ((F x.1.1 a, F' x.1.2 b), F x.2.1 a, F' x.2.2 b) ∈ u
Tactic: apply (tendsto_swap4_prod.eventually ((h v hv).prod_mk (h' w hw))).mono
-- 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 α
x : α
p : Filter ι
hp : p.NeBot
hf : UniformCauchySeqOn F p s
hx : x ∈ s
⊢ Cauchy.{u_2} (α := β) (map (fun (i : ι) ↦ F i x) p)
have simp : Tendsto (fun (p : ι × ι) ↦ (F p.1 x, F p.2 x)) (p ×ˢ p) (𝓤 β)
Tactic: simp only [cauchy_map_iff, hp, true_and]
-- 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 α
x : α
p : Filter ι
hp : p.NeBot
hf : UniformCauchySeqOn F p s
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ (fun (p : ι × ι) ↦ (F p.1 x, F p.2 x)) ⁻¹' u ∈ p ×ˢ p
have h : ∀ (a : ι × ι),
  Membership.mem (γ := Set (ι × ι))
    {x_1 : ι × ι |
      Membership.mem (γ := Set (ι × ι)) {x : ι × ι | (fun (m : ι × ι) ↦ ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u) x} x_1 →
        Membership.mem (γ := Set (ι × ι)) ((fun (p : ι × ι) ↦ (F p.1 x, F p.2 x)) ⁻¹' u) x_1}
    a
Tactic: filter_upwards [hf u hu] with p hp using hp x hx
-- 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 α
x : α
p : Filter ι
hp : p.NeBot
hf : UniformCauchySeqOn F p s
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
h :
  ∀ (a : ι × ι),
    Membership.mem (γ := Set (ι × ι))
      {x_1 : ι × ι |
        Membership.mem (γ := Set (ι × ι)) {x : ι × ι | (fun (m : ι × ι) ↦ ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u) x} x_1 →
          Membership.mem (γ := Set (ι × ι)) ((fun (p : ι × ι) ↦ (F p.1 x, F p.2 x)) ⁻¹' u) x_1}
      a
⊢ (fun (p : ι × ι) ↦ (F p.1 x, F p.2 x)) ⁻¹' u ∈ p ×ˢ p
have h₁ : ∀ (a : ι × ι),
  (∀ x ∈ s, (F a.1 x, F a.2 x) ∈ u) → Membership.mem (γ := Set (ι × ι)) ((fun (p : ι × ι) ↦ (F p.1 x, F p.2 x)) ⁻¹' u) a
Tactic: filter_upwards [hf u hu] with p hp using hp x hx
-- 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 α
l : Filter ι
inst_1 : l.IsCountablyGenerated
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun (n : ℕ) ↦ F (u n)) f atTop s
⊢ TendstoUniformlyOn F f l s
have rw : ∀ (x : ℕ → ι × α), Tendsto x atTop (l ×ˢ 𝓟 s) → Tendsto ((fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) ∘ x) atTop (𝓤 β)
Tactic: rw [tendstoUniformlyOn_iff_tendsto, tendsto_iff_seq_tendsto]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
inst_1 : l.IsCountablyGenerated
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun (n : ℕ) ↦ F (u n)) f atTop s
u : ℕ → ι × α
hu : Tendsto u atTop (l ×ˢ 𝓟 s)
⊢ Tendsto ((fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) ∘ u) atTop (𝓤 β)
have hu₁ : Tendsto (fun (n : ℕ) ↦ (u n).1) atTop l ∧ Tendsto (fun (n : ℕ) ↦ (u n).2) atTop (𝓟 s)
Tactic: rw [tendsto_prod_iff'] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
inst_1 : l.IsCountablyGenerated
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun (n : ℕ) ↦ F (u n)) f atTop s
u : ℕ → ι × α
hu : Tendsto (fun (n : ℕ) ↦ (u n).1) atTop l ∧ Tendsto (fun (n : ℕ) ↦ (u n).2) atTop (𝓟 s)
⊢ Tendsto ((fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) ∘ u) atTop (𝓤 β)
have h₁ : TendstoUniformlyOn (fun (n : ℕ) ↦ F (u n).1) f atTop s
Tactic: specialize h (fun n => (u n).fst) hu.1
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
inst_1 : l.IsCountablyGenerated
u : ℕ → ι × α
hu : Tendsto (fun (n : ℕ) ↦ (u n).1) atTop l ∧ Tendsto (fun (n : ℕ) ↦ (u n).2) atTop (𝓟 s)
h : TendstoUniformlyOn (fun (n : ℕ) ↦ F (u n).1) f atTop s
⊢ Tendsto ((fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) ∘ u) atTop (𝓤 β)
have h₁ : Tendsto (fun (q : ℕ × α) ↦ (f q.2, F (u q.1).1 q.2)) (SProd.sprod (α := Filter ℕ) atTop (𝓟 s)) (𝓤 β)
Tactic: rw [tendstoUniformlyOn_iff_tendsto] at h
Cleared hypotheses: h