-- Mathlib/Topology/Algebra/Module/Alternating/Topology.lean
lemma isClosed_range_toContinuousMultilinearMap [ContinuousSMul 𝕜 E] [T2Space F] :
    IsClosed (Set.range (toContinuousMultilinearMap : (E [⋀^ι]→L[𝕜] F) →
      ContinuousMultilinearMap 𝕜 (fun _ : ι ↦ E) F))

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : T2Space F
x✝³ : ι → E
x✝² x✝¹ : ι
x✝ : x✝³ x✝² = x✝³ x✝¹
⊢ IsClosed (⋂ (_ : x✝² ≠ x✝¹), {x | x x✝³ = 0})

Tactic:
refine isClosed_iInter fun _ ↦ ?_

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : T2Space F
x✝⁴ : ι → E
x✝³ x✝² : ι
x✝¹ : x✝⁴ x✝³ = x✝⁴ x✝²
x✝ : x✝³ ≠ x✝²
⊢ IsClosed {x | x x✝⁴ = 0}

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : T2Space F
x✝⁴ : ι → E
x✝³ x✝² : ι
x✝¹ : x✝⁴ x✝³ = x✝⁴ x✝²
x✝ : x✝³ ≠ x✝²
⊢ IsClosed {x | x x✝⁴ = 0}

Tactic:
exact isClosed_singleton.preimage (continuous_eval_const _)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : T2Space F
⊢ IsClosed (range toContinuousMultilinearMap)

Tactic:
simp only [range_toContinuousMultilinearMap, setOf_forall]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : T2Space F
⊢ IsClosed (⋂ i, ⋂ i_1, ⋂ i_2, ⋂ (_ : i i_1 = i i_2), ⋂ (_ : i_1 ≠ i_2), {x | x i = 0})

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : T2Space F
⊢ IsClosed (⋂ i, ⋂ i_1, ⋂ i_2, ⋂ (_ : i i_1 = i i_2), ⋂ (_ : i_1 ≠ i_2), {x | x i = 0})

Tactic:
repeat refine isClosed_iInter fun _ ↦ ?_

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : T2Space F
x✝⁴ : ι → E
x✝³ x✝² : ι
x✝¹ : x✝⁴ x✝³ = x✝⁴ x✝²
x✝ : x✝³ ≠ x✝²
⊢ IsClosed {x | x x✝⁴ = 0}