awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : IsScalarTower ℝ A A
inst_5 : SMulCommClass ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : ∀ x ∈ σₙ ℝ a, 0 ≤ x
x : ℝ
hx : 0 ≤ x
⊢ √x * √x = id x

Tactic:
simp [← sq, Real.sq_sqrt hx]

Premises used: Real.sq_sqrt, sq
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a : A
⊢ 0 ≤ a ↔
    IsSelfAdjoint a ∧ QuasispectrumRestricts (R := NNReal) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)

Tactic:
⟨fun ha ↦ ⟨.of_nonneg ha, .nnreal_of_nonneg ha⟩, ?_⟩

Premises used: IsSelfAdjoint.of_nonneg, And.intro, Iff.intro, QuasispectrumRestricts.nnreal_of_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a : A
refine :
  IsSelfAdjoint a ∧ QuasispectrumRestricts (R := NNReal) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal) →
    0 ≤ a
⊢ 0 ≤ a ↔
    IsSelfAdjoint a ∧ QuasispectrumRestricts (R := NNReal) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)

Tactic:
refine ⟨fun ha ↦ ⟨.of_nonneg ha, .nnreal_of_nonneg ha⟩, ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a : A
ha₁ : IsSelfAdjoint a
ha₂ : QuasispectrumRestricts (R := NNReal) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
obtain :
  ∀ (x : A) (hx : IsSelfAdjoint x) (ha₁ : IsSelfAdjoint (x * x))
    (ha₂ : QuasispectrumRestricts (R := NNReal) (S := ℝ) (x * x) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)),
    0 ≤ x * x
⊢ 0 ≤ a

Tactic:
obtain ⟨x, hx, -, rfl⟩ := CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts ha₁ ha₂

Premises used: CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
x : A
hx : IsSelfAdjoint x
ha₁ : IsSelfAdjoint (x * x)
ha₂ : QuasispectrumRestricts (R := NNReal) (S := ℝ) (x * x) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
⊢ 0 ≤ x * x

Tactic:
simpa [sq, hx.star_eq] using star_mul_self_nonneg x

Premises used: sq, star_mul_self_nonneg, IsSelfAdjoint.star_eq
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
⊢ NonUnitalContinuousFunctionalCalculus ℝ≥0 A fun (x : A) ↦ 0 ≤ x

Tactic:
QuasispectrumRestricts.cfc (q := IsSelfAdjoint) ContinuousMap.realToNNReal
    NNReal.isClosedEmbedding_coe le_rfl
    (fun _ ↦ nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts)

Premises used: le_rfl, NNReal.isClosedEmbedding_coe, ContinuousMap.realToNNReal, QuasispectrumRestricts.cfc, nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
h : Commute a b
rw :
  IsSelfAdjoint (a * b) ∧
    QuasispectrumRestricts (R := NNReal) (S := ℝ) (a * b) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
⊢ 0 ≤ a * b

Tactic:
rw [nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts]

Premises used: nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
h : Commute a b
⊢ IsSelfAdjoint (a * b) ∧
    QuasispectrumRestricts (R := NNReal) (S := ℝ) (a * b) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)

Tactic:
⟨ha.isSelfAdjoint.commute_iff hb.isSelfAdjoint |>.mp h, ?_⟩

Premises used: LE.le.isSelfAdjoint, IsSelfAdjoint.commute_iff, And.intro, Iff.mp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
h : Commute a b
refine : QuasispectrumRestricts (R := NNReal) (S := ℝ) (a * b) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
⊢ IsSelfAdjoint (a * b) ∧
    QuasispectrumRestricts (R := NNReal) (S := ℝ) (a * b) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)

Tactic:
refine ⟨ha.isSelfAdjoint.commute_iff hb.isSelfAdjoint |>.mp h, ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
h : Commute a b
⊢ IsSelfAdjoint b ∧ QuasispectrumRestricts (R := NNReal) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)

Tactic:
rw [nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts] at hb

Premises used: nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
h : Commute a b
hb₁ : IsSelfAdjoint b ∧ QuasispectrumRestricts (R := NNReal) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
⊢ Commute a b

Tactic:
rw [nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts] at hb

