awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E_1 : Type u_4
inst_1 : NormedAddCommGroup E_1
inst_2 : InnerProductSpace 𝕜 E_1
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
V : Type u_7
inst_8 : NormedAddCommGroup V
inst_9 : InnerProductSpace 𝕜 V
inst_10 : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L_1 L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank.{u_3, u_7} 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
E : ↥Sᗮ ≃ₗᵢ[𝕜] ↥LSᗮ
L3 : ↥Sᗮ →ₗᵢ[𝕜] V := LSᗮ.subtypeₗᵢ.comp E.toLinearIsometry
this_1 : CompleteSpace.{u_7} ↥S
this : CompleteSpace V
p1 : V →ₗ[𝕜] ↥S := (↑S.orthogonalProjection : V →ₗ[𝕜] ↥S)
p2 : V →ₗ[𝕜] ↥Sᗮ := (↑Sᗮ.orthogonalProjection : V →ₗ[𝕜] ↥Sᗮ)
M : V →ₗ[𝕜] V := L.toLinearMap ∘ₗ p1 + L3.toLinearMap ∘ₗ p2
M_norm_map : ∀ (x : V), Norm.norm (E := V) ((M : (a : V) → V) x : V) = ‖x‖
⊢ V →ₗᵢ[𝕜] V

