-- Mathlib/Topology/Algebra/Module/FiniteDimension.lean
theorem LinearMap.continuous_of_finiteDimensional [T2Space E] [FiniteDimensional 𝕜 E]
    (f : E →ₗ[𝕜] F') : Continuous f

Proof state:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F' : Type x
inst✝⁷ : AddCommGroup F'
inst✝⁶ : Module 𝕜 F'
inst✝⁵ : TopologicalSpace F'
inst✝⁴ : IsTopologicalAddGroup F'
inst✝³ : ContinuousSMul 𝕜 F'
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 E)) 𝕜 E := Basis.ofVectorSpace 𝕜 E
A : Continuous ⇑b.equivFun
⊢ Continuous ⇑f

Tactic:
have B : Continuous (f.comp (b.equivFun.symm : (Basis.ofVectorSpaceIndex 𝕜 E → 𝕜) →ₗ[𝕜] E)) :=
  LinearMap.continuous_on_pi _

Result:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F' : Type x
inst✝⁷ : AddCommGroup F'
inst✝⁶ : Module 𝕜 F'
inst✝⁵ : TopologicalSpace F'
inst✝⁴ : IsTopologicalAddGroup F'
inst✝³ : ContinuousSMul 𝕜 F'
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 E)) 𝕜 E := Basis.ofVectorSpace 𝕜 E
A : Continuous ⇑b.equivFun
B : Continuous ⇑(f ∘ₗ ↑b.equivFun.symm)
⊢ Continuous ⇑f

Proof state:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F' : Type x
inst✝⁷ : AddCommGroup F'
inst✝⁶ : Module 𝕜 F'
inst✝⁵ : TopologicalSpace F'
inst✝⁴ : IsTopologicalAddGroup F'
inst✝³ : ContinuousSMul 𝕜 F'
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 E)) 𝕜 E := Basis.ofVectorSpace 𝕜 E
A : Continuous ⇑b.equivFun
B : Continuous ⇑(f ∘ₗ ↑b.equivFun.symm)
this : Continuous (⇑(f ∘ₗ ↑b.equivFun.symm) ∘ ⇑b.equivFun)
⊢ Continuous ⇑f

Tactic:
convert this

Result:
case h.e'_5
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F' : Type x
inst✝⁷ : AddCommGroup F'
inst✝⁶ : Module 𝕜 F'
inst✝⁵ : TopologicalSpace F'
inst✝⁴ : IsTopologicalAddGroup F'
inst✝³ : ContinuousSMul 𝕜 F'
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 E)) 𝕜 E := Basis.ofVectorSpace 𝕜 E
A : Continuous ⇑b.equivFun
B : Continuous ⇑(f ∘ₗ ↑b.equivFun.symm)
this : Continuous (⇑(f ∘ₗ ↑b.equivFun.symm) ∘ ⇑b.equivFun)
⊢ ⇑f = ⇑(f ∘ₗ ↑b.equivFun.symm) ∘ ⇑b.equivFun

Proof state:
case h.e'_5.h
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F' : Type x
inst✝⁷ : AddCommGroup F'
inst✝⁶ : Module 𝕜 F'
inst✝⁵ : TopologicalSpace F'
inst✝⁴ : IsTopologicalAddGroup F'
inst✝³ : ContinuousSMul 𝕜 F'
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 E)) 𝕜 E := Basis.ofVectorSpace 𝕜 E
A : Continuous ⇑b.equivFun
B : Continuous ⇑(f ∘ₗ ↑b.equivFun.symm)
this : Continuous (⇑(f ∘ₗ ↑b.equivFun.symm) ∘ ⇑b.equivFun)
x : E
⊢ f x = f (b.equivFun.symm ⇑(b.repr x))

Tactic:
rw [Basis.equivFun_symm_apply, Basis.sum_repr]

Result:
no goals

