awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
D : RankOneDecomposition 𝕜 X
n : ℕ
x : X
S : X →ₗ[𝕜] X := (↑(succSub D.P n) : X →ₗ[𝕜] X)
hrank : Module.finrank.{u_1, u_2} 𝕜 ↥S.range = 1
this : FiniteDimensional.{u_1, u_2} 𝕜 ↥S.range
⊢ ∃ (c : 𝕜), c • D.e n = (succSub D.P n : (a : X) → X) x
have hspan : 𝕜 ∙ D.e n = S.range
Tactic: have hspan : Submodule.span 𝕜 {D.e n} = S.range := by
    apply Submodule.eq_of_le_of_finrank_eq
    · exact (Submodule.span_singleton_le_iff_mem _ _).mpr (D.e_mem_range n)
    · simp [hrank, finrank_span_singleton (D.e_ne_zero 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
β : Type u_3
L : SummationFilter β
b : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : (n : ℕ) → (x : X) → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n : (a : X) → X) x = coeff n x • D.e n
n : ℕ
c : 𝕜
x : X
⊢ Eq.{u_2 + 1} (α := X) ((fun (x : 𝕜) ↦ x • D.e n) (coeff n (c • x)))
    ((fun (x : 𝕜) ↦ x • D.e n) (HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) (coeff n x)))
have dsimp : coeff n (c • x) • D.e n = (c • coeff n x) • D.e n
Tactic: dsimp only [RingHom.id_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
L : SummationFilter β
b : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : (n : ℕ) → (x : X) → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n : (a : X) → X) x = coeff n x • D.e n
n : ℕ
c : 𝕜
x : X
⊢ coeff n (c • x) • D.e n = (c • coeff n x) • D.e n
have rw : coeff n (c • x) • D.e n = (c * coeff n x) • D.e n
Tactic: rw [smul_eq_mul, ← smul_smul, ← hcoeff, ← hcoeff, map_smul]
-- 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 : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : (n : ℕ) → (x : X) → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n : (a : X) → X) x = coeff n x • D.e n
n : ℕ
c : 𝕜
x : X
rw : coeff n (c • x) • D.e n = (c * coeff n x) • D.e n
⊢ coeff n (c • x) • D.e n = (c • coeff n x) • D.e n
have rw₁ : coeff n (c • x) • D.e n = c • coeff n x • D.e n
Tactic: rw [smul_eq_mul, ← smul_smul, ← hcoeff, ← hcoeff, map_smul]
-- 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 : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : (n : ℕ) → (x : X) → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n : (a : X) → X) x = coeff n x • D.e n
n : ℕ
c : 𝕜
x : X
rw : coeff n (c • x) • D.e n = (c * coeff n x) • D.e n
rw₁ : coeff n (c • x) • D.e n = c • coeff n x • D.e n
⊢ coeff n (c • x) • D.e n = (c • coeff n x) • D.e n
have rw₂ : (succSub D.P n : (a : X) → X) (c • x) = c • coeff n x • D.e n
Tactic: rw [smul_eq_mul, ← smul_smul, ← hcoeff, ← hcoeff, map_smul]
-- 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 : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : (n : ℕ) → (x : X) → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n : (a : X) → X) x = coeff n x • D.e n
n : ℕ
c : 𝕜
x : X
rw : coeff n (c • x) • D.e n = (c * coeff n x) • D.e n
rw₁ : coeff n (c • x) • D.e n = c • coeff n x • D.e n
rw₂ : (succSub D.P n : (a : X) → X) (c • x) = c • coeff n x • D.e n
⊢ coeff n (c • x) • D.e n = (c • coeff n x) • D.e n
have rw₃ : (succSub D.P n : (a : X) → X) (c • x) = HSMul.hSMul (β := X) c ((succSub D.P n : (a : X) → X) x : X)
Tactic: rw [smul_eq_mul, ← smul_smul, ← hcoeff, ← hcoeff, map_smul]
-- 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 : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : (n : ℕ) → (x : X) → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n : (a : X) → X) x = coeff n x • D.e n
n : ℕ
c : 𝕜
x : X
rw : coeff n (c • x) • D.e n = (c * coeff n x) • D.e n
rw₁ : coeff n (c • x) • D.e n = c • coeff n x • D.e n
rw₂ : (succSub D.P n : (a : X) → X) (c • x) = c • coeff n x • D.e n
rw₃ : (succSub D.P n : (a : X) → X) (c • x) = HSMul.hSMul (β := X) c ((succSub D.P n : (a : X) → X) x : X)
⊢ coeff n (c • x) • D.e n = (c • coeff n x) • D.e n
have rw₄ : HSMul.hSMul (β := X) c ((succSub D.P n : (a : X) → X) x : X) =
  HSMul.hSMul (β := X) c ((succSub D.P n : (a : X) → X) x : X)
