awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
γ : Type u_3
ι : Type u_4
u : ι → UniformSpace γ
⊢ UniformFun.filter α γ (⨅ (i : ι), 𝓤 γ) = ⨅ (i : ι), 𝓤 (α →ᵤ γ)

Tactic:
(UniformFun.gc α γ).u_iInf

Premises used: Set.Mem, uniformity, setOf, GaloisConnection.u_iInf, UniformFun.filter, UniformFun.gc, FilterBasis.filter
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
γ : Type u_3
ι : Type u_4
u : ι → UniformSpace γ
⊢ UniformFun.filter α γ (⨅ (i : ι), 𝓤 γ) = ⨅ (i : ι), 𝓤 (α →ᵤ γ)

Tactic:
exact (UniformFun.gc α γ).u_iInf

Premises used: GaloisConnection.u_iInf, UniformFun.gc
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
γ : Type u_3
u₁ u₂ : UniformSpace γ
rw :
  Eq (α := UniformSpace (α →ᵤ γ)) (⨅ (i : Bool), uniformSpace α γ)
    (⨅ (b : Bool), bif b then uniformSpace α γ else uniformSpace α γ)
⊢ uniformSpace α γ = uniformSpace α γ ⊓ uniformSpace α γ

Tactic:
rw [inf_eq_iInf, inf_eq_iInf, UniformFun.iInf_eq]

Premises used: inf_eq_iInf, UniformFun.iInf_eq
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
γ : Type u_3
u₁ u₂ : UniformSpace γ
⊢ Eq (α := UniformSpace (α →ᵤ γ)) (⨅ (i : Bool), uniformSpace α γ)
    (⨅ (b : Bool), bif b then uniformSpace α γ else uniformSpace α γ)

Tactic:
iInf_congr fun i => ?_

Premises used: iInf_congr
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
γ : Type u_3
u₁ u₂ : UniformSpace γ
refine : ∀ (i : Bool), uniformSpace α γ = bif i then uniformSpace α γ else uniformSpace α γ
⊢ Eq (α := UniformSpace (α →ᵤ γ)) (⨅ (i : Bool), uniformSpace α γ)
    (⨅ (b : Bool), bif b then uniformSpace α γ else uniformSpace α γ)

Tactic:
refine iInf_congr fun i => ?_

Premises used: iInf_congr
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
γ : Type u_3
u₁ u₂ : UniformSpace γ
i : Bool
false : uniformSpace α γ = bif Bool.false then uniformSpace α γ else uniformSpace α γ
true : uniformSpace α γ = bif Bool.true then uniformSpace α γ else uniformSpace α γ
⊢ uniformSpace α γ = bif i then uniformSpace α γ else uniformSpace α γ

Tactic:
cases i
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
γ : Type u_3
u₁ u₂ : UniformSpace γ
⊢ uniformSpace α γ = bif false then uniformSpace α γ else uniformSpace α γ

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
γ : Type u_3
u₁ u₂ : UniformSpace γ
⊢ uniformSpace α γ = bif true then uniformSpace α γ else uniformSpace α γ

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
inst_1 : UniformSpace γ
f : γ → β
hf : IsUniformInducing f
⊢ IsUniformInducing (α := α →ᵤ γ) (β := α →ᵤ β)
    (Function.comp (β := α → β) (⇑ofFun : (a : α → β) → α →ᵤ β)
      ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑toFun : (a : α →ᵤ γ) → α → γ)))

Tactic:
⟨((UniformFun.hasBasis_uniformity _ _).comap _).eq_of_same_basis <|
    UniformFun.hasBasis_uniformity_of_basis _ _ (hf.basis_uniformity (𝓤 β).basis_sets)⟩

Premises used: UniformFun.hasBasis_uniformity, uniformity, UniformFun.hasBasis_uniformity_of_basis, Filter.HasBasis.comap, Filter.basis_sets, IsUniformInducing.mk, IsUniformInducing.basis_uniformity, Filter.HasBasis.eq_of_same_basis
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
f : γ → β
this : UniformSpace γ := UniformSpace.comap f inst
⊢ uniformSpace α γ = UniformSpace.comap (fun (x : α → γ) ↦ f ∘ x) (uniformSpace α β)

Tactic:
(UniformFun.postcomp_isUniformInducing (f := f) ⟨rfl⟩).comap_uniformSpace.symm

