awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f g : α → β
s : Set α
hf : UniformContinuousOn f s
h : EqOn f g s
apply :
  EventuallyEq.{ua, ub} (β := β × β) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (fun (x : α × α) ↦ (f x.1, f x.2)) fun (x : α × α) ↦
    (g x.1, g x.2)
⊢ UniformContinuousOn g s

Tactic:
apply hf.congr'

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f g : α → β
s : Set α
hf : UniformContinuousOn f s
h : EqOn f g s
apply :
  EventuallyEq.{ua, ub} (β := β × β) (𝓟 (s ×ˢ s)) (fun (x : α × α) ↦ (f x.1, f x.2)) fun (x : α × α) ↦ (g x.1, g x.2)
⊢ 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

Premises used: Filter.EventuallyEq.filter_mono, inf_le_right
-- Module: Mathlib.Topology.UniformSpace.Basic
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 : α
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)
⊢ (a, b) ∈ s ×ˢ s → (f (a, b).1, f (a, b).2) = (g (a, b).1, g (a, b).2)

Tactic:
⟨ha, hb⟩
-- Module: Mathlib.Topology.UniformSpace.Basic
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 : α
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:
simp [h ha, h hb]
-- Module: Mathlib.Topology.UniformSpace.Basic
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)
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)
⊢ EventuallyEq.{ua, ub} (β := β × β) (𝓟 (s ×ˢ s)) (fun (x : α × α) ↦ (f x.1, f x.2)) fun (x : α × α) ↦ (g x.1, g x.2)

Tactic:
filter_upwards [mem_principal_self _] with ⟨a, b⟩ ⟨ha, hb⟩ using by simp [h ha, h hb]

Premises used: Filter.mem_principal_self
-- Module: Mathlib.Topology.UniformSpace.Basic
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
change : Tendsto ((fun (x : β × β) ↦ (g x.1, g x.2)) ∘ fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 γ)
⊢ UniformContinuousOn (g ∘ f) s

Tactic:
change Tendsto ((fun x ↦ (g x.1, g x.2)) ∘ (fun x ↦ (f x.1, f x.2))) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 γ)

Premises used: SProd.sprod, uniformity, Function.comp, Prod.mk, Filter.Tendsto, Filter.principal, Min.min
-- Module: Mathlib.Topology.UniformSpace.Basic
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
apply : Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 β ⊓ 𝓟 (t ×ˢ t))
⊢ Tendsto ((fun (x : β × β) ↦ (g x.1, g x.2)) ∘ fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 γ)

Tactic:
apply Tendsto.comp hg

Premises used: Filter.Tendsto.comp
-- Module: Mathlib.Topology.UniformSpace.Basic
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))

Tactic:
tendsto_inf.2 ⟨hf, tendsto_inf_right ?_⟩

Premises used: Iff.mpr, Filter.tendsto_inf, And.intro, Filter.tendsto_inf_right
-- Module: Mathlib.Topology.UniformSpace.Basic
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
refine : Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓟 (s ×ˢ s)) (𝓟 (t ×ˢ t))
⊢ Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 β ⊓ 𝓟 (t ×ˢ t))

Tactic:
refine tendsto_inf.2 ⟨hf, tendsto_inf_right ?_⟩

Premises used: Iff.mpr, Filter.tendsto_inf, And.intro, Filter.tendsto_inf_right
-- Module: Mathlib.Topology.UniformSpace.Basic
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
simp : ∀ (a b : α), a ∈ s → b ∈ s → f a ∈ t ∧ f b ∈ t
⊢ Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓟 (s ×ˢ s)) (𝓟 (t ×ˢ t))

Tactic:
simp only [tendsto_principal, mem_prod, eventually_principal, and_imp, Prod.forall]

Premises used: and_imp, Filter.tendsto_principal, Filter.eventually_principal, Set.mem_prod, Prod.forall
-- Module: Mathlib.Topology.UniformSpace.Basic
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
⊢ ∀ (a b : α), a ∈ s → b ∈ s → f a ∈ t ∧ f b ∈ t

Tactic:
fun a b ha hb ↦ ⟨hst ha, hst hb⟩

