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
n : ℕ
inst_3 : n.AtLeastTwo
⊢ IsPositive.{u_1, u_2} (𝕜 := 𝕜) (E := E) (OfNat.ofNat n)

Tactic:
isPositive_natCast

Premises used: LinearMap.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 →ₗ[𝕜] E
hT : T.IsPositive
hS : S.IsPositive
⊢ (T + S).IsPositive

Tactic:
⟨hT.isSymmetric.add hS.isSymmetric, fun x => ?_⟩

Premises used: LinearMap.IsPositive, LinearMap.IsPositive.isSymmetric, And.intro, LinearMap.IsSymmetric.add
-- 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 →ₗ[𝕜] E
hT : T.IsPositive
hS : S.IsPositive
refine : ∀ (x : E), LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T + S : (a : E) → E) x, x⟫ : ℝ)
⊢ (T + S).IsPositive

Tactic:
refine ⟨hT.isSymmetric.add hS.isSymmetric, 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
T S : E →ₗ[𝕜] E
hT : T.IsPositive
hS : S.IsPositive
x : E
rw :
  0 ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫ : ℝ)
      ((re : (a : 𝕜) → ℝ) ⟪(S : (a : E) → E) x, x⟫ : ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T + S : (a : E) → E) x, x⟫ : ℝ)

Tactic:
rw [add_apply, inner_add_left, map_add]

Premises used: LinearMap.add_apply, map_add, inner_add_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 S : E →ₗ[𝕜] E
hT : T.IsPositive
hS : S.IsPositive
x : E
⊢ 0 ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫ : ℝ)
      ((re : (a : 𝕜) → ℝ) ⟪(S : (a : E) → E) x, x⟫ : ℝ)

Tactic:
add_nonneg (hT.re_inner_nonneg_left x) (hS.re_inner_nonneg_left x)

Premises used: add_nonneg, LinearMap.IsPositive.re_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 S : E →ₗ[𝕜] E
hT : T.IsPositive
hS : S.IsPositive
x : E
⊢ 0 ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫ : ℝ)
      ((re : (a : 𝕜) → ℝ) ⟪(S : (a : E) → E) x, x⟫ : ℝ)

Tactic:
exact add_nonneg (hT.re_inner_nonneg_left x) (hS.re_inner_nonneg_left x)

Premises used: add_nonneg, LinearMap.IsPositive.re_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
ι : Type u_4
T : ι → E →ₗ[𝕜] E
s : Finset ι
hT : ∀ i ∈ s, (T i).IsPositive
⊢ IsPositive.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ i ∈ s, T i)

Tactic:
⟨isSymmetric_sum s fun _ hi ↦ (hT _ hi).isSymmetric, fun _ ↦ ?_⟩

Premises used: LinearMap.isSymmetric_sum, LinearMap.IsPositive, LinearMap.IsPositive.isSymmetric, 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
ι : Type u_4
T : ι → E →ₗ[𝕜] E
s : Finset ι
hT : ∀ i ∈ s, (T i).IsPositive
refine : ∀ (x : E), LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(∑ i ∈ s, T i : (a : E) → E) x, x⟫ : ℝ)
⊢ IsPositive.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ i ∈ s, T i)

Tactic:
refine ⟨isSymmetric_sum s fun _ hi ↦ (hT _ hi).isSymmetric, fun _ ↦ ?_⟩
-- 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 →ₗ[𝕜] E
s : Finset ι
hT : ∀ i ∈ s, (T i).IsPositive
x : E
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(∑ i ∈ s, T i : (a : E) → E) x, x⟫ : ℝ)

Tactic:
simpa [sum_inner] using Finset.sum_nonneg fun _ hi ↦ (hT _ hi).re_inner_nonneg_left _

Premises used: sum_inner, Finset.sum_nonneg, LinearMap.IsPositive.re_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 →ₗ[𝕜] E
hT : T.IsPositive
⊢ T ≠ 0 ↔ ∃ (x : E), 0 < ⟪(T : (a : E) → E) x, x⟫

