-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem uniformSpace_eq_iInf_precomp_of_cover {δ : ι → Type*} (φ : Π i, δ i → α)
    (h_cover : ∃ I : Set ι, I.Finite ∧ ⋃ i ∈ I, range (φ i) = univ) :
    𝒰(α, β, _) = ⨅ i, .comap (ofFun ∘ (· ∘ φ i) ∘ toFun) 𝒰(δ i, β, _)

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ I, I.Finite ∧ ⋃ i ∈ I, range (φ i) = univ
⊢ uniformSpace α β = ⨅ i, UniformSpace.comap (⇑ofFun ∘ (fun x => x ∘ φ i) ∘ ⇑toFun) (uniformSpace (δ i) β)

Tactic:
ext : 1

Result:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ I, I.Finite ∧ ⋃ i ∈ I, range (φ i) = univ
⊢ 𝓤 (α →ᵤ β) = 𝓤 (α →ᵤ β)

Proof state:
case h.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
I : Set ι
I_finite : I.Finite
I_cover : ⋃ i ∈ I, range (φ i) = univ
⊢ ⨅ i, comap (Prod.map (⇑ofFun ∘ (fun x => x ∘ φ i) ∘ ⇑toFun) (⇑ofFun ∘ (fun x => x ∘ φ i) ∘ ⇑toFun)) (𝓤 (δ i →ᵤ β)) ≤
    𝓤 (α →ᵤ β)

Tactic:
refine Filter.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 ↦ ?_⟩

Result:
case h.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
I : Set ι
I_finite : I.Finite
I_cover : ⋃ i ∈ I, range (φ i) = univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x✝ : (α →ᵤ β) × (α →ᵤ β)
x : α
f g : α →ᵤ β
hfg :
  (f, g) ∈
    ⋂ i,
      Prod.map (⇑ofFun ∘ (fun x => x ∘ φ ↑i) ∘ ⇑toFun) (⇑ofFun ∘ (fun x => x ∘ φ ↑i) ∘ ⇑toFun) ⁻¹'
        UniformFun.gen (δ ↑i) β (⟨I, fun x => U⟩.snd i)
⊢ (toFun (f, g).1 x, toFun (f, g).2 x) ∈ U

Proof state:
case h.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
I : Set ι
I_finite : I.Finite
I_cover : ⋃ i ∈ I, range (φ i) = univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x✝ : (α →ᵤ β) × (α →ᵤ β)
x : α
f g : α →ᵤ β
hfg :
  (f, g) ∈
    ⋂ i,
      Prod.map (⇑ofFun ∘ (fun x => x ∘ φ ↑i) ∘ ⇑toFun) (⇑ofFun ∘ (fun x => x ∘ φ ↑i) ∘ ⇑toFun) ⁻¹'
        UniformFun.gen (δ ↑i) β (⟨I, fun x => U⟩.snd i)
⊢ (toFun (f, g).1 x, toFun (f, g).2 x) ∈ U

Tactic:
rcases mem_iUnion₂.mp <| I_cover.ge <| mem_univ x with ⟨i, hi, y, rfl⟩

Result:
case h.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
I : Set ι
I_finite : I.Finite
I_cover : ⋃ i ∈ I, range (φ i) = univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x✝ : (α →ᵤ β) × (α →ᵤ β)
f g : α →ᵤ β
hfg :
  (f, g) ∈
    ⋂ i,
      Prod.map (⇑ofFun ∘ (fun x => x ∘ φ ↑i) ∘ ⇑toFun) (⇑ofFun ∘ (fun x => x ∘ φ ↑i) ∘ ⇑toFun) ⁻¹'
        UniformFun.gen (δ ↑i) β (⟨I, fun x => U⟩.snd i)
i : ι
hi : i ∈ I
y : δ i
⊢ (toFun (f, g).1 (φ i y), toFun (f, g).2 (φ i y)) ∈ U

Proof state:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ I, I.Finite ∧ ⋃ i ∈ I, range (φ i) = univ
⊢ 𝓤 (α →ᵤ β) =
    ⨅ i, comap (Prod.map (⇑ofFun ∘ (fun x => x ∘ φ i) ∘ ⇑toFun) (⇑ofFun ∘ (fun x => x ∘ φ i) ∘ ⇑toFun)) (𝓤 (δ i →ᵤ β))

Tactic:
refine le_antisymm (le_iInf fun i ↦ tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous) ?_

Result:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ I, I.Finite ∧ ⋃ i ∈ I, range (φ i) = univ
⊢ ⨅ i, comap (Prod.map (⇑ofFun ∘ (fun x => x ∘ φ i) ∘ ⇑toFun) (⇑ofFun ∘ (fun x => x ∘ φ i) ∘ ⇑toFun)) (𝓤 (δ i →ᵤ β)) ≤
    𝓤 (α →ᵤ β)

Proof state:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ I, I.Finite ∧ ⋃ i ∈ I, range (φ i) = univ
⊢ 𝓤 (α →ᵤ β) = 𝓤 (α →ᵤ β)

Tactic:
simp_rw [iInf_uniformity, uniformity_comap]

Result:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ I, I.Finite ∧ ⋃ i ∈ I, range (φ i) = univ
⊢ 𝓤 (α →ᵤ β) =
    ⨅ i, comap (Prod.map (⇑ofFun ∘ (fun x => x ∘ φ i) ∘ ⇑toFun) (⇑ofFun ∘ (fun x => x ∘ φ i) ∘ ⇑toFun)) (𝓤 (δ i →ᵤ β))

Proof state:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ I, I.Finite ∧ ⋃ i ∈ I, range (φ i) = univ
⊢ ⨅ i, comap (Prod.map (⇑ofFun ∘ (fun x => x ∘ φ i) ∘ ⇑toFun) (⇑ofFun ∘ (fun x => x ∘ φ i) ∘ ⇑toFun)) (𝓤 (δ i →ᵤ β)) ≤
    𝓤 (α →ᵤ β)

Tactic:
rcases h_cover with ⟨I, I_finite, I_cover⟩

Result:
case h.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
I : Set ι
I_finite : I.Finite
I_cover : ⋃ i ∈ I, range (φ i) = univ
⊢ ⨅ i, comap (Prod.map (⇑ofFun ∘ (fun x => x ∘ φ i) ∘ ⇑toFun) (⇑ofFun ∘ (fun x => x ∘ φ i) ∘ ⇑toFun)) (𝓤 (δ i →ᵤ β)) ≤
    𝓤 (α →ᵤ β)

Proof state:
case h.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
I : Set ι
I_finite : I.Finite
I_cover : ⋃ i ∈ I, range (φ i) = univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x✝ : (α →ᵤ β) × (α →ᵤ β)
f g : α →ᵤ β
hfg :
  (f, g) ∈
    ⋂ i,
      Prod.map (⇑ofFun ∘ (fun x => x ∘ φ ↑i) ∘ ⇑toFun) (⇑ofFun ∘ (fun x => x ∘ φ ↑i) ∘ ⇑toFun) ⁻¹'
        UniformFun.gen (δ ↑i) β (⟨I, fun x => U⟩.snd i)
i : ι
hi : i ∈ I
y : δ i
⊢ (toFun (f, g).1 (φ i y), toFun (f, g).2 (φ i y)) ∈ U

Tactic:
exact mem_iInter.mp hfg ⟨i, hi⟩ y

Result:
no goals