Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F✝ : Type u_4
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : (i : ι) → TopologicalSpace (E i)
inst✝¹² : (i : ι) → AddCommGroup (E i)
inst✝¹¹ : (i : ι) → Module 𝕜 (E i)
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜 F✝
inst✝⁸ : UniformSpace F✝
inst✝⁷ : IsUniformAddGroup F✝
inst✝⁶ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
h : IsCoherentWith {s | IsVonNBounded 𝕜 s}
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : UniformSpace F
inst✝² : IsUniformAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
hF : T2Space F
H :
  ∀ {m : (i : ι) → E i},
    Continuous[topologicalSpace ((i : ι) → E i) F {s | IsVonNBounded 𝕜 s}, inst✝³.toTopologicalSpace] fun f ↦
      (toFun {s | IsVonNBounded 𝕜 s}) f m
⊢ IsComplete
    ({a | Continuous[Pi.topologicalSpace, inst✝³.toTopologicalSpace] ((toFun {s | IsVonNBounded 𝕜 s}) a)} ∩
      ((⋂ i,
          ⋂ i_1,
            ⋂ i_2,
              ⋂ i_3,
                {x |
                  (toFun {s | IsVonNBounded 𝕜 s}) x (update i i_1 (i_2 + i_3)) =
                    (toFun {s | IsVonNBounded 𝕜 s}) x (update i i_1 i_2) +
                      (toFun {s | IsVonNBounded 𝕜 s}) x (update i i_1 i_3)}) ∩
        ⋂ i,
          ⋂ i_1,
            ⋂ i_2,
              ⋂ i_3,
                {x |
                  (toFun {s | IsVonNBounded 𝕜 s}) x (update i i_1 (i_2 • i_3)) =
                    i_2 • (toFun {s | IsVonNBounded 𝕜 s}) x (update i i_1 i_3)}))

Tactic:
apply_rules [IsClosed.isComplete, IsClosed.inter]

Goal state after:
case h₁
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F✝ : Type u_4
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : (i : ι) → TopologicalSpace (E i)
inst✝¹² : (i : ι) → AddCommGroup (E i)
inst✝¹¹ : (i : ι) → Module 𝕜 (E i)
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜 F✝
inst✝⁸ : UniformSpace F✝
inst✝⁷ : IsUniformAddGroup F✝
inst✝⁶ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
h : IsCoherentWith {s | IsVonNBounded 𝕜 s}
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : UniformSpace F
inst✝² : IsUniformAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
hF : T2Space F
H :
  ∀ {m : (i : ι) → E i},
    Continuous[topologicalSpace ((i : ι) → E i) F {s | IsVonNBounded 𝕜 s}, inst✝³.toTopologicalSpace] fun f ↦
      (toFun {s | IsVonNBounded 𝕜 s}) f m
⊢ IsClosed[(uniformSpace ((i : ι) → E i) F {s | IsVonNBounded 𝕜 s}).toTopologicalSpace]
    {a | Continuous[Pi.topologicalSpace, inst✝³.toTopologicalSpace] ((toFun {s | IsVonNBounded 𝕜 s}) a)}

case h₂.h₁
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F✝ : Type u_4
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : (i : ι) → TopologicalSpace (E i)
inst✝¹² : (i : ι) → AddCommGroup (E i)
inst✝¹¹ : (i : ι) → Module 𝕜 (E i)
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜 F✝
inst✝⁸ : UniformSpace F✝
inst✝⁷ : IsUniformAddGroup F✝
inst✝⁶ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
h : IsCoherentWith {s | IsVonNBounded 𝕜 s}
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : UniformSpace F
inst✝² : IsUniformAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
hF : T2Space F
H :
  ∀ {m : (i : ι) → E i},
    Continuous[topologicalSpace ((i : ι) → E i) F {s | IsVonNBounded 𝕜 s}, inst✝³.toTopologicalSpace] fun f ↦
      (toFun {s | IsVonNBounded 𝕜 s}) f m
⊢ IsClosed[(uniformSpace ((i : ι) → E i) F {s | IsVonNBounded 𝕜 s}).toTopologicalSpace]
    (⋂ i,
      ⋂ i_1,
        ⋂ i_2,
          ⋂ i_3,
            {x |
              (toFun {s | IsVonNBounded 𝕜 s}) x (update i i_1 (i_2 + i_3)) =
                (toFun {s | IsVonNBounded 𝕜 s}) x (update i i_1 i_2) +
                  (toFun {s | IsVonNBounded 𝕜 s}) x (update i i_1 i_3)})

case h₂.h₂
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F✝ : Type u_4
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : (i : ι) → TopologicalSpace (E i)
inst✝¹² : (i : ι) → AddCommGroup (E i)
inst✝¹¹ : (i : ι) → Module 𝕜 (E i)
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜 F✝
inst✝⁸ : UniformSpace F✝
inst✝⁷ : IsUniformAddGroup F✝
inst✝⁶ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
h : IsCoherentWith {s | IsVonNBounded 𝕜 s}
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : UniformSpace F
inst✝² : IsUniformAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
hF : T2Space F
H :
  ∀ {m : (i : ι) → E i},
    Continuous[topologicalSpace ((i : ι) → E i) F {s | IsVonNBounded 𝕜 s}, inst✝³.toTopologicalSpace] fun f ↦
      (toFun {s | IsVonNBounded 𝕜 s}) f m
⊢ IsClosed[(uniformSpace ((i : ι) → E i) F {s | IsVonNBounded 𝕜 s}).toTopologicalSpace]
    (⋂ i,
      ⋂ i_1,
        ⋂ i_2,
          ⋂ i_3,
            {x |
              (toFun {s | IsVonNBounded 𝕜 s}) x (update i i_1 (i_2 • i_3)) =
                i_2 • (toFun {s | IsVonNBounded 𝕜 s}) x (update i i_1 i_3)})