awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_8 : TopologicalSpace X
inst_9 : OpensMeasurableSpace X
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_10 : 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
this : ∀ᵐ (x : X) ∂μ.restrict s, ContinuousOn (f x) (spectrum 𝕜 a)
⊢ 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:
aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry hs _ _ hf

Premises used: ContinuousMap.aeStronglyMeasurable_restrict_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 : NormedSpace ℝ A
inst_8 : TopologicalSpace X
inst_9 : OpensMeasurableSpace X
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_10 : 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
this : ∀ᵐ (x : X) ∂μ.restrict s, ContinuousOn (f x) (spectrum 𝕜 a)
⊢ 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:
exact aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry hs _ _ hf

Premises used: ContinuousMap.aeStronglyMeasurable_restrict_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 : NormedSpace ℝ A
inst_8 : TopologicalSpace X
inst_9 : OpensMeasurableSpace X
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_10 : 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
this : ∀ᵐ (x : X) ∂μ.restrict s, ContinuousOn (f x) (spectrum 𝕜 a)
⊢ 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:
hasFiniteIntegral_mkD_restrict_of_bound f _ this bound bound_int bound_ge

Premises used: ContinuousMap.hasFiniteIntegral_mkD_restrict_of_bound
-- 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
inst_8 : TopologicalSpace X
inst_9 : OpensMeasurableSpace X
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_10 : 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
this : ∀ᵐ (x : X) ∂μ.restrict s, ContinuousOn (f x) (spectrum 𝕜 a)
⊢ 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:
exact hasFiniteIntegral_mkD_restrict_of_bound f _ this bound bound_int bound_ge

Premises used: ContinuousMap.hasFiniteIntegral_mkD_restrict_of_bound
-- 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 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : NormedSpace 𝕜 A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : CompleteSpace A
inst_9 : NormedSpace ℝ A
a : A
f : X → C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀
hf₁ : Integrable f μ
ha : p a
rw rw₁ :
  Eq.{u_3 + 1} (α := A)
    (((cfcₙL (p := p) ha : C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀ →L[𝕜] A) :
          (a : C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀) → A)
        (∫ (x : X), f x ∂μ) :
      A)
    (((cfcₙL (p := p) ha : C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀ →L[𝕜] A) :
          (a : C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀) → A)
        (∫ (x : X), f x ∂μ) :
      A)
