awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : ∀ x ∈ spectrum ℝ a, 0 ≤ x
ha₂ : ∀ (x : ℝ), -x ∈ spectrum ℝ a → 0 ≤ x
h : ∀ (x : ℝ) (hx : x ∈ spectrum ℝ a) (this : 0 ≤ x), x = 0
⊢ ∀ y ∈ spectrum ℝ a, y = 0

Tactic:
peel ha₁ with x hx _
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : ∀ x ∈ spectrum ℝ a, 0 ≤ x
ha₂ : ∀ (x : ℝ), -x ∈ spectrum ℝ a → 0 ≤ x
x : ℝ
hx : x ∈ spectrum ℝ a
this : 0 ≤ x
linarith : x < 0 → 0 - x + (x - 0) = 0
linarith₁ : 0 < x → 0 - x + (0 - -x) = 0
⊢ x = 0

Tactic:
linarith [ha₂ (-x) ((neg_neg x).symm ▸ hx)]

Premises used: Eq.rec, neg_neg, Eq.symm, Neg.neg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_2
inst : Ring A
inst_1 : Algebra ℝ A
a : A
ha : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
r : ℝ
hr : 0 ≤ r
rw : ∀ (ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x) {r : ℝ} (hr : 0 ≤ r), ∀ x ∈ spectrum ℝ (r • a), 0 ≤ x
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) (r • a) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
rw [SpectrumRestricts.nnreal_iff] at ha ⊢

Premises used: SpectrumRestricts.nnreal_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_2
inst : Ring A
inst_1 : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
r : ℝ
hr : 0 ≤ r
⊢ Nontrivial A

