awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramMatrix (hypothesis)
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Finite n
v : n → E
h_gram : (gram 𝕜 v).PosDef
this : Fintype n
y : n → 𝕜
hy : Eq.{u_1 + 1} (α := E) (∑ i : n, y i • v i) 0
⊢ ∀ (i : n), y i = 0
have this₁ : ∀ (hx : y ≠ 0), 0 < star y ⬝ᵥ gram 𝕜 v *ᵥ y
Tactic: have := h_gram.dotProduct_mulVec_pos (x := y)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramMatrix (goal)
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Finite n
v : n → E
h_li : LinearIndependent 𝕜 v
⊢ (gram 𝕜 v).PosDef
have have : ∀ (this : Fintype n), (gram 𝕜 v).PosDef
Tactic: have := Fintype.ofFinite n
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramMatrix (hypothesis)
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Finite n
v : n → E
h_li : LinearIndependent 𝕜 v
this : Fintype n
⊢ (gram 𝕜 v).PosDef
have h_li₁ : ∀ (g : n → 𝕜), Eq.{u_1 + 1} (α := E) (∑ i : n, g i • v i) 0 → ∀ (i : n), g i = 0
Tactic: rw [Fintype.linearIndependent_iff] at h_li
Cleared hypotheses: h_li
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramMatrix (goal)
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Finite n
v : n → E
this : Fintype n
h_li : ∀ (g : n → 𝕜), Eq.{u_1 + 1} (α := E) (∑ i : n, g i • v i) 0 → ∀ (i : n), g i = 0
⊢ (gram 𝕜 v).PosDef
have refine : ∀ (x : n → 𝕜) (hx : x ≠ 0), star x ⬝ᵥ gram 𝕜 v *ᵥ x ≠ 0
Tactic: refine .of_dotProduct_mulVec_pos (isHermitian_gram _ _) fun x hx ↦
    ((posSemidef_gram ..).dotProduct_mulVec_nonneg _).lt_of_ne' ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramMatrix (goal)
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Finite n
v : n → E
this : Fintype n
h_li : ∀ (g : n → 𝕜), Eq.{u_1 + 1} (α := E) (∑ i : n, g i • v i) 0 → ∀ (i : n), g i = 0
x : n → 𝕜
hx : x ≠ 0
⊢ star x ⬝ᵥ gram 𝕜 v *ᵥ x ≠ 0
have rw : Ne.{u_1 + 1} (α := E) (∑ i : n, x i • v i) 0
Tactic: rw [star_dotProduct_gram_mulVec, inner_self_eq_zero.ne]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramMatrix (goal)
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype n
inst_4 : DecidableEq n
v : n → E
⊢ (gram 𝕜 v).det ≠ 0 ↔ LinearIndependent 𝕜 v
have rw : (gram 𝕜 v).det ≠ 0 ↔ (gram 𝕜 v).PosDef
Tactic: rw [← posDef_gram_iff_linearIndependent, (posSemidef_gram 𝕜 v).posDef_iff_det_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramMatrix (goal)
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype n
inst_4 : DecidableEq n
v : n → E
rw : (gram 𝕜 v).det ≠ 0 ↔ (gram 𝕜 v).PosDef
⊢ (gram 𝕜 v).det ≠ 0 ↔ LinearIndependent 𝕜 v
have rw₁ : (gram 𝕜 v).det ≠ 0 ↔ (gram 𝕜 v).det ≠ 0
Tactic: rw [← posDef_gram_iff_linearIndependent, (posSemidef_gram 𝕜 v).posDef_iff_det_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramMatrix (goal)
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_5
inst_3 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
v : n → E
⊢ gram 𝕜 v =
    HMul.hMul (α := Matrix n ι 𝕜)
      ((of : (a : ι → n → 𝕜) → Matrix ι n 𝕜) fun (i : ι) (j : n) ↦
          WithLp.ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) (v j)) i)ᴴ
      ((of : (a : ι → n → 𝕜) → Matrix ι n 𝕜) fun (i : ι) (j : n) ↦
        WithLp.ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) (v j)) i)
