awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
x : A
h : Membership.mem (γ := Submodule ℂ A) ⊤ x
a :
  Membership.mem (γ := Set A) {a : A | 0 ≤ a} (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺
⊢ Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
    (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺

Tactic:
refine subset_span ?_

Premises used: Submodule.subset_span
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
x : A
h : Membership.mem (γ := Submodule ℂ A) ⊤ x
⊢ Membership.mem (γ := Set A) {a : A | 0 ≤ a} (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺

Tactic:
apply CFC.posPart_nonneg

Premises used: CFC.posPart_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
x : A
h : Membership.mem (γ := Submodule ℂ A) ⊤ x
⊢ Membership.mem (γ := Set A) {a : A | 0 ≤ a} (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺

Tactic:
first | apply CFC.negPart_nonneg | apply CFC.posPart_nonneg

Premises used: CFC.negPart_nonneg, CFC.posPart_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
x : A
h : Membership.mem (γ := Submodule ℂ A) ⊤ x
⊢ Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
    (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻

Tactic:
subset_span ?_

Premises used: Submodule.subset_span
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
x : A
h : Membership.mem (γ := Submodule ℂ A) ⊤ x
a :
  Membership.mem (γ := Set A) {a : A | 0 ≤ a} (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻
⊢ Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
    (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻

Tactic:
refine subset_span ?_

Premises used: Submodule.subset_span
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
x : A
h : Membership.mem (γ := Submodule ℂ A) ⊤ x
⊢ Membership.mem (γ := Set A) {a : A | 0 ≤ a} (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻

Tactic:
apply CFC.negPart_nonneg

Premises used: CFC.negPart_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
x : A
h : Membership.mem (γ := Submodule ℂ A) ⊤ x
⊢ Membership.mem (γ := Set A) {a : A | 0 ≤ a} (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻

Tactic:
first | apply CFC.negPart_nonneg | apply CFC.posPart_nonneg

Premises used: CFC.negPart_nonneg, CFC.posPart_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
x : A
h : Membership.mem (γ := Submodule ℂ A) ⊤ x
⊢ Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
    (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺

Tactic:
subset_span ?_

Premises used: Submodule.subset_span
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
x : A
h : Membership.mem (γ := Submodule ℂ A) ⊤ x
a :
  Membership.mem (γ := Set A) {a : A | 0 ≤ a} (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺
⊢ Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
    (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺

Tactic:
refine subset_span ?_

Premises used: Submodule.subset_span
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
x : A
h : Membership.mem (γ := Submodule ℂ A) ⊤ x
⊢ Membership.mem (γ := Set A) {a : A | 0 ≤ a} (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺

Tactic:
apply CFC.posPart_nonneg

Premises used: CFC.posPart_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
x : A
h : Membership.mem (γ := Submodule ℂ A) ⊤ x
⊢ Membership.mem (γ := Set A) {a : A | 0 ≤ a} (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁺

Tactic:
first | apply CFC.negPart_nonneg | apply CFC.posPart_nonneg

Premises used: CFC.negPart_nonneg, CFC.posPart_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
x : A
h : Membership.mem (γ := Submodule ℂ A) ⊤ x
⊢ Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
    (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻

Tactic:
subset_span ?_

Premises used: Submodule.subset_span
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
x : A
h : Membership.mem (γ := Submodule ℂ A) ⊤ x
a :
  Membership.mem (γ := Set A) {a : A | 0 ≤ a} (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻
⊢ Membership.mem (γ := Submodule ℂ A) (span ℂ {a : A | 0 ≤ a})
    (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻

Tactic:
refine subset_span ?_

Premises used: Submodule.subset_span
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
x : A
h : Membership.mem (γ := Submodule ℂ A) ⊤ x
⊢ Membership.mem (γ := Set A) {a : A | 0 ≤ a} (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻

Tactic:
apply CFC.negPart_nonneg

Premises used: CFC.negPart_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : SMulCommClass ℂ A A
inst_3 : IsScalarTower ℂ A A
inst_4 : StarRing A
inst_5 : TopologicalSpace A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_8 : PartialOrder A
inst_9 : StarOrderedRing A
x : A
h : Membership.mem (γ := Submodule ℂ A) ⊤ x
⊢ Membership.mem (γ := Set A) {a : A | 0 ≤ a} (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) x) : A)⁻

Tactic:
first | apply CFC.negPart_nonneg | apply CFC.posPart_nonneg

Premises used: CFC.negPart_nonneg, CFC.posPart_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
pos : ∀ (ha : IsSelfAdjoint a), ‖a⁺‖ ≤ ‖a‖
by_cases : ∀ (ha : ¬IsSelfAdjoint a), ‖a⁺‖ ≤ ‖a‖
⊢ ‖a⁺‖ ≤ ‖a‖

Tactic:
by_cases ha : IsSelfAdjoint a

Premises used: IsSelfAdjoint
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : ¬IsSelfAdjoint a
⊢ ‖a⁺‖ ≤ ‖a‖

Tactic:
simp [CFC.posPart_def, cfcₙ_apply_of_not_predicate a ha]

Premises used: cfcₙ_apply_of_not_predicate, CFC.posPart_def
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : ¬IsSelfAdjoint a
⊢ ‖a⁺‖ ≤ ‖a‖

Tactic:
case neg => simp [CFC.posPart_def, cfcₙ_apply_of_not_predicate a ha]

Premises used: cfcₙ_apply_of_not_predicate, CFC.posPart_def
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ ‖a⁺‖ ≤ ‖a‖

Tactic:
norm_cfcₙ_le fun x hx ↦ ?_

Premises used: norm_cfcₙ_le
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
pos : ∀ (x : ℝ) (hx : x ∈ quasispectrum ℝ a), ‖x⁺‖ ≤ ‖a‖
⊢ ‖a⁺‖ ≤ ‖a‖

Tactic:
refine norm_cfcₙ_le fun x hx ↦ ?_

Premises used: norm_cfcₙ_le
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
pos : ∀ (h : x ≤ 0), ‖x⁺‖ ≤ ‖a‖
pos₁ : ∀ (h : 0 < x), ‖x⁺‖ ≤ ‖a‖
⊢ ‖x⁺‖ ≤ ‖a‖

Tactic:
obtain (h | h) := le_or_gt x 0

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
h : x ≤ 0
⊢ ‖x⁺‖ ≤ ‖a‖

Tactic:
simp [posPart_def, max_eq_right h]

Premises used: posPart_def, max_eq_right
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
h : 0 < x
pos : ‖x‖ ≤ ‖a‖
⊢ ‖x⁺‖ ≤ ‖a‖

Tactic:
simp only [posPart_def, max_eq_left h.le]

Premises used: LT.lt.le, posPart_def, max_eq_left
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
h : 0 < x
⊢ ‖x‖ ≤ ‖a‖

Tactic:
NonUnitalIsometricContinuousFunctionalCalculus.norm_quasispectrum_le a hx ha

Premises used: NonUnitalIsometricContinuousFunctionalCalculus.norm_quasispectrum_le
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
h : 0 < x
⊢ ‖x‖ ≤ ‖a‖

Tactic:
exact NonUnitalIsometricContinuousFunctionalCalculus.norm_quasispectrum_le a hx ha

Premises used: NonUnitalIsometricContinuousFunctionalCalculus.norm_quasispectrum_le
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
⊢ ‖a⁻‖ ≤ ‖a‖

Tactic:
simpa [CFC.negPart_neg] using norm_posPart_le (-a)

Premises used: CStarAlgebra.norm_posPart_le, CFC.negPart_neg, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ ‖a‖ = max ‖a⁺‖ ‖a⁻‖

Tactic:
le_antisymm ?_ <| max_le (norm_posPart_le a) (norm_negPart_le a)

Premises used: CStarAlgebra.norm_posPart_le, le_antisymm, max_le, CStarAlgebra.norm_negPart_le
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
refine : ‖a‖ ≤ max ‖a⁺‖ ‖a⁻‖
⊢ ‖a‖ = max ‖a⁺‖ ‖a⁻‖

Tactic:
refine le_antisymm ?_ <| max_le (norm_posPart_le a) (norm_negPart_le a)

Premises used: CStarAlgebra.norm_posPart_le, le_antisymm, max_le, CStarAlgebra.norm_negPart_le
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
rw : ‖cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a‖
| ‖a‖

Tactic:
rw [← cfcₙ_id' ℝ a]

Premises used: Real, cfcₙ_id'
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
conv_lhs : ‖cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a‖ ≤ max ‖a⁺‖ ‖a⁻‖
⊢ ‖a‖ ≤ max ‖a⁺‖ ‖a⁻‖

Tactic:
conv_lhs => rw [← cfcₙ_id' ℝ a]

Premises used: Real, cfcₙ_id'
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
rw : ∀ x ∈ quasispectrum ℝ a, ‖x‖ ≤ max ‖a⁺‖ ‖a⁻‖
⊢ ‖cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a‖ ≤ max ‖a⁺‖ ‖a⁻‖

Tactic:
rw [norm_cfcₙ_le_iff ..]

Premises used: norm_cfcₙ_le_iff
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
inl : ∀ (hx' : 0 ≤ x), ‖x‖ ≤ max ‖a⁺‖ ‖a⁻‖
inr : ∀ (hx' : x ≤ 0), ‖x‖ ≤ max ‖a⁺‖ ‖a⁻‖
⊢ ‖x‖ ≤ max ‖a⁺‖ ‖a⁻‖

Tactic:
obtain (hx' | hx') := le_total 0 x

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
hx' : 0 ≤ x
inl : ‖x‖ ≤ ‖a⁺‖
⊢ ‖x‖ ≤ max ‖a⁺‖ ‖a⁻‖

Tactic:
apply le_max_of_le_left

Premises used: le_max_of_le_left
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
hx' : 0 ≤ x
⊢ ‖x‖ ≤ ‖a⁺‖

Tactic:
le_of_eq_of_le ?_ <| norm_apply_le_norm_cfcₙ _ a hx

Premises used: le_of_eq_of_le, norm_apply_le_norm_cfcₙ
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
hx' : 0 ≤ x
inl : ‖x‖ = ‖x⁺‖
⊢ ‖x‖ ≤ ‖a⁺‖

Tactic:
refine le_of_eq_of_le ?_ <| norm_apply_le_norm_cfcₙ _ a hx

Premises used: le_of_eq_of_le, norm_apply_le_norm_cfcₙ
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
hx' : 0 ≤ x
inl inl₁ : ‖x‖ = ‖x‖
⊢ ‖x‖ = ‖x⁺‖

Tactic:
rw [posPart_eq_self.mpr hx']

Premises used: Iff.mpr, posPart_eq_self
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
hx' : x ≤ 0
inr : ‖x‖ ≤ ‖a⁻‖
⊢ ‖x‖ ≤ max ‖a⁺‖ ‖a⁻‖

Tactic:
apply le_max_of_le_right

Premises used: le_max_of_le_right
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
hx' : x ≤ 0
⊢ ‖x‖ ≤ ‖a⁻‖

Tactic:
le_of_eq_of_le ?_ <| norm_apply_le_norm_cfcₙ _ a hx

Premises used: le_of_eq_of_le, norm_apply_le_norm_cfcₙ
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
hx' : x ≤ 0
inr : ‖x‖ = ‖x⁻‖
⊢ ‖x‖ ≤ ‖a⁻‖

Tactic:
refine le_of_eq_of_le ?_ <| norm_apply_le_norm_cfcₙ _ a hx

Premises used: le_of_eq_of_le, norm_apply_le_norm_cfcₙ
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
hx' : x ≤ 0
inr : ‖x‖ = ‖-x‖
inr₁ inr₂ : ‖x‖ = ‖x‖
⊢ ‖x‖ = ‖x⁻‖

Tactic:
rw [negPart_eq_neg.mpr hx', norm_neg]

Premises used: Iff.mpr, norm_neg, negPart_eq_neg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
a b : ℝ≥0
⊢ a.nnrpow b = a ^ (↑b : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
y : ℝ≥0
⊢ Continuous (Y := ℝ≥0) fun (x : ℝ≥0) ↦ x.nnrpow y

Tactic:
continuous_rpow_const zero_le_coe

Premises used: NNReal.continuous_rpow_const, NNReal.zero_le_coe
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
y : ℝ≥0
⊢ Monotone (β := ℝ≥0) fun (x : ℝ≥0) ↦ x.nnrpow y

Tactic:
monotone_rpow_of_nonneg zero_le_coe

Premises used: NNReal.monotone_rpow_of_nonneg, NNReal.zero_le_coe
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a : A
y : ℝ≥0
⊢ nnrpow a y = a ^ y

Tactic:
rfl

Premises used: rfl