Premises used: And.intro
-- Module: Mathlib.Topology.UniformSpace.Basic
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
⊢ ∀ (a b : α), a ∈ s → b ∈ s → f a ∈ t ∧ f b ∈ t

Tactic:
exact fun a b ha hb ↦ ⟨hst ha, hst hb⟩
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → β
s : Set α
g : β → γ
hg : UniformContinuous g
hf : UniformContinuousOn f s
⊢ UniformContinuousOn (g ∘ f) s

Tactic:
(hg.uniformContinuousOn (s := univ)).comp hf (mapsTo_univ _ _)

Premises used: Set.mapsTo_univ, UniformContinuousOn.comp, UniformContinuous.uniformContinuousOn
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
f : α → β
u₁ : UniformSpace α
u₂ u₃ : UniformSpace β
h₁ : UniformContinuous f
h₂ : UniformContinuous f
⊢ UniformContinuous f

Tactic:
tendsto_inf.mpr ⟨h₁, h₂⟩

Premises used: Iff.mpr, UniformContinuous, Filter.tendsto_inf, uniformity, And.intro
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
f : α → β
u₁ u₂ : UniformSpace α
u₃ : UniformSpace β
hf : UniformContinuous f
⊢ UniformContinuous f

Tactic:
tendsto_inf_left hf

Premises used: UniformContinuous, uniformity, Filter.tendsto_inf_left
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
f : α → β
u₁ u₂ : UniformSpace α
u₃ : UniformSpace β
hf : UniformContinuous f
⊢ UniformContinuous f

Tactic:
tendsto_inf_right hf

Premises used: UniformContinuous, uniformity, Filter.tendsto_inf_right
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
f : α → β
u₁ : Set (UniformSpace α)
u₂ : UniformSpace β
u : UniformSpace α
h₁ : u ∈ u₁
hf : UniformContinuous f
rw : Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (⨅ (i : (↑u₁ : Type ua)), 𝓤 α) (𝓤 β)
⊢ Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)

Tactic:
rw [sInf_eq_iInf', iInf_uniformity]

Premises used: iInf_uniformity, sInf_eq_iInf'
-- Module: Mathlib.Topology.UniformSpace.Basic
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)) (⨅ (i : (↑u₁ : Type ua)), 𝓤 α) (𝓤 β)

Tactic:
tendsto_iInf' ⟨u, h₁⟩ hf

Premises used: Subtype.mk, Filter.tendsto_iInf'
-- Module: Mathlib.Topology.UniformSpace.Basic
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)) (⨅ (i : (↑u₁ : Type ua)), 𝓤 α) (𝓤 β)

Tactic:
exact tendsto_iInf' ⟨u, h₁⟩ hf
-- Module: Mathlib.Topology.UniformSpace.Basic
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)) (𝓤 α) (𝓤 β)
rw₃ 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)) (𝓤 α) (𝓤 β)
⊢ 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]

Premises used: iInf_uniformity, sInf_eq_iInf', Filter.tendsto_iInf, SetCoe.forall
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
ι : Sort u_1
f : α → β
u₁ : ι → UniformSpace α
u₂ : UniformSpace β
i : ι
hf : UniformContinuous f
rw : Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (⨅ (i : ι), 𝓤 α) (𝓤 β)
⊢ Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)

Tactic:
rw [iInf_uniformity]

Premises used: iInf_uniformity
-- Module: Mathlib.Topology.UniformSpace.Basic
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)) (⨅ (i : ι), 𝓤 α) (𝓤 β)

Tactic:
tendsto_iInf' i hf

Premises used: Filter.tendsto_iInf'
-- Module: Mathlib.Topology.UniformSpace.Basic
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)) (⨅ (i : ι), 𝓤 α) (𝓤 β)

Tactic:
exact tendsto_iInf' i hf
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
ι : Sort u_1
f : α → β
u₁ : UniformSpace α
u₂ : ι → UniformSpace β
rw :
  Tendsto.{ua, ub} (β := β × β) (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (⨅ (i : ι), 𝓤 β) ↔
    ∀ (i : ι), Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
rw₁ rw₂ :
  (∀ (i : ι), Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)) ↔
    ∀ (i : ι), Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
⊢ Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β) ↔
    ∀ (i : ι), Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)

Tactic:
rw [iInf_uniformity, tendsto_iInf]

