-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem uniformSpace_eq_inf_precomp_of_cover {δ₁ δ₂ : Type*} (φ₁ : δ₁ → α) (φ₂ : δ₂ → α)
    (h_cover : range φ₁ ∪ range φ₂ = univ) :
    𝒰(α, β, _) =
      .comap (ofFun ∘ (· ∘ φ₁) ∘ toFun) 𝒰(δ₁, β, _) ⊓
      .comap (ofFun ∘ (· ∘ φ₂) ∘ toFun) 𝒰(δ₂, β, _)

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ 𝓤 (α →ᵤ β) = 𝓤 (α →ᵤ β)

Tactic:
refine le_antisymm (le_inf ?_ ?_) ?_

Result:
case h.refine_1
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ 𝓤 (α →ᵤ β) ≤ 𝓤 (α →ᵤ β)

case h.refine_2
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ 𝓤 (α →ᵤ β) ≤ 𝓤 (α →ᵤ β)

case h.refine_3
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ 𝓤 (α →ᵤ β) ≤ 𝓤 (α →ᵤ β)

Proof state:
case h.refine_3
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ 𝓤 (α →ᵤ β) ≤ 𝓤 (α →ᵤ β)

Tactic:
refine
  (UniformFun.hasBasis_uniformity δ₁ β |>.comap _).inf
  (UniformFun.hasBasis_uniformity δ₂ β |>.comap _)
    |>.le_basis_iff (UniformFun.hasBasis_uniformity α β) |>.mpr fun U hU ↦
    ⟨⟨U, U⟩, ⟨hU, hU⟩, fun ⟨f, g⟩ hfg x ↦ ?_⟩

Result:
case h.refine_3
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x✝ : (α →ᵤ β) × (α →ᵤ β)
x : α
f g : α →ᵤ β
hfg :
  (f, g) ∈
    (fun p => ((⇑ofFun ∘ (fun x => x ∘ φ₁) ∘ ⇑toFun) p.1, (⇑ofFun ∘ (fun x => x ∘ φ₁) ∘ ⇑toFun) p.2)) ⁻¹'
        UniformFun.gen δ₁ β (U, U).1 ∩
      (fun p => ((⇑ofFun ∘ (fun x => x ∘ φ₂) ∘ ⇑toFun) p.1, (⇑ofFun ∘ (fun x => x ∘ φ₂) ∘ ⇑toFun) p.2)) ⁻¹'
        UniformFun.gen δ₂ β (U, U).2
⊢ (toFun (f, g).1 x, toFun (f, g).2 x) ∈ U

Proof state:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ uniformSpace α β =
    UniformSpace.comap (⇑ofFun ∘ (fun x => x ∘ φ₁) ∘ ⇑toFun) (uniformSpace δ₁ β) ⊓
      UniformSpace.comap (⇑ofFun ∘ (fun x => x ∘ φ₂) ∘ ⇑toFun) (uniformSpace δ₂ β)

Tactic:
ext : 1

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ 𝓤 (α →ᵤ β) = 𝓤 (α →ᵤ β)

Proof state:
case h.refine_3.inr.intro
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x✝ : (α →ᵤ β) × (α →ᵤ β)
f g : α →ᵤ β
hfg :
  (f, g) ∈
    (fun p => ((⇑ofFun ∘ (fun x => x ∘ φ₁) ∘ ⇑toFun) p.1, (⇑ofFun ∘ (fun x => x ∘ φ₁) ∘ ⇑toFun) p.2)) ⁻¹'
        UniformFun.gen δ₁ β (U, U).1 ∩
      (fun p => ((⇑ofFun ∘ (fun x => x ∘ φ₂) ∘ ⇑toFun) p.1, (⇑ofFun ∘ (fun x => x ∘ φ₂) ∘ ⇑toFun) p.2)) ⁻¹'
        UniformFun.gen δ₂ β (U, U).2
y : δ₂
⊢ (toFun (f, g).1 (φ₂ y), toFun (f, g).2 (φ₂ y)) ∈ U

Tactic:
exact hfg.2 y

Result:
no goals