Premises used: nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a b : A
ha : 0 ≤ a
hb : IsSelfAdjoint b ∧ QuasispectrumRestricts (R := NNReal) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
h : Commute a b
obtain :
  ∀ (x : A) (hx₁ : IsSelfAdjoint x)
    (hx₂ : QuasispectrumRestricts (R := NNReal) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal))
    (hb :
      IsSelfAdjoint (x * x) ∧
        QuasispectrumRestricts (R := NNReal) (S := ℝ) (x * x) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal))
    (h : Commute a (x * x)),
    QuasispectrumRestricts (R := NNReal) (S := ℝ) (a * (x * x)) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
⊢ QuasispectrumRestricts (R := NNReal) (S := ℝ) (a * b) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)

Tactic:
obtain ⟨x, hx₁, hx₂, rfl⟩ := CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts hb.1 hb.2

Premises used: CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts, And.right, And.left, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ a
x : A
hx₁ : IsSelfAdjoint x
hx₂ : QuasispectrumRestricts (R := NNReal) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
hb :
  IsSelfAdjoint (x * x) ∧
    QuasispectrumRestricts (R := NNReal) (S := ℝ) (x * x) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
h : Commute a (x * x)
⊢ 0 ≤ x

Tactic:
have hx := nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts.mpr ⟨hx₁, hx₂⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ a
x : A
hx₁ : IsSelfAdjoint x
hx₂ : QuasispectrumRestricts (R := NNReal) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
hb :
  IsSelfAdjoint (x * x) ∧
    QuasispectrumRestricts (R := NNReal) (S := ℝ) (x * x) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
h : Commute a (x * x)
hx : 0 ≤ x
rw : QuasispectrumRestricts (R := NNReal) (S := ℝ) (x * a * x) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
⊢ QuasispectrumRestricts (R := NNReal) (S := ℝ) (a * (x * x)) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)

Tactic:
rw [← mul_assoc, quasispectrumRestricts_iff, quasispectrum.mul_comm,
    ← quasispectrumRestricts_iff, ← mul_assoc]

Premises used: quasispectrumRestricts_iff, mul_assoc, quasispectrum.mul_comm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ a
x : A
hx₁ : IsSelfAdjoint x
hx₂ : QuasispectrumRestricts (R := NNReal) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
hb :
  IsSelfAdjoint (x * x) ∧
    QuasispectrumRestricts (R := NNReal) (S := ℝ) (x * x) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
h : Commute a (x * x)
hx : 0 ≤ x
⊢ QuasispectrumRestricts (R := NNReal) (S := ℝ) (x * a * x) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)

Tactic:
QuasispectrumRestricts.nnreal_of_nonneg <| conjugate_nonneg_of_nonneg ha hx

Premises used: conjugate_nonneg_of_nonneg, QuasispectrumRestricts.nnreal_of_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ a
x : A
hx₁ : IsSelfAdjoint x
hx₂ : QuasispectrumRestricts (R := NNReal) (S := ℝ) x (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
hb :
  IsSelfAdjoint (x * x) ∧
    QuasispectrumRestricts (R := NNReal) (S := ℝ) (x * x) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
h : Commute a (x * x)
hx : 0 ≤ x
⊢ QuasispectrumRestricts (R := NNReal) (S := ℝ) (x * a * x) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)

Tactic:
exact QuasispectrumRestricts.nnreal_of_nonneg <| conjugate_nonneg_of_nonneg ha hx

Premises used: conjugate_nonneg_of_nonneg, QuasispectrumRestricts.nnreal_of_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
⊢ Commute a b ↔ 0 ≤ a * b

Tactic:
⟨Commute.mul_nonneg ha hb,
  fun h => ha.isSelfAdjoint.commute_iff hb.isSelfAdjoint |>.mpr h.isSelfAdjoint⟩

Premises used: Iff.mpr, Commute.mul_nonneg, LE.le.isSelfAdjoint, IsSelfAdjoint.commute_iff, Iff.intro
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_2
inst : Ring A
inst_1 : StarRing A
inst_2 : LE A
inst_3 : TopologicalSpace A
inst_4 : Algebra ℝ≥0 A
inst_5 : ContinuousFunctionalCalculus ℝ≥0 A fun (x : A) ↦ 0 ≤ x
inst_6 : Nontrivial A
a : A
ha : 0 ≤ a
⊢ (σ ℝ≥0 a).Nonempty

