awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Bases
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))
rw₂ 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))
⊢ ∑ 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:
rw [← Finset.sum_union (Finset.disjoint_sdiff_inter A A₀).symm,
      Finset.union_comm, Finset.sdiff_union_inter]

Premises used: Finset.union_comm, Finset.sum_union, Disjoint.symm, Finset.disjoint_sdiff_inter, Finset.sdiff_union_inter
-- Module: Mathlib.Analysis.Normed.Module.Bases
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)

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]
-- Module: Mathlib.Analysis.Normed.Module.Bases
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)
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)
        ⋯ _root_.id)
      1
⊢ 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

Tactic:
rw [hdecomp]
-- Module: Mathlib.Analysis.Normed.Module.Bases
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)
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
⊢ norm (E := X) ((GeneralSchauderBasis.proj b (A \ A₀) : (a : X) → X) x : X) < 1

Tactic:
rw [GeneralSchauderBasis.proj_apply]

Premises used: GeneralSchauderBasis.proj_apply
-- Module: Mathlib.Analysis.Normed.Module.Bases
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.{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:
hA₀ (A \ A₀) Finset.sdiff_disjoint

Premises used: SDiff.sdiff, Finset.sdiff_disjoint
-- Module: Mathlib.Analysis.Normed.Module.Bases
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.{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:
exact hA₀ (A \ A₀) Finset.sdiff_disjoint

Premises used: SDiff.sdiff, Finset.sdiff_disjoint
-- Module: Mathlib.Analysis.Normed.Module.Bases
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

Tactic:
have htail : ‖b.proj (A \ A₀) x‖ < 1 := by
    rw [GeneralSchauderBasis.proj_apply]
    exact hA₀ (A \ A₀) Finset.sdiff_disjoint
-- Module: Mathlib.Analysis.Normed.Module.Bases
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
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)
      ⋯ _root_.id
⊢ ‖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

Tactic:
apply (norm_add_le _ _).trans (add_le_add _ htail.le)

Premises used: add_le_add, norm_add_le, LT.lt.le, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Module.Bases
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
⊢ 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)
      ⋯ _root_.id

Tactic:
Finset.le_sup' id <| Finset.mem_image_of_mem (fun B ↦ ‖b.proj B x‖)
      (Finset.mem_powerset.2 Finset.inter_subset_right)

Premises used: Iff.mpr, Norm.norm, Finset.inter_subset_right, id, Finset.mem_powerset, GeneralSchauderBasis.proj, Finset.mem_image_of_mem, Finset.le_sup', DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.Bases
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
⊢ 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)
      ⋯ _root_.id

Tactic:
exact Finset.le_sup' id <| Finset.mem_image_of_mem (fun B ↦ ‖b.proj B x‖)
      (Finset.mem_powerset.2 Finset.inter_subset_right)

Premises used: Iff.mpr, Norm.norm, Finset.inter_subset_right, id, Finset.mem_powerset, GeneralSchauderBasis.proj, Finset.mem_image_of_mem, Finset.le_sup', DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.Bases
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
obtain :
  ∀ (C : ℝ) (hC : ∀ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ ≤ C),
    BddAbove (α := ℝ≥0) (Set.range fun (A : Finset β) ↦ ‖GeneralSchauderBasis.proj b A‖₊)
⊢ BddAbove (α := ℝ≥0) (Set.range fun (A : Finset β) ↦ ‖GeneralSchauderBasis.proj b A‖₊)

Tactic:
obtain ⟨C, hC⟩ := b.exists_norm_proj_le

Premises used: UnconditionalSchauderBasis.exists_norm_proj_le
-- Module: Mathlib.Analysis.Normed.Module.Bases
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 : ℝ
hC : ∀ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ ≤ C
⊢ 0 ≤ C

Tactic:
simpa [GeneralSchauderBasis.proj_empty] using hC ∅

Premises used: GeneralSchauderBasis.proj_empty, EmptyCollection.emptyCollection
-- Module: Mathlib.Analysis.Normed.Module.Bases
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 : ℝ
hC : ∀ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ ≤ C
⊢ 0 ≤ C

Tactic:
have hCpos : 0 ≤ C := by simpa [GeneralSchauderBasis.proj_empty] using hC ∅
-- Module: Mathlib.Analysis.Normed.Module.Bases
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 : ℝ
hC : ∀ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ ≤ C
hCpos : 0 ≤ C
⊢ BddAbove (α := ℝ≥0) (Set.range fun (A : Finset β) ↦ ‖GeneralSchauderBasis.proj b A‖₊)

Tactic:
⟨C.toNNReal, ?_⟩

