awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
refine :
  ∀ (hA : A.IsHermitian) (x : n → 𝕜),
    LE.le (α := ℝ) (0 : ℝ)
        ((re : (a : 𝕜) → ℝ)
            (star
                (WithLp.ofLp (p := 2)
                  (((↑(EuclideanSpace.equiv n 𝕜) : EuclideanSpace 𝕜 n ≃ₗ[𝕜] n → 𝕜).toAddEquiv.symm :
                      (a : n → 𝕜) → EuclideanSpace 𝕜 n)
                    x)) ⬝ᵥ
              A.mulVec
                (WithLp.ofLp (p := 2)
                  (((↑(EuclideanSpace.equiv n 𝕜) : EuclideanSpace 𝕜 n ≃ₗ[𝕜] n → 𝕜).toAddEquiv.symm :
                      (a : n → 𝕜) → EuclideanSpace 𝕜 n)
                    x))) :
          ℝ) ↔
      LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) (star x ⬝ᵥ A.mulVec x) : ℝ) ∧
        Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) (star x ⬝ᵥ A.mulVec x) : ℝ) (0 : ℝ)
⊢ A.IsHermitian →
    ((∀ (x : EuclideanSpace 𝕜 n), LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) (star x.ofLp ⬝ᵥ A.mulVec x.ofLp) : ℝ)) ↔
      ∀ (x : n → 𝕜),
        LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) (star x ⬝ᵥ A.mulVec x) : ℝ) ∧
          Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) (star x ⬝ᵥ A.mulVec x) : ℝ) (0 : ℝ))

Tactic:
refine fun hA ↦ (EuclideanSpace.equiv n 𝕜).forall_congr' fun x ↦ ?_

Premises used: ContinuousLinearEquiv.toLinearEquiv, LinearEquiv.toAddEquiv, Equiv.forall_congr', AddEquiv.toEquiv, EuclideanSpace.equiv
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
x : n → 𝕜
⊢ LE.le (α := ℝ) (0 : ℝ)
      ((re : (a : 𝕜) → ℝ)
          (star
              (WithLp.ofLp (p := 2)
                (((↑(EuclideanSpace.equiv n 𝕜) : EuclideanSpace 𝕜 n ≃ₗ[𝕜] n → 𝕜).toAddEquiv.symm :
                    (a : n → 𝕜) → EuclideanSpace 𝕜 n)
                  x)) ⬝ᵥ
            A.mulVec
              (WithLp.ofLp (p := 2)
                (((↑(EuclideanSpace.equiv n 𝕜) : EuclideanSpace 𝕜 n ≃ₗ[𝕜] n → 𝕜).toAddEquiv.symm :
                    (a : n → 𝕜) → EuclideanSpace 𝕜 n)
                  x))) :
        ℝ) ↔
    LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) (star x ⬝ᵥ A.mulVec x) : ℝ) ∧
      Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) (star x ⬝ᵥ A.mulVec x) : ℝ) (0 : ℝ)

Tactic:
simp [hA.im_star_dotProduct_mulVec_self]

Premises used: Matrix.IsHermitian.im_star_dotProduct_mulVec_self
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Fintype ι
inst_4 : DecidableEq ι
A : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
rw :
  IsPositive (𝕜 := 𝕜) (E := EuclideanSpace 𝕜 ι)
      ((Matrix.toEuclideanLin : (a : Matrix ι ι 𝕜) → EuclideanSpace 𝕜 ι →ₗ[𝕜] EuclideanSpace 𝕜 ι)
        ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) A)) ↔
    A.IsPositive
⊢ Matrix.PosSemidef.{u_4, u_1} (n := ι) (R := 𝕜) ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) A) ↔
    A.IsPositive

Tactic:
rw [← Matrix.isPositive_toEuclideanLin_iff]

Premises used: Matrix.isPositive_toEuclideanLin_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Fintype ι
inst_4 : DecidableEq ι
A : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
⊢ ((↑b.repr.toLinearEquiv : E →ₗ[𝕜] EuclideanSpace 𝕜 ι) ∘ₗ
        A ∘ₗ (↑b.repr.symm.toLinearEquiv : EuclideanSpace 𝕜 ι →ₗ[𝕜] E)).IsPositive ↔
    A.IsPositive

