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
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‖ = ‖coeff n x • D.e n‖

Tactic:
(norm_smul _ _).symm

Premises used: norm_smul, Eq.symm
-- 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
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
rw rw₁ : ‖coeff n x • D.e n‖ = ‖coeff n x • D.e n‖
⊢ ‖coeff n x • D.e n‖ = norm (E := X) ((succSub D.P n : (a : X) → X) x : X)

Tactic:
rw [hcoeff]
-- 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
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 (E := X) ((succSub D.P n : (a : X) → X) x : X) ≤ ‖succSub D.P n‖ * ‖x‖

Tactic:
ContinuousLinearMap.le_opNorm _ _

Premises used: ContinuousLinearMap.le_opNorm
-- 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
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
calc : ‖coeff n x • D.e n‖ = norm (E := X) ((succSub D.P n : (a : X) → X) 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‖

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 _ _

Premises used: SchauderBasis.succSub, norm_smul, ContinuousLinearMap.le_opNorm, SchauderBasis.RankOneDecomposition.e, Eq.symm, SchauderBasis.RankOneDecomposition.P, 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
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), (succSub D.P j : (a : X) → X) x = D.e j

Tactic:
D.e_mem_range j

Premises used: Set.Mem, setOf, Set.range, SchauderBasis.RankOneDecomposition.e_mem_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
β : 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 : ℕ
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' := ⋯, 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))
⊢ 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))

Tactic:
obtain ⟨x, hx⟩ : ∃ x, (succSub D.P j) x = D.e j := D.e_mem_range j

Premises used: SchauderBasis.RankOneDecomposition.e, SchauderBasis.RankOneDecomposition.e_mem_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
β : 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
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)
⊢ 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))

Tactic:
simp only [mkContinuous_apply, LinearMap.coe_mk, AddHom.coe_mk]

Premises used: LinearMap.coe_mk, LinearMap.mkContinuous_apply, AddHom.coe_mk
-- 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
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
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)
⊢ 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:
rw [← hcoeff, ← hx, succSub_ortho D.proj_comp, hx]

Premises used: SchauderBasis.succSub_ortho, SchauderBasis.RankOneDecomposition.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
β : 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
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)
⊢ (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:
simp only [Pi.single_apply]

Premises used: Pi.single_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
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)
neg : ∀ (h : ¬i = j), 0 = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 (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)

Tactic:
split_ifs with h
-- 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
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
h : i = j
⊢ D.e j = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 (D.e i)

Tactic:
simp [h]
-- 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
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
h : ¬i = j
⊢ 0 = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 (D.e i)

Tactic:
simp [h]
-- 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
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
rw :
  Tendsto
    ((fun (s : Finset ℕ) ↦
        ∑ b ∈ s,
          HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜)
            (((mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (σ := RingHom.id 𝕜)
                      { toFun := coeff b, map_add' := ⋯, map_smul' := ⋯ : X →ₗ[𝕜] 𝕜 } (‖succSub D.P b‖ / ‖D.e b‖) ⋯ :
                    X →L[𝕜] 𝕜) :
                  (a : X) → 𝕜)
                x :
              𝕜)
            (D.e b)) ∘
      Finset.range)
    atTop (𝓝 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 ℕ)

Tactic:
rw [HasSum, SummationFilter.conditional_filter_eq_map_range, tendsto_map'_iff]

Premises used: SummationFilter.conditional_filter_eq_map_range, Filter.tendsto_map'_iff, HasSum, SummationFilter.unconditional
-- 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
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 : ℕ
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)
⊢ 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)

Tactic:
simp only [Function.comp, LinearMap.coe_mk, AddHom.coe_mk,
                   LinearMap.mkContinuous_apply, ← hcoeff]

