awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hcomp :
  ∀ (n m : ℕ) (x : X),
    Eq (α := X) ((P n : (a : X) → X) ((P m : (a : X) → X) x : X) : X) ((P (min n m) : (a : X) → X) x : X)
i j : ℕ
x : X
h : ¬i = j
neg :
  ∀ (h' : i < j),
    HSub.hSub (α := X) (β := X) ((P (min i j + 1) : (a : X) → X) x : X) ((P (min i (j + 1)) : (a : X) → X) x : X) -
        HSub.hSub (α := X) (β := X) ((P (min (i + 1) j) : (a : X) → X) x : X) ((P (min i j) : (a : X) → X) x : X) =
      0
⊢ HSub.hSub (α := X) (β := X) ((P (min i j + 1) : (a : X) → X) x : X) ((P (min i (j + 1)) : (a : X) → X) x : X) -
      HSub.hSub (α := X) (β := X) ((P (min (i + 1) j) : (a : X) → X) x : X) ((P (min i j) : (a : X) → X) x : X) =
    0
have neg₁ : ∀ (h' : i > j),
  HSub.hSub (α := X) (β := X) ((P (min i j + 1) : (a : X) → X) x : X) ((P (min i (j + 1)) : (a : X) → X) x : X) -
      HSub.hSub (α := X) (β := X) ((P (min (i + 1) j) : (a : X) → X) x : X) ((P (min i j) : (a : X) → X) x : X) =
    0
Tactic: rcases Nat.lt_or_gt_of_ne h with h' | h'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hcomp :
  ∀ (n m : ℕ) (x : X),
    Eq (α := X) ((P n : (a : X) → X) ((P m : (a : X) → X) x : X) : X) ((P (min n m) : (a : X) → X) x : X)
i j : ℕ
x : X
h : ¬i = j
h' : i < j
⊢ HSub.hSub (α := X) (β := X) ((P (min i j + 1) : (a : X) → X) x : X) ((P (min i (j + 1)) : (a : X) → X) x : X) -
      HSub.hSub (α := X) (β := X) ((P (min (i + 1) j) : (a : X) → X) x : X) ((P (min i j) : (a : X) → X) x : X) =
    0
have neg : HSub.hSub (α := X) (β := X) ((P (i + 1) : (a : X) → X) x : X) ((P i : (a : X) → X) x : X) -
    HSub.hSub (α := X) (β := X) ((P i.succ : (a : X) → X) x : X) ((P i : (a : X) → X) x : X) =
  0
Tactic: rw [min_eq_left_of_lt h', min_eq_left (Nat.succ_le_of_lt h'),
        min_eq_left_of_lt (Nat.lt_succ_of_lt h')]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hcomp :
  ∀ (n m : ℕ) (x : X),
    Eq (α := X) ((P n : (a : X) → X) ((P m : (a : X) → X) x : X) : X) ((P (min n m) : (a : X) → X) x : X)
i j : ℕ
x : X
h : ¬i = j
h' : i > j
⊢ HSub.hSub (α := X) (β := X) ((P (min i j + 1) : (a : X) → X) x : X) ((P (min i (j + 1)) : (a : X) → X) x : X) -
      HSub.hSub (α := X) (β := X) ((P (min (i + 1) j) : (a : X) → X) x : X) ((P (min i j) : (a : X) → X) x : X) =
    0
have neg : HSub.hSub (α := X) (β := X) ((P (j + 1) : (a : X) → X) x : X) ((P j.succ : (a : X) → X) x : X) -
    HSub.hSub (α := X) (β := X) ((P j : (a : X) → X) x : X) ((P j : (a : X) → X) x : X) =
  0
Tactic: rw [min_eq_right_of_lt h', min_eq_right (Nat.succ_le_of_lt h'),
        min_eq_right_of_lt (Nat.lt_succ_of_lt h')]
-- 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
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
⊢ Module.finrank.{u_1, u_2} 𝕜 ↥(↑(succSub P n) : X →ₗ[𝕜] X).range = 1
have hV : V ≤ W
Tactic: have hV : V ≤ W := by
    rintro _ ⟨y, rfl⟩
    exact ⟨P n y, by simp [ContinuousLinearMap.coe_coe, hcomp]⟩
-- 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
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
⊢ Module.finrank.{u_1, u_2} 𝕜 ↥(↑(succSub P n) : X →ₗ[𝕜] X).range = 1
have hUW : U ≤ W
Tactic: have hUW : U ≤ W := by
    rintro _ ⟨y, rfl⟩
    exact Submodule.sub_mem W ⟨y, rfl⟩ (hV ⟨y, rfl⟩)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
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
have a : W ≤ U ⊔ V
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
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
a : W ≤ U ⊔ V
⊢ W = U ⊔ V
have a₁ : U ⊔ V ≤ W
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
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
x y : X
hy : ((↑(P (n + 1)) : X →ₗ[𝕜] X) : (a : X) → X) y = x
⊢ x ∈ U ⊔ V
have a : HAdd.hAdd (β := X) (HSub.hSub (α := X) (β := X) ((P (n + 1) : (a : X) → X) y : X) ((P n : (a : X) → X) y : X))
    ((P n : (a : X) → X) y : X) ∈
  U ⊔ V
Tactic: rw [← hy, ContinuousLinearMap.coe_coe, ← sub_add_cancel ((P (n + 1)) y) ((P n) y)]
-- 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
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
⊢ Module.finrank.{u_1, u_2} 𝕜 ↥(↑(succSub P n) : X →ₗ[𝕜] X).range = 1
have hW : 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
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
⊢ x = (P n : (a : X) → X) x
have 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)
Tactic: rw [← hz, ContinuousLinearMap.coe_coe, hcomp, min_self]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
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)
⊢ x = (P n : (a : X) → X) x
have rw₁ : Eq (α := X) ((P n : (a : X) → X) z : X) ((P n : (a : X) → X) ((P n : (a : X) → X) z : X) : X)
Tactic: rw [← hz, ContinuousLinearMap.coe_coe, hcomp, min_self]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
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)
⊢ x = (P n : (a : X) → X) x
have rw₂ : Eq (α := X) ((P n : (a : X) → X) z : X) ((P (min n n) : (a : X) → X) z : X)
Tactic: rw [← hz, ContinuousLinearMap.coe_coe, hcomp, min_self]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
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)
⊢ x = (P n : (a : X) → X) x
have rw₃ : Eq (α := X) ((P n : (a : X) → X) z : X) ((P n : (a : X) → X) z : X)
Tactic: rw [← hz, ContinuousLinearMap.coe_coe, hcomp, min_self]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
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) x : X) (0 : X)
have rw : Eq (α := X) ((P n : (a : X) → X) ((succSub P n : (a : X) → X) y : X) : X) (0 : X)
Tactic: rw [← hy, ContinuousLinearMap.coe_coe]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
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
⊢ x = 0
have calc : x = (P n : (a : X) → X) x
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
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
⊢ x = 0
have calc₁ : Eq (α := X) ((P n : (a : X) → X) x : X) (0 : X)
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]
-- 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
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
⊢ Module.finrank.{u_1, u_2} 𝕜 ↥(↑(succSub P n) : X →ₗ[𝕜] X).range = 1
have hdisj : 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
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 < Module.finrank.{u_1, u_2} 𝕜 ↥W
have rw : 0 < n + 1
Tactic: rw [hrank]
-- 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
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 = ⊥
⊢ Module.finrank.{u_1, u_2} 𝕜 ↥(↑(succSub P n) : X →ₗ[𝕜] X).range = 1
have this : FiniteDimensional.{u_1, u_2} 𝕜 ↥W
Tactic: have : FiniteDimensional 𝕜 W := .of_finrank_pos (by rw [hrank]; exact Nat.succ_pos n)
-- 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
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
⊢ Module.finrank.{u_1, u_2} 𝕜 ↥(↑(succSub P n) : X →ₗ[𝕜] X).range = 1
have this₁ : FiniteDimensional.{u_1, u_2} 𝕜 ↥U
Tactic: have : FiniteDimensional 𝕜 U := Submodule.finiteDimensional_of_le hUW
-- 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
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
⊢ Module.finrank.{u_1, u_2} 𝕜 ↥(↑(succSub P n) : X →ₗ[𝕜] X).range = 1
have this₁ : FiniteDimensional.{u_1, u_2} 𝕜 ↥V
Tactic: have : FiniteDimensional 𝕜 V := Submodule.finiteDimensional_of_le hV
-- 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
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} 𝕜 ↥(↑(succSub P n) : X →ₗ[𝕜] X).range = 1
have 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
Tactic: have h_dim := Submodule.finrank_sup_add_finrank_inf_eq U V
-- 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
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
⊢ Module.finrank.{u_1, u_2} 𝕜 ↥(↑(succSub P n) : X →ₗ[𝕜] X).range = 1
have h_dim₁ : 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
Cleared hypotheses: h_dim
-- 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)
⊢ ∃ (c : 𝕜), c • D.e n = (succSub D.P n : (a : X) → X) x
have hrank : 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
-- 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
⊢ ∃ (c : 𝕜), c • D.e n = (succSub D.P n : (a : X) → X) x
have this : FiniteDimensional.{u_1, u_2} 𝕜 ↥S.range
Tactic: have : FiniteDimensional 𝕜 S.range := .of_finrank_pos (hrank.symm ▸ zero_lt_one)
-- 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
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
have hle : 𝕜 ∙ D.e n ≤ S.range
Tactic: apply Submodule.eq_of_le_of_finrank_eq
-- 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
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
⊢ 𝕜 ∙ D.e n = S.range
have hd : Module.finrank.{u_1, u_2} 𝕜 ↥(𝕜 ∙ D.e n) = Module.finrank.{u_1, u_2} 𝕜 ↥S.range
Tactic: apply Submodule.eq_of_le_of_finrank_eq