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
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank.{u_1, u_2} 𝕜 ↥(↑(P n) : X →ₗ[𝕜] X).range = n
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)
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n) : X →ₗ[𝕜] X).range
V : Submodule 𝕜 X := (↑(P n) : X →ₗ[𝕜] X).range
W : Submodule 𝕜 X := (↑(P (n + 1)) : X →ₗ[𝕜] X).range
hV : V ≤ W
hUW : U ≤ W
⊢ U ⊔ V ≤ W

Tactic:
sup_le hUW hV

Premises used: sup_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
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank.{u_1, u_2} 𝕜 ↥(↑(P n) : X →ₗ[𝕜] X).range = n
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)
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n) : X →ₗ[𝕜] X).range
V : Submodule 𝕜 X := (↑(P n) : X →ₗ[𝕜] X).range
W : Submodule 𝕜 X := (↑(P (n + 1)) : X →ₗ[𝕜] X).range
hV : V ≤ W
hUW : U ≤ W
⊢ U ⊔ V ≤ W

Tactic:
exact sup_le hUW hV

Premises used: sup_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
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank.{u_1, u_2} 𝕜 ↥(↑(P n) : X →ₗ[𝕜] X).range = n
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)
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n) : X →ₗ[𝕜] X).range
V : Submodule 𝕜 X := (↑(P n) : X →ₗ[𝕜] X).range
W : Submodule 𝕜 X := (↑(P (n + 1)) : X →ₗ[𝕜] X).range
hV : V ≤ W
hUW : U ≤ W
⊢ W = U ⊔ V

Tactic:
have hW : W = U ⊔ V := by
    apply le_antisymm
    · rintro x ⟨y, hy⟩
      rw [← hy, ContinuousLinearMap.coe_coe, ← sub_add_cancel ((P (n + 1)) y) ((P n) y)]
      exact Submodule.add_mem_sup ⟨y, rfl⟩ ⟨y, rfl⟩
    · exact sup_le hUW hV
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank.{u_1, u_2} 𝕜 ↥(↑(P n) : X →ₗ[𝕜] X).range = n
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)
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n) : X →ₗ[𝕜] X).range
V : Submodule 𝕜 X := (↑(P n) : X →ₗ[𝕜] X).range
W : Submodule 𝕜 X := (↑(P (n + 1)) : X →ₗ[𝕜] X).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
x : X
h : x ∈ U ⊓ V
y : X
hy : ((↑(succSub P n) : X →ₗ[𝕜] X) : (a : X) → X) y = x
z : X
hz : ((↑(P n) : X →ₗ[𝕜] X) : (a : X) → X) z = x
rw :
  Eq (α := X) (((↑(P n) : X →ₗ[𝕜] X) : (a : X) → X) z : X)
    ((P n : (a : X) → X) (((↑(P n) : X →ₗ[𝕜] X) : (a : X) → X) z : X) : X)
rw₁ : Eq (α := X) ((P n : (a : X) → X) z : X) ((P n : (a : X) → X) ((P n : (a : X) → X) z : X) : X)
rw₂ : Eq (α := X) ((P n : (a : X) → X) z : X) ((P (min n n) : (a : X) → X) z : X)
rw₃ rw₄ : Eq (α := X) ((P n : (a : X) → X) z : X) ((P n : (a : X) → X) z : X)
⊢ x = (P n : (a : X) → X) x

Tactic:
rw [← hz, ContinuousLinearMap.coe_coe, hcomp, min_self]

Premises used: min_self, 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
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank.{u_1, u_2} 𝕜 ↥(↑(P n) : X →ₗ[𝕜] X).range = n
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)
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n) : X →ₗ[𝕜] X).range
V : Submodule 𝕜 X := (↑(P n) : X →ₗ[𝕜] X).range
W : Submodule 𝕜 X := (↑(P (n + 1)) : X →ₗ[𝕜] X).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
x : X
h : x ∈ U ⊓ V
y : X
hy : ((↑(succSub P n) : X →ₗ[𝕜] X) : (a : X) → X) y = x
z : X
hz : ((↑(P n) : X →ₗ[𝕜] X) : (a : X) → X) z = x
rw : Eq (α := X) ((P n : (a : X) → X) ((succSub P n : (a : X) → X) y : X) : X) (0 : X)
⊢ Eq (α := X) ((P n : (a : X) → X) x : X) (0 : X)