Tactic:
simp [← hT.isSymmetric.inner_map_self_eq_zero, lt_iff_le_and_ne', hT.inner_nonneg_left]

Premises used: lt_iff_le_and_ne', LinearMap.IsSymmetric.inner_map_self_eq_zero, LinearMap.IsPositive.inner_nonneg_left, 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
T : E →ₗ[𝕜] E
hT : T.IsPositive
c : 𝕜
hc : 0 ≤ c
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) c = c

Tactic:
simp [conj_eq_iff_im, ← (le_iff_re_im.mp hc).right]

Premises used: RCLike.le_iff_re_im, And.right, RCLike.conj_eq_iff_im, 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
T : E →ₗ[𝕜] E
hT : T.IsPositive
c : 𝕜
hc : 0 ≤ c
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) c = c

Tactic:
have hc' : starRingEnd 𝕜 c = c := by
    simp [conj_eq_iff_im, ← (le_iff_re_im.mp hc).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
c : 𝕜
hc : 0 ≤ c
hc' : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) c = c
⊢ (c • T).IsPositive

Tactic:
⟨hT.left.smul hc', fun x => ?_⟩

Premises used: LinearMap.IsPositive, LinearMap.IsSymmetric.smul, And.left, 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
T : E →ₗ[𝕜] E
hT : T.IsPositive
c : 𝕜
hc : 0 ≤ c
hc' : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) c = c
refine : ∀ (x : E), LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(c • T : (a : E) → E) x, x⟫ : ℝ)
⊢ (c • T).IsPositive

Tactic:
refine ⟨hT.left.smul hc', 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
T : E →ₗ[𝕜] E
hT : T.IsPositive
c : 𝕜
hc : 0 ≤ c
hc' : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) c = c
x : E
rw : 0 ≤ HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) c : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫ : ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(c • T : (a : E) → E) x, x⟫ : ℝ)

Tactic:
rw [smul_apply, inner_smul_left, hc', mul_re, conj_eq_iff_im.mp hc', zero_mul, sub_zero]

Premises used: LinearMap.smul_apply, sub_zero, MulZeroClass.zero_mul, RCLike.conj_eq_iff_im, Iff.mp, RCLike.mul_re, 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
T : E →ₗ[𝕜] E
hT : T.IsPositive
c : 𝕜
hc : 0 ≤ c
hc' : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) c = c
x : E
⊢ 0 ≤ HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) c : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫ : ℝ)

Tactic:
mul_nonneg ((re_nonneg_of_nonneg hc').mpr hc) (re_inner_nonneg_left hT x)

Premises used: Iff.mpr, mul_nonneg, RCLike.re_nonneg_of_nonneg, LinearMap.IsPositive.re_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 →ₗ[𝕜] E
hT : T.IsPositive
c : 𝕜
hc : 0 ≤ c
hc' : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) c = c
x : E
⊢ 0 ≤ HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) c : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫ : ℝ)

