awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set (↑(sphere 0 r) : Type u_1)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
hr₀ : 0 < r
x : { x : ℝ // Membership.mem (γ := Set ℝ) (Ioi 0) x }
hxU : (↑x : ℝ) ∈ U
this :
  Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
        (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
          (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)) ''
      SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U) ∈
    𝓝 ((↑(y, x).2 : ℝ) • (↑(y, x).1 : E))
a : (↑(sphere 0 r) : Type u_1)
b : (↑(Ioi 0) : Type)
ha : (a, b).1 ∈ V
hb : Membership.mem (γ := Set (↑(Ioi 0) : Type)) (Ioi 0 ↓∩ U) (a, b).2
⊢ (↑(a, b).2 : ℝ) ∈ U

Tactic:
hb

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set (↑(sphere 0 r) : Type u_1)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
hr₀ : 0 < r
x : { x : ℝ // Membership.mem (γ := Set ℝ) (Ioi 0) x }
hxU : (↑x : ℝ) ∈ U
this :
  Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
        (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
          (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)) ''
      SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U) ∈
    𝓝 ((↑(y, x).2 : ℝ) • (↑(y, x).1 : E))
a : (↑(sphere 0 r) : Type u_1)
b : (↑(Ioi 0) : Type)
ha : (a, b).1 ∈ V
hb : Membership.mem (γ := Set (↑(Ioi 0) : Type)) (Ioi 0 ↓∩ U) (a, b).2
⊢ (↑(a, b).1 : E) ∈ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V

Tactic:
mem_image_of_mem _ ha

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set (↑(sphere 0 r) : Type u_1)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
hr₀ : 0 < r
x : { x : ℝ // Membership.mem (γ := Set ℝ) (Ioi 0) x }
hxU : (↑x : ℝ) ∈ U
this :
  Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
        (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
          (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)) ''
      SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U) ∈
    𝓝 ((↑(y, x).2 : ℝ) • (↑(y, x).1 : E))
a : (↑(sphere 0 r) : Type u_1)
b : (↑(Ioi 0) : Type)
ha : (a, b).1 ∈ V
hb : Membership.mem (γ := Set (↑(Ioi 0) : Type)) (Ioi 0 ↓∩ U) (a, b).2
⊢ (↑(a, b).2 : ℝ) ∈ U

Tactic:
exacts [hb, mem_image_of_mem _ ha]

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set (↑(sphere 0 r) : Type u_1)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
hr₀ : 0 < r
x : { x : ℝ // Membership.mem (γ := Set ℝ) (Ioi 0) x }
hxU : (↑x : ℝ) ∈ U
this :
  Membership.mem (γ := Filter E)
    (𝓝[{0}ᶜ]
      (↑((Homeomorph.symm (homeomorphSphereProd E r hr₀) :
              (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1))
            (y, x)) :
        E))
    (Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
        (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
          (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)) ''
      SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U))
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {0}ᶜ

Tactic:
isOpen_compl_singleton

Premises used: isOpen_compl_singleton
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set (↑(sphere 0 r) : Type u_1)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
hr₀ : 0 < r
x : { x : ℝ // Membership.mem (γ := Set ℝ) (Ioi 0) x }
hxU : (↑x : ℝ) ∈ U
this :
  Membership.mem (γ := Filter E)
    (𝓝[{0}ᶜ]
      (↑((Homeomorph.symm (homeomorphSphereProd E r hr₀) :
              (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1))
            (y, x)) :
        E))
    (Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
        (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
          (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)) ''
      SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U))
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {0}ᶜ

Tactic:
exact isOpen_compl_singleton

Premises used: isOpen_compl_singleton
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set (↑(sphere 0 r) : Type u_1)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
hr₀ : 0 < r
x : { x : ℝ // Membership.mem (γ := Set ℝ) (Ioi 0) x }
hxU : (↑x : ℝ) ∈ U
this :
  Membership.mem (γ := Filter E)
    (𝓝[{0}ᶜ]
      (↑((Homeomorph.symm (homeomorphSphereProd E r hr₀) :
              (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1))
            (y, x)) :
        E))
    (Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
        (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
          (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)) ''
      SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U))
