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
inst✝ : A.CoFG
⊢ IsStrictMap ⇑u ∧ IsClosed[inst✝³] ↑(↑u).range ↔
    IsStrictMap ⇑(u.domRestrict A) ∧ IsClosed[inst✝³] ↑(↑(u.domRestrict A)).range

Tactic:
by
  -- To reduce to step 4, we quotient by `N := A ⊓ u.ker`. Denoting by `π : E → E ⧸ N`
  -- the (automatically open) quotient map, `u` factors as `v ∘ π` with `v : E ⧸ N → F`.
  set N : Submodule 𝕜 E := A ⊓ u.ker
  set π : E →L[𝕜] E ⧸ N := N.mkQL
  set v : E ⧸ N →L[𝕜] F := N.liftQL u inf_le_right
  have π_quot : IsOpenQuotientMap π := N.isOpenQuotientMap_mkQL
  have u_eq : u = v ∘L π := rfl
  -- We also consider the submodule `B := map π A` of `E ⧸ N`. It has finite codimension and,
  -- by construction, it is disjoint from the kernel of `v`.
  set B : Submodule 𝕜 (E ⧸ N) := map N.mkQ A
  have B_cofg : B.CoFG :=
    quotientQuotientEquivQuotient N A inf_le_left |>.symm.finiteDimensional
  have v_ker : Disjoint v.ker B := by
    simp [disjoint_iff, v, B, toLinearMap_liftQL, ker_liftQ,
      map_inf_eq_map_inf_comap, comap_map_mkQ, N, inf_comm]
  -- Because `A` contains `N`, we have `A = comap π B`. In particular, `B` is closed.
  have comap_B : comap π.toLinearMap B = A := by simp [B, N, π]
  have A_mapsTo_B : MapsTo π A B := fun _ ↦ by simp [← comap_B]
  have B_closed : IsClosed (B : Set <| E ⧸ N) := by
    rwa [← π_quot.isQuotientMap.isClosed_preimage, ← π.coe_coe, ← comap_coe, comap_B]
  -- Thus, we can apply step 4 to `v` and `B`: we get that `v` is strict with closed range if
  -- and only if `v.domRestrict B` is strict with closed range.
  have step4_output : (IsStrictMap v ∧ IsClosed (v.range : Set F)) ↔
      (IsStrictMap (v.domRestrict B) ∧ IsClosed ((v.domRestrict B).range : Set F)) :=
    step4 v B B_closed v_ker
  -- Now, we wish to reduce our statement about `u` and `u.domRestrict A`
  -- to what we know about `v` and `v.domRestrict B`.
  -- First, it is clear that `range u = range v` and `map u A = map v B`.
  have range_eq : v.range = u.range := range_liftQ _ _ _
  have range_restr_eq : (v.domRestrict B).range = (u.domRestrict A).range := by
    simp [B, u_eq, π, ← map_comp]
  -- Now, recall the equality `A = comap π B`; it ensures that the restriction
  -- `π' : A → B` of the open quotient map `π` is *still* an (open) quotient map.
  set π' : A →L[𝕜] B := π.restrict A_mapsTo_B
  have π'_quot : IsOpenQuotientMap π' := by
    let φ : (N.mkQL ⁻¹' B) ≃ₜ A := .setCongr congr(SetLike.coe $comap_B)
    exact N.isOpenQuotientMap_mkQL.restrictPreimage B |>.comp
      φ.symm.isOpenQuotientMap
  -- Note that `u.domRestrict A` factors as `v.domRestrict B ∘ π'`.
  have u_restr_eq : u.domRestrict A = v.domRestrict B ∘L π' := rfl
  -- We conclude by invoking `IsQuotientMap.isStrictMap_iff` twice, to get that strictness of
  -- `u` (resp. `u.domRestrict A`) is equivalent to strictness of `v` (resp. `v.domRestrict B`).
  calc IsStrictMap u ∧ IsClosed (u.range : Set F)
      ↔ IsStrictMap v ∧ IsClosed (v.range : Set F) := by
        rw [← range_eq, u_eq, coe_comp, π_quot.isQuotientMap.isStrictMap_iff]
    _ ↔ IsStrictMap (v.domRestrict B) ∧ IsClosed ((v.domRestrict B).range : Set F) :=
        step4_output
    _ ↔ IsStrictMap (u.domRestrict A) ∧ IsClosed ((u.domRestrict A).range : Set F) := by
        rw [← range_restr_eq, u_restr_eq, coe_comp, π'_quot.isQuotientMap.isStrictMap_iff]

Goal state after: