awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
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⟫_ℂ : ℝ)
⊢ 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⟫_ℂ : ℝ)
have 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
Tactic: simp_rw [IsPositive, forall_and, isSymmetric_iff_inner_map_self_real,
    conj_eq_iff_re, re_to_complex, Complex.coe_algebraMap]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
⊢ T.IsPositive ↔ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T ∧ ∀ (x : E), 0 ≤ ⟪(T : (a : E) → E) x, x⟫
have 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⟫)
Tactic: simp_rw [IsPositive, and_congr_right_iff, ← RCLike.ofReal_nonneg (K := 𝕜)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
n : ℕ
⊢ IsPositive.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑n : E →ₗ[𝕜] E)
have refine : ∀ (x : E), LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪((↑n : E →ₗ[𝕜] E) : (a : E) → E) x, x⟫ : ℝ)
Tactic: refine ⟨IsSymmetric.natCast n, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
n : ℕ
x : E
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪((↑n : E →ₗ[𝕜] E) : (a : E) → E) x, x⟫ : ℝ)
have simp : 0 ≤ HMul.hMul (α := ℝ) (β := ℝ) ((↑n : ℝ) : ℝ) ((re : (a : 𝕜) → ℝ) ⟪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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
n : ℕ
x : E
⊢ 0 ≤ HMul.hMul (α := ℝ) (β := ℝ) ((↑n : ℝ) : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
have positivity : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) →
  0 ≤ HMul.hMul (α := ℝ) (β := ℝ) ((↑n : ℝ) : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
Tactic: positivity [inner_self_nonneg (x := x) (𝕜 := 𝕜)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T S : E →ₗ[𝕜] E
hT : T.IsPositive
hS : S.IsPositive
⊢ (T + S).IsPositive
have refine : ∀ (x : E), LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T + S : (a : E) → E) x, x⟫ : ℝ)
Tactic: refine ⟨hT.isSymmetric.add hS.isSymmetric, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T S : E →ₗ[𝕜] E
hT : T.IsPositive
hS : S.IsPositive
x : E
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T + S : (a : E) → E) x, x⟫ : ℝ)
have rw : 0 ≤
  HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫ : ℝ)
    ((re : (a : 𝕜) → ℝ) ⟪(S : (a : E) → E) x, x⟫ : ℝ)
Tactic: rw [add_apply, inner_add_left, map_add]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : 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)
have refine : ∀ (x : E), LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(∑ i ∈ s, T i : (a : E) → E) x, x⟫ : ℝ)
Tactic: refine ⟨isSymmetric_sum s fun _ hi ↦ (hT _ hi).isSymmetric, fun _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (hypothesis)
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
⊢ (c • T).IsPositive
have hc' : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) c = c
Tactic: have hc' : starRingEnd 𝕜 c = c := by
    simp [conj_eq_iff_im, ← (le_iff_re_im.mp hc).right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsPositive
c : 𝕜
hc : 0 ≤ c
hc' : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) c = c
⊢ (c • T).IsPositive
have refine : ∀ (x : E), LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(c • T : (a : E) → E) x, x⟫ : ℝ)
Tactic: refine ⟨hT.left.smul hc', fun x => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsPositive
c : 𝕜
hc : 0 ≤ c
hc' : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) c = c
x : E
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(c • T : (a : E) → E) x, x⟫ : ℝ)
have rw : 0 ≤ HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) c : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsPositive
hT' : T ≠ 0
α : 𝕜
⊢ (α • T).IsPositive ↔ 0 ≤ α
have refine : ∀ (h : (α • T).IsPositive), 0 ≤ α
Tactic: refine ⟨fun h ↦ ?_, hT.smul_of_nonneg⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsPositive
hT' : T ≠ 0
α : 𝕜
h : (α • T).IsPositive
⊢ 0 ≤ α
have obtain : ∀ (x : E) (hx : 0 < ⟪x, (T : (a : E) → E) x⟫), 0 ≤ α
Tactic: obtain ⟨x, hx⟩ := by simpa only [hT.1 _] using hT.ne_zero_iff.mp hT'
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (hypothesis)
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 ≤ α
have this : 0 ≤ α * ⟪x, (T : (a : E) → E) x⟫
Tactic: have := by simpa [inner_smul_right] using h.inner_nonneg_right x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
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
⊢ f₁ = f₂
have rw : ∀ (x : E), ⟪(f₁ - f₂ : (a : E) → E) x, x⟫ = 0
Tactic: rw [← sub_eq_zero, ← h₂.isSymmetric.inner_map_self_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (hypothesis)
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
⊢ ⟪(f₁ - f₂ : (a : E) → E) x, x⟫ = 0
have hba2 : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(f₂ - f₁ : (a : E) → E) x, x⟫ : ℝ)
Tactic: have hba2 := h₁.2 x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (hypothesis)
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⟫ : ℝ)
⊢ ⟪(f₁ - f₂ : (a : E) → E) x, x⟫ = 0
have hba2₁ : 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
Cleared hypotheses: hba2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
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 : ℝ)
⊢ ⟪(f₁ - f₂ : (a : E) → E) x, x⟫ = 0
have rw : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪(f₁ - f₂ : (a : E) → E) x, x⟫ : ℝ) (0 : ℝ)
Tactic: rw [← h₂.isSymmetric.coe_re_inner_apply_self, RCLike.ofReal_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsIdempotentElem T
⊢ T.IsPositive ↔ IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
have refine : ∀ (h : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T) (x : E),
  LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫ : ℝ)