Premises used: BddAbove, Set.Nonempty, Exists.intro, Real.toNNReal
-- Module: Mathlib.Analysis.Normed.Module.Bases
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 : ℝ
hC : ∀ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ ≤ C
hCpos : 0 ≤ C
refine :
  Membership.mem (γ := Set ℝ≥0) (upperBounds (Set.range fun (A : Finset β) ↦ ‖GeneralSchauderBasis.proj b A‖₊))
    C.toNNReal
⊢ BddAbove (α := ℝ≥0) (Set.range fun (A : Finset β) ↦ ‖GeneralSchauderBasis.proj b A‖₊)

Tactic:
refine ⟨C.toNNReal, ?_⟩
-- Module: Mathlib.Analysis.Normed.Module.Bases
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 : ℝ
hC : ∀ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ ≤ C
hCpos : 0 ≤ C
A : Finset β
rw : ‖GeneralSchauderBasis.proj b A‖ ≤ C
⊢ (fun (A : Finset β) ↦ ‖GeneralSchauderBasis.proj b A‖₊) A ≤ C.toNNReal

Tactic:
rw [← NNReal.coe_le_coe, Real.coe_toNNReal C hCpos, coe_nnnorm]

Premises used: Real.coe_toNNReal, coe_nnnorm, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.Normed.Module.Bases
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 : ℝ
hC : ∀ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ ≤ C
hCpos : 0 ≤ C
A : Finset β
⊢ ‖GeneralSchauderBasis.proj b A‖ ≤ C

Tactic:
hC A
-- Module: Mathlib.Analysis.Normed.Module.Bases
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 : ℝ
hC : ∀ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ ≤ C
hCpos : 0 ≤ C
A : Finset β
⊢ ‖GeneralSchauderBasis.proj b A‖ ≤ C

Tactic:
exact hC A
-- Module: Mathlib.Analysis.Normed.Module.Bases
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
A : Finset β
⊢ ‖GeneralSchauderBasis.proj b A‖₊ ≤ b.nnnormProjBound

Tactic:
le_ciSup (bddAbove_range_nnnorm_proj b) A

Premises used: le_ciSup, UnconditionalSchauderBasis.nnnormProjBound, UnconditionalSchauderBasis.bddAbove_range_nnnorm_proj
-- Module: Mathlib.Analysis.Normed.Module.Bases
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
A : Finset β
⊢ ‖GeneralSchauderBasis.proj b A‖ ≤ (↑b.nnnormProjBound : ℝ)

Tactic:
mod_cast b.nnnorm_proj_le_nnnormProjBound A

Premises used: Norm.norm, cast, LE.le, GeneralSchauderBasis.proj, UnconditionalSchauderBasis.nnnormProjBound, Eq.refl, UnconditionalSchauderBasis.nnnorm_proj_le_nnnormProjBound, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
rw : GeneralSchauderBasis.proj b (Finset.range 0) = 0
rw₁ : GeneralSchauderBasis.proj b ∅ = 0
rw₂ rw₃ : Eq.{u_2 + 1} (α := X →L[𝕜] X) 0 0
⊢ b.proj 0 = 0

Tactic:
rw [proj, Finset.range_zero, GeneralSchauderBasis.proj_empty]

Premises used: SchauderBasis.proj, GeneralSchauderBasis.proj_empty, Finset.range_zero
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
n : ℕ
x : X
rw :
  Eq (α := X) ((GeneralSchauderBasis.proj b (Finset.range n) : (a : X) → X) x : X)
    (∑ i ∈ Finset.range n, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : ℕ → X) i) : X)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := X)
    (∑ i ∈ Finset.range n, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : ℕ → X) i))
    (∑ i ∈ Finset.range n, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : ℕ → X) i))
⊢ Eq (α := X) ((b.proj n : (a : X) → X) x : X)
    (∑ i ∈ Finset.range n, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : ℕ → X) i) : X)

Tactic:
rw [proj, GeneralSchauderBasis.proj_apply]

Premises used: GeneralSchauderBasis.proj_apply, SchauderBasis.proj
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
n i : ℕ
rw : (if i ∈ Finset.range n then (↑b : ℕ → X) i else 0) = if i < n then (↑b : ℕ → X) i else 0
⊢ (b.proj n : (a : X) → X) ((↑b : ℕ → X) i) = if i < n then (↑b : ℕ → X) i else 0

Tactic:
rw [proj, GeneralSchauderBasis.proj_apply_basis_mem]

Premises used: SchauderBasis.proj, GeneralSchauderBasis.proj_apply_basis_mem
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
n i : ℕ
⊢ (if i ∈ Finset.range n then (↑b : ℕ → X) i else 0) = if i < n then (↑b : ℕ → X) i else 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
n : ℕ
rw :
  (↑(GeneralSchauderBasis.proj b (Finset.range n)) : X →ₗ[𝕜] X).range =
    Submodule.span 𝕜 ((↑b : ℕ → X) '' (↑(Finset.range n) : Set ℕ))
