awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
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
⊢ QuasispectrumRestricts (R := NNReal) (S := ℝ) (a * b) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
have 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)
Tactic: obtain ⟨x, hx₁, hx₂, rfl⟩ := CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts hb.1 hb.2
Cleared hypotheses: b, hb, h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (hypothesis)
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)
⊢ QuasispectrumRestricts (R := NNReal) (S := ℝ) (a * (x * x)) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
have hx : 0 ≤ x
Tactic: have hx := nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts.mpr ⟨hx₁, hx₂⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
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 := ℝ) (a * (x * x)) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
have rw : QuasispectrumRestricts (R := NNReal) (S := ℝ) (x * a * x) (⇑ContinuousMap.realToNNReal : (a : ℝ) → NNReal)
Tactic: rw [← mul_assoc, quasispectrumRestricts_iff, quasispectrum.mul_comm,
    ← quasispectrumRestricts_iff, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
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
⊢ Commute a b ↔ IsStrictlyPositive (a * b)
have rw : 0 ≤ a * b ↔ IsStrictlyPositive (a * b)
Tactic: rw [commute_iff_mul_nonneg ha.nonneg hb.nonneg]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
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 := IsSelfAdjoint) (fun (x : ℝ) ↦ (f (↑x : ℂ)).re) a
have rw : cfc (p := IsStarNormal) f a = cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f (↑x.re : ℂ)).re : ℂ)) a
Tactic: rw [cfc_real_eq_complex ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
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
have refine : ∀ (x : ℂ) (hx : x ∈ σ ℂ a), f x = (↑(f (↑x.re : ℂ)).re : ℂ)
Tactic: refine cfc_congr fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (hypothesis)
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
⊢ f x = (↑(f (↑x.re : ℂ)).re : ℂ)
have hf_real₁ : ∀ 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
Cleared hypotheses: hf_real
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
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
⊢ f x = (↑(f (↑x.re : ℂ)).re : ℂ)
have rw : f x = (↑(f x).re : ℂ)
Tactic: rw [← SpectrumRestricts.real_iff.mp ha.spectrumRestricts _ hx, hf_real _ hx]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
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 : ℂ)
⊢ f x = (↑(f (↑x.re : ℂ)).re : ℂ)
have rw₁ : f x = f x
Tactic: rw [← SpectrumRestricts.real_iff.mp ha.spectrumRestricts _ hx, hf_real _ hx]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
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
f : ℂ → ℂ
a : A
hf_real : ∀ x ∈ σₙ ℂ a, star (f x) = f x
ha : IsSelfAdjoint a
⊢ cfcₙ (p := IsStarNormal) f a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (f (↑x : ℂ)).re) a
have rw : cfcₙ (p := IsStarNormal) f a = cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f (↑x.re : ℂ)).re : ℂ)) a
Tactic: rw [cfcₙ_real_eq_complex ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
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
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
have refine : ∀ (x : ℂ) (hx : x ∈ σₙ ℂ a), f x = (↑(f (↑x.re : ℂ)).re : ℂ)
Tactic: refine cfcₙ_congr fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (hypothesis)
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
f : ℂ → ℂ
a : A
hf_real : ∀ x ∈ σₙ ℂ a, star (f x) = f x
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σₙ ℂ a
⊢ f x = (↑(f (↑x.re : ℂ)).re : ℂ)
have hf_real₁ : ∀ 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
Cleared hypotheses: hf_real
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
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
f : ℂ → ℂ
a : A
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σₙ ℂ a
hf_real : ∀ x ∈ σₙ ℂ a, (↑(f x).re : ℂ) = f x
⊢ f x = (↑(f (↑x.re : ℂ)).re : ℂ)
have rw : f x = (↑(f x).re : ℂ)
Tactic: rw [← QuasispectrumRestricts.real_iff.mp ha.quasispectrumRestricts _ hx, hf_real _ hx]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
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
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 : ℂ)
⊢ f x = (↑(f (↑x.re : ℂ)).re : ℂ)
have rw₁ : f x = f x
Tactic: rw [← QuasispectrumRestricts.real_iff.mp ha.quasispectrumRestricts _ hx, hf_real _ hx]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : IsSemitopologicalRing A
inst_7 : T2Space A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
f : ℝ → ℝ
a : A
hf_nonneg : ∀ x ∈ σ ℝ a, 0 ≤ f x
ha : 0 ≤ a
⊢ cfc (p := IsSelfAdjoint) f a = cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ (f (↑x : ℝ)).toNNReal) a
have rw : cfc (p := IsSelfAdjoint) f a = cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f (↑x.toNNReal : ℝ)).toNNReal : ℝ)) a
Tactic: rw [cfc_nnreal_eq_real ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : IsSemitopologicalRing A
inst_7 : T2Space A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
f : ℝ → ℝ
a : A
hf_nonneg : ∀ x ∈ σ ℝ a, 0 ≤ f x
ha : 0 ≤ a
⊢ cfc (p := IsSelfAdjoint) f a = cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f (↑x.toNNReal : ℝ)).toNNReal : ℝ)) a
have refine : ∀ (x : ℝ) (hx : x ∈ σ ℝ a), f x = (↑(f (↑x.toNNReal : ℝ)).toNNReal : ℝ)
Tactic: refine cfc_congr fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : IsSemitopologicalRing A
inst_7 : T2Space A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
f : ℝ → ℝ
a : A
hf_nonneg : ∀ x ∈ σ ℝ a, 0 ≤ f x
ha : 0 ≤ a
x : ℝ
hx : x ∈ σ ℝ a
⊢ f x = (↑(f (↑x.toNNReal : ℝ)).toNNReal : ℝ)
have rw : f x = (↑(f x).toNNReal : ℝ)
Tactic: rw [x.coe_toNNReal (spectrum_nonneg_of_nonneg ha hx), (f x).coe_toNNReal (hf_nonneg x hx)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : IsSemitopologicalRing A
inst_7 : T2Space A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
f : ℝ → ℝ
a : A
hf_nonneg : ∀ x ∈ σ ℝ a, 0 ≤ f x
ha : 0 ≤ a
x : ℝ
hx : x ∈ σ ℝ a
rw : f x = (↑(f x).toNNReal : ℝ)
⊢ f x = (↑(f (↑x.toNNReal : ℝ)).toNNReal : ℝ)
have rw₁ : f x = f x
Tactic: rw [x.coe_toNNReal (spectrum_nonneg_of_nonneg ha hx), (f x).coe_toNNReal (hf_nonneg x hx)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Module ℝ A
inst_6 : IsSemitopologicalRing A
inst_7 : IsScalarTower ℝ A A
inst_8 : SMulCommClass ℝ A A
inst_9 : T2Space A
inst_10 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_11 : NonnegSpectrumClass ℝ A
f : ℝ → ℝ
a : A
hf_nonneg : ∀ x ∈ σₙ ℝ a, 0 ≤ f x
ha : 0 ≤ a
⊢ cfcₙ (p := IsSelfAdjoint) f a = cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ (f (↑x : ℝ)).toNNReal) a
have rw : cfcₙ (p := IsSelfAdjoint) f a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f (↑x.toNNReal : ℝ)).toNNReal : ℝ)) a
Tactic: rw [cfcₙ_nnreal_eq_real ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Module ℝ A
inst_6 : IsSemitopologicalRing A
inst_7 : IsScalarTower ℝ A A
inst_8 : SMulCommClass ℝ A A
inst_9 : T2Space A
inst_10 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_11 : NonnegSpectrumClass ℝ A
f : ℝ → ℝ
a : A
hf_nonneg : ∀ x ∈ σₙ ℝ a, 0 ≤ f x
ha : 0 ≤ a
⊢ cfcₙ (p := IsSelfAdjoint) f a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f (↑x.toNNReal : ℝ)).toNNReal : ℝ)) a
have refine : ∀ (x : ℝ) (hx : x ∈ σₙ ℝ a), f x = (↑(f (↑x.toNNReal : ℝ)).toNNReal : ℝ)
Tactic: refine cfcₙ_congr fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Module ℝ A
inst_6 : IsSemitopologicalRing A
inst_7 : IsScalarTower ℝ A A
inst_8 : SMulCommClass ℝ A A
inst_9 : T2Space A
inst_10 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_11 : NonnegSpectrumClass ℝ A
f : ℝ → ℝ
a : A
hf_nonneg : ∀ x ∈ σₙ ℝ a, 0 ≤ f x
ha : 0 ≤ a
x : ℝ
hx : x ∈ σₙ ℝ a
⊢ f x = (↑(f (↑x.toNNReal : ℝ)).toNNReal : ℝ)
have rw : f x = (↑(f x).toNNReal : ℝ)
Tactic: rw [x.coe_toNNReal (quasispectrum_nonneg_of_nonneg _ ha _ hx),
    (f x).coe_toNNReal (hf_nonneg x hx)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Module ℝ A
inst_6 : IsSemitopologicalRing A
inst_7 : IsScalarTower ℝ A A
inst_8 : SMulCommClass ℝ A A
inst_9 : T2Space A
inst_10 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_11 : NonnegSpectrumClass ℝ A
f : ℝ → ℝ
a : A
hf_nonneg : ∀ x ∈ σₙ ℝ a, 0 ≤ f x
ha : 0 ≤ a
x : ℝ
hx : x ∈ σₙ ℝ a
rw : f x = (↑(f x).toNNReal : ℝ)
⊢ f x = (↑(f (↑x.toNNReal : ℝ)).toNNReal : ℝ)
have rw₁ : f x = f x
Tactic: rw [x.coe_toNNReal (quasispectrum_nonneg_of_nonneg _ ha _ hx),
    (f x).coe_toNNReal (hf_nonneg x hx)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : NormedRing A
inst_3 : StarRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : CompleteSpace A
inst_7 : NormedSpace ℝ A
a : A
f : X → C((↑(spectrum 𝕜 a) : Type u_2), 𝕜)
hf₁ : Integrable f μ
ha : p a
⊢ Eq.{u_3 + 1} (α := A)
    (∫ (x : X),
        ((cfcL (p := p) ha : C((↑(spectrum 𝕜 a) : Type u_2), 𝕜) →L[𝕜] A) : (a : C((↑(spectrum 𝕜 a) : Type u_2), 𝕜)) → A)
          (f x) ∂μ :
      A)
    (((cfcL (p := p) ha : C((↑(spectrum 𝕜 a) : Type u_2), 𝕜) →L[𝕜] A) : (a : C((↑(spectrum 𝕜 a) : Type u_2), 𝕜)) → A)
        (∫ (x : X), f x ∂μ) :
      A)
have rw : Eq.{u_3 + 1} (α := A)
  (((cfcL (p := p) ha : C((↑(spectrum 𝕜 a) : Type u_2), 𝕜) →L[𝕜] A) : (a : C((↑(spectrum 𝕜 a) : Type u_2), 𝕜)) → A)
      (∫ (x : X), f x ∂μ) :
    A)
  (((cfcL (p := p) ha : C((↑(spectrum 𝕜 a) : Type u_2), 𝕜) →L[𝕜] A) : (a : C((↑(spectrum 𝕜 a) : Type u_2), 𝕜)) → A)
      (∫ (x : X), f x ∂μ) :
    A)
Tactic: rw [ContinuousLinearMap.integral_comp_comm _ hf₁]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : NormedRing A
inst_3 : StarRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : CompleteSpace A
f : X → 𝕜 → 𝕜
a : A
hf :
  Integrable.{u_2, u_1} (ε := C((↑(spectrum 𝕜 a) : Type u_2), 𝕜))
    (fun (x : X) ↦ mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) μ
ha : p a
x : X
| cfc (p := p) (f x) a
have rw : (((cfcL (p := p) ha : C((↑(spectrum 𝕜 a) : Type u_2), 𝕜) →L[𝕜] A) : (a : C((↑(spectrum 𝕜 a) : Type u_2), 𝕜)) → A)
    (mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) :
  A)
Tactic: rw [cfc_eq_cfcL_mkD _ a]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : NormedRing A
inst_3 : StarRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : CompleteSpace A
f : X → 𝕜 → 𝕜
a : A
hf :
  Integrable.{u_2, u_1} (ε := C((↑(spectrum 𝕜 a) : Type u_2), 𝕜))
    (fun (x : X) ↦ mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) μ
ha : p a
⊢ Integrable.{u_3, u_1} (ε := A) (fun (x : X) ↦ cfc (p := p) (f x) a) μ
have conv : Integrable.{u_3, u_1} (ε := A)
  (fun (x : X) ↦
    ((cfcL (p := p) ha : C((↑(spectrum 𝕜 a) : Type u_2), 𝕜) →L[𝕜] A) : (a : C((↑(spectrum 𝕜 a) : Type u_2), 𝕜)) → A)
      (mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0))
  μ
Tactic: conv in cfc _ _ => rw [cfc_eq_cfcL_mkD _ a]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : NormedRing A
inst_3 : StarRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : CompleteSpace A
inst_7 : TopologicalSpace X
inst_8 : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_9 : SecondCountableTopologyEither.{u_1, u_2} X C((↑(spectrum 𝕜 a) : Type u_2), 𝕜)
hf : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set X) univ (spectrum 𝕜 a))
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound μ
ha : p a
⊢ Integrable.{u_3, u_1} (ε := A) (fun (x : X) ↦ cfc (p := p) (f x) a) μ
have refine_1 : AEStronglyMeasurable.{u_1, u_2} (β := C((↑(spectrum 𝕜 a) : Type u_2), 𝕜))
  (fun (x : X) ↦ mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) μ
