awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ
hr : r ≤ 0
a : A
⊢ (r • a)⁺ = -r • a⁻
have nth_rw : (- -r • a)⁺ = -r • a⁻
Tactic: nth_rw 1 [← neg_neg r]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ
hr : r ≤ 0
a : A
⊢ (- -r • a)⁺ = -r • a⁻
have rw : (-(-r • a))⁺ = -r • a⁻
Tactic: rw [neg_smul, ← smul_neg, posPart_smul_of_nonneg (neg_nonneg.mpr hr), posPart_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ
hr : r ≤ 0
a : A
rw : (-(-r • a))⁺ = -r • a⁻
⊢ (- -r • a)⁺ = -r • a⁻
have rw₁ : (-r • -a)⁺ = -r • a⁻
Tactic: rw [neg_smul, ← smul_neg, posPart_smul_of_nonneg (neg_nonneg.mpr hr), posPart_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ
hr : r ≤ 0
a : A
rw : (-(-r • a))⁺ = -r • a⁻
rw₁ : (-r • -a)⁺ = -r • a⁻
⊢ (- -r • a)⁺ = -r • a⁻
have rw₂ : -r • (-a)⁺ = -r • a⁻
Tactic: rw [neg_smul, ← smul_neg, posPart_smul_of_nonneg (neg_nonneg.mpr hr), posPart_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ
hr : r ≤ 0
a : A
rw : (-(-r • a))⁺ = -r • a⁻
rw₁ : (-r • -a)⁺ = -r • a⁻
rw₂ : -r • (-a)⁺ = -r • a⁻
⊢ (- -r • a)⁺ = -r • a⁻
have rw₃ : -r • a⁻ = -r • a⁻
Tactic: rw [neg_smul, ← smul_neg, posPart_smul_of_nonneg (neg_nonneg.mpr hr), posPart_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ
hr : 0 ≤ r
a : A
| (r • a)⁻
have rw : r • a⁻
Tactic: rw [← neg_neg r, neg_smul, negPart_neg, posPart_smul_of_nonpos (by simpa), neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ
hr : 0 ≤ r
a : A
⊢ (r • a)⁻ = r • a⁻
have conv_lhs : (r • a)⁻ = r • a⁻
Tactic: conv_lhs => rw [← neg_neg r, neg_smul, negPart_neg, posPart_smul_of_nonpos (by simpa), neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ
hr : 0 ≤ r
a : A
conv_lhs : (r • a)⁻ = r • a⁻
⊢ (r • a)⁻ = r • a⁻
have conv_lhs₁ : r • a⁻ = r • a⁻
Tactic: conv_lhs => rw [← neg_neg r, neg_smul, negPart_neg, posPart_smul_of_nonpos (by simpa), neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ
hr : r ≤ 0
a : A
| (r • a)⁻
have rw : -r • a⁺
Tactic: rw [← neg_neg r, neg_smul, negPart_neg, posPart_smul_of_nonneg (by simpa)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ
hr : r ≤ 0
a : A
⊢ (r • a)⁻ = -r • a⁺
have conv_lhs : (r • a)⁻ = -r • a⁺
Tactic: conv_lhs => rw [← neg_neg r, neg_smul, negPart_neg, posPart_smul_of_nonneg (by simpa)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : T2Space A
inst_8 : StarModule ℝ A
r : ℝ
hr : r ≤ 0
a : A
conv_lhs : (r • a)⁻ = -r • a⁺
⊢ (r • a)⁻ = -r • a⁺
have conv_lhs₁ : -r • a⁺ = -r • a⁺
Tactic: conv_lhs => rw [← neg_neg r, neg_smul, negPart_neg, posPart_smul_of_nonneg (by simpa)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
a b : A
hab : a = b - a⁻
hb : 0 ≤ b
⊢ a⁺ = b
have ha : IsSelfAdjoint a
Tactic: have ha := hab.symm ▸ hb.isSelfAdjoint.sub (negPart_nonneg a).isSelfAdjoint
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
a b : A
hab : a = b - a⁻
hb : 0 ≤ b
ha : IsSelfAdjoint a
⊢ a⁺ = b
have hab₁ : a⁺ - a⁻ = b - a⁻
Tactic: nth_rw 1 [← posPart_sub_negPart a] at hab
Cleared hypotheses: hab, hb, ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
a c : A
hac : a = a⁺ - c
hc : 0 ≤ c
⊢ a⁻ = c
have ha : IsSelfAdjoint a
Tactic: have ha := hac.symm ▸ (posPart_nonneg a).isSelfAdjoint.sub hc.isSelfAdjoint
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
a c : A
hac : a = a⁺ - c
hc : 0 ≤ c
ha : IsSelfAdjoint a
⊢ a⁻ = c
have hac₁ : a⁺ - a⁻ = a⁺ - c
Tactic: nth_rw 1 [← posPart_sub_negPart a] at hac
Cleared hypotheses: hac, hc, ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
⊢ a⁺ = a ↔ 0 ≤ a
have refine : ∀ (ha : 0 ≤ a), a⁺ = a
Tactic: refine ⟨fun ha ↦ ha ▸ posPart_nonneg a, fun ha ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ a
| a
have rw : cfcₙ (R := ℝ) (p := IsSelfAdjoint) id a
Tactic: rw [← cfcₙ_id ℝ a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ a
⊢ a⁺ = a
have conv_rhs : a⁺ = cfcₙ (R := ℝ) (p := IsSelfAdjoint) id a
Tactic: conv_rhs => rw [← cfcₙ_id ℝ a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺) a = cfcₙ (R := ℝ) (p := IsSelfAdjoint) id a
have refine : ∀ (x : ℝ) (hx : x ∈ quasispectrum ℝ a), x⁺ = id x
Tactic: refine cfcₙ_congr (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
ha : IsSelfAdjoint a
⊢ a⁻ = 0 ↔ 0 ≤ a
have rw : a⁻ = 0 ↔ a = a⁺
Tactic: rw [← posPart_eq_self, eq_comm (b := a)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
ha : IsSelfAdjoint a
⊢ a⁻ = 0 ↔ a = a⁺
have nth_rw : a⁻ = 0 ↔ a⁺ - a⁻ = a⁺
Tactic: nth_rw 2 [← posPart_sub_negPart a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
⊢ a⁻ = -a ↔ a ≤ 0
have rw : a = -a⁻ ↔ a ≤ 0
Tactic: rw [← neg_inj, neg_neg, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
ha : a = -a⁻
⊢ a ≤ 0
have rw : 0 ≤ a⁻
Tactic: rw [ha, neg_nonpos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
⊢ a = -a⁻ ↔ a ≤ 0
have refine : ∀ (ha : a ≤ 0), a = -a⁻
Tactic: refine ⟨fun ha ↦ by rw [ha, neg_nonpos]; exact negPart_nonneg a, fun ha ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
ha : a ≤ 0
⊢ a = -a⁻
have ha₁ : 0 ≤ -a
Tactic: rw [← neg_nonneg] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ -a
⊢ a = -a⁻
have rw : a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ -x⁻) a
Tactic: rw [negPart_def, ← cfcₙ_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ -a
⊢ a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ -x⁻) a
have x : IsSelfAdjoint a
Tactic: have _ : IsSelfAdjoint a := neg_neg a ▸ (IsSelfAdjoint.neg <| .of_nonneg ha)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ -a
h : IsSelfAdjoint a
| a
have rw : cfcₙ (R := ℝ) (p := IsSelfAdjoint) id a
Tactic: rw [← cfcₙ_id ℝ a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ -a
h : IsSelfAdjoint a
⊢ a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ -x⁻) a
have conv_lhs : cfcₙ (R := ℝ) (p := IsSelfAdjoint) id a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ -x⁻) a
Tactic: conv_lhs => rw [← cfcₙ_id ℝ a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ -a
h : IsSelfAdjoint a
⊢ cfcₙ (R := ℝ) (p := IsSelfAdjoint) id a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ -x⁻) a
have refine : ∀ (x : ℝ) (hx : x ∈ quasispectrum ℝ a), id x = -x⁻
Tactic: refine cfcₙ_congr fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ -a
h : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
⊢ id x = -x⁻
have hx₁ : -x ∈ quasispectrum ℝ (-a)
Tactic: rw [Unitization.quasispectrum_eq_spectrum_inr ℝ, ← neg_neg x, ← Set.mem_neg,
    spectrum.neg_eq, ← Unitization.inr_neg, ← Unitization.quasispectrum_eq_spectrum_inr ℝ] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ -a
h : IsSelfAdjoint a
x : ℝ
hx : -x ∈ quasispectrum ℝ (-a)
⊢ id x = -x⁻
have rw : x⁻ = -id x
Tactic: rw [← neg_eq_iff_eq_neg, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
ha : IsSelfAdjoint a
⊢ a⁺ = 0 ↔ a ≤ 0
have rw : a⁺ = 0 ↔ -a = a⁻
Tactic: rw [← negPart_eq_neg, eq_comm (b := -a)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
a : A
ha : IsSelfAdjoint a
⊢ a⁺ = 0 ↔ -a = a⁻
have nth_rw : a⁺ = 0 ↔ -(a⁺ - a⁻) = a⁻
Tactic: nth_rw 2 [← posPart_sub_negPart a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
⊢ a⁺ = b ∧ a⁻ = c
have hb' : IsSelfAdjoint b
Tactic: have hb' : IsSelfAdjoint b := .of_nonneg hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
⊢ a⁺ = b ∧ a⁻ = c
have hc' : IsSelfAdjoint (-c)
Tactic: have hc' : IsSelfAdjoint (-c) := .neg <| .of_nonneg hc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
⊢ a⁺ = b ∧ a⁻ = c
have ha : IsSelfAdjoint a
Tactic: have ha : IsSelfAdjoint a := habc ▸ hb'.sub <| .of_nonneg hc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
⊢ a⁺ = b ∧ a⁻ = c
have rw : a⁺ = b
Tactic: rw [and_iff_left_of_imp ?of_b_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
rw : a⁺ = b
⊢ a⁺ = b ∧ a⁻ = c
have rw₁ : a⁺ = b → a⁻ = c
Tactic: rw [and_iff_left_of_imp ?of_b_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
⊢ CompactSpace (↑s : Type)
have refine_1 : IsCompact (σₙ ℝ a)
Tactic: refine isCompact_iff_compactSpace.mp <| (IsCompact.union ?_ ?_).union ?_