awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Basic
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 α
haveI : (this : UniformSpace β) → Prop
⊢ Prop

Tactic:
haveI := sInf ubs
-- Module: Mathlib.Topology.UniformSpace.Basic
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_1 : UniformSpace α
this : UniformSpace β
⊢ Prop

Tactic:
exact @UniformContinuous _ _ _ uc fun p : α × β => f p.1 p.2

Premises used: UniformContinuous, Prod.fst, Prod.snd
-- Module: Mathlib.Topology.UniformSpace.Basic
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.{u_2, u_2} (α := α) id

Tactic:
have ha := uniformContinuous_sInf_dom ha uniformContinuous_id
-- Module: Mathlib.Topology.UniformSpace.Basic
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.{u_3, u_3} (α := β) id

Tactic:
have hb := uniformContinuous_sInf_dom hb uniformContinuous_id
-- Module: Mathlib.Topology.UniformSpace.Basic
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 (α := α × β) (Prod.map id id)

Tactic:
have h_unif_cont_id := @UniformContinuous.prodMap _ _ _ _ (sInf uas) (sInf ubs) ua ub _ _ ha hb
-- Module: Mathlib.Topology.UniformSpace.Basic
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
h_unif_cont_id : UniformContinuous (α := α × β) (Prod.map id id)
⊢ UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2

Tactic:
@UniformContinuous.comp _ _ _ (id _) (id _) _ _ _ hf h_unif_cont_id

Premises used: UniformContinuous.comp
-- Module: Mathlib.Topology.UniformSpace.Basic
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
h_unif_cont_id : UniformContinuous (α := α × β) (Prod.map id id)
⊢ UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2

Tactic:
exact @UniformContinuous.comp _ _ _ (id _) (id _) _ _ _ hf h_unif_cont_id

Premises used: UniformContinuous.comp
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → β → γ
⊢ UniformContinuous₂ f ↔ UniformContinuous (uncurry f)

Tactic:
Iff.rfl

Premises used: UniformContinuous₂, Iff.rfl
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → β → γ
h : UniformContinuous₂ f
⊢ UniformContinuous (uncurry f)

Tactic:
h

Premises used: UniformContinuous₂
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α × β → γ
rw : UniformContinuous (uncurry (Function.curry f)) ↔ UniformContinuous f
rw₁ rw₂ : UniformContinuous f ↔ UniformContinuous f
⊢ UniformContinuous₂ (Function.curry f) ↔ UniformContinuous f

Tactic:
rw [UniformContinuous₂, uncurry_curry]

Premises used: UniformContinuous₂, Function.uncurry_curry
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
f : α → β → γ
g : γ → δ
hg : UniformContinuous g
hf : UniformContinuous₂ f
⊢ UniformContinuous₂ (g ∘₂ f)

Tactic:
hg.comp hf

Premises used: UniformContinuous₂, UniformContinuous.comp, Function.bicompr
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
δ' : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
inst_4 : UniformSpace δ'
f : α → β → γ
ga : δ → α
gb : δ' → β
hf : UniformContinuous₂ f
hga : UniformContinuous ga
hgb : UniformContinuous gb
⊢ UniformContinuous₂ (Function.bicompl f ga gb)

Tactic:
hf.uniformContinuous.comp (hga.prodMap hgb)

Premises used: UniformContinuous₂, UniformContinuous.prodMap, UniformContinuous.comp, UniformContinuous₂.uniformContinuous, Function.bicompl
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
u : UniformSpace α
p : α → Prop
⊢ Eq.{ua + 1} (α := TopologicalSpace (Subtype p)) UniformSpace.toTopologicalSpace (instTopologicalSpaceSubtype (p := p))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.UniformSpace.Basic
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
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
⊢ 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α⟩

Premises used: comp_mem_uniformity_sets, And.left
-- Module: Mathlib.Topology.UniformSpace.Basic
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
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
⊢ 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β⟩