Tactic: refine ⟨fun h => h.isSymmetric, fun h => ⟨h, fun x => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsIdempotentElem T
h : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
x : E
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫ : ℝ)
have rw : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) (inner 𝕜 (E := E) ((T : (a : E) → E) x : E) ((T : (a : E) → E) x : E)) : ℝ)
Tactic: rw [← hT.eq, Module.End.mul_apply, h]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
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
⊢ ((↑f.toLinearEquiv : E →ₗ[𝕜] F) ∘ₗ T ∘ₗ (↑f.symm.toLinearEquiv : F →ₗ[𝕜] E)).IsPositive ↔ T.IsPositive
have 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⟫ : ℝ))
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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
⊢ IsPositive (𝕜 := 𝕜) (E := EuclideanSpace 𝕜 n)
      ((Matrix.toEuclideanLin : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) A) ↔
    A.PosSemidef
have 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 : ℝ))
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 := 𝕜)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
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 : ℝ))
have 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 : ℝ)
Tactic: refine fun hA ↦ (EuclideanSpace.equiv n 𝕜).forall_congr' fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Fintype ι
inst_4 : DecidableEq ι
A : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
⊢ Matrix.PosSemidef.{u_4, u_1} (n := ι) (R := 𝕜) ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) A) ↔
    A.IsPositive
have rw : IsPositive (𝕜 := 𝕜) (E := EuclideanSpace 𝕜 ι)
    ((Matrix.toEuclideanLin : (a : Matrix ι ι 𝕜) → EuclideanSpace 𝕜 ι →ₗ[𝕜] EuclideanSpace 𝕜 ι)
      ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) A)) ↔
  A.IsPositive
Tactic: rw [← Matrix.isPositive_toEuclideanLin_iff]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Fintype ι
inst_4 : DecidableEq ι
A : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
⊢ IsPositive (𝕜 := 𝕜) (E := EuclideanSpace 𝕜 ι)
      ((Matrix.toEuclideanLin : (a : Matrix ι ι 𝕜) → EuclideanSpace 𝕜 ι →ₗ[𝕜] EuclideanSpace 𝕜 ι)
        ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) A)) ↔
    A.IsPositive
have 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)
Tactic: convert! isPositive_linearIsometryEquiv_conj_iff b.repr
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Fintype ι
inst_4 : DecidableEq ι
A : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
⊢ (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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
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
have 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
Tactic: refine ⟨fun ⟨h1, h2⟩ a ha ↦ ?_, fun hpq ↦ (hp.sub_of_range_le_range hq hpq).isPositive⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (hypothesis)
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⟫ : ℝ)
⊢ a ∈ q.range
have h2₁ : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(q - p : (a : E) → E) a, a⟫ : ℝ)
Tactic: specialize h2 a
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
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⟫ : ℝ)
have rw : ((re : (a : 𝕜) → ℝ) ⟪(T * T : (a : E) → E) a, a⟫ : ℝ)
Tactic: rw [← hT.isIdempotentElem]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
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
have conv_lhs : (re : (a : 𝕜) → ℝ) ⟪(T * T : (a : E) → E) a, a⟫ = HPow.hPow (β := ℕ) (norm (E := E) ((T : (a : E) → E) a : E)) 2
Tactic: conv_lhs => rw [← hT.isIdempotentElem]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
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 * T : (a : E) → E) a, a⟫ = HPow.hPow (β := ℕ) (norm (E := E) ((T : (a : E) → E) a : E)) 2
have 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
Tactic: rw [Module.End.mul_apply, hT.isSymmetric]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (hypothesis)
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⟫ : ℝ)
⊢ a ∈ q.range
have 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
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 _
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (hypothesis)
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 ∈ q.range
have h2₁ : ‖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
Cleared hypotheses: h2