-- Mathlib/Topology/Algebra/Module/FiniteDimension.lean
theorem continuous_equivFun_basis_aux [T2Space E] {ι : Type v} [Fintype ι]
    (ξ : Basis ι 𝕜 E) : Continuous ξ.equivFun

Proof state:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [inst_5 : T2Space E] {ι : Type v}
    [inst_6 : Fintype ι] (ξ : Basis ι 𝕜 E),
    let this := IsTopologicalAddGroup.toUniformSpace E;
    let this := ⋯;
    Fintype.card ι = n → Continuous ⇑ξ.equivFun
E : Type v
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝¹ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E := uniformAddGroup_of_addCommGroup
hn : Fintype.card ι = n + 1
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 ↥s = n → IsClosed ↑s
⊢ ∀ (f : E →ₗ[𝕜] 𝕜), Continuous ⇑f

Tactic:
intro f

Result:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [inst_5 : T2Space E] {ι : Type v}
    [inst_6 : Fintype ι] (ξ : Basis ι 𝕜 E),
    let this := IsTopologicalAddGroup.toUniformSpace E;
    let this := ⋯;
    Fintype.card ι = n → Continuous ⇑ξ.equivFun
E : Type v
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝¹ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E := uniformAddGroup_of_addCommGroup
hn : Fintype.card ι = n + 1
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 ↥s = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
⊢ Continuous ⇑f

Proof state:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [inst_5 : T2Space E] {ι : Type v}
    [inst_6 : Fintype ι] (ξ : Basis ι 𝕜 E),
    let this := IsTopologicalAddGroup.toUniformSpace E;
    let this := ⋯;
    Fintype.card ι = n → Continuous ⇑ξ.equivFun
E : Type v
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝¹ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E := uniformAddGroup_of_addCommGroup
hn : Fintype.card ι = n + 1
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 ↥s = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 ↥(LinearMap.range f) = 0
⊢ finrank 𝕜 ↥(LinearMap.ker f) = n

Tactic:
have Z := f.finrank_range_add_finrank_ker

Result:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [inst_5 : T2Space E] {ι : Type v}
    [inst_6 : Fintype ι] (ξ : Basis ι 𝕜 E),
    let this := IsTopologicalAddGroup.toUniformSpace E;
    let this := ⋯;
    Fintype.card ι = n → Continuous ⇑ξ.equivFun
E : Type v
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝¹ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E := uniformAddGroup_of_addCommGroup
hn : Fintype.card ι = n + 1
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 ↥s = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 ↥(LinearMap.range f) = 0
Z : finrank 𝕜 ↥(LinearMap.range f) + finrank 𝕜 ↥(LinearMap.ker f) = finrank 𝕜 E
⊢ finrank 𝕜 ↥(LinearMap.ker f) = n