Tactic:
ContinuousFunctionalCalculus.spectrum_nonempty a ha

Premises used: ContinuousFunctionalCalculus.spectrum_nonempty
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : Ring A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
⊢ ContinuousFunctionalCalculus ℝ≥0 A fun (x : A) ↦ 0 ≤ x

Tactic:
SpectrumRestricts.cfc (q := IsSelfAdjoint) ContinuousMap.realToNNReal
    NNReal.isClosedEmbedding_coe le_rfl
    (fun _ ↦ nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts)

Premises used: le_rfl, NNReal.isClosedEmbedding_coe, ContinuousMap.realToNNReal, nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts, SpectrumRestricts.cfc
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : Ring A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
a b : A
ha : IsStrictlyPositive a
hb : IsStrictlyPositive b
rw : 0 ≤ a * b ↔ IsStrictlyPositive (a * b)
⊢ Commute a b ↔ IsStrictlyPositive (a * b)

Tactic:
rw [commute_iff_mul_nonneg ha.nonneg hb.nonneg]

Premises used: commute_iff_mul_nonneg, IsStrictlyPositive.nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : Ring A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
a b : A
ha : IsStrictlyPositive a
hb : IsStrictlyPositive b
⊢ 0 ≤ a * b ↔ IsStrictlyPositive (a * b)

Tactic:
⟨fun h => ha.isUnit.mul hb.isUnit |>.isStrictlyPositive h, fun h => h.nonneg⟩

Premises used: IsUnit.mul, IsUnit.isStrictlyPositive, Iff.intro, IsStrictlyPositive.isUnit, IsStrictlyPositive.nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : Ring A
inst_1 : PartialOrder A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : TopologicalSpace A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
a b : A
ha : IsStrictlyPositive a
hb : IsStrictlyPositive b
⊢ 0 ≤ a * b ↔ IsStrictlyPositive (a * b)

Tactic:
exact ⟨fun h => ha.isUnit.mul hb.isUnit |>.isStrictlyPositive h, fun h => h.nonneg⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst_5 : T2Space A
a : A
ha : IsSelfAdjoint a
⊢ Eq (α := C((↑(σ ℝ a) : Type), ℝ) →⋆ₐ[ℝ] A) (cfcHom (p := IsSelfAdjoint) ha)
    (SpectrumRestricts.starAlgHom (S := ℂ) (cfcHom (p := IsStarNormal) ⋯) (f := (↑Complex.reCLM : C(ℂ, ℝ))) ⋯)

Tactic:
ha.spectrumRestricts.cfcHom_eq_restrict _ ha ha.isStarNormal

Premises used: SpectrumRestricts.cfcHom_eq_restrict, IsSelfAdjoint.isStarNormal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst_5 : T2Space A
a : A
f : ℝ → ℝ
ha : IsSelfAdjoint a
⊢ cfc (p := IsSelfAdjoint) f a = cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) a

Tactic:
ha.spectrumRestricts.cfc_eq_restrict (f := Complex.reCLM)
    Complex.isometry_ofReal.isClosedEmbedding ha ha.isStarNormal f

Premises used: Complex.isometry_ofReal, IsSelfAdjoint.isStarNormal, Isometry.isClosedEmbedding, SpectrumRestricts.cfc_eq_restrict
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst_5 : T2Space A
a : A
f : ℝ → ℝ
ha : IsSelfAdjoint a
⊢ cfc (p := IsSelfAdjoint) f a = cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) a

Tactic:
exact ha.spectrumRestricts.cfc_eq_restrict (f := Complex.reCLM)
    Complex.isometry_ofReal.isClosedEmbedding ha ha.isStarNormal f

Premises used: Complex.isometry_ofReal, IsSelfAdjoint.isStarNormal, Isometry.isClosedEmbedding, SpectrumRestricts.cfc_eq_restrict
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst_5 : T2Space A
f : ℂ → ℂ
a : A
hf_real : ∀ x ∈ σ ℂ a, star (f x) = f x
ha : IsSelfAdjoint a
rw : cfc (p := IsStarNormal) f a = cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f (↑x.re : ℂ)).re : ℂ)) a
⊢ cfc (p := IsStarNormal) f a = cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (f (↑x : ℂ)).re) a

