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 : 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)
⊢ 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((↑(quasispectrum 𝕜 a) : Type u_2), 𝕜)₀)
  (fun (x : X) ↦ mkD ((quasispectrum 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) (f x)) 0) (μ.restrict s)
Tactic: refine cfcₙ_setIntegral' _ _ this f_zero ⟨?_, ?_⟩ ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
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 ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a) ‖cfc (p := p) f a‖
have obtain : ∀ (x : ℝ) (hx : IsGreatest ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a) x),
  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 _
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
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
⊢ IsGreatest ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a) ‖cfc (p := p) f a‖
have 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‖
Tactic: obtain ⟨x, hx', rfl⟩ := hx.1
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
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) ‖cfc (p := p) f a‖
have h : ‖cfc (p := p) f a‖ = (fun (x : 𝕜) ↦ ‖f x‖) x
Tactic: convert! hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
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)
⊢ ‖cfc (p := p) f a‖ = (fun (x : 𝕜) ↦ ‖f x‖) x
have h : ‖{ toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := sorry : C((↑(σ 𝕜 a) : Type u_1), 𝕜) }‖ =
  (fun (x : 𝕜) ↦ ‖f x‖) x
Tactic: rw [cfc_apply f a, norm_cfcHom a _]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
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)
⊢ ‖{ toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σ 𝕜 a) : Type u_1), 𝕜) }‖ =
    (fun (x : 𝕜) ↦ ‖f x‖) x
have h : ‖{ toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := sorry : C((↑(σ 𝕜 a) : Type u_1), 𝕜) }‖ ≤
  (fun (x : 𝕜) ↦ ‖f x‖) x
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
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
⊢ ‖{ toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σ 𝕜 a) : Type u_1), 𝕜) }‖ =
    (fun (x : 𝕜) ↦ ‖f x‖) x
have h₁ : (fun (x : 𝕜) ↦ ‖f x‖) x ≤
  ‖{ toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := sorry : C((↑(σ 𝕜 a) : Type u_1), 𝕜) }‖
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
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)
⊢ ‖{ toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σ 𝕜 a) : Type u_1), 𝕜) }‖ ≤
    (fun (x : 𝕜) ↦ ‖f x‖) x
have h : ∀ (x_1 : (↑(σ 𝕜 a) : Type u_1)),
  norm (E := 𝕜)
      (({ toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := sorry : C((↑(σ 𝕜 a) : Type u_1), 𝕜) } :
            (a : (↑(σ 𝕜 a) : Type u_1)) → 𝕜)
          x_1 :
        𝕜) ≤
    ‖f x‖
Tactic: apply ContinuousMap.norm_le _ (norm_nonneg _) |>.mpr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
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 ((fun (x : 𝕜) ↦ ‖f x‖₊) '' σ 𝕜 a) ‖cfc (p := p) f a‖₊
have h : (fun (x : 𝕜) ↦ ‖f x‖₊) '' σ 𝕜 a = Real.toNNReal '' (fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a
Tactic: convert! Real.toNNReal_monotone.map_isGreatest (.norm_cfc f a)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
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
⊢ IsGreatest ((fun (x : 𝕜) ↦ ‖f x‖₊) '' σ 𝕜 a) ‖cfc (p := p) f a‖₊
have h₁ : ‖cfc (p := p) f a‖₊ = ‖cfc (p := p) f a‖.toNNReal
Tactic: convert! Real.toNNReal_monotone.map_isGreatest (.norm_cfc f a)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
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
⊢ ‖f x‖ ≤ ‖cfc (p := p) f a‖
have revert : ∀ (hx : x ∈ σ 𝕜 a), ‖f x‖ ≤ ‖cfc (p := p) f a‖
Tactic: revert hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (hypothesis)
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
⊢ ∀ (hx : x ∈ σ 𝕜 a), ‖f x‖ ≤ ‖cfc (p := p) f a‖
have a₁ : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
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
c : ℝ
hc : 0 ≤ c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ ≤ c
⊢ ‖cfc (p := p) f a‖ ≤ c
have inl : Subsingleton A → ‖cfc (p := p) f a‖ ≤ c
Tactic: obtain (_ | _) := subsingleton_or_nontrivial A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
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
c : ℝ
hc : 0 ≤ c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ ≤ c
inl : Subsingleton A → ‖cfc (p := p) f a‖ ≤ c
⊢ ‖cfc (p := p) f a‖ ≤ c
have inr : Nontrivial A → ‖cfc (p := p) f a‖ ≤ c
Tactic: obtain (_ | _) := subsingleton_or_nontrivial A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
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
c : ℝ
hc : 0 ≤ c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ ≤ c
h_1 : Nontrivial A
⊢ ‖cfc (p := p) f a‖ ≤ c
have inr : ∀ (hf : ContinuousOn f (σ 𝕜 a)) (ha : p a),
  (fun (x : A) ↦ ‖x‖ ≤ c)
    ((cfcHom (p := p) ha : (a : C((↑(σ 𝕜 a) : Type u_1), 𝕜)) → A)
      { toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := sorry : C((↑(σ 𝕜 a) : Type u_1), 𝕜) })
Tactic: refine cfc_cases (‖·‖ ≤ c) a f (by simpa) fun hf ha ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
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
c : ℝ
hc : 0 ≤ c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ ≤ c
h_1 : Nontrivial A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
⊢ (fun (x : A) ↦ ‖x‖ ≤ c)
    ((cfcHom (p := p) ha : (a : C((↑(σ 𝕜 a) : Type u_1), 𝕜)) → A)
      { toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σ 𝕜 a) : Type u_1), 𝕜) })
