Extending a backward bound on a normed group homomorphism from a dense set

Possible TODO (from the PR's review, https://github.com/leanprover-community/mathlib/pull/8498 ): "This feels a lot like the second step in the proof of the Banach open mapping theorem (exists_preimage_norm_le) ... wonder if it would be possible to refactor it using one of [the lemmas in this file]."

theorem controlled_closure_of_complete {G : Type u_1} [NormedAddCommGroup G] [CompleteSpace G] {H : Type u_2} [NormedAddCommGroup H] {f : NormedAddGroupHom G H} {K : AddSubgroup H} {C : ℝ} {ε : ℝ} (hC : 0 < C) (hε : 0 < ε) (hyp : f.SurjectiveOnWith K C) : f.SurjectiveOnWith K.topologicalClosure (C + ε)

Given f : NormedAddGroupHom G H for some complete G and a subgroup K of H, if every element x of K has a preimage under f whose norm is at most C*‖x‖ then the same holds for elements of the (topological) closure of K with constant C+ε instead of C, for any positive ε.

theorem controlled_closure_range_of_complete {G : Type u_1} [NormedAddCommGroup G] [CompleteSpace G] {H : Type u_2} [NormedAddCommGroup H] {f : NormedAddGroupHom G H} {K : Type u_3} [SeminormedAddCommGroup K] {j : NormedAddGroupHom K H} (hj : ∀ (x : K), ‖j x‖ = ‖x‖) {C : ℝ} {ε : ℝ} (hC : 0 < C) (hε : 0 < ε) (hyp : ∀ (k : K), ∃ (g : G), f g = j k ∧ ‖g‖ ≤ C * ‖k‖) : f.SurjectiveOnWith j.range.topologicalClosure (C + ε)

Given f : NormedAddGroupHom G H for some complete G, if every element x of the image of an isometric immersion j : NormedAddGroupHom K H has a preimage under f whose norm is at most C*‖x‖ then the same holds for elements of the (topological) closure of this image with constant C+ε instead of C, for any positive ε. This is useful in particular if j is the inclusion of a normed group into its completion (in this case the closure is the full target group).