Premises used: iInf_uniformity, Filter.tendsto_iInf
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
hα : UniformSpace α
h : 𝓤 α = 𝓟 SetRel.id
⊢ DiscreteTopology α

Tactic:
⟨(UniformSpace.ext h.symm : ⊥ = hα) ▸ rfl⟩

Premises used: Eq.rec, UniformSpace.ext, DiscreteTopology.mk, Eq.symm, rfl
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
⊢ UniformContinuous.{ua, ua} (α := α) (β := Additive α) (⇑ofMul : (a : α) → Additive α)

Tactic:
uniformContinuous_id

Premises used: Additive, uniformContinuous_id
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
⊢ UniformContinuous.{ua, ua} (α := Additive α) (β := α) (⇑toMul : (a : Additive α) → α)

Tactic:
uniformContinuous_id

Premises used: Additive, uniformContinuous_id
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
⊢ UniformContinuous.{ua, ua} (α := α) (β := Multiplicative α) (⇑ofAdd : (a : α) → Multiplicative α)

Tactic:
uniformContinuous_id

Premises used: uniformContinuous_id, Multiplicative
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
⊢ UniformContinuous.{ua, ua} (α := Multiplicative α) (β := α) (⇑toAdd : (a : Multiplicative α) → α)

Tactic:
uniformContinuous_id

Premises used: uniformContinuous_id, Multiplicative
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
⊢ Eq (α := Filter (Additive α × Additive α)) (𝓤 (Additive α))
    (map (Prod.map (⇑ofMul : (a : α) → Additive α) (⇑ofMul : (a : α) → Additive α)) (𝓤 α))

Tactic:
rfl

Premises used: Set.Mem, Additive, Filter.map, uniformity, setOf, Prod.map, Set.preimage, rfl
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
⊢ Eq (α := Filter (Multiplicative α × Multiplicative α)) (𝓤 (Multiplicative α))
    (map (Prod.map (⇑ofAdd : (a : α) → Multiplicative α) (⇑ofAdd : (a : α) → Multiplicative α)) (𝓤 α))

Tactic:
rfl

Premises used: Set.Mem, Filter.map, uniformity, setOf, Prod.map, Multiplicative, Set.preimage, rfl
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
p : α → Prop
inst : UniformSpace α
⊢ Eq (α := Filter (Subtype p × Subtype p)) (𝓤 (Subtype p))
    (comap (fun (q : Subtype p × Subtype p) ↦ ((↑q.1 : α), (↑q.2 : α))) (𝓤 α))

Tactic:
rfl

Premises used: uniformity, rfl, Filter.comap
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
s : Set α
inst : UniformSpace α
⊢ Eq (α := Filter ((↑s : Type ua) × (↑s : Type ua))) (𝓤 (↑s : Type ua))
    (comap (Prod.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) (𝓤 α))

Tactic:
rfl

Premises used: uniformity, setOf, Prod.map, rfl, Filter.comap
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
s : Set α
inst : UniformSpace α
rw :
  map (α := (↑s : Type ua) × (↑s : Type ua))
      (Prod.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))
      (comap (Prod.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) (𝓤 α)) =
    𝓤 α ⊓ 𝓟 (s ×ˢ s)
rw₁ :
  𝓤 α ⊓
      𝓟
        (range (ι := (↑s : Type ua) × (↑s : Type ua))
          (Prod.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))) =
    𝓤 α ⊓ 𝓟 (s ×ˢ s)
rw₂ :
  𝓤 α ⊓
      𝓟
        (SProd.sprod (α := Set α) (β := Set α) (range (ι := (↑s : Type ua)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))
          (range (ι := (↑s : Type ua)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))) =
    𝓤 α ⊓ 𝓟 (s ×ˢ s)
rw₃ rw₄ : 𝓤 α ⊓ 𝓟 (s ×ˢ s) = 𝓤 α ⊓ 𝓟 (s ×ˢ s)
⊢ map (α := (↑s : Type ua) × (↑s : Type ua))
      (Prod.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) (𝓤 (↑s : Type ua)) =
    𝓤 α ⊓ 𝓟 (s ×ˢ s)

Tactic:
rw [uniformity_setCoe, map_comap, range_prodMap, Subtype.range_val]