⊢ Eq.{u_3 + 1} (α := A)
    (∫ (x : X),
        ((cfcₙL (p := p) ha : C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀ →L[𝕜] A) :
            (a : C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀) → A)
          (f x) ∂μ :
      A)
    (((cfcₙL (p := p) ha : C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀ →L[𝕜] A) :
          (a : C((↑(quasispectrum 𝕜 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 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : NormedSpace 𝕜 A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : CompleteSpace A
inst_9 : NormedSpace ℝ A
a : A
f : X → C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀
hf₁ : Integrable f μ
ha : p a
⊢ Eq.{u_3 + 1} (α := A)
    (∫ (x : X), (cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀) → A) (f x) ∂μ : A)
    ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀) → A) (∫ (x : X), f x ∂μ) : A)

Tactic:
cfcₙL_integral a f hf₁ ha

Premises used: cfcₙL_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 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : NormedSpace 𝕜 A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : CompleteSpace A
a : A
f : X → C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀
hf₁ : Integrable f μ
ha : p a
⊢ Integrable.{u_3, u_1} (ε := A)
    (fun (x : X) ↦
      ((cfcₙL (p := p) ha : C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀ →L[𝕜] A) :
          (a : C((↑(quasispectrum 𝕜 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 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : NormedSpace 𝕜 A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : CompleteSpace A
f : X → 𝕜 → 𝕜
a : A
hf :
  Integrable.{u_2, u_1} (ε := C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀)
    (fun (x : X) ↦ mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) μ
ha : p a
x : X
rw :
  (((cfcₙL (p := p) ha : C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀ →L[𝕜] A) :
        (a : C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀) → A)
      (mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) :
    A)
| cfcₙ (p := p) (f x) a

Tactic:
rw [cfcₙ_eq_cfcₙL_mkD _ a]

Premises used: cfcₙ_eq_cfcₙL_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 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : NormedSpace 𝕜 A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : CompleteSpace A
f : X → 𝕜 → 𝕜
a : A
hf :
  Integrable.{u_2, u_1} (ε := C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀)
    (fun (x : X) ↦ mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) μ
ha : p a
conv :
  Integrable.{u_3, u_1} (ε := A)
    (fun (x : X) ↦
      ((cfcₙL (p := p) ha : C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀ →L[𝕜] A) :
          (a : C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀) → A)
        (mkD ((quasispectrum 𝕜 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_cfcₙL_mkD _ a]

Premises used: cfcₙ, cfcₙ_eq_cfcₙL_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 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : NormedSpace 𝕜 A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : CompleteSpace A
f : X → 𝕜 → 𝕜
a : A
hf :
  Integrable.{u_2, u_1} (ε := C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀)
    (fun (x : X) ↦ mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) μ
ha : p a
⊢ Integrable.{u_3, u_1} (ε := A)
    (fun (x : X) ↦
      ((cfcₙL (p := p) ha : C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀ →L[𝕜] A) :
          (a : C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀) → A)
        (mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0))
    μ

Tactic:
cfcₙL_integrable _ _ hf ha

Premises used: cfcₙL_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 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : NormedSpace 𝕜 A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : CompleteSpace A
f : X → 𝕜 → 𝕜
a : A
hf :
  Integrable.{u_2, u_1} (ε := C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀)
    (fun (x : X) ↦ mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) μ
ha : p a
⊢ Integrable.{u_3, u_1} (ε := A)
    (fun (x : X) ↦
      ((cfcₙL (p := p) ha : C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀ →L[𝕜] A) :
          (a : C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀) → A)
        (mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0))
    μ

Tactic:
exact cfcₙL_integrable _ _ hf ha

Premises used: cfcₙL_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 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : NormedSpace 𝕜 A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : CompleteSpace A
s : Set X
f : X → 𝕜 → 𝕜
a : A
hf :
  IntegrableOn.{u_1, u_2} (ε := C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀)
    (fun (x : X) ↦ mkD ((quasispectrum 𝕜 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 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : NormedSpace 𝕜 A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : CompleteSpace A
s : Set X
f : X → 𝕜 → 𝕜
a : A
hf :
  IntegrableOn.{u_1, u_2} (ε := C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀)
    (fun (x : X) ↦ mkD ((quasispectrum 𝕜 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 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : NormedSpace 𝕜 A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : CompleteSpace A
inst_9 : TopologicalSpace X
inst_10 : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_11 : SecondCountableTopologyEither.{u_1, u_2} X C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)
hf : ContinuousOn (uncurry f) (SProd.sprod (α := Set X) univ (quasispectrum 𝕜 a))
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ quasispectrum 𝕜 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 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : NormedSpace 𝕜 A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : CompleteSpace A
inst_9 : TopologicalSpace X
inst_10 : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_11 : SecondCountableTopologyEither.{u_1, u_2} X C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)
hf : ContinuousOn (uncurry f) (SProd.sprod (α := Set X) univ (quasispectrum 𝕜 a))
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound μ
ha : p a
refine_1 :
  AEStronglyMeasurable.{u_1, u_2} (β := C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀)
    (fun (x : X) ↦ mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) μ
refine_2 :
  HasFiniteIntegral.{u_1, u_2} (ε := C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀)
    (fun (x : X) ↦ mkD ((quasispectrum 𝕜 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 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : NormedSpace 𝕜 A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : CompleteSpace A
inst_9 : TopologicalSpace X
inst_10 : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_11 : SecondCountableTopologyEither.{u_1, u_2} X C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)
hf : ContinuousOn (uncurry f) (SProd.sprod (α := Set X) univ (quasispectrum 𝕜 a))
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound μ
ha : p a
⊢ AEStronglyMeasurable.{u_1, u_2} (β := C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀)
    (fun (x : X) ↦ mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) μ

Tactic:
aeStronglyMeasurable_mkD_restrict_of_uncurry _ _ hf f_zero

Premises used: ContinuousMapZero.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 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : NormedSpace 𝕜 A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : CompleteSpace A
inst_9 : TopologicalSpace X
inst_10 : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_11 : SecondCountableTopologyEither.{u_1, u_2} X C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)
hf : ContinuousOn (uncurry f) (SProd.sprod (α := Set X) univ (quasispectrum 𝕜 a))
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound μ
ha : p a
⊢ AEStronglyMeasurable.{u_1, u_2} (β := C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀)
    (fun (x : X) ↦ mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) μ

Tactic:
exact aeStronglyMeasurable_mkD_restrict_of_uncurry _ _ hf f_zero

Premises used: ContinuousMapZero.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 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : NormedSpace 𝕜 A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : CompleteSpace A
inst_9 : TopologicalSpace X
inst_10 : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_11 : SecondCountableTopologyEither.{u_1, u_2} X C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)
hf : ContinuousOn (uncurry f) (SProd.sprod (α := Set X) univ (quasispectrum 𝕜 a))
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound μ
ha : p a
⊢ HasFiniteIntegral.{u_1, u_2} (ε := C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀)
    (fun (x : X) ↦ mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) μ

Tactic:
hasFiniteIntegral_mkD_restrict_of_bound f _ ?_ f_zero bound bound_int bound_ge

Premises used: Set.Mem, setOf, ContinuousMapZero.hasFiniteIntegral_mkD_restrict_of_bound
-- 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 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : NormedSpace 𝕜 A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : CompleteSpace A
inst_9 : TopologicalSpace X
inst_10 : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_11 : SecondCountableTopologyEither.{u_1, u_2} X C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)
hf : ContinuousOn (uncurry f) (SProd.sprod (α := Set X) univ (quasispectrum 𝕜 a))
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound μ
ha : p a
refine_2 : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)
⊢ HasFiniteIntegral.{u_1, u_2} (ε := C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀)
    (fun (x : X) ↦ mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) μ

Tactic:
refine hasFiniteIntegral_mkD_restrict_of_bound f _ ?_ f_zero bound bound_int bound_ge

Premises used: ContinuousMapZero.hasFiniteIntegral_mkD_restrict_of_bound
-- 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 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : NormedSpace 𝕜 A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : CompleteSpace A
inst_9 : TopologicalSpace X
inst_10 : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_11 : SecondCountableTopologyEither.{u_1, u_2} X C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)
hf : ContinuousOn (uncurry f) (SProd.sprod (α := Set X) univ (quasispectrum 𝕜 a))
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound μ
ha : p a
⊢ ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)

Tactic:
.of_forall fun x ↦
      hf.comp (Continuous.prodMk_right x).continuousOn fun _ hz ↦ ⟨Set.mem_univ _, hz⟩

Premises used: Continuous.continuousOn, Continuous.prodMk_right, Prod.mk, Filter.Eventually.of_forall, Prod.fst, ContinuousOn.comp, And.intro, Set.mem_univ
-- 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 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : NormedSpace 𝕜 A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : CompleteSpace A
inst_9 : TopologicalSpace X
inst_10 : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_11 : SecondCountableTopologyEither.{u_1, u_2} X C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)
hf : ContinuousOn (uncurry f) (SProd.sprod (α := Set X) univ (quasispectrum 𝕜 a))
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound μ
ha : p a
⊢ ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)

Tactic:
exact .of_forall fun x ↦
      hf.comp (Continuous.prodMk_right x).continuousOn fun _ hz ↦ ⟨Set.mem_univ _, hz⟩
-- 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 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : NormedSpace 𝕜 A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_8 : CompleteSpace A
inst_9 : TopologicalSpace X
inst_10 : OpensMeasurableSpace X
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_11 : SecondCountableTopologyEither.{u_1, u_2} X C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)
hf : ContinuousOn (uncurry f) (s ×ˢ quasispectrum 𝕜 a)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ quasispectrum 𝕜 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 μ

Tactic:
integrableOn_cfcₙ' _ _ ⟨?_, ?_⟩ ha

Premises used: integrableOn_cfcₙ', And.intro