awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E ≃ₗ[𝕜] E
hT : (↑T : E →ₗ[𝕜] E).IsPositive
x : E
this : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, (T.symm : (a : E) → E) x⟫ : ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪((↑T.symm : E →ₗ[𝕜] E) : (a : E) → E) x, x⟫ : ℝ)
have rwa : ∀ (this : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, ((↑T.symm : E →ₗ[𝕜] E) : (a : E) → E) x⟫ : ℝ)),
  LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪((↑T.symm : E →ₗ[𝕜] E) : (a : E) → E) x, x⟫ : ℝ)
Tactic: rwa [← T.symm.coe_toLinearMap, ← hT.isSymmetric.toLinearMap_symm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E ≃ₗ[𝕜] E
hT : (↑T : E →ₗ[𝕜] E).IsPositive
x : E
this : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, (T.symm : (a : E) → E) x⟫ : ℝ)
rwa :
  ∀ (this : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, ((↑T.symm : E →ₗ[𝕜] E) : (a : E) → E) x⟫ : ℝ)),
    LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪((↑T.symm : E →ₗ[𝕜] E) : (a : E) → E) x, x⟫ : ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪((↑T.symm : E →ₗ[𝕜] E) : (a : E) → E) x, x⟫ : ℝ)
have rwa₁ : ∀ (this : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪((↑T.symm : E →ₗ[𝕜] E) : (a : E) → E) x, x⟫ : ℝ)),
  LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪((↑T.symm : E →ₗ[𝕜] E) : (a : E) → E) x, x⟫ : ℝ)
