awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 : 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

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 : 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
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 : 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
⊢ ∀ 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 : 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 : ℂ)
rw₁ rw₂ : f x = f x
⊢ f x = (↑(f (↑x.re : ℂ)).re : ℂ)

Tactic:
rw [← QuasispectrumRestricts.real_iff.mp ha.quasispectrumRestricts _ hx, hf_real _ hx]

Premises used: IsSelfAdjoint.quasispectrumRestricts, QuasispectrumRestricts.real_iff, Iff.mp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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
a : A
ha : 0 ≤ a
⊢ Eq (α := C((↑(σ ℝ≥0 a) : Type), ℝ≥0) →⋆ₐ[ℝ≥0] A) (cfcHom (p := LE.le 0) ha)
    (SpectrumRestricts.starAlgHom (cfcHom (p := IsSelfAdjoint) ⋯) ⋯)

Tactic:
apply (SpectrumRestricts.nnreal_of_nonneg ha).cfcHom_eq_restrict _

Premises used: SpectrumRestricts.nnreal_of_nonneg, SpectrumRestricts.cfcHom_eq_restrict, ContinuousMap.realToNNReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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 : ℝ≥0 → ℝ≥0
a : A
ha : 0 ≤ a
⊢ cfc (p := fun (x : A) ↦ 0 ≤ x) f a = cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a

Tactic:
apply (SpectrumRestricts.nnreal_of_nonneg ha).cfc_eq_restrict _
    NNReal.isClosedEmbedding_coe ha (.of_nonneg ha)

Premises used: SpectrumRestricts.nnreal_of_nonneg, NNReal.isClosedEmbedding_coe, SpectrumRestricts.cfc_eq_restrict
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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
rw : cfc (p := IsSelfAdjoint) f a = cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f (↑x.toNNReal : ℝ)).toNNReal : ℝ)) a
⊢ cfc (p := IsSelfAdjoint) f a = cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ (f (↑x : ℝ)).toNNReal) a

Tactic:
rw [cfc_nnreal_eq_real ..]

Premises used: cfc_nnreal_eq_real
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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

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 : 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
refine : ∀ (x : ℝ) (hx : x ∈ σ ℝ a), f x = (↑(f (↑x.toNNReal : ℝ)).toNNReal : ℝ)
⊢ cfc (p := IsSelfAdjoint) f a = cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f (↑x.toNNReal : ℝ)).toNNReal : ℝ)) 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 : 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 : ℝ)
rw₁ rw₂ : f x = f x
⊢ f x = (↑(f (↑x.toNNReal : ℝ)).toNNReal : ℝ)

Tactic:
rw [x.coe_toNNReal (spectrum_nonneg_of_nonneg ha hx), (f x).coe_toNNReal (hf_nonneg x hx)]

Premises used: spectrum_nonneg_of_nonneg, Real.coe_toNNReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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
a : A
ha : 0 ≤ a
⊢ Eq (α := ContinuousMapZero (↑(σₙ ℝ≥0 a) : Type) ℝ≥0 →⋆ₙₐ[ℝ≥0] A) (cfcₙHom (p := LE.le 0) ha)
    (QuasispectrumRestricts.nonUnitalStarAlgHom (cfcₙHom (p := IsSelfAdjoint) ⋯) ⋯)

Tactic:
apply (QuasispectrumRestricts.nnreal_of_nonneg ha).cfcₙHom_eq_restrict _

Premises used: QuasispectrumRestricts.cfcₙHom_eq_restrict, ContinuousMap.realToNNReal, QuasispectrumRestricts.nnreal_of_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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 : ℝ≥0 → ℝ≥0
a : A
ha : 0 ≤ a
⊢ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a

Tactic:
apply (QuasispectrumRestricts.nnreal_of_nonneg ha).cfcₙ_eq_restrict _
    NNReal.isClosedEmbedding_coe ha (.of_nonneg ha)

Premises used: QuasispectrumRestricts.cfcₙ_eq_restrict, NNReal.isClosedEmbedding_coe, QuasispectrumRestricts.nnreal_of_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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
rw : cfcₙ (p := IsSelfAdjoint) f a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f (↑x.toNNReal : ℝ)).toNNReal : ℝ)) a
⊢ cfcₙ (p := IsSelfAdjoint) f a = cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ (f (↑x : ℝ)).toNNReal) a

Tactic:
rw [cfcₙ_nnreal_eq_real ..]

