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
inst_10 : TopologicalSpace X
inst_11 : OpensMeasurableSpace X
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_12 : 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
⊢ ∀ᵐ (x : X) ∂μ.restrict s, ContinuousOn (f x) (quasispectrum 𝕜 a)

Tactic:
have : ∀ᵐ (x : X) ∂(μ.restrict s), ContinuousOn (f x) (quasispectrum 𝕜 a) :=
    ae_restrict_of_forall_mem hs fun x hx ↦
      hf.comp (Continuous.prodMk_right x).continuousOn fun _ hz ↦ ⟨hx, 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
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_12 : 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
this : ∀ᵐ (x : X) ∂μ.restrict s, ContinuousOn (f x) (quasispectrum 𝕜 a)
⊢ cfcₙ (p := p) (fun (r : 𝕜) ↦ ∫ (x : X) in s, f x r ∂μ) a = ∫ (x : X) in s, cfcₙ (p := p) (f x) a ∂μ

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

Premises used: And.intro, cfcₙ_setIntegral'
-- 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
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_12 : 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
this : ∀ᵐ (x : X) ∂μ.restrict s, 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) (μ.restrict s)
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)
⊢ cfcₙ (p := p) (fun (r : 𝕜) ↦ ∫ (x : X) in s, f x r ∂μ) a = ∫ (x : X) in s, cfcₙ (p := p) (f x) a ∂μ

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

Premises used: And.intro, cfcₙ_setIntegral'
-- 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
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_12 : 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
this : ∀ᵐ (x : X) ∂μ.restrict s, 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) (μ.restrict s)

Tactic:
aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry hs _ _ hf f_zero

Premises used: ContinuousMapZero.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 : 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
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_12 : 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
this : ∀ᵐ (x : X) ∂μ.restrict s, 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) (μ.restrict s)

Tactic:
exact aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry hs _ _ hf f_zero

Premises used: ContinuousMapZero.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 : 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
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_12 : 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
this : ∀ᵐ (x : X) ∂μ.restrict s, 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) (μ.restrict s)

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
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst_12 : 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
this : ∀ᵐ (x : X) ∂μ.restrict s, 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) (μ.restrict s)

Tactic:
exact hasFiniteIntegral_mkD_restrict_of_bound f _ this f_zero bound bound_int bound_ge

Premises used: ContinuousMapZero.hasFiniteIntegral_mkD_restrict_of_bound
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : MetricSpace A
inst_8 : Algebra R A
inst_9 : IsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
⊢ Isometry.{u_1, u_2} (α := C((↑(σ R a) : Type u_1), R)) (β := A)
    (⇑(cfcHom (p := p) ⋯) : (a : C((↑(σ R a) : Type u_1), R)) → A)

Tactic:
IsometricContinuousFunctionalCalculus.isometric a ha

Premises used: IsometricContinuousFunctionalCalculus.isometric
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
f : C((↑(σ 𝕜 a) : Type u_1), 𝕜)
ha : p a
⊢ norm.{u_2} (E := A) ((cfcHom (p := p) ⋯ : (a : C((↑(σ 𝕜 a) : Type u_1), 𝕜)) → A) f : A) = ‖f‖

Tactic:
isometry_cfcHom a |>.norm_map_of_map_zero (map_zero _) f

Premises used: map_zero, Isometry.norm_map_of_map_zero
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
f : C((↑(σ 𝕜 a) : Type u_1), 𝕜)
ha : p a
⊢ norm.{u_2} (E := A) ((cfcHom (p := p) ⋯ : (a : C((↑(σ 𝕜 a) : Type u_1), 𝕜)) → A) f : A) = ‖f‖

Tactic:
refine isometry_cfcHom a |>.norm_map_of_map_zero (map_zero _) f

Premises used: map_zero, Isometry.norm_map_of_map_zero
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
f : C((↑(σ 𝕜 a) : Type u_1), 𝕜)
ha : p a
⊢ nnnorm.{u_2} (E := A) ((cfcHom (p := p) ⋯ : (a : C((↑(σ 𝕜 a) : Type u_1), 𝕜)) → A) f : A) = ‖f‖₊

Tactic:
Subtype.ext <| norm_cfcHom a f ha

Premises used: NNReal, norm_cfcHom, Subtype.ext
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
obtain :
  ∀ (x : ℝ) (hx : IsGreatest ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a) x),
    IsGreatest ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a) ‖cfc (p := p) f a‖
⊢ IsGreatest ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a) ‖cfc (p := p) f a‖

