awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ HSub.hSub (α := Unitization ℂ A) (↑x : Unitization ℂ A) (↑y : Unitization ℂ A) = 0

Tactic:
hyx.2.eq_zero_of_neg hyx.1 (neg_sub (x : A⁺¹) (y : A⁺¹) ▸ hxy.2)

Premises used: neg_sub, Unitization.inr, Eq.rec, SpectrumRestricts.eq_zero_of_neg, And.right, And.left, Eq.symm
-- 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)
⊢ HSub.hSub (α := Unitization ℂ A) (↑x : Unitization ℂ A) (↑y : Unitization ℂ A) = 0

Tactic:
exact hyx.2.eq_zero_of_neg hyx.1 (neg_sub (x : A⁺¹) (y : A⁺¹) ▸ hxy.2)

Premises used: neg_sub, Unitization.inr, Eq.rec, SpectrumRestricts.eq_zero_of_neg, And.right, And.left, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x y : A
mp :
  x ≤ y →
    ∃ (p : A),
      Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) p ∧ y = x + p
mpr :
  (∃ (p : A),
      Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) p ∧ y = x + p) →
    x ≤ y
⊢ x ≤ y ↔
    ∃ (p : A),
      Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) p ∧ y = x + p

Tactic:
constructor
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x y : A
h : x ≤ y
mp :
  ∀ (s : A) (hs₁ : IsSelfAdjoint s),
    QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) s (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) →
      ∀ (hs₂ : s * s = y - x),
        ∃ (p : A),
          Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) p ∧ y = x + p
⊢ ∃ (p : A),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) p ∧ y = x + p

Tactic:
obtain ⟨s, hs₁, _, hs₂⟩ :=
          CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts h.1 h.2

Premises used: CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts, And.right, And.left
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x y : A
h : x ≤ y
s : A
hs₁ : IsSelfAdjoint s
left : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) s (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hs₂ : s * s = y - x
rwa : ∀ (hs₂ : x + s * s = y), y = x + s * s
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hs₂ : y = x + s * s), y = x + s * s
⊢ y = x + s * s

Tactic:
rwa [eq_sub_iff_add_eq', eq_comm] at hs₂

Premises used: eq_sub_iff_add_eq', eq_comm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x y : A
h : x ≤ y
s : A
hs₁ : IsSelfAdjoint s
left : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) s (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hs₂ : s * s = y - x
mp : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) (s * s)
⊢ ∃ (p : A),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) p ∧ y = x + p

Tactic:
refine ⟨s * s, ?_, by rwa [eq_sub_iff_add_eq', eq_comm] at hs₂⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x y : A
h : x ≤ y
s : A
hs₁ : IsSelfAdjoint s
left : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) s (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hs₂ : s * s = y - x
⊢ (fun (s : A) ↦ star s * s) s = s * s

Tactic:
simp [hs₁.star_eq]

Premises used: IsSelfAdjoint.star_eq
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x y : A
h : x ≤ y
s : A
hs₁ : IsSelfAdjoint s
left : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) s (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hs₂ : s * s = y - x
⊢ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) (s * s)

