awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
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
refine_2 :
  ∀ (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 })
⊢ ‖cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ < c

Tactic:
refine cfcₙ_cases (‖·‖₊ < c) a f ?_ fun hf hf0 ha ↦ ?_

Premises used: NNNorm.nnnorm, LT.lt, cfcₙ_cases
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
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
⊢ (fun (x : A) ↦ ‖x‖₊ < c) 0

Tactic:
simpa using (h 0 (quasispectrum.zero_mem ℝ≥0 _)).pos

Premises used: LT.lt.pos, quasispectrum.zero_mem, NNReal, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
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
refine_2 : ∀ x ∈ f '' σₙ ℝ≥0 a, x < c
⊢ nnnorm (E := A)
      ((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 } :
        A) <
    c

Tactic:
simp only [← cfcₙ_apply f a, (IsGreatest.nnnorm_cfcₙ_nnreal f a hf hf0 ha |>.lt_iff)]

Premises used: IsGreatest.lt_iff, IsGreatest.nnnorm_cfcₙ_nnreal, cfcₙ_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
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
x : ℝ≥0
hx : x ∈ σₙ ℝ≥0 a
⊢ f x < c

Tactic:
h x hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
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
x : ℝ≥0
hx : x ∈ σₙ ℝ≥0 a
⊢ f x < c

Tactic:
exact h x hx
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
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
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf₀ : f 0 = 0
ha : 0 ≤ a
⊢ ‖cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ < c ↔ ∀ x ∈ σₙ ℝ≥0 a, f x < c

Tactic:
⟨fun h _ hx ↦ apply_le_nnnorm_cfcₙ_nnreal f a hx hf hf₀ ha |>.trans_lt h, nnnorm_cfcₙ_nnreal_lt⟩

Premises used: nnnorm_cfcₙ_nnreal_lt, Iff.intro, LE.le.trans_lt, apply_le_nnnorm_cfcₙ_nnreal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
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
a : A
ha : 0 ≤ a
⊢ IsGreatest (σₙ ℝ≥0 a) ‖a‖₊

Tactic:
simpa [cfcₙ_id ℝ≥0 a] using IsGreatest.nnnorm_cfcₙ_nnreal id a

Premises used: IsGreatest.nnnorm_cfcₙ_nnreal, id, NNReal, cfcₙ_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
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
a : A
x : ℝ≥0
hx : x ∈ σₙ ℝ≥0 a
ha : 0 ≤ a
⊢ x ≤ ‖a‖₊

Tactic:
simpa [cfcₙ_id ℝ≥0 a] using apply_le_nnnorm_cfcₙ_nnreal id a hx

Premises used: id, NNReal, cfcₙ_id, apply_le_nnnorm_cfcₙ_nnreal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
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 : MonotoneOn f (σₙ ℝ≥0 a)
hf₂ : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
ha : 0 ≤ a
⊢ ‖cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a‖₊ = f ‖a‖₊

Tactic:
IsGreatest.nnnorm_cfcₙ_nnreal f a |>.unique <| hf.map_isGreatest (isGreatest_quasispectrum a)

Premises used: NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_quasispectrum, MonotoneOn.map_isGreatest, IsGreatest.nnnorm_cfcₙ_nnreal, IsGreatest.unique
-- 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
ha : p a
⊢ CompactSpace.{u_1} (↑(σ 𝕜 a) : Type u_1)

Tactic:
have h_cpct : CompactSpace (spectrum 𝕜 a) := inferInstance
-- 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
ha : p a
h_cpct : CompactSpace.{u_1} (↑(σ 𝕜 a) : Type u_1)
simp : ∀ (h_cpct : IsCompact (σ 𝕜 a)), IsCompact (σ 𝕜 a ∪ {0})
⊢ CompactSpace.{u_1} (↑(σₙ 𝕜 a) : Type u_1)

Tactic:
simp only [← isCompact_iff_compactSpace, quasispectrum_eq_spectrum_union_zero] at h_cpct ⊢

Premises used: isCompact_iff_compactSpace, quasispectrum_eq_spectrum_union_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
ha : p a
h_cpct : IsCompact (σ 𝕜 a)
⊢ IsCompact (σ 𝕜 a ∪ {0})

Tactic:
h_cpct |>.union isCompact_singleton

Premises used: isCompact_singleton, IsCompact.union
-- 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
ha : p a
h_cpct : IsCompact (σ 𝕜 a)
⊢ IsCompact (σ 𝕜 a ∪ {0})

