-- Mathlib/Analysis/Normed/Operator/Banach.lean
theorem LinearMap.continuous_of_isClosed_graph (hg : IsClosed (g.graph : Set <| E × F)) :
    Continuous g

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : IsClosed ↑g.graph
this✝ : CompleteSpace ↥g.graph := completeSpace_coe_iff_isComplete.mpr (IsClosed.isComplete hg)
φ₀ : E →ₗ[𝕜] E × F := id.prod g
this : LeftInverse Prod.fst ⇑φ₀
⊢ Continuous ⇑g

Tactic:
let φ : E ≃ₗ[𝕜] g.graph :=
  (LinearEquiv.ofLeftInverse this).trans (LinearEquiv.ofEq _ _ g.graph_eq_range_prod.symm)

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : IsClosed ↑g.graph
this✝ : CompleteSpace ↥g.graph := completeSpace_coe_iff_isComplete.mpr (IsClosed.isComplete hg)
φ₀ : E →ₗ[𝕜] E × F := id.prod g
this : LeftInverse Prod.fst ⇑φ₀
φ : E ≃ₗ[𝕜] ↥g.graph := LinearEquiv.ofLeftInverse this ≪≫ₗ LinearEquiv.ofEq (range φ₀) g.graph ⋯
⊢ Continuous ⇑g

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : IsClosed ↑g.graph
this✝ : CompleteSpace ↥g.graph := completeSpace_coe_iff_isComplete.mpr (IsClosed.isComplete hg)
φ₀ : E →ₗ[𝕜] E × F := id.prod g
this : LeftInverse Prod.fst ⇑φ₀
φ : E ≃ₗ[𝕜] ↥g.graph := LinearEquiv.ofLeftInverse this ≪≫ₗ LinearEquiv.ofEq (range φ₀) g.graph ⋯
⊢ Continuous ⇑g

Tactic:
let ψ : g.graph ≃L[𝕜] E :=
  φ.symm.toContinuousLinearEquivOfContinuous continuous_subtype_val.fst

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : IsClosed ↑g.graph
this✝ : CompleteSpace ↥g.graph := completeSpace_coe_iff_isComplete.mpr (IsClosed.isComplete hg)
φ₀ : E →ₗ[𝕜] E × F := id.prod g
this : LeftInverse Prod.fst ⇑φ₀
φ : E ≃ₗ[𝕜] ↥g.graph := LinearEquiv.ofLeftInverse this ≪≫ₗ LinearEquiv.ofEq (range φ₀) g.graph ⋯
ψ : ↥g.graph ≃L[𝕜] E := φ.symm.toContinuousLinearEquivOfContinuous ⋯
⊢ Continuous ⇑g

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : IsClosed ↑g.graph
this✝ : CompleteSpace ↥g.graph := completeSpace_coe_iff_isComplete.mpr (IsClosed.isComplete hg)
φ₀ : E →ₗ[𝕜] E × F := id.prod g
this : LeftInverse Prod.fst ⇑φ₀
φ : E ≃ₗ[𝕜] ↥g.graph := LinearEquiv.ofLeftInverse this ≪≫ₗ LinearEquiv.ofEq (range φ₀) g.graph ⋯
ψ : ↥g.graph ≃L[𝕜] E := φ.symm.toContinuousLinearEquivOfContinuous ⋯
⊢ Continuous ⇑g

Tactic:
exact (continuous_subtype_val.comp ψ.symm.continuous).snd

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : IsClosed ↑g.graph
⊢ Continuous ⇑g

Tactic:
letI : CompleteSpace g.graph := completeSpace_coe_iff_isComplete.mpr hg.isComplete

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : IsClosed ↑g.graph
this : CompleteSpace ↥g.graph := completeSpace_coe_iff_isComplete.mpr (IsClosed.isComplete hg)
⊢ Continuous ⇑g

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : IsClosed ↑g.graph
this : CompleteSpace ↥g.graph := completeSpace_coe_iff_isComplete.mpr (IsClosed.isComplete hg)
φ₀ : E →ₗ[𝕜] E × F := id.prod g
⊢ Continuous ⇑g

Tactic:
have : Function.LeftInverse Prod.fst φ₀ := fun x => rfl

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : IsClosed ↑g.graph
this✝ : CompleteSpace ↥g.graph := completeSpace_coe_iff_isComplete.mpr (IsClosed.isComplete hg)
φ₀ : E →ₗ[𝕜] E × F := id.prod g
this : LeftInverse Prod.fst ⇑φ₀
⊢ Continuous ⇑g

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : IsClosed ↑g.graph
this : CompleteSpace ↥g.graph := completeSpace_coe_iff_isComplete.mpr (IsClosed.isComplete hg)
⊢ Continuous ⇑g

Tactic:
let φ₀ : E →ₗ[𝕜] E × F := LinearMap.id.prod g

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : IsClosed ↑g.graph
this : CompleteSpace ↥g.graph := completeSpace_coe_iff_isComplete.mpr (IsClosed.isComplete hg)
φ₀ : E →ₗ[𝕜] E × F := id.prod g
⊢ Continuous ⇑g