Tactic: refine integrable_cfc' _ _ ⟨?_, ?_⟩ ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : NormedRing A
inst_3 : StarRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : CompleteSpace A
inst_7 : TopologicalSpace X
inst_8 : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_9 : SecondCountableTopologyEither.{u_1, u_2} X C((↑(spectrum 𝕜 a) : Type u_2), 𝕜)
hf : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set X) univ (spectrum 𝕜 a))
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound μ
ha : p a
refine_1 :
  AEStronglyMeasurable.{u_1, u_2} (β := C((↑(spectrum 𝕜 a) : Type u_2), 𝕜))
    (fun (x : X) ↦ mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) μ
⊢ Integrable.{u_3, u_1} (ε := A) (fun (x : X) ↦ cfc (p := p) (f x) a) μ
have refine_2 : HasFiniteIntegral.{u_1, u_2} (ε := C((↑(spectrum 𝕜 a) : Type u_2), 𝕜))
  (fun (x : X) ↦ mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) μ
Tactic: refine integrable_cfc' _ _ ⟨?_, ?_⟩ ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : NormedRing A
inst_3 : StarRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : CompleteSpace A
inst_7 : TopologicalSpace X
inst_8 : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_9 : SecondCountableTopologyEither.{u_1, u_2} X C((↑(spectrum 𝕜 a) : Type u_2), 𝕜)
hf : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set X) univ (spectrum 𝕜 a))
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound μ
ha : p a
⊢ HasFiniteIntegral.{u_1, u_2} (ε := C((↑(spectrum 𝕜 a) : Type u_2), 𝕜))
    (fun (x : X) ↦ mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) μ