Premises used: LinearMap.coe_mk, LinearMap.mkContinuous_apply, Function.comp, AddHom.coe_mk
-- 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
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)
rw₁ rw₂ : Eq (α := X) ((D.P n : (a : X) → X) x : X) ((D.P n : (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)

Tactic:
rw [← ContinuousLinearMap.sum_apply, sum_succSub D.P D.proj_zero]

Premises used: ContinuousLinearMap.sum_apply, SchauderBasis.RankOneDecomposition.proj_zero, SchauderBasis.RankOneDecomposition.P, SchauderBasis.sum_succSub
-- 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
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
⊢ Tendsto
    ((fun (s : Finset ℕ) ↦
        ∑ b ∈ s,
          HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜)
            (((mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (σ := RingHom.id 𝕜)
                      { toFun := coeff b, map_add' := ⋯, map_smul' := ⋯ : X →ₗ[𝕜] 𝕜 } (‖succSub D.P b‖ / ‖D.e b‖) ⋯ :
                    X →L[𝕜] 𝕜) :
                  (a : X) → 𝕜)
                x :
              𝕜)
            (D.e b)) ∘
      Finset.range)
    atTop (𝓝 x)

Tactic:
exact (D.proj_tendsto x).congr fun n ↦ by
        simp only [Function.comp, LinearMap.coe_mk, AddHom.coe_mk,
                   LinearMap.mkContinuous_apply, ← hcoeff]
        rw [← ContinuousLinearMap.sum_apply, sum_succSub D.P D.proj_zero]

Premises used: SchauderBasis.RankOneDecomposition.proj_tendsto, Filter.Tendsto.congr
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
D : RankOneDecomposition 𝕜 X
h : ∀ (n : ℕ) (x : X), Eq (α := X) ((D.basis.proj n : (a : X) → X) x : X) ((D.P n : (a : X) → X) x : X)
⊢ D.basis.proj = D.P

Tactic:
ext n _
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
D : RankOneDecomposition 𝕜 X
n : ℕ
x : X
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)
⊢ Eq (α := X) ((D.basis.proj n : (a : X) → X) x : X) ((D.P n : (a : X) → X) x : X)

Tactic:
rw [SchauderBasis.proj_apply, ← sum_succSub D.P D.proj_zero n]

Premises used: SchauderBasis.proj_apply, SchauderBasis.RankOneDecomposition.proj_zero, SchauderBasis.RankOneDecomposition.P, SchauderBasis.sum_succSub
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
D : RankOneDecomposition 𝕜 X
n : ℕ
x : X
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)
⊢ 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:
simp only [ContinuousLinearMap.coe_sum', Finset.sum_apply]

Premises used: Finset.sum_apply, ContinuousLinearMap.coe_sum'
-- Module: Mathlib.Analysis.Normed.Module.Bases
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)

