awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun (x : Set α) ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun (x : Set α) ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → (↑(φ₁ ⁻¹' S) : Type u_5) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → (↑(φ₂ ⁻¹' S) : Type u_6) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₂
⊢ uniformSpace α β 𝔖 =
    UniformSpace.comap
        (Function.comp (β := δ₁ → β) (⇑(ofFun 𝔗₁) : (a : δ₁ → β) → δ₁ →ᵤ[𝔗₁] β)
          ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
        (uniformSpace δ₁ β 𝔗₁) ⊓
      UniformSpace.comap
        (Function.comp (β := δ₂ → β) (⇑(ofFun 𝔗₂) : (a : δ₂ → β) → δ₂ →ᵤ[𝔗₂] β)
          ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
        (uniformSpace δ₂ β 𝔗₂)
have this : ∀ S ∈ 𝔖,
  Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
    (UniformSpace.comap (β := (↑(φ₁ ⁻¹' S) : Type u_5) → β)
        (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₁ S)
        (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S) : Type u_5) β) ⊓
      UniformSpace.comap (β := (↑(φ₂ ⁻¹' S) : Type u_6) → β)
        (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₂ S)
        (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S) : Type u_6) β))
Tactic: have : ∀ S ∈ 𝔖, 𝒰(S, β, _) = .comap (· ∘ ψ₁ S) 𝒰(_, β, _) ⊓ .comap (· ∘ ψ₂ S) 𝒰(_, β, _) := by
    refine fun S hS ↦ UniformFun.uniformSpace_eq_inf_precomp_of_cover β _ _ ?_
    simpa only [← univ_subset_iff, ψ₁, ψ₂, range_restrictPreimage, ← preimage_union,
      ← image_subset_iff, image_univ, Subtype.range_val] using h_cover S hS
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun (x : Set α) ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun (x : Set α) ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → (↑(φ₁ ⁻¹' S) : Type u_5) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → (↑(φ₂ ⁻¹' S) : Type u_6) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
      (UniformSpace.comap (β := (↑(φ₁ ⁻¹' S) : Type u_5) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₁ S)
          (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S) : Type u_5) β) ⊓
        UniformSpace.comap (β := (↑(φ₂ ⁻¹' S) : Type u_6) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₂ S)
          (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S) : Type u_6) β))
⊢ uniformSpace α β 𝔖 =
    UniformSpace.comap
        (Function.comp (β := δ₁ → β) (⇑(ofFun 𝔗₁) : (a : δ₁ → β) → δ₁ →ᵤ[𝔗₁] β)
          ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
        (uniformSpace δ₁ β 𝔗₁) ⊓
      UniformSpace.comap
        (Function.comp (β := δ₂ → β) (⇑(ofFun 𝔗₂) : (a : δ₂ → β) → δ₂ →ᵤ[𝔗₂] β)
          ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
        (uniformSpace δ₂ β 𝔗₂)
have refine_1 : uniformSpace α β 𝔖 ≤
  UniformSpace.comap
    (Function.comp (β := δ₁ → β) (⇑(ofFun 𝔗₁) : (a : δ₁ → β) → δ₁ →ᵤ[𝔗₁] β)
      ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
    (uniformSpace δ₁ β 𝔗₁)
Tactic: refine le_antisymm (le_inf ?_ ?_) (le_iInf₂ fun S hS ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun (x : Set α) ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun (x : Set α) ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → (↑(φ₁ ⁻¹' S) : Type u_5) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → (↑(φ₂ ⁻¹' S) : Type u_6) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
      (UniformSpace.comap (β := (↑(φ₁ ⁻¹' S) : Type u_5) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₁ S)
          (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S) : Type u_5) β) ⊓
        UniformSpace.comap (β := (↑(φ₂ ⁻¹' S) : Type u_6) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₂ S)
          (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S) : Type u_6) β))
refine_1 :
  uniformSpace α β 𝔖 ≤
    UniformSpace.comap
      (Function.comp (β := δ₁ → β) (⇑(ofFun 𝔗₁) : (a : δ₁ → β) → δ₁ →ᵤ[𝔗₁] β)
        ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
      (uniformSpace δ₁ β 𝔗₁)
⊢ uniformSpace α β 𝔖 =
    UniformSpace.comap
        (Function.comp (β := δ₁ → β) (⇑(ofFun 𝔗₁) : (a : δ₁ → β) → δ₁ →ᵤ[𝔗₁] β)
          ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
        (uniformSpace δ₁ β 𝔗₁) ⊓
      UniformSpace.comap
        (Function.comp (β := δ₂ → β) (⇑(ofFun 𝔗₂) : (a : δ₂ → β) → δ₂ →ᵤ[𝔗₂] β)
          ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
        (uniformSpace δ₂ β 𝔗₂)
have refine_2 : uniformSpace α β 𝔖 ≤
  UniformSpace.comap
    (Function.comp (β := δ₂ → β) (⇑(ofFun 𝔗₂) : (a : δ₂ → β) → δ₂ →ᵤ[𝔗₂] β)
      ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
    (uniformSpace δ₂ β 𝔗₂)
Tactic: refine le_antisymm (le_inf ?_ ?_) (le_iInf₂ fun S hS ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun (x : Set α) ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun (x : Set α) ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → (↑(φ₁ ⁻¹' S) : Type u_5) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → (↑(φ₂ ⁻¹' S) : Type u_6) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
      (UniformSpace.comap (β := (↑(φ₁ ⁻¹' S) : Type u_5) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₁ S)
          (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S) : Type u_5) β) ⊓
        UniformSpace.comap (β := (↑(φ₂ ⁻¹' S) : Type u_6) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₂ S)
          (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S) : Type u_6) β))
⊢ uniformSpace α β 𝔖 ≤
    UniformSpace.comap
      (Function.comp (β := δ₁ → β) (⇑(ofFun 𝔗₁) : (a : δ₁ → β) → δ₁ →ᵤ[𝔗₁] β)
        ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
      (uniformSpace δ₁ β 𝔗₁)
have refine_1 : UniformContinuous (α := α →ᵤ[𝔖] β) (β := δ₁ →ᵤ[𝔗₁] β)
  (Function.comp (β := δ₁ → β) (⇑(ofFun 𝔗₁) : (a : δ₁ → β) → δ₁ →ᵤ[𝔗₁] β)
    ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
Tactic: rw [← uniformContinuous_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun (x : Set α) ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun (x : Set α) ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → (↑(φ₁ ⁻¹' S) : Type u_5) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → (↑(φ₂ ⁻¹' S) : Type u_6) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
      (UniformSpace.comap (β := (↑(φ₁ ⁻¹' S) : Type u_5) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₁ S)
          (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S) : Type u_5) β) ⊓
        UniformSpace.comap (β := (↑(φ₂ ⁻¹' S) : Type u_6) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₂ S)
          (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S) : Type u_6) β))
⊢ uniformSpace α β 𝔖 ≤
    UniformSpace.comap
      (Function.comp (β := δ₂ → β) (⇑(ofFun 𝔗₂) : (a : δ₂ → β) → δ₂ →ᵤ[𝔗₂] β)
        ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
      (uniformSpace δ₂ β 𝔗₂)
have refine_2 : UniformContinuous (α := α →ᵤ[𝔖] β) (β := δ₂ →ᵤ[𝔗₂] β)
  (Function.comp (β := δ₂ → β) (⇑(ofFun 𝔗₂) : (a : δ₂ → β) → δ₂ →ᵤ[𝔗₂] β)
    ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
Tactic: rw [← uniformContinuous_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ (I : Set ι), I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → (↑(φ i ⁻¹' S) : Type u_5) → (↑S : Type u_1) :=
  fun (S : Set α) (i : ι) ↦ S.restrictPreimage (φ i)
S : Set α
hS : S ∈ 𝔖
⊢ Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
    (⨅ (i : ι),
      UniformSpace.comap (β := (↑(φ i ⁻¹' S) : Type u_5) → β)
        (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ S i)
        (UniformFun.uniformSpace (↑(φ i ⁻¹' S) : Type u_5) β))
have rcases : ∀ (I : Set ι) (I_finite : I.Finite) (I_cover : S ⊆ ⋃ i ∈ I, range (φ i)),
  Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
    (⨅ (i : ι),
      UniformSpace.comap (β := (↑(φ i ⁻¹' S) : Type u_5) → β)
        (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ S i)
        (UniformFun.uniformSpace (↑(φ i ⁻¹' S) : Type u_5) β))
Tactic: rcases h_cover S hS with ⟨I, I_finite, I_cover⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ (I : Set ι), I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → (↑(φ i ⁻¹' S) : Type u_5) → (↑S : Type u_1) :=
  fun (S : Set α) (i : ι) ↦ S.restrictPreimage (φ i)
S : Set α
hS : S ∈ 𝔖
I : Set ι
I_finite : I.Finite
I_cover : S ⊆ ⋃ i ∈ I, range (φ i)
⊢ Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
    (⨅ (i : ι),
      UniformSpace.comap (β := (↑(φ i ⁻¹' S) : Type u_5) → β)
        (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ S i)
        (UniformFun.uniformSpace (↑(φ i ⁻¹' S) : Type u_5) β))
have refine : Eq.{u_1 + 1} (α := Set (↑S : Type u_1)) (⋃ i ∈ I, range (ψ S i)) univ
Tactic: refine UniformFun.uniformSpace_eq_iInf_precomp_of_cover β _ ⟨I, I_finite, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ (I : Set ι), I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → (↑(φ i ⁻¹' S) : Type u_5) → (↑S : Type u_1) :=
  fun (S : Set α) (i : ι) ↦ S.restrictPreimage (φ i)
⊢ uniformSpace α β 𝔖 =
    ⨅ (i : ι),
      UniformSpace.comap
        (Function.comp (β := δ i → β) (⇑(ofFun (𝔗 i)) : (a : δ i → β) → δ i →ᵤ[𝔗 i] β)
          ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
        (uniformSpace (δ i) β (𝔗 i))
have this : ∀ S ∈ 𝔖,
  Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
    (⨅ (i : ι),
      UniformSpace.comap (β := (↑(φ i ⁻¹' S) : Type u_5) → β)
        (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ S i)
        (UniformFun.uniformSpace (↑(φ i ⁻¹' S) : Type u_5) β))
Tactic: have : ∀ S ∈ 𝔖, 𝒰(S, β, _) = ⨅ i, .comap (· ∘ ψ S i) 𝒰(_, β, _) := fun S hS ↦ by
    rcases h_cover S hS with ⟨I, I_finite, I_cover⟩
    refine UniformFun.uniformSpace_eq_iInf_precomp_of_cover β _ ⟨I, I_finite, ?_⟩
    simpa only [← univ_subset_iff, ψ, range_restrictPreimage, ← preimage_iUnion₂,
      ← image_subset_iff, image_univ, Subtype.range_val] using I_cover
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ (I : Set ι), I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → (↑(φ i ⁻¹' S) : Type u_5) → (↑S : Type u_1) :=
  fun (S : Set α) (i : ι) ↦ S.restrictPreimage (φ i)
this :
  ∀ S ∈ 𝔖,
    Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
      (⨅ (i : ι),
        UniformSpace.comap (β := (↑(φ i ⁻¹' S) : Type u_5) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ S i)
          (UniformFun.uniformSpace (↑(φ i ⁻¹' S) : Type u_5) β))
⊢ uniformSpace α β 𝔖 =
    ⨅ (i : ι),
      UniformSpace.comap
        (Function.comp (β := δ i → β) (⇑(ofFun (𝔗 i)) : (a : δ i → β) → δ i →ᵤ[𝔗 i] β)
          ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
        (uniformSpace (δ i) β (𝔗 i))
have refine_1 : ∀ (i : ι),
  uniformSpace α β 𝔖 ≤
    UniformSpace.comap
      (Function.comp (β := δ i → β) (⇑(ofFun (𝔗 i)) : (a : δ i → β) → δ i →ᵤ[𝔗 i] β)
        ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
      (uniformSpace (δ i) β (𝔗 i))
Tactic: refine le_antisymm (le_iInf fun i ↦ ?_) (le_iInf₂ fun S hS ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ (I : Set ι), I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → (↑(φ i ⁻¹' S) : Type u_5) → (↑S : Type u_1) :=
  fun (S : Set α) (i : ι) ↦ S.restrictPreimage (φ i)
this :
  ∀ S ∈ 𝔖,
    Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
      (⨅ (i : ι),
        UniformSpace.comap (β := (↑(φ i ⁻¹' S) : Type u_5) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ S i)
          (UniformFun.uniformSpace (↑(φ i ⁻¹' S) : Type u_5) β))
refine_1 :
  ∀ (i : ι),
    uniformSpace α β 𝔖 ≤
      UniformSpace.comap
        (Function.comp (β := δ i → β) (⇑(ofFun (𝔗 i)) : (a : δ i → β) → δ i →ᵤ[𝔗 i] β)
          ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
        (uniformSpace (δ i) β (𝔗 i))
⊢ uniformSpace α β 𝔖 =
    ⨅ (i : ι),
      UniformSpace.comap
        (Function.comp (β := δ i → β) (⇑(ofFun (𝔗 i)) : (a : δ i → β) → δ i →ᵤ[𝔗 i] β)
          ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
        (uniformSpace (δ i) β (𝔗 i))
have refine_2 : ∀ (S : Set α) (hS : S ∈ 𝔖),
  LE.le (α := UniformSpace (α →ᵤ[𝔖] β))
    (⨅ (i : ι),
      UniformSpace.comap
        (Function.comp (β := δ i → β) (⇑(ofFun (𝔗 i)) : (a : δ i → β) → δ i →ᵤ[𝔗 i] β)
          ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
        (uniformSpace (δ i) β (𝔗 i)))
    (UniformSpace.comap (β := UniformFun.{u_1, u_2} (↑S : Type u_1) β)
      (Function.comp (β := (↑S : Type u_1) → β)
        ((⇑UniformFun.ofFun : (a : (↑S : Type u_1) → β) → UniformFun.{u_1, u_2} (↑S : Type u_1) β) :
          (a : (↑S : Type u_1) → β) → UniformFun.{u_1, u_2} (↑S : Type u_1) β)
        (Function.comp (β := α → β) (S.restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
          (α →ᵤ[𝔖] β) → (↑S : Type u_1) → β))
      (UniformFun.uniformSpace (↑S : Type u_1) β))
Tactic: refine le_antisymm (le_iInf fun i ↦ ?_) (le_iInf₂ fun S hS ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ (I : Set ι), I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → (↑(φ i ⁻¹' S) : Type u_5) → (↑S : Type u_1) :=
  fun (S : Set α) (i : ι) ↦ S.restrictPreimage (φ i)
this :
  ∀ S ∈ 𝔖,
    Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
      (⨅ (i : ι),
        UniformSpace.comap (β := (↑(φ i ⁻¹' S) : Type u_5) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ S i)
          (UniformFun.uniformSpace (↑(φ i ⁻¹' S) : Type u_5) β))
i : ι
⊢ uniformSpace α β 𝔖 ≤
    UniformSpace.comap
      (Function.comp (β := δ i → β) (⇑(ofFun (𝔗 i)) : (a : δ i → β) → δ i →ᵤ[𝔗 i] β)
        ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
      (uniformSpace (δ i) β (𝔗 i))
have refine_1 : UniformContinuous (α := α →ᵤ[𝔖] β) (β := δ i →ᵤ[𝔗 i] β)
  (Function.comp (β := δ i → β) (⇑(ofFun (𝔗 i)) : (a : δ i → β) → δ i →ᵤ[𝔗 i] β)
    ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
Tactic: rw [← uniformContinuous_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF : ∀ (i : ι) (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
⊢ TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (F i x)) (fun (x : α) ↦ g (f x)) p
have hg₁ : UniformContinuous (s.restrict (π := fun (a : β) ↦ γ) g)
Tactic: rw [uniformContinuousOn_iff_restrict] at hg
Cleared hypotheses: hg, h
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF : ∀ (i : ι) (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuous (s.restrict (π := fun (a : β) ↦ γ) g)
h : TendstoUniformly F f p
⊢ TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (F i x)) (fun (x : α) ↦ g (f x)) p
have lift : ∀ (F' : (i : ι) → α → (↑s : Type u_2)) (hF' : (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β)) = F)
  (comp_tendstoUniformly :
    ∀ (hF : ∀ (i : ι) (x : α), (↑(F' i x) : β) ∈ s) (hf : ∀ (x : α), f x ∈ s) (hg : UniformContinuousOn g s)
      (h : TendstoUniformly (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β)) f p),
      TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (↑(F' i x) : β)) (fun (x : α) ↦ g (f x)) p)
  (h : TendstoUniformly (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β)) f p),
  TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (↑(F' i x) : β)) (fun (x : α) ↦ g (f x)) p
Tactic: lift F to ι → α → s using hF with F' hF'
Cleared hypotheses: hF, h
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuous (s.restrict (π := fun (a : β) ↦ γ) g)
F' : (i : ι) → α → (↑s : Type u_2)
hF' : (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β)) = F
comp_tendstoUniformly :
  ∀ (hF : ∀ (i : ι) (x : α), (↑(F' i x) : β) ∈ s) (hf : ∀ (x : α), f x ∈ s) (hg : UniformContinuousOn g s)
    (h : TendstoUniformly (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β)) f p),
    TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (↑(F' i x) : β)) (fun (x : α) ↦ g (f x)) p
h : TendstoUniformly (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β)) f p
⊢ TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (↑(F' i x) : β)) (fun (x : α) ↦ g (f x)) p
have lift : ∀ (f' : (i : α) → (↑s : Type u_2)) (hf' : (fun (i : α) ↦ (↑(f' i) : β)) = f)
  (comp_tendstoUniformly :
    ∀ (hF : ∀ (i : ι) (x : α), (↑(F' i x) : β) ∈ s) (hf : ∀ (x : α), (↑(f' x) : β) ∈ s) (hg : UniformContinuousOn g s)
      (h :
        TendstoUniformly.{u_1, u_2, u_4} (β := β) (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β))
          (fun (i : α) ↦ (↑(f' i) : β)) p),
      TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (↑(F' i x) : β))
        (fun (x : α) ↦ g (↑(f' x) : β)) p)
  (h :
    TendstoUniformly.{u_1, u_2, u_4} (β := β) (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β)) (fun (i : α) ↦ (↑(f' i) : β))
      p),
  TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (↑(F' i x) : β)) (fun (x : α) ↦ g (↑(f' x) : β)) p
Tactic: lift f to α → s using hf with f' hf'
Cleared hypotheses: hf, comp_tendstoUniformly, h
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hg : UniformContinuous (s.restrict (π := fun (a : β) ↦ γ) g)
F' : (i : ι) → α → (↑s : Type u_2)
hF' : (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β)) = F
f' : (i : α) → (↑s : Type u_2)
hf' : (fun (i : α) ↦ (↑(f' i) : β)) = f
comp_tendstoUniformly :
  ∀ (hF : ∀ (i : ι) (x : α), (↑(F' i x) : β) ∈ s) (hf : ∀ (x : α), (↑(f' x) : β) ∈ s) (hg : UniformContinuousOn g s)
    (h :
      TendstoUniformly.{u_1, u_2, u_4} (β := β) (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β))
        (fun (i : α) ↦ (↑(f' i) : β)) p),
    TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (↑(F' i x) : β)) (fun (x : α) ↦ g (↑(f' x) : β))
      p
h :
  TendstoUniformly.{u_1, u_2, u_4} (β := β) (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β)) (fun (i : α) ↦ (↑(f' i) : β)) p
⊢ TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (↑(F' i x) : β)) (fun (x : α) ↦ g (↑(f' x) : β)) p
have h₁ : Tendsto (fun (q : ι × α) ↦ ((↑(f' q.2) : β), (↑(F' q.1 q.2) : β))) (SProd.sprod (β := Filter α) p ⊤) (𝓤 β)
Tactic: rw [tendstoUniformly_iff_tendsto] at h
Cleared hypotheses: h