-- 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 𝕜
E : Type v
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝¹ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E := uniformAddGroup_of_addCommGroup
this : ∀ (n : ℕ), Fintype.card ι = n → Continuous ⇑ξ.equivFun
⊢ Continuous ⇑ξ.equivFun

Tactic:
exact this _ rfl

Result:
no goals

Proof state:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this : UniformAddGroup E := uniformAddGroup_of_addCommGroup
⊢ Continuous ⇑ξ.equivFun

Tactic:
suffices ∀ n, Fintype.card ι = n → Continuous ξ.equivFun by exact this _ rfl

Result:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this : UniformAddGroup E := uniformAddGroup_of_addCommGroup
⊢ ∀ (n : ℕ), Fintype.card ι = n → Continuous ⇑ξ.equivFun

Proof state:
case neg
𝕜 : 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
this : finrank 𝕜 ↥(LinearMap.ker f) = n
⊢ Continuous ⇑f

Tactic:
have : IsClosed (LinearMap.ker f : Set E) := H₁ _ this

Result:
case neg
𝕜 : 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
this✝ : finrank 𝕜 ↥(LinearMap.ker f) = n
this : IsClosed ↑(LinearMap.ker f)
⊢ 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
s : Submodule 𝕜 E
s_dim : finrank 𝕜 ↥s = n
this : UniformAddGroup ↥s := AddSubgroup.uniformAddGroup s.toAddSubgroup
⊢ IsClosed ↑s

Tactic:
let b := Basis.ofVectorSpace 𝕜 s

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
⊢ IsClosed ↑s