awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_6 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
hc : 0 < c
h : ∀ x ∈ σ ℝ≥0 a, f x < c
h_1 : Nontrivial A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
⊢ (fun (x : A) ↦ ‖x‖₊ < c)
    ((cfcHom (p := fun (x : A) ↦ 0 ≤ x) ha : (a : C((↑(σ ℝ≥0 a) : Type), ℝ≥0)) → A)
      { toFun := (σ ℝ≥0 a).restrict (π := fun (a : ℝ≥0) ↦ ℝ≥0) f, continuous_toFun := ⋯ : C((↑(σ ℝ≥0 a) : Type), ℝ≥0) })
have inr : ∀ x ∈ f '' σ ℝ≥0 a, x < c
Tactic: simp only [← cfc_apply f a, (IsGreatest.nnnorm_cfc_nnreal f a hf ha |>.lt_iff)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
ha : 0 ≤ a
⊢ IsGreatest (f '' σₙ ℝ≥0 a) ‖cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a‖₊
have rw : IsGreatest (f '' σₙ ℝ≥0 a) ‖cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a‖₊
Tactic: rw [cfcₙ_nnreal_eq_real ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
ha : 0 ≤ a
⊢ IsGreatest (f '' σₙ ℝ≥0 a) ‖cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a‖₊
have ha' : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
Tactic: obtain ⟨-, ha'⟩ := nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts.mp ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
ha : 0 ≤ a
ha' : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ IsGreatest (f '' σₙ ℝ≥0 a) ‖cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a‖₊
have h : f '' σₙ ℝ≥0 a = (fun (x : ℝ) ↦ ‖(↑(f x.toNNReal) : ℝ)‖₊) '' σₙ ℝ a
Tactic: convert! IsGreatest.nnnorm_cfcₙ (fun x : ℝ ↦ (f x.toNNReal : ℝ)) a ?hf_cont (by simpa)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
ha : 0 ≤ a
ha' : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
h : f '' σₙ ℝ≥0 a = (fun (x : ℝ) ↦ ‖(↑(f x.toNNReal) : ℝ)‖₊) '' σₙ ℝ a
⊢ IsGreatest (f '' σₙ ℝ≥0 a) ‖cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a‖₊
have convert! : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (σₙ ℝ a)
Tactic: convert! IsGreatest.nnnorm_cfcₙ (fun x : ℝ ↦ (f x.toNNReal : ℝ)) a ?hf_cont (by simpa)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
x : ℝ≥0
hx : x ∈ σₙ ℝ≥0 a
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
ha : 0 ≤ a
⊢ f x ≤ ‖cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a‖₊
have revert : ∀ (hx : x ∈ σₙ ℝ≥0 a), f x ≤ ‖cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a‖₊
Tactic: revert hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x ≤ c
⊢ ‖cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ ≤ c
have refine : ∀ (hf : ContinuousOn f (σₙ ℝ≥0 a))
  (hf0 :
    Eq (α := ℝ≥0)
      (({ toFun := (σₙ ℝ≥0 a).restrict (π := fun (a : ℝ≥0) ↦ ℝ≥0) f, continuous_toFun := sorry :
            C((↑(σₙ ℝ≥0 a) : Type), ℝ≥0) } :
          (a : (↑(σₙ ℝ≥0 a) : Type)) → ℝ≥0)
        0)
      0)
  (ha : 0 ≤ a),
  (fun (x : A) ↦ ‖x‖₊ ≤ c)
    ((cfcₙHom (p := fun (x : A) ↦ 0 ≤ x) ha : (a : ContinuousMapZero (↑(σₙ ℝ≥0 a) : Type) ℝ≥0) → A)
      { toFun := (σₙ ℝ≥0 a).restrict (π := fun (a : ℝ≥0) ↦ ℝ≥0) f, continuous_toFun := sorry, map_zero' := hf0 :
        ContinuousMapZero (↑(σₙ ℝ≥0 a) : Type) ℝ≥0 })
Tactic: refine cfcₙ_cases (‖·‖₊ ≤ c) a f (by simp) fun hf hf0 ha ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x ≤ c
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 :
  Eq (α := ℝ≥0)
    (({ toFun := (σₙ ℝ≥0 a).restrict (π := fun (a : ℝ≥0) ↦ ℝ≥0) f, continuous_toFun := ⋯ :
          C((↑(σₙ ℝ≥0 a) : Type), ℝ≥0) } :
        (a : (↑(σₙ ℝ≥0 a) : Type)) → ℝ≥0)
      0)
    0
ha : 0 ≤ a
⊢ (fun (x : A) ↦ ‖x‖₊ ≤ c)
    ((cfcₙHom (p := fun (x : A) ↦ 0 ≤ x) ha : (a : ContinuousMapZero (↑(σₙ ℝ≥0 a) : Type) ℝ≥0) → A)
      { toFun := (σₙ ℝ≥0 a).restrict (π := fun (a : ℝ≥0) ↦ ℝ≥0) f, continuous_toFun := ⋯, map_zero' := hf0 :
        ContinuousMapZero (↑(σₙ ℝ≥0 a) : Type) ℝ≥0 })
have simp : c ∈ upperBounds (f '' σₙ ℝ≥0 a)
Tactic: simp only [← cfcₙ_apply f a, isLUB_le_iff (IsGreatest.nnnorm_cfcₙ_nnreal f a hf hf0 ha |>.isLUB)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x < c
⊢ ‖cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ < c
have refine_1 : (fun (x : A) ↦ ‖x‖₊ < c) 0
Tactic: refine cfcₙ_cases (‖·‖₊ < c) a f ?_ fun hf hf0 ha ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x < c
refine_1 : nnnorm.{u_1} (E := A) 0 < c
⊢ ‖cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ < c
have refine_2 : ∀ (hf : ContinuousOn f (σₙ ℝ≥0 a))
  (hf0 :
    Eq (α := ℝ≥0)
      (({ toFun := (σₙ ℝ≥0 a).restrict (π := fun (a : ℝ≥0) ↦ ℝ≥0) f, continuous_toFun := sorry :
            C((↑(σₙ ℝ≥0 a) : Type), ℝ≥0) } :
          (a : (↑(σₙ ℝ≥0 a) : Type)) → ℝ≥0)
        0)
      0)
  (ha : 0 ≤ a),
  (fun (x : A) ↦ ‖x‖₊ < c)
    ((cfcₙHom (p := fun (x : A) ↦ 0 ≤ x) ha : (a : ContinuousMapZero (↑(σₙ ℝ≥0 a) : Type) ℝ≥0) → A)
      { toFun := (σₙ ℝ≥0 a).restrict (π := fun (a : ℝ≥0) ↦ ℝ≥0) f, continuous_toFun := sorry, map_zero' := hf0 :
        ContinuousMapZero (↑(σₙ ℝ≥0 a) : Type) ℝ≥0 })
Tactic: refine cfcₙ_cases (‖·‖₊ < c) a f ?_ fun hf hf0 ha ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x < c
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 :
  Eq (α := ℝ≥0)
    (({ toFun := (σₙ ℝ≥0 a).restrict (π := fun (a : ℝ≥0) ↦ ℝ≥0) f, continuous_toFun := ⋯ :
          C((↑(σₙ ℝ≥0 a) : Type), ℝ≥0) } :
        (a : (↑(σₙ ℝ≥0 a) : Type)) → ℝ≥0)
      0)
    0
ha : 0 ≤ a
⊢ (fun (x : A) ↦ ‖x‖₊ < c)
    ((cfcₙHom (p := fun (x : A) ↦ 0 ≤ x) ha : (a : ContinuousMapZero (↑(σₙ ℝ≥0 a) : Type) ℝ≥0) → A)
      { toFun := (σₙ ℝ≥0 a).restrict (π := fun (a : ℝ≥0) ↦ ℝ≥0) f, continuous_toFun := ⋯, map_zero' := hf0 :
        ContinuousMapZero (↑(σₙ ℝ≥0 a) : Type) ℝ≥0 })
have refine_2 : ∀ x ∈ f '' σₙ ℝ≥0 a, x < c
Tactic: simp only [← cfcₙ_apply f a, (IsGreatest.nnnorm_cfcₙ_nnreal f a hf hf0 ha |>.lt_iff)]
-- 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
a : A
ha : p a
⊢ CompactSpace.{u_1} (↑(σₙ 𝕜 a) : Type u_1)
have h_cpct : CompactSpace.{u_1} (↑(σ 𝕜 a) : Type u_1)
Tactic: have h_cpct : CompactSpace (spectrum 𝕜 a) := inferInstance
-- 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
a : A
ha : p a
h_cpct : CompactSpace.{u_1} (↑(σ 𝕜 a) : Type u_1)
⊢ CompactSpace.{u_1} (↑(σₙ 𝕜 a) : Type u_1)
have simp : ∀ (h_cpct : IsCompact (σ 𝕜 a)), IsCompact (σ 𝕜 a ∪ {0})
Tactic: simp only [← isCompact_iff_compactSpace, quasispectrum_eq_spectrum_union_zero] at h_cpct ⊢
Cleared hypotheses: h_cpct
-- 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
a : A
ha : p a
⊢ Isometry.{u_1, u_2} (α := ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜) (β := A)
    (⇑(cfcₙHom (p := p) ha) : (a : ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜) → A)
have this : CompactSpace.{u_1} (↑(σₙ 𝕜 a) : Type u_1)
Tactic: have : CompactSpace (σₙ 𝕜 a) := by
      have h_cpct : CompactSpace (spectrum 𝕜 a) := inferInstance
      simp only [← isCompact_iff_compactSpace, quasispectrum_eq_spectrum_union_zero] at h_cpct ⊢
      exact h_cpct |>.union isCompact_singleton
-- 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
a : A
ha : p a
this : CompactSpace.{u_1} (↑(σₙ 𝕜 a) : Type u_1)
⊢ Isometry.{u_1, u_2} (α := ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜) (β := A)
    (⇑(cfcₙHom (p := p) ha) : (a : ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜) → A)
have rw : Isometry.{u_1, u_2} (α := ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜) (β := A)
  (⇑(NonUnitalStarAlgHom.comp (↑(cfcHom (p := p) ha) : C((↑(σ 𝕜 a) : Type u_1), 𝕜) →⋆ₙₐ[𝕜] A)
        (NonUnitalStarAlgHom.comp
          (↑(ContinuousMap.compStarAlgHom' 𝕜 𝕜
                { toFun := Set.inclusion (s := σ 𝕜 a) (t := σₙ 𝕜 a) sorry, continuous_toFun := sorry }) :
            C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) →⋆ₙₐ[𝕜] C((↑(σ 𝕜 a) : Type u_1), 𝕜))
          ContinuousMapZero.toContinuousMapHom)) :
    (a : ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜) → A)
Tactic: rw [cfcₙHom_eq_cfcₙHom_of_cfcHom, cfcₙHom_of_cfcHom]
-- 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
a : A
ha : p a
this : CompactSpace.{u_1} (↑(σₙ 𝕜 a) : Type u_1)
⊢ Isometry.{u_1, u_2} (α := ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜) (β := A)
    (⇑(NonUnitalStarAlgHom.comp (↑(cfcHom (p := p) ha) : C((↑(σ 𝕜 a) : Type u_1), 𝕜) →⋆ₙₐ[𝕜] A)
          (NonUnitalStarAlgHom.comp
            (↑(ContinuousMap.compStarAlgHom' 𝕜 𝕜
                  { toFun := Set.inclusion (s := σ 𝕜 a) (t := σₙ 𝕜 a) ⋯, continuous_toFun := ⋯ }) :
              C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) →⋆ₙₐ[𝕜] C((↑(σ 𝕜 a) : Type u_1), 𝕜))
            ContinuousMapZero.toContinuousMapHom)) :
      (a : ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜) → A)
have refine : Isometry (α := ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜) (β := C((↑(σ 𝕜 a) : Type u_1), 𝕜))
  (⇑(↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
            (NonUnitalStarAlgHom.comp
              (↑(ContinuousMap.compStarAlgHom' 𝕜 𝕜
                    { toFun := Set.inclusion (s := σ 𝕜 a) (t := σₙ 𝕜 a) sorry, continuous_toFun := sorry }) :
                C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) →⋆ₙₐ[𝕜] C((↑(σ 𝕜 a) : Type u_1), 𝕜))
              ContinuousMapZero.toContinuousMapHom)) :
        ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜 →ₙ* C((↑(σ 𝕜 a) : Type u_1), 𝕜)) :
    (a_1 : ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜) → C((↑(σ 𝕜 a) : Type u_1), 𝕜))