have a : ∀ (i j : n),
  gram 𝕜 v i j =
    HMul.hMul (α := Matrix n ι 𝕜) (β := Matrix ι n 𝕜)
      ((of : (a : ι → n → 𝕜) → Matrix ι n 𝕜) fun (i : ι) (j : n) ↦
          WithLp.ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) (v j)) i)ᴴ
      ((of : (a : ι → n → 𝕜) → Matrix ι n 𝕜) fun (i : ι) (j : n) ↦
        WithLp.ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) (v j)) i)
      i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramMatrix (goal)
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
⊢ (HPow.hPow (β := ℕ) ‖f‖ 2 • gram 𝕜 v - gram.{u_5, u_2, u_4} (E := F) 𝕜 ((⇑f : (a : E) → F) ∘ v)).PosSemidef
have refine : ∀ (c : n →₀ 𝕜),
  LE.le (α := 𝕜) 0
    (c.sum fun (i : n) (xi : 𝕜) ↦
      c.sum fun (j : n) (xj : 𝕜) ↦
        star xi * (HPow.hPow (β := ℕ) ‖f‖ 2 • gram 𝕜 v - gram.{u_5, u_2, u_4} (E := F) 𝕜 ((⇑f : (a : E) → F) ∘ v)) i j *
          xj)
Tactic: refine ⟨(isHermitian_gram 𝕜 v).smul (((Pi.isSelfAdjoint.mpr (congrFun rfl)).apply f).pow 2)
    |>.sub (isHermitian_gram 𝕜 (f ∘ v)), fun c ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramMatrix (goal)
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
⊢ LE.le (α := 𝕜) 0
    (c.sum fun (i : n) (xi : 𝕜) ↦
      c.sum fun (j : n) (xj : 𝕜) ↦
        star xi * (HPow.hPow (β := ℕ) ‖f‖ 2 • gram 𝕜 v - gram.{u_5, u_2, u_4} (E := F) 𝕜 ((⇑f : (a : E) → F) ∘ v)) i j *
          xj)
have simp_rw : LE.le.{u_4} (α := 𝕜)
  (∑ x ∈ c.support,
    ∑ x_1 ∈ c.support,
      HMul.hMul (β := 𝕜)
        (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜)
          (gram.{u_5, u_2, u_4} (E := F) 𝕜 ((⇑f : (a : E) → F) ∘ v) x x_1))
        ((c : (a : n) → 𝕜) x_1 : 𝕜))
  (∑ x ∈ c.support,
    ∑ x_1 ∈ c.support,
      HMul.hMul (β := 𝕜)
        (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜) (HPow.hPow (β := ℕ) ‖f‖ 2 • gram 𝕜 v x x_1))
        ((c : (a : n) → 𝕜) x_1 : 𝕜))
Tactic: simp_rw [Finsupp.sum, Matrix.sub_apply, Matrix.smul_apply, mul_sub, sub_mul,
    Finset.sum_sub_distrib, sub_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramMatrix (goal)
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
⊢ HPow.hPow (α := 𝕜) (β := ℕ)
      (↑(Norm.norm.{u_5} (E := F)
            ((f : (a : E) → F) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)) :
              F)) :
        𝕜)
      2 ≤
    HPow.hPow (β := ℕ) ‖f‖ 2 •
      HPow.hPow (α := 𝕜) (β := ℕ)
        (↑(Norm.norm.{u_1} (E := E)
              (∑ i ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) i : 𝕜) (v i))) :
          𝕜)
        2
