awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
simp_rw :
  Eq (α := Filter ((α × β) × α × β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓
      Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.2, p.2.2)) (𝓤 β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β))
simp_rw₁ :
  Eq (α := Filter ((α × β) × α × β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓
      Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.2, p.2.2)) (𝓤 β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
      (Filter.comap Prod.fst (𝓤 α) ⊓ Filter.comap Prod.snd (𝓤 β)))
simp_rw₂ :
  Eq (α := Filter ((α × β) × α × β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓
      Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.2, p.2.2)) (𝓤 β))
    (Filter.comap (β := Prod.{ua, ub} (α × α) (β × β)) (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
        (Filter.comap Prod.fst (𝓤 α)) ⊓
      Filter.comap (β := Prod.{ua, ub} (α × α) (β × β)) (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
        (Filter.comap Prod.snd (𝓤 β)))
simp_rw₃ :
  Eq (α := Filter ((α × β) × α × β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓
      Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.2, p.2.2)) (𝓤 β))
    (Filter.comap
        (Function.comp (β := Prod.{ua, ub} (α × α) (β × β)) Prod.fst fun (p : (α × β) × α × β) ↦
          ((p.1.1, p.2.1), p.1.2, p.2.2))
        (𝓤 α) ⊓
      Filter.comap
        (Function.comp (β := Prod.{ua, ub} (α × α) (β × β)) Prod.snd fun (p : (α × β) × α × β) ↦
          ((p.1.1, p.2.1), p.1.2, p.2.2))
        (𝓤 β))
⊢ Eq (α := Filter ((α × β) × α × β)) (𝓤 (α × β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β))

Tactic:
simp_rw [uniformity_prod, prod_eq_inf, Filter.comap_inf, Filter.comap_comap, Function.comp_def]

Premises used: Filter.prod_eq_inf, Filter.comap_inf, Function.comp_def, Filter.comap_comap, uniformity_prod
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
rw :
  Eq (α := Filter ((α × β) × α × β)) (𝓤 (α × β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β))
rw₁ rw₂ :
  Eq (α := Filter ((α × β) × α × β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β))
⊢ Eq (α := Filter ((α × β) × α × β)) (𝓤 (α × β))
    (map (fun (p : Prod.{ua, ub} (α × α) (β × β)) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β))

Tactic:
rw [map_swap4_eq_comap, uniformity_prod_eq_comap_prod]

Premises used: Filter.map_swap4_eq_comap, uniformity_prod_eq_comap_prod
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
s : SetRel β β
f : α → α → β
hf : UniformContinuous.{ua, ub} (β := β) fun (p : α × α) ↦ f p.1 p.2
hs : s ∈ 𝓤 β
⊢ Tendsto
    ((fun (x : (α × α) × α × α) ↦ (f x.1.1 x.1.2, f x.2.1 x.2.2)) ∘ fun (p : (α × α) × α × α) ↦
      ((p.1.1, p.2.1), p.1.2, p.2.2))
    (𝓤 α ×ˢ 𝓤 α) (𝓤 β)

Tactic:
rw [UniformContinuous, uniformity_prod_eq_prod, tendsto_map'_iff] at hf

Premises used: UniformContinuous, Filter.tendsto_map'_iff, uniformity_prod_eq_prod
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
s : SetRel β β
f : α → α → β
hf : UniformContinuous.{ua, ub} (β := β) fun (p : α × α) ↦ f p.1 p.2
hs : s ∈ 𝓤 β
hf₁ :
  Tendsto
    ((fun (x : (α × α) × α × α) ↦ (f x.1.1 x.1.2, f x.2.1 x.2.2)) ∘ fun (p : (α × α) × α × α) ↦
      ((p.1.1, p.2.1), p.1.2, p.2.2))
    (𝓤 α ×ˢ 𝓤 α) (𝓤 β)
⊢ s ∈ 𝓤 β

Tactic:
rw [UniformContinuous, uniformity_prod_eq_prod, tendsto_map'_iff] at hf

Premises used: UniformContinuous, Filter.tendsto_map'_iff, uniformity_prod_eq_prod
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
s : SetRel β β
f : α → α → β
hf :
  Tendsto
    ((fun (x : (α × α) × α × α) ↦ (f x.1.1 x.1.2, f x.2.1 x.2.2)) ∘ fun (p : (α × α) × α × α) ↦
      ((p.1.1, p.2.1), p.1.2, p.2.2))
    (𝓤 α ×ˢ 𝓤 α) (𝓤 β)
hs : s ∈ 𝓤 β
rcases :
  ∀ (u : Set (α × α)) (hu : u ∈ 𝓤 α) (v : Set (α × α)) (hv : v ∈ 𝓤 α)
    (huvt :
      u ×ˢ v ⊆
        ((fun (x : (α × α) × α × α) ↦ (f x.1.1 x.1.2, f x.2.1 x.2.2)) ∘ fun (p : (α × α) × α × α) ↦
            ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹'
          s),
    ∃ u ∈ 𝓤 α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s
⊢ ∃ u ∈ 𝓤 α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s

Tactic:
rcases mem_prod_iff.1 (mem_map.1 <| hf hs) with ⟨u, hu, v, hv, huvt⟩

Premises used: Iff.mp, Filter.mem_prod_iff, Filter.mem_map
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
s : SetRel β β
f : α → α → β
hf :
  Tendsto
    ((fun (x : (α × α) × α × α) ↦ (f x.1.1 x.1.2, f x.2.1 x.2.2)) ∘ fun (p : (α × α) × α × α) ↦
      ((p.1.1, p.2.1), p.1.2, p.2.2))
    (𝓤 α ×ˢ 𝓤 α) (𝓤 β)
hs : s ∈ 𝓤 β
u : Set (α × α)
hu : u ∈ 𝓤 α
v : Set (α × α)
hv : v ∈ 𝓤 α
huvt :
  u ×ˢ v ⊆
    ((fun (x : (α × α) × α × α) ↦ (f x.1.1 x.1.2, f x.2.1 x.2.2)) ∘ fun (p : (α × α) × α × α) ↦
        ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹'
      s
⊢ ∃ u ∈ 𝓤 α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s

Tactic:
⟨u, hu, fun a b c hab => @huvt ((_, _), (_, _)) ⟨hab, refl_mem_uniformity hv⟩⟩

Premises used: refl_mem_uniformity, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
s : SetRel β β
f : α → α → β
hf :
  Tendsto
    ((fun (x : (α × α) × α × α) ↦ (f x.1.1 x.1.2, f x.2.1 x.2.2)) ∘ fun (p : (α × α) × α × α) ↦
      ((p.1.1, p.2.1), p.1.2, p.2.2))
    (𝓤 α ×ˢ 𝓤 α) (𝓤 β)
hs : s ∈ 𝓤 β
u : Set (α × α)
hu : u ∈ 𝓤 α
v : Set (α × α)
hv : v ∈ 𝓤 α
huvt :
  u ×ˢ v ⊆
    ((fun (x : (α × α) × α × α) ↦ (f x.1.1 x.1.2, f x.2.1 x.2.2)) ∘ fun (p : (α × α) × α × α) ↦
        ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹'
      s
⊢ ∃ u ∈ 𝓤 α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s

Tactic:
exact ⟨u, hu, fun a b c hab => @huvt ((_, _), (_, _)) ⟨hab, refl_mem_uniformity hv⟩⟩
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
u : SetRel α α
v : SetRel β β
p : (α × β) × α × β
⊢ p ∈ entourageProd u v ↔ (p.1.1, p.2.1) ∈ u ∧ (p.1.2, p.2.2) ∈ v

Tactic:
Iff.rfl

Premises used: entourageProd, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
t₁ : UniformSpace α
t₂ : UniformSpace β
u : SetRel α α
v : SetRel β β
hu : u ∈ 𝓤 α
hv : v ∈ 𝓤 β
⊢ Membership.mem (γ := Filter ((α × β) × α × β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓
      Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.2, p.2.2)) (𝓤 β))
    (entourageProd u v)

Tactic:
inter_mem_inf (preimage_mem_comap hu) (preimage_mem_comap hv)

Premises used: entourageProd, Filter.inter_mem_inf, Set.Mem, setOf, Set.inter, Filter.preimage_mem_comap
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
t₁ : UniformSpace α
t₂ : UniformSpace β
u : SetRel α α
v : SetRel β β
hu : u ∈ 𝓤 α
hv : v ∈ 𝓤 β
⊢ Membership.mem (γ := Filter ((α × β) × α × β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓
      Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.2, p.2.2)) (𝓤 β))
    (entourageProd u v)

Tactic:
exact inter_mem_inf (preimage_mem_comap hu) (preimage_mem_comap hv)

Premises used: Filter.inter_mem_inf, Filter.preimage_mem_comap
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
u : SetRel α α
v : SetRel β β
x : α × β
h : ∀ (p : α × β), p ∈ ball x (entourageProd u v) ↔ p ∈ ball x.1 u ×ˢ ball x.2 v
⊢ ball x (entourageProd u v) = ball x.1 u ×ˢ ball x.2 v

Tactic:
ext p
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
u : SetRel α α
v : SetRel β β
x p : α × β
⊢ p ∈ ball x (entourageProd u v) ↔ p ∈ ball x.1 u ×ˢ ball x.2 v

Tactic:
simp only [ball, entourageProd, Set.mem_setOf_eq, Set.mem_prod, Set.mem_preimage]

Premises used: entourageProd, Set.mem_setOf_eq, UniformSpace.ball, Set.mem_prod, Set.mem_preimage
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
u : SetRel α α
v : SetRel β β
⊢ (entourageProd u v).inv = entourageProd u.inv v.inv

Tactic:
rfl

Premises used: entourageProd, Set.Mem, SetRel.inv, setOf, Set.preimage, Prod.swap, rfl
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
u : SetRel α α
v : SetRel β β
s : Set α
t : Set β
h : ∀ (x : α × β), x ∈ (entourageProd u v).image (s ×ˢ t) ↔ x ∈ u.image s ×ˢ v.image t
⊢ (entourageProd u v).image (s ×ˢ t) = u.image s ×ˢ v.image t

Tactic:
ext
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
u : SetRel α α
v : SetRel β β
s : Set α
t : Set β
x : α × β
h : (∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ (a, x.1) ∈ u ∧ (b, x.2) ∈ v) ↔ (∃ a ∈ s, (a, x.1) ∈ u) ∧ ∃ a ∈ t, (a, x.2) ∈ v
⊢ x ∈ (entourageProd u v).image (s ×ˢ t) ↔ x ∈ u.image s ×ˢ v.image t

Tactic:
simp only [mem_entourageProd, SetRel.mem_image, Set.mem_prod, Prod.exists]

Premises used: SetRel.mem_image, Set.mem_prod, mem_entourageProd, Prod.exists
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
u : SetRel α α
v : SetRel β β
s : Set α
t : Set β
x : α × β
⊢ (∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ (a, x.1) ∈ u ∧ (b, x.2) ∈ v) ↔ (∃ a ∈ s, (a, x.1) ∈ u) ∧ ∃ a ∈ t, (a, x.2) ∈ v

Tactic:
grind
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
u : SetRel α α
v : SetRel β β
s : Set α
t : Set β
⊢ (entourageProd u v).preimage (s ×ˢ t) = u.preimage s ×ˢ v.preimage t

Tactic:
image_entourageProd_prod u.inv v.inv s t

Premises used: entourageProd, Set.Mem, SetRel.inv, setOf, Set.preimage, SetRel.preimage, Prod.swap, image_entourageProd_prod
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
ιa : Type u_2
ιb : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
pa : ιa → Prop
pb : ιb → Prop
sa : ιa → SetRel α α
sb : ιb → SetRel β β
ha : (𝓤 α).HasBasis pa sa
hb : (𝓤 β).HasBasis pb sb
⊢ HasBasis (α := (α × β) × α × β) (𝓤 (α × β)) (fun (i : ιa × ιb) ↦ pa i.1 ∧ pb i.2) fun (i : ιa × ιb) ↦
    entourageProd (sa i.1) (sb i.2)

Tactic:
(ha.comap _).inf (hb.comap _)

Premises used: Filter.HasBasis.inf, entourageProd, Set.Mem, uniformity, setOf, Set.inter, Filter.HasBasis.comap, Set.preimage
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set ((α × β) × α × β)
h : Membership.mem (γ := Filter ((α × β) × α × β)) (𝓤 (α × β)) s
rcases :
  ∀ (w : Prod.{ua, ub} (Set (α × α)) (Set (β × β)))
    (hw : (w.1 ∈ 𝓤 α ∧ w.2 ∈ 𝓤 β) ∧ entourageProd (id w.1) (id w.2) ⊆ s), ∃ u ∈ 𝓤 α, ∃ v ∈ 𝓤 β, entourageProd u v ⊆ s
⊢ ∃ u ∈ 𝓤 α, ∃ v ∈ 𝓤 β, entourageProd u v ⊆ s

Tactic:
rcases (((𝓤 α).basis_sets.uniformity_prod (𝓤 β).basis_sets).mem_iff' s).1 h with ⟨w, hw⟩

Premises used: Filter.HasBasis.uniformity_prod, uniformity, Filter.basis_sets, Iff.mp, Filter.HasBasis.mem_iff'
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set ((α × β) × α × β)
h : Membership.mem (γ := Filter ((α × β) × α × β)) (𝓤 (α × β)) s
w : Prod.{ua, ub} (Set (α × α)) (Set (β × β))
hw : (w.1 ∈ 𝓤 α ∧ w.2 ∈ 𝓤 β) ∧ entourageProd (id w.1) (id w.2) ⊆ s
w₁ : Set (α × α)
left : w.1 ∈ 𝓤 α
w₂ : Set (β × β)
left₁ : w.2 ∈ 𝓤 β
right : entourageProd w.1 w.2 ⊆ s
⊢ ∃ u ∈ 𝓤 α, ∃ v ∈ 𝓤 β, entourageProd u v ⊆ s

Tactic:
use w.1, hw.1.1, w.2, hw.1.2, hw.2

Premises used: Prod.fst, And.right, And.left, Prod.snd
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
⊢ Tendsto (fun (p : (α × β) × α × β) ↦ (p.1.1, p.2.1)) (𝓤 (α × β)) (𝓤 α)

Tactic:
le_trans (map_mono inf_le_left) map_comap_le

Premises used: Filter.map_mono, Filter.Tendsto, inf_le_left, Filter.map_comap_le, le_trans
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
⊢ Tendsto (fun (p : (α × β) × α × β) ↦ (p.1.2, p.2.2)) (𝓤 (α × β)) (𝓤 β)

Tactic:
le_trans (map_mono inf_le_right) map_comap_le

Premises used: Filter.map_mono, inf_le_right, Filter.Tendsto, Filter.map_comap_le, le_trans
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
⊢ UniformContinuous (β := α) fun (p : α × β) ↦ p.1

Tactic:
tendsto_prod_uniformity_fst

Premises used: UniformContinuous, tendsto_prod_uniformity_fst
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
⊢ UniformContinuous (β := β) fun (p : α × β) ↦ p.2

Tactic:
tendsto_prod_uniformity_snd

Premises used: UniformContinuous, tendsto_prod_uniformity_snd
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f₁ : α → β
f₂ : α → γ
h₁ : UniformContinuous f₁
h₂ : UniformContinuous f₂
⊢ Tendsto (β := (β × γ) × β × γ) (fun (x : α × α) ↦ ((f₁ x.1, f₂ x.1), f₁ x.2, f₂ x.2)) (𝓤 α)
    (Filter.comap (fun (p : (β × γ) × β × γ) ↦ (p.1.1, p.2.1)) (𝓤 β) ⊓
      Filter.comap (fun (p : (β × γ) × β × γ) ↦ (p.1.2, p.2.2)) (𝓤 γ))

Tactic:
tendsto_inf.2 ⟨tendsto_comap_iff.2 h₁, tendsto_comap_iff.2 h₂⟩

Premises used: Iff.mpr, Filter.tendsto_inf, Set.Mem, setOf, Filter.tendsto_comap_iff, And.intro
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f₁ : α → β
f₂ : α → γ
h₁ : UniformContinuous f₁
h₂ : UniformContinuous f₂
⊢ Tendsto (β := (β × γ) × β × γ) (fun (x : α × α) ↦ ((f₁ x.1, f₂ x.1), f₁ x.2, f₂ x.2)) (𝓤 α)
    (Filter.comap (fun (p : (β × γ) × β × γ) ↦ (p.1.1, p.2.1)) (𝓤 β) ⊓
      Filter.comap (fun (p : (β × γ) × β × γ) ↦ (p.1.2, p.2.2)) (𝓤 γ))

Tactic:
exact tendsto_inf.2 ⟨tendsto_comap_iff.2 h₁, tendsto_comap_iff.2 h₂⟩
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α × β → γ
h : UniformContinuous f
b : β
⊢ UniformContinuous.{ua, uc} (β := γ) fun (a : α) ↦ f (a, b)

Tactic:
h.comp (uniformContinuous_id.prodMk uniformContinuous_const)

Premises used: UniformContinuous.prodMk, uniformContinuous_id, uniformContinuous_const, UniformContinuous.comp
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α × β → γ
h : UniformContinuous f
a : α
⊢ UniformContinuous.{ub, uc} (β := γ) fun (b : β) ↦ f (a, b)

Tactic:
h.comp (uniformContinuous_const.prodMk uniformContinuous_id)

Premises used: UniformContinuous.prodMk, uniformContinuous_id, uniformContinuous_const, UniformContinuous.comp
-- 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 : β → δ
hf : UniformContinuous f
hg : UniformContinuous g
⊢ UniformContinuous (Prod.map f g)

Tactic:
(hf.comp uniformContinuous_fst).prodMk (hg.comp uniformContinuous_snd)

Premises used: UniformContinuous.prodMk, Prod.map, uniformContinuous_snd, UniformContinuous.comp, uniformContinuous_fst
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
⊢ UniformContinuous (α := α × β) Prod.swap

Tactic:
uniformContinuous_snd.prodMk uniformContinuous_fst

Premises used: UniformContinuous.prodMk, uniformContinuous_snd, uniformContinuous_fst, Prod.swap
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type u_2
β : Type u_3
u : UniformSpace α
v : UniformSpace β
⊢ Eq (α := TopologicalSpace (α × β)) toTopologicalSpace instTopologicalSpaceProd

Tactic:
rfl

Premises used: setOf, rfl
-- 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 : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
haveI : (this : UniformSpace α) → Prop
⊢ Prop

Tactic:
haveI := ua1
-- 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 : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
this : UniformSpace α
haveI : (this : UniformSpace β) → Prop
⊢ Prop

Tactic:
haveI := ub1
-- 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 : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
this_1 : UniformSpace α
this : UniformSpace β
⊢ Prop

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

Premises used: UniformContinuous, Prod.fst, Prod.snd
-- 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 : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
haveI : (this : UniformSpace α) → Prop
⊢ Prop

Tactic:
haveI := ua1 ⊓ ua2
-- 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 : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
this : UniformSpace α
haveI : (this : UniformSpace β) → Prop
⊢ Prop

Tactic:
haveI := ub1 ⊓ ub2
-- 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 : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
this_1 : UniformSpace α
this : UniformSpace β
⊢ Prop

Tactic:
exact UniformContinuous 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 : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
⊢ UniformContinuous.{u_2, u_2} (α := α) id

Tactic:
have ha := @UniformContinuous.inf_dom_left _ _ id ua1 ua2 ua1 (@uniformContinuous_id _ (id _))
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
ha : UniformContinuous.{u_2, u_2} (α := α) id
⊢ UniformContinuous.{u_3, u_3} (α := β) id

Tactic:
have hb := @UniformContinuous.inf_dom_left _ _ id ub1 ub2 ub1 (@uniformContinuous_id _ (id _))
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
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 _ _ _ _ (ua1 ⊓ ua2) (ub1 ⊓ ub2) ua1 ub1 _ _ ha hb
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
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 _) _ _ _ h h_unif_cont_id

Premises used: UniformContinuous.comp
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
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 _) _ _ _ h h_unif_cont_id

Premises used: UniformContinuous.comp
-- 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 : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
haveI : (this : UniformSpace α) → Prop
⊢ Prop

Tactic:
haveI := ua2
-- 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 : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
this : UniformSpace α
haveI : (this : UniformSpace β) → Prop
⊢ Prop

Tactic:
haveI := ub2
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
⊢ UniformContinuous.{u_2, u_2} (α := α) id

Tactic:
have ha := @UniformContinuous.inf_dom_right _ _ id ua1 ua2 ua2 (@uniformContinuous_id _ (id _))
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
ha : UniformContinuous.{u_2, u_2} (α := α) id
⊢ UniformContinuous.{u_3, u_3} (α := β) id

Tactic:
have hb := @UniformContinuous.inf_dom_right _ _ id ub1 ub2 ub2 (@uniformContinuous_id _ (id _))
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
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 _ _ _ _ (ua1 ⊓ ua2) (ub1 ⊓ ub2) ua2 ub2 _ _ ha hb
-- 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
haveI : (this : UniformSpace α) → Prop
⊢ Prop

Tactic:
haveI := sInf uas