Tactic: refine isometry_cfcHom a |>.comp ?_
-- 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
a : A
ha : p a
this : CompactSpace.{u_1} (↑(σₙ 𝕜 a) : Type u_1)
⊢ Isometry (α := ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜) (β := C((↑(σ 𝕜 a) : Type u_1), 𝕜))
    (⇑(NonUnitalStarAlgHom.comp
          (↑(ContinuousMap.compStarAlgHom' 𝕜 𝕜
                { toFun := Set.inclusion (s := σ 𝕜 a) (t := σₙ 𝕜 a) ⋯, continuous_toFun := ⋯ }) :
            C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) →⋆ₙₐ[𝕜] C((↑(σ 𝕜 a) : Type u_1), 𝕜))
          ContinuousMapZero.toContinuousMapHom) :
      (a_1 : ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜) → C((↑(σ 𝕜 a) : Type u_1), 𝕜))
have refine : ∀ (f : ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜),
  norm (E := C((↑(σ 𝕜 a) : Type u_1), 𝕜))
      ((NonUnitalStarAlgHom.comp
              (↑(ContinuousMap.compStarAlgHom' 𝕜 𝕜
                    { toFun := Set.inclusion (s := σ 𝕜 a) (t := σₙ 𝕜 a) sorry, continuous_toFun := sorry :
                      C((↑(σ 𝕜 a) : Type u_1), (↑(σₙ 𝕜 a) : Type u_1)) }) :
                C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) →⋆ₙₐ[𝕜] C((↑(σ 𝕜 a) : Type u_1), 𝕜))
              ContinuousMapZero.toContinuousMapHom :
            (a_1 : ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜) → C((↑(σ 𝕜 a) : Type u_1), 𝕜))
          f :
        C((↑(σ 𝕜 a) : Type u_1), 𝕜)) =
    ‖f‖
