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 : 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) μ

Tactic:
hasFiniteIntegral_mkD_restrict_of_bound f _ ?_ 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 : 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_2 : ∀ᵐ (x : X) ∂μ, 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) μ

Tactic:
refine hasFiniteIntegral_mkD_restrict_of_bound f _ ?_ 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 : 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
⊢ ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 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 : 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
⊢ ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 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 : 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 μ

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

Premises used: integrableOn_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
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)
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)
⊢ IntegrableOn.{u_1, u_3} (ε := A) (fun (x : X) ↦ cfc (p := p) (f x) a) s μ

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

Premises used: integrableOn_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
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
⊢ 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 : 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
⊢ 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 : 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
⊢ 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 _ ?_ 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 : 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_2 : ∀ᵐ (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:
refine hasFiniteIntegral_mkD_restrict_of_bound f _ ?_ 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 : 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
⊢ ∀ᵐ (x : X) ∂μ.restrict s, ContinuousOn (f x) (spectrum 𝕜 a)

Tactic:
ae_restrict_of_forall_mem hs fun x hx ↦
      hf.comp (Continuous.prodMk_right x).continuousOn fun _ hz ↦ ⟨hx, hz⟩

Premises used: Continuous.continuousOn, Continuous.prodMk_right, MeasureTheory.ae_restrict_of_forall_mem, ContinuousOn.comp, 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
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
⊢ ∀ᵐ (x : X) ∂μ.restrict s, ContinuousOn (f x) (spectrum 𝕜 a)

Tactic:
exact ae_restrict_of_forall_mem hs fun x hx ↦
      hf.comp (Continuous.prodMk_right x).continuousOn fun _ hz ↦ ⟨hx, hz⟩

Premises used: Continuous.continuousOn, Continuous.prodMk_right, MeasureTheory.ae_restrict_of_forall_mem, ContinuousOn.comp, 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 : NormedSpace ℝ A
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 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
z : (↑(spectrum 𝕜 a) : Type u_2)
rw :
  Eq.{u_2 + 1} (α := 𝕜) (∫ (x : X), f x (↑z : 𝕜) ∂μ)
    (∫ (x : X),
      (mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 : (a : (↑(spectrum 𝕜 a) : Type u_2)) → 𝕜) z ∂μ)
⊢ Eq (α := 𝕜) (∫ (x : X), f x (↑z : 𝕜) ∂μ : 𝕜)
    ((∫ (x : X), mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 ∂μ :
          (a : (↑(spectrum 𝕜 a) : Type u_2)) → 𝕜)
        z :
      𝕜)

Tactic:
rw [integral_apply hf₂]

Premises used: ContinuousMap.integral_apply
-- 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
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 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
z : (↑(spectrum 𝕜 a) : Type u_2)
⊢ Eq.{u_2 + 1} (α := 𝕜) (∫ (x : X), f x (↑z : 𝕜) ∂μ)
    (∫ (x : X),
      (mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 : (a : (↑(spectrum 𝕜 a) : Type u_2)) → 𝕜) z ∂μ)

Tactic:
integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- 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
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 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
z : (↑(spectrum 𝕜 a) : Type u_2)
refine :
  Filter.EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ) (fun (x : X) ↦ f x (↑z : 𝕜)) fun (x : X) ↦
    (mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 : (a : (↑(spectrum 𝕜 a) : Type u_2)) → 𝕜) z
⊢ Eq.{u_2 + 1} (α := 𝕜) (∫ (x : X), f x (↑z : 𝕜) ∂μ)
    (∫ (x : X),
      (mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 : (a : (↑(spectrum 𝕜 a) : Type u_2)) → 𝕜) z ∂μ)

Tactic:
refine integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- 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
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 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
z : (↑(spectrum 𝕜 a) : Type u_2)
h :
  ∀ (x : X) (cont_x : ContinuousOn (f x) (spectrum 𝕜 a)),
    f x (↑z : 𝕜) =
      (mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 : (a : (↑(spectrum 𝕜 a) : Type u_2)) → 𝕜) z
⊢ Filter.EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ) (fun (x : X) ↦ f x (↑z : 𝕜)) fun (x : X) ↦
    (mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 : (a : (↑(spectrum 𝕜 a) : Type u_2)) → 𝕜) z

Tactic:
filter_upwards [hf₁] with x cont_x
-- 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
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 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
z : (↑(spectrum 𝕜 a) : Type u_2)
x : X
cont_x : ContinuousOn (f x) (spectrum 𝕜 a)
h h₁ : f x (↑z : 𝕜) = f x (↑z : 𝕜)
⊢ f x (↑z : 𝕜) =
    (mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 : (a : (↑(spectrum 𝕜 a) : Type u_2)) → 𝕜) z

