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
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
⊢ ∃ (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)),
  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)
        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)
-- 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
⊢ BddAbove (α := ℝ≥0) (Set.range fun (A : Finset β) ↦ ‖GeneralSchauderBasis.proj b A‖₊)
have obtain : ∀ (C : ℝ) (hC : ∀ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ ≤ C),
  BddAbove (α := ℝ≥0) (Set.range fun (A : Finset β) ↦ ‖GeneralSchauderBasis.proj b A‖₊)
Tactic: obtain ⟨C, hC⟩ := b.exists_norm_proj_le
-- 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
C : ℝ
hC : ∀ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ ≤ C
⊢ BddAbove (α := ℝ≥0) (Set.range fun (A : Finset β) ↦ ‖GeneralSchauderBasis.proj b A‖₊)
have hCpos : 0 ≤ C
Tactic: have hCpos : 0 ≤ C := by simpa [GeneralSchauderBasis.proj_empty] using hC ∅
-- 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 : ℝ
hC : ∀ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ ≤ C
hCpos : 0 ≤ C
⊢ BddAbove (α := ℝ≥0) (Set.range fun (A : Finset β) ↦ ‖GeneralSchauderBasis.proj b A‖₊)
have refine : Membership.mem (γ := Set ℝ≥0) (upperBounds (Set.range fun (A : Finset β) ↦ ‖GeneralSchauderBasis.proj b A‖₊)) C.toNNReal
Tactic: refine ⟨C.toNNReal, ?_⟩
-- 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 : ℝ
hC : ∀ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ ≤ C
hCpos : 0 ≤ C
A : Finset β
⊢ (fun (A : Finset β) ↦ ‖GeneralSchauderBasis.proj b A‖₊) A ≤ C.toNNReal
have rw : ‖GeneralSchauderBasis.proj b A‖ ≤ C
Tactic: rw [← NNReal.coe_le_coe, Real.coe_toNNReal C hCpos, coe_nnnorm]
-- 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
b : SchauderBasis 𝕜 X
⊢ b.proj 0 = 0
have rw : GeneralSchauderBasis.proj b (Finset.range 0) = 0
Tactic: rw [proj, Finset.range_zero, GeneralSchauderBasis.proj_empty]
-- 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
b : SchauderBasis 𝕜 X
rw : GeneralSchauderBasis.proj b (Finset.range 0) = 0
⊢ b.proj 0 = 0
have rw₁ : GeneralSchauderBasis.proj b ∅ = 0
Tactic: rw [proj, Finset.range_zero, GeneralSchauderBasis.proj_empty]
-- 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
b : SchauderBasis 𝕜 X
rw : GeneralSchauderBasis.proj b (Finset.range 0) = 0
rw₁ : GeneralSchauderBasis.proj b ∅ = 0
⊢ b.proj 0 = 0
have rw₂ : Eq.{u_2 + 1} (α := X →L[𝕜] X) 0 0
Tactic: rw [proj, Finset.range_zero, GeneralSchauderBasis.proj_empty]
-- 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
b : SchauderBasis 𝕜 X
n : ℕ
x : X
⊢ 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)
have 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)
Tactic: rw [proj, 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
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)
⊢ 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)
have 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))
Tactic: rw [proj, 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
b : SchauderBasis 𝕜 X
n i : ℕ
⊢ (b.proj n : (a : X) → X) ((↑b : ℕ → X) i) = if i < n then (↑b : ℕ → X) i else 0
have rw : (if i ∈ Finset.range n then (↑b : ℕ → X) i else 0) = if i < n then (↑b : ℕ → X) i else 0
Tactic: rw [proj, GeneralSchauderBasis.proj_apply_basis_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
b : SchauderBasis 𝕜 X
n : ℕ
⊢ (↑(b.proj n) : X →ₗ[𝕜] X).range = Submodule.span 𝕜 ((↑b : ℕ → X) '' (↑(Finset.range n) : Set ℕ))
have rw : (↑(GeneralSchauderBasis.proj b (Finset.range n)) : X →ₗ[𝕜] X).range =
  Submodule.span 𝕜 ((↑b : ℕ → X) '' (↑(Finset.range n) : Set ℕ))
Tactic: rw [proj, GeneralSchauderBasis.range_proj_eq_span]
-- 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
b : SchauderBasis 𝕜 X
n : ℕ
rw :
  (↑(GeneralSchauderBasis.proj b (Finset.range n)) : X →ₗ[𝕜] X).range =
    Submodule.span 𝕜 ((↑b : ℕ → X) '' (↑(Finset.range n) : Set ℕ))
⊢ (↑(b.proj n) : X →ₗ[𝕜] X).range = Submodule.span 𝕜 ((↑b : ℕ → X) '' (↑(Finset.range n) : Set ℕ))
have rw₁ : Eq (α := Submodule 𝕜 X) (Submodule.span 𝕜 ((↑b : ℕ → X) '' (↑(Finset.range n) : Set ℕ)))
  (Submodule.span 𝕜 ((↑b : ℕ → X) '' (↑(Finset.range n) : Set ℕ)))
Tactic: rw [proj, GeneralSchauderBasis.range_proj_eq_span]
-- 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
b : SchauderBasis 𝕜 X
n : ℕ
⊢ Module.finrank.{u_1, u_2} 𝕜 ↥(↑(b.proj n) : X →ₗ[𝕜] X).range = n
have rw : Module.finrank.{u_1, u_2} 𝕜 ↥(↑(GeneralSchauderBasis.proj b (Finset.range n)) : X →ₗ[𝕜] X).range = n
Tactic: rw [proj, GeneralSchauderBasis.finrank_range_proj, Finset.card_range]
-- 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
b : SchauderBasis 𝕜 X
n : ℕ
rw : Module.finrank.{u_1, u_2} 𝕜 ↥(↑(GeneralSchauderBasis.proj b (Finset.range n)) : X →ₗ[𝕜] X).range = n
⊢ Module.finrank.{u_1, u_2} 𝕜 ↥(↑(b.proj n) : X →ₗ[𝕜] X).range = n
have rw₁ : (Finset.range n).card = n
Tactic: rw [proj, GeneralSchauderBasis.finrank_range_proj, Finset.card_range]
-- 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
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
⊢ Module.finrank.{u_1, u_2} 𝕜 ↥(↑(b.proj n) : X →ₗ[𝕜] X).range = n
have rw₂ : n = n
Tactic: rw [proj, GeneralSchauderBasis.finrank_range_proj, Finset.card_range]
-- 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
b : SchauderBasis 𝕜 X
x : X
⊢ Tendsto (fun (n : ℕ) ↦ (b.proj n : (a : X) → X) x) atTop (𝓝 x)
have this : Tendsto (fun (A : Finset ℕ) ↦ (GeneralSchauderBasis.proj b A : (a : X) → X) x) (SummationFilter.conditional ℕ).filter
  (𝓝 x)
Tactic: have := GeneralSchauderBasis.tendsto_proj b x
-- 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
b : SchauderBasis 𝕜 X
x : X
this :
  Tendsto (fun (A : Finset ℕ) ↦ (GeneralSchauderBasis.proj b A : (a : X) → X) x) (SummationFilter.conditional ℕ).filter
    (𝓝 x)
⊢ Tendsto (fun (n : ℕ) ↦ (b.proj n : (a : X) → X) x) atTop (𝓝 x)
have 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)
Tactic: rwa [SummationFilter.conditional_filter_eq_map_range] at this
Cleared hypotheses: this
-- 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
b : SchauderBasis 𝕜 X
n m : ℕ
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)
have 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)
Tactic: simp only [proj, GeneralSchauderBasis.proj_comp]
-- 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
b : SchauderBasis 𝕜 X
n m : ℕ
x : X
⊢ 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)
have e_a : Finset.range n ∩ Finset.range m = Finset.range (min n m)
Tactic: congr 2
-- 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
b : SchauderBasis 𝕜 X
n m : ℕ
x : X
⊢ Finset.range n ∩ Finset.range m = Finset.range (min n m)
have e_a : ∀ (a : ℕ), a ∈ Finset.range n ∩ Finset.range m ↔ a ∈ Finset.range (min n m)
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
b : SchauderBasis 𝕜 X
n m : ℕ
x : X
a : ℕ
⊢ a ∈ Finset.range n ∩ Finset.range m ↔ a ∈ Finset.range (min n m)
have e_a : a < n ∧ a < m ↔ a < min n m
Tactic: simp only [Finset.mem_inter, Finset.mem_range]
-- 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
b : SchauderBasis 𝕜 X
inst_3 : CompleteSpace X
⊢ ∃ (C : ℝ), ∀ (n : ℕ), ‖b.proj n‖ ≤ C
have h : ∀ (x : X), ∃ (C : ℝ), ∀ (i : ℕ), norm (E := X) ((b.proj 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
b : SchauderBasis 𝕜 X
inst_3 : CompleteSpace X
x : X
⊢ ∃ (C : ℝ), ∀ (i : ℕ), norm (E := X) ((b.proj i : (a : X) → X) x : X) ≤ C
have h : ∀ (M : ℝ)
  (hM : ∀ (x_1 : X), Membership.mem (γ := Set X) (Set.range fun (n : ℕ) ↦ (b.proj n : (a : X) → X) x) x_1 → ‖x_1‖ ≤ M),
  ∃ (C : ℝ), ∀ (i : ℕ), norm (E := X) ((b.proj i : (a : X) → X) x : X) ≤ C
Tactic: obtain ⟨M, hM⟩ := isBounded_iff_forall_norm_le.mp
    (Metric.isBounded_range_of_tendsto (fun n ↦ b.proj n x) (tendsto_proj b x))
-- 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
b : SchauderBasis 𝕜 X
inst_3 : CompleteSpace X
⊢ BddAbove (α := ℝ≥0) (Set.range fun (n : ℕ) ↦ ‖b.proj n‖₊)
have obtain : ∀ (C : ℝ) (hC : ∀ (n : ℕ), ‖b.proj n‖ ≤ C), BddAbove (α := ℝ≥0) (Set.range fun (n : ℕ) ↦ ‖b.proj n‖₊)
Tactic: obtain ⟨C, hC⟩ := b.exists_norm_proj_le
-- 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
b : SchauderBasis 𝕜 X
inst_3 : CompleteSpace X
C : ℝ
hC : ∀ (n : ℕ), ‖b.proj n‖ ≤ C
⊢ BddAbove (α := ℝ≥0) (Set.range fun (n : ℕ) ↦ ‖b.proj n‖₊)
have hCpos : 0 ≤ C
Tactic: have hCpos : 0 ≤ C := by simpa [proj_zero] using hC 0
-- 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
b : SchauderBasis 𝕜 X
inst_3 : CompleteSpace X
C : ℝ
hC : ∀ (n : ℕ), ‖b.proj n‖ ≤ C
hCpos : 0 ≤ C
⊢ BddAbove (α := ℝ≥0) (Set.range fun (n : ℕ) ↦ ‖b.proj n‖₊)
have refine : Membership.mem (γ := Set ℝ≥0) (upperBounds (Set.range fun (n : ℕ) ↦ ‖b.proj n‖₊)) C.toNNReal
Tactic: refine ⟨C.toNNReal, ?_⟩
-- 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
b : SchauderBasis 𝕜 X
inst_3 : CompleteSpace X
C : ℝ
hC : ∀ (n : ℕ), ‖b.proj n‖ ≤ C
hCpos : 0 ≤ C
n : ℕ
⊢ (fun (n : ℕ) ↦ ‖b.proj n‖₊) n ≤ C.toNNReal
have rw : ‖b.proj n‖ ≤ C
Tactic: rw [← NNReal.coe_le_coe, Real.coe_toNNReal C hCpos, coe_nnnorm]
-- 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
P : ℕ → X →L[𝕜] X
h0 : P 0 = 0
n : ℕ
ih : ∑ i ∈ Finset.range n, succSub P i = P n
⊢ ∑ i ∈ Finset.range (n + 1), succSub P i = P (n + 1)
have succ : P n + (P (n + 1) - P n) = P (n + 1)
Tactic: rw [Finset.sum_range_succ, ih, succSub]
-- 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
P : ℕ → X →L[𝕜] X
h0 : P 0 = 0
n : ℕ
⊢ ∑ i ∈ Finset.range n, succSub P i = P n
have zero : ∑ i ∈ Finset.range 0, succSub P i = P 0
Tactic: induction n with
  | zero => simp [h0]
  | succ n ih => rw [Finset.sum_range_succ, ih, succSub]; abel
Cleared hypotheses: n
-- 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
P : ℕ → X →L[𝕜] X
h0 : P 0 = 0
n : ℕ
zero : ∑ i ∈ Finset.range 0, succSub P i = P 0
⊢ ∑ i ∈ Finset.range n, succSub P i = P n
have succ : ∀ (n : ℕ) (ih : ∑ i ∈ Finset.range n, succSub P i = P n), ∑ i ∈ Finset.range (n + 1), succSub P i = P (n + 1)
Tactic: induction n with
  | zero => simp [h0]
  | succ n ih => rw [Finset.sum_range_succ, ih, succSub]; abel
Cleared hypotheses: n
-- 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
P : ℕ → X →L[𝕜] X
hcomp :
  ∀ (n m : ℕ) (x : X),
    Eq (α := X) ((P n : (a : X) → X) ((P m : (a : X) → X) x : X) : X) ((P (min n m) : (a : X) → X) x : X)
i j : ℕ
x : X
⊢ Eq (α := X) ((succSub P i : (a : X) → X) ((succSub P j : (a : X) → X) x : X) : X)
    (if i = j then (succSub P j : (a : X) → X) x else 0 : X)
have simp : HSub.hSub (α := X) (β := X) ((P (min i j + 1) : (a : X) → X) x : X) ((P (min i (j + 1)) : (a : X) → X) x : X) -
    HSub.hSub (α := X) (β := X) ((P (min (i + 1) j) : (a : X) → X) x : X) ((P (min i j) : (a : X) → X) x : X) =
  if i = j then HSub.hSub (α := X) (β := X) ((P (j + 1) : (a : X) → X) x : X) ((P j : (a : X) → X) x : X) else 0
Tactic: simp only [succSub, ContinuousLinearMap.sub_apply, map_sub, hcomp,
    Nat.add_min_add_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
P : ℕ → X →L[𝕜] X
hcomp :
  ∀ (n m : ℕ) (x : X),
    Eq (α := X) ((P n : (a : X) → X) ((P m : (a : X) → X) x : X) : X) ((P (min n m) : (a : X) → X) x : X)
i j : ℕ
x : X
⊢ HSub.hSub (α := X) (β := X) ((P (min i j + 1) : (a : X) → X) x : X) ((P (min i (j + 1)) : (a : X) → X) x : X) -
      HSub.hSub (α := X) (β := X) ((P (min (i + 1) j) : (a : X) → X) x : X) ((P (min i j) : (a : X) → X) x : X) =
    if i = j then HSub.hSub (α := X) (β := X) ((P (j + 1) : (a : X) → X) x : X) ((P j : (a : X) → X) x : X) else 0
have pos : ∀ (h : i = j),
  HSub.hSub (α := X) (β := X) ((P (min i j + 1) : (a : X) → X) x : X) ((P (min i (j + 1)) : (a : X) → X) x : X) -
      HSub.hSub (α := X) (β := X) ((P (min (i + 1) j) : (a : X) → X) x : X) ((P (min i j) : (a : X) → X) x : X) =
    HSub.hSub (α := X) (β := X) ((P (j + 1) : (a : X) → X) x : X) ((P j : (a : X) → X) x : X)
Tactic: split_ifs with h
-- 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
P : ℕ → X →L[𝕜] X
hcomp :
  ∀ (n m : ℕ) (x : X),
    Eq (α := X) ((P n : (a : X) → X) ((P m : (a : X) → X) x : X) : X) ((P (min n m) : (a : X) → X) x : X)
i j : ℕ
x : X
pos :
  ∀ (h : i = j),
    HSub.hSub (α := X) (β := X) ((P (min i j + 1) : (a : X) → X) x : X) ((P (min i (j + 1)) : (a : X) → X) x : X) -
        HSub.hSub (α := X) (β := X) ((P (min (i + 1) j) : (a : X) → X) x : X) ((P (min i j) : (a : X) → X) x : X) =
      HSub.hSub (α := X) (β := X) ((P (j + 1) : (a : X) → X) x : X) ((P j : (a : X) → X) x : X)
⊢ HSub.hSub (α := X) (β := X) ((P (min i j + 1) : (a : X) → X) x : X) ((P (min i (j + 1)) : (a : X) → X) x : X) -
      HSub.hSub (α := X) (β := X) ((P (min (i + 1) j) : (a : X) → X) x : X) ((P (min i j) : (a : X) → X) x : X) =
    if i = j then HSub.hSub (α := X) (β := X) ((P (j + 1) : (a : X) → X) x : X) ((P j : (a : X) → X) x : X) else 0
have neg : ∀ (h : ¬i = j),
  HSub.hSub (α := X) (β := X) ((P (min i j + 1) : (a : X) → X) x : X) ((P (min i (j + 1)) : (a : X) → X) x : X) -
      HSub.hSub (α := X) (β := X) ((P (min (i + 1) j) : (a : X) → X) x : X) ((P (min i j) : (a : X) → X) x : X) =
    0
Tactic: split_ifs with h
-- 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
P : ℕ → X →L[𝕜] X
hcomp :
  ∀ (n m : ℕ) (x : X),
    Eq (α := X) ((P n : (a : X) → X) ((P m : (a : X) → X) x : X) : X) ((P (min n m) : (a : X) → X) x : X)
i j : ℕ
x : X
h : i = j
⊢ HSub.hSub (α := X) (β := X) ((P (min i j + 1) : (a : X) → X) x : X) ((P (min i (j + 1)) : (a : X) → X) x : X) -
      HSub.hSub (α := X) (β := X) ((P (min (i + 1) j) : (a : X) → X) x : X) ((P (min i j) : (a : X) → X) x : X) =
    HSub.hSub (α := X) (β := X) ((P (j + 1) : (a : X) → X) x : X) ((P j : (a : X) → X) x : X)
have pos : HSub.hSub (α := X) (β := X) ((P (j + 1) : (a : X) → X) x : X) ((P j : (a : X) → X) x : X) -
    HSub.hSub (α := X) (β := X) ((P j : (a : X) → X) x : X) ((P j : (a : X) → X) x : X) =
  HSub.hSub (α := X) (β := X) ((P (j + 1) : (a : X) → X) x : X) ((P j : (a : X) → X) x : X)
Tactic: rw [h, min_self, min_eq_right (Nat.le_succ j), Nat.min_eq_left (Nat.le_succ j)]
-- 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
P : ℕ → X →L[𝕜] X
hcomp :
  ∀ (n m : ℕ) (x : X),
    Eq (α := X) ((P n : (a : X) → X) ((P m : (a : X) → X) x : X) : X) ((P (min n m) : (a : X) → X) x : X)
i j : ℕ
x : X
h : ¬i = j
⊢ HSub.hSub (α := X) (β := X) ((P (min i j + 1) : (a : X) → X) x : X) ((P (min i (j + 1)) : (a : X) → X) x : X) -
      HSub.hSub (α := X) (β := X) ((P (min (i + 1) j) : (a : X) → X) x : X) ((P (min i j) : (a : X) → X) x : X) =
    0
have neg : ∀ (h' : i < j),
  HSub.hSub (α := X) (β := X) ((P (min i j + 1) : (a : X) → X) x : X) ((P (min i (j + 1)) : (a : X) → X) x : X) -
      HSub.hSub (α := X) (β := X) ((P (min (i + 1) j) : (a : X) → X) x : X) ((P (min i j) : (a : X) → X) x : X) =
    0
Tactic: rcases Nat.lt_or_gt_of_ne h with h' | h'