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
b : SchauderBasis 𝕜 X
inst_3 : CompleteSpace X
x : X
h :
  ∀ (M : ℝ)
    (hM :
      ∀ (x_1 : X), Membership.mem (γ := Set X) (Set.range fun (n : ℕ) ↦ (b.proj n : (a : X) → X) x) x_1 → ‖x_1‖ ≤ M),
    ∃ (C : ℝ), ∀ (i : ℕ), norm (E := X) ((b.proj i : (a : X) → X) x : X) ≤ C
⊢ ∃ (C : ℝ), ∀ (i : ℕ), norm (E := X) ((b.proj i : (a : X) → X) x : X) ≤ C

Tactic:
obtain ⟨M, hM⟩ := isBounded_iff_forall_norm_le.mp
    (Metric.isBounded_range_of_tendsto (fun n ↦ b.proj n x) (tendsto_proj b x))

Premises used: SchauderBasis.tendsto_proj, Metric.isBounded_range_of_tendsto, SchauderBasis.proj, isBounded_iff_forall_norm_le, Iff.mp, 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
b : SchauderBasis 𝕜 X
inst_3 : CompleteSpace X
x : X
M : ℝ
hM : ∀ (x_1 : X), Membership.mem (γ := Set X) (Set.range fun (n : ℕ) ↦ (b.proj n : (a : X) → X) x) x_1 → ‖x_1‖ ≤ M
⊢ ∃ (C : ℝ), ∀ (i : ℕ), norm (E := X) ((b.proj i : (a : X) → X) x : X) ≤ C

Tactic:
⟨M, Set.forall_mem_range.mp hM⟩

Premises used: Set.forall_mem_range, Exists.intro, 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
b : SchauderBasis 𝕜 X
inst_3 : CompleteSpace X
x : X
M : ℝ
hM : ∀ (x_1 : X), Membership.mem (γ := Set X) (Set.range fun (n : ℕ) ↦ (b.proj n : (a : X) → X) x) x_1 → ‖x_1‖ ≤ M
⊢ ∃ (C : ℝ), ∀ (i : ℕ), norm (E := X) ((b.proj i : (a : X) → X) x : X) ≤ C

Tactic:
exact ⟨M, Set.forall_mem_range.mp hM⟩
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
n : ℕ
⊢ ‖b.proj n‖ₑ ≤ b.enormProjBound

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

Premises used: SchauderBasis.enormProjBound, SchauderBasis.proj, le_iSup, ENorm.enorm
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
inst_3 : CompleteSpace X
obtain : ∀ (C : ℝ) (hC : ∀ (n : ℕ), ‖b.proj n‖ ≤ C), BddAbove (α := ℝ≥0) (Set.range fun (n : ℕ) ↦ ‖b.proj n‖₊)
⊢ BddAbove (α := ℝ≥0) (Set.range fun (n : ℕ) ↦ ‖b.proj n‖₊)

Tactic:
obtain ⟨C, hC⟩ := b.exists_norm_proj_le

Premises used: SchauderBasis.exists_norm_proj_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
b : SchauderBasis 𝕜 X
inst_3 : CompleteSpace X
C : ℝ
hC : ∀ (n : ℕ), ‖b.proj n‖ ≤ C
⊢ 0 ≤ C

Tactic:
simpa [proj_zero] using hC 0

Premises used: SchauderBasis.proj_zero, 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
b : SchauderBasis 𝕜 X
inst_3 : CompleteSpace X
C : ℝ
hC : ∀ (n : ℕ), ‖b.proj n‖ ≤ C
⊢ 0 ≤ C

Tactic:
have hCpos : 0 ≤ C := by simpa [proj_zero] using hC 0
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
inst_3 : CompleteSpace X
C : ℝ
hC : ∀ (n : ℕ), ‖b.proj n‖ ≤ C
hCpos : 0 ≤ C
⊢ BddAbove (α := ℝ≥0) (Set.range fun (n : ℕ) ↦ ‖b.proj n‖₊)

Tactic:
⟨C.toNNReal, ?_⟩

Premises used: BddAbove, Set.Nonempty, Exists.intro, Real.toNNReal
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
inst_3 : CompleteSpace X
C : ℝ
hC : ∀ (n : ℕ), ‖b.proj n‖ ≤ C
hCpos : 0 ≤ C
refine : Membership.mem (γ := Set ℝ≥0) (upperBounds (Set.range fun (n : ℕ) ↦ ‖b.proj n‖₊)) C.toNNReal
⊢ BddAbove (α := ℝ≥0) (Set.range fun (n : ℕ) ↦ ‖b.proj n‖₊)