Tactic: rw [smul_eq_mul, ← smul_smul, ← hcoeff, ← hcoeff, map_smul]
-- 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 : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : (n : ℕ) → (x : X) → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n : (a : X) → X) x = coeff n x • D.e n
n : ℕ
x : X
⊢ norm.{u_1} (E := 𝕜) (({ toFun := coeff n, map_add' := ⋯, map_smul' := ⋯ : X →ₗ[𝕜] 𝕜 } : (a : X) → 𝕜) x : 𝕜) ≤
    ‖succSub D.P n‖ / ‖D.e n‖ * ‖x‖
have rw : norm.{u_1} (E := 𝕜) (({ toFun := coeff n, map_add' := sorry, map_smul' := sorry : X →ₗ[𝕜] 𝕜 } : (a : X) → 𝕜) x : 𝕜) * ‖D.e n‖ ≤
  ‖succSub D.P n‖ * ‖x‖
Tactic: rw [div_mul_eq_mul_div, le_div_iff₀ (norm_pos_iff.mpr (D.e_ne_zero 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
β : Type u_3
L : SummationFilter β
b : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : (n : ℕ) → (x : X) → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n : (a : X) → X) x = coeff n x • D.e n
n : ℕ
x : X
⊢ ‖coeff n x • D.e n‖ = norm (E := X) ((succSub D.P n : (a : X) → X) x : X)
have rw : ‖coeff n x • D.e n‖ = ‖coeff n x • D.e n‖
Tactic: rw [hcoeff]
-- 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 : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : (n : ℕ) → (x : X) → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n : (a : X) → X) x = coeff n x • D.e n
n : ℕ
x : X
⊢ norm.{u_1} (E := 𝕜) (({ toFun := coeff n, map_add' := ⋯, map_smul' := ⋯ : X →ₗ[𝕜] 𝕜 } : (a : X) → 𝕜) x : 𝕜) *
      ‖D.e n‖ ≤
    ‖succSub D.P n‖ * ‖x‖
have calc : ‖coeff n x • D.e n‖ = norm (E := X) ((succSub D.P n : (a : X) → X) x : X)
Tactic: calc ‖coeff n x‖ * ‖D.e n‖ = ‖coeff n x • D.e n‖ := (norm_smul _ _).symm
          _ = ‖(succSub D.P n) x‖ := by rw [hcoeff]
          _ ≤ ‖succSub D.P n‖ * ‖x‖ := ContinuousLinearMap.le_opNorm _ _
-- 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 : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : (n : ℕ) → (x : X) → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n : (a : X) → X) x = coeff n x • D.e n
i j : ℕ
⊢ Eq.{u_2 + 1} (α := X)
    ((fun (x : 𝕜) ↦ x • D.e i)
      (((mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (σ := RingHom.id 𝕜) { toFun := coeff i, map_add' := ⋯, map_smul' := ⋯ }
              (‖succSub D.P i‖ / ‖D.e i‖) ⋯ :
            X →L[𝕜] 𝕜) :
          (a : X) → 𝕜)
        (D.e j)))
    ((fun (x : 𝕜) ↦ x • D.e i) (Pi.single (M := fun (a : ℕ) ↦ 𝕜) j 1 i))