⊢ Membership.mem (γ := Set E) {0}ᶜ
    (↑((Homeomorph.symm (homeomorphSphereProd E r hr₀) :
            (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1))
          (y, x)) :
      E)

Tactic:
simp [x.2.out.ne', ne_zero_of_mem_sphere, hr₀.ne']

Premises used: Membership.mem.out, ne_zero_of_mem_sphere, LT.lt.ne', Subtype.property
-- 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 : GeneralSchauderBasis β 𝕜 X L
⊢ LinearIndependent 𝕜 (↑b : β → X)

Tactic:
linearIndependent_iff.mpr (fun l hl ↦ l.ext ?_)

Premises used: Iff.mpr, Finsupp.ext, linearIndependent_iff
-- 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 : GeneralSchauderBasis β 𝕜 X L
refine :
  ∀ (l : β →₀ 𝕜)
    (hl : Eq.{u_2 + 1} (α := X) ((Finsupp.linearCombination 𝕜 (↑b : β → X) : (a : β →₀ 𝕜) → X) l : X) (0 : X)) (a : β),
    Eq.{u_1 + 1} (α := 𝕜) ((l : (a : β) → 𝕜) a : 𝕜) ((0 : (a : β) → 𝕜) a : 𝕜)
⊢ LinearIndependent 𝕜 (↑b : β → X)

Tactic:
refine linearIndependent_iff.mpr (fun l hl ↦ l.ext ?_)

Premises used: Iff.mpr, Finsupp.ext, linearIndependent_iff
-- 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 : GeneralSchauderBasis β 𝕜 X L
l : β →₀ 𝕜
hl : Eq.{u_2 + 1} (α := X) ((Finsupp.linearCombination 𝕜 (↑b : β → X) : (a : β →₀ 𝕜) → X) l : X) (0 : X)
⊢ ∀ (a : β), Eq.{u_1 + 1} (α := 𝕜) ((l : (a : β) → 𝕜) a : 𝕜) ((0 : (a : β) → 𝕜) a : 𝕜)

Tactic:
simpa [l.linearCombination_apply, Finsupp.sum, b.ortho, Pi.single_apply] using
    fun i ↦ congr_arg (b.coord i) hl

Premises used: Pi.single_apply, Finsupp.sum, Finsupp.linearCombination_apply, congr_arg, GeneralSchauderBasis.ortho, GeneralSchauderBasis.coord, 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 : GeneralSchauderBasis β 𝕜 X L
refine :
  ∀ (l : β →₀ 𝕜)
    (hl : Eq.{u_2 + 1} (α := X) ((Finsupp.linearCombination 𝕜 (↑b : β → X) : (a : β →₀ 𝕜) → X) l : X) (0 : X)) (a : β),
    Eq.{u_1 + 1} (α := 𝕜) ((l : (a : β) → 𝕜) a : 𝕜) ((0 : (a : β) → 𝕜) a : 𝕜)
⊢ LinearIndependent 𝕜 (↑b : β → X)

Tactic:
classical
  refine linearIndependent_iff.mpr (fun l hl ↦ l.ext ?_)
  simpa [l.linearCombination_apply, Finsupp.sum, b.ortho, Pi.single_apply] using
    fun i ↦ congr_arg (b.coord i) hl

Premises used: Iff.mpr, Finsupp.ext, Pi.single_apply, Finsupp.sum, GeneralSchauderBasis.ortho, linearIndependent_iff
-- 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 : GeneralSchauderBasis β 𝕜 X L
⊢ b.proj ∅ = 0

Tactic:
simp [proj]

Premises used: GeneralSchauderBasis.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
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A : Finset β
x : X
⊢ Eq (α := X) ((b.proj A : (a : X) → X) x : X)
    (∑ i ∈ A, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i) : X)

Tactic:
simp [proj, ContinuousLinearMap.sum_apply, ContinuousLinearMap.smulRight_apply]

