awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_8 : TopologicalSpace X
inst_9 : OpensMeasurableSpace X
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) (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
this : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 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) μ
⊢ cfc (p := p) (fun (r : 𝕜) ↦ ∫ (x : X), f x r ∂μ) a = ∫ (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 cfc_integral' _ _ this ⟨?_, ?_⟩ ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral (hypothesis)
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
⊢ cfc (p := p) (fun (r : 𝕜) ↦ ∫ (x : X) in s, f x r ∂μ) a = ∫ (x : X) in s, cfc (p := p) (f x) a ∂μ
have this : ∀ᵐ (x : X) ∂μ.restrict s, ContinuousOn (f x) (spectrum 𝕜 a)
Tactic: have : ∀ᵐ (x : X) ∂(μ.restrict s), ContinuousOn (f x) (spectrum 𝕜 a) :=
    ae_restrict_of_forall_mem hs fun x hx ↦
      hf.comp (Continuous.prodMk_right x).continuousOn fun _ hz ↦ ⟨hx, hz⟩
-- 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
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)
⊢ cfc (p := p) (fun (r : 𝕜) ↦ ∫ (x : X) in s, f x r ∂μ) a = ∫ (x : X) in s, 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) (μ.restrict s)
Tactic: refine cfc_setIntegral' _ _ this ⟨?_, ?_⟩ 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 : 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)
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)
⊢ cfc (p := p) (fun (r : 𝕜) ↦ ∫ (x : X) in s, f x r ∂μ) a = ∫ (x : X) in s, 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) (μ.restrict s)
Tactic: refine cfc_setIntegral' _ _ this ⟨?_, ?_⟩ 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 : 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ₙ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)
have 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)
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 : 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
| cfcₙ (p := p) (f x) a
have 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)
Tactic: rw [cfcₙ_eq_cfcₙL_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 : 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ₙ (p := p) (f x) a) μ
have 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))
  μ
Tactic: conv in cfcₙ _ _ => rw [cfcₙ_eq_cfcₙL_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 : 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) μ
have 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) μ
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 : 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) μ
⊢ Integrable.{u_3, u_1} (ε := A) (fun (x : X) ↦ cfcₙ (p := p) (f x) a) μ
have 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) μ
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 : 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) μ
have refine_2 : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)
Tactic: refine hasFiniteIntegral_mkD_restrict_of_bound f _ ?_ f_zero 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 : 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 μ
have 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) (μ.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 : 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
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) (μ.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((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀)
  (fun (x : X) ↦ mkD ((quasispectrum 𝕜 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 : 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
⊢ HasFiniteIntegral.{u_1, u_2} (ε := C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀)
    (fun (x : X) ↦ mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) (μ.restrict s)
have refine_2 : ∀ᵐ (x : X) ∂μ.restrict s, ContinuousOn (f x) (quasispectrum 𝕜 a)
Tactic: refine hasFiniteIntegral_mkD_restrict_of_bound f _ ?_ f_zero 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 : 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
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)
hf₂ : ∀ᵐ (x : X) ∂μ, f x 0 = 0
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
z : (↑(quasispectrum 𝕜 a) : Type u_2)
⊢ Eq (α := 𝕜) (∫ (x : X), f x (↑z : 𝕜) ∂μ : 𝕜)
    ((∫ (x : X), mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 ∂μ :
          (a : (↑(quasispectrum 𝕜 a) : Type u_2)) → 𝕜)
        z :
      𝕜)
have rw : Eq.{u_2 + 1} (α := 𝕜) (∫ (x : X), f x (↑z : 𝕜) ∂μ)
  (∫ (x : X),
    (mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 : (a : (↑(quasispectrum 𝕜 a) : Type u_2)) → 𝕜)
      z ∂μ)
Tactic: rw [integral_apply 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 : 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
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)
hf₂ : ∀ᵐ (x : X) ∂μ, f x 0 = 0
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
z : (↑(quasispectrum 𝕜 a) : Type u_2)
⊢ Eq.{u_2 + 1} (α := 𝕜) (∫ (x : X), f x (↑z : 𝕜) ∂μ)
    (∫ (x : X),
      (mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 : (a : (↑(quasispectrum 𝕜 a) : Type u_2)) → 𝕜)
        z ∂μ)
have refine : Filter.EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ) (fun (x : X) ↦ f x (↑z : 𝕜)) fun (x : X) ↦
  (mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 : (a : (↑(quasispectrum 𝕜 a) : Type u_2)) → 𝕜) z
Tactic: refine integral_congr_ae ?_
-- 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 : 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
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)
hf₂ : ∀ᵐ (x : X) ∂μ, f x 0 = 0
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
z : (↑(quasispectrum 𝕜 a) : Type u_2)
⊢ Filter.EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ) (fun (x : X) ↦ f x (↑z : 𝕜)) fun (x : X) ↦
    (mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 : (a : (↑(quasispectrum 𝕜 a) : Type u_2)) → 𝕜) z
have h : ∀ (x : X) (cont_x : ContinuousOn (f x) (quasispectrum 𝕜 a)) (zero_x : f x 0 = 0),
  f x (↑z : 𝕜) =
    (mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 : (a : (↑(quasispectrum 𝕜 a) : Type u_2)) → 𝕜) z
Tactic: filter_upwards [hf₁, hf₂] with x cont_x zero_x
-- 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 : 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
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)
hf₂ : ∀ᵐ (x : X) ∂μ, f x 0 = 0
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
z : (↑(quasispectrum 𝕜 a) : Type u_2)
x : X
cont_x : ContinuousOn (f x) (quasispectrum 𝕜 a)
zero_x : f x 0 = 0
⊢ f x (↑z : 𝕜) =
    (mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 : (a : (↑(quasispectrum 𝕜 a) : Type u_2)) → 𝕜) z
