awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
V : Set (β × β)
hV : V ∈ 𝓤 β
s : Set α
hs : s ∈ 𝔖
T : Set (Set α)
hT𝔗 : T ⊆ 𝔗
hT : T.Finite
hsT : s ⊆ ⋃₀ T
refine :
  ∀ (f : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β))
    (hf : Membership.mem (γ := Set ((α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β))) (⋂ i ∈ T, UniformOnFun.gen 𝔗 i V) f),
    Membership.mem (γ := Set ((α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β)))
      {x : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β) |
        (Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x.1,
            Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)
              x.2) ∈
          UniformOnFun.gen 𝔖 s V}
      f
⊢ ∃ (I : Set (Set α)),
    I.Finite ∧
      (∀ i ∈ I, i ∈ 𝔗) ∧
        Subset (α := Set ((α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β))) (⋂ i ∈ I, UniformOnFun.gen 𝔗 i V)
          {x : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β) |
            (Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)
                  x.1,
                Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)
                  x.2) ∈
              UniformOnFun.gen 𝔖 s V}

Tactic:
refine ⟨T, hT, hT𝔗, fun f hf ↦ ?_⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
V : Set (β × β)
hV : V ∈ 𝓤 β
s : Set α
hs : s ∈ 𝔖
T : Set (Set α)
hT𝔗 : T ⊆ 𝔗
hT : T.Finite
hsT : s ⊆ ⋃₀ T
f : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β)
hf : Membership.mem (γ := Set ((α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β))) (⋂ i ∈ T, UniformOnFun.gen 𝔗 i V) f
simp :
  ∀
    (hf :
      ∀ (i : Set α) (i_1 : i ∈ T),
        ∀ x ∈ i,
          Membership.mem (α := β × β) V
            (((toFun 𝔗 : (a : α →ᵤ[𝔗] β) → α → β) f.1 x, (toFun 𝔗 : (a : α →ᵤ[𝔗] β) → α → β) f.2 x) : β × β)),
    ∀ x ∈ s,
      Membership.mem (α := β × β) V
        (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β)
              ((ofFun 𝔗 : (a : α → β) → α →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f.1) : α →ᵤ[𝔗] β) x,
            (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β)
              ((ofFun 𝔗 : (a : α → β) → α →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f.2) : α →ᵤ[𝔗] β) x) :
          β × β)
⊢ Membership.mem (γ := Set ((α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β)))
    {x : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β) |
      (Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x.1,
          Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)
            x.2) ∈
        UniformOnFun.gen 𝔖 s V}
    f

Tactic:
simp only [UniformOnFun.gen, Set.mem_iInter, Set.mem_setOf_eq, Function.comp_apply] at hf ⊢

Premises used: UniformOnFun.gen, Set.mem_setOf_eq, Set.mem_iInter, Function.comp_apply
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
V : Set (β × β)
hV : V ∈ 𝓤 β
s : Set α
hs : s ∈ 𝔖
T : Set (Set α)
hT𝔗 : T ⊆ 𝔗
hT : T.Finite
hsT : s ⊆ ⋃₀ T
f : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β)
hf :
  ∀ (i : Set α) (i_1 : i ∈ T),
    ∀ x ∈ i,
      Membership.mem (α := β × β) V
        (((toFun 𝔗 : (a : α →ᵤ[𝔗] β) → α → β) f.1 x, (toFun 𝔗 : (a : α →ᵤ[𝔗] β) → α → β) f.2 x) : β × β)
x : α
hx : x ∈ s
obtain :
  ∀ (t : Set α) (ht : t ∈ T) (hxt : x ∈ t),
    Membership.mem (α := β × β) V
      (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β)
            ((ofFun 𝔗 : (a : α → β) → α →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f.1) : α →ᵤ[𝔗] β) x,
          (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β)
            ((ofFun 𝔗 : (a : α → β) → α →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f.2) : α →ᵤ[𝔗] β) x) :
        β × β)
⊢ Membership.mem (α := β × β) V
    (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β)
          ((ofFun 𝔗 : (a : α → β) → α →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f.1) : α →ᵤ[𝔗] β) x,
        (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β)
          ((ofFun 𝔗 : (a : α → β) → α →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f.2) : α →ᵤ[𝔗] β) x) :
      β × β)

