awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α_1 : Type ua
β_1 : Type ub
γ_1 : Type uc
δ : Type ud
ι : Sort u_1
inst : UniformSpace α_1
inst_1 : UniformSpace β_1
inst_2 : UniformSpace γ_1
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha : ua ∈ uas
hb : ub ∈ ubs
hf : UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
⊢ Prop
have haveI : (this : UniformSpace α) → Prop
Tactic: haveI := sInf uas
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α_1 : Type ua
β_1 : Type ub
γ_1 : Type uc
δ : Type ud
ι : Sort u_1
inst : UniformSpace α_1
inst_1 : UniformSpace β_1
inst_2 : UniformSpace γ_1
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha : ua ∈ uas
hb : ub ∈ ubs
hf : UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
this : UniformSpace α
⊢ Prop
have haveI : (this : UniformSpace β) → Prop
Tactic: haveI := sInf ubs
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (hypothesis)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha : ua ∈ uas
hb : ub ∈ ubs
hf : UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
x : UniformSpace (α × β) := instUniformSpaceProd
⊢ UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
have ha₁ : UniformContinuous.{u_2, u_2} (α := α) id
Tactic: have ha := uniformContinuous_sInf_dom ha uniformContinuous_id
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (hypothesis)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha_1 : ua ∈ uas
hb : ub ∈ ubs
hf : UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
x : UniformSpace (α × β) := instUniformSpaceProd
ha : UniformContinuous.{u_2, u_2} (α := α) id
⊢ UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
have hb₁ : UniformContinuous.{u_3, u_3} (α := β) id
Tactic: have hb := uniformContinuous_sInf_dom hb uniformContinuous_id
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (hypothesis)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha_1 : ua ∈ uas
hb_1 : ub ∈ ubs
hf : UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
x : UniformSpace (α × β) := instUniformSpaceProd
ha : UniformContinuous.{u_2, u_2} (α := α) id
hb : UniformContinuous.{u_3, u_3} (α := β) id
⊢ UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
have h_unif_cont_id : UniformContinuous (α := α × β) (Prod.map id id)
Tactic: have h_unif_cont_id := @UniformContinuous.prodMap _ _ _ _ (sInf uas) (sInf ubs) ua ub _ _ ha 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 : α × β → γ
⊢ UniformContinuous₂ (Function.curry f) ↔ UniformContinuous f
have rw : UniformContinuous (uncurry (Function.curry f)) ↔ UniformContinuous f
Tactic: rw [UniformContinuous₂, uncurry_curry]
-- 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 : α × β → γ
rw : UniformContinuous (uncurry (Function.curry f)) ↔ UniformContinuous f
⊢ UniformContinuous₂ (Function.curry f) ↔ UniformContinuous f
have rw₁ : UniformContinuous f ↔ UniformContinuous f
Tactic: rw [UniformContinuous₂, uncurry_curry]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set ((α ⊕ β) × (α ⊕ β))
hs :
  Membership.mem (γ := Filter ((α ⊕ β) × (α ⊕ β)))
    (map (fun (p : α × α) ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun (p : β × β) ↦ (inr p.1, inr p.2)) (𝓤 β)) s
⊢ Membership.mem (γ := Filter ((α ⊕ β) × (α ⊕ β)))
    (Filter.lift' (α := (α ⊕ β) × (α ⊕ β))
      (map (fun (p : α × α) ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun (p : β × β) ↦ (inr p.1, inr p.2)) (𝓤 β))
      fun (s : Set ((α ⊕ β) × (α ⊕ β))) ↦ s ○ s)
    s
