awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h :
  ∀ x ∈ s,
    ∀ u ∈ 𝓤 β,
      ∃ (pa : ι → Prop),
        (∀ᶠ (x : ι) in p, pa x) ∧
          ∃ (pb : α → Prop), (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
have mpr : ∀ (pa : ι → Prop) (hpa : ∀ᶠ (x : ι) in p, pa x) (pb : α → Prop) (hpb : ∀ᶠ (y : α) in 𝓝[s] x, pb y)
  (h : ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u), ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
Tactic: obtain ⟨pa, hpa, pb, hpb, h⟩ := h x hx u hu
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
hf : TendstoLocallyUniformlyOn F f p s
a : α
ha : a ∈ s
⊢ Tendsto (fun (i : ι) ↦ F i a) p (𝓝 (f a))
have refine : 𝓟 {a} ≤ 𝓝[s] a
Tactic: refine ((tendstoLocallyUniformlyOn_iff_filter.mp hf) a ha).tendsto_at ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
G : ι → α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x)
⊢ TendstoLocallyUniformlyOn G f p s
have hg₁ : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2)
Tactic: have hg : ∀ᶠ x in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2) := by
    simpa using eventually_prod_principal_iff.2 hg
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
G : ι → α → β
hf : TendstoLocallyUniformlyOn F f p s
hg_1 : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2)
⊢ TendstoLocallyUniformlyOn G f p s
have rw : ∀ (hf : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β))
  (hg : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x))
  (hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2)),
  ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