Tactic: refine AddMonoidHomClass.isometry_of_norm _ fun f ↦ ?_
-- 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
a : A
ha : p a
this : CompactSpace.{u_1} (↑(σₙ 𝕜 a) : Type u_1)
f : ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜
ι : C((↑(σ 𝕜 a) : Type u_1), (↑(σₙ 𝕜 a) : Type u_1)) :=
  { toFun := Set.inclusion (s := σ 𝕜 a) (t := σₙ 𝕜 a) ⋯, continuous_toFun := ⋯ }
⊢ norm (E := C((↑(σ 𝕜 a) : Type u_1), 𝕜))
      ((NonUnitalStarAlgHom.comp
              (↑(ContinuousMap.compStarAlgHom' 𝕜 𝕜
                    { toFun := Set.inclusion (s := σ 𝕜 a) (t := σₙ 𝕜 a) ⋯, continuous_toFun := ⋯ :
                      C((↑(σ 𝕜 a) : Type u_1), (↑(σₙ 𝕜 a) : Type u_1)) }) :
                C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) →⋆ₙₐ[𝕜] C((↑(σ 𝕜 a) : Type u_1), 𝕜))
              ContinuousMapZero.toContinuousMapHom :
            (a_1 : ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜) → C((↑(σ 𝕜 a) : Type u_1), 𝕜))
          f :
        C((↑(σ 𝕜 a) : Type u_1), 𝕜)) =
    ‖f‖