Tactic:
isPositive_linearIsometryEquiv_conj_iff b.repr

Premises used: OrthonormalBasis.repr, LinearMap.isPositive_linearIsometryEquiv_conj_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Fintype ι
inst_4 : DecidableEq ι
A : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
h :
  (Matrix.toEuclideanLin : (a : Matrix ι ι 𝕜) → EuclideanSpace 𝕜 ι →ₗ[𝕜] EuclideanSpace 𝕜 ι)
      ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) A) =
    (↑b.repr.toLinearEquiv : E →ₗ[𝕜] EuclideanSpace 𝕜 ι) ∘ₗ
      A ∘ₗ (↑b.repr.symm.toLinearEquiv : EuclideanSpace 𝕜 ι →ₗ[𝕜] E)
⊢ IsPositive (𝕜 := 𝕜) (E := EuclideanSpace 𝕜 ι)
      ((Matrix.toEuclideanLin : (a : Matrix ι ι 𝕜) → EuclideanSpace 𝕜 ι →ₗ[𝕜] EuclideanSpace 𝕜 ι)
        ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) A)) ↔
    A.IsPositive

Tactic:
convert! isPositive_linearIsometryEquiv_conj_iff b.repr

Premises used: OrthonormalBasis.repr, LinearMap.isPositive_linearIsometryEquiv_conj_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Fintype ι
inst_4 : DecidableEq ι
A : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
h :
  ∀ (x : EuclideanSpace 𝕜 ι) (i : ι),
    Eq.{u_1 + 1} (α := 𝕜)
      (WithLp.ofLp (p := 2)
        ((((Matrix.toEuclideanLin : (a : Matrix ι ι 𝕜) → EuclideanSpace 𝕜 ι →ₗ[𝕜] EuclideanSpace 𝕜 ι)
                ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) A) :
              EuclideanSpace 𝕜 ι →ₗ[𝕜] EuclideanSpace 𝕜 ι) :
            (a : EuclideanSpace 𝕜 ι) → EuclideanSpace 𝕜 ι)
          x)
        i)
      (WithLp.ofLp (p := 2)
        (((↑b.repr.toLinearEquiv : E →ₗ[𝕜] EuclideanSpace 𝕜 ι) ∘ₗ
              A ∘ₗ (↑b.repr.symm.toLinearEquiv : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) :
            (a : EuclideanSpace 𝕜 ι) → EuclideanSpace 𝕜 ι)
          x)
        i)
⊢ (Matrix.toEuclideanLin : (a : Matrix ι ι 𝕜) → EuclideanSpace 𝕜 ι →ₗ[𝕜] EuclideanSpace 𝕜 ι)
      ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) A) =
    (↑b.repr.toLinearEquiv : E →ₗ[𝕜] EuclideanSpace 𝕜 ι) ∘ₗ
      A ∘ₗ (↑b.repr.symm.toLinearEquiv : EuclideanSpace 𝕜 ι →ₗ[𝕜] E)

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Fintype ι
inst_4 : DecidableEq ι
A : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
x : EuclideanSpace 𝕜 ι
i : ι
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (WithLp.ofLp (p := 2)
      ((((Matrix.toEuclideanLin : (a : Matrix ι ι 𝕜) → EuclideanSpace 𝕜 ι →ₗ[𝕜] EuclideanSpace 𝕜 ι)
              ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) A) :
            EuclideanSpace 𝕜 ι →ₗ[𝕜] EuclideanSpace 𝕜 ι) :
          (a : EuclideanSpace 𝕜 ι) → EuclideanSpace 𝕜 ι)
        x)
      i)
    (WithLp.ofLp (p := 2)
      (((↑b.repr.toLinearEquiv : E →ₗ[𝕜] EuclideanSpace 𝕜 ι) ∘ₗ
            A ∘ₗ (↑b.repr.symm.toLinearEquiv : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) :
          (a : EuclideanSpace 𝕜 ι) → EuclideanSpace 𝕜 ι)
        x)
      i)

Tactic:
simp [LinearMap.toMatrix]

Premises used: LinearMap.toMatrix
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
⊢ p.IsPositive

Tactic:
hp.isIdempotentElem.isPositive_iff_isSymmetric.mpr hp.isSymmetric

Premises used: Iff.mpr, LinearMap.IsSymmetricProjection.isIdempotentElem, LinearMap.IsSymmetricProjection.isSymmetric, LinearMap.IsIdempotentElem.isPositive_iff_isSymmetric
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) q
⊢ p ≤ q ↔ p.range ≤ q.range

Tactic:
⟨fun ⟨h1, h2⟩ a ha ↦ ?_, fun hpq ↦ (hp.sub_of_range_le_range hq hpq).isPositive⟩

Premises used: LinearMap.IsSymmetricProjection.isPositive, LinearMap.IsSymmetricProjection.sub_of_range_le_range, Membership.mem, LinearMap.range, _private.0.LinearMap.IsSymmetricProjection.le_iff_range_le_range.match_1, Iff.intro
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) q
refine :
  p ≤ q →
    ∀ (a : E) (ha : a ∈ p.range) (h1 : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (q - p))
      (h2 : ∀ (x : E), LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(q - p : (a : E) → E) x, x⟫ : ℝ)), a ∈ q.range
⊢ p ≤ q ↔ p.range ≤ q.range

Tactic:
refine ⟨fun ⟨h1, h2⟩ a ha ↦ ?_, fun hpq ↦ (hp.sub_of_range_le_range hq hpq).isPositive⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) q
h : p ≤ q
a : E
ha : a ∈ p.range
h1 : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (q - p)
h2 : ∀ (x : E), LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(q - p : (a : E) → E) x, x⟫ : ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(q - p : (a : E) → E) a, a⟫ : ℝ)

Tactic:
specialize h2 a
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) q
h : p ≤ q
a : E
ha : a ∈ p.range
h1 : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (q - p)
h2 : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(q - p : (a : E) → E) a, a⟫ : ℝ)
T : E →ₗ[𝕜] E
hT : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
rw : ((re : (a : 𝕜) → ℝ) ⟪(T * T : (a : E) → E) a, a⟫ : ℝ)
| ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) a, a⟫ : ℝ)

Tactic:
rw [← hT.isIdempotentElem]

Premises used: LinearMap.IsSymmetricProjection.isIdempotentElem
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) q
h : p ≤ q
a : E
ha : a ∈ p.range
h1 : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (q - p)
h2 : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(q - p : (a : E) → E) a, a⟫ : ℝ)
T : E →ₗ[𝕜] E
hT : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
conv_lhs :
  (re : (a : 𝕜) → ℝ) ⟪(T * T : (a : E) → E) a, a⟫ = HPow.hPow (β := ℕ) (norm (E := E) ((T : (a : E) → E) a : E)) 2
⊢ (re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) a, a⟫ = HPow.hPow (β := ℕ) (norm (E := E) ((T : (a : E) → E) a : E)) 2

Tactic:
conv_lhs => rw [← hT.isIdempotentElem]

Premises used: LinearMap.IsSymmetricProjection.isIdempotentElem
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) q
h : p ≤ q
a : E
ha : a ∈ p.range
h1 : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (q - p)
h2 : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(q - p : (a : E) → E) a, a⟫ : ℝ)
T : E →ₗ[𝕜] E
hT : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
rw :
  (re : (a : 𝕜) → ℝ) (inner 𝕜 (E := E) ((T : (a : E) → E) a : E) ((T : (a : E) → E) a : E)) =
    HPow.hPow (β := ℕ) (norm (E := E) ((T : (a : E) → E) a : E)) 2
⊢ (re : (a : 𝕜) → ℝ) ⟪(T * T : (a : E) → E) a, a⟫ = HPow.hPow (β := ℕ) (norm (E := E) ((T : (a : E) → E) a : E)) 2

Tactic:
rw [Module.End.mul_apply, hT.isSymmetric]

Premises used: LinearMap.IsSymmetricProjection.isSymmetric, Module.End.mul_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) q
h : p ≤ q
a : E
ha : a ∈ p.range
h1 : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (q - p)
h2 : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(q - p : (a : E) → E) a, a⟫ : ℝ)
T : E →ₗ[𝕜] E
hT : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
⊢ (re : (a : 𝕜) → ℝ) (inner 𝕜 (E := E) ((T : (a : E) → E) a : E) ((T : (a : E) → E) a : E)) =
    HPow.hPow (β := ℕ) (norm (E := E) ((T : (a : E) → E) a : E)) 2

Tactic:
inner_self_eq_norm_sq _

Premises used: inner_self_eq_norm_sq
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) q
h : p ≤ q
a : E
ha : a ∈ p.range
h1 : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (q - p)
h2 : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(q - p : (a : E) → E) a, a⟫ : ℝ)
T : E →ₗ[𝕜] E
hT : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
⊢ (re : (a : 𝕜) → ℝ) (inner 𝕜 (E := E) ((T : (a : E) → E) a : E) ((T : (a : E) → E) a : E)) =
    HPow.hPow (β := ℕ) (norm (E := E) ((T : (a : E) → E) a : E)) 2

Tactic:
exact inner_self_eq_norm_sq _

Premises used: inner_self_eq_norm_sq
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) q
h : p ≤ q
a : E
ha : a ∈ p.range
h1 : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (q - p)
h2 : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(q - p : (a : E) → E) a, a⟫ : ℝ)
⊢ ∀ {T : E →ₗ[𝕜] E} (hT : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) T),
    (re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) a, a⟫ = HPow.hPow (β := ℕ) (norm (E := E) ((T : (a : E) → E) a : E)) 2

Tactic:
have hh {T : E →ₗ[𝕜] E} (hT : T.IsSymmetricProjection) : RCLike.re ⟪T a, a⟫_𝕜 = ‖T a‖ ^ 2 := by
    conv_lhs => rw [← hT.isIdempotentElem]
    rw [Module.End.mul_apply, hT.isSymmetric]
    exact inner_self_eq_norm_sq _
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) q
h : p ≤ q
a : E
ha : a ∈ p.range
h1 : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (q - p)
h2 : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(q - p : (a : E) → E) a, a⟫ : ℝ)
hh :
  ∀ {T : E →ₗ[𝕜] E} (hT : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) T),
    (re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) a, a⟫ = HPow.hPow (β := ℕ) (norm (E := E) ((T : (a : E) → E) a : E)) 2
⊢ ‖a‖ ≤ norm (E := E) ((q : (a : E) → E) a : E)

Tactic:
simp_rw [sub_apply, inner_sub_left, map_sub, hh hq, hh hp,
    hp.isIdempotentElem.mem_range_iff.mp ha, sub_nonneg, sq_le_sq, abs_norm] at h2

Premises used: map_sub, LinearMap.IsSymmetricProjection.isIdempotentElem, sq_le_sq, inner_sub_left, LinearMap.IsIdempotentElem.mem_range_iff, Iff.mp, LinearMap.sub_apply, abs_norm, sub_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) q
h : p ≤ q
a : E
ha : a ∈ p.range
h1 : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (q - p)
hh :
  ∀ {T : E →ₗ[𝕜] E} (hT : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) T),
    (re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) a, a⟫ = HPow.hPow (β := ℕ) (norm (E := E) ((T : (a : E) → E) a : E)) 2
h2 : ‖a‖ ≤ norm (E := E) ((q : (a : E) → E) a : E)
obtain :
  ∀ (U : Submodule 𝕜 E) (w : U.HasOrthogonalProjection)
    (hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑U.starProjection : E →ₗ[𝕜] E)),
    p ≤ (↑U.starProjection : E →ₗ[𝕜] E) →
      ∀ (h1 : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) ((↑U.starProjection : E →ₗ[𝕜] E) - p))
        (h2 : ‖a‖ ≤ norm (E := E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) a : E)),
        a ∈ (↑U.starProjection : E →ₗ[𝕜] E).range
⊢ a ∈ q.range

Tactic:
obtain ⟨U, _, rfl⟩ := isSymmetricProjection_iff_eq_coe_starProjection.mp hq

Premises used: Iff.mp, LinearMap.isSymmetricProjection_iff_eq_coe_starProjection, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
a : E
ha : a ∈ p.range
hh :
  ∀ {T : E →ₗ[𝕜] E} (hT : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) T),
    (re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) a, a⟫ = HPow.hPow (β := ℕ) (norm (E := E) ((T : (a : E) → E) a : E)) 2
