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 : 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)
⊢ Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑(∫ (x : X), mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 ∂μ) :
      (a : (↑(quasispectrum 𝕜 a) : Type u_2)) → 𝕜)

Tactic:
exact map_continuous (∫ x, mkD ((quasispectrum 𝕜 a).restrict (f x)) 0 ∂μ)

Premises used: quasispectrum, ContinuousMapZero.mkD, MeasureTheory.integral, ContinuousMapClass.map_continuous, Set.restrict, OfNat.ofNat
-- 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
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.{u_2 + 1} (α := 𝕜) (∫ (x : X), f x (↑0 : 𝕜) ∂μ) 0

Tactic:
integral_eq_zero_of_ae hf₂

Premises used: MeasureTheory.integral_eq_zero_of_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 : 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.{u_2 + 1} (α := 𝕜) (∫ (x : X), f x (↑0 : 𝕜) ∂μ) 0

Tactic:
exact integral_eq_zero_of_ae hf₂

Premises used: MeasureTheory.integral_eq_zero_of_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 : 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 :
        𝕜)

Tactic:
have key₂ (z : quasispectrum 𝕜 a) :
      ∫ x, f x z ∂μ = mkD ((quasispectrum 𝕜 a).restrict (fun z ↦ ∫ x, f x z ∂μ)) 0 z := by
    rw [mkD_apply_of_continuousOn]
    · rw [continuousOn_iff_continuous_restrict]
      refine continuous_congr key₁ |>.mpr ?_
      exact map_continuous (∫ x, mkD ((quasispectrum 𝕜 a).restrict (f x)) 0 ∂μ)
    · exact integral_eq_zero_of_ae hf₂
-- 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
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 :
        𝕜)
key₂ :
  ∀ (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 :
        𝕜)
simp_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)
        (mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) fun (z : 𝕜) ↦ ∫ (x : X), f x z ∂μ) 0) :
      A)
    (((cfcₙL (p := p) ha : C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀ →L[𝕜] A) :
          (a : C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀) → A)
        (∫ (x : X), mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 ∂μ) :
      A)
⊢ cfcₙ (p := p) (fun (z : 𝕜) ↦ ∫ (x : X), f x z ∂μ) a = ∫ (x : X), cfcₙ (p := p) (f x) a ∂μ

Tactic:
simp_rw [cfcₙ_eq_cfcₙL_mkD _ a, cfcₙL_integral a _ hf₃ ha]

Premises used: cfcₙL_integral, 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
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 :
        𝕜)
key₂ :
  ∀ (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 :
        𝕜)
h :
  Eq.{u_2 + 1} (α := C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀)
    (mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) fun (z : 𝕜) ↦ ∫ (x : X), f x z ∂μ) 0)
    (∫ (x : X), mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 ∂μ)
⊢ 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)
        (mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) fun (z : 𝕜) ↦ ∫ (x : X), f x z ∂μ) 0) :
      A)
    (((cfcₙL (p := p) ha : C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀ →L[𝕜] A) :
          (a : C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀) → A)
        (∫ (x : X), mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 ∂μ) :
      A)

Tactic:
congr
-- 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
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 :
        𝕜)
key₂ :
  ∀ (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 :
        𝕜)
h :
  ∀ (z : (↑(quasispectrum 𝕜 a) : Type u_2)),
    Eq (α := 𝕜)
      ((mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) fun (z : 𝕜) ↦ ∫ (x : X), f x z ∂μ) 0 :
            (a : (↑(quasispectrum 𝕜 a) : Type u_2)) → 𝕜)
          z :
        𝕜)
      ((∫ (x : X), mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 ∂μ :
            (a : (↑(quasispectrum 𝕜 a) : Type u_2)) → 𝕜)
          z :
        𝕜)
⊢ Eq.{u_2 + 1} (α := C((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀)
    (mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) fun (z : 𝕜) ↦ ∫ (x : X), f x z ∂μ) 0)
    (∫ (x : X), mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 ∂μ)

Tactic:
ext z
-- 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
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 :
        𝕜)
key₂ :
  ∀ (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 :
        𝕜)
