-- 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 →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 ↥(LinearMap.range f) = 0
Z : finrank 𝕜 ↥(LinearMap.range f) + finrank 𝕜 ↥(LinearMap.ker f) = n + 1
this : finrank 𝕜 ↥(LinearMap.range f) = 1
⊢ finrank 𝕜 ↥(LinearMap.ker f) = n

Tactic:
rw [this, add_comm, Nat.add_one] at Z

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.ker f)).succ = n + 1
this : finrank 𝕜 ↥(LinearMap.range f) = 1
⊢ finrank 𝕜 ↥(LinearMap.ker f) = n

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
s : Submodule 𝕜 E
s_dim : finrank 𝕜 ↥s = n
this✝¹ : UniformAddGroup ↥s := AddSubgroup.uniformAddGroup s.toAddSubgroup
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s)) 𝕜 ↥s := Basis.ofVectorSpace 𝕜 ↥s
this✝ : Fintype.card ↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) = n
this : Continuous ⇑b.equivFun
⊢ IsUniformEmbedding ⇑b.equivFun.symm.toEquiv

Tactic:
exact
  b.equivFun.symm.isUniformEmbedding b.equivFun.symm.toLinearMap.continuous_on_pi this

Result:
no goals

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
Z : finrank 𝕜 ↥(LinearMap.range f) + finrank 𝕜 ↥(LinearMap.ker f) = finrank 𝕜 E
⊢ finrank 𝕜 ↥(LinearMap.ker f) = n

Tactic:
rw [finrank_eq_card_basis ξ, hn] at Z

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) = n + 1
⊢ finrank 𝕜 ↥(LinearMap.ker f) = n