have obtain : ∀ (x : X) (hx : (succSub D.P j : (a : X) → X) x = D.e j),
  Eq.{u_2 + 1} (α := X)
    ((fun (x : 𝕜) ↦ x • D.e i)
      (((mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (σ := RingHom.id 𝕜) { toFun := coeff i, map_add' := sorry, map_smul' := sorry }
              (‖succSub D.P i‖ / ‖D.e i‖) sorry :
            X →L[𝕜] 𝕜) :
          (a : X) → 𝕜)
        (D.e j)))
    ((fun (x : 𝕜) ↦ x • D.e i) (Pi.single (M := fun (a : ℕ) ↦ 𝕜) j 1 i))
Tactic: obtain ⟨x, hx⟩ : ∃ x, (succSub D.P j) x = D.e j := D.e_mem_range 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
β : Type u_3
L : SummationFilter β
b : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : (n : ℕ) → (x : X) → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n : (a : X) → X) x = coeff n x • D.e n
i j : ℕ
x : X
hx : (succSub D.P j : (a : X) → X) x = D.e j
⊢ Eq.{u_2 + 1} (α := X)
    ((fun (x : 𝕜) ↦ x • D.e i)
      (((mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (σ := RingHom.id 𝕜) { toFun := coeff i, map_add' := ⋯, map_smul' := ⋯ }
              (‖succSub D.P i‖ / ‖D.e i‖) ⋯ :
            X →L[𝕜] 𝕜) :
          (a : X) → 𝕜)
        (D.e j)))
    ((fun (x : 𝕜) ↦ x • D.e i) (Pi.single (M := fun (a : ℕ) ↦ 𝕜) j 1 i))
have simp : coeff i (D.e j) • D.e i = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (Pi.single (M := fun (a : ℕ) ↦ 𝕜) j 1 i : 𝕜) (D.e i)
Tactic: simp only [mkContinuous_apply, LinearMap.coe_mk, AddHom.coe_mk]
-- 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 : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : (n : ℕ) → (x : X) → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n : (a : X) → X) x = coeff n x • D.e n
i j : ℕ
x : X
hx : (succSub D.P j : (a : X) → X) x = D.e j
⊢ coeff i (D.e j) • D.e i = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (Pi.single (M := fun (a : ℕ) ↦ 𝕜) j 1 i : 𝕜) (D.e i)
have rw : (if i = j then D.e j else 0) = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (Pi.single (M := fun (a : ℕ) ↦ 𝕜) j 1 i : 𝕜) (D.e i)
Tactic: rw [← hcoeff, ← hx, succSub_ortho D.proj_comp, hx]
-- 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 : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : (n : ℕ) → (x : X) → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n : (a : X) → X) x = coeff n x • D.e n
i j : ℕ
x : X
hx : (succSub D.P j : (a : X) → X) x = D.e j
⊢ (if i = j then D.e j else 0) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (Pi.single (M := fun (a : ℕ) ↦ 𝕜) j 1 i : 𝕜) (D.e i)
have simp : (if i = j then D.e j else 0) = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (if i = j then 1 else 0) (D.e i)
Tactic: simp only [Pi.single_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
L : SummationFilter β
b : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : (n : ℕ) → (x : X) → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n : (a : X) → X) x = coeff n x • D.e n
i j : ℕ
x : X
hx : (succSub D.P j : (a : X) → X) x = D.e j
⊢ (if i = j then D.e j else 0) = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (if i = j then 1 else 0) (D.e i)
have pos : ∀ (h : i = j), D.e j = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 (D.e i)
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
β : Type u_3
L : SummationFilter β
b : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : (n : ℕ) → (x : X) → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n : (a : X) → X) x = coeff n x • D.e n
i j : ℕ
x : X
hx : (succSub D.P j : (a : X) → X) x = D.e j
pos : ∀ (h : i = j), D.e j = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 (D.e i)
⊢ (if i = j then D.e j else 0) = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (if i = j then 1 else 0) (D.e i)
have neg : ∀ (h : ¬i = j), 0 = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 (D.e i)
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
β : Type u_3
L : SummationFilter β
b : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : (n : ℕ) → (x : X) → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n : (a : X) → X) x = coeff n x • D.e n
x : X
⊢ HasSum
    (fun (i : ℕ) ↦
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜)
        (((mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (σ := RingHom.id 𝕜) { toFun := coeff i, map_add' := ⋯, map_smul' := ⋯ }
                  (‖succSub D.P i‖ / ‖D.e i‖) ⋯ :
                X →L[𝕜] 𝕜) :
              (a : X) → 𝕜)
            x :
          𝕜)
        (D.e i))
    x (SummationFilter.conditional ℕ)
