feat: isClosed_eqLocus (leanprover-community#40712)

This PR was automatically created from PR leanprover-community#39100 by @ADedecker via a [review comment](leanprover-community#39100 (comment)) by @ADedecker.

Co-authored-by: ADedecker <48656793+ADedecker@users.noreply.github.com>

Author: 2 people

Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean

@@ -686,13 +686,22 @@ end ApplyAction
 
 theorem isClosed_ker [T1Space M₂] (f : M₁ →SL[σ₁₂] M₂) :
     IsClosed (f.ker : Set M₁) :=
-  continuous_iff_isClosed.1 (map_continuous f) _ isClosed_singleton
+  isClosed_singleton.preimage f.continuous
+
+theorem isClosed_eqLocus [T2Space M₂] (f g : M₁ →SL[σ₁₂] M₂) :
+    IsClosed (f.eqLocus g : Set M₁) :=
+  isClosed_eq f.continuous g.continuous
 
 theorem isComplete_ker {M' : Type*} [UniformSpace M'] [CompleteSpace M'] [AddCommMonoid M']
     [Module R₁ M'] [T1Space M₂] (f : M' →SL[σ₁₂] M₂) :
     IsComplete (f.ker : Set M') :=
   (isClosed_ker f).isComplete
 
+theorem isComplete_eqLocus {M' : Type*} [UniformSpace M'] [CompleteSpace M'] [AddCommMonoid M']
+    [Module R₁ M'] [T2Space M₂] (f g : M' →SL[σ₁₂] M₂) :
+    IsComplete (f.eqLocus g : Set M') :=
+  (isClosed_eqLocus f g).isComplete
+
 instance completeSpace_ker {M' : Type*} [UniformSpace M'] [CompleteSpace M']
     [AddCommMonoid M'] [Module R₁ M'] [T1Space M₂]
     (f : M' →SL[σ₁₂] M₂) : CompleteSpace f.ker :=
@@ -701,7 +710,7 @@ instance completeSpace_ker {M' : Type*} [UniformSpace M'] [CompleteSpace M']
 instance completeSpace_eqLocus {M' : Type*} [UniformSpace M'] [CompleteSpace M']
     [AddCommMonoid M'] [Module R₁ M'] [T2Space M₂]
     (f g : M' →SL[σ₁₂] M₂) : CompleteSpace (f.toLinearMap.eqLocus g.toLinearMap) :=
-  IsClosed.completeSpace_coe (hs := isClosed_eq (map_continuous f) (map_continuous g))
+  (isComplete_eqLocus f g).completeSpace_coe
 
 section