Proof state:
case h.e'_5
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F' : Type x
inst✝⁷ : AddCommGroup F'
inst✝⁶ : Module 𝕜 F'
inst✝⁵ : TopologicalSpace F'
inst✝⁴ : IsTopologicalAddGroup F'
inst✝³ : ContinuousSMul 𝕜 F'
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 E)) 𝕜 E := Basis.ofVectorSpace 𝕜 E
A : Continuous ⇑b.equivFun
B : Continuous ⇑(f ∘ₗ ↑b.equivFun.symm)
this : Continuous (⇑(f ∘ₗ ↑b.equivFun.symm) ∘ ⇑b.equivFun)
⊢ ⇑f = ⇑(f ∘ₗ ↑b.equivFun.symm) ∘ ⇑b.equivFun

Tactic:
ext x

Result:
case h.e'_5.h
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F' : Type x
inst✝⁷ : AddCommGroup F'
inst✝⁶ : Module 𝕜 F'
inst✝⁵ : TopologicalSpace F'
inst✝⁴ : IsTopologicalAddGroup F'
inst✝³ : ContinuousSMul 𝕜 F'
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 E)) 𝕜 E := Basis.ofVectorSpace 𝕜 E
A : Continuous ⇑b.equivFun
B : Continuous ⇑(f ∘ₗ ↑b.equivFun.symm)
this : Continuous (⇑(f ∘ₗ ↑b.equivFun.symm) ∘ ⇑b.equivFun)
x : E
⊢ f x = (⇑(f ∘ₗ ↑b.equivFun.symm) ∘ ⇑b.equivFun) x

Proof state:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F' : Type x
inst✝⁷ : AddCommGroup F'
inst✝⁶ : Module 𝕜 F'
inst✝⁵ : TopologicalSpace F'
inst✝⁴ : IsTopologicalAddGroup F'
inst✝³ : ContinuousSMul 𝕜 F'
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 E)) 𝕜 E := Basis.ofVectorSpace 𝕜 E
⊢ Continuous ⇑f

Tactic:
have A : Continuous b.equivFun := continuous_equivFun_basis_aux b

Result:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F' : Type x
inst✝⁷ : AddCommGroup F'
inst✝⁶ : Module 𝕜 F'
inst✝⁵ : TopologicalSpace F'
inst✝⁴ : IsTopologicalAddGroup F'
inst✝³ : ContinuousSMul 𝕜 F'
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 E)) 𝕜 E := Basis.ofVectorSpace 𝕜 E
A : Continuous ⇑b.equivFun
⊢ Continuous ⇑f

Proof state:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F' : Type x
inst✝⁷ : AddCommGroup F'
inst✝⁶ : Module 𝕜 F'
inst✝⁵ : TopologicalSpace F'
inst✝⁴ : IsTopologicalAddGroup F'
inst✝³ : ContinuousSMul 𝕜 F'
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 E)) 𝕜 E := Basis.ofVectorSpace 𝕜 E
A : Continuous ⇑b.equivFun
B : Continuous ⇑(f ∘ₗ ↑b.equivFun.symm)
⊢ Continuous ⇑f

Tactic:
have :
  Continuous
    (f.comp (b.equivFun.symm : (Basis.ofVectorSpaceIndex 𝕜 E → 𝕜) →ₗ[𝕜] E) ∘ b.equivFun) :=
  B.comp A

Result:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
F' : Type x
inst✝⁷ : AddCommGroup F'
inst✝⁶ : Module 𝕜 F'
inst✝⁵ : TopologicalSpace F'
inst✝⁴ : IsTopologicalAddGroup F'
inst✝³ : ContinuousSMul 𝕜 F'
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 E)) 𝕜 E := Basis.ofVectorSpace 𝕜 E
A : Continuous ⇑b.equivFun
B : Continuous ⇑(f ∘ₗ ↑b.equivFun.symm)
this : Continuous (⇑(f ∘ₗ ↑b.equivFun.symm) ∘ ⇑b.equivFun)
⊢ Continuous ⇑f