have rcases : ∀ (tα : Set (α × α)) (htα : tα ∈ 𝓤 α) (Htα : tα ○ tα ⊆ (fun (p : α × α) ↦ (inl p.1, inl p.2)) ⁻¹' s),
  Membership.mem (γ := Filter ((α ⊕ β) × (α ⊕ β)))
    (Filter.lift' (α := (α ⊕ β) × (α ⊕ β))
      (map (fun (p : α × α) ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun (p : β × β) ↦ (inr p.1, inr p.2)) (𝓤 β))
      fun (s : Set ((α ⊕ β) × (α ⊕ β))) ↦ s ○ s)
    s
Tactic: rcases comp_mem_uniformity_sets hs.1 with ⟨tα, htα, Htα⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set ((α ⊕ β) × (α ⊕ β))
hs :
  Membership.mem (γ := Filter ((α ⊕ β) × (α ⊕ β)))
    (map (fun (p : α × α) ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun (p : β × β) ↦ (inr p.1, inr p.2)) (𝓤 β)) s
tα : Set (α × α)
htα : tα ∈ 𝓤 α
Htα : tα ○ tα ⊆ (fun (p : α × α) ↦ (inl p.1, inl p.2)) ⁻¹' s
⊢ Membership.mem (γ := Filter ((α ⊕ β) × (α ⊕ β)))
    (Filter.lift' (α := (α ⊕ β) × (α ⊕ β))
      (map (fun (p : α × α) ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun (p : β × β) ↦ (inr p.1, inr p.2)) (𝓤 β))
      fun (s : Set ((α ⊕ β) × (α ⊕ β))) ↦ s ○ s)
    s
have rcases : ∀ (tβ : Set (β × β)) (htβ : tβ ∈ 𝓤 β) (Htβ : tβ ○ tβ ⊆ (fun (p : β × β) ↦ (inr p.1, inr p.2)) ⁻¹' s),
  Membership.mem (γ := Filter ((α ⊕ β) × (α ⊕ β)))
    (Filter.lift' (α := (α ⊕ β) × (α ⊕ β))
      (map (fun (p : α × α) ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun (p : β × β) ↦ (inr p.1, inr p.2)) (𝓤 β))
      fun (s : Set ((α ⊕ β) × (α ⊕ β))) ↦ s ○ s)
    s
Tactic: rcases comp_mem_uniformity_sets hs.2 with ⟨tβ, htβ, Htβ⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set ((α ⊕ β) × (α ⊕ β))
hs :
  Membership.mem (γ := Filter ((α ⊕ β) × (α ⊕ β)))
    (map (fun (p : α × α) ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun (p : β × β) ↦ (inr p.1, inr p.2)) (𝓤 β)) s
tα : Set (α × α)
htα : tα ∈ 𝓤 α
Htα : tα ○ tα ⊆ (fun (p : α × α) ↦ (inl p.1, inl p.2)) ⁻¹' s
tβ : Set (β × β)
htβ : tβ ∈ 𝓤 β
Htβ : tβ ○ tβ ⊆ (fun (p : β × β) ↦ (inr p.1, inr p.2)) ⁻¹' s
⊢ Membership.mem (γ := Filter ((α ⊕ β) × (α ⊕ β)))
    (Filter.lift' (α := (α ⊕ β) × (α ⊕ β))
      (map (fun (p : α × α) ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun (p : β × β) ↦ (inr p.1, inr p.2)) (𝓤 β))
      fun (s : Set ((α ⊕ β) × (α ⊕ β))) ↦ s ○ s)
    s
have h : ∀ (a : (α ⊕ β) × (α ⊕ β)),
  Membership.mem (γ := Set ((α ⊕ β) × (α ⊕ β)))
      (SetRel.comp (β := α ⊕ β)
        ((fun (p : α × α) ↦ (inl p.1, inl p.2)) '' tα ∪ (fun (p : β × β) ↦ (inr p.1, inr p.2)) '' tβ)
        ((fun (p : α × α) ↦ (inl p.1, inl p.2)) '' tα ∪ (fun (p : β × β) ↦ (inr p.1, inr p.2)) '' tβ))
      a →
    a ∈ s
Tactic: filter_upwards [mem_lift' (union_mem_sup (image_mem_map htα) (image_mem_map htβ))]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst : UniformSpace α
inst_1 : UniformSpace β
x : α ⊕ β
⊢ 𝓝 x =
    comap (Prod.mk x)
      (map (fun (p : α × α) ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun (p : β × β) ↦ (inr p.1, inr p.2)) (𝓤 β))
have h : ∀ (s : Set (α ⊕ β)),
  s ∈ 𝓝 x ↔
    Membership.mem (γ := Filter (α ⊕ β))
      (comap (Prod.mk x)
        (map (fun (p : α × α) ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun (p : β × β) ↦ (inr p.1, inr p.2)) (𝓤 β)))
      s
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst : UniformSpace α
inst_1 : UniformSpace β
x : α ⊕ β
s : Set (α ⊕ β)
⊢ s ∈ 𝓝 x ↔
    Membership.mem (γ := Filter (α ⊕ β))
      (comap (Prod.mk x)
        (map (fun (p : α × α) ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun (p : β × β) ↦ (inr p.1, inr p.2)) (𝓤 β)))
      s
have h : ∀ (val : α),
  Membership.mem (γ := Filter (α ⊕ β)) (𝓝 (inl val)) s ↔
    Membership.mem (γ := Filter (α ⊕ β))
      (comap (β := (α ⊕ β) × (α ⊕ β)) (Prod.mk (inl val))
        (map (fun (p : α × α) ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun (p : β × β) ↦ (inr p.1, inr p.2)) (𝓤 β)))
      s
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst : UniformSpace α
inst_1 : UniformSpace β
x : α ⊕ β
s : Set (α ⊕ β)
h :
  ∀ (val : α),
    Membership.mem (γ := Filter (α ⊕ β)) (𝓝 (inl val)) s ↔
      Membership.mem (γ := Filter (α ⊕ β))
        (comap (β := (α ⊕ β) × (α ⊕ β)) (Prod.mk (inl val))
          (map (fun (p : α × α) ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun (p : β × β) ↦ (inr p.1, inr p.2)) (𝓤 β)))
        s
⊢ s ∈ 𝓝 x ↔
    Membership.mem (γ := Filter (α ⊕ β))
      (comap (Prod.mk x)
        (map (fun (p : α × α) ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun (p : β × β) ↦ (inr p.1, inr p.2)) (𝓤 β)))
      s
have h₁ : ∀ (val : β),
  Membership.mem (γ := Filter (α ⊕ β)) (𝓝 (inr val)) s ↔
    Membership.mem (γ := Filter (α ⊕ β))
      (comap (β := (α ⊕ β) × (α ⊕ β)) (Prod.mk (inr val))
        (map (fun (p : α × α) ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun (p : β × β) ↦ (inr p.1, inr p.2)) (𝓤 β)))
      s
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto u f (𝓝 a) ↔ Tendsto (fun (x : β) ↦ (a, u x)) f (𝓤 α)
have rw : Tendsto (Prod.mk a ∘ u) f (𝓤 α) ↔ Tendsto (fun (x : β) ↦ (a, u x)) f (𝓤 α)
Tactic: rw [nhds_eq_comap_uniformity, tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto u f (𝓝 a) ↔ Tendsto (fun (x : β) ↦ (u x, a)) f (𝓤 α)
have rw : Tendsto ((fun (y : α) ↦ (y, a)) ∘ u) f (𝓤 α) ↔ Tendsto (fun (x : β) ↦ (u x, a)) f (𝓤 α)
Tactic: rw [nhds_eq_comap_uniformity', tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
f : β → α
b : β
⊢ ContinuousAt f b ↔ Tendsto (fun (x : β) ↦ (f b, f x)) (𝓝 b) (𝓤 α)
have rw : Tendsto f (𝓝 b) (𝓝 (f b)) ↔ Tendsto (fun (x : β) ↦ (f b, f x)) (𝓝 b) (𝓤 α)
Tactic: rw [ContinuousAt, tendsto_nhds_right]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
f : β → α
b : β
rw : Tendsto f (𝓝 b) (𝓝 (f b)) ↔ Tendsto (fun (x : β) ↦ (f b, f x)) (𝓝 b) (𝓤 α)
⊢ ContinuousAt f b ↔ Tendsto (fun (x : β) ↦ (f b, f x)) (𝓝 b) (𝓤 α)
have rw₁ : Tendsto (fun (x : β) ↦ (f b, f x)) (𝓝 b) (𝓤 α) ↔ Tendsto (fun (x : β) ↦ (f b, f x)) (𝓝 b) (𝓤 α)
Tactic: rw [ContinuousAt, tendsto_nhds_right]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
f : β → α
b : β
⊢ ContinuousAt f b ↔ Tendsto (fun (x : β) ↦ (f x, f b)) (𝓝 b) (𝓤 α)
have rw : Tendsto f (𝓝 b) (𝓝 (f b)) ↔ Tendsto (fun (x : β) ↦ (f x, f b)) (𝓝 b) (𝓤 α)
Tactic: rw [ContinuousAt, tendsto_nhds_left]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
f : β → α
b : β
rw : Tendsto f (𝓝 b) (𝓝 (f b)) ↔ Tendsto (fun (x : β) ↦ (f x, f b)) (𝓝 b) (𝓤 α)
⊢ ContinuousAt f b ↔ Tendsto (fun (x : β) ↦ (f x, f b)) (𝓝 b) (𝓤 α)
have rw₁ : Tendsto (fun (x : β) ↦ (f x, f b)) (𝓝 b) (𝓤 α) ↔ Tendsto (fun (x : β) ↦ (f x, f b)) (𝓝 b) (𝓤 α)
Tactic: rw [ContinuousAt, tendsto_nhds_left]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
f : β → α
b : β
s : Set β
⊢ ContinuousWithinAt f s b ↔ Tendsto (fun (x : β) ↦ (f b, f x)) (𝓝[s] b) (𝓤 α)
have rw : Tendsto f (𝓝[s] b) (𝓝 (f b)) ↔ Tendsto (fun (x : β) ↦ (f b, f x)) (𝓝[s] b) (𝓤 α)
Tactic: rw [ContinuousWithinAt, tendsto_nhds_right]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
f : β → α
b : β
s : Set β
rw : Tendsto f (𝓝[s] b) (𝓝 (f b)) ↔ Tendsto (fun (x : β) ↦ (f b, f x)) (𝓝[s] b) (𝓤 α)
⊢ ContinuousWithinAt f s b ↔ Tendsto (fun (x : β) ↦ (f b, f x)) (𝓝[s] b) (𝓤 α)
have rw₁ : Tendsto (fun (x : β) ↦ (f b, f x)) (𝓝[s] b) (𝓤 α) ↔ Tendsto (fun (x : β) ↦ (f b, f x)) (𝓝[s] b) (𝓤 α)
Tactic: rw [ContinuousWithinAt, tendsto_nhds_right]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
f : β → α
b : β
s : Set β
⊢ ContinuousWithinAt f s b ↔ Tendsto (fun (x : β) ↦ (f x, f b)) (𝓝[s] b) (𝓤 α)
have rw : Tendsto f (𝓝[s] b) (𝓝 (f b)) ↔ Tendsto (fun (x : β) ↦ (f x, f b)) (𝓝[s] b) (𝓤 α)
Tactic: rw [ContinuousWithinAt, tendsto_nhds_left]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
f : β → α
b : β
s : Set β
rw : Tendsto f (𝓝[s] b) (𝓝 (f b)) ↔ Tendsto (fun (x : β) ↦ (f x, f b)) (𝓝[s] b) (𝓤 α)
⊢ ContinuousWithinAt f s b ↔ Tendsto (fun (x : β) ↦ (f x, f b)) (𝓝[s] b) (𝓤 α)
have rw₁ : Tendsto (fun (x : β) ↦ (f x, f b)) (𝓝[s] b) (𝓤 α) ↔ Tendsto (fun (x : β) ↦ (f x, f b)) (𝓝[s] b) (𝓤 α)
Tactic: rw [ContinuousWithinAt, tendsto_nhds_left]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
⊢ ∃ (t : Set β), IsOpen[inst_1] t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r
have obtain : ∀ (t : Set (α × α)) (ht : t ∈ 𝓤 α) (htsymm : SetRel.IsSymm t) (htr : t ○ t ⊆ r),
  ∃ (t : Set β), IsOpen[inst_1] t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r
Tactic: obtain ⟨t, ht, htsymm, htr⟩ := comp_symm_mem_uniformity_sets hr
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (hypothesis)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SetRel.IsSymm t
htr : t ○ t ⊆ r
⊢ ∃ (t : Set β), IsOpen[inst_1] t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r
have A : {z : β | (f x, f z) ∈ t} ∈ 𝓝 x
Tactic: have A : {z | (f x, f z) ∈ t} ∈ 𝓝 x := (hf x hx).preimage_mem_nhds (mem_nhds_left (f x) ht)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (hypothesis)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SetRel.IsSymm t
htr : t ○ t ⊆ r
A : {z : β | (f x, f z) ∈ t} ∈ 𝓝 x
⊢ ∃ (t : Set β), IsOpen[inst_1] t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r
have B : {z : β | (g x, g z) ∈ t} ∈ 𝓝 x
Tactic: have B : {z | (g x, g z) ∈ t} ∈ 𝓝 x := (hg x hx).preimage_mem_nhds (mem_nhds_left (g x) ht)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SetRel.IsSymm t
htr : t ○ t ⊆ r
A : {z : β | (f x, f z) ∈ t} ∈ 𝓝 x
B : {z : β | (g x, g z) ∈ t} ∈ 𝓝 x
⊢ ∃ (t : Set β), IsOpen[inst_1] t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r
have rcases : ∀ (u : Set β) (hu : u ⊆ {z : β | (f x, f z) ∈ t} ∩ {z : β | (g x, g z) ∈ t}) (u_open : IsOpen[inst_1] u) (xu : x ∈ u),
  ∃ (t : Set β), IsOpen[inst_1] t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r
Tactic: rcases _root_.mem_nhds_iff.1 (inter_mem A B) with ⟨u, hu, u_open, xu⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SetRel.IsSymm t
htr : t ○ t ⊆ r
A : {z : β | (f x, f z) ∈ t} ∈ 𝓝 x
B : {z : β | (g x, g z) ∈ t} ∈ 𝓝 x
u : Set β
hu : u ⊆ {z : β | (f x, f z) ∈ t} ∩ {z : β | (g x, g z) ∈ t}
u_open : IsOpen[inst_1] u
xu : x ∈ u
⊢ ∃ (t : Set β), IsOpen[inst_1] t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r
have refine : ∀ (y : β) (hy : y ∈ u), (f y, g y) ∈ r
Tactic: refine ⟨u, u_open, xu, fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (hypothesis)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SetRel.IsSymm t
htr : t ○ t ⊆ r
A : {z : β | (f x, f z) ∈ t} ∈ 𝓝 x
B : {z : β | (g x, g z) ∈ t} ∈ 𝓝 x
u : Set β
hu : u ⊆ {z : β | (f x, f z) ∈ t} ∩ {z : β | (g x, g z) ∈ t}
u_open : IsOpen[inst_1] u
xu : x ∈ u
y : β
hy : y ∈ u
⊢ (f y, g y) ∈ r
have I1 : (f y, f x) ∈ t
Tactic: have I1 : (f y, f x) ∈ t := SetRel.symm t (hu hy).1
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (hypothesis)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SetRel.IsSymm t
htr : t ○ t ⊆ r
A : {z : β | (f x, f z) ∈ t} ∈ 𝓝 x
B : {z : β | (g x, g z) ∈ t} ∈ 𝓝 x
u : Set β
hu : u ⊆ {z : β | (f x, f z) ∈ t} ∩ {z : β | (g x, g z) ∈ t}
u_open : IsOpen[inst_1] u
xu : x ∈ u
y : β
hy : y ∈ u
I1 : (f y, f x) ∈ t
⊢ (f y, g y) ∈ r
have I2 : (g x, g y) ∈ t
Tactic: have I2 : (g x, g y) ∈ t := (hu hy).2
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (hypothesis)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SetRel.IsSymm t
htr : t ○ t ⊆ r
A : {z : β | (f x, f z) ∈ t} ∈ 𝓝 x
B : {z : β | (g x, g z) ∈ t} ∈ 𝓝 x
u : Set β
hu : u ⊆ {z : β | (f x, f z) ∈ t} ∩ {z : β | (g x, g z) ∈ t}
u_open : IsOpen[inst_1] u
xu : x ∈ u
y : β
hy : y ∈ u
I1 : (f y, f x) ∈ t
I2 : (g x, g y) ∈ t
⊢ (f y, g y) ∈ r
have I1₁ : (f y, g x) ∈ t
Tactic: rw [hfg hx] at I1
Cleared hypotheses: I1, I2
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (hypothesis)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
⊢ ∃ (t : Set β), IsOpen[inst_1] t ∧ s ⊆ t ∧ ∀ x ∈ t, (f x, g x) ∈ r
have A : ∀ x ∈ s, ∃ (t : Set β), IsOpen[inst_1] t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r
Tactic: have A : ∀ x ∈ s, ∃ t, IsOpen t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r := by
    intro x hx
    obtain ⟨t, ht, htsymm, htr⟩ := comp_symm_mem_uniformity_sets hr
    have A : {z | (f x, f z) ∈ t} ∈ 𝓝 x := (hf x hx).preimage_mem_nhds (mem_nhds_left (f x) ht)
    have B : {z | (g x, g z) ∈ t} ∈ 𝓝 x := (hg x hx).preimage_mem_nhds (mem_nhds_left (g x) ht)
    rcases _root_.mem_nhds_iff.1 (inter_mem A B) with ⟨u, hu, u_open, xu⟩
    refine ⟨u, u_open, xu, fun y hy ↦ ?_⟩
    have I1 : (f y, f x) ∈ t := SetRel.symm t (hu hy).1
    have I2 : (g x, g y) ∈ t := (hu hy).2
    rw [hfg hx] at I1
    exact htr (SetRel.prodMk_mem_comp I1 I2)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
A : ∀ x ∈ s, ∃ (t : Set β), IsOpen[inst_1] t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r
⊢ ∃ (t : Set β), IsOpen[inst_1] t ∧ s ⊆ t ∧ ∀ x ∈ t, (f x, g x) ∈ r
have choose! : ∀ (t : (x : β) → Set β) (t_open : ∀ x ∈ s, IsOpen[inst_1] (t x)) (xt : ∀ x ∈ s, x ∈ t x)
  (ht : ∀ x ∈ s, ∀ z ∈ t x, (f z, g z) ∈ r), ∃ (t : Set β), IsOpen[inst_1] t ∧ s ⊆ t ∧ ∀ x ∈ t, (f x, g x) ∈ r
Tactic: choose! t t_open xt ht using A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
t : (x : β) → Set β
t_open : ∀ x ∈ s, IsOpen[inst_1] (t x)
xt : ∀ x ∈ s, x ∈ t x
ht : ∀ x ∈ s, ∀ z ∈ t x, (f z, g z) ∈ r
⊢ ∃ (t : Set β), IsOpen[inst_1] t ∧ s ⊆ t ∧ ∀ x ∈ t, (f x, g x) ∈ r
have refine : ∀ (x : β), Membership.mem (γ := Set β) (⋃ x ∈ s, t x) x → (f x, g x) ∈ r
Tactic: refine ⟨⋃ x ∈ s, t x, isOpen_biUnion t_open, fun x hx ↦ mem_biUnion hx (xt x hx), ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (hypothesis)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
t : (x : β) → Set β
t_open : ∀ x ∈ s, IsOpen[inst_1] (t x)
xt : ∀ x ∈ s, x ∈ t x
ht : ∀ x ∈ s, ∀ z ∈ t x, (f z, g z) ∈ r
x : β
hx : Membership.mem (γ := Set β) (⋃ x ∈ s, t x) x
⊢ (f x, g x) ∈ r
have hx₁ : ∃ i ∈ s, x ∈ t i
Tactic: simp only [mem_iUnion, exists_prop] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
t : (x : β) → Set β
t_open : ∀ x ∈ s, IsOpen[inst_1] (t x)
xt : ∀ x ∈ s, x ∈ t x
ht : ∀ x ∈ s, ∀ z ∈ t x, (f z, g z) ∈ r
x : β
hx : ∃ i ∈ s, x ∈ t i
⊢ (f x, g x) ∈ r
have rcases : ∀ (y : β) (ys : y ∈ s) (hy : x ∈ t y), (f x, g x) ∈ r
Tactic: rcases hx with ⟨y, ys, hy⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
uniformSpace : UniformSpace α
l : Filter α
h : Cauchy l
⊢ Cauchy (↑(Ultrafilter.of l) : Filter α)
have this : l.NeBot
Tactic: haveI := h.1
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
uniformSpace : UniformSpace α
l : Filter α
h : Cauchy l
this : l.NeBot
⊢ Cauchy (↑(Ultrafilter.of l) : Filter α)
have this₁ : (↑(Ultrafilter.of l) : Filter α) ≤ l
Tactic: have := Ultrafilter.of_le l
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
l : Filter β
f : β → α
⊢ Cauchy (map f l) ↔ l.NeBot ∧ Tendsto (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)
have rw : (map f l).NeBot ∧ map f l ×ˢ map f l ≤ 𝓤 α ↔ l.NeBot ∧ Tendsto (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)
Tactic: rw [Cauchy, map_neBot_iff, prod_map_map_eq, Tendsto]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
l : Filter β
f : β → α
rw : (map f l).NeBot ∧ map f l ×ˢ map f l ≤ 𝓤 α ↔ l.NeBot ∧ Tendsto (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)
⊢ Cauchy (map f l) ↔ l.NeBot ∧ Tendsto (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)
have rw₁ : l.NeBot ∧ map f l ×ˢ map f l ≤ 𝓤 α ↔ l.NeBot ∧ Tendsto (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)
Tactic: rw [Cauchy, map_neBot_iff, prod_map_map_eq, Tendsto]