Tactic:
exact AddSubmonoid.subset_closure ⟨s, by simp [hs₁.star_eq]⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x p : A
hp : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) p
mpr : IsSelfAdjoint p ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) p (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ x ≤ x + p

Tactic:
simp +instances only [spectralOrder, add_sub_cancel_left]

Premises used: CStarAlgebra.spectralOrder, add_sub_cancel_left
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x_2 p x : A
hx : Membership.mem (γ := Set A) (Set.range fun (s : A) ↦ star s * s) x
mpr :
  ∀ (s : A),
    IsSelfAdjoint.{u_1} (R := A) ((fun (s : A) ↦ star s * s) s) ∧
      QuasispectrumRestricts.{0, 0, u_1} (R := ℝ≥0) (S := ℝ) (A := A) ((fun (s : A) ↦ star s * s) s)
        (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ IsSelfAdjoint x ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
obtain ⟨s, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x p s : A
⊢ IsSelfAdjoint.{u_1} (R := A) ((fun (s : A) ↦ star s * s) s) ∧
    QuasispectrumRestricts.{0, 0, u_1} (R := ℝ≥0) (S := ℝ) (A := A) ((fun (s : A) ↦ star s * s) s)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
⟨IsSelfAdjoint.star_mul_self s, ?_⟩

Premises used: IsSelfAdjoint.star_mul_self, And.intro
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x p s : A
mpr :
  QuasispectrumRestricts.{0, 0, u_1} (R := ℝ≥0) (S := ℝ) (A := A) ((fun (s : A) ↦ star s * s) s)
    (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ IsSelfAdjoint.{u_1} (R := A) ((fun (s : A) ↦ star s * s) s) ∧
    QuasispectrumRestricts.{0, 0, u_1} (R := ℝ≥0) (S := ℝ) (A := A) ((fun (s : A) ↦ star s * s) s)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
refine ⟨IsSelfAdjoint.star_mul_self s, ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x p s : A
mpr : ∀ x ∈ spectrum ℝ (HMul.hMul (α := Unitization ℂ A) (star (↑s : Unitization ℂ A)) (↑s : Unitization ℂ A)), 0 ≤ x
⊢ QuasispectrumRestricts.{0, 0, u_1} (R := ℝ≥0) (S := ℝ) (A := A) ((fun (s : A) ↦ star s * s) s)
    (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

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

Premises used: quasispectrumRestricts_iff_spectrumRestricts_inr', SpectrumRestricts.nnreal_iff, Unitization.inr_star, Unitization.inr_mul, Complex
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x p s : A
⊢ ∀ x ∈ spectrum ℝ (HMul.hMul (α := Unitization ℂ A) (star (↑s : Unitization ℂ A)) (↑s : Unitization ℂ A)), 0 ≤ x

Tactic:
spectrum_star_mul_self_nonneg

Premises used: Set.Mem, Unitization.inl, spectrum_star_mul_self_nonneg, Unitization.inlRingHom
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x p s : A
⊢ ∀ x ∈ spectrum ℝ (HMul.hMul (α := Unitization ℂ A) (star (↑s : Unitization ℂ A)) (↑s : Unitization ℂ A)), 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 : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x p : A
mpr : IsSelfAdjoint.{u_1} (R := A) 0 ∧ ∀ x ∈ spectrum.{0, u_1} ℝ (A := Unitization ℂ A) (↑0 : Unitization ℂ A), 0 ≤ x
⊢ IsSelfAdjoint.{u_1} (R := A) 0 ∧
    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
x_1 : PartialOrder A := spectralOrder A
x p : A
⊢ IsSelfAdjoint.{u_1} (R := A) 0 ∧ ∀ 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_1 : PartialOrder A := spectralOrder A
x_2 p x y : A
hx_1 : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) x
hy_1 : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) y
hx : IsSelfAdjoint x ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hy : IsSelfAdjoint y ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) y (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
mpr :
  ∀
    (hx :
      IsSelfAdjoint (R := Unitization ℂ A) (↑x : Unitization ℂ A) ∧
        SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑x : Unitization ℂ A)
          (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0))
    (hy :
      IsSelfAdjoint (R := Unitization ℂ A) (↑y : Unitization ℂ A) ∧
        SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑y : Unitization ℂ A)
          (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)),
    IsSelfAdjoint (R := Unitization ℂ A) (↑(x + y) : Unitization ℂ A) ∧
      SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑(x + y) : Unitization ℂ A)
        (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ IsSelfAdjoint (x + y) ∧
    QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) (x + y) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

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

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_1 : PartialOrder A := spectralOrder A
x_2 p x y : A
hx_1 : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) x
hy_1 : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) y
hx :
  IsSelfAdjoint (R := Unitization ℂ A) (↑x : Unitization ℂ A) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑x : Unitization ℂ A)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hy :
  IsSelfAdjoint (R := Unitization ℂ A) (↑y : Unitization ℂ A) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑y : Unitization ℂ A)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
mpr :
  IsSelfAdjoint (HAdd.hAdd (α := Unitization ℂ A) (↑x : Unitization ℂ A) (↑y : Unitization ℂ A)) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ)
      (HAdd.hAdd (α := Unitization ℂ A) (↑x : Unitization ℂ A) (↑y : Unitization ℂ A))
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ IsSelfAdjoint (R := Unitization ℂ A) (↑(x + y) : Unitization ℂ A) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑(x + y) : Unitization ℂ A)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
rw [Unitization.inr_add]

