awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (hypothesis)
Goal:
α : Type ua
inst : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : SetRel α α
ht : IsOpen[instTopologicalSpaceProd] t
hst : s ⊆ t
ht_comp : t ⊆ {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}
this : s ⊆ interior d
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d
have this₁ : interior d ∈ 𝓤 α
Tactic: have : interior d ∈ 𝓤 α := by filter_upwards [hs] using this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ interior s ∈ 𝓤 α
have rw : interior s ∈ (𝓤 α).lift' interior
Tactic: rw [uniformity_eq_uniformity_interior]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
⊢ IsOpen[inst.toTopologicalSpace] s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s
have rw : (∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s) ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s
Tactic: rw [isOpen_iff_ball_subset]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
⊢ (∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s) ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s
have mp : (∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s) → ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
mp : (∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s) → ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s
⊢ (∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s) ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s
have mpr : (∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s) → ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
h : ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
x : α
hx : x ∈ s
⊢ ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s
have mp : ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hV' : ball x V ⊆ s), ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s
Tactic: obtain ⟨V, hV, hV'⟩ := h x hx
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
h : ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s
x : α
hx : x ∈ s
⊢ ∃ V ∈ 𝓤 α, ball x V ⊆ s
have mpr : ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hV' : ball x V ⊆ s), ∃ V ∈ 𝓤 α, ball x V ⊆ s
Tactic: obtain ⟨V, hV, -, hV'⟩ := h x hx
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
U : SetRel α α
hs : Dense s
hU : U ∈ 𝓤 α
⊢ Eq.{ua + 1} (α := Set α) (⋃ x ∈ s, ball x U) univ
have refine : ∀ (y : α), ∃ (i : α) (_ : i ∈ s), y ∈ ball i U
Tactic: refine iUnion₂_eq_univ_iff.2 fun y => ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
U : SetRel α α
hs : Dense s
hU : U ∈ 𝓤 α
y : α
⊢ ∃ (i : α) (_ : i ∈ s), y ∈ ball i U
have rcases : ∀ (x : α) (hxs : x ∈ s) (hxy : (x, y) ∈ U), ∃ (i : α) (_ : i ∈ s), y ∈ ball i U
Tactic: rcases hs.inter_nhds_nonempty (mem_nhds_right y hU) with ⟨x, hxs, hxy : (x, y) ∈ U⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
ι : Type u_2
xs : ι → α
xs_dense : DenseRange xs
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ Eq.{ua + 1} (α := Set α) (⋃ (i : ι), ball (xs i) U) univ
have rw : Eq.{ua + 1} (α := Set α) (⋃ x ∈ range xs, ball x U) univ
Tactic: rw [← biUnion_range (f := xs) (g := fun x ↦ UniformSpace.ball x U)]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
⊢ (𝓤 α).HasBasis (fun (V : SetRel α α) ↦ V ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] V ∧ V.IsSymm) id
have simp : (𝓤 α).HasBasis (fun (V : SetRel α α) ↦ (V ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] V) ∧ V.IsSymm) id
Tactic: simp only [← and_assoc]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
⊢ (𝓤 α).HasBasis (fun (V : SetRel α α) ↦ (V ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] V) ∧ V.IsSymm) id
have refine : ∀ (s : SetRel α α) (hs : s ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] s),
  (s.symmetrize ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] s.symmetrize) ∧ s.symmetrize.IsSymm ∧ id s.symmetrize ⊆ id s
Tactic: refine uniformity_hasBasis_open.restrict fun s hs => ⟨SetRel.symmetrize s, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ ∃ t ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] t ∧ SetRel.IsSymm t ∧ t ○ t ⊆ s
have obtain : ∀ (t : Set (α × α)) (ht₁ : t ∈ 𝓤 α) (ht₂ : t ○ t ⊆ s),
  ∃ t ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] t ∧ SetRel.IsSymm t ∧ t ○ t ⊆ s
