awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x_1 : (α →ᵤ β) × (α →ᵤ β)
x : α
f g : α →ᵤ β
hfg :
  Membership.mem (γ := Set ((α →ᵤ β) × (α →ᵤ β)))
    ((fun (p : (α →ᵤ β) × (α →ᵤ β)) ↦
          (Function.comp (β := δ₁ → β) (⇑ofFun : (a : δ₁ → β) → δ₁ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.1,
            Function.comp (β := δ₁ → β) (⇑ofFun : (a : δ₁ → β) → δ₁ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.2)) ⁻¹'
        UniformFun.gen δ₁ β (U, U).1 ∩
      (fun (p : (α →ᵤ β) × (α →ᵤ β)) ↦
          (Function.comp (β := δ₂ → β) (⇑ofFun : (a : δ₂ → β) → δ₂ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.1,
            Function.comp (β := δ₂ → β) (⇑ofFun : (a : δ₂ → β) → δ₂ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.2)) ⁻¹'
        UniformFun.gen δ₂ β (U, U).2)
    (f, g)
⊢ Membership.mem (α := β × β) U
    (((toFun : (a : α →ᵤ β) → α → β) (f, g).1 x, (toFun : (a : α →ᵤ β) → α → β) (f, g).2 x) : β × β)
have h : ∀ (y : δ₁),
  Membership.mem (α := β × β) U
    (((toFun : (a : α →ᵤ β) → α → β) (f, g).1 (φ₁ y), (toFun : (a : α →ᵤ β) → α → β) (f, g).2 (φ₁ y)) : β × β)
Tactic: rcases h_cover.ge <| mem_univ x with (⟨y, rfl⟩ | ⟨y, rfl⟩)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x_1 : (α →ᵤ β) × (α →ᵤ β)
x : α
f g : α →ᵤ β
hfg :
  Membership.mem (γ := Set ((α →ᵤ β) × (α →ᵤ β)))
    ((fun (p : (α →ᵤ β) × (α →ᵤ β)) ↦
          (Function.comp (β := δ₁ → β) (⇑ofFun : (a : δ₁ → β) → δ₁ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.1,
            Function.comp (β := δ₁ → β) (⇑ofFun : (a : δ₁ → β) → δ₁ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.2)) ⁻¹'
        UniformFun.gen δ₁ β (U, U).1 ∩
      (fun (p : (α →ᵤ β) × (α →ᵤ β)) ↦
          (Function.comp (β := δ₂ → β) (⇑ofFun : (a : δ₂ → β) → δ₂ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.1,
            Function.comp (β := δ₂ → β) (⇑ofFun : (a : δ₂ → β) → δ₂ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.2)) ⁻¹'
        UniformFun.gen δ₂ β (U, U).2)
    (f, g)
h :
  ∀ (y : δ₁),
    Membership.mem (α := β × β) U
      (((toFun : (a : α →ᵤ β) → α → β) (f, g).1 (φ₁ y), (toFun : (a : α →ᵤ β) → α → β) (f, g).2 (φ₁ y)) : β × β)
⊢ Membership.mem (α := β × β) U
    (((toFun : (a : α →ᵤ β) → α → β) (f, g).1 x, (toFun : (a : α →ᵤ β) → α → β) (f, g).2 x) : β × β)
have h₁ : ∀ (y : δ₂),
  Membership.mem (α := β × β) U
    (((toFun : (a : α →ᵤ β) → α → β) (f, g).1 (φ₂ y), (toFun : (a : α →ᵤ β) → α → β) (f, g).2 (φ₂ y)) : β × β)
Tactic: rcases h_cover.ge <| mem_univ x with (⟨y, rfl⟩ | ⟨y, rfl⟩)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ (I : Set ι), I.Finite ∧ Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ I, range (φ i)) univ
⊢ uniformSpace α β =
    ⨅ (i : ι),
      UniformSpace.comap (β := UniformFun.{u_6, u_2} (δ i) β)
        (Function.comp (β := δ i → β) (⇑ofFun : (a : δ i → β) → δ i →ᵤ β)
          ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)))
        (uniformSpace (δ i) β)
have h : Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ (I : Set ι), I.Finite ∧ Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ I, range (φ i)) univ
⊢ Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))
have h : Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β))
  (⨅ (i : ι),
    comap (β := UniformFun.{u_6, u_2} (δ i) β × UniformFun.{u_6, u_2} (δ i) β)
      (Prod.map
        (Function.comp (β := δ i → β) (⇑ofFun : (a : δ i → β) → δ i →ᵤ β)
          ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)))
        (Function.comp (β := δ i → β) (⇑ofFun : (a : δ i → β) → δ i →ᵤ β)
          ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑toFun : (a : α →ᵤ β) → α → β))))
      (𝓤 (UniformFun.{u_6, u_2} (δ i) β)))