U : Submodule 𝕜 E
w : U.HasOrthogonalProjection
hq : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑U.starProjection : E →ₗ[𝕜] E)
h : p ≤ (↑U.starProjection : E →ₗ[𝕜] E)
h1 : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) ((↑U.starProjection : E →ₗ[𝕜] E) - p)
h2 : ‖a‖ ≤ norm (E := E) (((↑U.starProjection : E →ₗ[𝕜] E) : (a : E) → E) a : E)
⊢ a ∈ (↑U.starProjection : E →ₗ[𝕜] E).range

Tactic:
simpa [Submodule.toLinearMap_starProjection_eq_isComplProjection] using
    U.mem_iff_norm_starProjection _ |>.mpr <| le_antisymm (U.norm_starProjection_apply_le a) h2

Premises used: Iff.mpr, Submodule.norm_starProjection_apply_le, Submodule.toLinearMap_starProjection_eq_isComplProjection, le_antisymm, Submodule.mem_iff_norm_starProjection
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsPositive
unfold :
  LE.le.{u_1} (α := 𝕜) (0 : 𝕜)
    ((if H : ∃ (s : Finset E), Nonempty (Module.Basis (↥s) 𝕜 E) then traceAux 𝕜 ⋯.some else 0 : (a : E →ₗ[𝕜] E) → 𝕜) f :
      𝕜)
⊢ LE.le.{u_1} (α := 𝕜) (0 : 𝕜) ((trace 𝕜 E : (a : E →ₗ[𝕜] E) → 𝕜) f : 𝕜)

Tactic:
unfold trace

Premises used: LinearMap.trace
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsPositive
pos :
  ∀ (h : ∃ (s : Finset E), Nonempty (Module.Basis (↥s) 𝕜 E)),
    LE.le.{u_1} (α := 𝕜) (0 : 𝕜) ((traceAux 𝕜 ⋯.some : (a : E →ₗ[𝕜] E) → 𝕜) f : 𝕜)
neg :
  ∀ (h : ¬∃ (s : Finset E), Nonempty (Module.Basis (↥s) 𝕜 E)),
    LE.le.{u_1} (α := 𝕜) (0 : 𝕜) ((0 : (a : E →ₗ[𝕜] E) → 𝕜) f : 𝕜)
⊢ LE.le.{u_1} (α := 𝕜) (0 : 𝕜)
    ((if H : ∃ (s : Finset E), Nonempty (Module.Basis (↥s) 𝕜 E) then traceAux 𝕜 ⋯.some else 0 : (a : E →ₗ[𝕜] E) → 𝕜) f :
      𝕜)

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsPositive
h : ∃ (s : Finset E), Nonempty (Module.Basis (↥s) 𝕜 E)
⊢ FiniteDimensional 𝕜 E

Tactic:
have : FiniteDimensional 𝕜 E := Module.Finite.of_basis h.choose_spec.some
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsPositive
h : ∃ (s : Finset E), Nonempty (Module.Basis (↥s) 𝕜 E)
this : FiniteDimensional 𝕜 E
pos :
  LE.le.{u_1} (α := 𝕜) (0 : 𝕜)
    ((traceAux 𝕜 (OrthonormalBasis.toBasis (stdOrthonormalBasis 𝕜 E)) : (a : E →ₗ[𝕜] E) → 𝕜) f : 𝕜)
⊢ LE.le.{u_1} (α := 𝕜) (0 : 𝕜) ((traceAux 𝕜 ⋯.some : (a : E →ₗ[𝕜] E) → 𝕜) f : 𝕜)

Tactic:
simp_rw [traceAux_eq 𝕜 _ (stdOrthonormalBasis 𝕜 E).toBasis]

Premises used: OrthonormalBasis.toBasis, LinearMap.traceAux_eq, stdOrthonormalBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsPositive
h : ∃ (s : Finset E), Nonempty (Module.Basis (↥s) 𝕜 E)
this : FiniteDimensional 𝕜 E
⊢ LE.le.{u_1} (α := 𝕜) (0 : 𝕜)
    ((traceAux 𝕜 (OrthonormalBasis.toBasis (stdOrthonormalBasis 𝕜 E)) : (a : E →ₗ[𝕜] E) → 𝕜) f : 𝕜)