have rw : Tendsto
  ((fun (s : Finset ℕ) ↦
      ∑ b ∈ s,
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜)
          (((mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (σ := RingHom.id 𝕜)
                    { toFun := coeff b, map_add' := sorry, map_smul' := sorry : X →ₗ[𝕜] 𝕜 } (‖succSub D.P b‖ / ‖D.e b‖) sorry :
                  X →L[𝕜] 𝕜) :
                (a : X) → 𝕜)
              x :
            𝕜)
          (D.e b)) ∘
    Finset.range)
  atTop (𝓝 x)
Tactic: rw [HasSum, SummationFilter.conditional_filter_eq_map_range, tendsto_map'_iff]
-- 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 : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : (n : ℕ) → (x : X) → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n : (a : X) → X) x = coeff n x • D.e n
x : X
n : ℕ
⊢ Eq (α := X) ((D.P n : (a : X) → X) x : X)
    (((fun (s : Finset ℕ) ↦
            ∑ b ∈ s,
              HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜)
                (((mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (σ := RingHom.id 𝕜)
                          { toFun := coeff b, map_add' := ⋯, map_smul' := ⋯ } (‖succSub D.P b‖ / ‖D.e b‖) ⋯ :
                        X →L[𝕜] 𝕜) :
                      (a : X) → 𝕜)
                    x :
                  𝕜)
                (D.e b)) ∘
          Finset.range)
        n :
      X)
have simp : Eq (α := X) ((D.P n : (a : X) → X) x : X) (∑ x_1 ∈ Finset.range n, (succSub D.P x_1 : (a : X) → X) x : X)
Tactic: simp only [Function.comp, LinearMap.coe_mk, AddHom.coe_mk,
                   LinearMap.mkContinuous_apply, ← hcoeff]
-- 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 : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : (n : ℕ) → (x : X) → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n : (a : X) → X) x = coeff n x • D.e n
x : X
n : ℕ
⊢ Eq (α := X) ((D.P n : (a : X) → X) x : X) (∑ x_1 ∈ Finset.range n, (succSub D.P x_1 : (a : X) → X) x : X)
have rw : Eq (α := X) ((D.P n : (a : X) → X) x : X) ((∑ d ∈ Finset.range n, succSub D.P d : (a : X) → X) x : X)
Tactic: rw [← ContinuousLinearMap.sum_apply, sum_succSub D.P D.proj_zero]
-- 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 : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : (n : ℕ) → (x : X) → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n : (a : X) → X) x = coeff n x • D.e n
x : X
n : ℕ
rw : Eq (α := X) ((D.P n : (a : X) → X) x : X) ((∑ d ∈ Finset.range n, succSub D.P d : (a : X) → X) x : X)
⊢ Eq (α := X) ((D.P n : (a : X) → X) x : X) (∑ x_1 ∈ Finset.range n, (succSub D.P x_1 : (a : X) → X) x : X)
have rw₁ : Eq (α := X) ((D.P n : (a : X) → X) x : X) ((D.P n : (a : X) → X) x : X)
Tactic: rw [← ContinuousLinearMap.sum_apply, sum_succSub D.P D.proj_zero]
-- 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
D : RankOneDecomposition 𝕜 X
⊢ D.basis.proj = D.P
have h : ∀ (n : ℕ) (x : X), Eq (α := X) ((D.basis.proj n : (a : X) → X) x : X) ((D.P n : (a : X) → X) x : X)
Tactic: ext 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
D : RankOneDecomposition 𝕜 X
n : ℕ
x : X
⊢ Eq (α := X) ((D.basis.proj n : (a : X) → X) x : X) ((D.P n : (a : X) → X) x : X)
have h : Eq (α := X)
  (∑ i ∈ Finset.range n,
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((D.basis.coord i : (a : X) → 𝕜) x : 𝕜) ((↑D.basis : ℕ → X) i) :
    X)
  ((∑ i ∈ Finset.range n, succSub D.P i : (a : X) → X) x : X)