Premises used: IsUniformInducing.comap_uniformSpace, UniformFun.postcomp_isUniformInducing, UniformFun, IsUniformInducing.mk, Eq.symm, rfl
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
f : γ → β
this : UniformSpace γ := UniformSpace.comap f inst
⊢ uniformSpace α γ = UniformSpace.comap (fun (x : α → γ) ↦ f ∘ x) (uniformSpace α β)

Tactic:
exact (UniformFun.postcomp_isUniformInducing (f := f) ⟨rfl⟩).comap_uniformSpace.symm

Premises used: IsUniformInducing.comap_uniformSpace, UniformFun.postcomp_isUniformInducing, IsUniformInducing.mk, Eq.symm, rfl
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
inst_1 : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ UniformContinuous (α := α →ᵤ γ) (β := α →ᵤ β)
    (Function.comp (β := α → β) (⇑ofFun : (a : α → β) → α →ᵤ β)
      ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑toFun : (a : α →ᵤ γ) → α → γ)))

Tactic:
uniformContinuous_iff.mpr ?_

Premises used: Iff.mpr, uniformContinuous_iff
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
inst_1 : UniformSpace γ
f : γ → β
hf : UniformContinuous f
refine :
  uniformSpace α γ ≤
    UniformSpace.comap
      (Function.comp (β := α → β) (⇑ofFun : (a : α → β) → α →ᵤ β)
        ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑toFun : (a : α →ᵤ γ) → α → γ)))
      (uniformSpace α β)
⊢ UniformContinuous (α := α →ᵤ γ) (β := α →ᵤ β)
    (Function.comp (β := α → β) (⇑ofFun : (a : α → β) → α →ᵤ β)
      ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑toFun : (a : α →ᵤ γ) → α → γ)))

Tactic:
refine uniformContinuous_iff.mpr ?_

Premises used: Iff.mpr, uniformContinuous_iff
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
inst_1 : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ uniformSpace α γ ≤ uniformSpace α γ

Tactic:
UniformFun.mono (uniformContinuous_iff.mp hf)

Premises used: UniformFun.mono, uniformContinuous_iff, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
inst_1 : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ uniformSpace α γ = UniformSpace.comap (fun (x : α → γ) ↦ f ∘ x) (uniformSpace α β)

Tactic:
UniformFun.comap_eq

Premises used: UniformFun.comap_eq
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
inst_1 : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ uniformSpace α γ = UniformSpace.comap (fun (x : α → γ) ↦ f ∘ x) (uniformSpace α β)

Tactic:
exact UniformFun.comap_eq

Premises used: UniformFun.comap_eq
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
inst_1 : UniformSpace γ
f : γ → β
hf : UniformContinuous f
_ : uniformSpace α γ = UniformSpace.comap (fun (x : α → γ) ↦ f ∘ x) (uniformSpace α β)
⊢ uniformSpace α γ ≤
    UniformSpace.comap
      (Function.comp (β := α → β) (⇑ofFun : (a : α → β) → α →ᵤ β)
        ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑toFun : (a : α →ᵤ γ) → α → γ)))
      (uniformSpace α β)

Tactic:
calc
      𝒰(α, γ, _) ≤ 𝒰(α, γ, ‹UniformSpace β›.comap f) :=
        UniformFun.mono (uniformContinuous_iff.mp hf)
      _ = 𝒰(α, β, _).comap (f ∘ ·) := by exact UniformFun.comap_eq

Premises used: UniformFun.mono, Function.comp, UniformFun.uniformSpace, uniformContinuous_iff, Iff.mp, UniformSpace.comap
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
f : γ → α
rw :
  ∀ ib ∈ 𝓤 β,
    ∃ ia ∈ 𝓤 β,
      ∀ x ∈ UniformFun.gen α β ia,
        Membership.mem (α := (γ →ᵤ β) × (γ →ᵤ β)) (UniformFun.gen γ β ib)
          (((ofFun : (a : γ → β) → γ →ᵤ β) ((toFun : (a : α →ᵤ β) → α → β) x.1 ∘ f),
              (ofFun : (a : γ → β) → γ →ᵤ β) ((toFun : (a : α →ᵤ β) → α → β) x.2 ∘ f)) :
            (γ →ᵤ β) × (γ →ᵤ β))
