awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : DecidableEq n
i : n
x : E
⊢ gram.{u_1, u_2, u_4} (E := E) 𝕜 (Pi.single (M := fun (a : n) ↦ E) i x) i i = single i i (⟪x, x⟫_𝕜) i i

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : n → E
m : Set n
f : (↑m : Type u_2) → n
⊢ (gram 𝕜 v).submatrix f f = gram 𝕜 (v ∘ f)

Tactic:
rfl

Premises used: Matrix.gram, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : n → E
⊢ (gram 𝕜 v).IsHermitian

Tactic:
Matrix.ext fun _ _ ↦ inner_conj_symm _ _

Premises used: Matrix.IsHermitian, Matrix.ext, inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype n
v : n → E
x y : n → 𝕜
trans :
  star x ⬝ᵥ gram 𝕜 v *ᵥ y =
    ∑ i : n, ∑ j : n, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x i) : 𝕜) (y j) * ⟪v i, v j⟫_𝕜
trans₁ :
  ∑ i : n, ∑ j : n, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x i) : 𝕜) (y j) * ⟪v i, v j⟫_𝕜 =
    inner.{u_4, u_1} 𝕜 (E := E) (∑ i : n, x i • v i) (∑ i : n, y i • v i)
⊢ star x ⬝ᵥ gram 𝕜 v *ᵥ y = inner.{u_4, u_1} 𝕜 (E := E) (∑ i : n, x i • v i) (∑ i : n, y i • v i)

Tactic:
trans ∑ i, ∑ j, conj (x i) * y j * ⟪v i, v j⟫_𝕜
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype n
v : n → E
x y : n → 𝕜
simp_rw :
  Eq.{u_4 + 1} (α := 𝕜) (∑ i : n, star x i * (gram 𝕜 v *ᵥ y) i)
    (∑ i : n, ∑ j : n, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x i) : 𝕜) (y j) * ⟪v i, v j⟫_𝕜)
simp_rw₁ :
  Eq.{u_4 + 1} (α := 𝕜) (∑ i : n, star x i * (gram 𝕜 v *ᵥ y) i)
    (∑ x_1 : n, ∑ x_2 : n, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x x_1) : 𝕜) (y x_2 * ⟪v x_1, v x_2⟫_𝕜))
simp_rw₂ :
  Eq.{u_4 + 1} (α := 𝕜) (∑ i : n, star x i * (gram 𝕜 v *ᵥ y) i)
    (∑ x_1 : n,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x x_1) : 𝕜) (∑ i : n, y i * ⟪v x_1, v i⟫_𝕜 : 𝕜))
simp_rw₃ :
  Eq.{u_4 + 1} (α := 𝕜) (∑ x_1 : n, star x x_1 * (fun (j : n) ↦ gram 𝕜 v x_1 j) ⬝ᵥ y)
    (∑ x_1 : n,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x x_1) : 𝕜) (∑ i : n, y i * ⟪v x_1, v i⟫_𝕜 : 𝕜))
simp_rw₄ :
  Eq.{u_4 + 1} (α := 𝕜) (∑ x_1 : n, star x x_1 * ∑ x : n, gram 𝕜 v x_1 x * y x)
    (∑ x_1 : n,
      HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x x_1) : 𝕜) (∑ i : n, y i * ⟪v x_1, v i⟫_𝕜 : 𝕜))
simp_rw₅ :
  Eq.{u_4 + 1} (α := 𝕜) (∑ x_1 : n, (∑ x : n, y x * gram 𝕜 v x_1 x) * star x x_1)
    (∑ x_1 : n,
      HMul.hMul (α := 𝕜) (β := 𝕜) (∑ i : n, y i * ⟪v x_1, v i⟫_𝕜 : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x x_1) : 𝕜))
simp_rw₆ :
  Eq.{u_4 + 1} (α := 𝕜) (∑ x_1 : n, (∑ x : n, y x * gram 𝕜 v x_1 x) * star x x_1)
    (∑ x_1 : n, (∑ i : n, y i * ⟪v x_1, v i⟫_𝕜) * star (x x_1))