Tactic:
obtain ⟨t, ht, hxt⟩ := Set.mem_sUnion.mp <| hsT hx

Premises used: Iff.mp, Set.mem_sUnion
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
V : Set (β × β)
hV : V ∈ 𝓤 β
s : Set α
hs : s ∈ 𝔖
T : Set (Set α)
hT𝔗 : T ⊆ 𝔗
hT : T.Finite
hsT : s ⊆ ⋃₀ T
f : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β)
hf :
  ∀ (i : Set α) (i_1 : i ∈ T),
    ∀ x ∈ i,
      Membership.mem (α := β × β) V
        (((toFun 𝔗 : (a : α →ᵤ[𝔗] β) → α → β) f.1 x, (toFun 𝔗 : (a : α →ᵤ[𝔗] β) → α → β) f.2 x) : β × β)
x : α
hx : x ∈ s
t : Set α
ht : t ∈ T
hxt : x ∈ t
⊢ Membership.mem (α := β × β) V
    (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β)
          ((ofFun 𝔗 : (a : α → β) → α →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f.1) : α →ᵤ[𝔗] β) x,
        (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β)
          ((ofFun 𝔗 : (a : α → β) → α →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f.2) : α →ᵤ[𝔗] β) x) :
      β × β)

Tactic:
hf t ht x hxt

Premises used: Set.Mem
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
V : Set (β × β)
hV : V ∈ 𝓤 β
s : Set α
hs : s ∈ 𝔖
T : Set (Set α)
hT𝔗 : T ⊆ 𝔗
hT : T.Finite
hsT : s ⊆ ⋃₀ T
f : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β)
hf :
  ∀ (i : Set α) (i_1 : i ∈ T),
    ∀ x ∈ i,
      Membership.mem (α := β × β) V
        (((toFun 𝔗 : (a : α →ᵤ[𝔗] β) → α → β) f.1 x, (toFun 𝔗 : (a : α →ᵤ[𝔗] β) → α → β) f.2 x) : β × β)
x : α
hx : x ∈ s
t : Set α
ht : t ∈ T
hxt : x ∈ t
⊢ Membership.mem (α := β × β) V
    (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β)
          ((ofFun 𝔗 : (a : α → β) → α →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f.1) : α →ᵤ[𝔗] β) x,
        (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β)
          ((ofFun 𝔗 : (a : α → β) → α →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f.2) : α →ᵤ[𝔗] β) x) :
      β × β)

Tactic:
exact hf t ht x hxt
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
γ : Type u_3
u₁ u₂ : UniformSpace γ
hu : u₁ ≤ u₂
𝔖₁ 𝔖₂ : Set (Set α)
h𝔖 : 𝔖₂ ⊆ 𝔖₁
⊢ uniformSpace α γ 𝔖₁ ≤ uniformSpace α γ 𝔖₂

Tactic:
calc
    𝒱(α, γ, 𝔖₁, u₁) ≤ 𝒱(α, γ, 𝔖₂, u₁) := iInf_le_iInf_of_subset h𝔖
    _ ≤ 𝒱(α, γ, 𝔖₂, u₂) := iInf₂_mono fun _i _hi => UniformSpace.comap_mono <| UniformFun.mono hu

Premises used: Trans.trans, UniformFun.mono, UniformSpace.comap_mono, iInf₂_mono, iInf_le_iInf_of_subset
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : UniformSpace β
𝔖 : Set (Set α)
x : α
hxs : x ∈ s
hs : s ∈ 𝔖
⊢ UniformContinuous (α := α →ᵤ[𝔖] β) (β := β)
    (Function.comp (β := (x : α) → β) (Function.eval (β := fun (a : α) ↦ β) x) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
      (α →ᵤ[𝔖] β) → β)

Tactic:
(UniformFun.uniformContinuous_eval β (⟨x, hxs⟩ : s)).comp
    (UniformOnFun.uniformContinuous_restrict α β 𝔖 hs)

