-- Module: Mathlib.Topology.Algebra.Module.FiniteDimension
Goal:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst : AddCommGroup E
inst_1 : Module 𝕜 E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : CompleteSpace 𝕜
inst_6 : T2Space E
ι : Type v
inst_7 : Finite ι
ξ : Basis ι 𝕜 E
this_1 : Fintype ι
this_2 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E := ⋯
n : ℕ
hn : Fintype.card ι = n
zero :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_8 : Module 𝕜 E] [inst_9 : TopologicalSpace E] [IsTopologicalAddGroup E]
    [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_13 : Finite ι] (ξ : Basis ι 𝕜 E) (this : Fintype ι)
    (hn : Fintype.card ι = 0), Continuous[_, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)
succ :
  ∀ (n : ℕ)
    (IH :
      ∀ {E : Type v} [inst : AddCommGroup E] [inst_8 : Module 𝕜 E] [inst_9 : TopologicalSpace E]
        [inst_10 : IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_13 : Finite ι]
        (ξ : Basis ι 𝕜 E) (this : Fintype ι),
        let this_3 := IsTopologicalAddGroup.rightUniformSpace E;
        let this_4 : IsUniformAddGroup E := ⋯;
        ∀ (hn : Fintype.card ι = n), Continuous[_, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜))
    {E : Type v} [inst : AddCommGroup E] [inst_8 : Module 𝕜 E] [inst_9 : TopologicalSpace E] [IsTopologicalAddGroup E]
    [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_13 : Finite ι] (ξ : Basis ι 𝕜 E) (this : Fintype ι)
    (hn : Fintype.card ι = n + 1), Continuous[_, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)
⊢ Continuous[inst_2, Pi.topologicalSpace] (⇑ξ.equivFun : (a : E) → ι → 𝕜)

Tactic:
induction n generalizing ι E with
  | zero =>
    rw [Fintype.card_eq_zero_iff] at hn
    exact continuous_of_const fun x y => funext hn.elim
  | succ n IH =>
    haveI : FiniteDimensional 𝕜 E := ξ.finiteDimensional_of_finite
    -- first step: thanks to the induction hypothesis, any n-dimensional subspace is equivalent
    -- to a standard space of dimension n, hence it is complete and therefore closed.
    have H₁ : ∀ s : Submodule 𝕜 E, finrank 𝕜 s = n → IsClosed (s : Set E) := by
      intro s s_dim
      letI : IsUniformAddGroup s := s.toAddSubgroup.isUniformAddGroup
      let b := Basis.ofVectorSpace 𝕜 s
      have U : IsUniformEmbedding b.equivFun.symm.toEquiv := by
        have : Fintype.card (Basis.ofVectorSpaceIndex 𝕜 s) = n := by
          rw [← s_dim]
          exact (finrank_eq_card_basis b).symm
        have : Continuous b.equivFun := IH b inferInstance this
        exact
          b.equivFun.symm.isUniformEmbedding b.equivFun.symm.toLinearMap.continuous_on_pi this
      have : IsComplete (s : Set E) :=
        completeSpace_coe_iff_isComplete.1 ((completeSpace_congr U).1 inferInstance)
      exact this.isClosed
    -- second step: any linear form is continuous, as its kernel is closed by the first step
    have H₂ : ∀ f : E →ₗ[𝕜] 𝕜, Continuous f := by
      intro f
      by_cases H : finrank 𝕜 (LinearMap.range f) = 0
      · rw [Submodule.finrank_eq_zero, LinearMap.range_eq_bot] at H
        rw [H]
        exact continuous_zero
      · have : finrank 𝕜 (LinearMap.ker f) = n := by
          have Z := f.finrank_range_add_finrank_ker
          rw [finrank_eq_card_basis ξ, hn] at Z
          have : finrank 𝕜 (LinearMap.range f) = 1 :=
            le_antisymm (finrank_self 𝕜 ▸ (LinearMap.range f).finrank_le) (zero_lt_iff.mpr H)
          rw [this, add_comm, Nat.add_one] at Z
          exact Nat.succ.inj Z
        have : IsClosed (LinearMap.ker f : Set E) := H₁ _ this
        exact LinearMap.continuous_of_isClosed_ker f this
    rw [continuous_pi_iff]
    intro i
    change Continuous (ξ.coord i)
    exact H₂ (ξ.coord i)

Premises used: continuous_pi_iff, Fintype.card_eq_zero_iff