Premises used: comp_mem_uniformity_sets, And.right
-- Module: Mathlib.Topology.UniformSpace.Basic
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
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
⊢ 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:
filter_upwards [mem_lift' (union_mem_sup (image_mem_map htα) (image_mem_map htβ))]

Premises used: Filter.image_mem_map, Filter.mem_lift', Filter.union_mem_sup
-- Module: Mathlib.Topology.UniformSpace.Basic
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
a b : α
hab : (a, b) ∈ tα
c : α
hbc : (b, c) ∈ tα
⊢ (inl (a, b).1, inl (b, c).2) ∈ s

Tactic:
@Htα (_, _) ⟨b, hab, hbc⟩

Premises used: Set.Mem, setOf, Set.preimage, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Basic
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
a b : β
hab : (a, b) ∈ tβ
c : β
hbc : (b, c) ∈ tβ
⊢ (inr (a, b).1, inr (b, c).2) ∈ s

Tactic:
@Htβ (_, _) ⟨b, hab, hbc⟩

Premises used: Set.Mem, setOf, Set.preimage, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Basic
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
a b : α
hab : (a, b) ∈ tα
c : α
hbc : (b, c) ∈ tα
⊢ (inl (a, b).1, inl (b, c).2) ∈ s

Tactic:
exacts [@Htα (_, _) ⟨b, hab, hbc⟩, @Htβ (_, _) ⟨b, hab, hbc⟩]

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst : UniformSpace α
inst_1 : UniformSpace β
x : α ⊕ β
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
⊢ 𝓝 x =
    comap (Prod.mk x)
      (map (fun (p : α × α) ↦ (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun (p : β × β) ↦ (inr p.1, inr p.2)) (𝓤 β))

Tactic:
ext
-- Module: Mathlib.Topology.UniformSpace.Basic
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
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
⊢ 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:
cases x
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set (α ⊕ β)
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:
simp [mem_comap', -mem_comap, nhds_inl, nhds_inr, nhds_eq_comap_uniformity,
      Prod.ext_iff]

Premises used: Prod.ext_iff, nhds_inl, nhds_inr, Filter.mem_comap, nhds_eq_comap_uniformity, Filter.mem_comap'
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set (α ⊕ β)
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:
simp [mem_comap', -mem_comap, nhds_inl, nhds_inr, nhds_eq_comap_uniformity,
      Prod.ext_iff]

Premises used: Prod.ext_iff, nhds_inl, nhds_inr, Filter.mem_comap, nhds_eq_comap_uniformity, Filter.mem_comap'
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
a : SetRel α α
ha : a ∈ 𝓤 α
b : SetRel β β
hb : b ∈ 𝓤 β
⊢ Membership.mem (γ := Filter ((α ⊕ β) × (α ⊕ β))) (𝓤 (α ⊕ β)) (Prod.map inl inl '' a ∪ Prod.map inr inr '' b)

Tactic:
union_mem_sup (image_mem_map ha) (image_mem_map hb)

Premises used: Set.Mem, setOf, Filter.image_mem_map, Filter.union_mem_sup
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
⊢ 𝓤 (α ⊕ β) = map (Prod.map inl inl) (𝓤 α) ⊔ map (Prod.map inr inr) (𝓤 β)

Tactic:
rfl

Premises used: Set.Mem, uniformity, setOf, Prod.map, rfl
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
⊢ UniformContinuous (α := α) (β := α ⊕ β) inl

Tactic:
le_sup_left

Premises used: UniformContinuous, le_sup_left, Set.Mem, Filter.Tendsto
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
⊢ UniformContinuous (α := β) (β := α ⊕ β) inr

Tactic:
le_sup_right

Premises used: UniformContinuous, Set.Mem, le_sup_right, Filter.Tendsto
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : (𝓤 α).IsCountablyGenerated
inst_3 : (𝓤 β).IsCountablyGenerated
⊢ (map (Prod.map inl inl) (𝓤 α) ⊔ map (Prod.map inr inr) (𝓤 β)).IsCountablyGenerated

Tactic:
infer_instance
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
f : Filter β
u : β → α
a : α
rw : Tendsto (Prod.mk a ∘ u) f (𝓤 α) ↔ Tendsto (fun (x : β) ↦ (a, u x)) f (𝓤 α)
⊢ Tendsto u f (𝓝 a) ↔ Tendsto (fun (x : β) ↦ (a, u x)) f (𝓤 α)

Tactic:
rw [nhds_eq_comap_uniformity, tendsto_comap_iff]

Premises used: Filter.tendsto_comap_iff, nhds_eq_comap_uniformity
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto (Prod.mk a ∘ u) f (𝓤 α) ↔ Tendsto (fun (x : β) ↦ (a, u x)) f (𝓤 α)

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
f : Filter β
u : β → α
a : α
rw : Tendsto ((fun (y : α) ↦ (y, a)) ∘ u) f (𝓤 α) ↔ Tendsto (fun (x : β) ↦ (u x, a)) f (𝓤 α)
⊢ Tendsto u f (𝓝 a) ↔ Tendsto (fun (x : β) ↦ (u x, a)) f (𝓤 α)

Tactic:
rw [nhds_eq_comap_uniformity', tendsto_comap_iff]

Premises used: Filter.tendsto_comap_iff, nhds_eq_comap_uniformity'
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto ((fun (y : α) ↦ (y, a)) ∘ u) f (𝓤 α) ↔ Tendsto (fun (x : β) ↦ (u x, a)) f (𝓤 α)

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Basic
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) (𝓤 α)
rw₁ rw₂ : Tendsto (fun (x : β) ↦ (f b, f x)) (𝓝 b) (𝓤 α) ↔ Tendsto (fun (x : β) ↦ (f b, f x)) (𝓝 b) (𝓤 α)
⊢ ContinuousAt f b ↔ Tendsto (fun (x : β) ↦ (f b, f x)) (𝓝 b) (𝓤 α)

Tactic:
rw [ContinuousAt, tendsto_nhds_right]

Premises used: ContinuousAt, Uniform.tendsto_nhds_right
-- Module: Mathlib.Topology.UniformSpace.Basic
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) (𝓤 α)
rw₁ rw₂ : Tendsto (fun (x : β) ↦ (f x, f b)) (𝓝 b) (𝓤 α) ↔ Tendsto (fun (x : β) ↦ (f x, f b)) (𝓝 b) (𝓤 α)
⊢ ContinuousAt f b ↔ Tendsto (fun (x : β) ↦ (f x, f b)) (𝓝 b) (𝓤 α)

Tactic:
rw [ContinuousAt, tendsto_nhds_left]

Premises used: ContinuousAt, Uniform.tendsto_nhds_left
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
f : β → α
b : β
⊢ ContinuousAt f b ↔ Tendsto (fun (x : β × β) ↦ (f x.1, f x.2)) (𝓝 (b, b)) (𝓤 α)

Tactic:
⟨fun H => le_trans (H.prodMap' H) (nhds_le_uniformity _), fun H =>
    continuousAt_iff'_left.2 <| H.comp <| tendsto_id.prodMk_nhds tendsto_const_nhds⟩

Premises used: Iff.mpr, Filter.tendsto_id, tendsto_const_nhds, ContinuousAt.prodMap', nhds_le_uniformity, Uniform.continuousAt_iff'_left, Iff.intro, Filter.Tendsto.comp, Filter.Tendsto.prodMk_nhds, le_trans
-- Module: Mathlib.Topology.UniformSpace.Basic
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) (𝓤 α)
rw₁ rw₂ : Tendsto (fun (x : β) ↦ (f b, f x)) (𝓝[s] b) (𝓤 α) ↔ Tendsto (fun (x : β) ↦ (f b, f x)) (𝓝[s] b) (𝓤 α)
⊢ ContinuousWithinAt f s b ↔ Tendsto (fun (x : β) ↦ (f b, f x)) (𝓝[s] b) (𝓤 α)

Tactic:
rw [ContinuousWithinAt, tendsto_nhds_right]

Premises used: ContinuousWithinAt, Uniform.tendsto_nhds_right
-- Module: Mathlib.Topology.UniformSpace.Basic
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) (𝓤 α)
rw₁ rw₂ : Tendsto (fun (x : β) ↦ (f x, f b)) (𝓝[s] b) (𝓤 α) ↔ Tendsto (fun (x : β) ↦ (f x, f b)) (𝓝[s] b) (𝓤 α)
⊢ ContinuousWithinAt f s b ↔ Tendsto (fun (x : β) ↦ (f x, f b)) (𝓝[s] b) (𝓤 α)