simp_rw₇ :
  Eq.{u_4 + 1} (α := 𝕜) (∑ x_1 : n, (∑ x : n, y x * ⟪v x_1, v x⟫_𝕜) * star x x_1)
    (∑ x_1 : n, (∑ i : n, y i * ⟪v x_1, v i⟫_𝕜) * star (x x_1))
⊢ star x ⬝ᵥ gram 𝕜 v *ᵥ y =
    ∑ i : n, ∑ j : n, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x i) : 𝕜) (y j) * ⟪v i, v j⟫_𝕜

Tactic:
simp_rw [dotProduct, mul_assoc, ← Finset.mul_sum, mulVec, dotProduct, mul_comm, ← star_def,
      gram_apply, Pi.star_apply]

Premises used: Finset.mul_sum, RCLike.star_def, dotProduct, mul_assoc, Pi.star_apply, mul_comm, Matrix.gram_apply, Matrix.mulVec
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype n
v : n → E
x y : n → 𝕜
simp_rw :
  Eq.{u_4 + 1} (α := 𝕜)
    (∑ i : n, ∑ j : n, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x i) : 𝕜) (y j) * ⟪v i, v j⟫_𝕜)
    (∑ i : n, ⟪x i • v i, ∑ i : n, y i • v i⟫_𝕜)
simp_rw₁ :
  Eq.{u_4 + 1} (α := 𝕜)
    (∑ i : n, ∑ j : n, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x i) : 𝕜) (y j) * ⟪v i, v j⟫_𝕜)
    (∑ x_1 : n, ∑ i : n, ⟪x x_1 • v x_1, y i • v i⟫_𝕜)
simp_rw₂ :
  Eq.{u_4 + 1} (α := 𝕜)
    (∑ i : n, ∑ j : n, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x i) : 𝕜) (y j) * ⟪v i, v j⟫_𝕜)
    (∑ x_1 : n, ∑ x_2 : n, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x x_1) : 𝕜) ⟪v x_1, y x_2 • v x_2⟫_𝕜)
simp_rw₃ :
  Eq.{u_4 + 1} (α := 𝕜)
    (∑ i : n, ∑ j : n, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x i) : 𝕜) (y j) * ⟪v i, v j⟫_𝕜)
    (∑ x_1 : n, ∑ x_2 : n, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x x_1) : 𝕜) (y x_2 * ⟪v x_1, v x_2⟫_𝕜))
⊢ ∑ i : n, ∑ j : n, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x i) : 𝕜) (y j) * ⟪v i, v j⟫_𝕜 =
    inner.{u_4, u_1} 𝕜 (E := E) (∑ i : n, x i • v i) (∑ i : n, y i • v i)

Tactic:
simp_rw [sum_inner, inner_sum, inner_smul_left, inner_smul_right, mul_assoc]

Premises used: inner_sum, mul_assoc, sum_inner, inner_smul_right, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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
have : ∀ (this : Fintype n), (gram 𝕜 v).PosSemidef
⊢ (gram 𝕜 v).PosSemidef

Tactic:
have := Fintype.ofFinite n
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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
this : Fintype n
⊢ (gram 𝕜 v).PosSemidef

Tactic:
.of_dotProduct_mulVec_nonneg (isHermitian_gram _ _) fun x ↦ ?_

Premises used: Matrix.isHermitian_gram, Matrix.PosSemidef.of_dotProduct_mulVec_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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
this : Fintype n
refine : ∀ (x : n → 𝕜), 0 ≤ star x ⬝ᵥ gram 𝕜 v *ᵥ x
⊢ (gram 𝕜 v).PosSemidef