Tactic: simp_rw [iInf_uniformity, uniformity_comap]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ (I : Set ι), I.Finite ∧ Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ I, range (φ i)) univ
⊢ Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β))
    (⨅ (i : ι),
      comap (β := UniformFun.{u_6, u_2} (δ i) β × UniformFun.{u_6, u_2} (δ i) β)
        (Prod.map
          (Function.comp (β := δ i → β) (⇑ofFun : (a : δ i → β) → δ i →ᵤ β)
            ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)))
          (Function.comp (β := δ i → β) (⇑ofFun : (a : δ i → β) → δ i →ᵤ β)
            ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑toFun : (a : α →ᵤ β) → α → β))))
        (𝓤 (UniformFun.{u_6, u_2} (δ i) β)))
have h : LE.le (α := Filter ((α →ᵤ β) × (α →ᵤ β)))
  (⨅ (i : ι),
    comap (β := UniformFun.{u_6, u_2} (δ i) β × UniformFun.{u_6, u_2} (δ i) β)
      (Prod.map
        (Function.comp (β := δ i → β) (⇑ofFun : (a : δ i → β) → δ i →ᵤ β)
          ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)))
        (Function.comp (β := δ i → β) (⇑ofFun : (a : δ i → β) → δ i →ᵤ β)
          ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑toFun : (a : α →ᵤ β) → α → β))))
      (𝓤 (UniformFun.{u_6, u_2} (δ i) β)))
  (𝓤 (α →ᵤ β))
Tactic: refine le_antisymm (le_iInf fun i ↦ tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous) ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ (I : Set ι), I.Finite ∧ Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ I, range (φ i)) univ
⊢ LE.le (α := Filter ((α →ᵤ β) × (α →ᵤ β)))
    (⨅ (i : ι),
      comap (β := UniformFun.{u_6, u_2} (δ i) β × UniformFun.{u_6, u_2} (δ i) β)
        (Prod.map
          (Function.comp (β := δ i → β) (⇑ofFun : (a : δ i → β) → δ i →ᵤ β)
            ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)))
          (Function.comp (β := δ i → β) (⇑ofFun : (a : δ i → β) → δ i →ᵤ β)
            ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑toFun : (a : α →ᵤ β) → α → β))))
        (𝓤 (UniformFun.{u_6, u_2} (δ i) β)))
    (𝓤 (α →ᵤ β))
have h : ∀ (I : Set ι) (I_finite : I.Finite) (I_cover : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ I, range (φ i)) univ),
  LE.le (α := Filter ((α →ᵤ β) × (α →ᵤ β)))
    (⨅ (i : ι),
      comap (β := UniformFun.{u_6, u_2} (δ i) β × UniformFun.{u_6, u_2} (δ i) β)
        (Prod.map
          (Function.comp (β := δ i → β) (⇑ofFun : (a : δ i → β) → δ i →ᵤ β)
            ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)))
          (Function.comp (β := δ i → β) (⇑ofFun : (a : δ i → β) → δ i →ᵤ β)
            ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑toFun : (a : α →ᵤ β) → α → β))))
        (𝓤 (UniformFun.{u_6, u_2} (δ i) β)))
    (𝓤 (α →ᵤ β))
Tactic: rcases h_cover with ⟨I, I_finite, I_cover⟩
Cleared hypotheses: h_cover
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
I : Set ι
I_finite : I.Finite
I_cover : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ I, range (φ i)) univ
⊢ LE.le (α := Filter ((α →ᵤ β) × (α →ᵤ β)))
    (⨅ (i : ι),
      comap (β := UniformFun.{u_6, u_2} (δ i) β × UniformFun.{u_6, u_2} (δ i) β)
        (Prod.map
          (Function.comp (β := δ i → β) (⇑ofFun : (a : δ i → β) → δ i →ᵤ β)
            ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)))
          (Function.comp (β := δ i → β) (⇑ofFun : (a : δ i → β) → δ i →ᵤ β)
            ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑toFun : (a : α →ᵤ β) → α → β))))
        (𝓤 (UniformFun.{u_6, u_2} (δ i) β)))
    (𝓤 (α →ᵤ β))