⊢ UniformContinuous (β := γ →ᵤ β) fun (g : α →ᵤ β) ↦
    (ofFun : (a : γ → β) → γ →ᵤ β) ((toFun : (a : α →ᵤ β) → α → β) g ∘ f)

Tactic:
rw [UniformContinuous,
      (UniformFun.hasBasis_uniformity α β).tendsto_iff (UniformFun.hasBasis_uniformity γ β)]

Premises used: UniformContinuous, Filter.HasBasis.tendsto_iff, UniformFun.hasBasis_uniformity
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
f : γ → α
⊢ ∀ ib ∈ 𝓤 β,
    ∃ ia ∈ 𝓤 β,
      ∀ x ∈ UniformFun.gen α β ia,
        Membership.mem (α := (γ →ᵤ β) × (γ →ᵤ β)) (UniformFun.gen γ β ib)
          (((ofFun : (a : γ → β) → γ →ᵤ β) ((toFun : (a : α →ᵤ β) → α → β) x.1 ∘ f),
              (ofFun : (a : γ → β) → γ →ᵤ β) ((toFun : (a : α →ᵤ β) → α → β) x.2 ∘ f)) :
            (γ →ᵤ β) × (γ →ᵤ β))

Tactic:
fun U hU => ⟨U, hU, fun uv huv x => huv (f x)⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
f : γ → α
⊢ ∀ ib ∈ 𝓤 β,
    ∃ ia ∈ 𝓤 β,
      ∀ x ∈ UniformFun.gen α β ia,
        Membership.mem (α := (γ →ᵤ β) × (γ →ᵤ β)) (UniformFun.gen γ β ib)
          (((ofFun : (a : γ → β) → γ →ᵤ β) ((toFun : (a : α →ᵤ β) → α → β) x.1 ∘ f),
              (ofFun : (a : γ → β) → γ →ᵤ β) ((toFun : (a : α →ᵤ β) → α → β) x.2 ∘ f)) :
            (γ →ᵤ β) × (γ →ᵤ β))

Tactic:
exact fun U hU => ⟨U, hU, fun uv huv x => huv (f x)⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
rw : ∀ (i : α), UniformContinuous (β := β) fun (x : α →ᵤ β) ↦ (toFun : (a : α →ᵤ β) → α → β) x i
⊢ UniformContinuous (α := α →ᵤ β) (β := α → β) (⇑toFun : (a : α →ᵤ β) → α → β)

Tactic:
rw [uniformContinuous_pi]

Premises used: uniformContinuous_pi
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
x : α
⊢ UniformContinuous (β := β) fun (x_1 : α →ᵤ β) ↦ (toFun : (a : α →ᵤ β) → α → β) x_1 x

Tactic:
uniformContinuous_eval β x

Premises used: UniformFun.uniformContinuous_eval
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
x : α
⊢ UniformContinuous (β := β) fun (x_1 : α →ᵤ β) ↦ (toFun : (a : α →ᵤ β) → α → β) x_1 x

Tactic:
exact uniformContinuous_eval β x

Premises used: UniformFun.uniformContinuous_eval
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
inst_1 : T2Space β
⊢ T2Space (α →ᵤ β)

Tactic:
.of_injective_continuous toFun.injective UniformFun.uniformContinuous_toFun.continuous

Premises used: T2Space.of_injective_continuous, UniformFun.toFun, UniformContinuous.continuous, Equiv.injective, UniformFun.uniformContinuous_toFun
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
p : Filter ι
inst : UniformSpace β
F : ι → α →ᵤ β
f : α →ᵤ β
rw :
  (∀ i ∈ 𝓤 β, ∀ᶠ (x : ι) in p, Membership.mem (γ := Set (α →ᵤ β)) {g : α →ᵤ β | (f, g) ∈ UniformFun.gen α β i} (F x)) ↔
    ∀ u ∈ 𝓤 β,
      ∀ᶠ (n : ι) in p,
        ∀ (x : α),
          Membership.mem (α := β × β) u
            (((toFun : (a : α →ᵤ β) → α → β) f x, ((⇑toFun : (a : α →ᵤ β) → α → β) ∘ F) n x) : β × β)
⊢ Tendsto F p (𝓝 f) ↔
    TendstoUniformly.{u_1, u_2, u_4} (α := α) (β := β) ((⇑toFun : (a : α →ᵤ β) → α → β) ∘ F)
      ((toFun : (a : α →ᵤ β) → α → β) f) p