Tactic:
rw [mkD_apply_of_continuousOn cont_x]

Premises used: ContinuousMap.mkD_apply_of_continuousOn
-- 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
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 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
⊢ ∀ (z : (↑(spectrum 𝕜 a) : Type u_2)),
    Eq (α := 𝕜) (∫ (x : X), f x (↑z : 𝕜) ∂μ : 𝕜)
      ((∫ (x : X), mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 ∂μ :
            (a : (↑(spectrum 𝕜 a) : Type u_2)) → 𝕜)
          z :
        𝕜)

Tactic:
have key₁ (z : spectrum 𝕜 a) :
      ∫ x, f x z ∂μ = (∫ x, mkD ((spectrum 𝕜 a).restrict (f x)) 0 ∂μ) z := by
    rw [integral_apply hf₂]
    refine integral_congr_ae ?_
    filter_upwards [hf₁] with x cont_x
    rw [mkD_apply_of_continuousOn cont_x]
-- 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
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 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
key₁ :
  ∀ (z : (↑(spectrum 𝕜 a) : Type u_2)),
    Eq (α := 𝕜) (∫ (x : X), f x (↑z : 𝕜) ∂μ : 𝕜)
      ((∫ (x : X), mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 ∂μ :
            (a : (↑(spectrum 𝕜 a) : Type u_2)) → 𝕜)
          z :
        𝕜)
z : (↑(spectrum 𝕜 a) : Type u_2)
rw : ContinuousOn (Y := 𝕜) (fun (z : 𝕜) ↦ ∫ (x : X), f x z ∂μ) (spectrum 𝕜 a)
⊢ Eq (α := 𝕜) (∫ (x : X), f x (↑z : 𝕜) ∂μ : 𝕜)
    ((mkD ((spectrum 𝕜 a).restrict (π := fun (z : 𝕜) ↦ 𝕜) fun (z : 𝕜) ↦ ∫ (x : X), f x z ∂μ) 0 :
          (a : (↑(spectrum 𝕜 a) : Type u_2)) → 𝕜)
        z :
      𝕜)

Tactic:
rw [mkD_apply_of_continuousOn]

Premises used: ContinuousMap.mkD_apply_of_continuousOn
-- 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
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 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
key₁ :
  ∀ (z : (↑(spectrum 𝕜 a) : Type u_2)),
    Eq (α := 𝕜) (∫ (x : X), f x (↑z : 𝕜) ∂μ : 𝕜)
      ((∫ (x : X), mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 ∂μ :
            (a : (↑(spectrum 𝕜 a) : Type u_2)) → 𝕜)
          z :
        𝕜)
z : (↑(spectrum 𝕜 a) : Type u_2)
rw :
  Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) fun (z : 𝕜) ↦ ∫ (x : X), f x z ∂μ)
⊢ ContinuousOn (Y := 𝕜) (fun (z : 𝕜) ↦ ∫ (x : X), f x z ∂μ) (spectrum 𝕜 a)

Tactic:
rw [continuousOn_iff_continuous_restrict]

Premises used: continuousOn_iff_continuous_restrict
-- 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
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 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
key₁ :
  ∀ (z : (↑(spectrum 𝕜 a) : Type u_2)),
    Eq (α := 𝕜) (∫ (x : X), f x (↑z : 𝕜) ∂μ : 𝕜)
      ((∫ (x : X), mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 ∂μ :
            (a : (↑(spectrum 𝕜 a) : Type u_2)) → 𝕜)
          z :
        𝕜)
z : (↑(spectrum 𝕜 a) : Type u_2)
⊢ Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) fun (z : 𝕜) ↦ ∫ (x : X), f x z ∂μ)

Tactic:
continuous_congr key₁ |>.mpr ?_

Premises used: Iff.mpr, continuous_congr, Set.restrict
-- 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
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 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
key₁ :
  ∀ (z : (↑(spectrum 𝕜 a) : Type u_2)),
    Eq (α := 𝕜) (∫ (x : X), f x (↑z : 𝕜) ∂μ : 𝕜)
      ((∫ (x : X), mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 ∂μ :
            (a : (↑(spectrum 𝕜 a) : Type u_2)) → 𝕜)
          z :
        𝕜)
z : (↑(spectrum 𝕜 a) : Type u_2)
refine :
  Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑(∫ (x : X), mkD ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 ∂μ) :
      (a : (↑(spectrum 𝕜 a) : Type u_2)) → 𝕜)
⊢ Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ((spectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) fun (z : 𝕜) ↦ ∫ (x : X), f x z ∂μ)

Tactic:
refine continuous_congr key₁ |>.mpr ?_

Premises used: Iff.mpr, continuous_congr