have norm_cast : HPow.hPow (β := ℕ)
    (Norm.norm.{u_5} (E := F)
      ((f : (a : E) → F) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)) : F))
    2 ≤
  HPow.hPow (β := ℕ) ‖f‖ 2 •
    HPow.hPow (β := ℕ)
      (Norm.norm.{u_1} (E := E) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)))
      2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramMatrix (goal)
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
⊢ HPow.hPow (β := ℕ)
      (Norm.norm.{u_5} (E := F)
        ((f : (a : E) → F) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)) : F))
      2 ≤
    HPow.hPow (β := ℕ) ‖f‖ 2 •
      HPow.hPow (β := ℕ)
        (Norm.norm.{u_1} (E := E)
          (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)))
        2
have h₁ : LE.le (α := ℝ) 0
  (Norm.norm.{u_5} (E := F)
    ((f : (a : E) → F) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)) : F))
Tactic: grw [f.le_opNorm _, smul_eq_mul, ← mul_pow]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramMatrix (goal)
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
h₁ :
  LE.le (α := ℝ) 0
    (Norm.norm.{u_5} (E := F)
      ((f : (a : E) → F) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)) : F))
⊢ HPow.hPow (β := ℕ)
      (Norm.norm.{u_5} (E := F)
        ((f : (a : E) → F) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)) : F))
      2 ≤
    HPow.hPow (β := ℕ) ‖f‖ 2 •
      HPow.hPow (β := ℕ)
        (Norm.norm.{u_1} (E := E)
          (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)))
        2
have grw : HPow.hPow (β := ℕ)
    (‖f‖ *
      Norm.norm.{u_1} (E := E) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)))
    2 ≤
  HPow.hPow (β := ℕ) ‖f‖ 2 •
    HPow.hPow (β := ℕ)
      (Norm.norm.{u_1} (E := E) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)))
      2
Tactic: grw [f.le_opNorm _, smul_eq_mul, ← mul_pow]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramMatrix (goal)
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
h₁ :
  LE.le (α := ℝ) 0
    (Norm.norm.{u_5} (E := F)
      ((f : (a : E) → F) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)) : F))
grw :
  HPow.hPow (β := ℕ)
      (‖f‖ *
        Norm.norm.{u_1} (E := E)
          (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)))
      2 ≤
    HPow.hPow (β := ℕ) ‖f‖ 2 •
      HPow.hPow (β := ℕ)
        (Norm.norm.{u_1} (E := E)
          (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)))
        2
⊢ HPow.hPow (β := ℕ)
      (Norm.norm.{u_5} (E := F)
        ((f : (a : E) → F) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)) : F))
      2 ≤
    HPow.hPow (β := ℕ) ‖f‖ 2 •
      HPow.hPow (β := ℕ)
        (Norm.norm.{u_1} (E := E)
          (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)))
        2
have grw₁ : HPow.hPow (β := ℕ)
    (‖f‖ *
      Norm.norm.{u_1} (E := E) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)))
    2 ≤
  HPow.hPow (β := ℕ) ‖f‖ 2 *
    HPow.hPow (β := ℕ)
      (Norm.norm.{u_1} (E := E) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)))
      2
Tactic: grw [f.le_opNorm _, smul_eq_mul, ← mul_pow]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramMatrix (goal)
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
h₁ :
  LE.le (α := ℝ) 0
    (Norm.norm.{u_5} (E := F)
      ((f : (a : E) → F) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)) : F))
grw :
  HPow.hPow (β := ℕ)
      (‖f‖ *
        Norm.norm.{u_1} (E := E)
          (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)))
      2 ≤
    HPow.hPow (β := ℕ) ‖f‖ 2 •
      HPow.hPow (β := ℕ)
        (Norm.norm.{u_1} (E := E)
          (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)))
        2
grw₁ :
  HPow.hPow (β := ℕ)
      (‖f‖ *
        Norm.norm.{u_1} (E := E)
          (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)))
      2 ≤
    HPow.hPow (β := ℕ) ‖f‖ 2 *
      HPow.hPow (β := ℕ)
        (Norm.norm.{u_1} (E := E)
          (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)))
        2