Tactic:
posSemidef_toMatrix_iff (stdOrthonormalBasis 𝕜 E) |>.mpr hf |>.trace_nonneg

Premises used: Multiset.sum, Iff.mpr, Matrix.diag, Multiset.foldr, Matrix.trace, Matrix.PosSemidef.trace_nonneg, LinearMap.posSemidef_toMatrix_iff, Finset.sum, stdOrthonormalBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsPositive
h : ∃ (s : Finset E), Nonempty (Module.Basis (↥s) 𝕜 E)
this : FiniteDimensional 𝕜 E
⊢ LE.le.{u_1} (α := 𝕜) (0 : 𝕜)
    ((traceAux 𝕜 (OrthonormalBasis.toBasis (stdOrthonormalBasis 𝕜 E)) : (a : E →ₗ[𝕜] E) → 𝕜) f : 𝕜)

Tactic:
exact posSemidef_toMatrix_iff (stdOrthonormalBasis 𝕜 E) |>.mpr hf |>.trace_nonneg

Premises used: Iff.mpr, Matrix.PosSemidef.trace_nonneg, LinearMap.posSemidef_toMatrix_iff, stdOrthonormalBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsPositive
h : ∃ (s : Finset E), Nonempty (Module.Basis (↥s) 𝕜 E)
this : FiniteDimensional 𝕜 E
pos :
  LE.le.{u_1} (α := 𝕜) (0 : 𝕜)
    ((traceAux 𝕜 (OrthonormalBasis.toBasis (stdOrthonormalBasis 𝕜 E)) : (a : E →ₗ[𝕜] E) → 𝕜) f : 𝕜)
⊢ LE.le.{u_1} (α := 𝕜) (0 : 𝕜) ((traceAux 𝕜 ⋯.some : (a : E →ₗ[𝕜] E) → 𝕜) f : 𝕜)

Tactic:
classical
    simp_rw [traceAux_eq 𝕜 _ (stdOrthonormalBasis 𝕜 E).toBasis]
    exact posSemidef_toMatrix_iff (stdOrthonormalBasis 𝕜 E) |>.mpr hf |>.trace_nonneg

Premises used: Iff.mpr, Matrix.PosSemidef.trace_nonneg, LinearMap.posSemidef_toMatrix_iff, OrthonormalBasis.toBasis, LinearMap.traceAux_eq, stdOrthonormalBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsPositive
h : ¬∃ (s : Finset E), Nonempty (Module.Basis (↥s) 𝕜 E)
⊢ LE.le.{u_1} (α := 𝕜) (0 : 𝕜) ((0 : (a : E →ₗ[𝕜] E) → 𝕜) f : 𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (E →ₗ[𝕜] E) 𝕜)
    (PositiveLinearMap.toLinearMap (tracePositiveLinearMap 𝕜 E)) (trace 𝕜 E)

Tactic:
rfl

Premises used: LinearMap.trace, dite, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E →ₗ[𝕜] E
⊢ Eq.{u_1 + 1} (α := 𝕜) ((tracePositiveLinearMap 𝕜 E : (a : E →ₗ[𝕜] E) → 𝕜) x : 𝕜)
    ((trace 𝕜 E : (a : E →ₗ[𝕜] E) → 𝕜) x : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
⊢ T.IsPositive ↔ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E) ∧ ∀ (x : E), 0 ≤ T.reApplyInnerSelf x

Tactic:
Iff.rfl

Premises used: Iff.rfl, ContinuousLinearMap.IsPositive
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
T : E →L[𝕜] E
⊢ T.IsPositive ↔ IsSelfAdjoint T ∧ ∀ (x : E), 0 ≤ T.reApplyInnerSelf x

Tactic:
simp [IsPositive, isSelfAdjoint_iff_isSymmetric, LinearMap.IsSymmetric]

Premises used: ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric, ContinuousLinearMap.IsPositive, LinearMap.IsSymmetric
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
⊢ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)

Tactic:
hT.1

Premises used: And.left