awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
h : univ ∈ 𝔖
U : Set (β × β)
hU : U ∈ 𝓤 β
⊢ ∀ᶠ (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) in 𝓤 (α →ᵤ[𝔖] β),
    Membership.mem (α := (α →ᵤ β) × (α →ᵤ β)) (UniformFun.gen α β U)
      (((UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.1),
          (UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.2)) :
        (α →ᵤ β) × (α →ᵤ β))
have h₁ : ∀ (a : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)),
  Membership.mem (γ := Set ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
    {x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) |
      x ∈ UniformOnFun.gen 𝔖 univ U →
        Membership.mem (γ := Set ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
          {x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) |
            (fun (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) ↦
                Membership.mem (α := (α →ᵤ β) × (α →ᵤ β)) (UniformFun.gen α β U)
                  (((UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.1),
                      (UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.2)) :
                    (α →ᵤ β) × (α →ᵤ β)))
              x}
          x}
    a
Tactic: filter_upwards [UniformOnFun.gen_mem_uniformity _ _ h hU] with f hf x using hf x (mem_univ _)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
h : univ ∈ 𝔖
U : Set (β × β)
hU : U ∈ 𝓤 β
h₁ :
  ∀ (a : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)),
    Membership.mem (γ := Set ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
      {x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) |
        x ∈ UniformOnFun.gen 𝔖 univ U →
          Membership.mem (γ := Set ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
            {x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) |
              (fun (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) ↦
                  Membership.mem (α := (α →ᵤ β) × (α →ᵤ β)) (UniformFun.gen α β U)
                    (((UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.1),
                        (UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.2)) :
                      (α →ᵤ β) × (α →ᵤ β)))
                x}
            x}
      a
⊢ ∀ᶠ (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) in 𝓤 (α →ᵤ[𝔖] β),
    Membership.mem (α := (α →ᵤ β) × (α →ᵤ β)) (UniformFun.gen α β U)
      (((UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.1),
          (UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.2)) :
        (α →ᵤ β) × (α →ᵤ β))
have h₂ : ∀ a ∈ UniformOnFun.gen 𝔖 univ U,
  Membership.mem (α := (α →ᵤ β) × (α →ᵤ β)) (UniformFun.gen α β U)
    (((UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) a.1),
        (UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) a.2)) :
      (α →ᵤ β) × (α →ᵤ β))
Tactic: filter_upwards [UniformOnFun.gen_mem_uniformity _ _ h hU] with f hf x using hf x (mem_univ _)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
h : univ ∈ 𝔖
U : Set (β × β)
hU : U ∈ 𝓤 β
h₁ :
  ∀ (a : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)),
    Membership.mem (γ := Set ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
      {x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) |
        x ∈ UniformOnFun.gen 𝔖 univ U →
          Membership.mem (γ := Set ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
            {x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) |
              (fun (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) ↦
                  Membership.mem (α := (α →ᵤ β) × (α →ᵤ β)) (UniformFun.gen α β U)
                    (((UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.1),
                        (UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.2)) :
                      (α →ᵤ β) × (α →ᵤ β)))
                x}
            x}
      a
h₂ :
  ∀ a ∈ UniformOnFun.gen 𝔖 univ U,
    Membership.mem (α := (α →ᵤ β) × (α →ᵤ β)) (UniformFun.gen α β U)
      (((UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) a.1),
          (UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) a.2)) :
        (α →ᵤ β) × (α →ᵤ β))
⊢ ∀ᶠ (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) in 𝓤 (α →ᵤ[𝔖] β),
    Membership.mem (α := (α →ᵤ β) × (α →ᵤ β)) (UniformFun.gen α β U)
      (((UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.1),
          (UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.2)) :
        (α →ᵤ β) × (α →ᵤ β))
have h₃ : ∀ (f : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) (hf : f ∈ UniformOnFun.gen 𝔖 univ U) (x : α),
  Membership.mem (α := β × β) U
    (((UniformFun.toFun : (a : α →ᵤ β) → α → β)
          (((UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f.1),
                (UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f.2)).1 :
            α →ᵤ β)
          x,
        (UniformFun.toFun : (a : α →ᵤ β) → α → β)
          (((UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f.1),
                (UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f.2)).2 :
            α →ᵤ β)
          x) :
      β × β)
Tactic: filter_upwards [UniformOnFun.gen_mem_uniformity _ _ h hU] with f hf x using hf x (mem_univ _)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
⊢ UniformContinuous (α := α →ᵤ[𝔗] β) (β := α →ᵤ[𝔖] β)
    (Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β))
have simp : Tendsto (β := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))
  (fun (x : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β)) ↦
    (Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x.1,
      Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x.2))
  (⨅ i₂ ∈ 𝓤 β, ⨅ i₁ ∈ 𝔗, 𝓟 (UniformOnFun.gen 𝔗 i₁ i₂)) (⨅ i₂ ∈ 𝓤 β, ⨅ i₁ ∈ 𝔖, 𝓟 (UniformOnFun.gen 𝔖 i₁ i₂))
Tactic: simp only [UniformContinuous, UniformOnFun.uniformity_eq, iInf₂_comm (ι₂ := Set (β × β))]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
⊢ Tendsto (β := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))
    (fun (x : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β)) ↦
      (Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x.1,
        Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x.2))
    (⨅ i₂ ∈ 𝓤 β, ⨅ i₁ ∈ 𝔗, 𝓟 (UniformOnFun.gen 𝔗 i₁ i₂)) (⨅ i₂ ∈ 𝓤 β, ⨅ i₁ ∈ 𝔖, 𝓟 (UniformOnFun.gen 𝔖 i₁ i₂))
