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

Proof state:
case succ
𝕜 : 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
H₂ : ∀ (f : E →ₗ[𝕜] 𝕜), Continuous ⇑f
i : ι
⊢ Continuous fun a => ξ.equivFun a i

Tactic:
change Continuous (ξ.coord i)

Result:
case succ
𝕜 : 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
H₂ : ∀ (f : E →ₗ[𝕜] 𝕜), Continuous ⇑f
i : ι
⊢ Continuous ⇑(ξ.coord i)

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
⊢ Fintype.card ↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) = n

Tactic:
rw [← s_dim]

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

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), finrank 𝕜 ↥s = n → IsClosed ↑s

Tactic:
intro s s_dim

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
s : Submodule 𝕜 E
s_dim : finrank 𝕜 ↥s = n
⊢ IsClosed ↑s