have h : f x (↑z : 𝕜) = f x (↑z : 𝕜)
Tactic: rw [mkD_apply_of_continuousOn cont_x zero_x]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral (hypothesis)
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
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)
hf₂ : ∀ᵐ (x : X) ∂μ, f x 0 = 0
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
⊢ cfcₙ (p := p) (fun (z : 𝕜) ↦ ∫ (x : X), f x z ∂μ) a = ∫ (x : X), cfcₙ (p := p) (f x) a ∂μ
have key₁ : ∀ (z : (↑(quasispectrum 𝕜 a) : Type u_2)),
  Eq (α := 𝕜) (∫ (x : X), f x (↑z : 𝕜) ∂μ : 𝕜)
    ((∫ (x : X), mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 ∂μ :
          (a : (↑(quasispectrum 𝕜 a) : Type u_2)) → 𝕜)
        z :
      𝕜)
Tactic: have key₁ (z : quasispectrum 𝕜 a) :
      ∫ x, f x z ∂μ = (∫ x, mkD ((quasispectrum 𝕜 a).restrict (f x)) 0 ∂μ) z := by
    rw [integral_apply hf₃]
    refine integral_congr_ae ?_
    filter_upwards [hf₁, hf₂] with x cont_x zero_x
    rw [mkD_apply_of_continuousOn cont_x zero_x]
-- 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 : 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
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)
hf₂ : ∀ᵐ (x : X) ∂μ, f x 0 = 0
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
key₁ :
  ∀ (z : (↑(quasispectrum 𝕜 a) : Type u_2)),
    Eq (α := 𝕜) (∫ (x : X), f x (↑z : 𝕜) ∂μ : 𝕜)
      ((∫ (x : X), mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 ∂μ :
            (a : (↑(quasispectrum 𝕜 a) : Type u_2)) → 𝕜)
          z :
        𝕜)
z : (↑(quasispectrum 𝕜 a) : Type u_2)
⊢ Eq (α := 𝕜) (∫ (x : X), f x (↑z : 𝕜) ∂μ : 𝕜)
    ((mkD ((quasispectrum 𝕜 a).restrict (π := fun (z : 𝕜) ↦ 𝕜) fun (z : 𝕜) ↦ ∫ (x : X), f x z ∂μ) 0 :
          (a : (↑(quasispectrum 𝕜 a) : Type u_2)) → 𝕜)
        z :
      𝕜)
have hf : ContinuousOn (Y := 𝕜) (fun (z : 𝕜) ↦ ∫ (x : X), f x z ∂μ) (quasispectrum 𝕜 a)
Tactic: rw [mkD_apply_of_continuousOn]