Tactic:
refine ⟨C.toNNReal, ?_⟩
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
inst_3 : CompleteSpace X
C : ℝ
hC : ∀ (n : ℕ), ‖b.proj n‖ ≤ C
hCpos : 0 ≤ C
n : ℕ
rw : ‖b.proj n‖ ≤ C
⊢ (fun (n : ℕ) ↦ ‖b.proj n‖₊) n ≤ C.toNNReal

Tactic:
rw [← NNReal.coe_le_coe, Real.coe_toNNReal C hCpos, coe_nnnorm]

Premises used: Real.coe_toNNReal, coe_nnnorm, NNReal.coe_le_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
b : SchauderBasis 𝕜 X
inst_3 : CompleteSpace X
C : ℝ
hC : ∀ (n : ℕ), ‖b.proj n‖ ≤ C
hCpos : 0 ≤ C
n : ℕ
⊢ ‖b.proj n‖ ≤ C

Tactic:
hC 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
b : SchauderBasis 𝕜 X
inst_3 : CompleteSpace X
C : ℝ
hC : ∀ (n : ℕ), ‖b.proj n‖ ≤ C
hCpos : 0 ≤ C
n : ℕ
⊢ ‖b.proj n‖ ≤ C

Tactic:
exact hC 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
b : SchauderBasis 𝕜 X
inst_3 : CompleteSpace X
n : ℕ
⊢ ‖b.proj n‖₊ ≤ b.nnnormProjBound

Tactic:
le_ciSup (bddAbove_range_nnnorm_proj b) n

Premises used: SchauderBasis.bddAbove_range_nnnorm_proj, le_ciSup, SchauderBasis.nnnormProjBound
-- Module: Mathlib.Analysis.Normed.Module.Bases
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
inst_3 : CompleteSpace X
n : ℕ
⊢ ‖b.proj n‖ ≤ (↑b.nnnormProjBound : ℝ)

Tactic:
mod_cast b.nnnorm_proj_le_nnnormProjBound n

Premises used: Norm.norm, SchauderBasis.proj, cast, LE.le, SchauderBasis.nnnorm_proj_le_nnnormProjBound, Eq.refl, NNReal.toReal, SchauderBasis.nnnormProjBound
-- 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
h0 : P 0 = 0
⊢ ∑ i ∈ Finset.range 0, succSub P i = P 0

Tactic:
simp [h0]
-- 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
h0 : P 0 = 0
n : ℕ
ih : ∑ i ∈ Finset.range n, succSub P i = P n
succ : P n + (P (n + 1) - P n) = P (n + 1)
⊢ ∑ i ∈ Finset.range (n + 1), succSub P i = P (n + 1)

Tactic:
rw [Finset.sum_range_succ, ih, succSub]

Premises used: SchauderBasis.succSub, Finset.sum_range_succ
-- 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
h0 : P 0 = 0
n : ℕ
ih : ∑ i ∈ Finset.range n, succSub P i = P n
⊢ P n + (P (n + 1) - P n) = P (n + 1)

Tactic:
abel
-- 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
h0 : P 0 = 0
n : ℕ
zero : ∑ i ∈ Finset.range 0, succSub P i = P 0
succ : ∀ (n : ℕ) (ih : ∑ i ∈ Finset.range n, succSub P i = P n), ∑ i ∈ Finset.range (n + 1), succSub P i = P (n + 1)
⊢ ∑ i ∈ Finset.range n, succSub P i = P n

Tactic:
induction n with
  | zero => simp [h0]
  | succ n ih => rw [Finset.sum_range_succ, ih, succSub]; abel

Premises used: SchauderBasis.succSub, Finset.sum_range_succ
-- 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
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
simp :
  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) =
    if i = j then HSub.hSub (α := X) (β := X) ((P (j + 1) : (a : X) → X) x : X) ((P j : (a : X) → X) x : X) else 0
⊢ Eq (α := X) ((succSub P i : (a : X) → X) ((succSub P j : (a : X) → X) x : X) : X)
    (if i = j then (succSub P j : (a : X) → X) x else 0 : X)

Tactic:
simp only [succSub, ContinuousLinearMap.sub_apply, map_sub, hcomp,
    Nat.add_min_add_right]