Premises used: ContinuousLinearMap.sum_apply, GeneralSchauderBasis.proj, ContinuousLinearMap.smulRight_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 : GeneralSchauderBasis β 𝕜 X L
A : Finset β
i : β
⊢ (b.proj A : (a : X) → X) ((↑b : β → X) i) = if i ∈ A then (↑b : β → X) i else 0

Tactic:
simp [b.ortho, Pi.single_apply]

Premises used: Pi.single_apply, GeneralSchauderBasis.ortho
-- 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 : GeneralSchauderBasis β 𝕜 X L
x : X
⊢ Tendsto (fun (A : Finset β) ↦ (b.proj A : (a : X) → X) x) L.filter (𝓝 x)

Tactic:
simpa using b.expansion x

Premises used: GeneralSchauderBasis.expansion
-- 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 : GeneralSchauderBasis β 𝕜 X L
A : Finset β
a : (↑(b.proj A) : X →ₗ[𝕜] X).range ≤ Submodule.span 𝕜 ((↑b : β → X) '' (↑A : Set β))
a₁ : Submodule.span 𝕜 ((↑b : β → X) '' (↑A : Set β)) ≤ (↑(b.proj A) : X →ₗ[𝕜] X).range
⊢ (↑(b.proj A) : X →ₗ[𝕜] X).range = Submodule.span 𝕜 ((↑b : β → X) '' (↑A : Set β))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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 : GeneralSchauderBasis β 𝕜 X L
A : Finset β
x : X
a :
  Membership.mem (γ := Submodule 𝕜 X) (Submodule.span 𝕜 ((↑b : β → X) '' (↑A : Set β)))
    (∑ i ∈ A, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
⊢ Membership.mem (α := X) (γ := Submodule 𝕜 X) (Submodule.span 𝕜 ((↑b : β → X) '' (↑A : Set β)))
    (((↑(b.proj A) : X →ₗ[𝕜] X) : (a : X) → X) x : X)

Tactic:
rw [ContinuousLinearMap.coe_coe, proj_apply]

Premises used: GeneralSchauderBasis.proj_apply, ContinuousLinearMap.coe_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 : GeneralSchauderBasis β 𝕜 X L
A : Finset β
x : X
⊢ Membership.mem (γ := Submodule 𝕜 X) (Submodule.span 𝕜 ((↑b : β → X) '' (↑A : Set β)))
    (∑ i ∈ A, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))

Tactic:
Submodule.sum_mem _ fun i hi ↦
      Submodule.smul_mem _ _ (Submodule.subset_span ⟨i, hi, rfl⟩)

Premises used: Submodule.sum_mem, SetLike.coe, And.intro, Exists.intro, Submodule.span, GeneralSchauderBasis.basis, Set.image, Submodule.subset_span, GeneralSchauderBasis.coord, DFunLike.coe, rfl, Submodule.smul_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
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A : Finset β
x : X
⊢ Membership.mem (γ := Submodule 𝕜 X) (Submodule.span 𝕜 ((↑b : β → X) '' (↑A : Set β)))
    (∑ i ∈ A, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))