Tactic:
Finset.sum_congr rfl fun i _ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
D : RankOneDecomposition 𝕜 X
n : ℕ
x : X
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
⊢ 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:
refine Finset.sum_congr rfl fun i _ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Normed.Module.Bases
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_1 : i ∈ Finset.range n
h : D.basisCoeff i x • D.e i = (succSub D.P i : (a : X) → X) x
⊢ 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:
dsimp [basis, mkContinuous_apply, IsLinearMap.mk'_apply]

Premises used: LinearMap.mkContinuous_apply, SchauderBasis.RankOneDecomposition.basis, IsLinearMap.mk'_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
D : RankOneDecomposition 𝕜 X
n : ℕ
x : X
i : ℕ
h_1 : i ∈ Finset.range n
h h₁ : Eq (α := X) ((succSub D.P i : (a : X) → X) x : X) ((succSub D.P i : (a : X) → X) x : X)
⊢ D.basisCoeff i x • D.e i = (succSub D.P i : (a : X) → X) x

Tactic:
rw [basisCoeff_spec]

Premises used: SchauderBasis.RankOneDecomposition.basisCoeff_spec
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
D : RankOneDecomposition 𝕜 X
⊢ (↑D.basis : ℕ → X) = D.e

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
α : Type u_5
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
⊢ NormSMulClass 𝕜 E

Tactic:
haveI : IsBoundedSMul 𝕜 E := .of_norm_smul_le NormedSpace.norm_smul_le
  NormedDivisionRing.toNormSMulClass

Premises used: NormedDivisionRing.toNormSMulClass
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
α : Type u_5
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
⊢ IsBoundedSMul 𝕜 E

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Analysis.Normed.Module.Basic
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‖
rw₃ rw₄ : ‖n • x‖ = ‖n • x‖
⊢ ‖n • x‖ = norm.{u_1} (E := 𝕜) (↑n : 𝕜) * ‖x‖

Tactic:
rw [← norm_smul, ← Int.smul_one_eq_cast, smul_assoc, one_smul]

Premises used: Int.smul_one_eq_cast, norm_smul, smul_assoc, one_smul
-- Module: Mathlib.Analysis.Normed.Module.Basic
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
rw₃ rw₄ : |(↑n : ℝ)| * norm.{u_6} (E := α) 1 = |(↑n : ℝ)| * norm.{u_6} (E := α) 1
⊢ norm.{u_6} (E := α) (↑n : α) = (↑|n| : ℝ) * norm.{u_6} (E := α) 1

Tactic:
rw [← zsmul_one, norm_smul, Int.norm_eq_abs, Int.cast_abs]

Premises used: Int.cast_abs, norm_smul, Int.norm_eq_abs, zsmul_one
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
α : Type u_6
inst : SeminormedRing α
inst_1 : NormSMulClass ℤ α
n : ℕ
⊢ norm.{u_6} (E := α) (↑n : α) = (↑n : ℝ) * norm.{u_6} (E := α) 1

Tactic:
simpa using norm_intCast_eq_abs_mul_norm_one α n

Premises used: Nat.cast, norm_intCast_eq_abs_mul_norm_one
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
α : Type u_6
inst : SeminormedRing α
inst_1 : NormOneClass α
inst_2 : NormSMulClass ℤ α
a : ℕ
⊢ norm.{u_6} (E := α) (↑a : α) = (↑a : ℝ)

Tactic:
simpa using norm_natCast_eq_mul_norm_one α a

Premises used: norm_natCast_eq_mul_norm_one
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
x : E
ε : ℝ
h : 0 < ε
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (y : E) ↦ ‖c • (y - x)‖

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
x : E
ε : ℝ
h : 0 < ε
⊢ ‖c • (x - x)‖ = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
α : Type u_5
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : α → 𝕜
g : α → E
l : Filter α
hf : Tendsto f l (𝓝 0)
hg : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (Norm.norm ∘ g)
⊢ Tendsto.{u_5, u_3} (β := E) (fun (x : α) ↦ f x • g x) l (𝓝 0)

Tactic:
hf.op_zero_isBoundedUnder_le hg (· • ·) norm_smul_le

Premises used: norm_smul_le, Filter.Tendsto.op_zero_isBoundedUnder_le, HSMul.hSMul
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
α : Type u_5
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : α → 𝕜
g : α → E
l : Filter α
hf : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ f)
hg : Tendsto g l (𝓝 0)
⊢ Tendsto.{u_5, u_3} (β := E) (fun (x : α) ↦ f x • g x) l (𝓝 0)

Tactic:
hg.op_zero_isBoundedUnder_le hf (flip (· • ·)) fun x y =>
    (norm_smul_le y x).trans_eq (mul_comm _ _)

Premises used: norm_smul_le, Norm.norm, LE.le.trans_eq, Filter.Tendsto.op_zero_isBoundedUnder_le, flip, mul_comm, HSMul.hSMul
-- Module: Mathlib.Analysis.Normed.Module.Basic
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
⊢ IsAddTorsionFree E

Tactic:
have : IsAddTorsionFree E := .of_module_rat E
-- Module: Mathlib.Analysis.Normed.Module.Basic
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
this : IsAddTorsionFree E
inl : DiscreteTopology.{u_6} ↥(AddSubgroup.zmultiples 0)
inr : ∀ (he : e ≠ 0), DiscreteTopology.{u_6} ↥(AddSubgroup.zmultiples e)
⊢ DiscreteTopology.{u_6} ↥(AddSubgroup.zmultiples e)

Tactic:
rcases eq_or_ne e 0 with (rfl | he)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Module.Basic
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
this : IsAddTorsionFree E
inl : DiscreteTopology.{u_6} ↥⊥
⊢ DiscreteTopology.{u_6} ↥(AddSubgroup.zmultiples 0)

Tactic:
rw [AddSubgroup.zmultiples_zero_eq_bot]

Premises used: AddSubgroup.zmultiples_zero_eq_bot
-- Module: Mathlib.Analysis.Normed.Module.Basic
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
this : IsAddTorsionFree E
⊢ DiscreteTopology.{u_6} ↥⊥

Tactic:
Subsingleton.discreteTopology (α := ↑(⊥ : Subspace ℚ E))

Premises used: Set.Mem, Subsingleton.discreteTopology