Tactic:
exact mul_nonneg ((re_nonneg_of_nonneg hc').mpr hc) (re_inner_nonneg_left hT x)

Premises used: Iff.mpr, mul_nonneg, RCLike.re_nonneg_of_nonneg, LinearMap.IsPositive.re_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 →ₗ[𝕜] E
hT : T.IsPositive
hT' : T ≠ 0
α : 𝕜
⊢ (α • T).IsPositive ↔ 0 ≤ α

Tactic:
⟨fun h ↦ ?_, hT.smul_of_nonneg⟩

Premises used: LinearMap.IsPositive.smul_of_nonneg, 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
T : E →ₗ[𝕜] E
hT : T.IsPositive
hT' : T ≠ 0
α : 𝕜
refine : ∀ (h : (α • T).IsPositive), 0 ≤ α
⊢ (α • T).IsPositive ↔ 0 ≤ α

Tactic:
refine ⟨fun h ↦ ?_, hT.smul_of_nonneg⟩
-- 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
hT' : T ≠ 0
α : 𝕜
h : (α • T).IsPositive
⊢ ∃ (x : E), 0 < ⟪x, (T : (a : E) → E) x⟫

Tactic:
simpa only [hT.1 _] using hT.ne_zero_iff.mp hT'

Premises used: LinearMap.IsPositive.ne_zero_iff, And.left, 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
T : E →ₗ[𝕜] E
hT : T.IsPositive
hT' : T ≠ 0
α : 𝕜
h : (α • T).IsPositive
obtain : ∀ (x : E) (hx : 0 < ⟪x, (T : (a : E) → E) x⟫), 0 ≤ α
⊢ 0 ≤ α

Tactic:
obtain ⟨x, hx⟩ := by simpa only [hT.1 _] using hT.ne_zero_iff.mp 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
hT' : T ≠ 0
α : 𝕜
h : (α • T).IsPositive
x : E
hx : 0 < ⟪x, (T : (a : E) → E) x⟫
⊢ 0 ≤ α * ⟪x, (T : (a : E) → E) x⟫

Tactic:
simpa [inner_smul_right] using h.inner_nonneg_right x

Premises used: inner_smul_right, 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
T : E →ₗ[𝕜] E
hT : T.IsPositive
hT' : T ≠ 0
α : 𝕜
h : (α • T).IsPositive
x : E
hx : 0 < ⟪x, (T : (a : E) → E) x⟫
⊢ 0 ≤ α * ⟪x, (T : (a : E) → E) x⟫

Tactic:
have := by simpa [inner_smul_right] using h.inner_nonneg_right x
-- 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
hT' : T ≠ 0
α : 𝕜
h : (α • T).IsPositive
x : E
hx : 0 < ⟪x, (T : (a : E) → E) x⟫
this : 0 ≤ α * ⟪x, (T : (a : E) → E) x⟫
⊢ HSMul.hSMul (α := 𝕜) 0 ⟪x, (T : (a : E) → E) x⟫ ≤ α • ⟪x, (T : (a : E) → E) x⟫

Tactic:
simpa
-- 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
hT' : T ≠ 0
α : 𝕜
h : (α • T).IsPositive
x : E
hx : 0 < ⟪x, (T : (a : E) → E) x⟫
this : 0 ≤ α * ⟪x, (T : (a : E) → E) x⟫
⊢ 0 ≤ α

Tactic:
exact le_of_smul_le_smul_of_pos_right (by simpa) hx

Premises used: le_of_smul_le_smul_of_pos_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
n : ℕ
hT : T.IsPositive
hn : Module.finrank 𝕜 E = n
i : Fin n
⊢ 0 ≤ ⋯.eigenvalues hn i

Tactic:
simpa only [hT.isSymmetric.apply_eigenvectorBasis, inner_smul_real_left, RCLike.smul_re,
    inner_self_eq_norm_sq, OrthonormalBasis.norm_eq_one, one_pow, mul_one]
      using hT.right (hT.isSymmetric.eigenvectorBasis hn i)

Premises used: one_pow, RCLike.smul_re, OrthonormalBasis.norm_eq_one, inner_self_eq_norm_sq, LinearMap.IsSymmetric.eigenvectorBasis, LinearMap.IsPositive.isSymmetric, And.right, inner_smul_real_left, LinearMap.IsSymmetric.apply_eigenvectorBasis, mul_one, 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
x : E →ₗ[𝕜] E
⊢ (x - x).IsPositive

Tactic:
simp
-- 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
x x_1 x_2 : E →ₗ[𝕜] E
h₁ : (x_1 - x).IsPositive
h₂ : (x_2 - x_1).IsPositive
⊢ (x_2 - x).IsPositive

Tactic:
simpa using h₁.add h₂

Premises used: LinearMap.IsPositive.add
-- 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
f₁ f₂ : E →ₗ[𝕜] E
h₁ : (f₂ - f₁).IsPositive
h₂ : (f₁ - f₂).IsPositive
rw : ∀ (x : E), ⟪(f₁ - f₂ : (a : E) → E) x, x⟫ = 0
⊢ f₁ = f₂

Tactic:
rw [← sub_eq_zero, ← h₂.isSymmetric.inner_map_self_eq_zero]

Premises used: sub_eq_zero, LinearMap.IsSymmetric.inner_map_self_eq_zero, LinearMap.IsPositive.isSymmetric
-- 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
f₁ f₂ : E →ₗ[𝕜] E
h₁ : (f₂ - f₁).IsPositive
h₂ : (f₁ - f₂).IsPositive
x : E
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(f₂ - f₁ : (a : E) → E) x, x⟫ : ℝ)

Tactic:
have hba2 := h₁.2 x
-- 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
f₁ f₂ : E →ₗ[𝕜] E
h₁ : (f₂ - f₁).IsPositive
h₂ : (f₁ - f₂).IsPositive
x : E
hba2 : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(f₂ - f₁ : (a : E) → E) x, x⟫ : ℝ)
⊢ LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(f₁ - f₂ : (a : E) → E) x, x⟫ : ℝ) (0 : ℝ)