z : (↑(quasispectrum 𝕜 a) : Type u_2)
h :
  Eq (α := 𝕜)
    ((mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) fun (z : 𝕜) ↦ ∫ (x : X), f x z ∂μ) 0 :
          (a : (↑(quasispectrum 𝕜 a) : Type u_2)) → 𝕜)
        z :
      𝕜)
    (∫ (x : X), f x (↑z : 𝕜) ∂μ : 𝕜)
h₁ h₂ :
  Eq (α := 𝕜)
    ((mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) fun (z : 𝕜) ↦ ∫ (x : X), f x z ∂μ) 0 :
          (a : (↑(quasispectrum 𝕜 a) : Type u_2)) → 𝕜)
        z :
      𝕜)
    ((mkD ((quasispectrum 𝕜 a).restrict (π := fun (z : 𝕜) ↦ 𝕜) fun (z : 𝕜) ↦ ∫ (x : X), f x z ∂μ) 0 :
          (a : (↑(quasispectrum 𝕜 a) : Type u_2)) → 𝕜)
        z :
      𝕜)
⊢ Eq (α := 𝕜)
    ((mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) fun (z : 𝕜) ↦ ∫ (x : X), f x z ∂μ) 0 :
          (a : (↑(quasispectrum 𝕜 a) : Type u_2)) → 𝕜)
        z :
      𝕜)
    ((∫ (x : X), mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0 ∂μ :
          (a : (↑(quasispectrum 𝕜 a) : Type u_2)) → 𝕜)
        z :
      𝕜)

Tactic:
rw [← key₁, key₂]
-- 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
inst_9 : NormedSpace ℝ A
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ.restrict s, ContinuousOn (f x) (quasispectrum 𝕜 a)
hf₂ : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0
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
⊢ cfcₙ (p := p) (fun (z : 𝕜) ↦ ∫ (x : X) in s, f x z ∂μ) a = ∫ (x : X) in s, cfcₙ (p := p) (f x) a ∂μ

Tactic:
cfcₙ_integral' _ _ hf₁ hf₂ hf₃ ha

Premises used: cfcₙ_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
inst_9 : NormedSpace ℝ A
inst_10 : TopologicalSpace X
inst_11 : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_12 : 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:
have : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a) := .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 : NormedSpace ℝ A
inst_10 : TopologicalSpace X
inst_11 : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_12 : 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
this : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)
⊢ cfcₙ (p := p) (fun (r : 𝕜) ↦ ∫ (x : X), f x r ∂μ) a = ∫ (x : X), cfcₙ (p := p) (f x) a ∂μ

Tactic:
cfcₙ_integral' _ _ this f_zero ⟨?_, ?_⟩ ha

Premises used: And.intro, cfcₙ_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
inst_9 : NormedSpace ℝ A
inst_10 : TopologicalSpace X
inst_11 : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_12 : 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
this : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 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) μ
⊢ cfcₙ (p := p) (fun (r : 𝕜) ↦ ∫ (x : X), f x r ∂μ) a = ∫ (x : X), cfcₙ (p := p) (f x) a ∂μ

Tactic:
refine cfcₙ_integral' _ _ this f_zero ⟨?_, ?_⟩ ha

Premises used: And.intro, cfcₙ_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
inst_9 : NormedSpace ℝ A
inst_10 : TopologicalSpace X
inst_11 : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_12 : 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
this : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 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 : NormedSpace ℝ A
inst_10 : TopologicalSpace X
inst_11 : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_12 : 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
this : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 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 : NormedSpace ℝ A
inst_10 : TopologicalSpace X
inst_11 : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_12 : 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
this : ∀ᵐ (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:
hasFiniteIntegral_mkD_restrict_of_bound f _ this 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 : NormedSpace ℝ A
inst_10 : TopologicalSpace X
inst_11 : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_12 : 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
this : ∀ᵐ (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:
exact hasFiniteIntegral_mkD_restrict_of_bound f _ this f_zero bound bound_int bound_ge

Premises used: ContinuousMapZero.hasFiniteIntegral_mkD_restrict_of_bound