Tactic:
obtain ⟨x, hx⟩ := ContinuousFunctionalCalculus.isCompact_spectrum a
    |>.image_of_continuousOn hf.norm |>.exists_isGreatest <|
    (ContinuousFunctionalCalculus.spectrum_nonempty a ha).image _

Premises used: ContinuousFunctionalCalculus.isCompact_spectrum, Set.Nonempty.image, IsCompact.image_of_continuousOn, ContinuousOn.norm, IsCompact.exists_isGreatest, ContinuousFunctionalCalculus.spectrum_nonempty
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
x : ℝ
hx : IsGreatest ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a) x
obtain :
  ∀ (x : 𝕜) (hx' : x ∈ σ 𝕜 a) (hx : IsGreatest (α := ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a) ((fun (x : 𝕜) ↦ ‖f x‖) x)),
    IsGreatest ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a) ‖cfc (p := p) f a‖
⊢ IsGreatest ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a) ‖cfc (p := p) f a‖

Tactic:
obtain ⟨x, hx', rfl⟩ := hx.1

Premises used: And.left, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
x : 𝕜
hx' : x ∈ σ 𝕜 a
hx : IsGreatest (α := ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a) ((fun (x : 𝕜) ↦ ‖f x‖) x)
⊢ IsGreatest (α := ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a) ((fun (x : 𝕜) ↦ ‖f x‖) x)

Tactic:
hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
x : 𝕜
hx' : x ∈ σ 𝕜 a
hx : IsGreatest (α := ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a) ((fun (x : 𝕜) ↦ ‖f x‖) x)
h : ‖cfc (p := p) f a‖ = (fun (x : 𝕜) ↦ ‖f x‖) x
⊢ IsGreatest ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a) ‖cfc (p := p) f a‖

Tactic:
convert! hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
x : 𝕜
hx' : x ∈ σ 𝕜 a
hx : IsGreatest (α := ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a) ((fun (x : 𝕜) ↦ ‖f x‖) x)
h :
  ‖{ toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σ 𝕜 a) : Type u_1), 𝕜) }‖ =
    (fun (x : 𝕜) ↦ ‖f x‖) x
⊢ ‖cfc (p := p) f a‖ = (fun (x : 𝕜) ↦ ‖f x‖) x

Tactic:
rw [cfc_apply f a, norm_cfcHom a _]

Premises used: cfc_apply, norm_cfcHom
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
x : 𝕜
hx' : x ∈ σ 𝕜 a
hx : IsGreatest (α := ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a) ((fun (x : 𝕜) ↦ ‖f x‖) x)
h :
  ‖{ toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σ 𝕜 a) : Type u_1), 𝕜) }‖ ≤
    (fun (x : 𝕜) ↦ ‖f x‖) x
h₁ :
  (fun (x : 𝕜) ↦ ‖f x‖) x ≤
    ‖{ toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σ 𝕜 a) : Type u_1), 𝕜) }‖
⊢ ‖{ toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σ 𝕜 a) : Type u_1), 𝕜) }‖ =
    (fun (x : 𝕜) ↦ ‖f x‖) x

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
x : 𝕜
hx' : x ∈ σ 𝕜 a
hx : IsGreatest (α := ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a) ((fun (x : 𝕜) ↦ ‖f x‖) x)
h :
  ∀ (x_1 : (↑(σ 𝕜 a) : Type u_1)),
    norm (E := 𝕜)
        (({ toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σ 𝕜 a) : Type u_1), 𝕜) } :
              (a : (↑(σ 𝕜 a) : Type u_1)) → 𝕜)
            x_1 :
          𝕜) ≤
      ‖f x‖
⊢ ‖{ toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σ 𝕜 a) : Type u_1), 𝕜) }‖ ≤
    (fun (x : 𝕜) ↦ ‖f x‖) x

Tactic:
apply ContinuousMap.norm_le _ (norm_nonneg _) |>.mpr

Premises used: Iff.mpr, ContinuousMap.norm_le, norm_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
x : 𝕜
hx' : x ∈ σ 𝕜 a
hx : IsGreatest (α := ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a) ((fun (x : 𝕜) ↦ ‖f x‖) x)
y : 𝕜
hy : y ∈ σ 𝕜 a
⊢ norm (E := 𝕜)
      (({ toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σ 𝕜 a) : Type u_1), 𝕜) } :
            (a : (↑(σ 𝕜 a) : Type u_1)) → 𝕜)
          (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ σ 𝕜 a) y hy) :
        𝕜) ≤
    ‖f x‖