⊢ HPow.hPow (β := ℕ)
      (Norm.norm.{u_5} (E := F)
        ((f : (a : E) → F) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)) : F))
      2 ≤
    HPow.hPow (β := ℕ) ‖f‖ 2 •
      HPow.hPow (β := ℕ)
        (Norm.norm.{u_1} (E := E)
          (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)))
        2
have grw₂ : HPow.hPow (β := ℕ)
    (‖f‖ *
      Norm.norm.{u_1} (E := E) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)))
    2 ≤
  HPow.hPow (β := ℕ)
    (‖f‖ *
      Norm.norm.{u_1} (E := E) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)))
    2
Tactic: grw [f.le_opNorm _, smul_eq_mul, ← mul_pow]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramMatrix (goal)
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
⊢ LE.le.{u_4} (α := 𝕜)
    (∑ x ∈ c.support,
      ∑ x_1 ∈ c.support,
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜)
            (gram.{u_5, u_2, u_4} (E := F) 𝕜 ((⇑f : (a : E) → F) ∘ v) x x_1))
          ((c : (a : n) → 𝕜) x_1 : 𝕜))
    (∑ x ∈ c.support,
      ∑ x_1 ∈ c.support,
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜) (HPow.hPow (β := ℕ) ‖f‖ 2 • gram 𝕜 v x x_1))
          ((c : (a : n) → 𝕜) x_1 : 𝕜))
have h1 : ∑ x ∈ c.support,
    ∑ y ∈ c.support,
      HMul.hMul (β := 𝕜)
        (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜)
          (gram.{u_5, u_2, u_4} (E := F) 𝕜 ((⇑f : (a : E) → F) ∘ v) x y))
        ((c : (a : n) → 𝕜) y : 𝕜) =
  HPow.hPow (α := 𝕜) (β := ℕ)
    (↑(Norm.norm.{u_5} (E := F)
          ((f : (a : E) → F) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)) :
            F)) :
      𝕜)
    2
Tactic: calc
    ∑ x ∈ c.support, ∑ y ∈ c.support, star (c x) * gram 𝕜 (f ∘ v) x y * c y
    _ = (‖f (∑ x ∈ c.support, c x • v x)‖ : 𝕜) ^ 2 := ?h1
    _ ≤ ‖f‖ ^ 2 • (‖∑ i ∈ c.support, c i • v i‖ : 𝕜) ^ 2 := by
      norm_cast
      grw [f.le_opNorm _, smul_eq_mul, ← mul_pow]
    _ = ∑ x ∈ c.support, ∑ y ∈ c.support, star (c x) * ‖f‖ ^ 2 • gram 𝕜 v x y * c y := ?h2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramMatrix (goal)
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
h1 :
  ∑ x ∈ c.support,
      ∑ y ∈ c.support,
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜)
            (gram.{u_5, u_2, u_4} (E := F) 𝕜 ((⇑f : (a : E) → F) ∘ v) x y))
          ((c : (a : n) → 𝕜) y : 𝕜) =
    HPow.hPow (α := 𝕜) (β := ℕ)
      (↑(Norm.norm.{u_5} (E := F)
            ((f : (a : E) → F) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)) :
              F)) :
        𝕜)
      2
⊢ LE.le.{u_4} (α := 𝕜)
    (∑ x ∈ c.support,
      ∑ x_1 ∈ c.support,
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜)
            (gram.{u_5, u_2, u_4} (E := F) 𝕜 ((⇑f : (a : E) → F) ∘ v) x x_1))
          ((c : (a : n) → 𝕜) x_1 : 𝕜))
    (∑ x ∈ c.support,
      ∑ x_1 ∈ c.support,
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜) (HPow.hPow (β := ℕ) ‖f‖ 2 • gram 𝕜 v x x_1))
          ((c : (a : n) → 𝕜) x_1 : 𝕜))
