awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  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
h_c_spec₁ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) (c * star c) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ Set.EqOn (β := ℝ) 0 (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x⁻ 3) (spectrum ℝ a)

Tactic:
have h_eqOn := eqOn_of_cfc_eq_cfc (ha := ha) h_eq_negPart_a
-- 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 :
  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
h_c_spec₁ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) (c * star c) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
h_eqOn : Set.EqOn (β := ℝ) 0 (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x⁻ 3) (spectrum ℝ a)
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Tactic:
fun x hx ↦ negPart_eq_zero.mp <| eq_zero_of_pow_eq_zero (h_eqOn hx).symm

Premises used: Iff.mp, negPart_eq_zero, eq_zero_of_pow_eq_zero, Eq.symm
-- 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 :
  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
h_c_spec₁ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) (c * star c) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
h_eqOn : Set.EqOn (β := ℝ) 0 (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x⁻ 3) (spectrum ℝ a)
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Tactic:
exact fun x hx ↦ negPart_eq_zero.mp <| eq_zero_of_pow_eq_zero (h_eqOn hx).symm

Premises used: Iff.mp, negPart_eq_zero, eq_zero_of_pow_eq_zero, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_2
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : ContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
x : ℝ
ha : IsSelfAdjoint a
⊢ (↑x : ℂ) ∈ spectrum ℂ a ↔ x ∈ spectrum ℝ a

Tactic:
simp [← ha.spectrumRestricts.algebraMap_image]

Premises used: SpectrumRestricts.algebraMap_image, IsSelfAdjoint.spectrumRestricts
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
⊢ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) a

Tactic:
rw [StarOrderedRing.nonneg_iff] at ha

Premises used: StarOrderedRing.nonneg_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a x : A
hx : Membership.mem (γ := Set A) (Set.range fun (s : A) ↦ star s * s) x
mem : ∀ (b : A), ∀ x ∈ spectrum.{0, u_1} ℝ (A := A) ((fun (s : A) ↦ star s * s) b), 0 ≤ x
⊢ ∀ x_1 ∈ spectrum ℝ x, 0 ≤ x_1

Tactic:
obtain ⟨b, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
⊢ ∀ x ∈ spectrum.{0, u_1} ℝ (A := A) ((fun (s : A) ↦ star s * s) b), 0 ≤ x

Tactic:
spectrum_star_mul_self_nonneg

Premises used: Set.Mem, spectrum_star_mul_self_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
⊢ ∀ x ∈ spectrum.{0, u_1} ℝ (A := A) ((fun (s : A) ↦ star s * s) b), 0 ≤ x

Tactic:
exact spectrum_star_mul_self_nonneg

Premises used: spectrum_star_mul_self_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ Nontrivial A

Tactic:
nontriviality A
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
h : Nontrivial A
⊢ ∀ x ∈ spectrum.{0, u_1} ℝ (A := A) 0, 0 ≤ x

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a x y : A
x_mem : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) x
y_mem : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) y
hx : ∀ x_1 ∈ spectrum ℝ x, 0 ≤ x_1
hy : ∀ x ∈ spectrum ℝ y, 0 ≤ x
add :
  ∀ (hx : SpectrumRestricts (R := ℝ≥0) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0))
    (hy : SpectrumRestricts (R := ℝ≥0) (S := ℝ) y (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)),
    SpectrumRestricts (R := ℝ≥0) (S := ℝ) (x + y) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ ∀ x_1 ∈ spectrum ℝ (x + y), 0 ≤ x_1

Tactic:
rw [← SpectrumRestricts.nnreal_iff] at hx hy ⊢