Premises used: cfcₙ_nnreal_eq_real
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
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

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 : 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
refine : ∀ (x : ℝ) (hx : x ∈ σₙ ℝ a), f x = (↑(f (↑x.toNNReal : ℝ)).toNNReal : ℝ)
⊢ cfcₙ (p := IsSelfAdjoint) f a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f (↑x.toNNReal : ℝ)).toNNReal : ℝ)) 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 : 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 : ℝ)
rw₁ rw₂ : f x = f x
⊢ f x = (↑(f (↑x.toNNReal : ℝ)).toNNReal : ℝ)

Tactic:
rw [x.coe_toNNReal (quasispectrum_nonneg_of_nonneg _ ha _ hx),
    (f x).coe_toNNReal (hf_nonneg x hx)]

Premises used: Real.coe_toNNReal, NonnegSpectrumClass.quasispectrum_nonneg_of_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
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
rw 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)
⊢ 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)

Tactic:
rw [ContinuousLinearMap.integral_comp_comm _ hf₁]

Premises used: ContinuousLinearMap.integral_comp_comm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
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
a : A
f : X → C((↑(spectrum 𝕜 a) : Type u_2), 𝕜)
hf₁ : Integrable f μ
ha : p a
⊢ 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)
        (f x))
    μ

Tactic:
ContinuousLinearMap.integrable_comp _ hf₁

Premises used: ContinuousLinearMap.integrable_comp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
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), (cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_2), 𝕜)) → A) (f x) ∂μ : A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_2), 𝕜)) → A) (∫ (x : X), f x ∂μ) : A)

Tactic:
cfcL_integral a f hf₁ ha

Premises used: cfcL_integral
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
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
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)
| cfc (p := p) (f x) a

Tactic:
rw [cfc_eq_cfcL_mkD _ a]

Premises used: cfc_eq_cfcL_mkD
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
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
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))
    μ
⊢ Integrable.{u_3, u_1} (ε := A) (fun (x : X) ↦ cfc (p := p) (f x) a) μ

Tactic:
conv in cfc _ _ => rw [cfc_eq_cfcL_mkD _ a]

Premises used: cfc, cfc_eq_cfcL_mkD
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
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) ↦
      ((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:
cfcL_integrable _ _ hf ha

Premises used: cfcL_integrable
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
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) ↦
      ((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:
exact cfcL_integrable _ _ hf ha

Premises used: cfcL_integrable
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
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
s : Set X
f : X → 𝕜 → 𝕜
a : A
hf :
  IntegrableOn.{u_1, u_2} (ε := C((↑(spectrum 𝕜 a) : Type u_2), 𝕜))
    (fun (x : X) ↦ mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) s μ
ha : p a
⊢ IntegrableOn.{u_1, u_3} (ε := A) (fun (x : X) ↦ cfc (p := p) (f x) a) s μ

Tactic:
integrable_cfc' _ _ hf ha

Premises used: MeasureTheory.IntegrableOn, integrable_cfc'
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
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
s : Set X
f : X → 𝕜 → 𝕜
a : A
hf :
  IntegrableOn.{u_1, u_2} (ε := C((↑(spectrum 𝕜 a) : Type u_2), 𝕜))
    (fun (x : X) ↦ mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) s μ
ha : p a
⊢ IntegrableOn.{u_1, u_3} (ε := A) (fun (x : X) ↦ cfc (p := p) (f x) a) s μ

Tactic:
exact integrable_cfc' _ _ hf ha

Premises used: integrable_cfc'
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
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) μ

Tactic:
integrable_cfc' _ _ ⟨?_, ?_⟩ ha

Premises used: integrable_cfc', And.intro
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
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) μ
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) μ
⊢ Integrable.{u_3, u_1} (ε := A) (fun (x : X) ↦ cfc (p := p) (f x) a) μ

Tactic:
refine integrable_cfc' _ _ ⟨?_, ?_⟩ ha

Premises used: integrable_cfc', And.intro
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
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
⊢ AEStronglyMeasurable.{u_1, u_2} (β := C((↑(spectrum 𝕜 a) : Type u_2), 𝕜))
    (fun (x : X) ↦ mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) μ

Tactic:
aeStronglyMeasurable_mkD_restrict_of_uncurry _ _ hf

Premises used: ContinuousMap.aeStronglyMeasurable_mkD_restrict_of_uncurry
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
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
⊢ AEStronglyMeasurable.{u_1, u_2} (β := C((↑(spectrum 𝕜 a) : Type u_2), 𝕜))
    (fun (x : X) ↦ mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) μ

Tactic:
exact aeStronglyMeasurable_mkD_restrict_of_uncurry _ _ hf

Premises used: ContinuousMap.aeStronglyMeasurable_mkD_restrict_of_uncurry