-- Mathlib/Topology/Algebra/Module/StrongTopology.lean
theorem nhds_zero_eq_of_basis [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E))
    {ι : Type*} {p : ι → Prop} {b : ι → Set F} (h : (𝓝 0 : Filter F).HasBasis p b) :
    𝓝 (0 : UniformConvergenceCLM σ F 𝔖) =
      ⨅ (s : Set E) (_ : s ∈ 𝔖) (i : ι) (_ : p i),
        𝓟 {f : UniformConvergenceCLM σ F 𝔖 | MapsTo f s (b i)}

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
ι : Type u_5
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this✝ : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
this : UniformAddGroup F
⊢ comap (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe)
      (⨅ s ∈ 𝔖,
        ⨅ i,
          ⨅ (_ : p i),
            𝓟
              {g |
                ∀ x ∈ s,
                  ((UniformOnFun.toFun 𝔖) ((⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) 0) x, (UniformOnFun.toFun 𝔖) g x) ∈
                    {x | x.2 - x.1 ∈ b i}}) =
    ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {f | MapsTo (⇑f) s (b i)}

Tactic:
simp [MapsTo]

Result:
no goals

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
ι : Type u_5
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
⊢ 𝓝 0 = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {f | MapsTo (⇑f) s (b i)}

Tactic:
letI : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F

Result:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
ι : Type u_5
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
⊢ 𝓝 0 = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {f | MapsTo (⇑f) s (b i)}

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
ι : Type u_5
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
⊢ 𝓝 0 = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {f | MapsTo (⇑f) s (b i)}

Tactic:
haveI : UniformAddGroup F := uniformAddGroup_of_addCommGroup

Result:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
ι : Type u_5
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this✝ : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
this : UniformAddGroup F
⊢ 𝓝 0 = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {f | MapsTo (⇑f) s (b i)}

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
ι : Type u_5
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this✝ : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
this : UniformAddGroup F
⊢ 𝓝 0 = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {f | MapsTo (⇑f) s (b i)}

Tactic:
rw [(isEmbedding_coeFn σ F 𝔖).isInducing.nhds_eq_comap,
  UniformOnFun.nhds_eq_of_basis _ _ h.uniformity_of_nhds_zero]

Result:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
ι : Type u_5
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this✝ : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
this : UniformAddGroup F
⊢ comap (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe)
      (⨅ s ∈ 𝔖,
        ⨅ i,
          ⨅ (_ : p i),
            𝓟
              {g |
                ∀ x ∈ s,
                  ((UniformOnFun.toFun 𝔖) ((⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) 0) x, (UniformOnFun.toFun 𝔖) g x) ∈
                    {x | x.2 - x.1 ∈ b i}}) =
    ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {f | MapsTo (⇑f) s (b i)}