Premises used: SchauderBasis.succSub, map_sub, Nat.add_min_add_right, ContinuousLinearMap.sub_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
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
pos :
  ∀ (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) =
      HSub.hSub (α := X) (β := X) ((P (j + 1) : (a : X) → X) x : X) ((P j : (a : X) → X) x : X)
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) =
    if i = j then HSub.hSub (α := X) (β := X) ((P (j + 1) : (a : X) → X) x : X) ((P j : (a : X) → X) x : X) else 0

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
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
pos :
  HSub.hSub (α := X) (β := X) ((P (j + 1) : (a : X) → X) x : X) ((P j : (a : X) → X) x : X) -
      HSub.hSub (α := X) (β := X) ((P j : (a : X) → X) x : X) ((P j : (a : X) → X) x : X) =
    HSub.hSub (α := X) (β := X) ((P (j + 1) : (a : X) → X) x : X) ((P j : (a : X) → X) x : X)
⊢ 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) =
    HSub.hSub (α := X) (β := X) ((P (j + 1) : (a : X) → X) x : X) ((P j : (a : X) → X) x : X)

Tactic:
rw [h, min_self, min_eq_right (Nat.le_succ j), Nat.min_eq_left (Nat.le_succ j)]

Premises used: min_self, Nat.le_succ, min_eq_right, Nat.min_eq_left
-- 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
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
⊢ HSub.hSub (α := X) (β := X) ((P (j + 1) : (a : X) → X) x : X) ((P j : (a : X) → X) x : X) -
      HSub.hSub (α := X) (β := X) ((P j : (a : X) → X) x : X) ((P j : (a : X) → X) x : X) =
    HSub.hSub (α := X) (β := X) ((P (j + 1) : (a : X) → X) x : X) ((P j : (a : X) → X) x : X)

Tactic:
abel
-- 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
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
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

Tactic:
rcases Nat.lt_or_gt_of_ne h with h' | h'

Premises used: Nat.lt_or_gt_of_ne
-- 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
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
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
⊢ 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:
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')]

Premises used: Nat.succ_le_of_lt, min_eq_left_of_lt, min_eq_left, Nat.lt_succ_of_lt
-- 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
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 (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:
abel
-- 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
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
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
⊢ 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:
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')]

Premises used: Nat.succ_le_of_lt, min_eq_right, min_eq_right_of_lt, Nat.lt_succ_of_lt
-- 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
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 (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:
abel
-- 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
y : X
⊢ Eq (α := X) (((↑(P (n + 1)) : X →ₗ[𝕜] X) : (a : X) → X) ((P n : (a : X) → X) y : X) : X)
    (((↑(P n) : X →ₗ[𝕜] X) : (a : X) → X) y : X)

Tactic:
simp [ContinuousLinearMap.coe_coe, hcomp]

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
y : X
⊢ Membership.mem (α := X) W (((↑(P n) : X →ₗ[𝕜] X) : (a : X) → X) y : X)

Tactic:
exact ⟨P n y, by simp [ContinuousLinearMap.coe_coe, 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
⊢ V ≤ W

Tactic:
have hV : V ≤ W := by
    rintro _ ⟨y, rfl⟩
    exact ⟨P n y, by simp [ContinuousLinearMap.coe_coe, 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
y : X
⊢ Membership.mem (α := X) W (((↑(succSub P n) : X →ₗ[𝕜] X) : (a : X) → X) y : X)

Tactic:
Submodule.sub_mem W ⟨y, rfl⟩ (hV ⟨y, rfl⟩)

Premises used: Set.Mem, Exists.intro, rfl, Submodule.sub_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
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
y : X
⊢ Membership.mem (α := X) W (((↑(succSub P n) : X →ₗ[𝕜] X) : (a : X) → X) y : X)

Tactic:
exact Submodule.sub_mem W ⟨y, rfl⟩ (hV ⟨y, rfl⟩)

Premises used: Exists.intro, rfl, Submodule.sub_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
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
⊢ U ≤ W

Tactic:
have hUW : U ≤ W := by
    rintro _ ⟨y, rfl⟩
    exact Submodule.sub_mem W ⟨y, rfl⟩ (hV ⟨y, 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
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
a₁ : U ⊔ V ≤ W
⊢ W = U ⊔ V

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
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
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
⊢ x ∈ U ⊔ V

Tactic:
rw [← hy, ContinuousLinearMap.coe_coe, ← sub_add_cancel ((P (n + 1)) y) ((P n) y)]

Premises used: ContinuousLinearMap.coe_coe, HAdd.hAdd, OfNat.ofNat, sub_add_cancel, 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
x y : X
hy : ((↑(P (n + 1)) : X →ₗ[𝕜] X) : (a : X) → X) y = x
⊢ 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:
Submodule.add_mem_sup ⟨y, rfl⟩ ⟨y, rfl⟩

Premises used: Set.Mem, Submodule.add_mem_sup, Exists.intro, 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
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
⊢ 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:
exact Submodule.add_mem_sup ⟨y, rfl⟩ ⟨y, rfl⟩