have h : ∀ (U : Set (β × β)) (hU : U ∈ 𝓤 β) (x : (α →ᵤ β) × (α →ᵤ β)) (x : α) (f g : α →ᵤ β)
  (hfg :
    Membership.mem (γ := Set ((α →ᵤ β) × (α →ᵤ β)))
      (⋂ (i :
        (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_4)) → Set (β × β))
              (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_4)) → Set (β × β)) I fun (x : (↑I : Type u_4)) ↦ U)) :
          Type u_4)),
        preimage (β := UniformFun.{u_6, u_2} (δ (↑i : ι)) β × UniformFun.{u_6, u_2} (δ (↑i : ι)) β)
          (Prod.map
            (Function.comp (β := δ (↑i : ι) → β) (⇑ofFun : (a : δ (↑i : ι) → β) → δ (↑i : ι) →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ (↑i : ι)) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)))
            (Function.comp (β := δ (↑i : ι) → β) (⇑ofFun : (a : δ (↑i : ι) → β) → δ (↑i : ι) →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ (↑i : ι)) ∘ (⇑toFun : (a : α →ᵤ β) → α → β))))
          (UniformFun.gen (δ (↑i : ι)) β
            (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_4)) → Set (β × β))
              (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_4)) → Set (β × β)) I fun (x : (↑I : Type u_4)) ↦ U)
              i)))
      (f, g)),
  Membership.mem (α := β × β) U
    (((toFun : (a : α →ᵤ β) → α → β) (f, g).1 x, (toFun : (a : α →ᵤ β) → α → β) (f, g).2 x) : β × β)
Tactic: refine HasBasis.iInf (fun i : ι ↦ UniformFun.hasBasis_uniformity (δ i) β |>.comap _)
      |>.le_basis_iff (UniformFun.hasBasis_uniformity α β) |>.mpr fun U hU ↦
    ⟨⟨I, fun _ ↦ U⟩, ⟨I_finite, fun _ ↦ hU⟩, fun ⟨f, g⟩ hfg x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
I : Set ι
I_finite : I.Finite
I_cover : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ I, range (φ i)) univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x_1 : (α →ᵤ β) × (α →ᵤ β)
x : α
f g : α →ᵤ β
hfg :
  Membership.mem (γ := Set ((α →ᵤ β) × (α →ᵤ β)))
    (⋂ (i :
      (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_4)) → Set (β × β))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_4)) → Set (β × β)) I fun (x : (↑I : Type u_4)) ↦ U)) :
        Type u_4)),
      preimage (β := UniformFun.{u_6, u_2} (δ (↑i : ι)) β × UniformFun.{u_6, u_2} (δ (↑i : ι)) β)
        (Prod.map
          (Function.comp (β := δ (↑i : ι) → β) (⇑ofFun : (a : δ (↑i : ι) → β) → δ (↑i : ι) →ᵤ β)
            ((fun (x : α → β) ↦ x ∘ φ (↑i : ι)) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)))
          (Function.comp (β := δ (↑i : ι) → β) (⇑ofFun : (a : δ (↑i : ι) → β) → δ (↑i : ι) →ᵤ β)
            ((fun (x : α → β) ↦ x ∘ φ (↑i : ι)) ∘ (⇑toFun : (a : α →ᵤ β) → α → β))))
        (UniformFun.gen (δ (↑i : ι)) β
          (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_4)) → Set (β × β))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_4)) → Set (β × β)) I fun (x : (↑I : Type u_4)) ↦ U) i)))
    (f, g)
⊢ Membership.mem (α := β × β) U
    (((toFun : (a : α →ᵤ β) → α → β) (f, g).1 x, (toFun : (a : α →ᵤ β) → α → β) (f, g).2 x) : β × β)
have h : ∀ (i : ι) (hi : i ∈ I) (y : δ i),
  Membership.mem (α := β × β) U
    (((toFun : (a : α →ᵤ β) → α → β) (f, g).1 (φ i y), (toFun : (a : α →ᵤ β) → α → β) (f, g).2 (φ i y)) : β × β)