Tactic:
rw [ContinuousWithinAt, tendsto_nhds_left]

Premises used: ContinuousWithinAt, Uniform.tendsto_nhds_left
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
f : β → α
s : Set β
⊢ ContinuousOn f s ↔ ∀ b ∈ s, Tendsto (fun (x : β) ↦ (f b, f x)) (𝓝[s] b) (𝓤 α)

Tactic:
simp [ContinuousOn, continuousWithinAt_iff'_right]

Premises used: Uniform.continuousWithinAt_iff'_right, ContinuousOn
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
f : β → α
s : Set β
⊢ ContinuousOn f s ↔ ∀ b ∈ s, Tendsto (fun (x : β) ↦ (f x, f b)) (𝓝[s] b) (𝓤 α)

Tactic:
simp [ContinuousOn, continuousWithinAt_iff'_left]

Premises used: Uniform.continuousWithinAt_iff'_left, ContinuousOn
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
f : β → α
⊢ Continuous[inst_1, inst.toTopologicalSpace] f ↔ ∀ (b : β), Tendsto (fun (x : β) ↦ (f b, f x)) (𝓝 b) (𝓤 α)

Tactic:
continuous_iff_continuousAt.trans <| forall_congr' fun _ => tendsto_nhds_right

Premises used: Uniform.tendsto_nhds_right, forall_congr', Iff.trans, continuous_iff_continuousAt
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
f : β → α
⊢ Continuous[inst_1, inst.toTopologicalSpace] f ↔ ∀ (b : β), Tendsto (fun (x : β) ↦ (f x, f b)) (𝓝 b) (𝓤 α)

Tactic:
continuous_iff_continuousAt.trans <| forall_congr' fun _ => tendsto_nhds_left

Premises used: forall_congr', Iff.trans, Uniform.tendsto_nhds_left, continuous_iff_continuousAt
-- Module: Mathlib.Topology.UniformSpace.Basic
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
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
⊢ ∃ (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

Premises used: comp_symm_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.Basic
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
⊢ {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)
-- Module: Mathlib.Topology.UniformSpace.Basic
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
⊢ {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)