Tactic:
rw [← hy, ContinuousLinearMap.coe_coe]

Premises used: 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
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank.{u_1, u_2} 𝕜 ↥(↑(P n) : X →ₗ[𝕜] X).range = n
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)
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n) : X →ₗ[𝕜] X).range
V : Submodule 𝕜 X := (↑(P n) : X →ₗ[𝕜] X).range
W : Submodule 𝕜 X := (↑(P (n + 1)) : X →ₗ[𝕜] X).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
x : X
h : x ∈ U ⊓ V
y : X
hy : ((↑(succSub P n) : X →ₗ[𝕜] X) : (a : X) → X) y = x
z : X
hz : ((↑(P n) : X →ₗ[𝕜] X) : (a : X) → X) z = x
⊢ Eq (α := X) ((P n : (a : X) → X) ((succSub P n : (a : X) → X) y : X) : X) (0 : X)

Tactic:
simp [succSub, map_sub, hcomp]

Premises used: SchauderBasis.succSub, map_sub
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank.{u_1, u_2} 𝕜 ↥(↑(P n) : X →ₗ[𝕜] X).range = n
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)
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n) : X →ₗ[𝕜] X).range
V : Submodule 𝕜 X := (↑(P n) : X →ₗ[𝕜] X).range
W : Submodule 𝕜 X := (↑(P (n + 1)) : X →ₗ[𝕜] X).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
x : X
h : x ∈ U ⊓ V
y : X
hy : ((↑(succSub P n) : X →ₗ[𝕜] X) : (a : X) → X) y = x
z : X
hz : ((↑(P n) : X →ₗ[𝕜] X) : (a : X) → X) z = x
calc : x = (P n : (a : X) → X) x
calc₁ : Eq (α := X) ((P n : (a : X) → X) x : X) (0 : X)
⊢ x = 0

Tactic:
calc x = (P n) x := by rw [← hz, ContinuousLinearMap.coe_coe, hcomp, min_self]
         _ = 0       := by rw [← hy, ContinuousLinearMap.coe_coe]; simp [succSub, map_sub, hcomp]

Premises used: 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
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank.{u_1, u_2} 𝕜 ↥(↑(P n) : X →ₗ[𝕜] X).range = n
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)
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n) : X →ₗ[𝕜] X).range
V : Submodule 𝕜 X := (↑(P n) : X →ₗ[𝕜] X).range
W : Submodule 𝕜 X := (↑(P (n + 1)) : X →ₗ[𝕜] X).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
⊢ U ⊓ V = ⊥

Tactic:
have hdisj : U ⊓ V = ⊥ := eq_bot_iff.mpr fun x ⟨⟨y, hy⟩, ⟨z, hz⟩⟩ ↦ by
    simp only [Submodule.mem_bot]
    calc x = (P n) x := by rw [← hz, ContinuousLinearMap.coe_coe, hcomp, min_self]
         _ = 0       := by rw [← hy, ContinuousLinearMap.coe_coe]; simp [succSub, map_sub, hcomp]
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank.{u_1, u_2} 𝕜 ↥(↑(P n) : X →ₗ[𝕜] X).range = n
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)
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n) : X →ₗ[𝕜] X).range
V : Submodule 𝕜 X := (↑(P n) : X →ₗ[𝕜] X).range
W : Submodule 𝕜 X := (↑(P (n + 1)) : X →ₗ[𝕜] X).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
hdisj : U ⊓ V = ⊥
rw : 0 < n + 1
⊢ 0 < Module.finrank.{u_1, u_2} 𝕜 ↥W

Tactic:
rw [hrank]
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank.{u_1, u_2} 𝕜 ↥(↑(P n) : X →ₗ[𝕜] X).range = n
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)
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n) : X →ₗ[𝕜] X).range
V : Submodule 𝕜 X := (↑(P n) : X →ₗ[𝕜] X).range
W : Submodule 𝕜 X := (↑(P (n + 1)) : X →ₗ[𝕜] X).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
hdisj : U ⊓ V = ⊥
⊢ 0 < n + 1

