awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  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)
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x
have h_eqOn : 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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x
have ha₁ : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) a
Tactic: rw [StarOrderedRing.nonneg_iff] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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
⊢ ∀ x_1 ∈ spectrum ℝ x, 0 ≤ x_1
have mem : ∀ (b : A), ∀ x ∈ spectrum.{0, u_1} ℝ (A := A) ((fun (s : A) ↦ star s * s) b), 0 ≤ x
Tactic: obtain ⟨b, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ ∀ x ∈ spectrum.{0, u_1} ℝ (A := A) 0, 0 ≤ x
have a₁ : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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
⊢ ∀ x_1 ∈ spectrum ℝ (x + y), 0 ≤ x_1
have 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)
Tactic: rw [← SpectrumRestricts.nnreal_iff] at hx hy ⊢
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
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)
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) (x + y) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
have x_mem₁ : 0 ≤ x
Tactic: rw [← StarOrderedRing.nonneg_iff] at x_mem y_mem
Cleared hypotheses: x_mem, y_mem, hx, hy
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
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
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) (x + y) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
have y_mem₁ : 0 ≤ y
Tactic: rw [← StarOrderedRing.nonneg_iff] at x_mem y_mem
Cleared hypotheses: x_mem, y_mem, hx, hy
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x
have mem : ∀ (x : A) (hx : Membership.mem (γ := Set A) (Set.range fun (s : A) ↦ star s * s) x), ∀ x_1 ∈ spectrum ℝ x, 0 ≤ x_1
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
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x
have zero : ∀ x ∈ spectrum.{0, u_1} ℝ (A := A) 0, 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
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x
have 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
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
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : 0 ≤ a
x : ℂ
⊢ x ∈ σₙ ℂ a → 0 ≤ x
have rw : x = 0 ∨ x ∈ spectrum ℂ a → 0 ≤ x
Tactic: rw [mem_quasispectrum_iff]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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
have refine : x = 0 ∨ x ∈ spectrum ℂ a → ∀ (hx : x ∈ spectrum ℂ a), 0 ≤ x
Tactic: refine (Or.elim · ge_of_eq fun hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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
⊢ 0 ≤ x
have 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 : ℂ)
Tactic: obtain ⟨y, hy, rfl⟩ := (IsSelfAdjoint.of_nonneg ha).spectrumRestricts.algebraMap_image ▸ hx
Cleared hypotheses: x, h, hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
⊢ ∀ (a : A),
    IsSelfAdjoint (a - a) ∧
      QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) (a - a) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
have simp : QuasispectrumRestricts.{0, 0, u_1} (R := ℝ≥0) (S := ℝ) (A := A) 0 (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
Tactic: simp only [sub_self, IsSelfAdjoint.zero, true_and, forall_const]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
⊢ QuasispectrumRestricts.{0, 0, u_1} (R := ℝ≥0) (S := ℝ) (A := A) 0 (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
have rw : ∀ x ∈ spectrum.{0, u_1} ℝ (A := Unitization ℂ A) (↑0 : Unitization ℂ A), 0 ≤ x
Tactic: rw [quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ, SpectrumRestricts.nnreal_iff]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
⊢ ∀ x ∈ spectrum.{0, u_1} ℝ (A := Unitization ℂ A) (↑0 : Unitization ℂ 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_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)
⊢ IsSelfAdjoint (z - x) ∧
    QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) (z - x) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
have 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)
Tactic: simp +singlePass only [← Unitization.isSelfAdjoint_inr (R := ℂ),
      quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ] at hxy hyz ⊢
Cleared hypotheses: hxy, hyz
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
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)
⊢ x = y
have 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)
Tactic: rw [← Unitization.isSelfAdjoint_inr (R := ℂ),
      quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ, Unitization.inr_sub ℂ] at hxy hyx
Cleared hypotheses: hxy, hyx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
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)
⊢ x = y
have 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)
Tactic: rw [← Unitization.isSelfAdjoint_inr (R := ℂ),
      quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ, Unitization.inr_sub ℂ] at hxy hyx
Cleared hypotheses: hxy, hyx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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)
⊢ x = y
have rw : x - y = 0
Tactic: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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)
⊢ x - y = 0
have a : Eq (α := Unitization ℂ A) (↑(x - y) : Unitization ℂ A) (↑0 : Unitization ℂ A)
Tactic: apply Unitization.inr_injective (R := ℂ)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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)
⊢ Eq (α := Unitization ℂ A) (↑(x - y) : Unitization ℂ A) (↑0 : Unitization ℂ A)
have a : HSub.hSub (α := Unitization ℂ A) (↑x : Unitization ℂ A) (↑y : Unitization ℂ A) = 0
Tactic: rw [Unitization.inr_zero, Unitization.inr_sub]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x y : A
⊢ x ≤ y ↔
    ∃ (p : A),
      Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) p ∧ y = x + p
have mp : x ≤ y →
  ∃ (p : A),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) p ∧ y = x + p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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
⊢ x ≤ y ↔
    ∃ (p : A),
      Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) p ∧ y = x + p
have mpr : (∃ (p : A),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) p ∧ y = x + p) →
  x ≤ y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x y : A
h : x ≤ y
⊢ ∃ (p : A),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) p ∧ y = x + p
have 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
Tactic: obtain ⟨s, hs₁, _, hs₂⟩ :=
          CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts h.1 h.2
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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
⊢ y = x + s * s
have rwa : ∀ (hs₂ : x + s * s = y), y = x + s * s
Tactic: rwa [eq_sub_iff_add_eq', eq_comm] at hs₂
Cleared hypotheses: hs₂
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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
⊢ y = x + s * s
have rwa₁ : ∀ (hs₂ : y = x + s * s), y = x + s * s
Tactic: rwa [eq_sub_iff_add_eq', eq_comm] at hs₂
Cleared hypotheses: hs₂
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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
⊢ ∃ (p : A),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) p ∧ y = x + p
have mp : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (Set.range fun (s : A) ↦ star s * s)) (s * s)
Tactic: refine ⟨s * s, ?_, by rwa [eq_sub_iff_add_eq', eq_comm] at hs₂⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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
⊢ x ≤ x + p
have mpr : IsSelfAdjoint p ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) p (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
Tactic: simp +instances only [spectralOrder, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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
⊢ IsSelfAdjoint x ∧ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
have 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)
Tactic: obtain ⟨s, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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)
have mpr : 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, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x p s : A
⊢ QuasispectrumRestricts.{0, 0, u_1} (R := ℝ≥0) (S := ℝ) (A := A) ((fun (s : A) ↦ star s * s) s)
    (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
have mpr : ∀ x ∈ spectrum ℝ (HMul.hMul (α := Unitization ℂ A) (star (↑s : Unitization ℂ A)) (↑s : Unitization ℂ A)), 0 ≤ x
Tactic: rw [quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ,
            SpectrumRestricts.nnreal_iff, Unitization.inr_mul, Unitization.inr_star]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
x_1 : PartialOrder A := spectralOrder A
x p : A
⊢ IsSelfAdjoint.{u_1} (R := A) 0 ∧
    QuasispectrumRestricts.{0, 0, u_1} (R := ℝ≥0) (S := ℝ) (A := A) 0 (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
have mpr : IsSelfAdjoint.{u_1} (R := A) 0 ∧ ∀ x ∈ spectrum.{0, u_1} ℝ (A := Unitization ℂ A) (↑0 : Unitization ℂ A), 0 ≤ x
Tactic: rw [quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ, SpectrumRestricts.nnreal_iff]