-- Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean
/-- Corollary of the **Hahn-Banach theorem**: if `f : p → F` is a continuous linear map
from a submodule of a normed space `E` over `𝕜`, `𝕜 = ℝ` or `𝕜 = ℂ`,
with a finite dimensional range, then `f` admits an extension to a continuous linear map `E → F`.

Note that contrary to the case `F = 𝕜`, see `exists_extension_norm_eq`,
we provide no estimates on the norm of the extension.
-/
lemma ContinuousLinearMap.exist_extension_of_finiteDimensional_range {p : Submodule 𝕜 E}
    (f : p →L[𝕜] F) [FiniteDimensional 𝕜 (LinearMap.range f)] :
    ∃ g : E →L[𝕜] F, f = g.comp p.subtypeL

Proof state:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : Submodule 𝕜 E
f : ↥p →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(LinearMap.range f)
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
b : Basis (Fin (finrank 𝕜 ↥(LinearMap.range f))) 𝕜 ↥(LinearMap.range f) := finBasis 𝕜 ↥(LinearMap.range f)
e : ↥(LinearMap.range f) ≃L[𝕜] Fin (finrank 𝕜 ↥(LinearMap.range f)) → 𝕜 := b.equivFunL
fi : Fin (finrank 𝕜 ↥(LinearMap.range f)) → ↥p →L[𝕜] 𝕜 :=
  fun i => (LinearMap.toContinuousLinearMap (b.coord i)).comp (f.codRestrict (LinearMap.range f) ⋯)
gi : Fin (finrank 𝕜 ↥(LinearMap.range f)) → E →L[𝕜] 𝕜
hgf : ∀ (i : Fin (finrank 𝕜 ↥(LinearMap.range f))) (x : ↥p), (gi i) ↑x = (fi i) x
a✝ : ∀ (i : Fin (finrank 𝕜 ↥(LinearMap.range f))), ‖gi i‖ = ‖fi i‖
⊢ f = ((LinearMap.range f).subtypeL.comp ((↑e.symm).comp (pi gi))).comp p.subtypeL

Tactic:
ext x

Result:
case h.h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : Submodule 𝕜 E
f : ↥p →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(LinearMap.range f)
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
b : Basis (Fin (finrank 𝕜 ↥(LinearMap.range f))) 𝕜 ↥(LinearMap.range f) := finBasis 𝕜 ↥(LinearMap.range f)
e : ↥(LinearMap.range f) ≃L[𝕜] Fin (finrank 𝕜 ↥(LinearMap.range f)) → 𝕜 := b.equivFunL
fi : Fin (finrank 𝕜 ↥(LinearMap.range f)) → ↥p →L[𝕜] 𝕜 :=
  fun i => (LinearMap.toContinuousLinearMap (b.coord i)).comp (f.codRestrict (LinearMap.range f) ⋯)
gi : Fin (finrank 𝕜 ↥(LinearMap.range f)) → E →L[𝕜] 𝕜
hgf : ∀ (i : Fin (finrank 𝕜 ↥(LinearMap.range f))) (x : ↥p), (gi i) ↑x = (fi i) x
a✝ : ∀ (i : Fin (finrank 𝕜 ↥(LinearMap.range f))), ‖gi i‖ = ‖fi i‖
x : ↥p
⊢ f x = (((LinearMap.range f).subtypeL.comp ((↑e.symm).comp (pi gi))).comp p.subtypeL) x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : Submodule 𝕜 E
f : ↥p →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(LinearMap.range f)
⊢ ∃ g, f = g.comp p.subtypeL

Tactic:
letI : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : Submodule 𝕜 E
f : ↥p →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(LinearMap.range f)
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ ∃ g, f = g.comp p.subtypeL

Proof state:
case h.h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : Submodule 𝕜 E
f : ↥p →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(LinearMap.range f)
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
b : Basis (Fin (finrank 𝕜 ↥(LinearMap.range f))) 𝕜 ↥(LinearMap.range f) := finBasis 𝕜 ↥(LinearMap.range f)
e : ↥(LinearMap.range f) ≃L[𝕜] Fin (finrank 𝕜 ↥(LinearMap.range f)) → 𝕜 := b.equivFunL
fi : Fin (finrank 𝕜 ↥(LinearMap.range f)) → ↥p →L[𝕜] 𝕜 :=
  fun i => (LinearMap.toContinuousLinearMap (b.coord i)).comp (f.codRestrict (LinearMap.range f) ⋯)
gi : Fin (finrank 𝕜 ↥(LinearMap.range f)) → E →L[𝕜] 𝕜
hgf : ∀ (i : Fin (finrank 𝕜 ↥(LinearMap.range f))) (x : ↥p), (gi i) ↑x = (fi i) x
a✝ : ∀ (i : Fin (finrank 𝕜 ↥(LinearMap.range f))), ‖gi i‖ = ‖fi i‖
x : ↥p
⊢ f x = (((LinearMap.range f).subtypeL.comp ((↑e.symm).comp (pi gi))).comp p.subtypeL) x

Tactic:
simp [fi, e, hgf]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : Submodule 𝕜 E
f : ↥p →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(LinearMap.range f)
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
b : Basis (Fin (finrank 𝕜 ↥(LinearMap.range f))) 𝕜 ↥(LinearMap.range f) := finBasis 𝕜 ↥(LinearMap.range f)
e : ↥(LinearMap.range f) ≃L[𝕜] Fin (finrank 𝕜 ↥(LinearMap.range f)) → 𝕜 := b.equivFunL
⊢ ∃ g, f = g.comp p.subtypeL

Tactic:
set fi := fun i ↦ (LinearMap.toContinuousLinearMap (b.coord i)).comp
  (f.codRestrict _ <| LinearMap.mem_range_self _)

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : Submodule 𝕜 E
f : ↥p →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(LinearMap.range f)
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
b : Basis (Fin (finrank 𝕜 ↥(LinearMap.range f))) 𝕜 ↥(LinearMap.range f) := finBasis 𝕜 ↥(LinearMap.range f)
e : ↥(LinearMap.range f) ≃L[𝕜] Fin (finrank 𝕜 ↥(LinearMap.range f)) → 𝕜 := b.equivFunL
fi : Fin (finrank 𝕜 ↥(LinearMap.range f)) → ↥p →L[𝕜] 𝕜 :=
  fun i => (LinearMap.toContinuousLinearMap (b.coord i)).comp (f.codRestrict (LinearMap.range f) ⋯)
⊢ ∃ g, f = g.comp p.subtypeL

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : Submodule 𝕜 E
f : ↥p →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(LinearMap.range f)
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ ∃ g, f = g.comp p.subtypeL

Tactic:
set b := Module.finBasis 𝕜 (LinearMap.range f)

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : Submodule 𝕜 E
f : ↥p →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(LinearMap.range f)
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
b : Basis (Fin (finrank 𝕜 ↥(LinearMap.range f))) 𝕜 ↥(LinearMap.range f) := finBasis 𝕜 ↥(LinearMap.range f)
⊢ ∃ g, f = g.comp p.subtypeL