Tactic:
refine .of_dotProduct_mulVec_nonneg (isHermitian_gram _ _) fun x ↦ ?_
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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
this : Fintype n
x : n → 𝕜
rw :
  LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) 0 : ℝ)
      ((re : (a : 𝕜) → ℝ) (inner.{u_4, u_1} 𝕜 (E := E) (∑ i : n, x i • v i) (∑ i : n, x i • v i)) : ℝ) ∧
    Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) 0 : ℝ)
      ((im : (a : 𝕜) → ℝ) (inner.{u_4, u_1} 𝕜 (E := E) (∑ i : n, x i • v i) (∑ i : n, x i • v i)) : ℝ)
⊢ 0 ≤ star x ⬝ᵥ gram 𝕜 v *ᵥ x

Tactic:
rw [star_dotProduct_gram_mulVec, le_iff_re_im]

Premises used: RCLike.le_iff_re_im, Matrix.star_dotProduct_gram_mulVec
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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
this : Fintype n
x : n → 𝕜
⊢ LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) 0 : ℝ)
      ((re : (a : 𝕜) → ℝ) (inner.{u_4, u_1} 𝕜 (E := E) (∑ i : n, x i • v i) (∑ i : n, x i • v i)) : ℝ) ∧
    Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) 0 : ℝ)
      ((im : (a : 𝕜) → ℝ) (inner.{u_4, u_1} 𝕜 (E := E) (∑ i : n, x i • v i) (∑ i : n, x i • v i)) : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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
have : ∀ (this : Fintype n), LinearIndependent 𝕜 v
⊢ LinearIndependent 𝕜 v

Tactic:
have := Fintype.ofFinite n
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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
rw : ∀ (g : n → 𝕜), Eq.{u_1 + 1} (α := E) (∑ i : n, g i • v i) 0 → ∀ (i : n), g i = 0
⊢ LinearIndependent 𝕜 v

Tactic:
rw [Fintype.linearIndependent_iff]

Premises used: Fintype.linearIndependent_iff
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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
⊢ ∀ (hx : y ≠ 0), 0 < star y ⬝ᵥ gram 𝕜 v *ᵥ y

Tactic:
have := h_gram.dotProduct_mulVec_pos (x := y)
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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_1 : Fintype n
y : n → 𝕜
hy : Eq.{u_1 + 1} (α := E) (∑ i : n, y i • v i) 0
this : ∀ (hx : y ≠ 0), 0 < star y ⬝ᵥ gram 𝕜 v *ᵥ y
⊢ ∀ (i : n), y i = 0

Tactic:
simp_all [star_dotProduct_gram_mulVec]

Premises used: Matrix.star_dotProduct_gram_mulVec
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype n
inst_4 : DecidableEq n
v : n → E
h : (gram 𝕜 v).det ≠ 0
⊢ LinearIndependent 𝕜 v

Tactic:
linearIndependent_of_posDef_gram <| (posSemidef_gram 𝕜 v).posDef_iff_det_ne_zero.mpr h

Premises used: Iff.mpr, Matrix.linearIndependent_of_posDef_gram, Matrix.posSemidef_gram, Matrix.PosSemidef.posDef_iff_det_ne_zero
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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
have : ∀ (this : Fintype n), (gram 𝕜 v).PosDef
⊢ (gram 𝕜 v).PosDef

Tactic:
have := Fintype.ofFinite n
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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
⊢ ∀ (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

Premises used: Fintype.linearIndependent_iff
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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

Tactic:
.of_dotProduct_mulVec_pos (isHermitian_gram _ _) fun x hx ↦
    ((posSemidef_gram ..).dotProduct_mulVec_nonneg _).lt_of_ne' ?_

Premises used: Matrix.isHermitian_gram, Matrix.posSemidef_gram, Matrix.PosSemidef.dotProduct_mulVec_nonneg, LE.le.lt_of_ne', Matrix.PosDef.of_dotProduct_mulVec_pos
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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
refine : ∀ (x : n → 𝕜) (hx : x ≠ 0), star x ⬝ᵥ gram 𝕜 v *ᵥ x ≠ 0
⊢ (gram 𝕜 v).PosDef

Tactic:
refine .of_dotProduct_mulVec_pos (isHermitian_gram _ _) fun x hx ↦
    ((posSemidef_gram ..).dotProduct_mulVec_nonneg _).lt_of_ne' ?_
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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
rw : Ne.{u_1 + 1} (α := E) (∑ i : n, x i • v i) 0
⊢ star x ⬝ᵥ gram 𝕜 v *ᵥ x ≠ 0

Tactic:
rw [star_dotProduct_gram_mulVec, inner_self_eq_zero.ne]

Premises used: inner_self_eq_zero, Matrix.star_dotProduct_gram_mulVec, Iff.ne
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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
⊢ Ne.{u_1 + 1} (α := E) (∑ i : n, x i • v i) 0

Tactic:
mt (h_li x) (mt funext hx)

Premises used: mt, funext
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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
⊢ Ne.{u_1 + 1} (α := E) (∑ i : n, x i • v i) 0

Tactic:
exact mt (h_li x) (mt funext hx)

Premises used: mt, funext
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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
⊢ (gram 𝕜 v).PosDef ↔ LinearIndependent 𝕜 v

Tactic:
⟨linearIndependent_of_posDef_gram, posDef_gram_of_linearIndependent⟩

Premises used: Matrix.posDef_gram_of_linearIndependent, Matrix.linearIndependent_of_posDef_gram, Iff.intro
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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
rw₁ rw₂ : (gram 𝕜 v).det ≠ 0 ↔ (gram 𝕜 v).det ≠ 0
⊢ (gram 𝕜 v).det ≠ 0 ↔ LinearIndependent 𝕜 v

Tactic:
rw [← posDef_gram_iff_linearIndependent, (posSemidef_gram 𝕜 v).posDef_iff_det_ne_zero]

Premises used: Matrix.posDef_gram_iff_linearIndependent, Matrix.posSemidef_gram, Matrix.PosSemidef.posDef_iff_det_ne_zero
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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
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
⊢ 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)

Tactic:
ext i j
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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
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:
simp [mul_apply, b.repr_apply_apply, b.sum_inner_mul_inner]

Premises used: OrthonormalBasis.sum_inner_mul_inner, Matrix.mul_apply, OrthonormalBasis.repr_apply_apply
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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

Tactic:
⟨(isHermitian_gram 𝕜 v).smul (((Pi.isSelfAdjoint.mpr (congrFun rfl)).apply f).pow 2)
    |>.sub (isHermitian_gram 𝕜 (f ∘ v)), fun c ↦ ?_⟩

Premises used: Function.comp, Matrix.isHermitian_gram, Matrix.PosSemidef, Matrix.IsHermitian.smul, And.intro, IsSelfAdjoint.pow, Matrix.IsHermitian.sub, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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
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)
⊢ (HPow.hPow (β := ℕ) ‖f‖ 2 • gram 𝕜 v - gram.{u_5, u_2, u_4} (E := F) 𝕜 ((⇑f : (a : E) → F) ∘ v)).PosSemidef

Tactic:
refine ⟨(isHermitian_gram 𝕜 v).smul (((Pi.isSelfAdjoint.mpr (congrFun rfl)).apply f).pow 2)
    |>.sub (isHermitian_gram 𝕜 (f ∘ v)), fun c ↦ ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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 →₀ 𝕜
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 : 𝕜))
⊢ 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:
simp_rw [Finsupp.sum, Matrix.sub_apply, Matrix.smul_apply, mul_sub, sub_mul,
    Finset.sum_sub_distrib, sub_nonneg]

Premises used: mul_sub, Finsupp.sum, Matrix.sub_apply, Matrix.smul_apply, sub_mul, Finset.sum_sub_distrib, sub_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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

Tactic:
?h1
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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 →₀ 𝕜
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
⊢ 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

Tactic:
norm_cast
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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
grw₂ 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
⊢ 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:
grw [f.le_opNorm _, smul_eq_mul, ← mul_pow]

Premises used: ContinuousLinearMap.le_opNorm, smul_eq_mul, mul_pow
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
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 : 𝕜)

Tactic:
?h2