Tactic: obtain ⟨t, ht₁, ht₂⟩ := comp_mem_uniformity_sets hs
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
t : Set (α × α)
ht₁ : t ∈ 𝓤 α
ht₂ : t ○ t ⊆ s
⊢ ∃ t ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] t ∧ SetRel.IsSymm t ∧ t ○ t ⊆ s
have obtain : ∀ (u : SetRel α α) (hu₄ : u ⊆ t) (hu₁ : u ∈ 𝓤 α) (hu₂ : IsOpen[instTopologicalSpaceProd] u) (hu₃ : u.IsSymm),
  ∃ t ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] t ∧ SetRel.IsSymm t ∧ t ○ t ⊆ s
Tactic: obtain ⟨u, ⟨hu₁, hu₂, hu₃⟩, hu₄ : u ⊆ t⟩ := uniformity_hasBasis_open_symmetric.mem_iff.mp ht₁
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (hypothesis)
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
s : α
x : TopologicalSpace α := ⊥
⊢ 𝓝 s = comap (Prod.mk s) (𝓟 SetRel.id)
have this : DiscreteTopology α
Tactic: have := discreteTopology_bot α
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u₁ u₂ : UniformSpace α
x : α
⊢ 𝓝 x = comap (Prod.mk x) (𝓤 α ⊓ 𝓤 α)
have rw : 𝓝 x ⊓ 𝓝 x = comap (Prod.mk x) (𝓤 α ⊓ 𝓤 α)
Tactic: rw [@nhds_inf _ u₁.toTopologicalSpace _, @nhds_eq_comap_uniformity _ u₁,
          @nhds_eq_comap_uniformity _ u₂, comap_inf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u₁ u₂ : UniformSpace α
x : α
rw : 𝓝 x ⊓ 𝓝 x = comap (Prod.mk x) (𝓤 α ⊓ 𝓤 α)
⊢ 𝓝 x = comap (Prod.mk x) (𝓤 α ⊓ 𝓤 α)
have rw₁ : comap (Prod.mk x) (𝓤 α) ⊓ 𝓝 x = comap (Prod.mk x) (𝓤 α ⊓ 𝓤 α)
Tactic: rw [@nhds_inf _ u₁.toTopologicalSpace _, @nhds_eq_comap_uniformity _ u₁,
          @nhds_eq_comap_uniformity _ u₂, comap_inf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u₁ u₂ : UniformSpace α
x : α
rw : 𝓝 x ⊓ 𝓝 x = comap (Prod.mk x) (𝓤 α ⊓ 𝓤 α)
rw₁ : comap (Prod.mk x) (𝓤 α) ⊓ 𝓝 x = comap (Prod.mk x) (𝓤 α ⊓ 𝓤 α)
⊢ 𝓝 x = comap (Prod.mk x) (𝓤 α ⊓ 𝓤 α)
have rw₂ : comap (Prod.mk x) (𝓤 α) ⊓ comap (Prod.mk x) (𝓤 α) = comap (Prod.mk x) (𝓤 α ⊓ 𝓤 α)
Tactic: rw [@nhds_inf _ u₁.toTopologicalSpace _, @nhds_eq_comap_uniformity _ u₁,
          @nhds_eq_comap_uniformity _ u₂, comap_inf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u₁ u₂ : UniformSpace α
x : α
rw : 𝓝 x ⊓ 𝓝 x = comap (Prod.mk x) (𝓤 α ⊓ 𝓤 α)
rw₁ : comap (Prod.mk x) (𝓤 α) ⊓ 𝓝 x = comap (Prod.mk x) (𝓤 α ⊓ 𝓤 α)
rw₂ : comap (Prod.mk x) (𝓤 α) ⊓ comap (Prod.mk x) (𝓤 α) = comap (Prod.mk x) (𝓤 α ⊓ 𝓤 α)
⊢ 𝓝 x = comap (Prod.mk x) (𝓤 α ⊓ 𝓤 α)
have rw₃ : comap (Prod.mk x) (𝓤 α) ⊓ comap (Prod.mk x) (𝓤 α) = comap (Prod.mk x) (𝓤 α) ⊓ comap (Prod.mk x) (𝓤 α)
Tactic: rw [@nhds_inf _ u₁.toTopologicalSpace _, @nhds_eq_comap_uniformity _ u₁,
          @nhds_eq_comap_uniformity _ u₂, comap_inf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst : Subsingleton α
u : UniformSpace α
⊢ Membership.mem (γ := Filter (α × α)) ((fun (u : UniformSpace α) ↦ 𝓤 α) u) SetRel.id
have rw : Membership.mem (γ := Filter (α × α)) ((fun (u : UniformSpace α) ↦ 𝓤 α) u) univ
Tactic: rw [SetRel.id, ← diagonal, diagonal_eq_univ]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
⊢ Tendsto.{ua, ua} (α := α × α) Prod.swap (Filter.comap (fun (p : α × α) ↦ (f p.1, f p.2)) (𝓤 β))
    (Filter.comap (fun (p : α × α) ↦ (f p.1, f p.2)) (𝓤 β))
have simp : Tendsto.{ua, ub} (α := α × α) ((fun (p : α × α) ↦ (f p.1, f p.2)) ∘ Prod.swap)
  (Filter.comap (fun (p : α × α) ↦ (f p.1, f p.2)) (𝓤 β)) (𝓤 β)
Tactic: simp only [tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
⊢ LE.le.{ua} (α := Filter (α × α))
    (Filter.lift' (α := α × α) (Filter.comap (fun (p : α × α) ↦ (f p.1, f p.2)) (𝓤 β)) fun (s : Set (α × α)) ↦ s ○ s)
    (Filter.comap.{ua, ub} (β := β × β) (fun (p : α × α) ↦ (f p.1, f p.2))
      (Filter.lift' (α := β × β) UniformSpace.uniformity fun (s : Set (β × β)) ↦ s ○ s))
have rw : LE.le.{ua} (α := Filter (α × α))
  ((𝓤 β).lift' ((fun (s : Set (α × α)) ↦ s ○ s) ∘ preimage fun (p : α × α) ↦ (f p.1, f p.2)))
  (Filter.lift'.{ub, ua} (α := β × β) UniformSpace.uniformity
    (Function.comp (β := Set (β × β)) (preimage fun (p : α × α) ↦ (f p.1, f p.2)) fun (s : Set (β × β)) ↦ s ○ s))
Tactic: rw [comap_lift'_eq, comap_lift'_eq2]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
rw :
  LE.le.{ua} (α := Filter (α × α))
    ((𝓤 β).lift' ((fun (s : Set (α × α)) ↦ s ○ s) ∘ preimage fun (p : α × α) ↦ (f p.1, f p.2)))
    (Filter.lift'.{ub, ua} (α := β × β) UniformSpace.uniformity
      (Function.comp (β := Set (β × β)) (preimage fun (p : α × α) ↦ (f p.1, f p.2)) fun (s : Set (β × β)) ↦ s ○ s))
⊢ LE.le.{ua} (α := Filter (α × α))
    (Filter.lift' (α := α × α) (Filter.comap (fun (p : α × α) ↦ (f p.1, f p.2)) (𝓤 β)) fun (s : Set (α × α)) ↦ s ○ s)
    (Filter.comap.{ua, ub} (β := β × β) (fun (p : α × α) ↦ (f p.1, f p.2))
      (Filter.lift' (α := β × β) UniformSpace.uniformity fun (s : Set (β × β)) ↦ s ○ s))
have rw₁ : Monotone (β := Set (α × α)) fun (s : Set (α × α)) ↦ s ○ s
Tactic: rw [comap_lift'_eq, comap_lift'_eq2]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
f : α → β
U : SetRel β β
x : α
⊢ UniformSpace.ball x (Prod.map f f ⁻¹' U) = f ⁻¹' UniformSpace.ball (f x) U
have h : ∀ (x_1 : α), x_1 ∈ UniformSpace.ball x (Prod.map f f ⁻¹' U) ↔ x_1 ∈ f ⁻¹' UniformSpace.ball (f x) U
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type u_2
⊢ Eq.{u_2 + 1} (α := (u : UniformSpace α) → UniformSpace α) (UniformSpace.comap id) id
have h : ∀ (x : UniformSpace α), 𝓤 α = 𝓤 α
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type u_2
x : UniformSpace α
⊢ 𝓤 α = 𝓤 α
have h : comap (Prod.map id id) (𝓤 α) = 𝓤 α
Tactic: rw [uniformity_comap, Prod.map_id, comap_id]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type u_2
x : UniformSpace α
h : comap (Prod.map id id) (𝓤 α) = 𝓤 α
⊢ 𝓤 α = 𝓤 α
have h₁ : comap id (𝓤 α) = 𝓤 α
Tactic: rw [uniformity_comap, Prod.map_id, comap_id]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type u_2
x : UniformSpace α
h : comap (Prod.map id id) (𝓤 α) = 𝓤 α
h₁ : comap id (𝓤 α) = 𝓤 α
⊢ 𝓤 α = 𝓤 α
have h₂ : 𝓤 α = 𝓤 α
Tactic: rw [uniformity_comap, Prod.map_id, comap_id]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
uγ : UniformSpace γ
f : α → β
g : β → γ
⊢ comap (g ∘ f) uγ = comap f (comap g uγ)
have h : 𝓤 α = 𝓤 α
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
ι : Sort u_2
α : Type u_3
γ : Type u_4
u : ι → UniformSpace γ
f : α → γ
⊢ comap f (⨅ (i : ι), u i) = ⨅ (i : ι), comap f (u i)
have h : 𝓤 α = 𝓤 α
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
u v : UniformSpace α
⊢ u ≤ v ↔ UniformContinuous.{ua, ua} (α := α) id
have rw : u ≤ v ↔ u ≤ UniformSpace.comap id v
Tactic: rw [uniformContinuous_iff, uniformSpace_comap_id, id]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
u v : UniformSpace α
rw : u ≤ v ↔ u ≤ UniformSpace.comap id v
⊢ u ≤ v ↔ UniformContinuous.{ua, ua} (α := α) id
have rw₁ : u ≤ v ↔ u ≤ id v
Tactic: rw [uniformContinuous_iff, uniformSpace_comap_id, id]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
u v : UniformSpace α
rw : u ≤ v ↔ u ≤ UniformSpace.comap id v
rw₁ : u ≤ v ↔ u ≤ id v
⊢ u ≤ v ↔ UniformContinuous.{ua, ua} (α := α) id
have rw₂ : u ≤ v ↔ u ≤ v
Tactic: rw [uniformContinuous_iff, uniformSpace_comap_id, id]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
u₁ u₂ : UniformSpace α
h : u₁ ≤ u₂
a : α
⊢ 𝓝 a ≤ 𝓝 a
have rw : (𝓤 α).lift' (ball a) ≤ (𝓤 α).lift' (ball a)
Tactic: rw [@nhds_eq_uniformity α u₁ a, @nhds_eq_uniformity α u₂ a]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
s : Set (UniformSpace α)
⊢ Eq.{ua + 1} (α := TopologicalSpace α) toTopologicalSpace (⨅ i ∈ s, toTopologicalSpace)
have rw : Eq.{ua + 1} (α := TopologicalSpace α) toTopologicalSpace (⨅ i ∈ s, toTopologicalSpace)
Tactic: rw [sInf_eq_iInf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f g : α → β
s : Set α
hf : UniformContinuousOn f s
h : EqOn f g s
⊢ UniformContinuousOn g s
have apply : EventuallyEq.{ua, ub} (β := β × β) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (fun (x : α × α) ↦ (f x.1, f x.2)) fun (x : α × α) ↦
  (g x.1, g x.2)
Tactic: apply hf.congr'
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f g : α → β
s : Set α
hf : UniformContinuousOn f s
h : EqOn f g s
⊢ EventuallyEq.{ua, ub} (β := β × β) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (fun (x : α × α) ↦ (f x.1, f x.2)) fun (x : α × α) ↦
    (g x.1, g x.2)
have apply : EventuallyEq.{ua, ub} (β := β × β) (𝓟 (s ×ˢ s)) (fun (x : α × α) ↦ (f x.1, f x.2)) fun (x : α × α) ↦ (g x.1, g x.2)
Tactic: apply EventuallyEq.filter_mono _ inf_le_right
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f g : α → β
s : Set α
hf : UniformContinuousOn f s
h : EqOn f g s
a b : α
⊢ (a, b) ∈ s ×ˢ s → (f (a, b).1, f (a, b).2) = (g (a, b).1, g (a, b).2)
have h₁ : ∀ (ha : (a, b).1 ∈ s) (hb : (a, b).2 ∈ s), (f (a, b).1, f (a, b).2) = (g (a, b).1, g (a, b).2)
Tactic: ⟨ha, hb⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f g : α → β
s : Set α
hf : UniformContinuousOn f s
h : EqOn f g s
⊢ EventuallyEq.{ua, ub} (β := β × β) (𝓟 (s ×ˢ s)) (fun (x : α × α) ↦ (f x.1, f x.2)) fun (x : α × α) ↦ (g x.1, g x.2)
have h₁ : ∀ (a : α × α),
  Membership.mem (γ := Set (α × α))
    {x : α × α |
      x ∈ s ×ˢ s →
        Membership.mem (γ := Set (α × α))
          {x : α × α |
            (fun (x : α × α) ↦
                Eq.{ub + 1} (α := β × β) ((fun (x : α × α) ↦ (f x.1, f x.2)) x) ((fun (x : α × α) ↦ (g x.1, g x.2)) x))
              x}
          x}
    a
Tactic: filter_upwards [mem_principal_self _] with ⟨a, b⟩ ⟨ha, hb⟩ using by simp [h ha, h hb]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f g : α → β
s : Set α
hf : UniformContinuousOn f s
h : EqOn f g s
h₁ :
  ∀ (a : α × α),
    Membership.mem (γ := Set (α × α))
      {x : α × α |
        x ∈ s ×ˢ s →
          Membership.mem (γ := Set (α × α))
            {x : α × α |
              (fun (x : α × α) ↦
                  Eq.{ub + 1} (α := β × β) ((fun (x : α × α) ↦ (f x.1, f x.2)) x)
                    ((fun (x : α × α) ↦ (g x.1, g x.2)) x))
                x}
            x}
      a
⊢ EventuallyEq.{ua, ub} (β := β × β) (𝓟 (s ×ˢ s)) (fun (x : α × α) ↦ (f x.1, f x.2)) fun (x : α × α) ↦ (g x.1, g x.2)
have h₂ : ∀ a ∈ s ×ˢ s, (f a.1, f a.2) = (g a.1, g a.2)
Tactic: filter_upwards [mem_principal_self _] with ⟨a, b⟩ ⟨ha, hb⟩ using by simp [h ha, h hb]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f g : α → β
s : Set α
hf : UniformContinuousOn f s
h : EqOn f g s
h₁ :
  ∀ (a : α × α),
    Membership.mem (γ := Set (α × α))
      {x : α × α |
        x ∈ s ×ˢ s →
          Membership.mem (γ := Set (α × α))
            {x : α × α |
              (fun (x : α × α) ↦
                  Eq.{ub + 1} (α := β × β) ((fun (x : α × α) ↦ (f x.1, f x.2)) x)
                    ((fun (x : α × α) ↦ (g x.1, g x.2)) x))
                x}
            x}
      a
h₂ : ∀ a ∈ s ×ˢ s, (f a.1, f a.2) = (g a.1, g a.2)
⊢ EventuallyEq.{ua, ub} (β := β × β) (𝓟 (s ×ˢ s)) (fun (x : α × α) ↦ (f x.1, f x.2)) fun (x : α × α) ↦ (g x.1, g x.2)
have h₃ : ∀ (a b : α) (ha : (a, b).1 ∈ s) (hb : (a, b).2 ∈ s), (f (a, b).1, f (a, b).2) = (g (a, b).1, g (a, b).2)
Tactic: filter_upwards [mem_principal_self _] with ⟨a, b⟩ ⟨ha, hb⟩ using by simp [h ha, h hb]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → β
s : Set α
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : UniformContinuousOn f s
hst : MapsTo f s t
⊢ UniformContinuousOn (g ∘ f) s
have change : Tendsto ((fun (x : β × β) ↦ (g x.1, g x.2)) ∘ fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 γ)
Tactic: change Tendsto ((fun x ↦ (g x.1, g x.2)) ∘ (fun x ↦ (f x.1, f x.2))) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 γ)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → β
s : Set α
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : UniformContinuousOn f s
hst : MapsTo f s t
⊢ Tendsto ((fun (x : β × β) ↦ (g x.1, g x.2)) ∘ fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 γ)
have apply : Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 β ⊓ 𝓟 (t ×ˢ t))
Tactic: apply Tendsto.comp hg
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → β
s : Set α
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : UniformContinuousOn f s
hst : MapsTo f s t
⊢ Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 β ⊓ 𝓟 (t ×ˢ t))
have refine : Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓟 (s ×ˢ s)) (𝓟 (t ×ˢ t))
Tactic: refine tendsto_inf.2 ⟨hf, tendsto_inf_right ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → β
s : Set α
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : UniformContinuousOn f s
hst : MapsTo f s t
⊢ Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓟 (s ×ˢ s)) (𝓟 (t ×ˢ t))
have simp : ∀ (a b : α), a ∈ s → b ∈ s → f a ∈ t ∧ f b ∈ t
Tactic: simp only [tendsto_principal, mem_prod, eventually_principal, and_imp, Prod.forall]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
f : α → β
u₁ : Set (UniformSpace α)
u₂ : UniformSpace β
u : UniformSpace α
h₁ : u ∈ u₁
hf : UniformContinuous f
⊢ Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
have rw : Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (⨅ (i : (↑u₁ : Type ua)), 𝓤 α) (𝓤 β)
Tactic: rw [sInf_eq_iInf', iInf_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
f : α → β
u₁ : UniformSpace α
u₂ : Set (UniformSpace β)
⊢ Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β) ↔
    ∀ u ∈ u₂, Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
have rw : Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β) ↔
  ∀ u ∈ u₂, Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
Tactic: rw [sInf_eq_iInf', iInf_uniformity, tendsto_iInf, SetCoe.forall]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
f : α → β
u₁ : UniformSpace α
u₂ : Set (UniformSpace β)
rw :
  Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β) ↔
    ∀ u ∈ u₂, Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
⊢ Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β) ↔
    ∀ u ∈ u₂, Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
have rw₁ : Tendsto.{ua, ub} (β := β × β) (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (⨅ (i : (↑u₂ : Type ub)), 𝓤 β) ↔
  ∀ u ∈ u₂, Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
Tactic: rw [sInf_eq_iInf', iInf_uniformity, tendsto_iInf, SetCoe.forall]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
f : α → β
u₁ : UniformSpace α
u₂ : Set (UniformSpace β)
rw :
  Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β) ↔
    ∀ u ∈ u₂, Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
rw₁ :
  Tendsto.{ua, ub} (β := β × β) (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (⨅ (i : (↑u₂ : Type ub)), 𝓤 β) ↔
    ∀ u ∈ u₂, Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
⊢ Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β) ↔
    ∀ u ∈ u₂, Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
have rw₂ : (∀ (i : (↑u₂ : Type ub)), Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)) ↔
  ∀ u ∈ u₂, Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
Tactic: rw [sInf_eq_iInf', iInf_uniformity, tendsto_iInf, SetCoe.forall]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
f : α → β
u₁ : UniformSpace α
u₂ : Set (UniformSpace β)
rw :
  Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β) ↔
    ∀ u ∈ u₂, Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
rw₁ :
  Tendsto.{ua, ub} (β := β × β) (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (⨅ (i : (↑u₂ : Type ub)), 𝓤 β) ↔
    ∀ u ∈ u₂, Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
rw₂ :
  (∀ (i : (↑u₂ : Type ub)), Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)) ↔
    ∀ u ∈ u₂, Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
⊢ Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β) ↔
    ∀ u ∈ u₂, Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
have rw₃ : (∀ (x : UniformSpace β) (h : x ∈ u₂), Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)) ↔
  ∀ u ∈ u₂, Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
Tactic: rw [sInf_eq_iInf', iInf_uniformity, tendsto_iInf, SetCoe.forall]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
ι : Sort u_1
f : α → β
u₁ : ι → UniformSpace α
u₂ : UniformSpace β
i : ι
hf : UniformContinuous f
⊢ Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
have rw : Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (⨅ (i : ι), 𝓤 α) (𝓤 β)
Tactic: rw [iInf_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
ι : Sort u_1
f : α → β
u₁ : UniformSpace α
u₂ : ι → UniformSpace β
⊢ Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β) ↔
    ∀ (i : ι), Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
have rw : Tendsto.{ua, ub} (β := β × β) (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (⨅ (i : ι), 𝓤 β) ↔
  ∀ (i : ι), Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
Tactic: rw [iInf_uniformity, tendsto_iInf]