have inr : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a)) c
Tactic: simp only [← cfc_apply f a, isLUB_le_iff (IsGreatest.norm_cfc f a hf ha |>.isLUB)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
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
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
⊢ ‖cfc (p := p) f a‖ < c
have inl : Subsingleton A → ‖cfc (p := p) f a‖ < c
Tactic: obtain (_ | _) := subsingleton_or_nontrivial A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
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
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
inl : Subsingleton A → ‖cfc (p := p) f a‖ < c
⊢ ‖cfc (p := p) f a‖ < c
have inr : Nontrivial A → ‖cfc (p := p) f a‖ < c
Tactic: obtain (_ | _) := subsingleton_or_nontrivial A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
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
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
h_1 : Nontrivial A
⊢ ‖cfc (p := p) f a‖ < c
have inr : ∀ (hf : ContinuousOn f (σ 𝕜 a)) (ha : p a),
  (fun (x : A) ↦ ‖x‖ < c)
    ((cfcHom (p := p) ha : (a : C((↑(σ 𝕜 a) : Type u_1), 𝕜)) → A)
      { toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := sorry : C((↑(σ 𝕜 a) : Type u_1), 𝕜) })
Tactic: refine cfc_cases (‖·‖ < c) a f (by simpa) fun hf ha ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
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
c : ℝ
hc : 0 < c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c
h_1 : Nontrivial A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
⊢ (fun (x : A) ↦ ‖x‖ < c)
    ((cfcHom (p := p) ha : (a : C((↑(σ 𝕜 a) : Type u_1), 𝕜)) → A)
      { toFun := (σ 𝕜 a).restrict (π := fun (a : 𝕜) ↦ 𝕜) f, continuous_toFun := ⋯ : C((↑(σ 𝕜 a) : Type u_1), 𝕜) })
have inr : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ((fun (x : 𝕜) ↦ ‖f x‖) '' σ 𝕜 a) x → x < c
Tactic: simp only [← cfc_apply f a, (IsGreatest.norm_cfc f a hf ha |>.lt_iff)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (hypothesis)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : MetricSpace A
inst_19 : IsometricContinuousFunctionalCalculus S A q
inst_20 : CompleteSpace R
inst_21 : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : Isometry.{u_1, u_2} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
⊢ Isometry.{u_1, u_3} (α := C((↑(σ R a) : Type u_1), R)) (β := A)
    (⇑(cfcHom (p := p) ha) : (a : C((↑(σ R a) : Type u_1), R)) → A)
have ha' : q a
Tactic: obtain ⟨ha', haf⟩ := h a |>.mp ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (hypothesis)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : MetricSpace A
inst_19 : IsometricContinuousFunctionalCalculus S A q
inst_20 : CompleteSpace R
inst_21 : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : Isometry.{u_1, u_2} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
ha' : q a
⊢ Isometry.{u_1, u_3} (α := C((↑(σ R a) : Type u_1), R)) (β := A)
    (⇑(cfcHom (p := p) ha) : (a : C((↑(σ R a) : Type u_1), R)) → A)
have haf : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
Tactic: obtain ⟨ha', haf⟩ := h a |>.mp ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : MetricSpace A
inst_19 : IsometricContinuousFunctionalCalculus S A q
inst_20 : CompleteSpace R
inst_21 : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : Isometry.{u_1, u_2} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
this : ContinuousFunctionalCalculus R A p
⊢ Isometry.{u_1, u_3} (α := C((↑(σ R a) : Type u_1), R)) (β := A)
    (⇑(cfcHom (p := p) ha) : (a : C((↑(σ R a) : Type u_1), R)) → A)
have rw : Isometry.{u_1, u_3} (α := C((↑(σ R a) : Type u_1), R)) (β := A)
  (⇑(starAlgHom (cfcHom (p := q) ha') haf) : (a : C((↑(σ R a) : Type u_1), R)) → A)
Tactic: rw [cfcHom_eq_restrict f ha ha' haf]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : MetricSpace A
inst_19 : IsometricContinuousFunctionalCalculus S A q
inst_20 : CompleteSpace R
inst_21 : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : Isometry.{u_1, u_2} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
this : ContinuousFunctionalCalculus R A p
⊢ Isometry.{u_1, u_3} (α := C((↑(σ R a) : Type u_1), R)) (β := A)
    (⇑(starAlgHom (cfcHom (p := q) ha') haf) : (a : C((↑(σ R a) : Type u_1), R)) → A)
have refine : ∀ (g₁ g₂ : C((↑(σ R a) : Type u_1), R)),
  dist.{u_3} (α := A) ((starAlgHom (cfcHom (p := q) ha') haf : (a : C((↑(σ R a) : Type u_1), R)) → A) g₁ : A)
      ((starAlgHom (cfcHom (p := q) ha') haf : (a : C((↑(σ R a) : Type u_1), R)) → A) g₂ : A) =
    dist g₁ g₂
Tactic: refine .of_dist_eq fun g₁ g₂ ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : MetricSpace A
inst_19 : IsometricContinuousFunctionalCalculus S A q
inst_20 : CompleteSpace R
inst_21 : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : Isometry.{u_1, u_2} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
this : ContinuousFunctionalCalculus R A p
g₁ g₂ : C((↑(σ R a) : Type u_1), R)
⊢ dist.{u_3} (α := A) ((starAlgHom (cfcHom (p := q) ha') haf : (a : C((↑(σ R a) : Type u_1), R)) → A) g₁ : A)
      ((starAlgHom (cfcHom (p := q) ha') haf : (a : C((↑(σ R a) : Type u_1), R)) → A) g₂ : A) =
    dist g₁ g₂
have simp : dist.{u_2} (α := C((↑(σ S a) : Type u_2), S))
    (ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := sorry : C(R, S) }
      (g₁.comp
        { toFun := Subtype.map (p := fun (x : S) ↦ x ∈ σ S a) (q := fun (x : R) ↦ x ∈ σ R a) (⇑f : (a : S) → R) sorry,
          continuous_toFun := sorry : ContinuousMap.{u_2, u_1} (↑(σ S a) : Type u_2) (↑(σ R a) : Type u_1) }))
    (ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := sorry : C(R, S) }
      (g₂.comp
        { toFun := Subtype.map (p := fun (x : S) ↦ x ∈ σ S a) (q := fun (x : R) ↦ x ∈ σ R a) (⇑f : (a : S) → R) sorry,
          continuous_toFun := sorry : ContinuousMap.{u_2, u_1} (↑(σ S a) : Type u_2) (↑(σ R a) : Type u_1) })) =
  dist g₁ g₂
Tactic: simp only [starAlgHom_apply, isometry_cfcHom a ha' |>.dist_eq]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : MetricSpace A
inst_19 : IsometricContinuousFunctionalCalculus S A q
inst_20 : CompleteSpace R
inst_21 : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : Isometry.{u_1, u_2} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
this : ContinuousFunctionalCalculus R A p
g₁ g₂ : C((↑(σ R a) : Type u_1), R)
⊢ dist.{u_2} (α := C((↑(σ S a) : Type u_2), S))
      (ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ : C(R, S) }
        (g₁.comp
          { toFun := Subtype.map (p := fun (x : S) ↦ x ∈ σ S a) (q := fun (x : R) ↦ x ∈ σ R a) (⇑f : (a : S) → R) ⋯,
            continuous_toFun := ⋯ : ContinuousMap.{u_2, u_1} (↑(σ S a) : Type u_2) (↑(σ R a) : Type u_1) }))
      (ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ : C(R, S) }
        (g₂.comp
          { toFun := Subtype.map (p := fun (x : S) ↦ x ∈ σ S a) (q := fun (x : R) ↦ x ∈ σ R a) (⇑f : (a : S) → R) ⋯,
            continuous_toFun := ⋯ : ContinuousMap.{u_2, u_1} (↑(σ S a) : Type u_2) (↑(σ R a) : Type u_1) })) =
    dist g₁ g₂
have refine_1 : dist.{u_2} (α := C((↑(σ S a) : Type u_2), S))
    (ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := sorry : C(R, S) }
      (g₁.comp
        { toFun := Subtype.map (p := fun (x : S) ↦ x ∈ σ S a) (q := fun (x : R) ↦ x ∈ σ R a) (⇑f : (a : S) → R) sorry,
          continuous_toFun := sorry : ContinuousMap.{u_2, u_1} (↑(σ S a) : Type u_2) (↑(σ R a) : Type u_1) }))
    (ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := sorry : C(R, S) }
      (g₂.comp
        { toFun := Subtype.map (p := fun (x : S) ↦ x ∈ σ S a) (q := fun (x : R) ↦ x ∈ σ R a) (⇑f : (a : S) → R) sorry,
          continuous_toFun := sorry : ContinuousMap.{u_2, u_1} (↑(σ S a) : Type u_2) (↑(σ R a) : Type u_1) })) ≤
  dist g₁ g₂
Tactic: refine le_antisymm ?_ ?_