Premises used: uniformity_setCoe, Filter.map_comap, Subtype.range_val, Set.range_prodMap
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
p : α → Prop
inst : UniformSpace α
⊢ UniformContinuous.{ua, ua} (α := { a : α // p a }) (Subtype.val (p := fun (a : α) ↦ p a))

Tactic:
uniformContinuous_comap

Premises used: uniformContinuous_comap
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
p : α → Prop
inst : UniformSpace α
inst_1 : UniformSpace β
f : β → α
hf : UniformContinuous f
h : ∀ (x : β), p (f x)
⊢ UniformContinuous.{ub, ua} (β := Subtype p) fun (x : β) ↦ Subtype.mk (p := p) (f x) ⋯

Tactic:
uniformContinuous_comap' hf

Premises used: uniformContinuous_comap'
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
p : α → Prop
q : β → Prop
f : α → β
hf : UniformContinuous f
h : ∀ (x : α), p x → q (f x)
⊢ UniformContinuous (Subtype.map (p := p) (q := q) f h)

Tactic:
(hf.comp uniformContinuous_subtype_val).subtype_mk _

Premises used: Subtype.map, UniformContinuous.comp, uniformContinuous_subtype_val, UniformContinuous.subtype_mk
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
rw :
  Tendsto.{ua, ub} (α := (↑s : Type ua) × (↑s : Type ua))
      ((fun (x : α × α) ↦ (f x.1, f x.2)) ∘
        Prod.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))
      (𝓤 (↑s : Type ua)) (𝓤 β) ↔
    Tendsto
      (fun (x : (↑s : Type ua) × (↑s : Type ua)) ↦
        (s.restrict (π := fun (a : α) ↦ β) f x.1, s.restrict (π := fun (a : α) ↦ β) f x.2))
      (𝓤 (↑s : Type ua)) (𝓤 β)
⊢ Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 β) ↔
    Tendsto
      (fun (x : (↑s : Type ua) × (↑s : Type ua)) ↦
        (s.restrict (π := fun (a : α) ↦ β) f x.1, s.restrict (π := fun (a : α) ↦ β) f x.2))
      (𝓤 (↑s : Type ua)) (𝓤 β)

Tactic:
rw [← map_uniformity_set_coe, tendsto_map'_iff]

Premises used: Filter.tendsto_map'_iff, map_uniformity_set_coe
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
⊢ Tendsto.{ua, ub} (α := (↑s : Type ua) × (↑s : Type ua))
      ((fun (x : α × α) ↦ (f x.1, f x.2)) ∘
        Prod.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))
      (𝓤 (↑s : Type ua)) (𝓤 β) ↔
    Tendsto
      (fun (x : (↑s : Type ua) × (↑s : Type ua)) ↦
        (s.restrict (π := fun (a : α) ↦ β) f x.1, s.restrict (π := fun (a : α) ↦ β) f x.2))
      (𝓤 (↑s : Type ua)) (𝓤 β)

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
a : α
hf : UniformContinuous.{ua, ub} (β := β) fun (x : (↑s : Type ua)) ↦ f (↑x : α)
ha : s ∈ 𝓝 a
rw : Tendsto f (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ⋯))) (𝓝 (f a))
⊢ Tendsto f (𝓝 a) (𝓝 (f a))

Tactic:
rw [(@map_nhds_subtype_coe_eq_nhds α _ (· ∈ s) a (mem_of_mem_nhds ha) ha).symm]

Premises used: mem_of_mem_nhds, map_nhds_subtype_coe_eq_nhds, Eq.symm
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
a : α
hf : UniformContinuous.{ua, ub} (β := β) fun (x : (↑s : Type ua)) ↦ f (↑x : α)
ha : s ∈ 𝓝 a
⊢ Tendsto f (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ⋯))) (𝓝 (f a))

Tactic:
tendsto_map' hf.continuous.continuousAt

Premises used: Filter.tendsto_map', UniformContinuous.continuous, Continuous.continuousAt
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
a : α
hf : UniformContinuous.{ua, ub} (β := β) fun (x : (↑s : Type ua)) ↦ f (↑x : α)
ha : s ∈ 𝓝 a
⊢ Tendsto f (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ⋯))) (𝓝 (f a))