have change : norm (E := C((↑(σ 𝕜 a) : Type u_1), 𝕜)) (ContinuousMap.comp (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) ι) =
  norm (E := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜))
Tactic: change ‖(f : C(σₙ 𝕜 a, 𝕜)).comp ι‖ = ‖(f : C(σₙ 𝕜 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
a : A
ha : p a
this : CompactSpace.{u_1} (↑(σₙ 𝕜 a) : Type u_1)
f : ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜
ι : C((↑(σ 𝕜 a) : Type u_1), (↑(σₙ 𝕜 a) : Type u_1)) :=
  { toFun := Set.inclusion (s := σ 𝕜 a) (t := σₙ 𝕜 a) ⋯, continuous_toFun := ⋯ }
⊢ norm (E := C((↑(σ 𝕜 a) : Type u_1), 𝕜)) (ContinuousMap.comp (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) ι) =
    norm (E := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜))
have apply : ∀ (x : (↑(σ 𝕜 a) : Type u_1)),
  norm (E := 𝕜) ((ContinuousMap.comp (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) ι : (a : (↑(σ 𝕜 a) : Type u_1)) → 𝕜) x : 𝕜) ≤
    norm (E := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜))
Tactic: apply le_antisymm (ContinuousMap.norm_le _ (by positivity) |>.mpr ?_)
      (ContinuousMap.norm_le _ (by positivity) |>.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
a : A
ha : p a
this : CompactSpace.{u_1} (↑(σₙ 𝕜 a) : Type u_1)
f : ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜
ι : C((↑(σ 𝕜 a) : Type u_1), (↑(σₙ 𝕜 a) : Type u_1)) :=
  { toFun := Set.inclusion (s := σ 𝕜 a) (t := σₙ 𝕜 a) ⋯, continuous_toFun := ⋯ }
apply :
  ∀ (x : (↑(σ 𝕜 a) : Type u_1)),
    norm (E := 𝕜) ((ContinuousMap.comp (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) ι : (a : (↑(σ 𝕜 a) : Type u_1)) → 𝕜) x : 𝕜) ≤
      norm (E := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜))
⊢ norm (E := C((↑(σ 𝕜 a) : Type u_1), 𝕜)) (ContinuousMap.comp (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) ι) =
    norm (E := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜))