Tactic:
nontriviality A
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_2
inst : Ring A
inst_1 : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
r : ℝ
hr : 0 ≤ r
h : Nontrivial A
x : ℝ
hx : x ∈ spectrum ℝ (r • a)
pos : ∀ (hr' : r = 0), 0 ≤ x
neg : ∀ (hr' : ¬r = 0), 0 ≤ x
⊢ 0 ≤ x

Tactic:
by_cases hr' : r = 0
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_2
inst : Ring A
inst_1 : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
r : ℝ
hr : 0 ≤ r
h : Nontrivial A
x : ℝ
hx : x ∈ spectrum ℝ (r • a)
hr' : r = 0
⊢ x = 0

Tactic:
simp only [hr', zero_smul, spectrum.zero_eq, Set.mem_singleton_iff] at hx ⊢

Premises used: zero_smul, Set.mem_singleton_iff, spectrum.zero_eq
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_2
inst : Ring A
inst_1 : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
r : ℝ
hr : 0 ≤ r
h : Nontrivial A
x : ℝ
hr' : r = 0
hx : x = 0
⊢ 0 ≤ x

Tactic:
hx.symm.le

Premises used: Eq.le, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_2
inst : Ring A
inst_1 : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
r : ℝ
hr : 0 ≤ r
h : Nontrivial A
x : ℝ
hr' : r = 0
hx : x = 0
⊢ 0 ≤ x

Tactic:
exact hx.symm.le

Premises used: Eq.le, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_2
inst : Ring A
inst_1 : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
r : ℝ
hr : 0 ≤ r
h : Nontrivial A
x : ℝ
hx : x ∈ spectrum ℝ (r • a)
hr' : ¬r = 0
⊢ IsUnit r

Tactic:
IsUnit.mk0 r hr'

Premises used: IsUnit.mk0
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_2
inst : Ring A
inst_1 : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
r : ℝ
hr : 0 ≤ r
h : Nontrivial A
x : ℝ
hx : x ∈ spectrum ℝ (r • a)
hr' : ¬r = 0
neg : ∀ (r : ℝˣ) (hr : 0 ≤ (↑r : ℝ)) (hx : x ∈ spectrum ℝ ((↑r : ℝ) • a)) (hr' : ¬(↑r : ℝ) = 0), 0 ≤ x
⊢ 0 ≤ x

Tactic:
lift r to ℝˣ using IsUnit.mk0 r hr'

Premises used: IsUnit.mk0
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_2
inst : Ring A
inst_1 : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
h : Nontrivial A
x : ℝ
r : ℝˣ
hr : 0 ≤ (↑r : ℝ)
hx : x ∈ spectrum ℝ ((↑r : ℝ) • a)
hr' : ¬(↑r : ℝ) = 0
⊢ r⁻¹ • x ∈ spectrum ℝ a

Tactic:
rw [← Units.smul_def, spectrum.unit_smul_eq_smul, Set.mem_smul_set_iff_inv_smul_mem] at hx

Premises used: Units.smul_def, Set.mem_smul_set_iff_inv_smul_mem, spectrum.unit_smul_eq_smul
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_2
inst : Ring A
inst_1 : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
h : Nontrivial A
x : ℝ
r : ℝˣ
hr : 0 ≤ (↑r : ℝ)
hx : x ∈ spectrum ℝ ((↑r : ℝ) • a)
hr' : ¬(↑r : ℝ) = 0
hx₁ : r⁻¹ • x ∈ spectrum ℝ a
⊢ ¬(↑r : ℝ) = 0

Tactic:
rw [← Units.smul_def, spectrum.unit_smul_eq_smul, Set.mem_smul_set_iff_inv_smul_mem] at hx

Premises used: Units.smul_def, Set.mem_smul_set_iff_inv_smul_mem, spectrum.unit_smul_eq_smul
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_2
inst : Ring A
inst_1 : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
h : Nontrivial A
x : ℝ
r : ℝˣ
hr : 0 ≤ (↑r : ℝ)
hx : r⁻¹ • x ∈ spectrum ℝ a
hr' : ¬(↑r : ℝ) = 0
⊢ 0 ≤ x

Tactic:
le_of_smul_le_smul_left ?_ (inv_pos.mpr <| lt_of_le_of_ne hr <| ne_comm.mpr hr')

Premises used: Iff.mpr, inv_pos, le_of_smul_le_smul_left, ne_comm, lt_of_le_of_ne
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_2
inst : Ring A
inst_1 : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
h : Nontrivial A
x : ℝ
r : ℝˣ
hr : 0 ≤ (↑r : ℝ)
hx : r⁻¹ • x ∈ spectrum ℝ a
hr' : ¬(↑r : ℝ) = 0
neg : HSMul.hSMul (β := ℝ) (↑r : ℝ)⁻¹ 0 ≤ (↑r : ℝ)⁻¹ • x
⊢ 0 ≤ x

Tactic:
refine le_of_smul_le_smul_left ?_ (inv_pos.mpr <| lt_of_le_of_ne hr <| ne_comm.mpr hr')

Premises used: Iff.mpr, inv_pos, le_of_smul_le_smul_left, ne_comm, lt_of_le_of_ne
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_2
inst : Ring A
inst_1 : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
h : Nontrivial A
x : ℝ
r : ℝˣ
hr : 0 ≤ (↑r : ℝ)
hx : r⁻¹ • x ∈ spectrum ℝ a
hr' : ¬(↑r : ℝ) = 0
⊢ HSMul.hSMul (β := ℝ) (↑r : ℝ)⁻¹ 0 ≤ (↑r : ℝ)⁻¹ • x

Tactic:
simpa [Units.smul_def] using ha _ hx

Premises used: Units.smul_def
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
set :
  let a := star b * b;
  ∀ (a_def : a = star b * b), ∀ x ∈ spectrum ℝ a, 0 ≤ x
⊢ ∀ x ∈ spectrum ℝ (star b * b), 0 ≤ x

Tactic:
set a := star b * b with a_def

Premises used: Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
⊢ IsSelfAdjoint a

Tactic:
simp [a_def]
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
⊢ IsSelfAdjoint a

Tactic:
have ha : IsSelfAdjoint a := by simp [a_def]
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
⊢ -(star c * c) = -a⁻ * a * a⁻

Tactic:
simp only [star_mul, c, mul_assoc, ← mul_assoc (star b), ← a_def, CFC.negPart_def,
        neg_mul, IsSelfAdjoint.cfcₙ (f := (·⁻)).star_eq]

Premises used: mul_assoc, StarMul.star_mul, CFC.negPart_def, neg_mul, IsSelfAdjoint.star_eq, Star.star, IsSelfAdjoint.cfcₙ
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
⊢ -a⁻ * (a⁺ - a⁻) * a⁻ = HPow.hPow (β := ℕ) a⁻ 3

Tactic:
simp [mul_sub, pow_succ]

Premises used: mul_sub, pow_succ
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
⊢ -(star c * c) = HPow.hPow (β := ℕ) a⁻ 3

Tactic:
have h_eq_negPart_a : -(star c * c) = a⁻ ^ 3 := calc
    -(star c * c) = - a⁻ * a * a⁻ := by
      simp only [star_mul, c, mul_assoc, ← mul_assoc (star b), ← a_def, CFC.negPart_def,
        neg_mul, IsSelfAdjoint.cfcₙ (f := (·⁻)).star_eq]
    _ = - a⁻ * (a⁺ - a⁻) * a⁻ :=
      congr(- a⁻ * $(CFC.posPart_sub_negPart a ha) * a⁻).symm
    _ = a⁻ ^ 3 := by simp [mul_sub, pow_succ]
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = HPow.hPow (β := ℕ) a⁻ 3
simp : ∀ x ∈ spectrum ℝ (HPow.hPow (β := ℕ) (cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a) 3), 0 ≤ x
⊢ SpectrumRestricts (R := ℝ≥0) (-(star c * c)) fun (x : ℝ) ↦ (ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) x

Tactic:
simp only [SpectrumRestricts.nnreal_iff, h_eq_negPart_a, CFC.negPart_def]

Premises used: SpectrumRestricts.nnreal_iff, CFC.negPart_def
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = HPow.hPow (β := ℕ) a⁻ 3
⊢ Eq (α := ℝ) 0⁻ 0

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = HPow.hPow (β := ℕ) a⁻ 3
rw : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x⁻ 3) '' spectrum ℝ a) x → 0 ≤ x
⊢ ∀ x ∈ spectrum ℝ (HPow.hPow (β := ℕ) (cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a) 3), 0 ≤ x

Tactic:
rw [cfcₙ_eq_cfc (hf0 := by simp), ← cfc_pow (ha := ha) .., cfc_map_spectrum (ha := ha) ..]

Premises used: cfc_pow, cfcₙ_eq_cfc, cfc_map_spectrum
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = HPow.hPow (β := ℕ) a⁻ 3
x : ℝ
⊢ LE.le (α := ℝ) 0 ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x⁻ 3) x)

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = HPow.hPow (β := ℕ) a⁻ 3
⊢ SpectrumRestricts (R := ℝ≥0) (-(star c * c)) fun (x : ℝ) ↦ (ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) x

Tactic:
have h_c_spec₀ : SpectrumRestricts (-(star c * c)) (ContinuousMap.realToNNReal ·) := by
    simp only [SpectrumRestricts.nnreal_iff, h_eq_negPart_a, CFC.negPart_def]
    rw [cfcₙ_eq_cfc (hf0 := by simp), ← cfc_pow (ha := ha) .., cfc_map_spectrum (ha := ha) ..]
    rintro - ⟨x, -, rfl⟩
    positivity
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = HPow.hPow (β := ℕ) a⁻ 3
h_c_spec₀ : SpectrumRestricts (R := ℝ≥0) (-(star c * c)) fun (x : ℝ) ↦ (ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) x
rw :
  SpectrumRestricts (R := ℝ≥0) (S := ℝ)
    (HSMul.hSMul (α := ℕ) 2
        (HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) c) : A) 2 +
          HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) c) : A) 2) +
      -(star c * c))
    (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) (c * star c) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
