awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A : Finset β
i : β
hi : i ∈ (↑A : Set β)
h : (b.proj A : (a : X) → X) ((↑b : β → X) i) = (↑b : β → X) i
⊢ ((↑(b.proj A) : X →ₗ[𝕜] X) : (a : X) → X) ((↑b : β → X) i) = (↑b : β → X) i
have h₁ : (if i ∈ A then (↑b : β → X) i else 0) = (↑b : β → X) i
Tactic: rw [ContinuousLinearMap.coe_coe, proj_apply_basis_mem, if_pos (Finset.mem_coe.mp hi)]
-- 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
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A : Finset β
i : β
hi : i ∈ (↑A : Set β)
h : (b.proj A : (a : X) → X) ((↑b : β → X) i) = (↑b : β → X) i
h₁ : (if i ∈ A then (↑b : β → X) i else 0) = (↑b : β → X) i
⊢ ((↑(b.proj A) : X →ₗ[𝕜] X) : (a : X) → X) ((↑b : β → X) i) = (↑b : β → X) i
have h₂ : (↑b : β → X) i = (↑b : β → X) i
Tactic: rw [ContinuousLinearMap.coe_coe, proj_apply_basis_mem, if_pos (Finset.mem_coe.mp hi)]
-- 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
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A B : Finset β
x : X
⊢ Eq (α := X) ((b.proj A : (a : X) → X) ((b.proj B : (a : X) → X) x : X) : X) ((b.proj (A ∩ B) : (a : X) → X) x : X)
have simp : Eq.{u_2 + 1} (α := X)
  (∑ i ∈ B ∩ A, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
  (∑ i ∈ A ∩ B, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
Tactic: simp only [proj_apply, map_sum, map_smul, b.ortho, Pi.single_apply, ite_smul, one_smul, zero_smul,
    Finset.sum_ite_eq', smul_ite, smul_zero, Finset.sum_ite_mem]
-- 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
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A B : Finset β
x : X
⊢ Eq.{u_2 + 1} (α := X)
    (∑ i ∈ B ∩ A, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
    (∑ i ∈ A ∩ B, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
have e_s : B ∩ A = A ∩ B
Tactic: congr 1
-- 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
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A B : Finset β
x : X
⊢ B ∩ A = A ∩ B
have e_s : ∀ (a : β), a ∈ B ∩ A ↔ a ∈ A ∩ B
Tactic: ext _
-- 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
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A : Finset β
⊢ Module.finrank.{u_1, u_2} 𝕜 ↥(↑(b.proj A) : X →ₗ[𝕜] X).range = A.card
have rw : Fintype.card.{u_3} (↑(↑A : Set β) : Type u_3) = A.card
Tactic: rw [range_proj_eq_span, Set.image_eq_range, finrank_span_eq_card]
-- 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
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A : Finset β
rw : Fintype.card.{u_3} (↑(↑A : Set β) : Type u_3) = A.card
⊢ Module.finrank.{u_1, u_2} 𝕜 ↥(↑(b.proj A) : X →ₗ[𝕜] X).range = A.card
have rw₁ : LinearIndependent.{u_3, u_1, u_2} 𝕜 (M := X) fun (x : (↑(↑A : Set β) : Type u_3)) ↦ (↑b : β → X) (↑x : β)
Tactic: rw [range_proj_eq_span, Set.image_eq_range, finrank_span_eq_card]
-- 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
⊢ ∃ (C : ℝ), ∀ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ ≤ C
have h : ∀ (x : X), ∃ (C : ℝ), ∀ (i : Finset β), norm (E := X) ((GeneralSchauderBasis.proj b i : (a : X) → X) x : X) ≤ C
Tactic: apply banach_steinhaus
-- 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
x : X
⊢ ∃ (C : ℝ), ∀ (i : Finset β), norm (E := X) ((GeneralSchauderBasis.proj b i : (a : X) → X) x : X) ≤ C
have h : ∀ (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
Tactic: obtain ⟨A₀, hA₀⟩ := summable_iff_vanishing_norm.mp (b.expansion x).summable 1 zero_lt_one
-- 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
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
have h : ∀ (i : Finset β),
  norm (E := X) ((GeneralSchauderBasis.proj b i : (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: use (A₀.powerset.image fun B ↦ ‖b.proj B x‖).sup' ((Finset.powerset_nonempty A₀).image _) id + 1
-- 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
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 β
⊢ (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)
have simp : ∑ i ∈ A, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i) =
  HAdd.hAdd (α := X)
    (∑ i ∈ A ∩ A₀, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
    (∑ i ∈ A \ A₀, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
Tactic: simp only [GeneralSchauderBasis.proj_apply]
-- 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
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 β
⊢ ∑ i ∈ A, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i) =
    HAdd.hAdd (α := X)
      (∑ i ∈ A ∩ A₀, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
      (∑ i ∈ A \ A₀, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
have rw : Eq.{u_2 + 1} (α := X) (∑ i ∈ A, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
  (∑ x_1 ∈ A ∩ A₀ ∪ A \ A₀, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord x_1 : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) x_1))
Tactic: rw [← Finset.sum_union (Finset.disjoint_sdiff_inter A A₀).symm,
      Finset.union_comm, Finset.sdiff_union_inter]
-- 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
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 β
rw :
  Eq.{u_2 + 1} (α := X)
    (∑ i ∈ A, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
    (∑ x_1 ∈ A ∩ A₀ ∪ A \ A₀,
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord x_1 : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) x_1))
⊢ ∑ i ∈ A, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i) =
    HAdd.hAdd (α := X)
      (∑ i ∈ A ∩ A₀, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
      (∑ i ∈ A \ A₀, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
have rw₁ : Eq.{u_2 + 1} (α := X) (∑ i ∈ A, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
  (∑ x_1 ∈ A \ A₀ ∪ A ∩ A₀, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord x_1 : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) x_1))
Tactic: rw [← Finset.sum_union (Finset.disjoint_sdiff_inter A A₀).symm,
      Finset.union_comm, Finset.sdiff_union_inter]
-- 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
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 β
rw :
  Eq.{u_2 + 1} (α := X)
    (∑ i ∈ A, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
    (∑ x_1 ∈ A ∩ A₀ ∪ A \ A₀,
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord x_1 : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) x_1))
rw₁ :
  Eq.{u_2 + 1} (α := X)
    (∑ i ∈ A, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
    (∑ x_1 ∈ A \ A₀ ∪ A ∩ A₀,
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord x_1 : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) x_1))
⊢ ∑ i ∈ A, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i) =
    HAdd.hAdd (α := X)
      (∑ i ∈ A ∩ A₀, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
      (∑ i ∈ A \ A₀, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
have rw₂ : Eq.{u_2 + 1} (α := X) (∑ i ∈ A, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
  (∑ x_1 ∈ A, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord x_1 : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) x_1))
Tactic: rw [← Finset.sum_union (Finset.disjoint_sdiff_inter A A₀).symm,
      Finset.union_comm, Finset.sdiff_union_inter]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (hypothesis)
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
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
have 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)
Tactic: 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]
-- 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
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
have h : ‖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: rw [hdecomp]
-- 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
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₀) : (a : X) → X) x : X) < 1
have rw : norm.{u_2} (E := X)
    (∑ i ∈ A \ A₀, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i)) <
  1
Tactic: rw [GeneralSchauderBasis.proj_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (hypothesis)
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
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)
        ⋯ _root_.id)
      1