have refine : ∀ (V : Set (β × β)) (hV : V ∈ 𝓤 β),
  Tendsto (β := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))
    (fun (x : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β)) ↦
      (Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x.1,
        Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x.2))
    (⨅ i₁ ∈ 𝔗, 𝓟 (UniformOnFun.gen 𝔗 i₁ V)) (⨅ i₁ ∈ 𝔖, 𝓟 (UniformOnFun.gen 𝔖 i₁ V))
Tactic: refine tendsto_iInf_iInf fun V ↦ tendsto_iInf_iInf fun hV ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ Tendsto (β := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))
    (fun (x : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β)) ↦
      (Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x.1,
        Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x.2))
    (⨅ i₁ ∈ 𝔗, 𝓟 (UniformOnFun.gen 𝔗 i₁ V)) (⨅ i₁ ∈ 𝔖, 𝓟 (UniformOnFun.gen 𝔖 i₁ V))
have simp : ∀ (i : Set α) (i_1 : i ∈ 𝔖),
  ∃ (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 𝔖 i V}
Tactic: simp only [tendsto_iInf, tendsto_principal, Filter.Eventually, mem_biInf_principal]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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 ∈ 𝔖
⊢ ∃ (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}
have obtain : ∀ (T : Set (Set α)) (hT𝔗 : T ⊆ 𝔗) (hT : T.Finite) (hsT : s ⊆ ⋃₀ T),
  ∃ (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: obtain ⟨T, hT𝔗, hT, hsT⟩ := h s hs
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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
⊢ ∃ (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}
have 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
Tactic: refine ⟨T, hT, hT𝔗, fun f hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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
⊢ 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
have 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) :
        β × β)
Tactic: simp only [UniformOnFun.gen, Set.mem_iInter, Set.mem_setOf_eq, Function.comp_apply] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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
⊢ Membership.mem (α := β × β) V
    (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β)
          ((ofFun 𝔗 : (a : α → β) → α →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f.1) : α →ᵤ[𝔗] β) x,
        (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β)
          ((ofFun 𝔗 : (a : α → β) → α →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f.2) : α →ᵤ[𝔗] β) x) :
      β × β)
have 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) :
      β × β)
Tactic: obtain ⟨t, ht, hxt⟩ := Set.mem_sUnion.mp <| hsT hx
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
γ : Type u_3
ι : Type u_4
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ uniformSpace α γ 𝔖 = ⨅ (i : ι), uniformSpace α γ 𝔖
have 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) γ))
Tactic: simp_rw [UniformOnFun.uniformSpace, UniformFun.iInf_eq, UniformSpace.comap_iInf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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) γ))
    (⨅ (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) γ))
have 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) γ))
Tactic: rw [iInf_comm]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
γ : Type u_3
𝔖 : Set (Set α)
u₁ u₂ : UniformSpace γ
⊢ uniformSpace α γ 𝔖 = uniformSpace α γ 𝔖 ⊓ uniformSpace α γ 𝔖
have rw : Eq (α := UniformSpace (α →ᵤ[𝔖] γ)) (⨅ (i : Bool), uniformSpace α γ 𝔖)
  (⨅ (b : Bool), bif b then uniformSpace α γ 𝔖 else uniformSpace α γ 𝔖)
Tactic: rw [inf_eq_iInf, inf_eq_iInf, UniformOnFun.iInf_eq]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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 α γ 𝔖)
have refine : ∀ (i : Bool), uniformSpace α γ 𝔖 = bif i then uniformSpace α γ 𝔖 else uniformSpace α γ 𝔖
Tactic: refine iInf_congr fun i => ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
γ : Type u_3
𝔖 : Set (Set α)
u₁ u₂ : UniformSpace γ
i : Bool
⊢ uniformSpace α γ 𝔖 = bif i then uniformSpace α γ 𝔖 else uniformSpace α γ 𝔖
have false : uniformSpace α γ 𝔖 = bif false then uniformSpace α γ 𝔖 else uniformSpace α γ 𝔖
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
γ : Type u_3
𝔖 : Set (Set α)
u₁ u₂ : UniformSpace γ
i : Bool
false : uniformSpace α γ 𝔖 = bif Bool.false then uniformSpace α γ 𝔖 else uniformSpace α γ 𝔖
⊢ uniformSpace α γ 𝔖 = bif i then uniformSpace α γ 𝔖 else uniformSpace α γ 𝔖
have true : uniformSpace α γ 𝔖 = bif true then uniformSpace α γ 𝔖 else uniformSpace α γ 𝔖
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
𝔖 : Set (Set α)
f : γ → β
⊢ uniformSpace α γ 𝔖 = UniformSpace.comap (fun (x : α → γ) ↦ f ∘ x) (uniformSpace α β 𝔖)
have 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) β))
Tactic: simp_rw [UniformOnFun.uniformSpace, UniformSpace.comap_iInf, UniformFun.comap_eq, ←
    UniformSpace.comap_comap]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ UniformContinuous (α := α →ᵤ[𝔖] γ) (β := α →ᵤ[𝔖] β)
    (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β)
      ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ)))
have rw : uniformSpace α γ 𝔖 ≤
  UniformSpace.comap
    (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β)
      ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ)))
    (uniformSpace α β 𝔖)
Tactic: rw [uniformContinuous_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : UniformSpace γ
f : γ → β
hf : IsUniformInducing f
⊢ IsUniformInducing (α := α →ᵤ[𝔖] γ) (β := α →ᵤ[𝔖] β)
    (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β)
      ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ)))
have 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))
    (𝓤 (α →ᵤ[𝔖] β)))
  (𝓤 (α →ᵤ[𝔖] γ))
Tactic: constructor