rw [eq_sub_iff_add_eq'.mpr <| star_mul_self_add_self_mul_star c, sub_eq_add_neg, ← sq, ← sq]

Premises used: Iff.mpr, eq_sub_iff_add_eq', sub_eq_add_neg, star_mul_self_add_self_mul_star, sq
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = HPow.hPow (β := ℕ) a⁻ 3
h_c_spec₀ : SpectrumRestricts (R := ℝ≥0) (-(star c * c)) fun (x : ℝ) ↦ (ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) x
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ)
    (HSMul.hSMul (α := ℕ) 2
        (HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) c) : A) 2 +
          HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) c) : A) 2) +
      -(star c * c))
    (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
SpectrumRestricts.nnreal_add ?_ ?_ ?_ h_c_spec₀

Premises used: SpectrumRestricts.nnreal_add
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = HPow.hPow (β := ℕ) a⁻ 3
h_c_spec₀ : SpectrumRestricts (R := ℝ≥0) (-(star c * c)) fun (x : ℝ) ↦ (ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) x
refine_1 :
  IsSelfAdjoint
    (HSMul.hSMul (α := ℕ) 2
      (HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) c) : A) 2 +
        HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) c) : A) 2))
refine_2 : IsSelfAdjoint (-(star c * c))
refine_3 :
  SpectrumRestricts (R := ℝ≥0) (S := ℝ)
    (HSMul.hSMul (α := ℕ) 2
      (HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) c) : A) 2 +
        HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) c) : A) 2))
    (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ)
    (HSMul.hSMul (α := ℕ) 2
        (HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) c) : A) 2 +
          HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) c) : A) 2) +
      -(star c * c))
    (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
refine SpectrumRestricts.nnreal_add ?_ ?_ ?_ h_c_spec₀

Premises used: SpectrumRestricts.nnreal_add
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = HPow.hPow (β := ℕ) a⁻ 3
h_c_spec₀ : SpectrumRestricts (R := ℝ≥0) (-(star c * c)) fun (x : ℝ) ↦ (ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) x
⊢ IsSelfAdjoint
    (HSMul.hSMul (α := ℕ) 2
      (HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) c) : A) 2 +
        HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) c) : A) 2))

