awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (hypothesis)
Goal:
ι : Type u_1
E : Type u_2
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
b : OrthonormalBasis ι ℝ E
L : StrongDual ℝ E
⊢ HPow.hPow (β := ℕ) ‖L‖ 2 = ∑ i : ι, HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : E) → ℝ) ((b : (a : ι) → E) i : E) : ℝ) 2
have this : FiniteDimensional ℝ E
Tactic: have := b.toBasis.finiteDimensional_of_finite
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
b : OrthonormalBasis ι ℝ E
L : StrongDual ℝ E
this : FiniteDimensional ℝ E
⊢ HPow.hPow (β := ℕ) ‖L‖ 2 = ∑ i : ι, HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : E) → ℝ) ((b : (a : ι) → E) i : E) : ℝ) 2
have simp_rw : HPow.hPow (β := ℕ)
    (norm (E := E) ((LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E) : (a : StrongDual ℝ E) → E) L : E)) 2 =
  ∑ i : ι, HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : E) → ℝ) ((b : (a : ι) → E) i : E) : ℝ) 2
Tactic: simp_rw [← (InnerProductSpace.toDual ℝ E).symm.norm_map, ← b.sum_sq_inner_left,
    InnerProductSpace.toDual_symm_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
b : OrthonormalBasis ι ℝ E
L : StrongDual ℝ E
this : FiniteDimensional ℝ E
simp_rw :
  HPow.hPow (β := ℕ)
      (norm (E := E) ((LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E) : (a : StrongDual ℝ E) → E) L : E)) 2 =
    ∑ i : ι, HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : E) → ℝ) ((b : (a : ι) → E) i : E) : ℝ) 2
⊢ HPow.hPow (β := ℕ) ‖L‖ 2 = ∑ i : ι, HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : E) → ℝ) ((b : (a : ι) → E) i : E) : ℝ) 2
have simp_rw₁ : Eq (α := ℝ)
  (∑ i : ι,
    HPow.hPow (β := ℕ)
      (inner ℝ (E := E) ((LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E) : (a : StrongDual ℝ E) → E) L : E)
        ((b : (a : ι) → E) i : E))
      2)
  (∑ i : ι, HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : E) → ℝ) ((b : (a : ι) → E) i : E) : ℝ) 2)
Tactic: simp_rw [← (InnerProductSpace.toDual ℝ E).symm.norm_map, ← b.sum_sq_inner_left,
    InnerProductSpace.toDual_symm_apply]
-- 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 : 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) = single i i ⟪x, x⟫_𝕜
have a : ∀ (j k : n), gram.{u_1, u_2, u_4} (E := E) 𝕜 (Pi.single (M := fun (a : n) ↦ E) i x) j k = single i i (⟪x, x⟫_𝕜) j k
Tactic: ext j k
-- 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 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : DecidableEq n
i : n
x : E
j k : n
⊢ gram.{u_1, u_2, u_4} (E := E) 𝕜 (Pi.single (M := fun (a : n) ↦ E) i x) j k = single i i (⟪x, x⟫_𝕜) j k
have a : ∀ (hij : i ≠ j), gram.{u_1, u_2, u_4} (E := E) 𝕜 (Pi.single (M := fun (a : n) ↦ E) i x) j k = single i i (⟪x, x⟫_𝕜) j k
Tactic: obtain hij | rfl := ne_or_eq 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 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : DecidableEq n
i : n
x : E
j k : n
a :
  ∀ (hij : i ≠ j),
    gram.{u_1, u_2, u_4} (E := E) 𝕜 (Pi.single (M := fun (a : n) ↦ E) i x) j k = single i i (⟪x, x⟫_𝕜) j k