Tactic:
rw [(UniformFun.hasBasis_nhds α β f).tendsto_right_iff, TendstoUniformly]

Premises used: TendstoUniformly, Filter.HasBasis.tendsto_right_iff, UniformFun.hasBasis_nhds
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
p : Filter ι
inst : UniformSpace β
F : ι → α →ᵤ β
f : α →ᵤ β
⊢ (∀ i ∈ 𝓤 β, ∀ᶠ (x : ι) in p, Membership.mem (γ := Set (α →ᵤ β)) {g : α →ᵤ β | (f, g) ∈ UniformFun.gen α β i} (F x)) ↔
    ∀ u ∈ 𝓤 β,
      ∀ᶠ (n : ι) in p,
        ∀ (x : α),
          Membership.mem (α := β × β) u
            (((toFun : (a : α →ᵤ β) → α → β) f x, ((⇑toFun : (a : α →ᵤ β) → α → β) ∘ F) n x) : β × β)

Tactic:
simp only [mem_setOf, UniformFun.gen, Function.comp_def]

Premises used: UniformFun.gen, Set.mem_setOf, Function.comp_def
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
inst_1 : UniformSpace γ
comap_uniformity :
  Eq (α := Filter ((α →ᵤ β × γ) × (α →ᵤ β × γ)))
    (comap (β := ((α →ᵤ β) × (α →ᵤ γ)) × (α →ᵤ β) × (α →ᵤ γ))
      (fun (x : (α →ᵤ β × γ) × (α →ᵤ β × γ)) ↦
        ((Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ : (a : α →ᵤ β × γ) → (α →ᵤ β) × (α →ᵤ γ))
            x.1,
          (Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ : (a : α →ᵤ β × γ) → (α →ᵤ β) × (α →ᵤ γ))
            x.2))
      (𝓤 ((α →ᵤ β) × (α →ᵤ γ))))
    (𝓤 (α →ᵤ β × γ))
⊢ IsUniformInducing (α := α →ᵤ β × γ) (β := (α →ᵤ β) × (α →ᵤ γ))
    (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) : (a : α →ᵤ β × γ) → (α →ᵤ β) × (α →ᵤ γ))

Tactic:
constructor
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
inst_1 : UniformSpace γ
comap_uniformity :
  Eq (α := UniformSpace ((i : α) → β × γ))
    (UniformSpace.comap (β := ((i : α) → β) × ((i : α) → γ))
      (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
        (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ))
      instUniformSpaceProd)
    (uniformSpace α (β × γ))
⊢ Eq (α := Filter (((i : α) → β × γ) × ((i : α) → β × γ))) (𝓤 ((i : α) → β × γ)) (𝓤 (α → β × γ))

Tactic:
congr
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
inst_1 : UniformSpace γ
comap_uniformity :
  Eq (α := UniformSpace ((i : α) → β × γ))
    (UniformSpace.comap
        (Function.comp (β := ((i : α) → β) × ((i : α) → γ)) Prod.fst
          (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
            (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ)))
        (uniformSpace α β) ⊓
      UniformSpace.comap
        (Function.comp (β := ((i : α) → β) × ((i : α) → γ)) Prod.snd
          (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
            (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ)))
        (uniformSpace α γ))
    (uniformSpace α (β × γ))
⊢ Eq (α := UniformSpace ((i : α) → β × γ))
    (UniformSpace.comap
      (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
        (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ))
      (UniformSpace.comap Prod.fst (uniformSpace α β) ⊓ UniformSpace.comap Prod.snd (uniformSpace α γ)))
    (uniformSpace α (β × γ))

Tactic:
rw [UniformSpace.comap_inf, ← UniformSpace.comap_comap, ← UniformSpace.comap_comap]

Premises used: UniformSpace.comap_inf, UniformSpace.comap_comap
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
inst_1 : UniformSpace γ
⊢ Eq (α := UniformSpace (α →ᵤ β × γ)) (uniformSpace α (β × γ) ⊓ uniformSpace α (β × γ)) (uniformSpace α (β × γ))

