-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem hasAntitoneBasis_uniformity {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)]
    {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)

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝² : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
t : ι → Set α
V : ι → Set (β × β)
ht : ∀ (n : ι), t n ∈ 𝔖
hmono : Monotone t
hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n
hb : (𝓤 β).HasAntitoneBasis V
this : Nonempty ι
⊢ ∀ (i : ι × ι), True → ∃ i', True ∧ UniformOnFun.gen 𝔖 (t i') (V i') ⊆ UniformOnFun.gen 𝔖 (t i.1) (V i.2)

Tactic:
rintro ⟨k, l⟩ -

Result:
case refine_1.mk
α : Type u_1
β : Type u_2
inst✝² : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
t : ι → Set α
V : ι → Set (β × β)
ht : ∀ (n : ι), t n ∈ 𝔖
hmono : Monotone t
hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n
hb : (𝓤 β).HasAntitoneBasis V
this : Nonempty ι
k l : ι
⊢ ∃ i', True ∧ UniformOnFun.gen 𝔖 (t i') (V i') ⊆ UniformOnFun.gen 𝔖 (t (k, l).1) (V (k, l).2)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
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)

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⟩, ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝² : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
t : ι → Set α
V : ι → Set (β × β)
ht : ∀ (n : ι), t n ∈ 𝔖
hmono : Monotone t
hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n
hb : (𝓤 β).HasAntitoneBasis V
this : Nonempty ι
⊢ ∀ (i : ι × ι), True → ∃ i', True ∧ UniformOnFun.gen 𝔖 (t i') (V i') ⊆ UniformOnFun.gen 𝔖 (t i.1) (V i.2)

case refine_2
α : Type u_1
β : Type u_2
inst✝² : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
t : ι → Set α
V : ι → Set (β × β)
ht : ∀ (n : ι), t n ∈ 𝔖
hmono : Monotone t
hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n
hb : (𝓤 β).HasAntitoneBasis V
this : Nonempty ι
⊢ Antitone fun n => UniformOnFun.gen 𝔖 (t n) (V n)

Proof state:
case refine_1.mk.intro.intro
α : Type u_1
β : Type u_2
inst✝² : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
t : ι → Set α
V : ι → Set (β × β)
ht : ∀ (n : ι), t n ∈ 𝔖
hmono : Monotone t
hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n
hb : (𝓤 β).HasAntitoneBasis V
this : Nonempty ι
k l n : ι
hkn : k ≤ n
hln : l ≤ n
⊢ ∃ i', True ∧ UniformOnFun.gen 𝔖 (t i') (V i') ⊆ UniformOnFun.gen 𝔖 (t (k, l).1) (V (k, l).2)

Tactic:
exact ⟨n, trivial, UniformOnFun.gen_mono (hmono hkn) (hb.2 <| hln)⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
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)

Tactic:
have := hb.nonempty

Result:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
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)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝² : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
t : ι → Set α
V : ι → Set (β × β)
ht : ∀ (n : ι), t n ∈ 𝔖
hmono : Monotone t
hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n
hb : (𝓤 β).HasAntitoneBasis V
this : Nonempty ι
⊢ Antitone fun n => UniformOnFun.gen 𝔖 (t n) (V n)

Tactic:
exact fun k l h ↦ UniformOnFun.gen_mono (hmono h) (hb.2 h)

Result:
no goals