Premises used: SpectrumRestricts.nnreal_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a x y : A
x_mem : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) x
y_mem : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) y
hx : SpectrumRestricts (R := ℝ≥0) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hy : SpectrumRestricts (R := ℝ≥0) (S := ℝ) y (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ 0 ≤ x

Tactic:
rw [← StarOrderedRing.nonneg_iff] at x_mem y_mem

Premises used: StarOrderedRing.nonneg_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a x y : A
x_mem : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) x
y_mem : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) y
hx : SpectrumRestricts (R := ℝ≥0) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hy : SpectrumRestricts (R := ℝ≥0) (S := ℝ) y (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
x_mem₁ : 0 ≤ x
⊢ 0 ≤ y

Tactic:
rw [← StarOrderedRing.nonneg_iff] at x_mem y_mem

Premises used: StarOrderedRing.nonneg_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a x y : A
x_mem : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) x
y_mem : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) y
hx : SpectrumRestricts (R := ℝ≥0) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hy : SpectrumRestricts (R := ℝ≥0) (S := ℝ) y (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
x_mem₁ : 0 ≤ x
y_mem₁ : 0 ≤ y
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
rw [← StarOrderedRing.nonneg_iff] at x_mem y_mem

Premises used: StarOrderedRing.nonneg_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a x y : A
x_mem : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) x
y_mem : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) y
hx : SpectrumRestricts (R := ℝ≥0) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hy : SpectrumRestricts (R := ℝ≥0) (S := ℝ) y (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
x_mem₁ : 0 ≤ x
y_mem₁ : 0 ≤ y
hx₁ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) y (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
rw [← StarOrderedRing.nonneg_iff] at x_mem y_mem

Premises used: StarOrderedRing.nonneg_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a x y : A
x_mem : 0 ≤ x
y_mem : 0 ≤ y
hx : SpectrumRestricts (R := ℝ≥0) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hy : SpectrumRestricts (R := ℝ≥0) (S := ℝ) y (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) (x + y) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
hx.nnreal_add (.of_nonneg x_mem) (.of_nonneg y_mem) hy

Premises used: IsSelfAdjoint.of_nonneg, SpectrumRestricts.nnreal_add
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a x y : A
x_mem : 0 ≤ x
y_mem : 0 ≤ y
hx : SpectrumRestricts (R := ℝ≥0) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hy : SpectrumRestricts (R := ℝ≥0) (S := ℝ) y (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) (x + y) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
exact hx.nnreal_add (.of_nonneg x_mem) (.of_nonneg y_mem) hy

Premises used: IsSelfAdjoint.of_nonneg, SpectrumRestricts.nnreal_add
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) a
mem : ∀ (x : A) (hx : Membership.mem (γ := Set A) (Set.range fun (s : A) ↦ star s * s) x), ∀ x_1 ∈ spectrum ℝ x, 0 ≤ x_1
zero : ∀ x ∈ spectrum.{0, u_1} ℝ (A := A) 0, 0 ≤ x
add :
  ∀ (x y : A)
    (x_mem : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) x)
    (y_mem : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) y)
    (hx : ∀ x_1 ∈ spectrum ℝ x, 0 ≤ x_1) (hy : ∀ x ∈ spectrum ℝ y, 0 ≤ x), ∀ x_1 ∈ spectrum ℝ (x + y), 0 ≤ x_1
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Tactic:
induction ha using AddSubmonoid.closure_induction with
    | mem x hx =>
      obtain ⟨b, rfl⟩ := hx
      exact spectrum_star_mul_self_nonneg
    | zero =>
      nontriviality A
      simp
    | add x y x_mem y_mem hx hy =>
      rw [← SpectrumRestricts.nnreal_iff] at hx hy ⊢
      rw [← StarOrderedRing.nonneg_iff] at x_mem y_mem
      exact hx.nnreal_add (.of_nonneg x_mem) (.of_nonneg y_mem) hy

Premises used: SpectrumRestricts.nnreal_iff, spectrum_star_mul_self_nonneg, StarOrderedRing.nonneg_iff, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
x : ℂ
rw : x = 0 ∨ x ∈ spectrum ℂ a → 0 ≤ x
⊢ x ∈ σₙ ℂ a → 0 ≤ x

Tactic:
rw [mem_quasispectrum_iff]

Premises used: mem_quasispectrum_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
x : ℂ
⊢ x = 0 ∨ x ∈ spectrum ℂ a → 0 ≤ x

Tactic:
(Or.elim · ge_of_eq fun hx ↦ ?_)

Premises used: ge_of_eq, Or.elim
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
x : ℂ
refine : x = 0 ∨ x ∈ spectrum ℂ a → ∀ (hx : x ∈ spectrum ℂ a), 0 ≤ x
⊢ x = 0 ∨ x ∈ spectrum ℂ a → 0 ≤ x

Tactic:
refine (Or.elim · ge_of_eq fun hx ↦ ?_)

Premises used: ge_of_eq, Or.elim
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
x : ℂ
h : x = 0 ∨ x ∈ spectrum ℂ a
hx : x ∈ spectrum ℂ a
obtain :
  ∀ (y : ℝ) (hy : y ∈ spectrum ℝ a),
    Eq (α := ℂ) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) y : ℂ) (0 : ℂ) ∨
        Membership.mem (α := ℂ) (spectrum ℂ a) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) y : ℂ) →
      ∀ (hx : Membership.mem (α := ℂ) (spectrum ℂ a) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) y : ℂ)),
        LE.le (α := ℂ) (0 : ℂ) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) y : ℂ)
⊢ 0 ≤ x