Tactic: rcases mem_iUnion₂.mp <| I_cover.ge <| mem_univ x with ⟨i, hi, y, rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
S : Set α
V : Set (β × β)
⊢ UniformOnFun.gen 𝔖 S V =
    preimage (β := ((a : (↑S : Type u_1)) → β) × ((a : (↑S : Type u_1)) → β))
      (Prod.map
          (Function.comp (β := (a : α) → β) (S.restrict (π := fun (a : α) ↦ β))
            (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β))
          (Function.comp (β := (a : α) → β) (S.restrict (π := fun (a : α) ↦ β))
            (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β)) :
        (α →ᵤ β) × (α →ᵤ β) → ((a : (↑S : Type u_1)) → β) × ((a : (↑S : Type u_1)) → β))
      (UniformFun.gen (↑S : Type u_1) β V :
        Set (UniformFun.{u_1, u_2} (↑S : Type u_1) β × UniformFun.{u_1, u_2} (↑S : Type u_1) β))
have h : ∀ (uv : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)),
  uv ∈ UniformOnFun.gen 𝔖 S V ↔
    Membership.mem (γ := Set ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
      (preimage (β := ((a : (↑S : Type u_1)) → β) × ((a : (↑S : Type u_1)) → β))
        (Prod.map
            (Function.comp (β := (a : α) → β) (S.restrict (π := fun (a : α) ↦ β))
              (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β))
            (Function.comp (β := (a : α) → β) (S.restrict (π := fun (a : α) ↦ β))
              (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β)) :
          (α →ᵤ β) × (α →ᵤ β) → ((a : (↑S : Type u_1)) → β) × ((a : (↑S : Type u_1)) → β))
        (UniformFun.gen (↑S : Type u_1) β V :
          Set (UniformFun.{u_1, u_2} (↑S : Type u_1) β × UniformFun.{u_1, u_2} (↑S : Type u_1) β)))
      uv
Tactic: ext uv
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
⊢ topologicalSpace α β 𝔖 =
    ⨅ s ∈ 𝔖,
      TopologicalSpace.induced (Y := 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.topologicalSpace (↑s : Type u_1) β)
have simp : Eq (α := TopologicalSpace (α →ᵤ[𝔖] β)) (⨅ i ∈ 𝔖, UniformSpace.toTopologicalSpace)
  (⨅ s ∈ 𝔖,
    TopologicalSpace.induced (Y := 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.topologicalSpace (↑s : Type u_1) β))
Tactic: simp only [UniformOnFun.topologicalSpace, UniformSpace.toTopologicalSpace_iInf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
𝔖 : Set (Set α)
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
S : Set α
⊢ HasBasis (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) (𝓤 (α →ᵤ[𝔖] β)) p fun (i : ι) ↦ UniformOnFun.gen 𝔖 S (s i)
have simp_rw : HasBasis (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))
  (comap (Prod.map (S.restrict (π := fun (a : α) ↦ β)) (S.restrict (π := fun (a : α) ↦ β)))
    (𝓤 ((a : (↑S : Type u_1)) → β)))
  p fun (i : ι) ↦
  preimage (β := ((a : (↑S : Type u_1)) → β) × ((a : (↑S : Type u_1)) → β))
    (Prod.map
        (Function.comp (β := (a : α) → β) (S.restrict (π := fun (a : α) ↦ β))
          (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β))
        (Function.comp (β := (a : α) → β) (S.restrict (π := fun (a : α) ↦ β))
          (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β)) :
      (α →ᵤ β) × (α →ᵤ β) → ((a : (↑S : Type u_1)) → β) × ((a : (↑S : Type u_1)) → β))
    (UniformFun.gen (↑S : Type u_1) β (s i) :
      Set (UniformFun.{u_1, u_2} (↑S : Type u_1) β × UniformFun.{u_1, u_2} (↑S : Type u_1) β))
Tactic: simp_rw [UniformOnFun.gen_eq_preimage_restrict, uniformity_comap]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
𝔖 : Set (Set α)
h : 𝔖.Nonempty
h' : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) 𝔖
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
⊢ HasBasis (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) (𝓤 (α →ᵤ[𝔖] β)) (fun (Si : Prod.{u_1, u_4} (Set α) ι) ↦ Si.1 ∈ 𝔖 ∧ p Si.2)
    fun (Si : Prod.{u_1, u_4} (Set α) ι) ↦ UniformOnFun.gen 𝔖 Si.1 (s Si.2)
have simp : HasBasis (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) (⨅ i ∈ 𝔖, 𝓤 (α →ᵤ[𝔖] β))
  (fun (Si : Prod.{u_1, u_4} (Set α) ι) ↦ Si.1 ∈ 𝔖 ∧ p Si.2) fun (Si : Prod.{u_1, u_4} (Set α) ι) ↦
  UniformOnFun.gen 𝔖 Si.1 (s Si.2)
Tactic: simp only [iInf_uniformity]
-- 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
inst_1 : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ (i : ι), s ⊆ t i
hb : (𝓤 β).HasBasis p V
⊢ HasBasis (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) (𝓤 (α →ᵤ[𝔖] β)) (fun (i : ι × ι') ↦ p i.2) fun (i : ι × ι') ↦
    UniformOnFun.gen 𝔖 (t i.1) (V i.2)
have hne : 𝔖.Nonempty
Tactic: have hne : 𝔖.Nonempty := (range_nonempty t).mono (range_subset_iff.2 ht)
-- 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
inst_1 : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ (i : ι), s ⊆ t i
hb : (𝓤 β).HasBasis p V
hne : 𝔖.Nonempty
s₁ : Set α
hs₁ : s₁ ∈ 𝔖
s₂ : Set α
hs₂ : s₂ ∈ 𝔖
⊢ ∃ z ∈ 𝔖, (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s₁ z ∧ (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s₂ z
have rcases : ∀ (i₁ : ι) (his₁ : s₁ ⊆ t i₁) (i₂ : ι) (his₂ : s₂ ⊆ t i₂),
  ∃ z ∈ 𝔖, (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s₁ z ∧ (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s₂ z
Tactic: rcases hex s₁ hs₁, hex s₂ hs₂ with ⟨⟨i₁, his₁⟩, i₂, his₂⟩
-- 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
inst_1 : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ (i : ι), s ⊆ t i
hb : (𝓤 β).HasBasis p V
hne : 𝔖.Nonempty
s₁ : Set α
hs₁ : s₁ ∈ 𝔖
s₂ : Set α
hs₂ : s₂ ∈ 𝔖
i₁ : ι
his₁ : s₁ ⊆ t i₁
i₂ : ι
his₂ : s₂ ⊆ t i₂
⊢ ∃ z ∈ 𝔖, (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s₁ z ∧ (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s₂ z
have rcases : ∀ (i : ι) (hi₁ : t i₁ ⊆ t i) (hi₂ : t i₂ ⊆ t i),
  ∃ z ∈ 𝔖, (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s₁ z ∧ (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s₂ z
Tactic: rcases hdir i₁ i₂ with ⟨i, hi₁, hi₂⟩
-- 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
inst_1 : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ (i : ι), s ⊆ t i
hb : (𝓤 β).HasBasis p V
hne : 𝔖.Nonempty
⊢ HasBasis (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) (𝓤 (α →ᵤ[𝔖] β)) (fun (i : ι × ι') ↦ p i.2) fun (i : ι × ι') ↦
    UniformOnFun.gen 𝔖 (t i.1) (V i.2)
have hd : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) 𝔖
Tactic: have hd : DirectedOn (· ⊆ ·) 𝔖 := fun s₁ hs₁ s₂ hs₂ ↦ by
    rcases hex s₁ hs₁, hex s₂ hs₂ with ⟨⟨i₁, his₁⟩, i₂, his₂⟩
    rcases hdir i₁ i₂ with ⟨i, hi₁, hi₂⟩
    exact ⟨t i, ht _, his₁.trans hi₁, his₂.trans hi₂⟩
-- 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
inst_1 : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ (i : ι), s ⊆ t i
hb : (𝓤 β).HasBasis p V
hne : 𝔖.Nonempty
hd : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) 𝔖
⊢ HasBasis (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) (𝓤 (α →ᵤ[𝔖] β)) (fun (i : ι × ι') ↦ p i.2) fun (i : ι × ι') ↦
    UniformOnFun.gen 𝔖 (t i.1) (V i.2)
have refine : ∀ (x : Prod.{u_1, u_6} (Set α) ι') (s : Set α) (i' : ι'),
  (s, i').1 ∈ 𝔖 ∧ p (s, i').2 →
    ∀ (hs : (s, i').1 ∈ 𝔖) (hi' : p (s, i').2),
      ∃ (i'_1 : ι × ι'),
        p i'_1.2 ∧ UniformOnFun.gen 𝔖 (t i'_1.1) (V i'_1.2) ⊆ UniformOnFun.gen 𝔖 (s, i').1 (V (s, i').2)
Tactic: refine (UniformOnFun.hasBasis_uniformity_of_basis α β 𝔖 hne hd hb).to_hasBasis
    (fun ⟨s, i'⟩ ⟨hs, hi'⟩ ↦ ?_) fun ⟨i, i'⟩ hi' ↦ ⟨(t i, i'), ⟨ht i, hi'⟩, Subset.rfl⟩
-- 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
inst_1 : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ (i : ι), s ⊆ t i
hb : (𝓤 β).HasBasis p V
hne : 𝔖.Nonempty
hd : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) 𝔖
x : Prod.{u_1, u_6} (Set α) ι'
s : Set α
i' : ι'
h : (s, i').1 ∈ 𝔖 ∧ p (s, i').2
hs : (s, i').1 ∈ 𝔖
hi' : p (s, i').2
⊢ ∃ (i'_1 : ι × ι'), p i'_1.2 ∧ UniformOnFun.gen 𝔖 (t i'_1.1) (V i'_1.2) ⊆ UniformOnFun.gen 𝔖 (s, i').1 (V (s, i').2)
have rcases : ∀ (i : ι) (hi : s ⊆ t i),
  ∃ (i'_1 : ι × ι'), p i'_1.2 ∧ UniformOnFun.gen 𝔖 (t i'_1.1) (V i'_1.2) ⊆ UniformOnFun.gen 𝔖 (s, i').1 (V (s, i').2)
Tactic: rcases hex s hs with ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
t : ι → Set α
V : ι → Set (β × β)
ht : ∀ (n : ι), t n ∈ 𝔖
hmono : Monotone t
hex : ∀ s ∈ 𝔖, ∃ (n : ι), s ⊆ t n
hb : (𝓤 β).HasAntitoneBasis V
⊢ HasAntitoneBasis (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) (𝓤 (α →ᵤ[𝔖] β)) fun (n : ι) ↦ UniformOnFun.gen 𝔖 (t n) (V n)
have this : Nonempty ι
Tactic: have := hb.nonempty
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
t : ι → Set α
V : ι → Set (β × β)
ht : ∀ (n : ι), t n ∈ 𝔖
hmono : Monotone t
hex : ∀ s ∈ 𝔖, ∃ (n : ι), s ⊆ t n
hb : (𝓤 β).HasAntitoneBasis V
this : Nonempty ι
⊢ HasAntitoneBasis (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) (𝓤 (α →ᵤ[𝔖] β)) fun (n : ι) ↦ UniformOnFun.gen 𝔖 (t n) (V n)
have refine_1 : ∀ (i : ι × ι), True → ∃ (i' : ι), True ∧ UniformOnFun.gen 𝔖 (t i') (V i') ⊆ UniformOnFun.gen 𝔖 (t i.1) (V i.2)
Tactic: refine ⟨(UniformOnFun.hasBasis_uniformity_of_covering_of_basis 𝔖
    ht hmono.directed_le hex hb.1).to_hasBasis ?_ fun i _ ↦ ⟨(i, i), trivial, Subset.rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
t : ι → Set α
V : ι → Set (β × β)
ht : ∀ (n : ι), t n ∈ 𝔖
hmono : Monotone t
hex : ∀ s ∈ 𝔖, ∃ (n : ι), s ⊆ t n
hb : (𝓤 β).HasAntitoneBasis V
this : Nonempty ι
refine_1 :
  ∀ (i : ι × ι), True → ∃ (i' : ι), True ∧ UniformOnFun.gen 𝔖 (t i') (V i') ⊆ UniformOnFun.gen 𝔖 (t i.1) (V i.2)
⊢ HasAntitoneBasis (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) (𝓤 (α →ᵤ[𝔖] β)) fun (n : ι) ↦ UniformOnFun.gen 𝔖 (t n) (V n)
have refine_2 : Antitone (β := Set ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) fun (n : ι) ↦ UniformOnFun.gen 𝔖 (t n) (V n)
Tactic: refine ⟨(UniformOnFun.hasBasis_uniformity_of_covering_of_basis 𝔖
    ht hmono.directed_le hex hb.1).to_hasBasis ?_ fun i _ ↦ ⟨(i, i), trivial, Subset.rfl⟩, ?_⟩