Tactic:
exact Submodule.sum_mem _ fun i hi ↦
      Submodule.smul_mem _ _ (Submodule.subset_span ⟨i, hi, 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
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A : Finset β
a : (↑b : β → X) '' (↑A : Set β) ⊆ (↑(↑(b.proj A) : X →ₗ[𝕜] X).range : Set X)
⊢ Submodule.span 𝕜 ((↑b : β → X) '' (↑A : Set β)) ≤ (↑(b.proj A) : X →ₗ[𝕜] X).range

Tactic:
rw [Submodule.span_le]

Premises used: Submodule.span_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
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A : Finset β
i : β
hi : i ∈ (↑A : Set β)
h : ((↑(b.proj A) : X →ₗ[𝕜] X) : (a : X) → X) ((↑b : β → X) i) = (↑b : β → X) i
⊢ (↑b : β → X) i ∈ (↑(↑(b.proj A) : X →ₗ[𝕜] X).range : Set X)

Tactic:
use b i

Premises used: GeneralSchauderBasis.basis
-- 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 : GeneralSchauderBasis β 𝕜 X L
A : Finset β
i : β
hi : i ∈ (↑A : Set β)
h : (b.proj A : (a : X) → X) ((↑b : β → X) i) = (↑b : β → X) i
h₁ : (if i ∈ A then (↑b : β → X) i else 0) = (↑b : β → X) i
h₂ h₃ : (↑b : β → X) i = (↑b : β → X) i
⊢ ((↑(b.proj A) : X →ₗ[𝕜] X) : (a : X) → X) ((↑b : β → X) i) = (↑b : β → X) i

Tactic:
rw [ContinuousLinearMap.coe_coe, proj_apply_basis_mem, if_pos (Finset.mem_coe.mp hi)]

Premises used: GeneralSchauderBasis.proj_apply_basis_mem, ContinuousLinearMap.coe_coe, if_pos, Iff.mp, Finset.mem_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 : GeneralSchauderBasis β 𝕜 X L
A B : Finset β
x : X
simp :
  Eq.{u_2 + 1} (α := X)
    (∑ i ∈ B ∩ A, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
    (∑ i ∈ A ∩ B, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
⊢ Eq (α := X) ((b.proj A : (a : X) → X) ((b.proj B : (a : X) → X) x : X) : X) ((b.proj (A ∩ B) : (a : X) → X) x : X)

Tactic:
simp only [proj_apply, map_sum, map_smul, b.ortho, Pi.single_apply, ite_smul, one_smul, zero_smul,
    Finset.sum_ite_eq', smul_ite, smul_zero, Finset.sum_ite_mem]

Premises used: Finset.sum_ite_mem, GeneralSchauderBasis.proj_apply, Finset.sum_ite_eq', Pi.single_apply, smul_zero, map_sum, one_smul, smul_ite, zero_smul, GeneralSchauderBasis.ortho, ite_smul, map_smul
-- 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 : GeneralSchauderBasis β 𝕜 X L
A B : Finset β
x : X
e_s : B ∩ A = A ∩ B
⊢ Eq.{u_2 + 1} (α := X)
    (∑ i ∈ B ∩ A, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
    (∑ i ∈ A ∩ B, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))

Tactic:
congr 1
-- 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 : GeneralSchauderBasis β 𝕜 X L
A B : Finset β
x : X
e_s : ∀ (a : β), a ∈ B ∩ A ↔ a ∈ A ∩ B
⊢ B ∩ A = A ∩ B

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
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A B : Finset β
x : X
a : β
⊢ a ∈ B ∩ A ↔ a ∈ A ∩ B

Tactic:
simp [and_comm]

Premises used: and_comm
-- 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 : GeneralSchauderBasis β 𝕜 X L
A : Finset β
rw : Fintype.card.{u_3} (↑(↑A : Set β) : Type u_3) = A.card
rw₁ : LinearIndependent.{u_3, u_1, u_2} 𝕜 (M := X) fun (x : (↑(↑A : Set β) : Type u_3)) ↦ (↑b : β → X) (↑x : β)
⊢ Module.finrank.{u_1, u_2} 𝕜 ↥(↑(b.proj A) : X →ₗ[𝕜] X).range = A.card

Tactic:
rw [range_proj_eq_span, Set.image_eq_range, finrank_span_eq_card]

Premises used: Set.image_eq_range, finrank_span_eq_card, 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
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A : Finset β
⊢ Fintype.card.{u_3} (↑(↑A : Set β) : Type u_3) = A.card

Tactic:
Fintype.card_coe A

Premises used: Fintype.card_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 : GeneralSchauderBasis β 𝕜 X L
A : Finset β
⊢ Fintype.card.{u_3} (↑(↑A : Set β) : Type u_3) = A.card

Tactic:
exact Fintype.card_coe A

Premises used: Fintype.card_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 : GeneralSchauderBasis β 𝕜 X L
A : Finset β
⊢ LinearIndependent.{u_3, u_1, u_2} 𝕜 (M := X) fun (x : (↑(↑A : Set β) : Type u_3)) ↦ (↑b : β → X) (↑x : β)

Tactic:
b.linearIndependent.comp (fun i : A ↦ i.val) Subtype.val_injective

Premises used: Subtype.val_injective, Subtype.val, LinearIndependent.comp, GeneralSchauderBasis.linearIndependent
-- 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 : GeneralSchauderBasis β 𝕜 X L
A : Finset β
⊢ LinearIndependent.{u_3, u_1, u_2} 𝕜 (M := X) fun (x : (↑(↑A : Set β) : Type u_3)) ↦ (↑b : β → X) (↑x : β)

Tactic:
exact b.linearIndependent.comp (fun i : A ↦ i.val) Subtype.val_injective

Premises used: Subtype.val_injective, Subtype.val, LinearIndependent.comp, GeneralSchauderBasis.linearIndependent
-- 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
A : Finset β
⊢ ‖GeneralSchauderBasis.proj b A‖ₑ ≤ b.enormProjBound

Tactic:
le_iSup (fun A ↦ ‖b.proj A‖ₑ) A

Premises used: le_iSup, UnconditionalSchauderBasis.enormProjBound, ENorm.enorm, GeneralSchauderBasis.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
h : ∀ (x : X), ∃ (C : ℝ), ∀ (i : Finset β), norm (E := X) ((GeneralSchauderBasis.proj b i : (a : X) → X) x : X) ≤ C
⊢ ∃ (C : ℝ), ∀ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ ≤ C

Tactic:
apply banach_steinhaus

Premises used: banach_steinhaus
-- 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
h :
  ∀ (A₀ : Finset β)
    (hA₀ :
      ∀ (t : Finset β),
        Disjoint t A₀ →
          norm.{u_2} (E := X)
              (∑ i ∈ t, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i)) <
            1),
    ∃ (C : ℝ), ∀ (i : Finset β), norm (E := X) ((GeneralSchauderBasis.proj b i : (a : X) → X) x : X) ≤ C
⊢ ∃ (C : ℝ), ∀ (i : Finset β), norm (E := X) ((GeneralSchauderBasis.proj b i : (a : X) → X) x : X) ≤ C

Tactic:
obtain ⟨A₀, hA₀⟩ := summable_iff_vanishing_norm.mp (b.expansion x).summable 1 zero_lt_one

Premises used: GeneralSchauderBasis.expansion, summable_iff_vanishing_norm, HasSum.summable, zero_lt_one, Iff.mp, OfNat.ofNat
-- 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
h :
  ∀ (i : Finset β),
    norm (E := X) ((GeneralSchauderBasis.proj b i : (a : X) → X) x : X) ≤
      HAdd.hAdd (α := ℝ)
        (Finset.sup'
          (Finset.image (fun (B : Finset β) ↦ norm (E := X) ((GeneralSchauderBasis.proj b B : (a : X) → X) x : X))
            A₀.powerset)
          ⋯ _root_.id)
        1
⊢ ∃ (C : ℝ), ∀ (i : Finset β), norm (E := X) ((GeneralSchauderBasis.proj b i : (a : X) → X) x : X) ≤ C

Tactic:
use (A₀.powerset.image fun B ↦ ‖b.proj B x‖).sup' ((Finset.powerset_nonempty A₀).image _) id + 1

Premises used: Norm.norm, Finset.Nonempty.image, id, Finset.powerset_nonempty, GeneralSchauderBasis.proj, Finset.powerset, Finset.sup', DFunLike.coe, Finset.image
-- 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 β
simp :
  ∑ i ∈ A, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i) =
    HAdd.hAdd (α := X)
      (∑ i ∈ A ∩ A₀, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
      (∑ i ∈ A \ A₀, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
⊢ (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:
simp only [GeneralSchauderBasis.proj_apply]

Premises used: GeneralSchauderBasis.proj_apply