Tactic:
exact tendsto_map' hf.continuous.continuousAt

Premises used: Filter.tendsto_map', UniformContinuous.continuous, Continuous.continuousAt
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
h : UniformContinuousOn f s
⊢ UniformContinuous (s.restrict (π := fun (a : α) ↦ β) f)

Tactic:
rw [uniformContinuousOn_iff_restrict] at h

Premises used: uniformContinuousOn_iff_restrict
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
h : UniformContinuous (s.restrict (π := fun (a : α) ↦ β) f)
rw : Continuous[instTopologicalSpaceSubtype, inst_1.toTopologicalSpace] (s.restrict (π := fun (a : α) ↦ β) f)
⊢ ContinuousOn f s

Tactic:
rw [continuousOn_iff_continuous_restrict]

Premises used: continuousOn_iff_continuous_restrict
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
h : UniformContinuous (s.restrict (π := fun (a : α) ↦ β) f)
⊢ Continuous[instTopologicalSpaceSubtype, inst_1.toTopologicalSpace] (s.restrict (π := fun (a : α) ↦ β) f)

Tactic:
h.continuous

Premises used: UniformContinuous.continuous
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
h : UniformContinuous (s.restrict (π := fun (a : α) ↦ β) f)
⊢ Continuous[instTopologicalSpaceSubtype, inst_1.toTopologicalSpace] (s.restrict (π := fun (a : α) ↦ β) f)

Tactic:
exact h.continuous

Premises used: UniformContinuous.continuous
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst : UniformSpace α
inst_1 : (𝓤 α).IsCountablyGenerated
s : Set α
⊢ IsCountablyGenerated.{ua} (α := (↑s : Type ua) × (↑s : Type ua)) (𝓤 (↑s : Type ua))

Tactic:
Filter.comap.isCountablyGenerated _ _

Premises used: uniformity, setOf, Filter.comap.isCountablyGenerated, Filter.comap
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
⊢ Eq (α := Filter (αᵐᵒᵖ × αᵐᵒᵖ)) (𝓤 αᵐᵒᵖ)
    (comap (fun (q : αᵐᵒᵖ × αᵐᵒᵖ) ↦ (MulOpposite.unop q.1, MulOpposite.unop q.2)) (𝓤 α))

Tactic:
rfl

Premises used: uniformity, rfl, Filter.comap
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
⊢ comap (β := αᵐᵒᵖ × αᵐᵒᵖ) (fun (p : α × α) ↦ (MulOpposite.op p.1, MulOpposite.op p.2)) (𝓤 αᵐᵒᵖ) = 𝓤 α

Tactic:
simpa [uniformity_mulOpposite, comap_comap, (· ∘ ·)] using comap_id

Premises used: Function.comp, Filter.comap_comap, Filter.comap_id, uniformity_mulOpposite
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
⊢ UniformContinuous.{ua, ua} (α := αᵐᵒᵖ) unop

Tactic:
uniformContinuous_comap

Premises used: uniformContinuous_comap
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
⊢ UniformContinuous.{ua, ua} (α := α) op

Tactic:
uniformContinuous_comap' uniformContinuous_id

Premises used: uniformContinuous_id, uniformContinuous_comap'
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst : UniformSpace α
inst_1 : UniformSpace β
⊢ Eq (α := TopologicalSpace (α × β)) instTopologicalSpaceProd toTopologicalSpace

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst : UniformSpace α
inst_1 : UniformSpace β
⊢ Eq (α := TopologicalSpace (α × β)) instTopologicalSpaceProd toTopologicalSpace

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
⊢ Eq (α := Filter ((α × β) × α × β)) (𝓤 (α × β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓
      Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.2, p.2.2)) (𝓤 β))

Tactic:
rfl

Premises used: Set.Mem, uniformity, setOf, rfl
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst : UniformSpace α
inst_1 : (𝓤 α).IsCountablyGenerated
inst_2 : UniformSpace β
inst_3 : (𝓤 β).IsCountablyGenerated
⊢ IsCountablyGenerated (α := (α × β) × α × β)
    (Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓
      Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.2, p.2.2)) (𝓤 β))

Tactic:
infer_instance