have h2 : HPow.hPow (β := ℕ) ‖f‖ 2 •
    HPow.hPow (α := 𝕜) (β := ℕ)
      (↑(Norm.norm.{u_1} (E := E)
            (∑ i ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) i : 𝕜) (v i))) :
        𝕜)
      2 =
  ∑ x ∈ c.support,
    ∑ y ∈ c.support,
      HMul.hMul (β := 𝕜) (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜) (HPow.hPow (β := ℕ) ‖f‖ 2 • gram 𝕜 v x y))
        ((c : (a : n) → 𝕜) y : 𝕜)
Tactic: calc
    ∑ x ∈ c.support, ∑ y ∈ c.support, star (c x) * gram 𝕜 (f ∘ v) x y * c y
    _ = (‖f (∑ x ∈ c.support, c x • v x)‖ : 𝕜) ^ 2 := ?h1
    _ ≤ ‖f‖ ^ 2 • (‖∑ i ∈ c.support, c i • v i‖ : 𝕜) ^ 2 := by
      norm_cast
      grw [f.le_opNorm _, smul_eq_mul, ← mul_pow]
    _ = ∑ x ∈ c.support, ∑ y ∈ c.support, star (c x) * ‖f‖ ^ 2 • gram 𝕜 v x y * c y := ?h2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramMatrix (goal)
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
⊢ ∑ x ∈ c.support,
      ∑ y ∈ c.support,
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜)
            (gram.{u_5, u_2, u_4} (E := F) 𝕜 ((⇑f : (a : E) → F) ∘ v) x y))
          ((c : (a : n) → 𝕜) y : 𝕜) =
    HPow.hPow (α := 𝕜) (β := ℕ)
      (↑(Norm.norm.{u_5} (E := F)
            ((f : (a : E) → F) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)) :
              F)) :
        𝕜)
      2
have h1 : ∑ y ∈ c.support,
    ∑ x ∈ c.support,
      HMul.hMul (β := 𝕜)
        (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜)
          (gram.{u_5, u_2, u_4} (E := F) 𝕜 ((⇑f : (a : E) → F) ∘ v) x y))
        ((c : (a : n) → 𝕜) y : 𝕜) =
  HPow.hPow (α := 𝕜) (β := ℕ)
    (↑(Norm.norm.{u_5} (E := F)
          ((f : (a : E) → F) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)) :
            F)) :
      𝕜)
    2
Tactic: rw [Finset.sum_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramMatrix (goal)
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
⊢ ∑ y ∈ c.support,
      ∑ x ∈ c.support,
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜)
            (gram.{u_5, u_2, u_4} (E := F) 𝕜 ((⇑f : (a : E) → F) ∘ v) x y))
          ((c : (a : n) → 𝕜) y : 𝕜) =
    HPow.hPow (α := 𝕜) (β := ℕ)
      (↑(Norm.norm.{u_5} (E := F)
            ((f : (a : E) → F) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)) :
              F)) :
        𝕜)
      2
have h1 : Eq.{u_4 + 1} (α := 𝕜)
  (∑ x ∈ c.support,
    ∑ x_1 ∈ c.support,
      HMul.hMul (β := 𝕜)
        (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((c : (a : n) → 𝕜) x_1 : 𝕜) : 𝕜)
          (inner.{u_4, u_5} 𝕜 (E := F) ((f : (a : E) → F) (v x_1) : F) ((f : (a : E) → F) (v x) : F)))
        ((c : (a : n) → 𝕜) x : 𝕜))
  (∑ x ∈ c.support,
    ∑ i ∈ c.support,
      HMul.hMul (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜)
        (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((c : (a : n) → 𝕜) i : 𝕜) : 𝕜)
          (inner.{u_4, u_5} 𝕜 (E := F) ((f : (a : E) → F) (v i) : F) ((f : (a : E) → F) (v x) : F))))