Tactic:
Nat.succ_pos n

Premises used: Nat.succ_pos
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank.{u_1, u_2} 𝕜 ↥(↑(P n) : X →ₗ[𝕜] X).range = n
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)
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n) : X →ₗ[𝕜] X).range
V : Submodule 𝕜 X := (↑(P n) : X →ₗ[𝕜] X).range
W : Submodule 𝕜 X := (↑(P (n + 1)) : X →ₗ[𝕜] X).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
hdisj : U ⊓ V = ⊥
⊢ 0 < n + 1

Tactic:
exact Nat.succ_pos n

Premises used: Nat.succ_pos
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank.{u_1, u_2} 𝕜 ↥(↑(P n) : X →ₗ[𝕜] X).range = n
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)
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n) : X →ₗ[𝕜] X).range
V : Submodule 𝕜 X := (↑(P n) : X →ₗ[𝕜] X).range
W : Submodule 𝕜 X := (↑(P (n + 1)) : X →ₗ[𝕜] X).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
hdisj : U ⊓ V = ⊥
⊢ FiniteDimensional.{u_1, u_2} 𝕜 ↥W

Tactic:
have : FiniteDimensional 𝕜 W := .of_finrank_pos (by rw [hrank]; exact Nat.succ_pos 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
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank.{u_1, u_2} 𝕜 ↥(↑(P n) : X →ₗ[𝕜] X).range = n
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)
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n) : X →ₗ[𝕜] X).range
V : Submodule 𝕜 X := (↑(P n) : X →ₗ[𝕜] X).range
W : Submodule 𝕜 X := (↑(P (n + 1)) : X →ₗ[𝕜] X).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
hdisj : U ⊓ V = ⊥
this : FiniteDimensional.{u_1, u_2} 𝕜 ↥W
⊢ FiniteDimensional.{u_1, u_2} 𝕜 ↥U

Tactic:
have : FiniteDimensional 𝕜 U := Submodule.finiteDimensional_of_le hUW
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank.{u_1, u_2} 𝕜 ↥(↑(P n) : X →ₗ[𝕜] X).range = n
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)
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n) : X →ₗ[𝕜] X).range
V : Submodule 𝕜 X := (↑(P n) : X →ₗ[𝕜] X).range
W : Submodule 𝕜 X := (↑(P (n + 1)) : X →ₗ[𝕜] X).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
hdisj : U ⊓ V = ⊥
this_1 : FiniteDimensional.{u_1, u_2} 𝕜 ↥W
this : FiniteDimensional.{u_1, u_2} 𝕜 ↥U
⊢ FiniteDimensional.{u_1, u_2} 𝕜 ↥V

Tactic:
have : FiniteDimensional 𝕜 V := Submodule.finiteDimensional_of_le hV
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank.{u_1, u_2} 𝕜 ↥(↑(P n) : X →ₗ[𝕜] X).range = n
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)
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n) : X →ₗ[𝕜] X).range
V : Submodule 𝕜 X := (↑(P n) : X →ₗ[𝕜] X).range
W : Submodule 𝕜 X := (↑(P (n + 1)) : X →ₗ[𝕜] X).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
hdisj : U ⊓ V = ⊥
this_1 : FiniteDimensional.{u_1, u_2} 𝕜 ↥W
this_2 : FiniteDimensional.{u_1, u_2} 𝕜 ↥U
this : FiniteDimensional.{u_1, u_2} 𝕜 ↥V
⊢ Module.finrank.{u_1, u_2} 𝕜 ↥(U ⊔ V) + Module.finrank.{u_1, u_2} 𝕜 ↥(U ⊓ V) =
    Module.finrank.{u_1, u_2} 𝕜 ↥U + Module.finrank.{u_1, u_2} 𝕜 ↥V