Tactic:
obtain ⟨y, hy, rfl⟩ := (IsSelfAdjoint.of_nonneg ha).spectrumRestricts.algebraMap_image ▸ hx

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
y : ℝ
hy : y ∈ spectrum ℝ a
h :
  Eq (α := ℂ) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) y : ℂ) (0 : ℂ) ∨
    Membership.mem (α := ℂ) (spectrum ℂ a) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) y : ℂ)
hx : Membership.mem (α := ℂ) (spectrum ℂ a) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) y : ℂ)
⊢ LE.le (α := ℂ) (0 : ℂ) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) y : ℂ)

Tactic:
simpa using spectrum_nonneg_of_nonneg ha hy

Premises used: spectrum_nonneg_of_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
simp : QuasispectrumRestricts.{0, 0, u_1} (R := ℝ≥0) (S := ℝ) (A := A) 0 (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ ∀ (a : A),
    IsSelfAdjoint (a - a) ∧
      QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) (a - a) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
simp only [sub_self, IsSelfAdjoint.zero, true_and, forall_const]

Premises used: sub_self, IsSelfAdjoint.zero, forall_const, true_and
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
rw : ∀ x ∈ spectrum.{0, u_1} ℝ (A := Unitization ℂ A) (↑0 : Unitization ℂ A), 0 ≤ x
⊢ QuasispectrumRestricts.{0, 0, u_1} (R := ℝ≥0) (S := ℝ) (A := A) 0 (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
rw [quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ, SpectrumRestricts.nnreal_iff]

Premises used: quasispectrumRestricts_iff_spectrumRestricts_inr', SpectrumRestricts.nnreal_iff, Complex
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
⊢ Nontrivial A

Tactic:
nontriviality A
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
h : Nontrivial A
⊢ ∀ x ∈ spectrum.{0, u_1} ℝ (A := Unitization ℂ A) (↑0 : Unitization ℂ A), 0 ≤ x

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x y z : A
hxy :
  IsSelfAdjoint (y - x) ∧
    QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) (y - x) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hyz :
  IsSelfAdjoint (z - y) ∧
    QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) (z - y) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
simp :
  ∀
    (hxy :
      IsSelfAdjoint (R := Unitization ℂ A) (↑(y - x) : Unitization ℂ A) ∧
        SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑(y - x) : Unitization ℂ A)
          (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0))
    (hyz :
      IsSelfAdjoint (R := Unitization ℂ A) (↑(z - y) : Unitization ℂ A) ∧
        SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑(z - y) : Unitization ℂ A)
          (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)),
    IsSelfAdjoint (R := Unitization ℂ A) (↑(z - x) : Unitization ℂ A) ∧
      SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑(z - x) : Unitization ℂ A)
        (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ IsSelfAdjoint (z - x) ∧
    QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) (z - x) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
simp +singlePass only [← Unitization.isSelfAdjoint_inr (R := ℂ),
      quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ] at hxy hyz ⊢

Premises used: quasispectrumRestricts_iff_spectrumRestricts_inr', Unitization.isSelfAdjoint_inr, Complex
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x y z : A
hxy :
  IsSelfAdjoint (R := Unitization ℂ A) (↑(y - x) : Unitization ℂ A) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑(y - x) : Unitization ℂ A)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hyz :
  IsSelfAdjoint (R := Unitization ℂ A) (↑(z - y) : Unitization ℂ A) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑(z - y) : Unitization ℂ A)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ IsSelfAdjoint (R := Unitization ℂ A) (↑(z - x) : Unitization ℂ A)

Tactic:
simpa using hyz.1.add hxy.1

Premises used: And.left, IsSelfAdjoint.add
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x y z : A
hxy :
  IsSelfAdjoint (R := Unitization ℂ A) (↑(y - x) : Unitization ℂ A) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑(y - x) : Unitization ℂ A)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hyz :
  IsSelfAdjoint (R := Unitization ℂ A) (↑(z - y) : Unitization ℂ A) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑(z - y) : Unitization ℂ A)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑(z - x) : Unitization ℂ A)
    (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
simpa using hyz.2.nnreal_add hyz.1 hxy.1 hxy.2

Premises used: And.right, And.left, SpectrumRestricts.nnreal_add
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x y z : A
hxy :
  IsSelfAdjoint (R := Unitization ℂ A) (↑(y - x) : Unitization ℂ A) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑(y - x) : Unitization ℂ A)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hyz :
  IsSelfAdjoint (R := Unitization ℂ A) (↑(z - y) : Unitization ℂ A) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑(z - y) : Unitization ℂ A)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ IsSelfAdjoint (R := Unitization ℂ A) (↑(z - x) : Unitization ℂ A) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑(z - x) : Unitization ℂ A)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