have htail : norm (E := X) ((GeneralSchauderBasis.proj b (A \ A₀) : (a : X) → X) x : X) < 1
Tactic: have htail : ‖b.proj (A \ A₀) x‖ < 1 := by
    rw [GeneralSchauderBasis.proj_apply]
    exact hA₀ (A \ A₀) Finset.sdiff_disjoint
-- 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
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)
htail : norm (E := X) ((GeneralSchauderBasis.proj b (A \ A₀) : (a : X) → X) x : X) < 1
⊢ ‖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)
        ⋯ _root_.id)
      1
have apply : norm (E := X) ((GeneralSchauderBasis.proj b (A ∩ A₀) : (a : X) → X) x : X) ≤
  Finset.sup'
    (Finset.image (fun (B : Finset β) ↦ norm (E := X) ((GeneralSchauderBasis.proj b B : (a : X) → X) x : X))
      A₀.powerset)
    sorry _root_.id
Tactic: apply (norm_add_le _ _).trans (add_le_add _ htail.le)
-- 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
⊢ ∃ (C : ℝ), ∀ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ ≤ C
have h : ∀ (x : X), ∃ (C : ℝ), ∀ (i : Finset β), norm (E := X) ((GeneralSchauderBasis.proj b i : (a : X) → X) x : X) ≤ C
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)
-- 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
⊢ ∃ (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),
  ∃ (C : ℝ), ∀ (i : Finset β), norm (E := X) ((GeneralSchauderBasis.proj b i : (a : X) → X) x : X) ≤ C
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)
-- 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
⊢ ∃ (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)
  (i : Finset β),
  norm (E := X) ((GeneralSchauderBasis.proj b i : (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)