-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Integral.lean
/-- The non-unital continuous functional calculus commutes with integration. -/
lemma cfcₙ_integral [TopologicalSpace X] [OpensMeasurableSpace X] (f : X → 𝕜 → 𝕜)
    (bound : X → ℝ) (a : A) [SecondCountableTopologyEither X C(quasispectrum 𝕜 a, 𝕜)₀]
    (hf₁ : ∀ x, ContinuousOn (f x) (quasispectrum 𝕜 a))
    (hf₂ : ∀ x, f x 0 = 0)
    (hf₃ : Continuous (fun x ↦ (⟨⟨_, hf₁ x |>.restrict⟩, hf₂ x⟩ : C(quasispectrum 𝕜 a, 𝕜)₀)))
    (hbound : ∀ x, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖)
    (hbound_finite_integral : HasFiniteIntegral bound μ) (ha : p a

Proof state:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : RCLike 𝕜
inst✝¹¹ : MeasurableSpace X
μ : Measure X
inst✝¹⁰ : NonUnitalNormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : CompleteSpace A
inst✝⁷ : NormedSpace 𝕜 A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : NonUnitalContinuousFunctionalCalculus 𝕜 p
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)₀
hf₁ : ∀ (x : X), ContinuousOn (f x) (quasispectrum 𝕜 a)
hf₂ : ∀ (x : X), f x 0 = 0
hf₃ : Continuous fun x => { toFun := (quasispectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯, map_zero' := ⋯ }
hbound : ∀ (x : X), ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖
hbound_finite_integral : HasFiniteIntegral bound μ
ha : autoParam (p a) _auto✝
fc : X → C(↑(quasispectrum 𝕜 a), 𝕜)₀ :=
  fun x => { toFun := (quasispectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯, map_zero' := ⋯ }
fc_integrable : Integrable fc μ
h_int_fc : ((quasispectrum 𝕜 a).restrict fun x => ∫ (x_1 : X), f x_1 x ∂μ) = ⇑(∫ (x : X), fc x ∂μ)
hcont₂ : ContinuousOn (fun r => ∫ (x : X), f x r ∂μ) (quasispectrum 𝕜 a)
⊢ cfcₙ (fun r => ∫ (x : X), f x r ∂μ) a = ∫ (x : X), cfcₙ (f x) a ∂μ

Tactic:
rw [integral_congr_ae (.of_forall fun _ ↦ cfcₙ_apply ..), cfcₙ_apply ..,
  cfcₙHom_integral _ _ fc_integrable]

Result:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : RCLike 𝕜
inst✝¹¹ : MeasurableSpace X
μ : Measure X
inst✝¹⁰ : NonUnitalNormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : CompleteSpace A
inst✝⁷ : NormedSpace 𝕜 A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : NonUnitalContinuousFunctionalCalculus 𝕜 p
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)₀
hf₁ : ∀ (x : X), ContinuousOn (f x) (quasispectrum 𝕜 a)
hf₂ : ∀ (x : X), f x 0 = 0
hf₃ : Continuous fun x => { toFun := (quasispectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯, map_zero' := ⋯ }
hbound : ∀ (x : X), ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖
hbound_finite_integral : HasFiniteIntegral bound μ
ha : autoParam (p a) _auto✝
fc : X → C(↑(quasispectrum 𝕜 a), 𝕜)₀ :=
  fun x => { toFun := (quasispectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯, map_zero' := ⋯ }
fc_integrable : Integrable fc μ
h_int_fc : ((quasispectrum 𝕜 a).restrict fun x => ∫ (x_1 : X), f x_1 x ∂μ) = ⇑(∫ (x : X), fc x ∂μ)
hcont₂ : ContinuousOn (fun r => ∫ (x : X), f x r ∂μ) (quasispectrum 𝕜 a)
⊢ (cfcₙHom ha)
      { toFun := (quasispectrum 𝕜 a).restrict fun r => ∫ (x : X), f x r ∂μ, continuous_toFun := ⋯, map_zero' := ⋯ } =
    (cfcₙHom ha) (∫ (x : X), fc x ∂μ)

Proof state:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : RCLike 𝕜
inst✝¹¹ : MeasurableSpace X
μ : Measure X
inst✝¹⁰ : NonUnitalNormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : CompleteSpace A
inst✝⁷ : NormedSpace 𝕜 A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : NonUnitalContinuousFunctionalCalculus 𝕜 p
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)₀
hf₁ : ∀ (x : X), ContinuousOn (f x) (quasispectrum 𝕜 a)
hf₂ : ∀ (x : X), f x 0 = 0
hf₃ : Continuous fun x => { toFun := (quasispectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯, map_zero' := ⋯ }
hbound : ∀ (x : X), ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖
hbound_finite_integral : HasFiniteIntegral bound μ
ha : autoParam (p a) _auto✝
fc : X → C(↑(quasispectrum 𝕜 a), 𝕜)₀ :=
  fun x => { toFun := (quasispectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯, map_zero' := ⋯ }
⊢ HasFiniteIntegral fc μ

Tactic:
refine hbound_finite_integral.mono <| .of_forall fun x ↦ ?_

Result:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : RCLike 𝕜
inst✝¹¹ : MeasurableSpace X
μ : Measure X
inst✝¹⁰ : NonUnitalNormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : CompleteSpace A
inst✝⁷ : NormedSpace 𝕜 A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : NonUnitalContinuousFunctionalCalculus 𝕜 p
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)₀
hf₁ : ∀ (x : X), ContinuousOn (f x) (quasispectrum 𝕜 a)
hf₂ : ∀ (x : X), f x 0 = 0
hf₃ : Continuous fun x => { toFun := (quasispectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯, map_zero' := ⋯ }
hbound : ∀ (x : X), ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖
hbound_finite_integral : HasFiniteIntegral bound μ
ha : autoParam (p a) _auto✝
fc : X → C(↑(quasispectrum 𝕜 a), 𝕜)₀ :=
  fun x => { toFun := (quasispectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯, map_zero' := ⋯ }
x : X
⊢ ‖fc x‖ ≤ ‖bound x‖

Proof state:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : RCLike 𝕜
inst✝¹¹ : MeasurableSpace X
μ : Measure X
inst✝¹⁰ : NonUnitalNormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : CompleteSpace A
inst✝⁷ : NormedSpace 𝕜 A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : NonUnitalContinuousFunctionalCalculus 𝕜 p
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)₀
hf₁ : ∀ (x : X), ContinuousOn (f x) (quasispectrum 𝕜 a)
hf₂ : ∀ (x : X), f x 0 = 0
hf₃ : Continuous fun x => { toFun := (quasispectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯, map_zero' := ⋯ }
hbound : ∀ (x : X), ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖
hbound_finite_integral : HasFiniteIntegral bound μ
ha : autoParam (p a) _auto✝
fc : X → C(↑(quasispectrum 𝕜 a), 𝕜)₀ :=
  fun x => { toFun := (quasispectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯, map_zero' := ⋯ }
fc_integrable : Integrable fc μ
h_int_fc : ((quasispectrum 𝕜 a).restrict fun x => ∫ (x_1 : X), f x_1 x ∂μ) = ⇑(∫ (x : X), fc x ∂μ)
⊢ ContinuousOn (fun r => ∫ (x : X), f x r ∂μ) (quasispectrum 𝕜 a)

Tactic:
rw [continuousOn_iff_continuous_restrict]

Result:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : RCLike 𝕜
inst✝¹¹ : MeasurableSpace X
μ : Measure X
inst✝¹⁰ : NonUnitalNormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : CompleteSpace A
inst✝⁷ : NormedSpace 𝕜 A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : NonUnitalContinuousFunctionalCalculus 𝕜 p
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)₀
hf₁ : ∀ (x : X), ContinuousOn (f x) (quasispectrum 𝕜 a)
hf₂ : ∀ (x : X), f x 0 = 0
hf₃ : Continuous fun x => { toFun := (quasispectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯, map_zero' := ⋯ }
hbound : ∀ (x : X), ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖
hbound_finite_integral : HasFiniteIntegral bound μ
ha : autoParam (p a) _auto✝
fc : X → C(↑(quasispectrum 𝕜 a), 𝕜)₀ :=
  fun x => { toFun := (quasispectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯, map_zero' := ⋯ }
fc_integrable : Integrable fc μ
h_int_fc : ((quasispectrum 𝕜 a).restrict fun x => ∫ (x_1 : X), f x_1 x ∂μ) = ⇑(∫ (x : X), fc x ∂μ)
⊢ Continuous ((quasispectrum 𝕜 a).restrict fun r => ∫ (x : X), f x r ∂μ)