awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hT : T.IsPositive
⊢ IsSelfAdjoint T

Tactic:
hT.isSymmetric.isSelfAdjoint

Premises used: LinearMap.IsSymmetric.isSelfAdjoint, ContinuousLinearMap.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
T : E →L[𝕜] E
hT : T.IsPositive
x y : E
⊢ ⟪(T : (a : E) → E) x, y⟫ = ⟪x, (T : (a : E) → E) y⟫

Tactic:
hT.isSymmetric _ _

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

Tactic:
hT.2 x

Premises used: ContinuousLinearMap.reApplyInnerSelf, 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
inst_3 : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
⊢ IsPositive.{u_1, u_2} (𝕜 := 𝕜) (E := E)
      (((toContinuousLinearMap : (E →ₗ[𝕜] E) ≃ₗ[𝕜] E →L[𝕜] E) : (a : E →ₗ[𝕜] E) → E →L[𝕜] E) T) ↔
    T.IsPositive

Tactic:
Iff.rfl

Premises used: Iff.rfl, ContinuousLinearMap.IsPositive, ContinuousLinearMap.reApplyInnerSelf, 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 →L[𝕜] E
⊢ (↑T : E →ₗ[𝕜] E).IsPositive ↔ T.IsPositive

Tactic:
Iff.rfl

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

Tactic:
hT.toLinearMap.re_inner_nonneg_right x

Premises used: LinearMap.IsPositive.re_inner_nonneg_right, ContinuousLinearMap.IsPositive.toLinearMap
-- 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 : (a : E) → E) x, x⟫

Tactic:
LinearMap.isPositive_iff _

Premises used: ContinuousLinearMap.IsPositive, ContinuousLinearMap.reApplyInnerSelf, LinearMap.IsPositive, 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
inst_3 : CompleteSpace E
T : E →L[𝕜] E
⊢ T.IsPositive ↔ IsSelfAdjoint T ∧ ∀ (x : E), 0 ≤ ⟪(T : (a : E) → E) x, x⟫

Tactic:
simp [isSelfAdjoint_iff_isSymmetric, isPositive_iff]

Premises used: ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric, ContinuousLinearMap.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 →L[𝕜] E
hT : T.IsPositive
x : E
⊢ 0 ≤ ⟪(T : (a : E) → E) x, x⟫

Tactic:
hT.toLinearMap.inner_nonneg_left x

Premises used: ContinuousLinearMap.IsPositive.toLinearMap, LinearMap.IsPositive.inner_nonneg_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 →L[𝕜] E
hT : T.IsPositive
x : E
⊢ 0 ≤ ⟪x, (T : (a : E) → E) x⟫

Tactic:
hT.toLinearMap.inner_nonneg_right x

Premises used: ContinuousLinearMap.IsPositive.toLinearMap, LinearMap.IsPositive.inner_nonneg_right
-- 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) 0

Tactic:
LinearMap.isPositive_zero

Premises used: ContinuousLinearMap.IsPositive, ContinuousLinearMap.reApplyInnerSelf, LinearMap.isPositive_zero, 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
⊢ IsPositive (ContinuousLinearMap.id 𝕜 E)

Tactic:
LinearMap.isPositive_id

Premises used: LinearMap.isPositive_id, ContinuousLinearMap.IsPositive, ContinuousLinearMap.reApplyInnerSelf, 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
⊢ IsPositive.{u_1, u_2} (𝕜 := 𝕜) (E := E) 1

Tactic:
LinearMap.isPositive_one

Premises used: ContinuousLinearMap.IsPositive, ContinuousLinearMap.reApplyInnerSelf, LinearMap.IsPositive, 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 →L[𝕜] E)

Tactic:
(isPositive_toLinearMap_iff _).mp LinearMap.isPositive_natCast

Premises used: ContinuousLinearMap.isPositive_toLinearMap_iff, LinearMap.isPositive_natCast, Iff.mp
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
n : ℕ
inst_3 : n.AtLeastTwo
⊢ IsPositive.{u_1, u_2} (𝕜 := 𝕜) (E := E) (OfNat.ofNat n)

Tactic:
isPositive_natCast

Premises used: ContinuousLinearMap.isPositive_natCast
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T S : E →L[𝕜] E
hT : T.IsPositive
hS : S.IsPositive
⊢ (T + S).IsPositive

Tactic:
(isPositive_toLinearMap_iff _).mp (hT.toLinearMap.add hS.toLinearMap)