Premises used: Subtype.mk, UniformContinuous.comp, UniformOnFun.uniformContinuous_restrict, UniformFun.uniformContinuous_eval, Set.restrict
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
x : α
hx : x ∈ ⋃₀ 𝔖
⊢ UniformContinuous (α := α →ᵤ[𝔖] β) (β := β)
    (Function.comp (β := (x : α) → β) (Function.eval (β := fun (a : α) ↦ β) x) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
      (α →ᵤ[𝔖] β) → β)

Tactic:
let ⟨_s, hs, hxs⟩ := hx
  uniformContinuous_eval_of_mem _ _ hxs hs

Premises used: UniformContinuous, Function.comp, Function.eval, UniformOnFun.toFun, _private.0.UniformOnFun.uniformContinuous_eval_of_mem_sUnion.match_1, UniformOnFun.uniformContinuous_eval_of_mem, DFunLike.coe
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
h : ⋃₀ 𝔖 = univ
x : α
⊢ UniformContinuous (α := α →ᵤ[𝔖] β) (β := β)
    (Function.comp (β := (x : α) → β) (Function.eval (β := fun (a : α) ↦ β) x) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
      (α →ᵤ[𝔖] β) → β)

Tactic:
uniformContinuous_eval_of_mem_sUnion _ _ <| h.symm ▸ mem_univ _

Premises used: Eq.rec, UniformOnFun.uniformContinuous_eval_of_mem_sUnion, Set.mem_univ, Eq.symm
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
γ : Type u_3
ι : Type u_4
𝔖 : Set (Set α)
u : ι → UniformSpace γ
simp_rw :
  Eq (α := UniformSpace (α →ᵤ[𝔖] γ))
    (⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        UniformSpace.comap (β := UniformFun.{u_1, u_3} (↑s : Type u_1) γ)
          (Function.comp (β := (↑s : Type u_1) → γ)
            ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → γ) → UniformFun.{u_1, u_3} (↑s : Type u_1) γ) :
              (a : (↑s : Type u_1) → γ) → UniformFun.{u_1, u_3} (↑s : Type u_1) γ)
            (Function.comp (β := α → γ) (s.restrict (π := fun (a : α) ↦ γ)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ) :
              (α →ᵤ[𝔖] γ) → (↑s : Type u_1) → γ))
          (UniformFun.uniformSpace (↑s : Type u_1) γ))
    (⨅ (i : ι),
      ⨅ s ∈ 𝔖,
        UniformSpace.comap (β := UniformFun.{u_1, u_3} (↑s : Type u_1) γ)
          (Function.comp (β := (↑s : Type u_1) → γ)
            ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → γ) → UniformFun.{u_1, u_3} (↑s : Type u_1) γ) :
              (a : (↑s : Type u_1) → γ) → UniformFun.{u_1, u_3} (↑s : Type u_1) γ)
            (Function.comp (β := α → γ) (s.restrict (π := fun (a : α) ↦ γ)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ) :
              (α →ᵤ[𝔖] γ) → (↑s : Type u_1) → γ))
          (UniformFun.uniformSpace (↑s : Type u_1) γ))
⊢ uniformSpace α γ 𝔖 = ⨅ (i : ι), uniformSpace α γ 𝔖

Tactic:
simp_rw [UniformOnFun.uniformSpace, UniformFun.iInf_eq, UniformSpace.comap_iInf]