Tactic:
.smul (star_trivial _) <| ((ℜ c).prop.pow 2).add ((ℑ c).prop.pow 2)

Premises used: imaginaryPart, TrivialStar.star_trivial, Subtype.prop, IsSelfAdjoint.add, IsSelfAdjoint.pow, IsSelfAdjoint.smul, realPart, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = HPow.hPow (β := ℕ) a⁻ 3
h_c_spec₀ : SpectrumRestricts (R := ℝ≥0) (-(star c * c)) fun (x : ℝ) ↦ (ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) x
⊢ IsSelfAdjoint
    (HSMul.hSMul (α := ℕ) 2
      (HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) c) : A) 2 +
        HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) c) : A) 2))

Tactic:
exact .smul (star_trivial _) <| ((ℜ c).prop.pow 2).add ((ℑ c).prop.pow 2)

Premises used: imaginaryPart, Subtype.prop, IsSelfAdjoint.add, IsSelfAdjoint.pow, realPart, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = HPow.hPow (β := ℕ) a⁻ 3
h_c_spec₀ : SpectrumRestricts (R := ℝ≥0) (-(star c * c)) fun (x : ℝ) ↦ (ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) x
⊢ IsSelfAdjoint (-(star c * c))

Tactic:
.neg <| .star_mul_self c

Premises used: IsSelfAdjoint.star_mul_self, IsSelfAdjoint.neg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = HPow.hPow (β := ℕ) a⁻ 3
h_c_spec₀ : SpectrumRestricts (R := ℝ≥0) (-(star c * c)) fun (x : ℝ) ↦ (ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) x
⊢ IsSelfAdjoint (-(star c * c))

Tactic:
exact .neg <| .star_mul_self c
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = HPow.hPow (β := ℕ) a⁻ 3
h_c_spec₀ : SpectrumRestricts (R := ℝ≥0) (-(star c * c)) fun (x : ℝ) ↦ (ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) x
refine_3 :
  SpectrumRestricts (R := ℝ≥0) (S := ℝ)
    (HSMul.hSMul (α := ℝ) (↑2 : ℝ)
      (HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) c) : A) 2 +
        HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) c) : A) 2))
    (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ)
    (HSMul.hSMul (α := ℕ) 2
      (HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) c) : A) 2 +
        HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) c) : A) 2))
    (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
rw [← Nat.cast_smul_eq_nsmul ℝ]

Premises used: Real, Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = HPow.hPow (β := ℕ) a⁻ 3
h_c_spec₀ : SpectrumRestricts (R := ℝ≥0) (-(star c * c)) fun (x : ℝ) ↦ (ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) x
⊢ LE.le (α := ℝ) 0 (↑2 : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = HPow.hPow (β := ℕ) a⁻ 3
h_c_spec₀ : SpectrumRestricts (R := ℝ≥0) (-(star c * c)) fun (x : ℝ) ↦ (ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) x
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ)
    (HSMul.hSMul (α := ℝ) (↑2 : ℝ)
      (HPow.hPow (α := A) (β := ℕ) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) c) : A) 2 +
        HPow.hPow (α := A) (β := ℕ) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) c) : A) 2))
    (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
refine (ℜ c).2.sq_spectrumRestricts.nnreal_add ((ℜ c).2.pow 2) ((ℑ c).2.pow 2)
        (ℑ c).2.sq_spectrumRestricts |>.smul_of_nonneg <| by simp

Premises used: SpectrumRestricts.smul_of_nonneg, imaginaryPart, IsSelfAdjoint.sq_spectrumRestricts, IsSelfAdjoint.pow, realPart, OfNat.ofNat, DFunLike.coe, SpectrumRestricts.nnreal_add, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = HPow.hPow (β := ℕ) a⁻ 3
h_c_spec₀ : SpectrumRestricts (R := ℝ≥0) (-(star c * c)) fun (x : ℝ) ↦ (ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) x
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) (c * star c) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
have h_c_spec₁ : SpectrumRestricts (c * star c) ContinuousMap.realToNNReal := by
    rw [eq_sub_iff_add_eq'.mpr <| star_mul_self_add_self_mul_star c, sub_eq_add_neg, ← sq, ← sq]
    refine SpectrumRestricts.nnreal_add ?_ ?_ ?_ h_c_spec₀
    · exact .smul (star_trivial _) <| ((ℜ c).prop.pow 2).add ((ℑ c).prop.pow 2)
    · exact .neg <| .star_mul_self c
    · rw [← Nat.cast_smul_eq_nsmul ℝ]
      refine (ℜ c).2.sq_spectrumRestricts.nnreal_add ((ℜ c).2.pow 2) ((ℑ c).2.pow 2)
        (ℑ c).2.sq_spectrumRestricts |>.smul_of_nonneg <| by simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : 0 = HPow.hPow (β := ℕ) (cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a) 3
h_c_spec₀ : SpectrumRestricts (R := ℝ≥0) (-(star c * c)) fun (x : ℝ) ↦ (ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) x
h_c_spec₁ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) (c * star c) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ Eq (α := ℝ) 0⁻ 0

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = HPow.hPow (β := ℕ) a⁻ 3
h_c_spec₀ : SpectrumRestricts (R := ℝ≥0) (-(star c * c)) fun (x : ℝ) ↦ (ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) x
h_c_spec₁ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) (c * star c) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ cfc (R := ℝ) (p := IsSelfAdjoint) 0 a = cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x⁻ 3) a