exact ⟨by simpa using hyz.1.add hxy.1, by simpa using hyz.2.nnreal_add hyz.1 hxy.1 hxy.2⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x y : A
hxy :
  IsSelfAdjoint (y - x) ∧
    QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) (y - x) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hyx :
  IsSelfAdjoint (x - y) ∧
    QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) (x - y) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ IsSelfAdjoint (HSub.hSub (α := Unitization ℂ A) (↑y : Unitization ℂ A) (↑x : Unitization ℂ A)) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ)
      (HSub.hSub (α := Unitization ℂ A) (↑y : Unitization ℂ A) (↑x : Unitization ℂ A))
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
rw [← Unitization.isSelfAdjoint_inr (R := ℂ),
      quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ, Unitization.inr_sub ℂ] at hxy hyx

Premises used: quasispectrumRestricts_iff_spectrumRestricts_inr', Unitization.inr_sub, Unitization.isSelfAdjoint_inr, Complex
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x y : A
hxy :
  IsSelfAdjoint (y - x) ∧
    QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) (y - x) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hyx :
  IsSelfAdjoint (x - y) ∧
    QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) (x - y) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hxy₁ :
  IsSelfAdjoint (HSub.hSub (α := Unitization ℂ A) (↑y : Unitization ℂ A) (↑x : Unitization ℂ A)) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ)
      (HSub.hSub (α := Unitization ℂ A) (↑y : Unitization ℂ A) (↑x : Unitization ℂ A))
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ IsSelfAdjoint (HSub.hSub (α := Unitization ℂ A) (↑x : Unitization ℂ A) (↑y : Unitization ℂ A)) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ)
      (HSub.hSub (α := Unitization ℂ A) (↑x : Unitization ℂ A) (↑y : Unitization ℂ A))
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
rw [← Unitization.isSelfAdjoint_inr (R := ℂ),
      quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ, Unitization.inr_sub ℂ] at hxy hyx

Premises used: quasispectrumRestricts_iff_spectrumRestricts_inr', Unitization.inr_sub, Unitization.isSelfAdjoint_inr, Complex
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x y : A
hxy :
  IsSelfAdjoint (HSub.hSub (α := Unitization ℂ A) (↑y : Unitization ℂ A) (↑x : Unitization ℂ A)) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ)
      (HSub.hSub (α := Unitization ℂ A) (↑y : Unitization ℂ A) (↑x : Unitization ℂ A))
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hyx :
  IsSelfAdjoint (HSub.hSub (α := Unitization ℂ A) (↑x : Unitization ℂ A) (↑y : Unitization ℂ A)) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ)
      (HSub.hSub (α := Unitization ℂ A) (↑x : Unitization ℂ A) (↑y : Unitization ℂ A))
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
rw : x - y = 0
⊢ x = y

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x y : A
hxy :
  IsSelfAdjoint (HSub.hSub (α := Unitization ℂ A) (↑y : Unitization ℂ A) (↑x : Unitization ℂ A)) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ)
      (HSub.hSub (α := Unitization ℂ A) (↑y : Unitization ℂ A) (↑x : Unitization ℂ A))
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hyx :
  IsSelfAdjoint (HSub.hSub (α := Unitization ℂ A) (↑x : Unitization ℂ A) (↑y : Unitization ℂ A)) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ)
      (HSub.hSub (α := Unitization ℂ A) (↑x : Unitization ℂ A) (↑y : Unitization ℂ A))
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
a : Eq (α := Unitization ℂ A) (↑(x - y) : Unitization ℂ A) (↑0 : Unitization ℂ A)
⊢ x - y = 0

Tactic:
apply Unitization.inr_injective (R := ℂ)

Premises used: Unitization.inr_injective
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x y : A
hxy :
  IsSelfAdjoint (HSub.hSub (α := Unitization ℂ A) (↑y : Unitization ℂ A) (↑x : Unitization ℂ A)) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ)
      (HSub.hSub (α := Unitization ℂ A) (↑y : Unitization ℂ A) (↑x : Unitization ℂ A))
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hyx :
  IsSelfAdjoint (HSub.hSub (α := Unitization ℂ A) (↑x : Unitization ℂ A) (↑y : Unitization ℂ A)) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ)
      (HSub.hSub (α := Unitization ℂ A) (↑x : Unitization ℂ A) (↑y : Unitization ℂ A))
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
a : HSub.hSub (α := Unitization ℂ A) (↑x : Unitization ℂ A) (↑y : Unitization ℂ A) = 0
⊢ Eq (α := Unitization ℂ A) (↑(x - y) : Unitization ℂ A) (↑0 : Unitization ℂ A)

Tactic:
rw [Unitization.inr_zero, Unitization.inr_sub]

Premises used: Unitization.inr_sub, Unitization.inr_zero