⊢ gram.{u_1, u_2, u_4} (E := E) 𝕜 (Pi.single (M := fun (a : n) ↦ E) i x) j k = single i i (⟪x, x⟫_𝕜) j k
have a₁ : gram.{u_1, u_2, u_4} (E := E) 𝕜 (Pi.single (M := fun (a : n) ↦ E) i x) i k = single i i (⟪x, x⟫_𝕜) i k
Tactic: obtain hij | rfl := ne_or_eq i j
Cleared hypotheses: 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 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : DecidableEq n
i : n
x : E
k : n
⊢ gram.{u_1, u_2, u_4} (E := E) 𝕜 (Pi.single (M := fun (a : n) ↦ E) i x) i k = single i i (⟪x, x⟫_𝕜) i k
have a : ∀ (hik : i ≠ k), gram.{u_1, u_2, u_4} (E := E) 𝕜 (Pi.single (M := fun (a : n) ↦ E) i x) i k = single i i (⟪x, x⟫_𝕜) i k
Tactic: obtain hik | rfl := ne_or_eq i k
-- 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 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : DecidableEq n
i : n
x : E
k : n
a :
  ∀ (hik : i ≠ k),
    gram.{u_1, u_2, u_4} (E := E) 𝕜 (Pi.single (M := fun (a : n) ↦ E) i x) i k = single i i (⟪x, x⟫_𝕜) i k
⊢ gram.{u_1, u_2, u_4} (E := E) 𝕜 (Pi.single (M := fun (a : n) ↦ E) i x) i k = single i i (⟪x, x⟫_𝕜) i k
have a₁ : 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: obtain hik | rfl := ne_or_eq i k
Cleared hypotheses: k
-- 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 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype n
v : n → E
x y : n → 𝕜
⊢ star x ⬝ᵥ gram 𝕜 v *ᵥ y = inner.{u_4, u_1} 𝕜 (E := E) (∑ i : n, x i • v i) (∑ i : n, y i • v i)
have trans : star x ⬝ᵥ gram 𝕜 v *ᵥ y =
  ∑ i : n, ∑ j : n, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x i) : 𝕜) (y j) * ⟪v i, v j⟫_𝕜
Tactic: trans ∑ i, ∑ j, conj (x i) * y j * ⟪v i, v 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 : 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⟫_𝕜
⊢ star x ⬝ᵥ gram 𝕜 v *ᵥ y = inner.{u_4, u_1} 𝕜 (E := E) (∑ i : n, x i • v i) (∑ i : n, y i • v i)
have 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)
Tactic: trans ∑ i, ∑ j, conj (x i) * y j * ⟪v i, v 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 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype n
v : n → E
x y : n → 𝕜
⊢ star x ⬝ᵥ gram 𝕜 v *ᵥ y =
    ∑ i : n, ∑ j : n, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x i) : 𝕜) (y j) * ⟪v i, v j⟫_𝕜
have 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⟫_𝕜)
Tactic: simp_rw [dotProduct, mul_assoc, ← Finset.mul_sum, mulVec, dotProduct, mul_comm, ← star_def,
      gram_apply, Pi.star_apply]
-- 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 : 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⟫_𝕜)
⊢ star x ⬝ᵥ gram 𝕜 v *ᵥ y =
    ∑ i : n, ∑ j : n, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x i) : 𝕜) (y j) * ⟪v i, v j⟫_𝕜
have 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⟫_𝕜))
Tactic: simp_rw [dotProduct, mul_assoc, ← Finset.mul_sum, mulVec, dotProduct, mul_comm, ← star_def,
      gram_apply, Pi.star_apply]
-- 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 : 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⟫_𝕜))
⊢ star x ⬝ᵥ gram 𝕜 v *ᵥ y =
    ∑ i : n, ∑ j : n, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x i) : 𝕜) (y j) * ⟪v i, v j⟫_𝕜
have 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⟫_𝕜 : 𝕜))
Tactic: simp_rw [dotProduct, mul_assoc, ← Finset.mul_sum, mulVec, dotProduct, mul_comm, ← star_def,
      gram_apply, Pi.star_apply]
-- 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 : 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⟫_𝕜 : 𝕜))
⊢ star x ⬝ᵥ gram 𝕜 v *ᵥ y =
    ∑ i : n, ∑ j : n, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x i) : 𝕜) (y j) * ⟪v i, v j⟫_𝕜
have 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⟫_𝕜 : 𝕜))
Tactic: simp_rw [dotProduct, mul_assoc, ← Finset.mul_sum, mulVec, dotProduct, mul_comm, ← star_def,
      gram_apply, Pi.star_apply]
-- 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 : 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⟫_𝕜 : 𝕜))
⊢ star x ⬝ᵥ gram 𝕜 v *ᵥ y =
    ∑ i : n, ∑ j : n, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x i) : 𝕜) (y j) * ⟪v i, v j⟫_𝕜