Premises used: Unitization.inr_add
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x_2 p x y : A
hx_1 : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) x
hy_1 : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) y
hx :
  IsSelfAdjoint (R := Unitization ℂ A) (↑x : Unitization ℂ A) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑x : Unitization ℂ A)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hy :
  IsSelfAdjoint (R := Unitization ℂ A) (↑y : Unitization ℂ A) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑y : Unitization ℂ A)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ IsSelfAdjoint (HAdd.hAdd (α := Unitization ℂ A) (↑x : Unitization ℂ A) (↑y : Unitization ℂ A)) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ)
      (HAdd.hAdd (α := Unitization ℂ A) (↑x : Unitization ℂ A) (↑y : Unitization ℂ A))
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
⟨hx.1.add hy.1, hx.2.nnreal_add hx.1 hy.1 hy.2⟩

Premises used: And.right, And.left, And.intro, IsSelfAdjoint.add, SpectrumRestricts.nnreal_add
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x_2 p x y : A
hx_1 : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) x
hy_1 : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) y
hx :
  IsSelfAdjoint (R := Unitization ℂ A) (↑x : Unitization ℂ A) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑x : Unitization ℂ A)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hy :
  IsSelfAdjoint (R := Unitization ℂ A) (↑y : Unitization ℂ A) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℂ A) (↑y : Unitization ℂ A)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ IsSelfAdjoint (HAdd.hAdd (α := Unitization ℂ A) (↑x : Unitization ℂ A) (↑y : Unitization ℂ A)) ∧
    SpectrumRestricts (R := ℝ≥0) (S := ℝ)
      (HAdd.hAdd (α := Unitization ℂ A) (↑x : Unitization ℂ A) (↑y : Unitization ℂ A))
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
exact ⟨hx.1.add hy.1, hx.2.nnreal_add hx.1 hy.1 hy.2⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x p : A
hp : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) p
mpr :
  ∀ (x : A) (hx : Membership.mem (γ := Set A) (Set.range fun (s : A) ↦ star s * s) x),
    IsSelfAdjoint x ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
mpr₁ :
  IsSelfAdjoint.{u_1} (R := A) 0 ∧
    QuasispectrumRestricts.{0, 0, u_1} (R := ℝ≥0) (S := ℝ) (A := A) 0 (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
mpr₂ :
  ∀ (x y : A),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) x →
      Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) y →
        ∀
          (hx :
            IsSelfAdjoint x ∧
              QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0))
          (hy :
            IsSelfAdjoint y ∧
              QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) y (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)),
          IsSelfAdjoint (x + y) ∧
            QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) (x + y) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ IsSelfAdjoint p ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) p (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
induction hp using AddSubmonoid.closure_induction with
        | mem x hx =>
          obtain ⟨s, rfl⟩ := hx
          refine ⟨IsSelfAdjoint.star_mul_self s, ?_⟩
          rw [quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ,
            SpectrumRestricts.nnreal_iff, Unitization.inr_mul, Unitization.inr_star]
          exact spectrum_star_mul_self_nonneg
        | zero =>
          rw [quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ, SpectrumRestricts.nnreal_iff]
          simp
        | add x y _ _ hx hy =>
          simp +singlePass only [← Unitization.isSelfAdjoint_inr (R := ℂ),
            quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ] at hx hy ⊢
          rw [Unitization.inr_add]
          exact ⟨hx.1.add hy.1, hx.2.nnreal_add hx.1 hy.1 hy.2⟩

Premises used: quasispectrumRestricts_iff_spectrumRestricts_inr', SpectrumRestricts.nnreal_iff, Unitization.inr_star, spectrum_star_mul_self_nonneg, Unitization.inr_mul, Unitization.isSelfAdjoint_inr, Unitization.inr_add, Complex, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
rw : ∀ x ∈ spectrum ℝ (A := Unitization ℂ A) (↑a : Unitization ℂ A), 0 ≤ x
⊢ ∀ x ∈ σₙ ℝ a, 0 ≤ x

Tactic:
rw [Unitization.quasispectrum_eq_spectrum_inr' _ ℂ]

Premises used: Unitization.quasispectrum_eq_spectrum_inr', Complex
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
x : PartialOrder (Unitization ℂ A) := spectralOrder (Unitization ℂ A)
⊢ StarOrderedRing.{u_1} (Unitization ℂ A)

Tactic:
have := CStarAlgebra.spectralOrderedRing A⁺¹
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
x : PartialOrder (Unitization ℂ A) := spectralOrder (Unitization ℂ A)
this : StarOrderedRing.{u_1} (Unitization ℂ A)
ha₁ : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
⊢ ∀ x ∈ spectrum ℝ (A := Unitization ℂ A) (↑a : Unitization ℂ A), 0 ≤ x

Tactic:
apply spectrum_nonneg_of_nonneg

Premises used: spectrum_nonneg_of_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
x : PartialOrder (Unitization ℂ A) := spectralOrder (Unitization ℂ A)
this : StarOrderedRing.{u_1} (Unitization ℂ A)
ha₁ :
  ∀ (ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) a)
    (this : StarOrderedRing.{u_1} (Unitization ℂ A)),
    Membership.mem (γ := AddSubmonoid (Unitization ℂ A))
      (AddSubmonoid.closure (Set.range fun (s : Unitization ℂ A) ↦ star s * s)) (↑a : Unitization ℂ A)
⊢ LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ 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 : NonUnitalCStarAlgebra 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
x : PartialOrder (Unitization ℂ A) := spectralOrder (Unitization ℂ A)
this : StarOrderedRing.{u_1} (Unitization ℂ A)
⊢ Membership.mem (α := Unitization ℂ A) (γ := AddSubmonoid (Unitization ℂ A))
    (AddSubmonoid.map (F := A →⋆ₙₐ[ℂ] Unitization ℂ A) (Unitization.inrNonUnitalStarAlgHom ℂ A)
      (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)))
    ((Unitization.inrNonUnitalStarAlgHom ℂ A : (a : A) → Unitization ℂ A) a : Unitization ℂ A)