Tactic:
have := (@UniformFun.inf_eq α (β × γ)
      (UniformSpace.comap Prod.fst ‹_›) (UniformSpace.comap Prod.snd ‹_›)).symm
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
inst_1 : UniformSpace γ
this : Eq (α := UniformSpace (α →ᵤ β × γ)) (uniformSpace α (β × γ) ⊓ uniformSpace α (β × γ)) (uniformSpace α (β × γ))
comap_uniformity :
  ∀
    (this :
      Eq (α := UniformSpace (α →ᵤ β × γ))
        (UniformSpace.comap (fun (x : α → β × γ) ↦ Prod.fst ∘ x) (uniformSpace α β) ⊓ uniformSpace α (β × γ))
        (uniformSpace α (β × γ))),
    Eq (α := UniformSpace ((i : α) → β × γ))
      (UniformSpace.comap
          (Function.comp (β := ((i : α) → β) × ((i : α) → γ)) Prod.fst
            (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
              (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ)))
          (uniformSpace α β) ⊓
        UniformSpace.comap
          (Function.comp (β := ((i : α) → β) × ((i : α) → γ)) Prod.snd
            (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
              (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ)))
          (uniformSpace α γ))
      (uniformSpace α (β × γ))
comap_uniformity₁ comap_uniformity₂ comap_uniformity₃ comap_uniformity₄ :
  ∀
    (this :
      Eq (α := UniformSpace (α →ᵤ β × γ))
        (UniformSpace.comap (fun (x : α → β × γ) ↦ Prod.fst ∘ x) (uniformSpace α β) ⊓
          UniformSpace.comap (fun (x : α → β × γ) ↦ Prod.snd ∘ x) (uniformSpace α γ))
        (uniformSpace α (β × γ))),
    Eq (α := UniformSpace ((i : α) → β × γ))
      (UniformSpace.comap
          (Function.comp (β := ((i : α) → β) × ((i : α) → γ)) Prod.fst
            (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
              (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ)))
          (uniformSpace α β) ⊓
        UniformSpace.comap
          (Function.comp (β := ((i : α) → β) × ((i : α) → γ)) Prod.snd
            (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
              (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ)))
          (uniformSpace α γ))
      (uniformSpace α (β × γ))
⊢ Eq (α := UniformSpace ((i : α) → β × γ))
    (UniformSpace.comap
        (Function.comp (β := ((i : α) → β) × ((i : α) → γ)) Prod.fst
          (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
            (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ)))
        (uniformSpace α β) ⊓
      UniformSpace.comap
        (Function.comp (β := ((i : α) → β) × ((i : α) → γ)) Prod.snd
          (⇑(Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ) :
            (a : (i : α) → β × γ) → ((i : α) → β) × ((i : α) → γ)))
        (uniformSpace α γ))
    (uniformSpace α (β × γ))

Tactic:
rwa [UniformFun.comap_eq, UniformFun.comap_eq] at this

Premises used: UniformFun.comap_eq
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
⊢ IsUniformInducing (α := α →ᵤ (i : ι) → δ i) (β := (i : ι) → (fun (i : ι) ↦ α → δ i) i)
    (⇑(Equiv.piComm fun (a : α) ↦ δ) : (a : α →ᵤ (i : ι) → δ i) → (i : ι) → (fun (i : ι) ↦ α → δ i) i)

Tactic:
@IsUniformInducing.mk ?_ ?_ ?_ ?_ ?_ ?_

Premises used: IsUniformInducing.mk
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
refine :
  Eq (α := Filter ((α →ᵤ (i : ι) → δ i) × (α →ᵤ (i : ι) → δ i)))
    (comap (β := ((i : ι) → (fun (i : ι) ↦ α → δ i) i) × ((i : ι) → (fun (i : ι) ↦ α → δ i) i))
      (fun (x : (α →ᵤ (i : ι) → δ i) × (α →ᵤ (i : ι) → δ i)) ↦
        ((Equiv.piComm fun (a : α) ↦ δ : (a : α →ᵤ (i : ι) → δ i) → (i : ι) → (fun (i : ι) ↦ α → δ i) i) x.1,
          (Equiv.piComm fun (a : α) ↦ δ : (a : α →ᵤ (i : ι) → δ i) → (i : ι) → (fun (i : ι) ↦ α → δ i) i) x.2))
      (𝓤 ((i : ι) → (fun (i : ι) ↦ α → δ i) i)))
    (𝓤 (α →ᵤ (i : ι) → δ i))
⊢ IsUniformInducing (α := α →ᵤ (i : ι) → δ i) (β := (i : ι) → (fun (i : ι) ↦ α → δ i) i)
    (⇑(Equiv.piComm fun (a : α) ↦ δ) : (a : α →ᵤ (i : ι) → δ i) → (i : ι) → (fun (i : ι) ↦ α → δ i) i)

