awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : ‖a‖₊ ≤ t
this : IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)
rw :
  ∀ (ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞))
    (this : IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)),
    SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔
      spectralRadius ℝ (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a) ≤ (↑t : ℝ≥0∞)
rw₁ :
  ∀ (ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞))
    (this : IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)),
    SpectrumRestricts (R := ℝ) (S := ℂ) (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)
      (⇑Complex.reCLM : (a : ℂ) → ℝ)
rw₂ :
  ∀ (ht : spectralRadius ℂ a ≤ (↑t : ℝ≥0∞))
    (this : IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)),
    SpectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ)
rw₃ :
  ∀ (ht : spectralRadius ℂ a ≤ (↑t : ℝ≥0∞))
    (this : IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)),
    IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔
    ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a‖₊ ≤ t
have rw₄ : ∀ (ht : (↑‖a‖₊ : ℝ≥0∞) ≤ (↑t : ℝ≥0∞))
  (this : IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)), IsSelfAdjoint a
Tactic: rw [← ENNReal.coe_le_coe, ← IsSelfAdjoint.spectralRadius_eq_nnnorm,
    ← SpectrumRestricts.spectralRadius_eq (f := Complex.reCLM)] at ht ⊢
Cleared hypotheses: ht, this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hb₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) (a + b) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
have rw : ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖a‖₊ : ℝ) : A) a +
      HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖b‖₊ : ℝ) : A) b‖₊ ≤
  ‖a‖₊ + ‖b‖₊
Tactic: rw [SpectrumRestricts.nnreal_iff_nnnorm (ha₁.add hb₁) (nnnorm_add_le a b), NNReal.coe_add,
    map_add, add_sub_add_comm]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hb₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖a‖₊ : ℝ) : A) a +
        HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖b‖₊ : ℝ) : A) b‖₊ ≤
    ‖a‖₊ + ‖b‖₊
have refine : ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖a‖₊ : ℝ) : A) a‖₊ +
    ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖b‖₊ : ℝ) : A) b‖₊ ≤
  ‖a‖₊ + ‖b‖₊
Tactic: refine nnnorm_add_le _ _ |>.trans ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hb₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖a‖₊ : ℝ) : A) a‖₊ +
      ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖b‖₊ : ℝ) : A) b‖₊ ≤
    ‖a‖₊ + ‖b‖₊
have h₁ : ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖a‖₊ : ℝ) : A) a‖₊ ≤ ‖a‖₊
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hb₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
h₁ : ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖a‖₊ : ℝ) : A) a‖₊ ≤ ‖a‖₊
⊢ ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖a‖₊ : ℝ) : A) a‖₊ +
      ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖b‖₊ : ℝ) : A) b‖₊ ≤
    ‖a‖₊ + ‖b‖₊