Tactic:
rw [cfc_real_eq_complex ..]

Premises used: cfc_real_eq_complex
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst_5 : T2Space A
f : ℂ → ℂ
a : A
hf_real : ∀ x ∈ σ ℂ a, star (f x) = f x
ha : IsSelfAdjoint a
⊢ cfc (p := IsStarNormal) f a = cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f (↑x.re : ℂ)).re : ℂ)) a

Tactic:
cfc_congr fun x hx ↦ ?_

Premises used: cfc_congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst_5 : T2Space A
f : ℂ → ℂ
a : A
hf_real : ∀ x ∈ σ ℂ a, star (f x) = f x
ha : IsSelfAdjoint a
refine : ∀ (x : ℂ) (hx : x ∈ σ ℂ a), f x = (↑(f (↑x.re : ℂ)).re : ℂ)
⊢ cfc (p := IsStarNormal) f a = cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f (↑x.re : ℂ)).re : ℂ)) a

Tactic:
refine cfc_congr fun x hx ↦ ?_

Premises used: cfc_congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst_5 : T2Space A
f : ℂ → ℂ
a : A
hf_real : ∀ x ∈ σ ℂ a, star (f x) = f x
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σ ℂ a
⊢ ∀ x ∈ σ ℂ a, (↑(f x).re : ℂ) = f x

Tactic:
simp_rw [RCLike.star_def, RCLike.conj_eq_iff_re, RCLike.re_eq_complex_re,
    RCLike.ofReal_eq_complex_ofReal] at hf_real

Premises used: RCLike.star_def, RCLike.conj_eq_iff_re, RCLike.ofReal_eq_complex_ofReal, RCLike.re_eq_complex_re
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst_5 : T2Space A
f : ℂ → ℂ
a : A
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σ ℂ a
hf_real : ∀ x ∈ σ ℂ a, (↑(f x).re : ℂ) = f x
rw : f x = (↑(f x).re : ℂ)
rw₁ rw₂ : f x = f x
⊢ f x = (↑(f (↑x.re : ℂ)).re : ℂ)

Tactic:
rw [← SpectrumRestricts.real_iff.mp ha.spectrumRestricts _ hx, hf_real _ hx]

Premises used: IsSelfAdjoint.spectrumRestricts, SpectrumRestricts.real_iff, Iff.mp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : T2Space A
inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsSelfAdjoint a
⊢ Eq (α := ContinuousMapZero (↑(σₙ ℝ a) : Type) ℝ →⋆ₙₐ[ℝ] A) (cfcₙHom (p := IsSelfAdjoint) ha)
    (QuasispectrumRestricts.nonUnitalStarAlgHom (S := ℂ) (cfcₙHom (p := IsStarNormal) ⋯) (f :=
      (↑Complex.reCLM : C(ℂ, ℝ))) ⋯)

Tactic:
ha.quasispectrumRestricts.cfcₙHom_eq_restrict _ ha ha.isStarNormal

Premises used: QuasispectrumRestricts.cfcₙHom_eq_restrict, IsSelfAdjoint.isStarNormal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : T2Space A
inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
f : ℝ → ℝ
ha : IsSelfAdjoint a
⊢ cfcₙ (p := IsSelfAdjoint) f a = cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) a

Tactic:
ha.quasispectrumRestricts.cfcₙ_eq_restrict (f := Complex.reCLM)
    Complex.isometry_ofReal.isClosedEmbedding ha ha.isStarNormal f

Premises used: QuasispectrumRestricts.cfcₙ_eq_restrict, Complex.isometry_ofReal, IsSelfAdjoint.isStarNormal, Isometry.isClosedEmbedding
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : T2Space A
inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
f : ℝ → ℝ
ha : IsSelfAdjoint a
⊢ cfcₙ (p := IsSelfAdjoint) f a = cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) a

Tactic:
exact ha.quasispectrumRestricts.cfcₙ_eq_restrict (f := Complex.reCLM)
    Complex.isometry_ofReal.isClosedEmbedding ha ha.isStarNormal f

Premises used: QuasispectrumRestricts.cfcₙ_eq_restrict, Complex.isometry_ofReal, IsSelfAdjoint.isStarNormal, Isometry.isClosedEmbedding