have refine_2 : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 a)
Tactic: refine hasFiniteIntegral_mkD_restrict_of_bound f _ ?_ bound bound_int bound_ge
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : NormedRing A
inst_3 : StarRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : CompleteSpace A
inst_7 : TopologicalSpace X
inst_8 : OpensMeasurableSpace X
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_9 : SecondCountableTopologyEither.{u_1, u_2} X C((↑(spectrum 𝕜 a) : Type u_2), 𝕜)
hf : ContinuousOn (Function.uncurry f) (s ×ˢ spectrum 𝕜 a)
bound_ge : ∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound (μ.restrict s)
ha : p a
⊢ IntegrableOn.{u_1, u_3} (ε := A) (fun (x : X) ↦ cfc (p := p) (f x) a) s μ
have refine_1 : AEStronglyMeasurable.{u_1, u_2} (β := C((↑(spectrum 𝕜 a) : Type u_2), 𝕜))
  (fun (x : X) ↦ mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) (μ.restrict s)
Tactic: refine integrableOn_cfc' _ _ ⟨?_, ?_⟩ ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : NormedRing A
inst_3 : StarRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : ContinuousFunctionalCalculus 𝕜 A p
inst_6 : CompleteSpace A
inst_7 : TopologicalSpace X
inst_8 : OpensMeasurableSpace X
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_9 : SecondCountableTopologyEither.{u_1, u_2} X C((↑(spectrum 𝕜 a) : Type u_2), 𝕜)
hf : ContinuousOn (Function.uncurry f) (s ×ˢ spectrum 𝕜 a)
bound_ge : ∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound (μ.restrict s)
ha : p a
refine_1 :
  AEStronglyMeasurable.{u_1, u_2} (β := C((↑(spectrum 𝕜 a) : Type u_2), 𝕜))
    (fun (x : X) ↦ mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) (μ.restrict s)
⊢ IntegrableOn.{u_1, u_3} (ε := A) (fun (x : X) ↦ cfc (p := p) (f x) a) s μ
have refine_2 : HasFiniteIntegral.{u_1, u_2} (ε := C((↑(spectrum 𝕜 a) : Type u_2), 𝕜))
  (fun (x : X) ↦ mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) (μ.restrict s)
Tactic: refine integrableOn_cfc' _ _ ⟨?_, ?_⟩ ha