Tactic:
have h_dim := Submodule.finrank_sup_add_finrank_inf_eq U V
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank.{u_1, u_2} 𝕜 ↥(↑(P n) : X →ₗ[𝕜] X).range = n
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)
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n) : X →ₗ[𝕜] X).range
V : Submodule 𝕜 X := (↑(P n) : X →ₗ[𝕜] X).range
W : Submodule 𝕜 X := (↑(P (n + 1)) : X →ₗ[𝕜] X).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
hdisj : U ⊓ V = ⊥
this_1 : FiniteDimensional.{u_1, u_2} 𝕜 ↥W
this_2 : FiniteDimensional.{u_1, u_2} 𝕜 ↥U
this : FiniteDimensional.{u_1, u_2} 𝕜 ↥V
h_dim :
  Module.finrank.{u_1, u_2} 𝕜 ↥(U ⊔ V) + Module.finrank.{u_1, u_2} 𝕜 ↥(U ⊓ V) =
    Module.finrank.{u_1, u_2} 𝕜 ↥U + Module.finrank.{u_1, u_2} 𝕜 ↥V
⊢ 1 + n = Module.finrank.{u_1, u_2} 𝕜 ↥U + n

Tactic:
rw [hdisj, finrank_bot, add_zero, ← hW, hrank, hrank, Nat.add_comm] at h_dim

Premises used: finrank_bot, add_zero, Nat.add_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
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank.{u_1, u_2} 𝕜 ↥(↑(P n) : X →ₗ[𝕜] X).range = n
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)
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n) : X →ₗ[𝕜] X).range
V : Submodule 𝕜 X := (↑(P n) : X →ₗ[𝕜] X).range
W : Submodule 𝕜 X := (↑(P (n + 1)) : X →ₗ[𝕜] X).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
hdisj : U ⊓ V = ⊥
this_1 : FiniteDimensional.{u_1, u_2} 𝕜 ↥W
this_2 : FiniteDimensional.{u_1, u_2} 𝕜 ↥U
this : FiniteDimensional.{u_1, u_2} 𝕜 ↥V
h_dim : 1 + n = Module.finrank.{u_1, u_2} 𝕜 ↥U + n
⊢ Module.finrank.{u_1, u_2} 𝕜 ↥(↑(succSub P n) : X →ₗ[𝕜] X).range = 1

Tactic:
Nat.add_right_cancel h_dim.symm

Premises used: Nat.add_right_cancel, 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
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank.{u_1, u_2} 𝕜 ↥(↑(P n) : X →ₗ[𝕜] X).range = n
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)
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n) : X →ₗ[𝕜] X).range
V : Submodule 𝕜 X := (↑(P n) : X →ₗ[𝕜] X).range
W : Submodule 𝕜 X := (↑(P (n + 1)) : X →ₗ[𝕜] X).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
hdisj : U ⊓ V = ⊥
this_1 : FiniteDimensional.{u_1, u_2} 𝕜 ↥W
this_2 : FiniteDimensional.{u_1, u_2} 𝕜 ↥U
this : FiniteDimensional.{u_1, u_2} 𝕜 ↥V
h_dim : 1 + n = Module.finrank.{u_1, u_2} 𝕜 ↥U + n
⊢ Module.finrank.{u_1, u_2} 𝕜 ↥(↑(succSub P n) : X →ₗ[𝕜] X).range = 1

Tactic:
exact Nat.add_right_cancel h_dim.symm

Premises used: Nat.add_right_cancel, 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
D : RankOneDecomposition 𝕜 X
n : ℕ
x : X
S : X →ₗ[𝕜] X := (↑(succSub D.P n) : X →ₗ[𝕜] X)
⊢ Module.finrank.{u_1, u_2} 𝕜 ↥S.range = 1

Tactic:
have hrank : Module.finrank 𝕜 S.range = 1 :=
    finrank_range_succSub_eq_one D.finrank_range D.proj_comp 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
S : X →ₗ[𝕜] X := (↑(succSub D.P n) : X →ₗ[𝕜] X)
hrank : Module.finrank.{u_1, u_2} 𝕜 ↥S.range = 1
⊢ FiniteDimensional.{u_1, u_2} 𝕜 ↥S.range

Tactic:
have : FiniteDimensional 𝕜 S.range := .of_finrank_pos (hrank.symm ▸ zero_lt_one)
-- 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
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
hle : 𝕜 ∙ D.e n ≤ S.range
hd : Module.finrank.{u_1, u_2} 𝕜 ↥(𝕜 ∙ D.e n) = Module.finrank.{u_1, u_2} 𝕜 ↥S.range
⊢ 𝕜 ∙ D.e n = S.range