Tactic: rw [tendstoLocallyUniformlyOn_iff_forall_tendsto] at hf ⊢
Cleared hypotheses: hf, hg_1, hg
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
G : ι → α → β
hf : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hg_1 : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2)
⊢ ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
have refine : ∀ (x : α) (hx : x ∈ s) (hf : Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)),
  Tendsto (fun (y : ι × α) ↦ (f y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
Tactic: refine forall₂_imp (fun x hx hf => ?_) hf
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
G : ι → α → β
hf_1 : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hg_1 : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2)
x : α
hx : x ∈ s
hf : Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
⊢ Tendsto (fun (y : ι × α) ↦ (f y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
have rw : ∀
  (hf :
    ∀ (i : SetRel β β),
      i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (f x.2, F x.1 x.2) ∈ id i)
  (i : SetRel β β),
  i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (f x.2, G x.1 x.2) ∈ id i
Tactic: rw [uniformity_hasBasis_open.tendsto_right_iff] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ x ∈ s, Inseparable (f x) (g x)
⊢ ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (f x.2) (g x.2)
have rw : ∀ᶠ (x : ι) in p, ∀ y ∈ s, Inseparable (f (x, y).2) (g (x, y).2)
Tactic: rw [eventually_prod_principal_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ x ∈ s, Inseparable (f x) (g x)
⊢ TendstoLocallyUniformlyOn F g p s
have hg₁ : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (f x.2) (g x.2)
Tactic: have hg : ∀ᶠ x in p ×ˢ 𝓟 s, Inseparable (f x.2) (g x.2) := by
    rw [eventually_prod_principal_iff]
    exact .of_forall fun _ => hg
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf : TendstoLocallyUniformlyOn F f p s
hg_1 : ∀ x ∈ s, Inseparable (f x) (g x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (f x.2) (g x.2)
⊢ TendstoLocallyUniformlyOn F g p s
have rw : ∀ (hf : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β))
  (hg : ∀ x ∈ s, Inseparable (f x) (g x)) (hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (f x.2) (g x.2)),
  ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (g y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
Tactic: rw [tendstoLocallyUniformlyOn_iff_forall_tendsto] at hf ⊢
Cleared hypotheses: hf, hg_1, hg
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hg_1 : ∀ x ∈ s, Inseparable (f x) (g x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (f x.2) (g x.2)
⊢ ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (g y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
have refine : ∀ (x : α) (hx : x ∈ s) (hf : Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)),
  Tendsto (fun (y : ι × α) ↦ (g y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
Tactic: refine forall₂_imp (fun x hx hf => ?_) hf
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf_1 : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hg_1 : ∀ x ∈ s, Inseparable (f x) (g x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (f x.2) (g x.2)
x : α
hx : x ∈ s
hf : Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
⊢ Tendsto (fun (y : ι × α) ↦ (g y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
have rw : ∀
  (hf :
    ∀ (i : SetRel β β),
      i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (f x.2, F x.1 x.2) ∈ id i)
  (i : SetRel β β),
  i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (g x.2, F x.1 x.2) ∈ id i
Tactic: rw [uniformity_hasBasis_open.tendsto_right_iff] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Matrix (goal)
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : UniformSpace 𝕜
⊢ Eq (α := Filter (Matrix m n 𝕜 × Matrix m n 𝕜)) (𝓤 (Matrix m n 𝕜))
    (⨅ (i : m), ⨅ (j : n), Filter.comap (fun (a : Matrix m n 𝕜 × Matrix m n 𝕜) ↦ (a.1 i j, a.2 i j)) (𝓤 𝕜))
have erw : Eq (α := Filter (Matrix m n 𝕜 × Matrix m n 𝕜))
  (⨅ (i : m),
    Filter.comap (β := (n → 𝕜) × (n → 𝕜)) (fun (a : ((i : m) → n → 𝕜) × ((i : m) → n → 𝕜)) ↦ (a.1 i, a.2 i))
      (𝓤 (n → 𝕜)))
  (⨅ (i : m), ⨅ (j : n), Filter.comap (fun (a : Matrix m n 𝕜 × Matrix m n 𝕜) ↦ (a.1 i j, a.2 i j)) (𝓤 𝕜))
Tactic: erw [Pi.uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Matrix (goal)
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : UniformSpace 𝕜
⊢ Eq (α := Filter (Matrix m n 𝕜 × Matrix m n 𝕜))
    (⨅ (i : m),
      Filter.comap (β := (n → 𝕜) × (n → 𝕜)) (fun (a : ((i : m) → n → 𝕜) × ((i : m) → n → 𝕜)) ↦ (a.1 i, a.2 i))
        (𝓤 (n → 𝕜)))
    (⨅ (i : m), ⨅ (j : n), Filter.comap (fun (a : Matrix m n 𝕜 × Matrix m n 𝕜) ↦ (a.1 i j, a.2 i j)) (𝓤 𝕜))
have simp_rw : Eq (α := Filter (Matrix m n 𝕜 × Matrix m n 𝕜))
  (⨅ (i : m),
    ⨅ (i_1 : n),
      Filter.comap
        ((fun (a : ((i : n) → 𝕜) × ((i : n) → 𝕜)) ↦ (a.1 i_1, a.2 i_1)) ∘
          fun (a : ((i : m) → n → 𝕜) × ((i : m) → n → 𝕜)) ↦ (a.1 i, a.2 i))
        (𝓤 𝕜))
  (⨅ (i : m), ⨅ (j : n), Filter.comap (fun (a : Matrix m n 𝕜 × Matrix m n 𝕜) ↦ (a.1 i j, a.2 i j)) (𝓤 𝕜))
Tactic: simp_rw [Pi.uniformity, Filter.comap_iInf, Filter.comap_comap]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Matrix (goal)
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : UniformSpace 𝕜
β : Type u_4
inst_1 : UniformSpace β
f : β → Matrix m n 𝕜
⊢ UniformContinuous f ↔ ∀ (i : m) (j : n), UniformContinuous.{u_4, u_3} (β := 𝕜) fun (x : β) ↦ f x i j
have simp : (∀ (i : m) (i_1 : n),
    Filter.Tendsto ((fun (a : Matrix m n 𝕜 × Matrix m n 𝕜) ↦ (a.1 i i_1, a.2 i i_1)) ∘ fun (x : β × β) ↦ (f x.1, f x.2))
      (𝓤 β) (𝓤 𝕜)) ↔
  ∀ (i : m) (j : n), Filter.Tendsto (fun (x : β × β) ↦ (f x.1 i j, f x.2 i j)) (𝓤 β) (𝓤 𝕜)
Tactic: simp only [UniformContinuous, Matrix.uniformity, Filter.tendsto_iInf, Filter.tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Matrix (goal)
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : UniformSpace 𝕜
β : Type u_4
inst_1 : UniformSpace β
f : β → Matrix m n 𝕜
⊢ (∀ (i : m) (i_1 : n),
      Filter.Tendsto
        ((fun (a : Matrix m n 𝕜 × Matrix m n 𝕜) ↦ (a.1 i i_1, a.2 i i_1)) ∘ fun (x : β × β) ↦ (f x.1, f x.2)) (𝓤 β)
        (𝓤 𝕜)) ↔
    ∀ (i : m) (j : n), Filter.Tendsto (fun (x : β × β) ↦ (f x.1 i j, f x.2 i j)) (𝓤 β) (𝓤 𝕜)
have mp : (∀ (i : m) (i_1 : n),
    Filter.Tendsto ((fun (a : Matrix m n 𝕜 × Matrix m n 𝕜) ↦ (a.1 i i_1, a.2 i i_1)) ∘ fun (x : β × β) ↦ (f x.1, f x.2))
      (𝓤 β) (𝓤 𝕜)) →
  ∀ (i : m) (j : n), Filter.Tendsto (fun (x : β × β) ↦ (f x.1 i j, f x.2 i j)) (𝓤 β) (𝓤 𝕜)
Tactic: apply Iff.intro
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Matrix (goal)
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : UniformSpace 𝕜
β : Type u_4
inst_1 : UniformSpace β
f : β → Matrix m n 𝕜
mp :
  (∀ (i : m) (i_1 : n),
      Filter.Tendsto
        ((fun (a : Matrix m n 𝕜 × Matrix m n 𝕜) ↦ (a.1 i i_1, a.2 i i_1)) ∘ fun (x : β × β) ↦ (f x.1, f x.2)) (𝓤 β)
        (𝓤 𝕜)) →
    ∀ (i : m) (j : n), Filter.Tendsto (fun (x : β × β) ↦ (f x.1 i j, f x.2 i j)) (𝓤 β) (𝓤 𝕜)
⊢ (∀ (i : m) (i_1 : n),
      Filter.Tendsto
        ((fun (a : Matrix m n 𝕜 × Matrix m n 𝕜) ↦ (a.1 i i_1, a.2 i i_1)) ∘ fun (x : β × β) ↦ (f x.1, f x.2)) (𝓤 β)
        (𝓤 𝕜)) ↔
    ∀ (i : m) (j : n), Filter.Tendsto (fun (x : β × β) ↦ (f x.1 i j, f x.2 i j)) (𝓤 β) (𝓤 𝕜)
have mpr : (∀ (i : m) (j : n), Filter.Tendsto (fun (x : β × β) ↦ (f x.1 i j, f x.2 i j)) (𝓤 β) (𝓤 𝕜)) →
  ∀ (i : m) (i_1 : n),
    Filter.Tendsto ((fun (a : Matrix m n 𝕜 × Matrix m n 𝕜) ↦ (a.1 i i_1, a.2 i i_1)) ∘ fun (x : β × β) ↦ (f x.1, f x.2))
      (𝓤 β) (𝓤 𝕜)
Tactic: apply Iff.intro
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfFun (goal)
Goal:
X : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : PartialOrder M
d : X → X → M
refl : ∀ (x : X), d x x = 0
symm : ∀ (x y : X), d x y = d y x
triangle : ∀ (x y z : X), d x z ≤ d x y + d y z
half : ∀ ε > 0, ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε
r : M
h : r > 0
x : X × X
hx : Membership.mem (γ := Set (X × X)) {x : X × X | d x.1 x.2 < r} x
⊢ Membership.mem (γ := Set (X × X)) {x : X × X | d x.1 x.2 < r} x.swap
have rwa : d x.swap.1 x.swap.2 < r
Tactic: rwa [mem_setOf, symm]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.OfFun (goal)
Goal:
X : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : PartialOrder M
d : X → X → M
refl : ∀ (x : X), d x x = 0
symm : ∀ (x y : X), d x y = d y x
triangle : ∀ (x y z : X), d x z ≤ d x y + d y z
half : ∀ ε > 0, ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε
r : M
h : r > 0
x : X × X
hx : Membership.mem (γ := Set (X × X)) {x : X × X | d x.1 x.2 < r} x
rwa : d x.swap.1 x.swap.2 < r
⊢ Membership.mem (γ := Set (X × X)) {x : X × X | d x.1 x.2 < r} x.swap
have rwa₁ : d x.swap.2 x.swap.1 < r
Tactic: rwa [mem_setOf, symm]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Path (goal)
Goal:
X : Type u_1
inst : UniformSpace X
x y z : X
U : Set (X × X)
hU : U ∈ 𝓤 X
x_1 x_2 : Path x y × Path y z
t : (↑I : Type)
fst : Path x y
snd : Path y z
fst_1 : Path x y
snd_1 : Path y z
h :
  Membership.mem (γ := SetRel (Path x y × Path y z) (Path x y × Path y z))
    (entourageProd
      {γ : Path x y × Path x y |
        ∀ (t : (↑I : Type)),
          Membership.mem (α := X × X) (U, U).1
            (((γ.1 : (a : (↑I : Type)) → X) t, (γ.2 : (a : (↑I : Type)) → X) t) : X × X)}
      {γ : Path y z × Path y z |
        ∀ (t : (↑I : Type)),
          Membership.mem (α := X × X) (U, U).2
            (((γ.1 : (a : (↑I : Type)) → X) t, (γ.2 : (a : (↑I : Type)) → X) t) : X × X)})
    ((fst, snd), fst_1, snd_1)
h₁ :
  Membership.mem (γ := SetRel (Path x y) (Path x y))
    {γ : Path x y × Path x y |
      ∀ (t : (↑I : Type)),
        Membership.mem (α := X × X) (U, U).1
          (((γ.1 : (a : (↑I : Type)) → X) t, (γ.2 : (a : (↑I : Type)) → X) t) : X × X)}
    (fst, fst_1)
h₂ :
  Membership.mem (γ := SetRel (Path y z) (Path y z))
    {γ : Path y z × Path y z |
      ∀ (t : (↑I : Type)),
        Membership.mem (α := X × X) (U, U).2
          (((γ.1 : (a : (↑I : Type)) → X) t, (γ.2 : (a : (↑I : Type)) → X) t) : X × X)}
    (snd, snd_1)
⊢ Membership.mem (α := X × X) U
    ((((Function.uncurry trans (fst, snd), Function.uncurry trans (fst_1, snd_1)).1 : (a : (↑I : Type)) → X) t,
        ((Function.uncurry trans (fst, snd), Function.uncurry trans (fst_1, snd_1)).2 : (a : (↑I : Type)) → X) t) :
      X × X)
have pos : ∀ (ht : (↑t : ℝ) ≤ 2⁻¹),
  Membership.mem (α := X × X) U
    ((((Function.uncurry trans (fst, snd), Function.uncurry trans (fst_1, snd_1)).1 : (a : (↑I : Type)) → X) t,
        ((Function.uncurry trans (fst, snd), Function.uncurry trans (fst_1, snd_1)).2 : (a : (↑I : Type)) → X) t) :
      X × X)
Tactic: by_cases ht : (t : ℝ) ≤ 2⁻¹
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Path (goal)
Goal:
X : Type u_1
inst : UniformSpace X
x y z : X
U : Set (X × X)
hU : U ∈ 𝓤 X
x_1 x_2 : Path x y × Path y z
t : (↑I : Type)
fst : Path x y
snd : Path y z
fst_1 : Path x y
snd_1 : Path y z
h :
  Membership.mem (γ := SetRel (Path x y × Path y z) (Path x y × Path y z))
    (entourageProd
      {γ : Path x y × Path x y |
        ∀ (t : (↑I : Type)),
          Membership.mem (α := X × X) (U, U).1
            (((γ.1 : (a : (↑I : Type)) → X) t, (γ.2 : (a : (↑I : Type)) → X) t) : X × X)}
      {γ : Path y z × Path y z |
        ∀ (t : (↑I : Type)),
          Membership.mem (α := X × X) (U, U).2
            (((γ.1 : (a : (↑I : Type)) → X) t, (γ.2 : (a : (↑I : Type)) → X) t) : X × X)})
    ((fst, snd), fst_1, snd_1)
h₁ :
  Membership.mem (γ := SetRel (Path x y) (Path x y))
    {γ : Path x y × Path x y |
      ∀ (t : (↑I : Type)),
        Membership.mem (α := X × X) (U, U).1
          (((γ.1 : (a : (↑I : Type)) → X) t, (γ.2 : (a : (↑I : Type)) → X) t) : X × X)}
    (fst, fst_1)
h₂ :
  Membership.mem (γ := SetRel (Path y z) (Path y z))
    {γ : Path y z × Path y z |
      ∀ (t : (↑I : Type)),
        Membership.mem (α := X × X) (U, U).2
          (((γ.1 : (a : (↑I : Type)) → X) t, (γ.2 : (a : (↑I : Type)) → X) t) : X × X)}
    (snd, snd_1)
pos :
  ∀ (ht : (↑t : ℝ) ≤ 2⁻¹),
    Membership.mem (α := X × X) U
      ((((Function.uncurry trans (fst, snd), Function.uncurry trans (fst_1, snd_1)).1 : (a : (↑I : Type)) → X) t,
          ((Function.uncurry trans (fst, snd), Function.uncurry trans (fst_1, snd_1)).2 : (a : (↑I : Type)) → X) t) :
        X × X)
⊢ Membership.mem (α := X × X) U
    ((((Function.uncurry trans (fst, snd), Function.uncurry trans (fst_1, snd_1)).1 : (a : (↑I : Type)) → X) t,
        ((Function.uncurry trans (fst, snd), Function.uncurry trans (fst_1, snd_1)).2 : (a : (↑I : Type)) → X) t) :
      X × X)
have neg : ∀ (ht : ¬(↑t : ℝ) ≤ 2⁻¹),
  Membership.mem (α := X × X) U
    ((((Function.uncurry trans (fst, snd), Function.uncurry trans (fst_1, snd_1)).1 : (a : (↑I : Type)) → X) t,
        ((Function.uncurry trans (fst, snd), Function.uncurry trans (fst_1, snd_1)).2 : (a : (↑I : Type)) → X) t) :
      X × X)
Tactic: by_cases ht : (t : ℝ) ≤ 2⁻¹
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
⊢ uniformSpace α = ⨅ (i : ι), UniformSpace.comap (eval (β := α) i) (U i)
have h : Eq (α := Filter (((i : ι) → α i) × ((i : ι) → α i))) (𝓤 ((i : ι) → α i)) (𝓤 ((i : ι) → α i))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (goal)
Goal:
ι : Type u_1
ι' : Type u_2
β : Type u_3
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst : UniformSpace β
inst_1 : Countable ι
inst_2 : ∀ (i : ι), IsCountablyGenerated.{u} (α := α i × α i) (𝓤 (α i))
⊢ IsCountablyGenerated (α := ((i : ι) → α i) × ((i : ι) → α i)) (𝓤 ((i : ι) → α i))
have rw : IsCountablyGenerated (α := ((i : ι) → α i) × ((i : ι) → α i))
  (⨅ (i : ι), Filter.comap (β := α i × α i) (fun (a : ((i : ι) → α i) × ((i : ι) → α i)) ↦ (a.1 i, a.2 i)) (𝓤 (α i)))
Tactic: rw [Pi.uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst : Nonempty ι
l : Filter ((i : ι) → α i)
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy (map (eval (β := α) i) l)
have simp_rw : Cauchy l ↔ ∀ (i : ι), Cauchy (map (eval (β := α) i) l)
Tactic: simp_rw +instances [Pi.uniformSpace_eq, cauchy_iInf_uniformSpace, cauchy_comap_uniformSpace]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst : Nonempty ι
l : Filter ((i : ι) → α i)
simp_rw : Cauchy l ↔ ∀ (i : ι), Cauchy (map (eval (β := α) i) l)
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy (map (eval (β := α) i) l)
have simp_rw₁ : (∀ (i : ι), Cauchy l) ↔ ∀ (i : ι), Cauchy (map (eval (β := α) i) l)
Tactic: simp_rw +instances [Pi.uniformSpace_eq, cauchy_iInf_uniformSpace, cauchy_comap_uniformSpace]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
l : Filter ((i : ι) → α i)
inst : l.NeBot
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy (map (eval (β := α) i) l)
have simp_rw : Cauchy l ↔ ∀ (i : ι), Cauchy (map (eval (β := α) i) l)
Tactic: simp_rw +instances [Pi.uniformSpace_eq, cauchy_iInf_uniformSpace', cauchy_comap_uniformSpace]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
l : Filter ((i : ι) → α i)
inst : l.NeBot
simp_rw : Cauchy l ↔ ∀ (i : ι), Cauchy (map (eval (β := α) i) l)
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy (map (eval (β := α) i) l)
have simp_rw₁ : (∀ (i : ι), Cauchy l) ↔ ∀ (i : ι), Cauchy (map (eval (β := α) i) l)
Tactic: simp_rw +instances [Pi.uniformSpace_eq, cauchy_iInf_uniformSpace', cauchy_comap_uniformSpace]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst : Nonempty ι
l : (i : ι) → Filter (α i)
hl : ∀ (i : ι), Cauchy (l i)
⊢ Cauchy (Filter.pi (α := α) l)
have this : ∀ (i : ι), (l i).NeBot
Tactic: have := fun i ↦ (hl i).1
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
β : Type u_3
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst : UniformSpace β
inst_1 : ∀ (i : ι), CompleteSpace.{u} (α i)
f : Filter ((i : ι) → α i)
hf : Cauchy f
⊢ ∃ (x : (i : ι) → α i), f ≤ 𝓝 x
have this : f.NeBot
Tactic: have := hf.1
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
β : Type u_3
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst : UniformSpace β
inst_1 : ∀ (i : ι), CompleteSpace.{u} (α i)
f : Filter ((i : ι) → α i)
hf : Cauchy f
this : f.NeBot
⊢ ∃ (x : (i : ι) → α i), f ≤ 𝓝 x
have hf₁ : ∀ (i : ι), ∃ (x : α i), map (eval (β := α) i) f ≤ 𝓝 x
Tactic: simp_rw [cauchy_pi_iff', cauchy_iff_exists_le_nhds] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (goal)
Goal:
ι : Type u_1
ι' : Type u_2
β : Type u_3
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst : UniformSpace β
inst_1 : ∀ (i : ι), CompleteSpace.{u} (α i)
f : Filter ((i : ι) → α i)
this : f.NeBot
hf : ∀ (i : ι), ∃ (x : α i), map (eval (β := α) i) f ≤ 𝓝 x
⊢ ∃ (x : (i : ι) → α i), f ≤ 𝓝 x
have choose : ∀ (x : (i : ι) → α i) (hx : ∀ (i : ι), map (eval (β := α) i) f ≤ 𝓝 (x i)), ∃ (x : (i : ι) → α i), f ≤ 𝓝 x
Tactic: choose x hx using hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (goal)
Goal:
ι : Type u_1
ι' : Type u_2
β : Type u_3
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst : UniformSpace β
inst_1 : ∀ (i : ι), CompleteSpace.{u} (α i)
f : Filter ((i : ι) → α i)
this : f.NeBot
x : (i : ι) → α i
hx : ∀ (i : ι), map (eval (β := α) i) f ≤ 𝓝 (x i)
⊢ ∃ (x : (i : ι) → α i), f ≤ 𝓝 x
have h : f ≤ 𝓝 x
Tactic: use x
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (goal)
Goal:
ι : Type u_1
ι' : Type u_2
β : Type u_3
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst : UniformSpace β
inst_1 : ∀ (i : ι), CompleteSpace.{u} (α i)
f : Filter ((i : ι) → α i)
this : f.NeBot
x : (i : ι) → α i
hx : ∀ (i : ι), map (eval (β := α) i) f ≤ 𝓝 (x i)
⊢ f ≤ 𝓝 x
have h : f ≤ Filter.pi (α := α) fun (i : ι) ↦ 𝓝 (x i)
Tactic: rwa [nhds_pi, le_pi]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (goal)
Goal:
ι : Type u_1
ι' : Type u_2
β : Type u_3
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst : UniformSpace β
inst_1 : ∀ (i : ι), CompleteSpace.{u} (α i)
f : Filter ((i : ι) → α i)
this : f.NeBot
x : (i : ι) → α i
hx : ∀ (i : ι), map (eval (β := α) i) f ≤ 𝓝 (x i)
h : f ≤ Filter.pi (α := α) fun (i : ι) ↦ 𝓝 (x i)
⊢ f ≤ 𝓝 x
have h₁ : ∀ (i : ι), Tendsto (eval (β := α) i) f (𝓝 (x i))
Tactic: rwa [nhds_pi, le_pi]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
𝔖 : Set (Set ι)
⊢ Eq (α := UniformSpace ((a : ι) → α a))
    (UniformSpace.comap ((⋃₀ 𝔖).restrict (π := α)) (uniformSpace fun (i : (↑(⋃₀ 𝔖) : Type u_1)) ↦ α (↑i : ι)))
    (⨅ S ∈ 𝔖, UniformSpace.comap (S.restrict (π := α)) (uniformSpace fun (i : (↑S : Type u_1)) ↦ α (↑i : ι)))
have simp_rw : Eq (α := UniformSpace ((a : ι) → α a)) (⨅ i ∈ ⋃₀ 𝔖, UniformSpace.comap (eval (β := α) i) (U i))
  (⨅ S ∈ 𝔖, ⨅ i ∈ S, UniformSpace.comap (eval (β := α) i) (U i))
Tactic: simp_rw [Pi.uniformSpace_comap_restrict α, iInf_sUnion]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (hypothesis)
Goal:
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
ht : ∃ (t : TopologicalSpace X), T2Space X ∧ ∀ (i : ι), toTopologicalSpace ≤ t
⊢ CompleteSpace X
have a : Nontrivial X
Tactic: nontriviality X
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Pi (goal)
Goal:
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
ht : ∃ (t : TopologicalSpace X), T2Space X ∧ ∀ (i : ι), toTopologicalSpace ≤ t
h : Nontrivial X
⊢ CompleteSpace X
have rcases : ∀ (t : TopologicalSpace X) (ht : T2Space X) (hut : ∀ (i : ι), toTopologicalSpace ≤ t), CompleteSpace X
Tactic: rcases ht with ⟨t, ht, hut⟩
Cleared hypotheses: ht