Premises used: ContinuousLinearMap.IsPositive.toLinearMap, LinearMap.IsPositive.add, ContinuousLinearMap.isPositive_toLinearMap_iff, Iff.mp
-- 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
T : ι → E →L[𝕜] E
s : Finset ι
hT : ∀ i ∈ s, (T i).IsPositive
⊢ LinearMap.IsPositive.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑(∑ i ∈ s, T i) : E →ₗ[𝕜] E)

Tactic:
simp [LinearMap.isPositive_sum s hT]

Premises used: LinearMap.isPositive_sum
-- 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
c : 𝕜
hc : 0 ≤ c
⊢ (c • T).IsPositive

Tactic:
(isPositive_toLinearMap_iff _).mp (hT.toLinearMap.smul_of_nonneg hc)

Premises used: ContinuousLinearMap.IsPositive.toLinearMap, ContinuousLinearMap.isPositive_toLinearMap_iff, LinearMap.IsPositive.smul_of_nonneg, Iff.mp
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
T : E →L[𝕜] E
hT : T.IsPositive
S : E →L[𝕜] F
⊢ IsPositive (S ∘SL T.comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) S))

Tactic:
isPositive_def'.mpr ⟨hT.isSelfAdjoint.conj_adjoint S, fun x => ?_⟩

Premises used: Iff.mpr, IsSelfAdjoint.conj_adjoint, ContinuousLinearMap.isPositive_def', And.intro, ContinuousLinearMap.IsPositive.isSelfAdjoint
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
T : E →L[𝕜] E
hT : T.IsPositive
S : E →L[𝕜] F
refine :
  ∀ (x : F), 0 ≤ reApplyInnerSelf (S ∘SL T.comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) S)) x
⊢ IsPositive (S ∘SL T.comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) S))

Tactic:
refine isPositive_def'.mpr ⟨hT.isSelfAdjoint.conj_adjoint S, fun x => ?_⟩

Premises used: Iff.mpr, IsSelfAdjoint.conj_adjoint, ContinuousLinearMap.isPositive_def', And.intro, ContinuousLinearMap.IsPositive.isSelfAdjoint
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
T : E →L[𝕜] E
hT : T.IsPositive
S : E →L[𝕜] F
x : F
rw :
  LE.le (α := ℝ) (0 : ℝ)
    ((re : (a : 𝕜) → ℝ)
        (inner.{u_1, u_2} 𝕜 (E := E)
          ((T.comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) S) : (a : F) → E) x : E)
          ((((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) S : F →L[𝕜] E) : (a : F) → E) x : E)) :
      ℝ)
⊢ 0 ≤ reApplyInnerSelf (S ∘SL T.comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) S)) x

Tactic:
rw [reApplyInnerSelf, comp_apply, ← adjoint_inner_right]

Premises used: ContinuousLinearMap.reApplyInnerSelf, ContinuousLinearMap.adjoint_inner_right, ContinuousLinearMap.comp_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
T : E →L[𝕜] E
hT : T.IsPositive
S : E →L[𝕜] F
x : F
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((re : (a : 𝕜) → ℝ)
        (inner.{u_1, u_2} 𝕜 (E := E)
          ((T.comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) S) : (a : F) → E) x : E)
          ((((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) S : F →L[𝕜] E) : (a : F) → E) x : E)) :
      ℝ)

Tactic:
hT.re_inner_nonneg_left _

Premises used: ContinuousLinearMap.IsPositive.re_inner_nonneg_left
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
T : E →L[𝕜] E
hT : T.IsPositive
S : E →L[𝕜] F
x : F
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((re : (a : 𝕜) → ℝ)
        (inner.{u_1, u_2} 𝕜 (E := E)
          ((T.comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) S) : (a : F) → E) x : E)
          ((((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) S : F →L[𝕜] E) : (a : F) → E) x : E)) :
      ℝ)

Tactic:
exact hT.re_inner_nonneg_left _

Premises used: ContinuousLinearMap.IsPositive.re_inner_nonneg_left
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
S : E →L[𝕜] F
⊢ IsPositive (S.comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) S))

Tactic:
simpa using isPositive_one.conj_adjoint S

Premises used: ContinuousLinearMap.IsPositive.conj_adjoint, ContinuousLinearMap.isPositive_one
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
T : E →L[𝕜] E
hT : T.IsPositive
S : F →L[𝕜] E
⊢ IsPositive.{u_1, u_3} (E := F)
    (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) S)
      (T.comp (σ₁₂ := RingHom.id 𝕜)
        ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) ((adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) S))))

Tactic:
hT.conj_adjoint (S†)

Premises used: ContinuousLinearMap.IsPositive.conj_adjoint, ContinuousLinearMap.adjoint, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
T : E →L[𝕜] E
hT : T.IsPositive
S : F →L[𝕜] E
h : S = (adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) ((adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) S)
⊢ IsPositive (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) S) (T ∘SL S))