Tactic: rwa [← T.symm.coe_toLinearMap, ← hT.isSymmetric.toLinearMap_symm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
⊢ ContinuousLinearMap.IsPositive.{u_1, u_2} (𝕜 := 𝕜) (E := E)
    ((((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) x : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) x)
have simp_rw : True ∧ ∀ (x_1 : E), 0 ≤ HPow.hPow (β := ℕ) ‖⟪x, x_1⟫‖ 2
Tactic: simp_rw [ContinuousLinearMap.isPositive_iff, isSymmetric_rankOne_self, rankOne_apply,
    inner_smul_left, RCLike.conj_mul, ← RCLike.ofReal_pow, RCLike.ofReal_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
⊢ T.IsPositive ↔
    ∃ (m : ℕ) (u : Fin m → E),
      T =
        ∑ i : Fin m,
          (((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) (u i) : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) (u i)
have refine : ∀ (hT : T.IsPositive),
  ∃ (m : ℕ) (u : Fin m → E),
    T =
      ∑ i : Fin m, (((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) (u i) : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) (u i)
Tactic: refine ⟨fun hT ↦ ?_, fun ⟨m, u, hT⟩ ↦ hT ▸ isPositive_sum _ fun _ _ ↦ isPositive_rankOne_self _⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
a : (i : Fin (Module.finrank 𝕜 E)) → E :=
  fun (i : Fin (Module.finrank 𝕜 E)) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑√(⋯.eigenvalues ⋯ i) : 𝕜)
      ((⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) i : E)
⊢ ∃ (m : ℕ) (u : Fin m → E),
    T =
      ∑ i : Fin m, (((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) (u i) : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) (u i)
have refine : ∀ (x : E),
  Eq (α := E) ((T : (a : E) → E) x : E)
    ((∑ i : Fin (Module.finrank 𝕜 E),
            (((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) (a i) : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) (a i) :
          (a : E) → E)
        x :
      E)
Tactic: refine ⟨Module.finrank 𝕜 E, a, ext fun _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
a : (i : Fin (Module.finrank 𝕜 E)) → E :=
  fun (i : Fin (Module.finrank 𝕜 E)) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑√(⋯.eigenvalues ⋯ i) : 𝕜)
      ((⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) i : E)
x : E
⊢ Eq (α := E) ((T : (a : E) → E) x : E)
    ((∑ i : Fin (Module.finrank 𝕜 E),
            (((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) (a i) : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) (a i) :
          (a : E) → E)
        x :
      E)
have simp_rw : Eq (α := E) ((T : (a : E) → E) x : E)
  (∑ d : Fin (Module.finrank 𝕜 E),
      (((((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) (a d) : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) (a d) :
            E →L[𝕜] E) :
          (a : E) → E)
        x :
    E)
Tactic: simp_rw [sum_apply, rankOne_apply, a, inner_smul_left, smul_smul, mul_assoc, conj_ofReal,
    mul_comm (⟪_, _⟫_𝕜), ← mul_assoc, ← ofReal_mul,
    ← Real.sqrt_mul (hT.toLinearMap.nonneg_eigenvalues rfl _),
    Real.sqrt_mul_self (hT.toLinearMap.nonneg_eigenvalues rfl _), mul_comm _ (⟪_, _⟫_𝕜),
    ← smul_eq_mul, smul_assoc, ← hT.isSymmetric.apply_eigenvectorBasis, ← map_smul, ← map_sum,
    ← OrthonormalBasis.repr_apply_apply, OrthonormalBasis.sum_repr, coe_coe]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
a : (i : Fin (Module.finrank 𝕜 E)) → E :=
  fun (i : Fin (Module.finrank 𝕜 E)) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑√(⋯.eigenvalues ⋯ i) : 𝕜)
      ((⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) i : E)
x : E
simp_rw :
  Eq (α := E) ((T : (a : E) → E) x : E)
    (∑ d : Fin (Module.finrank 𝕜 E),
        (((((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) (a d) : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) (a d) :
              E →L[𝕜] E) :
            (a : E) → E)
          x :
      E)
⊢ Eq (α := E) ((T : (a : E) → E) x : E)
    ((∑ i : Fin (Module.finrank 𝕜 E),
            (((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) (a i) : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) (a i) :
          (a : E) → E)
        x :
      E)
have simp_rw₁ : Eq (α := E) ((T : (a : E) → E) x : E) (∑ x_1 : Fin (Module.finrank 𝕜 E), ⟪a x_1, x⟫ • a x_1 : E)
Tactic: simp_rw [sum_apply, rankOne_apply, a, inner_smul_left, smul_smul, mul_assoc, conj_ofReal,
    mul_comm (⟪_, _⟫_𝕜), ← mul_assoc, ← ofReal_mul,
    ← Real.sqrt_mul (hT.toLinearMap.nonneg_eigenvalues rfl _),
    Real.sqrt_mul_self (hT.toLinearMap.nonneg_eigenvalues rfl _), mul_comm _ (⟪_, _⟫_𝕜),
    ← smul_eq_mul, smul_assoc, ← hT.isSymmetric.apply_eigenvectorBasis, ← map_smul, ← map_sum,
    ← OrthonormalBasis.repr_apply_apply, OrthonormalBasis.sum_repr, coe_coe]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
a : (i : Fin (Module.finrank 𝕜 E)) → E :=
  fun (i : Fin (Module.finrank 𝕜 E)) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑√(⋯.eigenvalues ⋯ i) : 𝕜)
      ((⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) i : E)
x : E
simp_rw :
  Eq (α := E) ((T : (a : E) → E) x : E)
    (∑ d : Fin (Module.finrank 𝕜 E),
        (((((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) (a d) : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) (a d) :
              E →L[𝕜] E) :
            (a : E) → E)
          x :
      E)
simp_rw₁ : Eq (α := E) ((T : (a : E) → E) x : E) (∑ x_1 : Fin (Module.finrank 𝕜 E), ⟪a x_1, x⟫ • a x_1 : E)
simp_rw₂ :
  Eq (α := E) ((T : (a : E) → E) x : E)
    (∑ x_1 : Fin (Module.finrank 𝕜 E),
        ⟪HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑√(⋯.eigenvalues ⋯ x_1) : 𝕜)
              ((⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) x_1 : E),
            x⟫ •
          HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑√(⋯.eigenvalues ⋯ x_1) : 𝕜)
            ((⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) x_1 : E) :
      E)
⊢ Eq (α := E) ((T : (a : E) → E) x : E)
    ((∑ i : Fin (Module.finrank 𝕜 E),
            (((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) (a i) : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) (a i) :
          (a : E) → E)
        x :
      E)
have simp_rw₃ : Eq (α := E) ((T : (a : E) → E) x : E)
  (∑ x_1 : Fin (Module.finrank 𝕜 E),
      HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑√(sorry.eigenvalues sorry x_1) : 𝕜) : 𝕜)
          ⟪(sorry.eigenvectorBasis sorry : (a : Fin (Module.finrank 𝕜 E)) → E) x_1, x⟫ •
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑√(sorry.eigenvalues sorry x_1) : 𝕜)
          ((sorry.eigenvectorBasis sorry : (a : Fin (Module.finrank 𝕜 E)) → E) x_1 : E) :
    E)
Tactic: simp_rw [sum_apply, rankOne_apply, a, inner_smul_left, smul_smul, mul_assoc, conj_ofReal,
    mul_comm (⟪_, _⟫_𝕜), ← mul_assoc, ← ofReal_mul,
    ← Real.sqrt_mul (hT.toLinearMap.nonneg_eigenvalues rfl _),
    Real.sqrt_mul_self (hT.toLinearMap.nonneg_eigenvalues rfl _), mul_comm _ (⟪_, _⟫_𝕜),
    ← smul_eq_mul, smul_assoc, ← hT.isSymmetric.apply_eigenvectorBasis, ← map_smul, ← map_sum,
    ← OrthonormalBasis.repr_apply_apply, OrthonormalBasis.sum_repr, coe_coe]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
a : (i : Fin (Module.finrank 𝕜 E)) → E :=
  fun (i : Fin (Module.finrank 𝕜 E)) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑√(⋯.eigenvalues ⋯ i) : 𝕜)
      ((⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) i : E)
x : E
simp_rw :
  Eq (α := E) ((T : (a : E) → E) x : E)
    (∑ d : Fin (Module.finrank 𝕜 E),
        (((((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) (a d) : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) (a d) :
              E →L[𝕜] E) :
            (a : E) → E)
          x :
      E)
simp_rw₁ : Eq (α := E) ((T : (a : E) → E) x : E) (∑ x_1 : Fin (Module.finrank 𝕜 E), ⟪a x_1, x⟫ • a x_1 : E)
simp_rw₂ :
  Eq (α := E) ((T : (a : E) → E) x : E)
    (∑ x_1 : Fin (Module.finrank 𝕜 E),
        ⟪HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑√(⋯.eigenvalues ⋯ x_1) : 𝕜)
              ((⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) x_1 : E),
            x⟫ •
          HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑√(⋯.eigenvalues ⋯ x_1) : 𝕜)
            ((⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) x_1 : E) :
      E)
simp_rw₃ :
  Eq (α := E) ((T : (a : E) → E) x : E)
    (∑ x_1 : Fin (Module.finrank 𝕜 E),
        HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑√(⋯.eigenvalues ⋯ x_1) : 𝕜) : 𝕜)
            ⟪(⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) x_1, x⟫ •
          HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑√(⋯.eigenvalues ⋯ x_1) : 𝕜)
            ((⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) x_1 : E) :
      E)