Tactic:
apply Submodule.eq_of_le_of_finrank_eq

Premises used: Submodule.eq_of_le_of_finrank_eq
-- 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
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
⊢ 𝕜 ∙ D.e n ≤ S.range

Tactic:
(Submodule.span_singleton_le_iff_mem _ _).mpr (D.e_mem_range n)

Premises used: Iff.mpr, Set.Mem, Submodule.span_singleton_le_iff_mem, 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
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
⊢ 𝕜 ∙ D.e n ≤ S.range

Tactic:
exact (Submodule.span_singleton_le_iff_mem _ _).mpr (D.e_mem_range n)

Premises used: Iff.mpr, Submodule.span_singleton_le_iff_mem, 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
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
⊢ Module.finrank.{u_1, u_2} 𝕜 ↥(𝕜 ∙ D.e n) = Module.finrank.{u_1, u_2} 𝕜 ↥S.range

Tactic:
simp [hrank, finrank_span_singleton (D.e_ne_zero n)]

Premises used: SchauderBasis.RankOneDecomposition.e_ne_zero, finrank_span_singleton
-- 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
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
⊢ 𝕜 ∙ 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)]
-- 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
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
hspan : 𝕜 ∙ D.e n = S.range
⊢ ∃ (c : 𝕜), c • D.e n = (succSub D.P n : (a : X) → X) x

Tactic:
Submodule.mem_span_singleton.mp (hspan.symm ▸ LinearMap.mem_range_self S x)

Premises used: Submodule.mem_span_singleton, Eq.rec, LinearMap.mem_range_self, Iff.mp, 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
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
hspan : 𝕜 ∙ D.e n = S.range
⊢ ∃ (c : 𝕜), c • D.e n = (succSub D.P n : (a : X) → X) x

Tactic:
exact Submodule.mem_span_singleton.mp (hspan.symm ▸ LinearMap.mem_range_self S x)

Premises used: Submodule.mem_span_singleton, Iff.mp
-- 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
⊢ D.basisCoeff n x • D.e n = (succSub D.P n : (a : X) → X) x

Tactic:
Classical.choose_spec (exists_coeff D n x)

Premises used: Classical.choose_spec, SchauderBasis.RankOneDecomposition.exists_coeff, SchauderBasis.RankOneDecomposition.basisCoeff
-- 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 y : X
⊢ Eq.{u_2 + 1} (α := X) ((fun (x : 𝕜) ↦ x • D.e n) (coeff n (x + y)))
    ((fun (x : 𝕜) ↦ x • D.e n) (coeff n x + coeff n y))

Tactic:
simp only [add_smul, ← hcoeff, map_add]

Premises used: map_add, add_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 : 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
dsimp : coeff n (c • x) • D.e n = (c • coeff n x) • D.e n
⊢ 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)))

Tactic:
dsimp only [RingHom.id_apply]

Premises used: RingHom.id_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
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)
rw₄ 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)
⊢ 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]

Premises used: smul_smul, smul_eq_mul, 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 : 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 :
  norm.{u_1} (E := 𝕜) (({ toFun := coeff n, map_add' := ⋯, map_smul' := ⋯ : X →ₗ[𝕜] 𝕜 } : (a : X) → 𝕜) x : 𝕜) *
      ‖D.e n‖ ≤
    ‖succSub D.P n‖ * ‖x‖
⊢ norm.{u_1} (E := 𝕜) (({ toFun := coeff n, map_add' := ⋯, map_smul' := ⋯ : X →ₗ[𝕜] 𝕜 } : (a : X) → 𝕜) x : 𝕜) ≤
    ‖succSub D.P n‖ / ‖D.e n‖ * ‖x‖

Tactic:
rw [div_mul_eq_mul_div, le_div_iff₀ (norm_pos_iff.mpr (D.e_ne_zero n))]

Premises used: Iff.mpr, SchauderBasis.RankOneDecomposition.e_ne_zero, norm_pos_iff, div_mul_eq_mul_div, le_div_iff₀