Tactic:
convert! hT.conj_adjoint (S†)

Premises used: ContinuousLinearMap.IsPositive.conj_adjoint, ContinuousLinearMap.adjoint, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
T : E →L[𝕜] E
hT : T.IsPositive
S : F →L[𝕜] E
h h₁ : S = S
⊢ S = (adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) ((adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) S)

Tactic:
rw [adjoint_adjoint]

Premises used: ContinuousLinearMap.adjoint_adjoint
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
S : E →L[𝕜] F
⊢ IsPositive (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) S) S)

Tactic:
simpa using isPositive_one.adjoint_conj S

Premises used: ContinuousLinearMap.IsPositive.adjoint_conj, ContinuousLinearMap.isPositive_one
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] E
hT : T.IsPositive
S : E →ₗ[𝕜] F
⊢ CompleteSpace E

Tactic:
have := FiniteDimensional.complete 𝕜 E
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] E
hT : T.IsPositive
S : E →ₗ[𝕜] F
this : CompleteSpace E
⊢ CompleteSpace F

Tactic:
have := FiniteDimensional.complete 𝕜 F
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] E
hT : T.IsPositive
S : E →ₗ[𝕜] F
this_1 : CompleteSpace E
this : CompleteSpace F
⊢ LinearMap.IsPositive (S ∘ₗ T ∘ₗ (LinearMap.adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) S)

Tactic:
simpa [← isPositive_toContinuousLinearMap_iff] using
    ((T.isPositive_toContinuousLinearMap_iff.mpr hT).conj_adjoint S.toContinuousLinearMap)

Premises used: Iff.mpr, ContinuousLinearMap.IsPositive.conj_adjoint, LinearMap.isPositive_toContinuousLinearMap_iff, DFunLike.coe, LinearMap.toContinuousLinearMap
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
S : E →ₗ[𝕜] F
⊢ LinearMap.IsPositive (S ∘ₗ (LinearMap.adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) S)

Tactic:
simpa using LinearMap.isPositive_one.conj_adjoint S

Premises used: LinearMap.isPositive_one, LinearMap.IsPositive.conj_adjoint
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] E
hT : T.IsPositive
S : F →ₗ[𝕜] E
⊢ LinearMap.IsPositive.{u_1, u_3} (E := F)
    ((LinearMap.adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) S ∘ₗ
      T ∘ₗ (LinearMap.adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) ((LinearMap.adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) S))

Tactic:
hT.conj_adjoint S.adjoint

Premises used: DFunLike.coe, LinearMap.adjoint, LinearMap.IsPositive.conj_adjoint
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] E
hT : T.IsPositive
S : F →ₗ[𝕜] E
h : S = (LinearMap.adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) ((LinearMap.adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) S)
⊢ LinearMap.IsPositive ((LinearMap.adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) S ∘ₗ T ∘ₗ S)

Tactic:
convert! hT.conj_adjoint S.adjoint

Premises used: DFunLike.coe, LinearMap.adjoint, LinearMap.IsPositive.conj_adjoint
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] E
hT : T.IsPositive
S : F →ₗ[𝕜] E
h h₁ : S = S
⊢ S = (LinearMap.adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) ((LinearMap.adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) S)

Tactic:
rw [LinearMap.adjoint_adjoint]

Premises used: LinearMap.adjoint_adjoint
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
S : E →ₗ[𝕜] F
⊢ LinearMap.IsPositive ((LinearMap.adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) S ∘ₗ S)

Tactic:
simpa using LinearMap.isPositive_one.adjoint_conj S

Premises used: LinearMap.IsPositive.adjoint_conj, 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
U : Submodule 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
inst_3 : U.HasOrthogonalProjection
simp :
  (∀ (x y : E),
      ⟪(U.starProjection : (a : E) → E) ((T : (a : E) → E) ((U.starProjection : (a : E) → E) x : E) : E), y⟫ =
        ⟪x, (U.starProjection : (a : E) → E) ((T : (a : E) → E) ((U.starProjection : (a : E) → E) y : E) : E)⟫) ∧
    ∀ (x : E),
      0 ≤ ⟪(U.starProjection : (a : E) → E) ((T : (a : E) → E) ((U.starProjection : (a : E) → E) x : E) : E), x⟫
⊢ (U.starProjection ∘SL T ∘SL U.starProjection).IsPositive