⊢ Eq (α := E) ((T : (a : E) → E) x : E)
    ((∑ i : Fin (Module.finrank 𝕜 E),
            (((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) (a i) : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) (a i) :
          (a : E) → E)
        x :
      E)
have simp_rw₄ : Eq (α := E) ((T : (a : E) → E) x : E)
  (∑ x_1 : Fin (Module.finrank 𝕜 E),
      HSMul.hSMul (β := E)
        (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑√(sorry.eigenvalues sorry x_1) : 𝕜) : 𝕜)
            ⟪(sorry.eigenvectorBasis sorry : (a : Fin (Module.finrank 𝕜 E)) → E) x_1, x⟫ *
          (↑√(sorry.eigenvalues sorry x_1) : 𝕜))
        ((sorry.eigenvectorBasis sorry : (a : Fin (Module.finrank 𝕜 E)) → E) x_1 : E) :
    E)
Tactic: simp_rw [sum_apply, rankOne_apply, a, inner_smul_left, smul_smul, mul_assoc, conj_ofReal,
    mul_comm (⟪_, _⟫_𝕜), ← mul_assoc, ← ofReal_mul,
    ← Real.sqrt_mul (hT.toLinearMap.nonneg_eigenvalues rfl _),
    Real.sqrt_mul_self (hT.toLinearMap.nonneg_eigenvalues rfl _), mul_comm _ (⟪_, _⟫_𝕜),
    ← smul_eq_mul, smul_assoc, ← hT.isSymmetric.apply_eigenvectorBasis, ← map_smul, ← map_sum,
    ← OrthonormalBasis.repr_apply_apply, OrthonormalBasis.sum_repr, coe_coe]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_4