Tactic:
hx.2 ⟨y, hy, rfl⟩

Premises used: And.right, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
x : 𝕜
hx' : x ∈ σ 𝕜 a
hx : IsGreatest (α := ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a) ((fun (x : 𝕜) ↦ ‖f x‖) x)
y : 𝕜
hy : y ∈ σ 𝕜 a
⊢ norm (E := 𝕜)
      (({ toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σ 𝕜 a) : Type u_1), 𝕜) } :
            (a : (↑(σ 𝕜 a) : Type u_1)) → 𝕜)
          (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ σ 𝕜 a) y hy) :
        𝕜) ≤
    ‖f x‖

Tactic:
exact hx.2 ⟨y, hy, rfl⟩

Premises used: And.right, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
x : 𝕜
hx' : x ∈ σ 𝕜 a
hx : IsGreatest (α := ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a) ((fun (x : 𝕜) ↦ ‖f x‖) x)
⊢ (fun (x : 𝕜) ↦ ‖f x‖) x ≤
    norm (E := 𝕜)
      (({ toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σ 𝕜 a) : Type u_1), 𝕜) } :
            (a : { x : 𝕜 // x ∈ σ 𝕜 a }) → 𝕜)
          (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ σ 𝕜 a) x hx') :
        𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
x : 𝕜
hx' : x ∈ σ 𝕜 a
hx : IsGreatest (α := ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a) ((fun (x : 𝕜) ↦ ‖f x‖) x)
⊢ (fun (x : 𝕜) ↦ ‖f x‖) x ≤
    ‖{ toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σ 𝕜 a) : Type u_1), 𝕜) }‖

Tactic:
exact le_trans (by simp) <| ContinuousMap.norm_coe_le_norm _ (⟨x, hx'⟩ : σ 𝕜 a)

Premises used: ContinuousMap.norm_coe_le_norm, Subtype.mk, le_trans
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
⊢ IsGreatest (Real.toNNReal '' (fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a) ‖cfc (p := p) f a‖.toNNReal

Tactic:
Real.toNNReal_monotone.map_isGreatest (.norm_cfc f a)

Premises used: IsGreatest.norm_cfc, Real.toNNReal_monotone, Monotone.map_isGreatest
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
h : (fun (x : 𝕜) ↦ ‖f x‖₊) '' σ 𝕜 a = Real.toNNReal '' (fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a
h₁ : ‖cfc (p := p) f a‖₊ = ‖cfc (p := p) f a‖.toNNReal
⊢ IsGreatest ((fun (x : 𝕜) ↦ ‖f x‖₊) '' σ 𝕜 a) ‖cfc (p := p) f a‖₊

Tactic:
convert! Real.toNNReal_monotone.map_isGreatest (.norm_cfc f a)

Premises used: IsGreatest.norm_cfc, Real.toNNReal_monotone, Monotone.map_isGreatest
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
⊢ (fun (x : 𝕜) ↦ ‖f x‖₊) '' σ 𝕜 a = Real.toNNReal '' (fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a

Tactic:
simp [Set.image_image, norm_toNNReal]

Premises used: Set.image_image, norm_toNNReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
⊢ ‖cfc (p := p) f a‖₊ = ‖cfc (p := p) f a‖.toNNReal

Tactic:
simp [Set.image_image, norm_toNNReal]

Premises used: Set.image_image, norm_toNNReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
x : 𝕜
hx : x ∈ σ 𝕜 a
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
revert : ∀ (hx : x ∈ σ 𝕜 a), ‖f x‖ ≤ ‖cfc (p := p) f a‖
⊢ ‖f x‖ ≤ ‖cfc (p := p) f a‖

Tactic:
revert hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
x : 𝕜
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
⊢ Nontrivial A

Tactic:
nontriviality A
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
x : 𝕜
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
h : Nontrivial A
⊢ ∀ (hx : x ∈ σ 𝕜 a), ‖f x‖ ≤ ‖cfc (p := p) f a‖

Tactic:
(IsGreatest.norm_cfc f a hf ha |>.2 ⟨x, ·, rfl⟩)

Premises used: IsGreatest.norm_cfc, And.right, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
x : 𝕜
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
h : Nontrivial A
⊢ ∀ (hx : x ∈ σ 𝕜 a), ‖f x‖ ≤ ‖cfc (p := p) f a‖

Tactic:
exact (IsGreatest.norm_cfc f a hf ha |>.2 ⟨x, ·, rfl⟩)

Premises used: IsGreatest.norm_cfc, And.right, And.intro, Exists.intro, rfl