Tactic:
simp only [isPositive_iff, IsSymmetric, coe_comp, LinearMap.coe_comp, coe_coe,
    Function.comp_apply, coe_comp']

Premises used: ContinuousLinearMap.coe_comp', ContinuousLinearMap.coe_coe, ContinuousLinearMap.coe_comp, LinearMap.coe_comp, ContinuousLinearMap.isPositive_iff, Function.comp_apply, 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
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
simp :
  (∀ (x y : ↥U),
      ⟪(U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E)), y⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E)), x⟫
⊢ IsPositive.{u_1, u_2} (𝕜 := 𝕜) (E := ↥U) (U.orthogonalProjection ∘SL T ∘SL U.subtypeL)

Tactic:
simp only [isPositive_iff, IsSymmetric, coe_comp, LinearMap.coe_comp, coe_coe,
    Function.comp_apply, coe_comp']

Premises used: ContinuousLinearMap.coe_comp', ContinuousLinearMap.coe_coe, ContinuousLinearMap.coe_comp, LinearMap.coe_comp, ContinuousLinearMap.isPositive_iff, Function.comp_apply, 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
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
simp_rw :
  (∀ (x y : ↥U),
      ⟪(T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E), (↑y : E)⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E), (↑x : E)⟫
simp_rw₁ :
  (∀ (x y : ↥U),
      ⟪(T : (a : E) → E) (↑x : E), (↑y : E)⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) (↑y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫
simp_rw₂ :
  (∀ (x y : ↥U), ⟪(T : (a : E) → E) (↑x : E), (↑y : E)⟫ = ⟪(↑x : E), (T : (a : E) → E) (↑y : E)⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫
simp_rw₃ :
  (∀ (x y : ↥U),
      ⟪((↑T : E →ₗ[𝕜] E) : (a : E) → E) (↑x : E), (↑y : E)⟫ = ⟪(↑x : E), ((↑T : E →ₗ[𝕜] E) : (a : E) → E) (↑y : E)⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪((↑T : E →ₗ[𝕜] E) : (a : E) → E) (↑x : E), (↑x : E)⟫
simp_rw₄ : (∀ (x y : ↥U), True) ∧ ∀ (x : ↥U), 0 ≤ ⟪(↑x : E), ((↑T : E →ₗ[𝕜] E) : (a : E) → E) (↑x : E)⟫
simp_rw₅ : (∀ (x y : ↥U), True) ∧ ∀ (x : ↥U), 0 ≤ ⟪(↑x : E), (T : (a : E) → E) (↑x : E)⟫
simp_rw₆ : (∀ (x y : ↥U), True) ∧ ∀ (y : ↥U), True
simp_rw₇ : True ∧ True
⊢ (∀ (x y : ↥U),
      ⟪(U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E)), y⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E)), x⟫

Tactic:
simp_rw [U.inner_orthogonalProjection_eq_of_mem_right, Submodule.subtypeL_apply,
    U.inner_orthogonalProjection_eq_of_mem_left, ← coe_coe, hT.isSymmetric _, coe_coe,
    hT.inner_nonneg_right, implies_true, and_self]

Premises used: ContinuousLinearMap.IsPositive.inner_nonneg_right, and_self, ContinuousLinearMap.IsPositive.isSymmetric, ContinuousLinearMap.coe_coe, Submodule.inner_orthogonalProjection_eq_of_mem_right, Submodule.inner_orthogonalProjection_eq_of_mem_left, Submodule.subtypeL_apply, implies_true
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_4
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
h : ∀ (x : H), HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) ≤ ‖⟪(f : (a : H) → H) x, x⟫‖
⊢ AntilipschitzWith (α := H) (β := H) c⁻¹ (⇑f : (a : H) → H)

Tactic:
f.antilipschitz_of_bound (K := c⁻¹) fun x ↦ ?_

Premises used: ContinuousLinearMap.antilipschitz_of_bound
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_4
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
h : ∀ (x : H), HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) ≤ ‖⟪(f : (a : H) → H) x, x⟫‖
refine : ∀ (x : H), ‖x‖ ≤ (↑c⁻¹ : ℝ) * norm (E := H) ((f : (a : H) → H) x : H)
⊢ AntilipschitzWith (α := H) (β := H) c⁻¹ (⇑f : (a : H) → H)

Tactic:
refine f.antilipschitz_of_bound (K := c⁻¹) fun x ↦ ?_

Premises used: ContinuousLinearMap.antilipschitz_of_bound
-- Module: Mathlib.Analysis.InnerProductSpace.Positive
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_4
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
h : ∀ (x : H), HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) ≤ ‖⟪(f : (a : H) → H) x, x⟫‖
x : H
⊢ 0 < (↑c : ℝ)

Tactic:
exact_mod_cast hc