Premises used: UniformOnFun.uniformSpace, UniformSpace.comap_iInf, UniformFun.iInf_eq
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
γ : Type u_3
ι : Type u_4
𝔖 : Set (Set α)
u : ι → UniformSpace γ
rw :
  Eq (α := UniformSpace (α →ᵤ[𝔖] γ))
    (⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        UniformSpace.comap (β := UniformFun.{u_1, u_3} (↑s : Type u_1) γ)
          (Function.comp (β := (↑s : Type u_1) → γ)
            ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → γ) → UniformFun.{u_1, u_3} (↑s : Type u_1) γ) :
              (a : (↑s : Type u_1) → γ) → UniformFun.{u_1, u_3} (↑s : Type u_1) γ)
            (Function.comp (β := α → γ) (s.restrict (π := fun (a : α) ↦ γ)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ) :
              (α →ᵤ[𝔖] γ) → (↑s : Type u_1) → γ))
          (UniformFun.uniformSpace (↑s : Type u_1) γ))
    (⨅ (j : Set α),
      ⨅ (i : ι),
        ⨅ (_ : j ∈ 𝔖),
          UniformSpace.comap (β := UniformFun.{u_1, u_3} (↑j : Type u_1) γ)
            (Function.comp (β := (↑j : Type u_1) → γ)
              ((⇑UniformFun.ofFun : (a : (↑j : Type u_1) → γ) → UniformFun.{u_1, u_3} (↑j : Type u_1) γ) :
                (a : (↑j : Type u_1) → γ) → UniformFun.{u_1, u_3} (↑j : Type u_1) γ)
              (Function.comp (β := α → γ) (j.restrict (π := fun (a : α) ↦ γ)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ) :
                (α →ᵤ[𝔖] γ) → (↑j : Type u_1) → γ))
            (UniformFun.uniformSpace (↑j : Type u_1) γ))
⊢ Eq (α := UniformSpace (α →ᵤ[𝔖] γ))
    (⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        UniformSpace.comap (β := UniformFun.{u_1, u_3} (↑s : Type u_1) γ)
          (Function.comp (β := (↑s : Type u_1) → γ)
            ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → γ) → UniformFun.{u_1, u_3} (↑s : Type u_1) γ) :
              (a : (↑s : Type u_1) → γ) → UniformFun.{u_1, u_3} (↑s : Type u_1) γ)
            (Function.comp (β := α → γ) (s.restrict (π := fun (a : α) ↦ γ)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ) :
              (α →ᵤ[𝔖] γ) → (↑s : Type u_1) → γ))
          (UniformFun.uniformSpace (↑s : Type u_1) γ))
    (⨅ (i : ι),
      ⨅ s ∈ 𝔖,
        UniformSpace.comap (β := UniformFun.{u_1, u_3} (↑s : Type u_1) γ)
          (Function.comp (β := (↑s : Type u_1) → γ)
            ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → γ) → UniformFun.{u_1, u_3} (↑s : Type u_1) γ) :
              (a : (↑s : Type u_1) → γ) → UniformFun.{u_1, u_3} (↑s : Type u_1) γ)
            (Function.comp (β := α → γ) (s.restrict (π := fun (a : α) ↦ γ)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ) :
              (α →ᵤ[𝔖] γ) → (↑s : Type u_1) → γ))
          (UniformFun.uniformSpace (↑s : Type u_1) γ))

Tactic:
rw [iInf_comm]

Premises used: iInf_comm
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
γ : Type u_3
ι : Type u_4
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ Eq (α := UniformSpace (α →ᵤ[𝔖] γ))
    (⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        UniformSpace.comap (β := UniformFun.{u_1, u_3} (↑s : Type u_1) γ)
          (Function.comp (β := (↑s : Type u_1) → γ)
            ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → γ) → UniformFun.{u_1, u_3} (↑s : Type u_1) γ) :
              (a : (↑s : Type u_1) → γ) → UniformFun.{u_1, u_3} (↑s : Type u_1) γ)
            (Function.comp (β := α → γ) (s.restrict (π := fun (a : α) ↦ γ)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ) :
              (α →ᵤ[𝔖] γ) → (↑s : Type u_1) → γ))
          (UniformFun.uniformSpace (↑s : Type u_1) γ))
    (⨅ (j : Set α),
      ⨅ (i : ι),
        ⨅ (_ : j ∈ 𝔖),
          UniformSpace.comap (β := UniformFun.{u_1, u_3} (↑j : Type u_1) γ)
            (Function.comp (β := (↑j : Type u_1) → γ)
              ((⇑UniformFun.ofFun : (a : (↑j : Type u_1) → γ) → UniformFun.{u_1, u_3} (↑j : Type u_1) γ) :
                (a : (↑j : Type u_1) → γ) → UniformFun.{u_1, u_3} (↑j : Type u_1) γ)
              (Function.comp (β := α → γ) (j.restrict (π := fun (a : α) ↦ γ)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ) :
                (α →ᵤ[𝔖] γ) → (↑j : Type u_1) → γ))
            (UniformFun.uniformSpace (↑j : Type u_1) γ))