Proof state:
case h.refine_3.inl.intro
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x✝ : (α →ᵤ β) × (α →ᵤ β)
f g : α →ᵤ β
hfg :
  (f, g) ∈
    (fun p => ((⇑ofFun ∘ (fun x => x ∘ φ₁) ∘ ⇑toFun) p.1, (⇑ofFun ∘ (fun x => x ∘ φ₁) ∘ ⇑toFun) p.2)) ⁻¹'
        UniformFun.gen δ₁ β (U, U).1 ∩
      (fun p => ((⇑ofFun ∘ (fun x => x ∘ φ₂) ∘ ⇑toFun) p.1, (⇑ofFun ∘ (fun x => x ∘ φ₂) ∘ ⇑toFun) p.2)) ⁻¹'
        UniformFun.gen δ₂ β (U, U).2
y : δ₁
⊢ (toFun (f, g).1 (φ₁ y), toFun (f, g).2 (φ₁ y)) ∈ U

Tactic:
exact hfg.1 y

Result:
no goals

Proof state:
case h.refine_1
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ 𝓤 (α →ᵤ β) ≤ 𝓤 (α →ᵤ β)

Tactic:
exact tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous

Result:
no goals

Proof state:
case h.refine_2
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ 𝓤 (α →ᵤ β) ≤ 𝓤 (α →ᵤ β)

Tactic:
exact tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous

Result:
no goals

Proof state:
case h.refine_3
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x✝ : (α →ᵤ β) × (α →ᵤ β)
x : α
f g : α →ᵤ β
hfg :
  (f, g) ∈
    (fun p => ((⇑ofFun ∘ (fun x => x ∘ φ₁) ∘ ⇑toFun) p.1, (⇑ofFun ∘ (fun x => x ∘ φ₁) ∘ ⇑toFun) p.2)) ⁻¹'
        UniformFun.gen δ₁ β (U, U).1 ∩
      (fun p => ((⇑ofFun ∘ (fun x => x ∘ φ₂) ∘ ⇑toFun) p.1, (⇑ofFun ∘ (fun x => x ∘ φ₂) ∘ ⇑toFun) p.2)) ⁻¹'
        UniformFun.gen δ₂ β (U, U).2
⊢ (toFun (f, g).1 x, toFun (f, g).2 x) ∈ U

Tactic:
rcases h_cover.ge <| mem_univ x with (⟨y, rfl⟩|⟨y, rfl⟩)

Result:
case h.refine_3.inl.intro
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x✝ : (α →ᵤ β) × (α →ᵤ β)
f g : α →ᵤ β
hfg :
  (f, g) ∈
    (fun p => ((⇑ofFun ∘ (fun x => x ∘ φ₁) ∘ ⇑toFun) p.1, (⇑ofFun ∘ (fun x => x ∘ φ₁) ∘ ⇑toFun) p.2)) ⁻¹'
        UniformFun.gen δ₁ β (U, U).1 ∩
      (fun p => ((⇑ofFun ∘ (fun x => x ∘ φ₂) ∘ ⇑toFun) p.1, (⇑ofFun ∘ (fun x => x ∘ φ₂) ∘ ⇑toFun) p.2)) ⁻¹'
        UniformFun.gen δ₂ β (U, U).2
y : δ₁
⊢ (toFun (f, g).1 (φ₁ y), toFun (f, g).2 (φ₁ y)) ∈ U

case h.refine_3.inr.intro
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x✝ : (α →ᵤ β) × (α →ᵤ β)
f g : α →ᵤ β
hfg :
  (f, g) ∈
    (fun p => ((⇑ofFun ∘ (fun x => x ∘ φ₁) ∘ ⇑toFun) p.1, (⇑ofFun ∘ (fun x => x ∘ φ₁) ∘ ⇑toFun) p.2)) ⁻¹'
        UniformFun.gen δ₁ β (U, U).1 ∩
      (fun p => ((⇑ofFun ∘ (fun x => x ∘ φ₂) ∘ ⇑toFun) p.1, (⇑ofFun ∘ (fun x => x ∘ φ₂) ∘ ⇑toFun) p.2)) ⁻¹'
        UniformFun.gen δ₂ β (U, U).2
y : δ₂
⊢ (toFun (f, g).1 (φ₂ y), toFun (f, g).2 (φ₂ y)) ∈ U