inst_1 : Finite n
M : Matrix n n 𝕜
⊢ M.PosSemidef ↔ ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))
have have : ∀ (this : Fintype n), M.PosSemidef ↔ ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))
Tactic: have := Fintype.ofFinite n
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_4
inst_1 : Finite n
M : Matrix n n 𝕜
this : Fintype n
⊢ M.PosSemidef ↔ ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))
have rw : (∃ (m : ℕ) (u : Fin m → EuclideanSpace 𝕜 n),
    Eq (α := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      (((toContinuousLinearMap :
              (EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) ≃ₗ[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :
            (a : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
          ((toEuclideanLin : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) M) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      (∑ i : Fin m,
          (((rankOne 𝕜 :
                    (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L⋆[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
                  (u i) :
                EuclideanSpace 𝕜 n →L⋆[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :
              (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
            (u i) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)) ↔
  ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))
Tactic: rw [← isPositive_toEuclideanLin_iff, ← isPositive_toContinuousLinearMap_iff,
    isPositive_iff_eq_sum_rankOne]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_4
inst_1 : Finite n
M : Matrix n n 𝕜
this : Fintype n
⊢ (∃ (m : ℕ) (u : Fin m → EuclideanSpace 𝕜 n),
      Eq (α := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
        (((toContinuousLinearMap :
                (EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) ≃ₗ[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :
              (a : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
            ((toEuclideanLin : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) M) :
          EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
        (∑ i : Fin m,
            (((rankOne 𝕜 :
                      (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L⋆[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
                    (u i) :
                  EuclideanSpace 𝕜 n →L⋆[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :
                (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
              (u i) :
          EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)) ↔
    ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))
have simp_rw : (∃ (m : ℕ) (u : Fin m → EuclideanSpace 𝕜 n), M = ∑ x : Fin m, vecMulVec (u x).ofLp (star (u x).ofLp)) ↔
  ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))
Tactic: simp_rw [eq_comm, ← LinearEquiv.symm_apply_eq, coe_toContinuousLinearMap_symm,
    ContinuousLinearMap.coe_sum, map_sum, symm_toEuclideanLin_rankOne, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_4
inst_1 : Finite n
M : Matrix n n 𝕜
⊢ M.PosSemidef ↔ ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))
have have : ∀ (this : Fintype n), M.PosSemidef ↔ ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))
Tactic: classical
  have := Fintype.ofFinite n
  rw [← isPositive_toEuclideanLin_iff, ← isPositive_toContinuousLinearMap_iff,
    isPositive_iff_eq_sum_rankOne]
  simp_rw [eq_comm, ← LinearEquiv.symm_apply_eq, coe_toContinuousLinearMap_symm,
    ContinuousLinearMap.coe_sum, map_sum, symm_toEuclideanLin_rankOne, eq_comm]
  exact ⟨fun ⟨m, u, hu⟩ ↦ ⟨m, fun i ↦ (u i).ofLp, hu⟩,
    fun ⟨m, u, hu⟩ ↦ ⟨m, fun i ↦ WithLp.toLp 2 (u i), hu⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_4
inst_1 : Finite n
M : Matrix n n 𝕜
have have₁ have₂ :
  ∀ (this : Fintype n), M.PosSemidef ↔ ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))
⊢ M.PosSemidef ↔ ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))
have have₃ : ∀ (this : Fintype n),
  (∃ (m : ℕ) (u : Fin m → EuclideanSpace 𝕜 n),
      Eq (α := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
        (((toContinuousLinearMap :
                (EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) ≃ₗ[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :
              (a : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
            ((toEuclideanLin : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) M) :
          EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
        (∑ i : Fin m,
            (((rankOne 𝕜 :
                      (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L⋆[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
                    (u i) :
                  EuclideanSpace 𝕜 n →L⋆[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :
                (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
              (u i) :
          EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)) ↔
    ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))
Tactic: classical
  have := Fintype.ofFinite n
  rw [← isPositive_toEuclideanLin_iff, ← isPositive_toContinuousLinearMap_iff,
    isPositive_iff_eq_sum_rankOne]
  simp_rw [eq_comm, ← LinearEquiv.symm_apply_eq, coe_toContinuousLinearMap_symm,
    ContinuousLinearMap.coe_sum, map_sum, symm_toEuclideanLin_rankOne, eq_comm]
  exact ⟨fun ⟨m, u, hu⟩ ↦ ⟨m, fun i ↦ (u i).ofLp, hu⟩,
    fun ⟨m, u, hu⟩ ↦ ⟨m, fun i ↦ WithLp.toLp 2 (u i), hu⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_4
inst_1 : Finite n
M : Matrix n n 𝕜
have have₁ have₂ :
  ∀ (this : Fintype n), M.PosSemidef ↔ ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))
have₃ :
  ∀ (this : Fintype n),
    (∃ (m : ℕ) (u : Fin m → EuclideanSpace 𝕜 n),
        Eq (α := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
          (((toContinuousLinearMap :
                  (EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) ≃ₗ[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :
                (a : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
              ((toEuclideanLin : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) M) :
            EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
          (∑ i : Fin m,
              (((rankOne 𝕜 :
                        (a : EuclideanSpace 𝕜 n) →
                          EuclideanSpace 𝕜 n →L⋆[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
                      (u i) :
                    EuclideanSpace 𝕜 n →L⋆[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :
                  (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
                (u i) :
            EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)) ↔
      ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))
⊢ M.PosSemidef ↔ ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))
have have₄ : ∀ (this : Fintype n),
  (∃ (m : ℕ) (u : Fin m → EuclideanSpace 𝕜 n), M = ∑ x : Fin m, vecMulVec (u x).ofLp (star (u x).ofLp)) ↔
    ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))
Tactic: classical
  have := Fintype.ofFinite n
  rw [← isPositive_toEuclideanLin_iff, ← isPositive_toContinuousLinearMap_iff,
    isPositive_iff_eq_sum_rankOne]
  simp_rw [eq_comm, ← LinearEquiv.symm_apply_eq, coe_toContinuousLinearMap_symm,
    ContinuousLinearMap.coe_sum, map_sum, symm_toEuclideanLin_rankOne, eq_comm]
  exact ⟨fun ⟨m, u, hu⟩ ↦ ⟨m, fun i ↦ (u i).ofLp, hu⟩,
    fun ⟨m, u, hu⟩ ↦ ⟨m, fun i ↦ WithLp.toLp 2 (u i), hu⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.ProdL2 (goal)
Goal:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x y z : WithLp 2 (E × F)
⊢ ⟪(x + y).fst, z.fst⟫_𝕜 + ⟪(x + y).snd, z.snd⟫_𝕜 =
    ⟪x.fst, z.fst⟫_𝕜 + ⟪x.snd, z.snd⟫_𝕜 + (⟪y.fst, z.fst⟫_𝕜 + ⟪y.snd, z.snd⟫_𝕜)
have simp : ⟪x.fst, z.fst⟫_𝕜 + ⟪y.fst, z.fst⟫_𝕜 + (⟪x.snd, z.snd⟫_𝕜 + ⟪y.snd, z.snd⟫_𝕜) =
  ⟪x.fst, z.fst⟫_𝕜 + ⟪x.snd, z.snd⟫_𝕜 + (⟪y.fst, z.fst⟫_𝕜 + ⟪y.snd, z.snd⟫_𝕜)
Tactic: simp only [add_fst, add_snd, inner_add_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.ProdL2 (goal)
Goal:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x y : WithLp 2 (E × F)
r : 𝕜
⊢ ⟪(r • x).fst, y.fst⟫_𝕜 + ⟪(r • x).snd, y.snd⟫_𝕜 =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) (⟪x.fst, y.fst⟫_𝕜 + ⟪x.snd, y.snd⟫_𝕜)
have simp : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) ⟪x.fst, y.fst⟫_𝕜 +
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) ⟪x.snd, y.snd⟫_𝕜 =
  HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) (⟪x.fst, y.fst⟫_𝕜 + ⟪x.snd, y.snd⟫_𝕜)
Tactic: simp only [smul_fst, inner_smul_left, smul_snd]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.ProdL2 (goal)
Goal:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
v : OrthonormalBasis ι₁ 𝕜 E
w : OrthonormalBasis ι₂ 𝕜 F
⊢ Orthonormal 𝕜 (E := WithLp 2 (E × F)) (ι := ι₁ ⊕ ι₂)
    (⇑((v.toBasis.prod w.toBasis).map (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (E × F)))) :
      (a : ι₁ ⊕ ι₂) → WithLp 2 (E × F))
have left : ∀ (i : ι₁ ⊕ ι₂),
  norm (E := WithLp 2 (E × F))
      (((v.toBasis.prod w.toBasis).map (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (E × F))) :
            (a : ι₁ ⊕ ι₂) → WithLp 2 (E × F))
          i :
        WithLp 2 (E × F)) =
    1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.ProdL2 (goal)
Goal:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
v : OrthonormalBasis ι₁ 𝕜 E
w : OrthonormalBasis ι₂ 𝕜 F
left :
  ∀ (i : ι₁ ⊕ ι₂),
    norm (E := WithLp 2 (E × F))
        (((v.toBasis.prod w.toBasis).map (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (E × F))) :
              (a : ι₁ ⊕ ι₂) → WithLp 2 (E × F))
            i :
          WithLp 2 (E × F)) =
      1
⊢ Orthonormal 𝕜 (E := WithLp 2 (E × F)) (ι := ι₁ ⊕ ι₂)
    (⇑((v.toBasis.prod w.toBasis).map (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (E × F)))) :
      (a : ι₁ ⊕ ι₂) → WithLp 2 (E × F))
have right : Pairwise fun (i j : ι₁ ⊕ ι₂) ↦
  inner 𝕜 (E := WithLp 2 (E × F))
      (((v.toBasis.prod w.toBasis).map (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (E × F))) :
            (a : ι₁ ⊕ ι₂) → WithLp 2 (E × F))
          i :
        WithLp 2 (E × F))
      (((v.toBasis.prod w.toBasis).map (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (E × F))) :
            (a : ι₁ ⊕ ι₂) → WithLp 2 (E × F))
          j :
        WithLp 2 (E × F)) =
    0
Tactic: constructor