rw₁ rw₂ :
  Eq (α := Submodule 𝕜 X) (Submodule.span 𝕜 ((↑b : ℕ → X) '' (↑(Finset.range n) : Set ℕ)))
    (Submodule.span 𝕜 ((↑b : ℕ → X) '' (↑(Finset.range n) : Set ℕ)))
⊢ (↑(b.proj n) : X →ₗ[𝕜] X).range = Submodule.span 𝕜 ((↑b : ℕ → X) '' (↑(Finset.range n) : Set ℕ))

Tactic:
rw [proj, GeneralSchauderBasis.range_proj_eq_span]

Premises used: SchauderBasis.proj, GeneralSchauderBasis.range_proj_eq_span
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
n : ℕ
rw : Module.finrank.{u_1, u_2} 𝕜 ↥(↑(GeneralSchauderBasis.proj b (Finset.range n)) : X →ₗ[𝕜] X).range = n
rw₁ : (Finset.range n).card = n
rw₂ rw₃ : n = n
⊢ Module.finrank.{u_1, u_2} 𝕜 ↥(↑(b.proj n) : X →ₗ[𝕜] X).range = n

Tactic:
rw [proj, GeneralSchauderBasis.finrank_range_proj, Finset.card_range]

Premises used: Finset.card_range, SchauderBasis.proj, GeneralSchauderBasis.finrank_range_proj
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
x : X
⊢ Tendsto (fun (A : Finset ℕ) ↦ (GeneralSchauderBasis.proj b A : (a : X) → X) x) (SummationFilter.conditional ℕ).filter
    (𝓝 x)

Tactic:
have := GeneralSchauderBasis.tendsto_proj b x
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
x : X
this :
  Tendsto (fun (A : Finset ℕ) ↦ (GeneralSchauderBasis.proj b A : (a : X) → X) x) (SummationFilter.conditional ℕ).filter
    (𝓝 x)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (this :
      Tendsto (fun (A : Finset ℕ) ↦ (GeneralSchauderBasis.proj b A : (a : X) → X) x) (map Finset.range atTop) (𝓝 x)),
    Tendsto (fun (n : ℕ) ↦ (b.proj n : (a : X) → X) x) atTop (𝓝 x)
⊢ Tendsto (fun (n : ℕ) ↦ (b.proj n : (a : X) → X) x) atTop (𝓝 x)

Tactic:
rwa [SummationFilter.conditional_filter_eq_map_range] at this

Premises used: SummationFilter.conditional_filter_eq_map_range
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
n m : ℕ
x : X
simp :
  Eq (α := X) ((GeneralSchauderBasis.proj b (Finset.range n ∩ Finset.range m) : (a : X) → X) x : X)
    ((GeneralSchauderBasis.proj b (Finset.range (min n m)) : (a : X) → X) x : X)
⊢ Eq (α := X) ((b.proj n : (a : X) → X) ((b.proj m : (a : X) → X) x : X) : X) ((b.proj (min n m) : (a : X) → X) x : X)

Tactic:
simp only [proj, GeneralSchauderBasis.proj_comp]

Premises used: SchauderBasis.proj, GeneralSchauderBasis.proj_comp
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
n m : ℕ
x : X
e_a : Finset.range n ∩ Finset.range m = Finset.range (min n m)
⊢ Eq (α := X) ((GeneralSchauderBasis.proj b (Finset.range n ∩ Finset.range m) : (a : X) → X) x : X)
    ((GeneralSchauderBasis.proj b (Finset.range (min n m)) : (a : X) → X) x : X)

Tactic:
congr 2
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
n m : ℕ
x : X
e_a : ∀ (a : ℕ), a ∈ Finset.range n ∩ Finset.range m ↔ a ∈ Finset.range (min n m)
⊢ Finset.range n ∩ Finset.range m = Finset.range (min n m)

Tactic:
ext _
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
n m : ℕ
x : X
a : ℕ
e_a : a < n ∧ a < m ↔ a < min n m
⊢ a ∈ Finset.range n ∩ Finset.range m ↔ a ∈ Finset.range (min n m)

Tactic:
simp only [Finset.mem_inter, Finset.mem_range]

Premises used: Finset.mem_range, Finset.mem_inter
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
n m : ℕ
x : X
a : ℕ
⊢ a < n ∧ a < m ↔ a < min n m

Tactic:
omega
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
inst_3 : CompleteSpace X
h : ∀ (x : X), ∃ (C : ℝ), ∀ (i : ℕ), norm (E := X) ((b.proj i : (a : X) → X) x : X) ≤ C
⊢ ∃ (C : ℝ), ∀ (n : ℕ), ‖b.proj n‖ ≤ C

Tactic:
apply banach_steinhaus

Premises used: banach_steinhaus