Tactic:
refine @IsUniformInducing.mk ?_ ?_ ?_ ?_ ?_ ?_

Premises used: IsUniformInducing.mk
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
change :
  Eq (α := Filter (((x : α) → (y : ι) → δ y) × ((x : α) → (y : ι) → δ y)))
    (comap (Prod.map (Function.swap (φ := fun (a : α) ↦ δ)) (Function.swap (φ := fun (a : α) ↦ δ)))
      (𝓤 ((i : ι) → (fun (i : ι) ↦ α → δ i) i)))
    (𝓤 (α →ᵤ (i : ι) → δ i))
⊢ Eq (α := Filter ((α →ᵤ (i : ι) → δ i) × (α →ᵤ (i : ι) → δ i)))
    (comap (β := ((i : ι) → (fun (i : ι) ↦ α → δ i) i) × ((i : ι) → (fun (i : ι) ↦ α → δ i) i))
      (fun (x : (α →ᵤ (i : ι) → δ i) × (α →ᵤ (i : ι) → δ i)) ↦
        ((Equiv.piComm fun (a : α) ↦ δ : (a : α →ᵤ (i : ι) → δ i) → (i : ι) → (fun (i : ι) ↦ α → δ i) i) x.1,
          (Equiv.piComm fun (a : α) ↦ δ : (a : α →ᵤ (i : ι) → δ i) → (i : ι) → (fun (i : ι) ↦ α → δ i) i) x.2))
      (𝓤 ((i : ι) → (fun (i : ι) ↦ α → δ i) i)))
    (𝓤 (α →ᵤ (i : ι) → δ i))

Tactic:
change comap (Prod.map Function.swap Function.swap) _ = _

Premises used: Function.swap, Prod.map, Filter.comap
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
h :
  Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
    (UniformSpace.comap (Function.swap (φ := fun (a : α) ↦ δ)) (Pi.uniformSpace fun (i : ι) ↦ α → δ i))
    (uniformSpace α ((i : ι) → δ i))
⊢ Eq (α := Filter (((x : α) → (y : ι) → δ y) × ((x : α) → (y : ι) → δ y))) (𝓤 ((x : α) → (y : ι) → δ y))
    (𝓤 (α →ᵤ (i : ι) → δ i))

Tactic:
congr
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
h :
  Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
    (⨅ (i : ι),
      UniformSpace.comap (Function.swap (φ := fun (a : α) ↦ δ))
        (UniformSpace.comap (Function.eval (β := fun (i : ι) ↦ α → δ i) i)
          ((fun (i : ι) ↦ (uniformSpace α (δ i) : UniformSpace (UniformFun.{u_1, u_5} α (δ i)))) i)))
    (⨅ (i : ι), uniformSpace α ((i : ι) → δ i))
⊢ Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
    (UniformSpace.comap (Function.swap (φ := fun (a : α) ↦ δ))
      (UniformSpace.ofCoreEq
        (UniformSpace.toCore
          (⨅ (i : ι),
            UniformSpace.comap (Function.eval (β := fun (i : ι) ↦ α → δ i) i)
              ((fun (i : ι) ↦ (uniformSpace α (δ i) : UniformSpace (UniformFun.{u_1, u_5} α (δ i)))) i)))
        (Pi.topologicalSpace (Y := fun (i : ι) ↦ α → δ i)) ⋯))
    (uniformSpace α ((i : ι) → δ i))

Tactic:
rw [UniformSpace.ofCoreEq_toCore, UniformSpace.ofCoreEq_toCore,
        UniformSpace.comap_iInf, UniformFun.iInf_eq]

Premises used: UniformSpace.ofCoreEq_toCore, UniformSpace.comap_iInf, UniformFun.iInf_eq
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
⊢ Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
    (⨅ (i : ι),
      UniformSpace.comap (Function.swap (φ := fun (a : α) ↦ δ))
        (UniformSpace.comap (Function.eval (β := fun (i : ι) ↦ α → δ i) i)
          ((fun (i : ι) ↦ (uniformSpace α (δ i) : UniformSpace (UniformFun.{u_1, u_5} α (δ i)))) i)))
    (⨅ (i : ι), uniformSpace α ((i : ι) → δ i))

Tactic:
iInf_congr fun i => ?_

Premises used: iInf_congr, UniformFun