Tactic:
rw [← neg_le_neg_iff, ← map_neg, ← inner_neg_left, ← neg_apply, neg_sub, neg_zero] at hba2

Premises used: neg_sub, LinearMap.neg_apply, map_neg, neg_zero, neg_le_neg_iff, inner_neg_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
f₁ f₂ : E →ₗ[𝕜] E
h₁ : (f₂ - f₁).IsPositive
h₂ : (f₁ - f₂).IsPositive
x : E
hba2 : LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(f₁ - f₂ : (a : E) → E) x, x⟫ : ℝ) (0 : ℝ)
rw : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(f₁ - f₂ : (a : E) → E) x, x⟫ : ℝ) (0 : ℝ)
⊢ ⟪(f₁ - f₂ : (a : E) → E) x, x⟫ = 0

Tactic:
rw [← h₂.isSymmetric.coe_re_inner_apply_self, RCLike.ofReal_eq_zero]

Premises used: RCLike.ofReal_eq_zero, LinearMap.IsPositive.isSymmetric, LinearMap.IsSymmetric.coe_re_inner_apply_self
-- 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
f₁ f₂ : E →ₗ[𝕜] E
h₁ : (f₂ - f₁).IsPositive
h₂ : (f₁ - f₂).IsPositive
x : E
hba2 : LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(f₁ - f₂ : (a : E) → E) x, x⟫ : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(f₁ - f₂ : (a : E) → E) x, x⟫ : ℝ) (0 : ℝ)

Tactic:
le_antisymm hba2 (h₂.2 _)

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

Tactic:
exact le_antisymm hba2 (h₂.2 _)

Premises used: le_antisymm, 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
f g : E →ₗ[𝕜] E
⊢ f ≤ g ↔ (g - f).IsPositive

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- 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
⊢ 0 ≤ f ↔ f.IsPositive

Tactic:
simpa using le_def 0 f

Premises used: LinearMap.le_def, OfNat.ofNat
-- 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
a b : E →ₗ[𝕜] E
hab : a ≤ b
c : E →ₗ[𝕜] E
⊢ a + c ≤ b + c

Tactic:
simpa [le_def]

Premises used: LinearMap.le_def
-- 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 : IsIdempotentElem T
⊢ T.IsPositive ↔ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T

Tactic:
⟨fun h => h.isSymmetric, fun h => ⟨h, fun x => ?_⟩⟩

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

Tactic:
refine ⟨fun h => h.isSymmetric, fun h => ⟨h, 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
T : E →ₗ[𝕜] E
hT : IsIdempotentElem T
h : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
x : E
rw :
  LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) (inner 𝕜 (E := E) ((T : (a : E) → E) x : E) ((T : (a : E) → E) x : E)) : ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫ : ℝ)

Tactic:
rw [← hT.eq, Module.End.mul_apply, h]

Premises used: IsIdempotentElem.eq, 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
T : E →ₗ[𝕜] E
hT : IsIdempotentElem T
h : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
x : E
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) (inner 𝕜 (E := E) ((T : (a : E) → E) x : E) ((T : (a : E) → E) x : E)) : ℝ)

Tactic:
inner_self_nonneg

Premises used: 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
T : E →ₗ[𝕜] E
hT : IsIdempotentElem T
h : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
x : E
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) (inner 𝕜 (E := E) ((T : (a : E) → E) x : E) ((T : (a : E) → E) x : E)) : ℝ)

Tactic:
exact inner_self_nonneg