Tactic:
rw [h_c_spec₁.mul_comm.eq_zero_of_neg (.star_mul_self c) h_c_spec₀, neg_zero, CFC.negPart_def,
    cfcₙ_eq_cfc (hf0 := by simp), ← cfc_pow _ _ (ha := ha), ← cfc_zero a (R := ℝ)] at h_eq_negPart_a

Premises used: cfc_pow, IsSelfAdjoint.star_mul_self, Real, cfcₙ_eq_cfc, SpectrumRestricts.eq_zero_of_neg, SpectrumRestricts.mul_comm, cfc_zero, CFC.negPart_def, neg_zero
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = HPow.hPow (β := ℕ) a⁻ 3
h_c_spec₀ : SpectrumRestricts (R := ℝ≥0) (-(star c * c)) fun (x : ℝ) ↦ (ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) x
h_c_spec₁ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) (c * star c) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
h_eq_negPart_a₁ :
  cfc (R := ℝ) (p := IsSelfAdjoint) 0 a = cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x⁻ 3) a
⊢ SpectrumRestricts (R := ℝ≥0) (-(star c * c)) fun (x : ℝ) ↦ (ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) x

Tactic:
rw [h_c_spec₁.mul_comm.eq_zero_of_neg (.star_mul_self c) h_c_spec₀, neg_zero, CFC.negPart_def,
    cfcₙ_eq_cfc (hf0 := by simp), ← cfc_pow _ _ (ha := ha), ← cfc_zero a (R := ℝ)] at h_eq_negPart_a

Premises used: cfc_pow, IsSelfAdjoint.star_mul_self, Real, cfcₙ_eq_cfc, SpectrumRestricts.eq_zero_of_neg, SpectrumRestricts.mul_comm, cfc_zero, CFC.negPart_def, neg_zero
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = HPow.hPow (β := ℕ) a⁻ 3
h_c_spec₀ : SpectrumRestricts (R := ℝ≥0) (-(star c * c)) fun (x : ℝ) ↦ (ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) x
h_c_spec₁ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) (c * star c) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
h_eq_negPart_a₁ :
  cfc (R := ℝ) (p := IsSelfAdjoint) 0 a = cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x⁻ 3) a
h_c_spec₂ : SpectrumRestricts (R := ℝ≥0) (-(star c * c)) fun (x : ℝ) ↦ (ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) x
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) (c * star c) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
rw [h_c_spec₁.mul_comm.eq_zero_of_neg (.star_mul_self c) h_c_spec₀, neg_zero, CFC.negPart_def,
    cfcₙ_eq_cfc (hf0 := by simp), ← cfc_pow _ _ (ha := ha), ← cfc_zero a (R := ℝ)] at h_eq_negPart_a

Premises used: cfc_pow, IsSelfAdjoint.star_mul_self, Real, cfcₙ_eq_cfc, SpectrumRestricts.eq_zero_of_neg, SpectrumRestricts.mul_comm, cfc_zero, CFC.negPart_def, neg_zero