-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem hasBasis_uniformity_of_covering_of_basis {ι ι' : Type*} [Nonempty ι]
    {t : ι → Set α} {p : ι' → Prop} {V : ι' → Set (β × β)} (ht : ∀ i, t i ∈ 𝔖)
    (hdir : Directed (· ⊆ ·) 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)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst✝ : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun x1 x2 => x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ i, s ⊆ t i
hb : (𝓤 β).HasBasis p V
hne : 𝔖.Nonempty
hd : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖
⊢ (𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun i => p i.2) fun i => UniformOnFun.gen 𝔖 (t i.1) (V 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⟩

Result:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst✝ : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun x1 x2 => x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ i, s ⊆ t i
hb : (𝓤 β).HasBasis p V
hne : 𝔖.Nonempty
hd : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖
x✝¹ : Set α × ι'
s : Set α
i' : ι'
x✝ : (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)

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst✝ : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun x1 x2 => 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₂
i : ι
hi₁ : t i₁ ⊆ t i
hi₂ : t i₂ ⊆ t i
⊢ ∃ z ∈ 𝔖, (fun x1 x2 => x1 ⊆ x2) s₁ z ∧ (fun x1 x2 => x1 ⊆ x2) s₂ z

Tactic:
exact ⟨t i, ht _, his₁.trans hi₁, his₂.trans hi₂⟩

Result:
no goals

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst✝ : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun x1 x2 => x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ i, s ⊆ t i
hb : (𝓤 β).HasBasis p V
hne : 𝔖.Nonempty
hd : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖
x✝¹ : Set α × ι'
s : Set α
i' : ι'
x✝ : (s, i').1 ∈ 𝔖 ∧ p (s, i').2
hs : (s, i').1 ∈ 𝔖
hi' : p (s, i').2
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:
exact ⟨(i, i'), hi', UniformOnFun.gen_mono hi Subset.rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst✝ : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun x1 x2 => x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ i, s ⊆ t i
hb : (𝓤 β).HasBasis p V
hne : 𝔖.Nonempty
hd : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖
x✝¹ : Set α × ι'
s : Set α
i' : ι'
x✝ : (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:
rcases hex s hs with ⟨i, hi⟩

Result:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst✝ : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun x1 x2 => x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ i, s ⊆ t i
hb : (𝓤 β).HasBasis p V
hne : 𝔖.Nonempty
hd : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖
x✝¹ : Set α × ι'
s : Set α
i' : ι'
x✝ : (s, i').1 ∈ 𝔖 ∧ p (s, i').2
hs : (s, i').1 ∈ 𝔖
hi' : p (s, i').2
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)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst✝ : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun x1 x2 => 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 => x1 ⊆ x2) s₁ z ∧ (fun x1 x2 => x1 ⊆ x2) s₂ z

Tactic:
rcases hex s₁ hs₁, hex s₂ hs₂ with ⟨⟨i₁, his₁⟩, i₂, his₂⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst✝ : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun x1 x2 => 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 => x1 ⊆ x2) s₁ z ∧ (fun x1 x2 => x1 ⊆ x2) s₂ z

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst✝ : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun x1 x2 => 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)

Tactic:
have hne : 𝔖.Nonempty := (range_nonempty t).mono (range_subset_iff.2 ht)

Result:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst✝ : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun x1 x2 => 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)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst✝ : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun x1 x2 => 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 => x1 ⊆ x2) s₁ z ∧ (fun x1 x2 => x1 ⊆ x2) s₂ z

Tactic:
rcases hdir i₁ i₂ with ⟨i, hi₁, hi₂⟩

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst✝ : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun x1 x2 => 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₂
i : ι
hi₁ : t i₁ ⊆ t i
hi₂ : t i₂ ⊆ t i
⊢ ∃ z ∈ 𝔖, (fun x1 x2 => x1 ⊆ x2) s₁ z ∧ (fun x1 x2 => x1 ⊆ x2) s₂ z