Tactic:
exact
    { toLinearMap := M
      norm_map' := M_norm_map }
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
V : Type u_7
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L : ↥S →ₗᵢ[𝕜] V
s : ↥S
simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Eq (α := V) ((L.extend : (a : V) → V) (↑s : V) : V) ((L : (a : ↥S) → V) s : V)

Tactic:
simp only [LinearIsometry.extend, ← LinearIsometry.coe_toLinearMap]

Premises used: LinearIsometry.coe_toLinearMap, LinearIsometry.extend
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
V : Type u_7
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L : ↥S →ₗᵢ[𝕜] V
s : ↥S
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [add_eq_left, LinearIsometry.coe_toLinearMap,
    LinearIsometryEquiv.coe_toLinearIsometry, LinearIsometry.coe_comp, Function.comp_apply,
    orthogonalProjection_mem_subspace_eq_self, LinearMap.coe_comp, ContinuousLinearMap.coe_coe,
    Submodule.coe_subtype, LinearMap.add_apply, Submodule.coe_eq_zero,
    LinearIsometryEquiv.map_eq_zero_iff, Submodule.coe_subtypeₗᵢ,
    orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, Submodule.orthogonal_orthogonal,
    Submodule.coe_mem]

Premises used: LinearIsometry.coe_toLinearMap, Submodule.orthogonalProjection_mem_subspace_eq_self, Submodule.orthogonal_orthogonal, LinearMap.add_apply, Submodule.orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, ContinuousLinearMap.coe_coe, Submodule.coe_mem, Submodule.coe_subtypeₗᵢ, LinearIsometryEquiv.coe_toLinearIsometry, add_eq_left, LinearMap.coe_comp, LinearIsometry.coe_comp, LinearIsometryEquiv.map_eq_zero_iff, Submodule.coe_eq_zero, Submodule.coe_subtype, Function.comp_apply
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
m : Type u_7
n : Type u_8
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix m n 𝕜
x : n → 𝕜
⊢ Eq (α := EuclideanSpace 𝕜 m)
    ((((toEuclideanLin : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) A :
            EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) :
          (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 m)
        (toLp 2 x) :
      EuclideanSpace 𝕜 m)
    (toLp 2 ((((toLin' : (a : Matrix m n 𝕜) → (n → 𝕜) →ₗ[𝕜] m → 𝕜) A : (n → 𝕜) →ₗ[𝕜] m → 𝕜) : (a : n → 𝕜) → m → 𝕜) x) :
      WithLp 2 (m → 𝕜))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
m : Type u_7
n : Type u_8
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix m n 𝕜
x : EuclideanSpace 𝕜 n
⊢ Eq (α := (i : m) → (fun (x : m) ↦ 𝕜) i)
    (ofLp (p := 2)
        ((((toEuclideanLin : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) A :
              EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) :
            (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 m)
          x) :
      (i : m) → (fun (x : m) ↦ 𝕜) i)
    ((((toLin' : (a : Matrix m n 𝕜) → (n → 𝕜) →ₗ[𝕜] m → 𝕜) A : (n → 𝕜) →ₗ[𝕜] m → 𝕜) : (a : n → 𝕜) → m → 𝕜) x.ofLp :
      m → 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
m : Type u_7
n : Type u_8
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix m n 𝕜
v : EuclideanSpace 𝕜 n
⊢ Eq (α := EuclideanSpace 𝕜 m)
    ((((toEuclideanLin : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) M :
            EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) :
          (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 m)
        v :
      EuclideanSpace 𝕜 m)
    (toLp 2 (M *ᵥ v.ofLp) : WithLp 2 (m → 𝕜))

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.mulVec, Finset.sum, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
m : Type u_7
n : Type u_8
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix m n 𝕜
v : EuclideanSpace 𝕜 n
⊢ ofLp (p := 2)
      ((((toEuclideanLin : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) M :
            EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) :
          (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 m)
        v) =
    M *ᵥ v.ofLp

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.mulVec, Finset.sum, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
m : Type u_7
n : Type u_8
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix m n 𝕜
v : n → 𝕜
⊢ Eq (α := EuclideanSpace 𝕜 m)
    ((((toEuclideanLin : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) M :
            EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) :
          (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 m)
        (toLp 2 v) :
      EuclideanSpace 𝕜 m)
    (toLp 2 (M *ᵥ v) : WithLp 2 (m → 𝕜))

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.mulVec, Finset.sum, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
m : Type u_7
n : Type u_8
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : Finite m
⊢ Eq (α := Matrix m n 𝕜 ≃ₗ[𝕜] EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) toEuclideanLin
    (toLin (PiLp.basisFun 2 𝕜 n) (PiLp.basisFun 2 𝕜 m))

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Matrix.toLin, LinearEquiv.symm, Function.update, dotProduct, Pi.single, dite, Matrix.mulVec, LinearEquiv.trans, Finset.sum, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
m : Type u_7
n : Type u_8
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : Fintype m
⊢ Eq (α := Matrix m n 𝕜 ≃ₗ[𝕜] EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) toEuclideanLin
    (toLin (OrthonormalBasis.toBasis (basisFun n 𝕜)) (OrthonormalBasis.toBasis (basisFun m 𝕜)))

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Matrix.toLin, LinearEquiv.symm, Function.update, dotProduct, Pi.single, dite, Matrix.mulVec, LinearEquiv.trans, Finset.sum, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
m : Type u_7
n : Type u_8
inst_1 : Fintype n
A B : Matrix m n 𝕜
i j : m
⊢ inner 𝕜 (E := WithLp 2 (n → 𝕜)) (toLp 2 (A i)) (toLp 2 (B j)) = (B * Aᴴ) j i

Tactic:
simp [PiLp.inner_apply, dotProduct, mul_apply']

Premises used: Matrix.mul_apply', dotProduct, PiLp.inner_apply
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
m : Type u_7
n : Type u_8
inst_1 : Fintype m
A B : Matrix m n 𝕜
i j : n
⊢ inner 𝕜 (E := WithLp 2 (m → 𝕜)) (toLp 2 (Aᵀ i)) (toLp 2 (Bᵀ j)) = (Aᴴ * B) i j

Tactic:
simp [PiLp.inner_apply, dotProduct, mul_apply', mul_comm]

Premises used: Matrix.mul_apply', dotProduct, mul_comm, PiLp.inner_apply
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
m : Type u_7
n : Type u_8
inst_3 : Fintype n
inst_4 : DecidableEq n
inst_5 : Fintype m
b : OrthonormalBasis n 𝕜 E
b₂ : OrthonormalBasis m 𝕜 𝕜
x : E
a :
  ∀ (i : m) (j : n),
    Eq.{u_3 + 1} (α := 𝕜)
      ((toMatrix b.toBasis b₂.toBasis : (a : E →ₗ[𝕜] 𝕜) → Matrix m n 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) x) i j : 𝕜)
      (vecMulVec (star (⇑b₂ : (a : m) → 𝕜)) (star (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 n) x))) i j : 𝕜)
⊢ Eq (α := Matrix m n 𝕜)
    ((toMatrix b.toBasis b₂.toBasis : (a : E →ₗ[𝕜] 𝕜) → Matrix m n 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) x) :
      Matrix m n 𝕜)
    (vecMulVec (star (⇑b₂ : (a : m) → 𝕜)) (star (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 n) x))) :
      Matrix m n 𝕜)

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
m : Type u_7
n : Type u_8
inst_3 : Fintype n
inst_4 : DecidableEq n
inst_5 : Fintype m
b : OrthonormalBasis n 𝕜 E
b₂ : OrthonormalBasis m 𝕜 𝕜
x : E
i : m
j : n
⊢ Eq.{u_3 + 1} (α := 𝕜)
    ((toMatrix b.toBasis b₂.toBasis : (a : E →ₗ[𝕜] 𝕜) → Matrix m n 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) x) i j : 𝕜)
    (vecMulVec (star (⇑b₂ : (a : m) → 𝕜)) (star (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 n) x))) i j : 𝕜)

Tactic:
simp [LinearMap.toMatrix_apply, vecMulVec_apply, OrthonormalBasis.repr_apply_apply, mul_comm]

Premises used: OrthonormalBasis.repr_apply_apply, Matrix.vecMulVec_apply, mul_comm, LinearMap.toMatrix_apply
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_7
E : Type u_8
F : Type u_9
ι : Type u_10
ι' : Type u_11
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : Finite ι
inst_6 : Fintype ι'
inst_7 : DecidableEq ι'
x : E
y : F
b : Basis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 F
have :
  ∀ (this : Fintype ι),
    Eq (α := Matrix ι ι' 𝕜)
      ((toMatrix b'.toBasis b : (a : F →ₗ[𝕜] E) → Matrix ι ι' 𝕜)
          (↑((((rankOne 𝕜 : (a : E) → F →L⋆[𝕜] F →L[𝕜] E) x : F →L⋆[𝕜] F →L[𝕜] E) : (a : F) → F →L[𝕜] E) y) :
            F →ₗ[𝕜] E) :
        Matrix ι ι' 𝕜)
      (Matrix.vecMulVec (⇑((b.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : (a : ι) → 𝕜)
          (star (ofLp (p := 2) ((b'.repr : (a : F) → EuclideanSpace 𝕜 ι') y))) :
        Matrix ι ι' 𝕜)
⊢ Eq (α := Matrix ι ι' 𝕜)
    ((toMatrix b'.toBasis b : (a : F →ₗ[𝕜] E) → Matrix ι ι' 𝕜)
        (↑((((rankOne 𝕜 : (a : E) → F →L⋆[𝕜] F →L[𝕜] E) x : F →L⋆[𝕜] F →L[𝕜] E) : (a : F) → F →L[𝕜] E) y) : F →ₗ[𝕜] E) :
      Matrix ι ι' 𝕜)
    (Matrix.vecMulVec (⇑((b.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : (a : ι) → 𝕜)
        (star (ofLp (p := 2) ((b'.repr : (a : F) → EuclideanSpace 𝕜 ι') y))) :
      Matrix ι ι' 𝕜)

Tactic:
have := Fintype.ofFinite ι
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
𝕜 : Type u_7
m : Type u_8
n : Type u_9
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
x : EuclideanSpace 𝕜 m
y : EuclideanSpace 𝕜 n
⊢ (LinearEquiv.symm toEuclideanLin : (a : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) → Matrix m n 𝕜)
      (↑((((rankOne 𝕜 :
                    (a : EuclideanSpace 𝕜 m) → EuclideanSpace 𝕜 n →L⋆[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
                  x :
                EuclideanSpace 𝕜 n →L⋆[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m) :
              (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
            y) :
        EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) =
    vecMulVec x.ofLp (star y.ofLp)

Tactic:
simp [toLpLin, toMatrix', ← ext_iff, vecMulVec_apply, inner_single_right, mul_comm]

Premises used: LinearMap.toMatrix', Matrix.toLpLin, Matrix.vecMulVec_apply, mul_comm, Matrix.ext_iff, EuclideanSpace.inner_single_right
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
inst_8 : Unique ι
h : finrank 𝕜 E = 1
v : E
hv : ‖v‖ = 1
⊢ v ≠ 0

Tactic:
aesop
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
inst_8 : Unique ι
h : finrank 𝕜 E = 1
v : E
hv : ‖v‖ = 1
⊢ Orthonormal.{u_3, u_4, u_1} 𝕜 (E := E) (ι := ι)
    (⇑(basisSingleton.{u_3, u_4, u_1} (K := 𝕜) ι h v ⋯ : Basis ι 𝕜 E) : (a : ι) → E)

Tactic:
simpa
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : Unique ι
h : finrank 𝕜 E = 1
v : E
hv : ‖v‖ = 1
i : ι
⊢ (orthonormalBasisSingleton ι 𝕜 h v hv : (a : ι) → E) i = v

Tactic:
simp [orthonormalBasisSingleton]

Premises used: FiniteDimensional.orthonormalBasisSingleton
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : Unique ι
h : finrank 𝕜 E = 1
v : E
hv : ‖v‖ = 1
⊢ OrthonormalBasis.toBasis (orthonormalBasisSingleton ι 𝕜 h v hv) = basisSingleton.{u_3, u_4, u_1} (K := 𝕜) ι h v ⋯

Tactic:
simp [orthonormalBasisSingleton]

Premises used: FiniteDimensional.orthonormalBasisSingleton
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : Unique ι
h : finrank 𝕜 E = 1
v : E
hv : ‖v‖ = 1
w : E
h₁ :
  ∀ (i : ι),
    Eq.{u_3 + 1} (α := 𝕜)
      (ofLp (p := 2) ((OrthonormalBasis.repr (orthonormalBasisSingleton ι 𝕜 h v hv) : (a : E) → EuclideanSpace 𝕜 ι) w)
          i :
        𝕜)
      (ofLp (EuclideanSpace.single default ⟪v, w⟫) i : 𝕜)
⊢ Eq (α := EuclideanSpace 𝕜 ι)
    ((OrthonormalBasis.repr (orthonormalBasisSingleton ι 𝕜 h v hv) : (a : E) → EuclideanSpace 𝕜 ι) w :
      EuclideanSpace 𝕜 ι)
    (EuclideanSpace.single default ⟪v, w⟫ : EuclideanSpace 𝕜 ι)

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : Unique ι
h : finrank 𝕜 E = 1
v : E
hv : ‖v‖ = 1
w : E
i : ι
⊢ Eq.{u_3 + 1} (α := 𝕜)
    (ofLp (p := 2) ((OrthonormalBasis.repr (orthonormalBasisSingleton ι 𝕜 h v hv) : (a : E) → EuclideanSpace 𝕜 ι) w) i :
      𝕜)
    (ofLp (EuclideanSpace.single default ⟪v, w⟫) i : 𝕜)

Tactic:
simp [OrthonormalBasis.repr_apply_apply, Unique.eq_default]

Premises used: OrthonormalBasis.repr_apply_apply, Unique.eq_default
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : Unique ι
h : finrank 𝕜 E = 1
v : E
hv : ‖v‖ = 1
⊢ Eq (α := Set E) (range.{u_4, u_1 + 1} (ι := ι) (⇑(orthonormalBasisSingleton ι 𝕜 h v hv) : (a : ι) → E)) {v}

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
T : E →ₗ[𝕜] E
hT : T.IsPositive
⊢ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T

Tactic:
hT.1

Premises used: And.left
-- 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 →ₗ[𝕜] E
hT : T.IsPositive
x : E
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫ : ℝ)

Tactic:
hT.2 x

Premises used: And.right
-- 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 →ₗ[𝕜] E
hT : T.IsPositive
x : E
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, (T : (a : E) → E) x⟫ : ℝ)

Tactic:
inner_re_symm (𝕜 := 𝕜) _ x ▸ hT.re_inner_nonneg_left x

Premises used: Eq.rec, inner_re_symm, LinearMap.IsPositive.re_inner_nonneg_left
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
E' : Type u_4
inst : NormedAddCommGroup E'
inst_1 : InnerProductSpace ℂ E'
T : E' →ₗ[ℂ] E'
simp_rw :
  (IsSymmetric.{0, u_4} (𝕜 := ℂ) (E := E') T ∧
      ∀ (x : E'), LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)) ↔
    ∀ (x : E'),
      (↑((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ) : ℂ) = ⟪(T : (a : E') → E') x, x⟫_ℂ ∧
        LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)
simp_rw₁ :
  (IsSymmetric.{0, u_4} (𝕜 := ℂ) (E := E') T ∧
      ∀ (x : E'), LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)) ↔
    (∀ (x : E'), (↑((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ) : ℂ) = ⟪(T : (a : E') → E') x, x⟫_ℂ) ∧
      ∀ (x : E'), LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)
simp_rw₂ :
  ((∀ (v : E'), (starRingEnd ℂ : (a : ℂ) → ℂ) ⟪(T : (a : E') → E') v, v⟫_ℂ = ⟪(T : (a : E') → E') v, v⟫_ℂ) ∧
      ∀ (x : E'), LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)) ↔
    (∀ (x : E'), (↑((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ) : ℂ) = ⟪(T : (a : E') → E') x, x⟫_ℂ) ∧
      ∀ (x : E'), LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)
simp_rw₃ :
  ((∀ (v : E'), (↑((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') v, v⟫_ℂ) : ℂ) = ⟪(T : (a : E') → E') v, v⟫_ℂ) ∧
      ∀ (x : E'), LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)) ↔
    (∀ (x : E'), (↑((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ) : ℂ) = ⟪(T : (a : E') → E') x, x⟫_ℂ) ∧
      ∀ (x : E'), LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)
simp_rw₄ :
  ((∀ (v : E'), (↑(⟪(T : (a : E') → E') v, v⟫_ℂ).re : ℂ) = ⟪(T : (a : E') → E') v, v⟫_ℂ) ∧
      ∀ (x : E'), 0 ≤ (⟪(T : (a : E') → E') x, x⟫_ℂ).re) ↔
    (∀ (x : E'), (↑(⟪(T : (a : E') → E') x, x⟫_ℂ).re : ℂ) = ⟪(T : (a : E') → E') x, x⟫_ℂ) ∧
      ∀ (x : E'), 0 ≤ (⟪(T : (a : E') → E') x, x⟫_ℂ).re
⊢ T.IsPositive ↔
    ∀ (x : E'),
      (↑((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ) : ℂ) = ⟪(T : (a : E') → E') x, x⟫_ℂ ∧
        LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)

Tactic:
simp_rw [IsPositive, forall_and, isSymmetric_iff_inner_map_self_real,
    conj_eq_iff_re, re_to_complex, Complex.coe_algebraMap]

Premises used: RCLike.conj_eq_iff_re, LinearMap.IsPositive, Complex.coe_algebraMap, LinearMap.isSymmetric_iff_inner_map_self_real, RCLike.re_to_complex, forall_and
-- 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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsPositive
⊢ IsSelfAdjoint T

Tactic:
(isSymmetric_iff_isSelfAdjoint _).mp hT.isSymmetric

Premises used: LinearMap.IsPositive.isSymmetric, Iff.mp, LinearMap.isSymmetric_iff_isSelfAdjoint
-- 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 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsPositive
⊢ (adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) T = T

Tactic:
hT.isSelfAdjoint

Premises used: IsSelfAdjoint, LinearMap.IsPositive.isSelfAdjoint
-- 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 →ₗ[𝕜] E
simp_rw :
  IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T →
    ((∀ (x : E), LE.le.{u_1} (α := 𝕜) 0 (↑((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫) : 𝕜)) ↔
      ∀ (x : E), 0 ≤ ⟪(T : (a : E) → E) x, x⟫)
⊢ T.IsPositive ↔ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T ∧ ∀ (x : E), 0 ≤ ⟪(T : (a : E) → E) x, x⟫

Tactic:
simp_rw [IsPositive, and_congr_right_iff, ← RCLike.ofReal_nonneg (K := 𝕜)]

Premises used: RCLike.ofReal_nonneg, and_congr_right_iff, LinearMap.IsPositive
-- 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 →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
⊢ (∀ (x : E), LE.le.{u_1} (α := 𝕜) 0 (↑((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫) : 𝕜)) ↔
    ∀ (x : E), 0 ≤ ⟪(T : (a : E) → E) x, x⟫

Tactic:
simp [hT]
-- 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 →ₗ[𝕜] E
hT : T.IsPositive
x : E
⊢ 0 ≤ ⟪(T : (a : E) → E) x, x⟫

Tactic:
(T.isPositive_iff.mp hT).right x

Premises used: And.right, Iff.mp, LinearMap.isPositive_iff
-- 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 →ₗ[𝕜] E
hT : T.IsPositive
x : E
⊢ 0 ≤ ⟪x, (T : (a : E) → E) x⟫

Tactic:
hT.isSymmetric _ _ ▸ hT.inner_nonneg_left x

Premises used: LinearMap.IsPositive.inner_nonneg_left, Eq.rec, LinearMap.IsPositive.isSymmetric
-- 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), LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(0 : (a : E) → E) x, x⟫ : ℝ)

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
⊢ IsPositive.{u_1, u_2} (𝕜 := 𝕜) (E := E) 1

Tactic:
⟨.id, fun _ => inner_self_nonneg⟩

Premises used: LinearMap.IsPositive, And.intro, LinearMap.IsSymmetric.id, inner_self_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ IsPositive.{u_1, u_2} (𝕜 := 𝕜) (E := E) id

Tactic:
isPositive_one

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

Tactic:
⟨IsSymmetric.natCast n, fun x => ?_⟩

Premises used: LinearMap.IsSymmetric.natCast, LinearMap.IsPositive, And.intro
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
n : ℕ
refine : ∀ (x : E), LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪((↑n : E →ₗ[𝕜] E) : (a : E) → E) x, x⟫ : ℝ)
⊢ IsPositive.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑n : E →ₗ[𝕜] E)

Tactic:
refine ⟨IsSymmetric.natCast n, fun x => ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
n : ℕ
x : E
simp : 0 ≤ HMul.hMul (α := ℝ) (β := ℝ) ((↑n : ℝ) : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪((↑n : E →ₗ[𝕜] E) : (a : E) → E) x, x⟫ : ℝ)

Tactic:
simp only [Module.End.natCast_apply, ← Nat.cast_smul_eq_nsmul 𝕜, inner_smul_left, map_natCast,
    mul_re, natCast_re, inner_self_im, mul_zero, sub_zero]

Premises used: sub_zero, inner_self_im, RCLike.natCast_re, MulZeroClass.mul_zero, map_natCast, Nat.cast_smul_eq_nsmul, RCLike.mul_re, Module.End.natCast_apply, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
n : ℕ
x : E
positivity positivity₁ positivity₂ positivity₃ :
  LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) →
    0 ≤ HMul.hMul (α := ℝ) (β := ℝ) ((↑n : ℝ) : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
⊢ 0 ≤ HMul.hMul (α := ℝ) (β := ℝ) ((↑n : ℝ) : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)

Tactic:
positivity [inner_self_nonneg (x := x) (𝕜 := 𝕜)]

Premises used: inner_self_nonneg