Tactic:
iInf_congr fun s => iInf_comm

Premises used: iInf_congr, iInf_comm
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
γ : Type u_3
ι : Type u_4
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ Eq (α := UniformSpace (α →ᵤ[𝔖] γ))
    (⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        UniformSpace.comap (β := UniformFun.{u_1, u_3} (↑s : Type u_1) γ)
          (Function.comp (β := (↑s : Type u_1) → γ)
            ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → γ) → UniformFun.{u_1, u_3} (↑s : Type u_1) γ) :
              (a : (↑s : Type u_1) → γ) → UniformFun.{u_1, u_3} (↑s : Type u_1) γ)
            (Function.comp (β := α → γ) (s.restrict (π := fun (a : α) ↦ γ)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ) :
              (α →ᵤ[𝔖] γ) → (↑s : Type u_1) → γ))
          (UniformFun.uniformSpace (↑s : Type u_1) γ))
    (⨅ (j : Set α),
      ⨅ (i : ι),
        ⨅ (_ : j ∈ 𝔖),
          UniformSpace.comap (β := UniformFun.{u_1, u_3} (↑j : Type u_1) γ)
            (Function.comp (β := (↑j : Type u_1) → γ)
              ((⇑UniformFun.ofFun : (a : (↑j : Type u_1) → γ) → UniformFun.{u_1, u_3} (↑j : Type u_1) γ) :
                (a : (↑j : Type u_1) → γ) → UniformFun.{u_1, u_3} (↑j : Type u_1) γ)
              (Function.comp (β := α → γ) (j.restrict (π := fun (a : α) ↦ γ)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ) :
                (α →ᵤ[𝔖] γ) → (↑j : Type u_1) → γ))
            (UniformFun.uniformSpace (↑j : Type u_1) γ))

Tactic:
exact iInf_congr fun s => iInf_comm

Premises used: iInf_congr, iInf_comm
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
γ : Type u_3
𝔖 : Set (Set α)
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, UniformOnFun.iInf_eq]