Tactic: simp [← inner_self_eq_norm_sq_to_K, inner_sum, sum_inner, inner_smul_left, inner_smul_right,
      Finset.mul_sum, Finset.smul_sum, RCLike.real_smul_eq_coe_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramMatrix (goal)
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
⊢ HPow.hPow (β := ℕ) ‖f‖ 2 •
      HPow.hPow (α := 𝕜) (β := ℕ)
        (↑(Norm.norm.{u_1} (E := E)
              (∑ i ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) i : 𝕜) (v i))) :
          𝕜)
        2 =
    ∑ x ∈ c.support,
      ∑ y ∈ c.support,
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜) (HPow.hPow (β := ℕ) ‖f‖ 2 • gram 𝕜 v x y))
          ((c : (a : n) → 𝕜) y : 𝕜)
have h2 : HPow.hPow (β := ℕ) ‖f‖ 2 •
    HPow.hPow (α := 𝕜) (β := ℕ)
      (↑(Norm.norm.{u_1} (E := E)
            (∑ i ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) i : 𝕜) (v i))) :
        𝕜)
      2 =
  ∑ y ∈ c.support,
    ∑ x ∈ c.support,
      HMul.hMul (β := 𝕜) (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜) (HPow.hPow (β := ℕ) ‖f‖ 2 • gram 𝕜 v x y))
        ((c : (a : n) → 𝕜) y : 𝕜)
Tactic: rw [Finset.sum_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramMatrix (goal)
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
⊢ HPow.hPow (β := ℕ) ‖f‖ 2 •
      HPow.hPow (α := 𝕜) (β := ℕ)
        (↑(Norm.norm.{u_1} (E := E)
              (∑ i ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) i : 𝕜) (v i))) :
          𝕜)
        2 =
    ∑ y ∈ c.support,
      ∑ x ∈ c.support,
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜) (HPow.hPow (β := ℕ) ‖f‖ 2 • gram 𝕜 v x y))
          ((c : (a : n) → 𝕜) y : 𝕜)
have h2 : Eq.{u_4 + 1} (α := 𝕜)
  (∑ x ∈ c.support,
    ∑ x_1 ∈ c.support,
      HPow.hPow (α := 𝕜) (β := ℕ) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖f‖ : 𝕜) 2 *
        HMul.hMul (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜)
          (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((c : (a : n) → 𝕜) x_1 : 𝕜) : 𝕜) ⟪v x_1, v x⟫_𝕜))
  (∑ x ∈ c.support,
    ∑ x_1 ∈ c.support,
      HMul.hMul (β := 𝕜)
        (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((c : (a : n) → 𝕜) x_1 : 𝕜) : 𝕜)
          (HPow.hPow (α := 𝕜) (β := ℕ) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖f‖ : 𝕜) 2 * ⟪v x_1, v x⟫_𝕜))
        ((c : (a : n) → 𝕜) x : 𝕜))
Tactic: simp [← inner_self_eq_norm_sq_to_K, inner_sum, sum_inner, inner_smul_left, inner_smul_right,
      Finset.mul_sum, Finset.smul_sum, RCLike.real_smul_eq_coe_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
n : ι
⊢ gramSchmidt 𝕜 f n = f n - ∑ i ∈ Iio n, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f n)
have rw : gramSchmidt 𝕜 f n = f n - ∑ x ∈ (Iio n).attach, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f (↑x : ι)) : (a : E) → E) (f n)
Tactic: rw [← sum_attach, attach_eq_univ, gramSchmidt]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
n : ι
rw : gramSchmidt 𝕜 f n = f n - ∑ x ∈ (Iio n).attach, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f (↑x : ι)) : (a : E) → E) (f n)
⊢ gramSchmidt 𝕜 f n = f n - ∑ i ∈ Iio n, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f n)
have rw₁ : gramSchmidt 𝕜 f n = f n - ∑ x : ↥(Iio n), (starProjection (𝕜 ∙ gramSchmidt 𝕜 f (↑x : ι)) : (a : E) → E) (f n)
Tactic: rw [← sum_attach, attach_eq_univ, gramSchmidt]