have h₂ : ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖b‖₊ : ℝ) : A) b‖₊ ≤ ‖b‖₊
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hb₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
h₁ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
h₂ : IsSelfAdjoint a
⊢ ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖a‖₊ : ℝ) : A) a‖₊ ≤ ‖a‖₊
have h₃ : ‖a‖₊ ≤ ‖a‖₊
Tactic: rw [← SpectrumRestricts.nnreal_iff_nnnorm]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hb₂ h₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
h₃ : IsSelfAdjoint b
⊢ ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖b‖₊ : ℝ) : A) b‖₊ ≤ ‖b‖₊
have h₄ : ‖b‖₊ ≤ ‖b‖₊
Tactic: rw [← SpectrumRestricts.nnreal_iff_nnnorm]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) (HPow.hPow (β := ℕ) a 2) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
have rw : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (id x) 2) '' spectrum ℝ a) x → 0 ≤ x
Tactic: rw [SpectrumRestricts.nnreal_iff, ← cfc_id (R := ℝ) a, ← cfc_pow .., cfc_map_spectrum ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) (-a) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ a = 0
have ha₃ : ∀ x ∈ spectrum ℝ a, 0 ≤ x
Tactic: rw [SpectrumRestricts.nnreal_iff] at ha₁ ha₂
Cleared hypotheses: ha₁, ha₂
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) (-a) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
ha₃ : ∀ x ∈ spectrum ℝ a, 0 ≤ x
⊢ a = 0
have ha₄ : ∀ x ∈ spectrum ℝ (-a), 0 ≤ x
Tactic: rw [SpectrumRestricts.nnreal_iff] at ha₁ ha₂
Cleared hypotheses: ha₁, ha₂
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : ∀ x ∈ spectrum ℝ a, 0 ≤ x
ha₂ : ∀ x ∈ spectrum ℝ (-a), 0 ≤ x
⊢ a = 0
have apply : spectrum ℝ a ⊆ {0}
Tactic: apply CFC.eq_zero_of_spectrum_subset_zero (R := ℝ) a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : ∀ x ∈ spectrum ℝ a, 0 ≤ x
ha₂ : ∀ x ∈ spectrum ℝ (-a), 0 ≤ x
⊢ ∀ y ∈ spectrum ℝ a, y = 0
have ha₃ : ∀ (x : ℝ), -x ∈ spectrum ℝ a → 0 ≤ x
Tactic: simp only [← spectrum.neg_eq, Set.mem_neg] at ha₂
Cleared hypotheses: ha₂
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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
⊢ ∀ y ∈ spectrum ℝ a, y = 0
have h : ∀ (x : ℝ) (hx : x ∈ spectrum ℝ a) (this : 0 ≤ x), x = 0
Tactic: peel ha₁ with x hx _
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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
⊢ x = 0
have linarith : x < 0 → 0 - x + (x - 0) = 0
Tactic: linarith [ha₂ (-x) ((neg_neg x).symm ▸ hx)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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
⊢ x = 0
have linarith₁ : 0 < x → 0 - x + (0 - -x) = 0
Tactic: linarith [ha₂ (-x) ((neg_neg x).symm ▸ hx)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) (r • a) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
have rw : ∀ (ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x) {r : ℝ} (hr : 0 ≤ r), ∀ x ∈ spectrum ℝ (r • a), 0 ≤ x
Tactic: rw [SpectrumRestricts.nnreal_iff] at ha ⊢
Cleared hypotheses: ha, r, hr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
Goal:
A : Type u_2
inst : Ring A
inst_1 : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
r : ℝ
hr : 0 ≤ r
⊢ ∀ x ∈ spectrum ℝ (r • a), 0 ≤ x
have a₁ : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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)
⊢ 0 ≤ x
have pos : ∀ (hr' : r = 0), 0 ≤ x
Tactic: by_cases hr' : r = 0
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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
⊢ 0 ≤ x
have neg : ∀ (hr' : ¬r = 0), 0 ≤ x
Tactic: by_cases hr' : r = 0
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
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
⊢ 0 ≤ x
have hx₁ : x = 0
Tactic: simp only [hr', zero_smul, spectrum.zero_eq, Set.mem_singleton_iff] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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
⊢ 0 ≤ x
have neg : ∀ (r : ℝˣ) (hr : 0 ≤ (↑r : ℝ)) (hx : x ∈ spectrum ℝ ((↑r : ℝ) • a)) (hr' : ¬(↑r : ℝ) = 0), 0 ≤ x
Tactic: lift r to ℝˣ using IsUnit.mk0 r hr'
Cleared hypotheses: r, hr, hx, hr'
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
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
⊢ 0 ≤ x
have hx₁ : r⁻¹ • x ∈ spectrum ℝ a
Tactic: rw [← Units.smul_def, spectrum.unit_smul_eq_smul, Set.mem_smul_set_iff_inv_smul_mem] at hx
Cleared hypotheses: hx, hr'
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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
have neg : HSMul.hSMul (β := ℝ) (↑r : ℝ)⁻¹ 0 ≤ (↑r : ℝ)⁻¹ • x
Tactic: refine le_of_smul_le_smul_left ?_ (inv_pos.mpr <| lt_of_le_of_ne hr <| ne_comm.mpr hr')
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
⊢ ∀ x ∈ spectrum ℝ (star b * b), 0 ≤ x
have set : let a := star b * b;
∀ (a_def : a = star b * b), ∀ x ∈ spectrum ℝ a, 0 ≤ x
Tactic: set a := star b * b with a_def
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x
have ha : IsSelfAdjoint a
Tactic: have ha : IsSelfAdjoint a := by simp [a_def]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
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⁻
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x
have h_eq_negPart_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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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
have simp : ∀ x ∈ spectrum ℝ (HPow.hPow (β := ℕ) (cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a) 3), 0 ≤ x
Tactic: simp only [SpectrumRestricts.nnreal_iff, h_eq_negPart_a, CFC.negPart_def]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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 ∈ spectrum ℝ (HPow.hPow (β := ℕ) (cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁻) a) 3), 0 ≤ x
have rw : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x⁻ 3) '' spectrum ℝ a) x → 0 ≤ x
Tactic: rw [cfcₙ_eq_cfc (hf0 := by simp), ← cfc_pow (ha := ha) .., cfc_map_spectrum (ha := ha) ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
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 ∈ spectrum ℝ a, 0 ≤ x
have h_c_spec₀ : 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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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)
have 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)
Tactic: rw [eq_sub_iff_add_eq'.mpr <| star_mul_self_add_self_mul_star c, sub_eq_add_neg, ← sq, ← sq]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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)
have 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))
Tactic: refine SpectrumRestricts.nnreal_add ?_ ?_ ?_ h_c_spec₀
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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))
⊢ 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)
have refine_2 : IsSelfAdjoint (-(star c * c))
Tactic: refine SpectrumRestricts.nnreal_add ?_ ?_ ?_ h_c_spec₀
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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))
⊢ 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)
have 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)
Tactic: refine SpectrumRestricts.nnreal_add ?_ ?_ ?_ h_c_spec₀
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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)
have 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)
Tactic: rw [← Nat.cast_smul_eq_nsmul ℝ]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
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
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x
have h_c_spec₁ : 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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
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)
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x
have h_eq_negPart_a₁ : 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
Cleared hypotheses: h_eq_negPart_a, h_c_spec₀, h_c_spec₁