Tactic:
exact h_cpct |>.union isCompact_singleton

Premises used: isCompact_singleton, IsCompact.union
-- 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
ha : p a
⊢ 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
-- 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
ha : p a
this : CompactSpace.{u_1} (↑(σₙ 𝕜 a) : Type u_1)
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) ⋯, continuous_toFun := ⋯ }) :
              C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) →⋆ₙₐ[𝕜] C((↑(σ 𝕜 a) : Type u_1), 𝕜))
            ContinuousMapZero.toContinuousMapHom)) :
      (a : ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜) → A)
⊢ Isometry.{u_1, u_2} (α := ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜) (β := A)
    (⇑(cfcₙHom (p := p) ha) : (a : ContinuousMapZero (↑(σₙ 𝕜 a) : Type u_1) 𝕜) → A)

Tactic:
rw [cfcₙHom_eq_cfcₙHom_of_cfcHom, cfcₙHom_of_cfcHom]

Premises used: cfcₙHom_eq_cfcₙHom_of_cfcHom, cfcₙHom_of_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
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)

Tactic:
isometry_cfcHom a |>.comp ?_

Premises used: Isometry.comp, isometry_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
a : A
ha : p a
this : CompactSpace.{u_1} (↑(σₙ 𝕜 a) : Type u_1)
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) ⋯, continuous_toFun := ⋯ }) :
                  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), 𝕜))
⊢ 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)

Tactic:
refine isometry_cfcHom a |>.comp ?_

Premises used: Isometry.comp, isometry_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
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), 𝕜))

Tactic:
AddMonoidHomClass.isometry_of_norm _ fun f ↦ ?_

Premises used: AddMonoidHomClass.isometry_of_norm, Set.Mem, setOf
-- 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
ha : p a
this : CompactSpace.{u_1} (↑(σₙ 𝕜 a) : Type u_1)
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) ⋯, 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‖
⊢ 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), 𝕜))

Tactic:
refine AddMonoidHomClass.isometry_of_norm _ fun f ↦ ?_

Premises used: AddMonoidHomClass.isometry_of_norm
-- 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
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 := ⋯ }
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), 𝕜))
⊢ 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‖

Tactic:
change ‖(f : C(σₙ 𝕜 a, 𝕜)).comp ι‖ = ‖(f : C(σₙ 𝕜 a, 𝕜))‖

Premises used: ContinuousMap.comp, toContinuousMap
-- 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
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 := ⋯ }
⊢ 0 ≤ norm (E := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜))

Tactic:
positivity
-- 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
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 := ⋯ }
⊢ 0 ≤ norm (E := C((↑(σ 𝕜 a) : Type u_1), 𝕜)) (ContinuousMap.comp (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) ι)

Tactic:
positivity
-- 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
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), 𝕜))
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), 𝕜)) ι)
⊢ 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:
apply le_antisymm (ContinuousMap.norm_le _ (by positivity) |>.mpr ?_)
      (ContinuousMap.norm_le _ (by positivity) |>.mpr ?_)

Premises used: Iff.mpr, ContinuousMap.norm_le, 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
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 := 𝕜)
      ((ContinuousMap.comp (↑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), 𝕜)) (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜))

Tactic:
(f : C(σₙ 𝕜 a, 𝕜)).norm_coe_le_norm ⟨x, spectrum_subset_quasispectrum 𝕜 a hx⟩

Premises used: spectrum_subset_quasispectrum, ContinuousMap.norm_coe_le_norm, Set.Mem, toContinuousMap, Subtype.mk
-- 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
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 := 𝕜)
      ((ContinuousMap.comp (↑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), 𝕜)) (↑f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜))

Tactic:
exact (f : C(σₙ 𝕜 a, 𝕜)).norm_coe_le_norm ⟨x, spectrum_subset_quasispectrum 𝕜 a hx⟩

Premises used: spectrum_subset_quasispectrum, ContinuousMap.norm_coe_le_norm, toContinuousMap, Subtype.mk
-- 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
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
⊢ x = 0 ∨ x ∈ σ 𝕜 a

Tactic:
simpa [quasispectrum_eq_spectrum_union_zero] using hx

Premises used: quasispectrum_eq_spectrum_union_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
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), 𝕜)) ι)
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), 𝕜)) ι)
⊢ 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

Premises used: spectrum, rfl