Module: Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : CompleteSpace 𝕜
E : Type u_2
F : Type u_3
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
A : Submodule 𝕜 E
A_closed : IsClosed[inst✝⁵] ↑A
A_cofg : A.CoFG
h_ker : Disjoint (↑u).ker A
range_u : (↑u).range = ⊤
range_u_restr : IsClosed[inst✝²] ↑(↑(u.domRestrict A)).range
⊢ IsStrictMap ⇑u ↔ IsStrictMap ⇑(u.domRestrict A)

Tactic:
rcases h_ker.exists_isCompl with ⟨S, ker_le_S, S_compl_A⟩
  have : FiniteDimensional 𝕜 S := .of_fg <| A_cofg.fg_of_isCompl S_compl_A.symm
  -- Because `u` is assumed surjective and `S ⊔ A = ⊤`, we have `map u S ⊔ map u A = ⊤`.
  -- Furthermore, because the kernel of `u` is fully contained in `S`, we can show that
  -- `map u S ⊓ map u A = ⊥`, so that `map u S` and `map u A` are in fact algebraic complements
  -- of each other.
  have uS_compl_uA : IsCompl (map u.toLinearMap S) (map u.toLinearMap A) :=
    ⟨disjoint_map_of_ker_le_left S_compl_A.disjoint ker_le_S,
      codisjoint_map (LinearMap.range_eq_top.mp range_u) S_compl_A.codisjoint⟩
  -- Because `A` (resp. `map u A`) is closed and `S` (resp `map u S`) has finite dimension,
  -- `A` and `S` (resp `map u A` and `map u S`) are in fact *topological* complements of each other.
  replace S_compl_A : IsTopCompl S A :=
    S_compl_A.symm.isTopCompl_of_finiteDimensional_quotient A_closed |>.symm
  replace uS_compl_uA : IsTopCompl (map u.toLinearMap S) (map u.toLinearMap A) :=
    uS_compl_uA.symm.isTopCompl_of_isClosed_of_finiteDimensional
      (by simpa using range_u_restr) |>.symm
  -- In particular, `S` and `map u S` are T2.
  have : T2Space (map u.toLinearMap S) := uS_compl_uA.t2Space (by simpa using range_u_restr)
  -- Thus, we have decomposed both the domain and the codomain into topological complements,
  -- and `u` preserves this decomposition, inducing maps `uₛ : S → map u S` and `uₐ : A → map u A`.
  set uₛ : S →L[𝕜] map u.toLinearMap S := u.restrict (fun _ ↦ mem_map_of_mem)
  set uₐ : A →L[𝕜] map u.toLinearMap A := u.restrict (fun _ ↦ mem_map_of_mem)
  -- Using the corresponding isomorphisms `(S × A) ≃L[𝕜] E` and `(map u S × map u A) ≃L[𝕜] F`,
  -- we have to show that the map `uₛ.prodMap uₐ : S × A → map u S × map u A` is strict
  -- if and only if `uₐ : A → map u A` is strict.
  -- This follows from `AddMonoidHom.isStrictMap_prodMap_iff`, and the fact that `uₛ` is a
  -- continuous linear map between T2 finite dimensional spaces, hence a strict map.
  set Φ : (S × A) ≃L[𝕜] E := prodEquivOfIsTopCompl S A S_compl_A
  set Ψ : (map u.toLinearMap S × map u.toLinearMap A) ≃L[𝕜] F :=
    prodEquivOfIsTopCompl _ _ uS_compl_uA
  have u_eq : u = Ψ ∘ (uₛ.prodMap uₐ) ∘ Φ.symm := by
    ext x
    simp [Φ, Ψ, uₛ, uₐ, ← map_add, projection_add_projection_eq_self]
  have u_restr_eq : u.domRestrict A = (map u.toLinearMap A).subtypeL ∘ uₐ := rfl
  suffices IsStrictMap (uₛ.prodMap uₐ) ↔ IsStrictMap uₐ by
    rwa [u_restr_eq, u_eq, ← (isEmbedding_subtypeL _).isStrictMap_iff,
      ← Ψ.isHomeomorph.isEmbedding.isStrictMap_iff,
      ← Φ.symm.isHomeomorph.isQuotientMap.isStrictMap_iff]
  simp_rw [← coe_coe, ContinuousLinearMap.coe_prodMap, LinearMap.isStrictMap_prodMap_iff, coe_coe,
    uₛ.isStrictMap_of_finiteDimensional, true_and]

Goal state after: