-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
β : Type u_3
b : UnconditionalSchauderBasis β 𝕜 X
inst_3 : CompleteSpace X
h h₁ : ∀ (x : X), ∃ (C : ℝ), ∀ (i : Finset β), norm (E := X) ((GeneralSchauderBasis.proj b i : (a : X) → X) x : X) ≤ C
h₂ :
  ∀ (x : X) (A₀ : Finset β)
    (hA₀ :
      ∀ (t : Finset β),
        Disjoint t A₀ →
          norm.{u_2} (E := X)
              (∑ i ∈ t, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i)) <
            1),
    ∃ (C : ℝ), ∀ (i : Finset β), norm (E := X) ((GeneralSchauderBasis.proj b i : (a : X) → X) x : X) ≤ C
h₃ h₄ :
  ∀ (x : X) (A₀ : Finset β)
    (hA₀ :
      ∀ (t : Finset β),
        Disjoint t A₀ →
          norm.{u_2} (E := X)
              (∑ i ∈ t, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i)) <
            1)
    (A : Finset β),
    norm (E := X) ((GeneralSchauderBasis.proj b A : (a : X) → X) x : X) ≤
      HAdd.hAdd (α := ℝ)
        (Finset.sup'
          (Finset.image (fun (B : Finset β) ↦ norm (E := X) ((GeneralSchauderBasis.proj b B : (a : X) → X) x : X))
            A₀.powerset)
          ⋯ _root_.id)
        1
h₅ :
  ∀ (x : X) (A₀ : Finset β)
    (hA₀ :
      ∀ (t : Finset β),
        Disjoint t A₀ →
          norm.{u_2} (E := X)
              (∑ i ∈ t, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i)) <
            1)
    (A : Finset β)
    (hdecomp :
      (GeneralSchauderBasis.proj b A : (a : X) → X) x =
        HAdd.hAdd (α := X) (β := X) ((GeneralSchauderBasis.proj b (A ∩ A₀) : (a : X) → X) x : X)
          ((GeneralSchauderBasis.proj b (A \ A₀) : (a : X) → X) x : X)),
    norm (E := X) ((GeneralSchauderBasis.proj b A : (a : X) → X) x : X) ≤
      HAdd.hAdd (α := ℝ)
        (Finset.sup'
          (Finset.image (fun (B : Finset β) ↦ norm (E := X) ((GeneralSchauderBasis.proj b B : (a : X) → X) x : X))
            A₀.powerset)
          ⋯ _root_.id)
        1
⊢ ∃ (C : ℝ), ∀ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ ≤ C
have h₆ : ∀ (x : X) (A₀ : Finset β)
  (hA₀ :
    ∀ (t : Finset β),
      Disjoint t A₀ →
        norm.{u_2} (E := X)
            (∑ i ∈ t, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i)) <
          1)
  (A : Finset β)
  (hdecomp :
    (GeneralSchauderBasis.proj b A : (a : X) → X) x =
      HAdd.hAdd (α := X) (β := X) ((GeneralSchauderBasis.proj b (A ∩ A₀) : (a : X) → X) x : X)
        ((GeneralSchauderBasis.proj b (A \ A₀) : (a : X) → X) x : X)),
  ‖HAdd.hAdd (α := X) (β := X) ((GeneralSchauderBasis.proj b (A ∩ A₀) : (a : X) → X) x : X)
        ((GeneralSchauderBasis.proj b (A \ A₀) : (a : X) → X) x : X)‖ ≤
    HAdd.hAdd (α := ℝ)
      (Finset.sup'
        (Finset.image (fun (B : Finset β) ↦ norm (E := X) ((GeneralSchauderBasis.proj b B : (a : X) → X) x : X))
          A₀.powerset)
        sorry _root_.id)
      1
Tactic: classical
  apply banach_steinhaus
  intro x
  obtain ⟨A₀, hA₀⟩ := summable_iff_vanishing_norm.mp (b.expansion x).summable 1 zero_lt_one
  use (A₀.powerset.image fun B ↦ ‖b.proj B x‖).sup' ((Finset.powerset_nonempty A₀).image _) id + 1
  intro A
  have hdecomp : b.proj A x = b.proj (A ∩ A₀) x + b.proj (A \ A₀) x := by
    simp only [GeneralSchauderBasis.proj_apply]
    rw [← Finset.sum_union (Finset.disjoint_sdiff_inter A A₀).symm,
      Finset.union_comm, Finset.sdiff_union_inter]
  rw [hdecomp]
  -- -- The projection on the tail (A \ A₀) at `x` is bounded by 1
  have htail : ‖b.proj (A \ A₀) x‖ < 1 := by
    rw [GeneralSchauderBasis.proj_apply]
    exact hA₀ (A \ A₀) Finset.sdiff_disjoint
  apply (norm_add_le _ _).trans (add_le_add _ htail.le)
  -- The projection on (A ∩ A₀) at `x` is bounded by the `sup'`.
  exact Finset.le_sup' id <| Finset.mem_image_of_mem (fun B ↦ ‖b.proj B x‖)
      (Finset.mem_powerset.2 Finset.inter_subset_right)