have 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⟫_𝕜 : 𝕜))
Tactic: simp_rw [dotProduct, mul_assoc, ← Finset.mul_sum, mulVec, dotProduct, mul_comm, ← star_def,
      gram_apply, Pi.star_apply]
-- 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 : 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⟫_𝕜 : 𝕜))
⊢ star x ⬝ᵥ gram 𝕜 v *ᵥ y =
    ∑ i : n, ∑ j : n, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x i) : 𝕜) (y j) * ⟪v i, v j⟫_𝕜
have 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) : 𝕜))
Tactic: simp_rw [dotProduct, mul_assoc, ← Finset.mul_sum, mulVec, dotProduct, mul_comm, ← star_def,
      gram_apply, Pi.star_apply]
-- 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 : 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) : 𝕜))
⊢ star x ⬝ᵥ gram 𝕜 v *ᵥ y =
    ∑ i : n, ∑ j : n, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x i) : 𝕜) (y j) * ⟪v i, v j⟫_𝕜
have 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))
Tactic: simp_rw [dotProduct, mul_assoc, ← Finset.mul_sum, mulVec, dotProduct, mul_comm, ← star_def,
      gram_apply, Pi.star_apply]
-- 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 : 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))
⊢ star x ⬝ᵥ gram 𝕜 v *ᵥ y =
    ∑ i : n, ∑ j : n, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x i) : 𝕜) (y j) * ⟪v i, v j⟫_𝕜
have 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))
Tactic: simp_rw [dotProduct, mul_assoc, ← Finset.mul_sum, mulVec, dotProduct, mul_comm, ← star_def,
      gram_apply, Pi.star_apply]
-- 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 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype n
v : n → E
x y : n → 𝕜
⊢ ∑ 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)
have 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⟫_𝕜)
Tactic: simp_rw [sum_inner, inner_sum, inner_smul_left, inner_smul_right, mul_assoc]
-- 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 : 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⟫_𝕜)
⊢ ∑ 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)
have 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⟫_𝕜)
Tactic: simp_rw [sum_inner, inner_sum, inner_smul_left, inner_smul_right, mul_assoc]
-- 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 : 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⟫_𝕜)
⊢ ∑ 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)
have 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⟫_𝕜)
Tactic: simp_rw [sum_inner, inner_sum, inner_smul_left, inner_smul_right, mul_assoc]
-- 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 : 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⟫_𝕜)
⊢ ∑ 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)
have 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⟫_𝕜))
Tactic: simp_rw [sum_inner, inner_sum, inner_smul_left, inner_smul_right, mul_assoc]
-- 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 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Finite n
v : n → E
⊢ (gram 𝕜 v).PosSemidef
have have : ∀ (this : Fintype n), (gram 𝕜 v).PosSemidef
Tactic: have := Fintype.ofFinite n
-- 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 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Finite n
v : n → E
this : Fintype n
⊢ (gram 𝕜 v).PosSemidef
have refine : ∀ (x : n → 𝕜), 0 ≤ star x ⬝ᵥ gram 𝕜 v *ᵥ x
Tactic: refine .of_dotProduct_mulVec_nonneg (isHermitian_gram _ _) fun x ↦ ?_
-- 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 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Finite n
v : n → E
this : Fintype n
x : n → 𝕜
⊢ 0 ≤ star x ⬝ᵥ gram 𝕜 v *ᵥ x
have 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)) : ℝ)
Tactic: rw [star_dotProduct_gram_mulVec, le_iff_re_im]
-- 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 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Finite n
v : n → E
h_gram : (gram 𝕜 v).PosDef
⊢ LinearIndependent 𝕜 v
have have : ∀ (this : Fintype n), LinearIndependent 𝕜 v
Tactic: have := Fintype.ofFinite n
-- 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 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Finite n
v : n → E
h_gram : (gram 𝕜 v).PosDef
this : Fintype n
⊢ LinearIndependent 𝕜 v
have rw : ∀ (g : n → 𝕜), Eq.{u_1 + 1} (α := E) (∑ i : n, g i • v i) 0 → ∀ (i : n), g i = 0
Tactic: rw [Fintype.linearIndependent_iff]