Tactic:
have := AddSubmonoid.mem_map_of_mem (Unitization.inrNonUnitalStarAlgHom ℂ A) ha
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra 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
x : PartialOrder (Unitization ℂ A) := spectralOrder (Unitization ℂ A)
this_1 : StarOrderedRing.{u_1} (Unitization ℂ A)
this :
  Membership.mem (α := Unitization ℂ A) (γ := AddSubmonoid (Unitization ℂ A))
    (AddSubmonoid.map (F := A →⋆ₙₐ[ℂ] Unitization ℂ A) (Unitization.inrNonUnitalStarAlgHom ℂ A)
      (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)))
    ((Unitization.inrNonUnitalStarAlgHom ℂ A : (a : A) → Unitization ℂ A) a : Unitization ℂ A)
⊢ Membership.mem (α := Unitization ℂ A) (γ := AddSubmonoid (Unitization ℂ A))
    (AddSubmonoid.closure
      (Set.range (ι := A)
        (Function.comp (β := A) (⇑(Unitization.inrNonUnitalStarAlgHom ℂ A) : (a : A) → Unitization ℂ A) fun (s : A) ↦
          star s * s)))
    ((Unitization.inrNonUnitalStarAlgHom ℂ A : (a : A) → Unitization ℂ A) a : Unitization ℂ A)

Tactic:
rw [AddMonoidHom.map_mclosure, ← Set.range_comp] at this

Premises used: Set.range_comp, AddMonoidHom.map_mclosure
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra 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
x : PartialOrder (Unitization ℂ A) := spectralOrder (Unitization ℂ A)
this_1 : StarOrderedRing.{u_1} (Unitization ℂ A)
this :
  Membership.mem (α := Unitization ℂ A) (γ := AddSubmonoid (Unitization ℂ A))
    (AddSubmonoid.closure
      (Set.range (ι := A)
        (Function.comp (β := A) (⇑(Unitization.inrNonUnitalStarAlgHom ℂ A) : (a : A) → Unitization ℂ A) fun (s : A) ↦
          star s * s)))
    ((Unitization.inrNonUnitalStarAlgHom ℂ A : (a : A) → Unitization ℂ A) a : Unitization ℂ A)
apply :
  Subset (α := Set (Unitization ℂ A))
    (Set.range (ι := A)
      (Function.comp (β := A) (⇑(Unitization.inrNonUnitalStarAlgHom ℂ A) : (a : A) → Unitization ℂ A) fun (s : A) ↦
        star s * s))
    (Set.range fun (s : Unitization ℂ A) ↦ star s * s)
⊢ Membership.mem (γ := AddSubmonoid (Unitization ℂ A))
    (AddSubmonoid.closure (Set.range fun (s : Unitization ℂ A) ↦ star s * s)) (↑a : Unitization ℂ A)

Tactic:
apply AddSubmonoid.closure_mono ?_ this

Premises used: AddSubmonoid.closure_mono