Tactic: rw [SchauderBasis.proj_apply, ← sum_succSub D.P D.proj_zero 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
D : RankOneDecomposition 𝕜 X
n : ℕ
x : X
⊢ Eq (α := X)
    (∑ i ∈ Finset.range n,
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((D.basis.coord i : (a : X) → 𝕜) x : 𝕜) ((↑D.basis : ℕ → X) i) :
      X)
    ((∑ i ∈ Finset.range n, succSub D.P i : (a : X) → X) x : X)
have h : Eq.{u_2 + 1} (α := X)
  (∑ i ∈ Finset.range n,
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((D.basis.coord i : (a : X) → 𝕜) x : 𝕜) ((↑D.basis : ℕ → X) i))
  (∑ c ∈ Finset.range n, (succSub D.P c : (a : X) → X) x)
Tactic: simp only [ContinuousLinearMap.coe_sum', Finset.sum_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
D : RankOneDecomposition 𝕜 X
n : ℕ
x : X
⊢ Eq.{u_2 + 1} (α := X)
    (∑ i ∈ Finset.range n,
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((D.basis.coord i : (a : X) → 𝕜) x : 𝕜) ((↑D.basis : ℕ → X) i))
    (∑ c ∈ Finset.range n, (succSub D.P c : (a : X) → X) x)
have h : ∀ i ∈ Finset.range n,
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((D.basis.coord i : (a : X) → 𝕜) x : 𝕜) ((↑D.basis : ℕ → X) i) =
    (succSub D.P i : (a : X) → X) x
Tactic: refine Finset.sum_congr rfl fun i _ ↦ ?_
-- 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
D : RankOneDecomposition 𝕜 X
n : ℕ
x : X
i : ℕ
h : i ∈ Finset.range n
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((D.basis.coord i : (a : X) → 𝕜) x : 𝕜) ((↑D.basis : ℕ → X) i) =
    (succSub D.P i : (a : X) → X) x
have h : D.basisCoeff i x • D.e i = (succSub D.P i : (a : X) → X) x
Tactic: dsimp [basis, mkContinuous_apply, IsLinearMap.mk'_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
D : RankOneDecomposition 𝕜 X
n : ℕ
x : X
i : ℕ
h : i ∈ Finset.range n
⊢ D.basisCoeff i x • D.e i = (succSub D.P i : (a : X) → X) x
have h : Eq (α := X) ((succSub D.P i : (a : X) → X) x : X) ((succSub D.P i : (a : X) → X) x : X)
Tactic: rw [basisCoeff_spec]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℤ
x : E
⊢ ‖n • x‖ = norm.{u_1} (E := 𝕜) (↑n : 𝕜) * ‖x‖
have rw : ‖n • x‖ = ‖HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n : 𝕜) x‖
Tactic: rw [← norm_smul, ← Int.smul_one_eq_cast, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℤ
x : E
rw : ‖n • x‖ = ‖HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n : 𝕜) x‖
⊢ ‖n • x‖ = norm.{u_1} (E := 𝕜) (↑n : 𝕜) * ‖x‖
have rw₁ : ‖n • x‖ = ‖HSMul.hSMul (β := 𝕜) n 1 • x‖
Tactic: rw [← norm_smul, ← Int.smul_one_eq_cast, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℤ
x : E
rw : ‖n • x‖ = ‖HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n : 𝕜) x‖
rw₁ : ‖n • x‖ = ‖HSMul.hSMul (β := 𝕜) n 1 • x‖
⊢ ‖n • x‖ = norm.{u_1} (E := 𝕜) (↑n : 𝕜) * ‖x‖
have rw₂ : ‖n • x‖ = ‖n • HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 1 x‖
Tactic: rw [← norm_smul, ← Int.smul_one_eq_cast, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℤ
x : E
rw : ‖n • x‖ = ‖HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n : 𝕜) x‖
rw₁ : ‖n • x‖ = ‖HSMul.hSMul (β := 𝕜) n 1 • x‖
rw₂ : ‖n • x‖ = ‖n • HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 1 x‖
⊢ ‖n • x‖ = norm.{u_1} (E := 𝕜) (↑n : 𝕜) * ‖x‖
have rw₃ : ‖n • x‖ = ‖n • x‖
Tactic: rw [← norm_smul, ← Int.smul_one_eq_cast, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
α : Type u_6
inst : SeminormedRing α
inst_1 : NormSMulClass ℤ α
n : ℤ
⊢ norm.{u_6} (E := α) (↑n : α) = (↑|n| : ℝ) * norm.{u_6} (E := α) 1
have rw : ‖HSMul.hSMul (β := α) n 1‖ = (↑|n| : ℝ) * norm.{u_6} (E := α) 1
Tactic: rw [← zsmul_one, norm_smul, Int.norm_eq_abs, Int.cast_abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
α : Type u_6
inst : SeminormedRing α
inst_1 : NormSMulClass ℤ α
n : ℤ
rw : ‖HSMul.hSMul (β := α) n 1‖ = (↑|n| : ℝ) * norm.{u_6} (E := α) 1
⊢ norm.{u_6} (E := α) (↑n : α) = (↑|n| : ℝ) * norm.{u_6} (E := α) 1
have rw₁ : ‖n‖ * norm.{u_6} (E := α) 1 = (↑|n| : ℝ) * norm.{u_6} (E := α) 1
Tactic: rw [← zsmul_one, norm_smul, Int.norm_eq_abs, Int.cast_abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
α : Type u_6
inst : SeminormedRing α
inst_1 : NormSMulClass ℤ α
n : ℤ
rw : ‖HSMul.hSMul (β := α) n 1‖ = (↑|n| : ℝ) * norm.{u_6} (E := α) 1
rw₁ : ‖n‖ * norm.{u_6} (E := α) 1 = (↑|n| : ℝ) * norm.{u_6} (E := α) 1
⊢ norm.{u_6} (E := α) (↑n : α) = (↑|n| : ℝ) * norm.{u_6} (E := α) 1
have rw₂ : |(↑n : ℝ)| * norm.{u_6} (E := α) 1 = (↑|n| : ℝ) * norm.{u_6} (E := α) 1
Tactic: rw [← zsmul_one, norm_smul, Int.norm_eq_abs, Int.cast_abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
Goal:
α : Type u_6
inst : SeminormedRing α
inst_1 : NormSMulClass ℤ α
n : ℤ
rw : ‖HSMul.hSMul (β := α) n 1‖ = (↑|n| : ℝ) * norm.{u_6} (E := α) 1
rw₁ : ‖n‖ * norm.{u_6} (E := α) 1 = (↑|n| : ℝ) * norm.{u_6} (E := α) 1
rw₂ : |(↑n : ℝ)| * norm.{u_6} (E := α) 1 = (↑|n| : ℝ) * norm.{u_6} (E := α) 1
⊢ norm.{u_6} (E := α) (↑n : α) = (↑|n| : ℝ) * norm.{u_6} (E := α) 1
have rw₃ : |(↑n : ℝ)| * norm.{u_6} (E := α) 1 = |(↑n : ℝ)| * norm.{u_6} (E := α) 1
Tactic: rw [← zsmul_one, norm_smul, Int.norm_eq_abs, Int.cast_abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E_1
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E_1
inst_4 : NormedSpace 𝕜 F
E : Type u_6
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℚ E
e : E
⊢ DiscreteTopology.{u_6} ↥(AddSubgroup.zmultiples e)
have this : IsAddTorsionFree E
Tactic: have : IsAddTorsionFree E := .of_module_rat E