Premises used: inf_eq_iInf, UniformOnFun.iInf_eq
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
γ : Type u_3
𝔖 : Set (Set α)
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
𝔖 : Set (Set α)
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
𝔖 : Set (Set α)
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
𝔖 : Set (Set α)
u₁ u₂ : UniformSpace γ
⊢ uniformSpace α γ 𝔖 = bif false then uniformSpace α γ 𝔖 else uniformSpace α γ 𝔖

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
γ : Type u_3
𝔖 : Set (Set α)
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 β
𝔖 : Set (Set α)
f : γ → β
simp_rw :
  Eq (α := UniformSpace (α →ᵤ[𝔖] γ))
    (⨅ s ∈ 𝔖,
      UniformSpace.comap (β := (↑s : Type u_1) → β)
        ((fun (x : (↑s : Type u_1) → γ) ↦ f ∘ x) ∘
          Function.comp (β := (↑s : Type u_1) → γ)
            ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → γ) → UniformFun.{u_1, u_3} (↑s : Type u_1) γ) :
              (a : (↑s : Type u_1) → γ) → UniformFun.{u_1, u_3} (↑s : Type u_1) γ)
            (Function.comp (β := α → γ) (s.restrict (π := fun (a : α) ↦ γ)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ) :
              (α →ᵤ[𝔖] γ) → (↑s : Type u_1) → γ))
        (UniformFun.uniformSpace (↑s : Type u_1) β))
    (⨅ i ∈ 𝔖,
      UniformSpace.comap (β := UniformFun.{u_1, u_2} (↑i : Type u_1) β)
        (Function.comp (β := α → β)
          (Function.comp (β := (↑i : Type u_1) → β)
            ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
              (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
            (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
              (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β))
          fun (x : α → γ) ↦ f ∘ x)
        (UniformFun.uniformSpace (↑i : Type u_1) β))
⊢ uniformSpace α γ 𝔖 = UniformSpace.comap (fun (x : α → γ) ↦ f ∘ x) (uniformSpace α β 𝔖)

Tactic:
simp_rw [UniformOnFun.uniformSpace, UniformSpace.comap_iInf, UniformFun.comap_eq, ←
    UniformSpace.comap_comap]

Premises used: UniformOnFun.uniformSpace, UniformSpace.comap_comap, UniformSpace.comap_iInf, UniformFun.comap_eq
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
𝔖 : Set (Set α)
f : γ → β
⊢ Eq (α := UniformSpace (α →ᵤ[𝔖] γ))
    (⨅ s ∈ 𝔖,
      UniformSpace.comap (β := (↑s : Type u_1) → β)
        ((fun (x : (↑s : Type u_1) → γ) ↦ f ∘ x) ∘
          Function.comp (β := (↑s : Type u_1) → γ)
            ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → γ) → UniformFun.{u_1, u_3} (↑s : Type u_1) γ) :
              (a : (↑s : Type u_1) → γ) → UniformFun.{u_1, u_3} (↑s : Type u_1) γ)
            (Function.comp (β := α → γ) (s.restrict (π := fun (a : α) ↦ γ)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ) :
              (α →ᵤ[𝔖] γ) → (↑s : Type u_1) → γ))
        (UniformFun.uniformSpace (↑s : Type u_1) β))
    (⨅ i ∈ 𝔖,
      UniformSpace.comap (β := UniformFun.{u_1, u_2} (↑i : Type u_1) β)
        (Function.comp (β := α → β)
          (Function.comp (β := (↑i : Type u_1) → β)
            ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
              (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
            (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
              (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β))
          fun (x : α → γ) ↦ f ∘ x)
        (UniformFun.uniformSpace (↑i : Type u_1) β))

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : UniformSpace γ
f : γ → β
hf : UniformContinuous f
rw :
  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:
rw [uniformContinuous_iff]

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

Tactic:
(UniformOnFun.mono (uniformContinuous_iff.mp hf) subset_rfl).trans_eq UniformOnFun.comap_eq

Premises used: UniformOnFun.mono, LE.le.trans_eq, uniformContinuous_iff, Iff.mp, subset_rfl, UniformOnFun.comap_eq
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ uniformSpace α γ 𝔖 ≤
    UniformSpace.comap
      (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β)
        ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ)))
      (uniformSpace α β 𝔖)

Tactic:
exact (UniformOnFun.mono (uniformContinuous_iff.mp hf) subset_rfl).trans_eq UniformOnFun.comap_eq

Premises used: UniformOnFun.mono, LE.le.trans_eq, uniformContinuous_iff, Iff.mp, subset_rfl, UniformOnFun.comap_eq
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : UniformSpace γ
f : γ → β
hf : IsUniformInducing f
comap_uniformity :
  Eq (α := Filter ((α →ᵤ[𝔖] γ) × (α →ᵤ[𝔖] γ)))
    (comap (β := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))
      (fun (x : (α →ᵤ[𝔖] γ) × (α →ᵤ[𝔖] γ)) ↦
        (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β)
            ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ)) x.1,
          Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β)
            ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ)) x.2))
      (𝓤 (α →ᵤ[𝔖] β)))
    (𝓤 (α →ᵤ[𝔖] γ))
⊢ IsUniformInducing (α := α →ᵤ[𝔖] γ) (β := α →ᵤ[𝔖] β)
    (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β)
      ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ)))

Tactic:
constructor
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : UniformSpace γ
f : γ → β
hf : IsUniformInducing f
⊢ comap (Prod.map f f) (𝓤 β) = 𝓤 γ

Tactic:
replace hf : (𝓤 β).comap (Prod.map f f) = _ := hf.comap_uniformity
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : UniformSpace γ
f : γ → β
hf : comap (Prod.map f f) (𝓤 β) = 𝓤 γ
⊢ 𝓤 γ = 𝓤 γ

Tactic:
rw [← uniformity_comap] at hf ⊢

Premises used: uniformity_comap