Premises used: inner_self_nonneg
-- 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
T : E →ₗ[𝕜] E
f : E ≃ₗᵢ[𝕜] F
simp_rw :
  IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T →
    ((∀ (x : F),
        LE.le (α := ℝ) (0 : ℝ)
          ((re : (a : 𝕜) → ℝ)
              (inner 𝕜 (E := E) ((T : (a : E) → E) ((f.symm : (a : F) → E) x : E) : E) ((f.symm : (a : F) → E) x : E)) :
            ℝ)) ↔
      ∀ (x : E), LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫ : ℝ))
⊢ ((↑f.toLinearEquiv : E →ₗ[𝕜] F) ∘ₗ T ∘ₗ (↑f.symm.toLinearEquiv : F →ₗ[𝕜] E)).IsPositive ↔ T.IsPositive

Tactic:
simp_rw [IsPositive, isSymmetric_linearIsometryEquiv_conj_iff, and_congr_right_iff,
    LinearIsometryEquiv.toLinearEquiv_symm, coe_comp, LinearEquiv.coe_coe,
    LinearIsometryEquiv.coe_toLinearEquiv, LinearIsometryEquiv.coe_symm_toLinearEquiv,
    Function.comp_apply, LinearIsometryEquiv.inner_map_eq_flip]

Premises used: LinearIsometryEquiv.inner_map_eq_flip, LinearIsometryEquiv.toLinearEquiv_symm, LinearIsometryEquiv.coe_toLinearEquiv, LinearMap.isSymmetric_linearIsometryEquiv_conj_iff, and_congr_right_iff, LinearIsometryEquiv.coe_symm_toLinearEquiv, LinearMap.IsPositive, LinearMap.coe_comp, Function.comp_apply, LinearEquiv.coe_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
T : E →ₗ[𝕜] E
f : E ≃ₗᵢ[𝕜] F
h_1 : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
h :
  ∀ (x : F),
    LE.le (α := ℝ) (0 : ℝ)
      ((re : (a : 𝕜) → ℝ)
          (inner 𝕜 (E := E) ((T : (a : E) → E) ((f.symm : (a : F) → E) x : E) : E) ((f.symm : (a : F) → E) x : E)) :
        ℝ)
x : E
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫ : ℝ)

Tactic:
simpa using h (f x)

Premises used: 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
T : E →ₗ[𝕜] E
f : E ≃ₗᵢ[𝕜] F
⊢ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T →
    ((∀ (x : F),
        LE.le (α := ℝ) (0 : ℝ)
          ((re : (a : 𝕜) → ℝ)
              (inner 𝕜 (E := E) ((T : (a : E) → E) ((f.symm : (a : F) → E) x : E) : E) ((f.symm : (a : F) → E) x : E)) :
            ℝ)) ↔
      ∀ (x : E), LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫ : ℝ))

Tactic:
exact fun _ => ⟨fun h x => by simpa using h (f x), fun h x => h _⟩
-- 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 𝕜
simp_rw :
  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 : ℝ))
⊢ IsPositive (𝕜 := 𝕜) (E := EuclideanSpace 𝕜 n)
      ((Matrix.toEuclideanLin : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) A) ↔
    A.PosSemidef

Tactic:
simp_rw [LinearMap.IsPositive, Matrix.isSymmetric_toEuclideanLin_iff, inner_re_symm,
    EuclideanSpace.inner_eq_star_dotProduct, Matrix.ofLp_toLpLin, Matrix.toLin'_apply,
    dotProduct_comm (A.mulVec _), Matrix.posSemidef_iff_dotProduct_mulVec, and_congr_right_iff,
    RCLike.nonneg_iff (K := 𝕜)]

Premises used: Matrix.isSymmetric_toEuclideanLin_iff, Matrix.ofLp_toLpLin, inner_re_symm, and_congr_right_iff, RCLike.nonneg_iff, LinearMap.IsPositive, EuclideanSpace.inner_eq_star_dotProduct, Matrix.posSemidef_iff_dotProduct_mulVec, Matrix.toLin'_apply, Matrix.mulVec, dotProduct_comm
-- 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 𝕜
⊢ 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:
fun hA ↦ (EuclideanSpace.equiv n 𝕜).forall_congr' fun x ↦ ?_

Premises used: ContinuousLinearEquiv.toLinearEquiv, LinearEquiv.toAddEquiv, Equiv.forall_congr', AddEquiv.toEquiv, EuclideanSpace.equiv