have apply₁ : ∀ (x : (↑(σₙ 𝕜 a) : Type u_1)),
  norm (E := 𝕜) (((↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) : (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜) x : 𝕜) ≤
    norm (E := C((↑(σ 𝕜 a) : Type u_1), 𝕜)) (ContinuousMap.comp (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) ι)
Tactic: apply le_antisymm (ContinuousMap.norm_le _ (by positivity) |>.mpr ?_)
      (ContinuousMap.norm_le _ (by positivity) |>.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
a : A
ha : p a
this : CompactSpace.{u_1} (↑(σₙ 𝕜 a) : Type u_1)
f : ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜
ι : C((↑(σ 𝕜 a) : Type u_1), (↑(σₙ 𝕜 a) : Type u_1)) :=
  { toFun := Set.inclusion (s := σ 𝕜 a) (t := σₙ 𝕜 a) ⋯, continuous_toFun := ⋯ }
x : 𝕜
hx : x ∈ σₙ 𝕜 a
⊢ norm (E := 𝕜)
      (((↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) : (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜)
          (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ σₙ 𝕜 a) x hx) :
        𝕜) ≤
    norm (E := C((↑(σ 𝕜 a) : Type u_1), 𝕜)) (ContinuousMap.comp (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) ι)
have inl : ∀ (hx : 0 ∈ σₙ 𝕜 a),
  norm (E := 𝕜)
      (((↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) : (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜)
          (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ σₙ 𝕜 a) 0 hx) :
        𝕜) ≤
    norm (E := C((↑(σ 𝕜 a) : Type u_1), 𝕜)) (ContinuousMap.comp (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) ι)
Tactic: obtain (rfl | hx') : x = 0 ∨ x ∈ σ 𝕜 a := by
        simpa [quasispectrum_eq_spectrum_union_zero] using hx
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
a : A
ha : p a
this : CompactSpace.{u_1} (↑(σₙ 𝕜 a) : Type u_1)
f : ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜
ι : C((↑(σ 𝕜 a) : Type u_1), (↑(σₙ 𝕜 a) : Type u_1)) :=
  { toFun := Set.inclusion (s := σ 𝕜 a) (t := σₙ 𝕜 a) ⋯, continuous_toFun := ⋯ }
x : 𝕜
hx : x ∈ σₙ 𝕜 a
inl :
  ∀ (hx : 0 ∈ σₙ 𝕜 a),
    norm (E := 𝕜)
        (((↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) : (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜)
            (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ σₙ 𝕜 a) 0 hx) :
          𝕜) ≤
      norm (E := C((↑(σ 𝕜 a) : Type u_1), 𝕜)) (ContinuousMap.comp (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) ι)
⊢ norm (E := 𝕜)
      (((↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) : (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜)
          (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ σₙ 𝕜 a) x hx) :
        𝕜) ≤
    norm (E := C((↑(σ 𝕜 a) : Type u_1), 𝕜)) (ContinuousMap.comp (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) ι)
have inr : ∀ (hx' : x ∈ σ 𝕜 a),
  norm (E := 𝕜)
      (((↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) : (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜)
          (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ σₙ 𝕜 a) x hx) :
        𝕜) ≤
    norm (E := C((↑(σ 𝕜 a) : Type u_1), 𝕜)) (ContinuousMap.comp (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) ι)
Tactic: obtain (rfl | hx') : x = 0 ∨ x ∈ σ 𝕜 a := by
        simpa [quasispectrum_eq_spectrum_union_zero] using 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
a : A
ha : p a
this : CompactSpace.{u_1} (↑(σₙ 𝕜 a) : Type u_1)
f : ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜
ι : C((↑(σ 𝕜 a) : Type u_1), (↑(σₙ 𝕜 a) : Type u_1)) :=
  { toFun := Set.inclusion (s := σ 𝕜 a) (t := σₙ 𝕜 a) ⋯, continuous_toFun := ⋯ }
hx : 0 ∈ σₙ 𝕜 a
⊢ norm (E := 𝕜)
      (((↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) : (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜)
          (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ σₙ 𝕜 a) 0 hx) :
        𝕜) ≤
    norm (E := C((↑(σ 𝕜 a) : Type u_1), 𝕜)) (ContinuousMap.comp (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) ι)
have inl : norm (E := 𝕜) ((f : (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜) 0 : 𝕜) ≤
  norm (E := C((↑(σ 𝕜 a) : Type u_1), 𝕜)) (ContinuousMap.comp (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) ι)
Tactic: change ‖f 0‖ ≤ _