awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : StarModule ℝ A
inst_12 : ContinuousStar A
inst_13 : ContinuousConstSMul ℝ A
inst_14 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : 0 ≤ cfcₙ (p := IsSelfAdjoint) f a
h₁ : ContinuousOn f (quasispectrum ℝ a)
h₂ : f 0 = 0
h₃ : IsSelfAdjoint a
⊢ ∃ (x : ℝ → ℝ), (∀ x_1 ∈ quasispectrum ℝ a, 0 ≤ x x_1) ∧ cfcₙ (p := IsSelfAdjoint) x a = cfcₙ (p := IsSelfAdjoint) f a

Tactic:
⟨f, ?_, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : StarModule ℝ A
inst_12 : ContinuousStar A
inst_13 : ContinuousConstSMul ℝ A
inst_14 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : 0 ≤ cfcₙ (p := IsSelfAdjoint) f a
h₁ : ContinuousOn f (quasispectrum ℝ a)
h₂ : f 0 = 0
h₃ : IsSelfAdjoint a
inl : ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x
⊢ ∃ (x : ℝ → ℝ), (∀ x_1 ∈ quasispectrum ℝ a, 0 ≤ x x_1) ∧ cfcₙ (p := IsSelfAdjoint) x a = cfcₙ (p := IsSelfAdjoint) f a

Tactic:
refine ⟨f, ?_, rfl⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : StarModule ℝ A
inst_12 : ContinuousStar A
inst_13 : ContinuousConstSMul ℝ A
inst_14 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : 0 ≤ cfcₙ (p := IsSelfAdjoint) f a
h₁ : ContinuousOn f (quasispectrum ℝ a)
h₂ : f 0 = 0
h₃ : IsSelfAdjoint a
inl inl₁ inl₂ inl₃ :
  ∀ (hf : ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x) (h₁ : ContinuousOn f (quasispectrum ℝ a)) (h₂ : f 0 = 0)
    (h₃ : IsSelfAdjoint a), ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x
⊢ ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x

Tactic:
rwa [cfcₙ_nonneg_iff f a] at hf

Premises used: cfcₙ_nonneg_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : StarModule ℝ A
inst_12 : ContinuousStar A
inst_13 : ContinuousConstSMul ℝ A
inst_14 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : 0 ≤ cfcₙ (p := IsSelfAdjoint) f a
h : ¬ContinuousOn f (quasispectrum ℝ a)
⊢ ∀ x ∈ quasispectrum ℝ a, LE.le (α := ℝ) 0 (0 x)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : StarModule ℝ A
inst_12 : ContinuousStar A
inst_13 : ContinuousConstSMul ℝ A
inst_14 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : 0 ≤ cfcₙ (p := IsSelfAdjoint) f a
h : ¬ContinuousOn f (quasispectrum ℝ a)
⊢ cfcₙ (R := ℝ) (p := IsSelfAdjoint) 0 a = cfcₙ (p := IsSelfAdjoint) f a

Tactic:
simp [cfcₙ_apply_of_not_continuousOn a h]

Premises used: cfcₙ_apply_of_not_continuousOn
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : StarModule ℝ A
inst_12 : ContinuousStar A
inst_13 : ContinuousConstSMul ℝ A
inst_14 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : 0 ≤ cfcₙ (p := IsSelfAdjoint) f a
h : ¬ContinuousOn f (quasispectrum ℝ a)
⊢ ∃ (x : ℝ → ℝ), (∀ x_1 ∈ quasispectrum ℝ a, 0 ≤ x x_1) ∧ cfcₙ (p := IsSelfAdjoint) x a = cfcₙ (p := IsSelfAdjoint) f a

Tactic:
exact ⟨0, by simp, by simp [cfcₙ_apply_of_not_continuousOn a h]⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : StarModule ℝ A
inst_12 : ContinuousStar A
inst_13 : ContinuousConstSMul ℝ A
inst_14 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : 0 ≤ cfcₙ (p := IsSelfAdjoint) f a
h : ¬f 0 = 0
⊢ ∀ x ∈ quasispectrum ℝ a, LE.le (α := ℝ) 0 (0 x)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : StarModule ℝ A
inst_12 : ContinuousStar A
inst_13 : ContinuousConstSMul ℝ A
inst_14 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : 0 ≤ cfcₙ (p := IsSelfAdjoint) f a
h : ¬f 0 = 0
⊢ cfcₙ (R := ℝ) (p := IsSelfAdjoint) 0 a = cfcₙ (p := IsSelfAdjoint) f a

Tactic:
simp [cfcₙ_apply_of_not_map_zero a h]

Premises used: cfcₙ_apply_of_not_map_zero
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : StarModule ℝ A
inst_12 : ContinuousStar A
inst_13 : ContinuousConstSMul ℝ A
inst_14 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : 0 ≤ cfcₙ (p := IsSelfAdjoint) f a
h : ¬f 0 = 0
⊢ ∃ (x : ℝ → ℝ), (∀ x_1 ∈ quasispectrum ℝ a, 0 ≤ x x_1) ∧ cfcₙ (p := IsSelfAdjoint) x a = cfcₙ (p := IsSelfAdjoint) f a

Tactic:
exact ⟨0, by simp, by simp [cfcₙ_apply_of_not_map_zero a h]⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : StarModule ℝ A
inst_12 : ContinuousStar A
inst_13 : ContinuousConstSMul ℝ A
inst_14 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : 0 ≤ cfcₙ (p := IsSelfAdjoint) f a
h : ¬IsSelfAdjoint a
⊢ ∀ x ∈ quasispectrum ℝ a, LE.le (α := ℝ) 0 (0 x)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : StarModule ℝ A
inst_12 : ContinuousStar A
inst_13 : ContinuousConstSMul ℝ A
inst_14 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : 0 ≤ cfcₙ (p := IsSelfAdjoint) f a
h : ¬IsSelfAdjoint a
⊢ cfcₙ (R := ℝ) (p := IsSelfAdjoint) 0 a = cfcₙ (p := IsSelfAdjoint) f a

Tactic:
simp [cfcₙ_apply_of_not_predicate a h]

Premises used: cfcₙ_apply_of_not_predicate
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : StarModule ℝ A
inst_12 : ContinuousStar A
inst_13 : ContinuousConstSMul ℝ A
inst_14 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : 0 ≤ cfcₙ (p := IsSelfAdjoint) f a
h : ¬IsSelfAdjoint a
⊢ ∃ (x : ℝ → ℝ), (∀ x_1 ∈ quasispectrum ℝ a, 0 ≤ x x_1) ∧ cfcₙ (p := IsSelfAdjoint) x a = cfcₙ (p := IsSelfAdjoint) f a

Tactic:
exact ⟨0, by simp, by simp [cfcₙ_apply_of_not_predicate a h]⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
rw : cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ HSMul.hSMul (α := ℝ) 2⁻¹ (x + star x)) a
| (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)

Tactic:
rw [realPart_apply_coe, ← cfcₙ_id' ℂ a, ← cfcₙ_star, ← cfcₙ_add .., ← cfcₙ_smul ..]

Premises used: cfcₙ_add, cfcₙ_id', cfcₙ_star, realPart_apply_coe, Complex, cfcₙ_smul
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
conv_rhs :
  cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ)) a =
    cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ HSMul.hSMul (α := ℝ) 2⁻¹ (x + star x)) a
⊢ cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ)) a =
    (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)

Tactic:
conv_rhs => rw [realPart_apply_coe, ← cfcₙ_id' ℂ a, ← cfcₙ_star, ← cfcₙ_add .., ← cfcₙ_smul ..]

Premises used: cfcₙ_add, cfcₙ_id', cfcₙ_star, realPart_apply_coe, Complex, cfcₙ_smul
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
⊢ cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ)) a =
    cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ HSMul.hSMul (α := ℝ) 2⁻¹ (x + star x)) a

Tactic:
cfcₙ_congr fun x hx ↦ ?_

Premises used: cfcₙ_congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
refine : ∀ (x : ℂ) (hx : x ∈ quasispectrum ℂ a), (↑x.re : ℂ) = HSMul.hSMul (α := ℝ) 2⁻¹ (x + star x)
⊢ cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ)) a =
    cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ HSMul.hSMul (α := ℝ) 2⁻¹ (x + star x)) a

Tactic:
refine cfcₙ_congr fun x hx ↦ ?_

Premises used: cfcₙ_congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
x : ℂ
hx : x ∈ quasispectrum ℂ a
rw : HAdd.hAdd (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) / 2 = HSMul.hSMul (α := ℝ) (β := ℂ) 2⁻¹ 1 • (x + star x)
⊢ (↑x.re : ℂ) = HSMul.hSMul (α := ℝ) 2⁻¹ (x + star x)

Tactic:
rw [Complex.re_eq_add_conj, ← smul_one_smul ℂ 2⁻¹]

Premises used: Complex.re_eq_add_conj, Inv.inv, smul_one_smul, Complex, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
x : ℂ
hx : x ∈ quasispectrum ℂ a
⊢ HAdd.hAdd (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) / 2 = HSMul.hSMul (α := ℝ) (β := ℂ) 2⁻¹ 1 • (x + star x)

Tactic:
simp [div_eq_inv_mul]

Premises used: div_eq_inv_mul
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
this :
  cfcₙ (p := IsStarNormal) (fun (z : ℂ) ↦ (↑z.re : ℂ) + I * (↑z.im : ℂ)) a =
    (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) +
      HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
⊢ (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) +
      I • cfcₙ (p := IsStarNormal) (fun (z : ℂ) ↦ (↑z.im : ℂ)) a =
    (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) +
      HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)

Tactic:
rw [cfcₙ_add .., cfcₙ_const_mul .., cfcₙ_re_id a] at this

Premises used: cfcₙ_re_id, cfcₙ_add, cfcₙ_const_mul
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
this :
  (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) +
      I • cfcₙ (p := IsStarNormal) (fun (z : ℂ) ↦ (↑z.im : ℂ)) a =
    (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) +
      HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
⊢ cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.im : ℂ)) a =
    (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
suffices :
  cfcₙ (p := IsStarNormal) (fun (z : ℂ) ↦ (↑z.re : ℂ) + I * (↑z.im : ℂ)) a =
    (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) +
      HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
⊢ cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.im : ℂ)) a =
    (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)

Tactic:
suffices cfcₙ (fun z : ℂ ↦ re z + I * im z) a = ℜ a + I • ℑ a by
    rw [cfcₙ_add .., cfcₙ_const_mul .., cfcₙ_re_id a] at this
    simpa
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
⊢ cfcₙ (p := IsStarNormal) (fun (z : ℂ) ↦ (↑z.re : ℂ) + I * (↑z.im : ℂ)) a =
    (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) +
      HSMul.hSMul (β := A) I (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)

Tactic:
simp [mul_comm I, re_add_im, cfcₙ_id' .., realPart_add_I_smul_imaginaryPart]

Premises used: realPart_add_I_smul_imaginaryPart, cfcₙ_id', mul_comm, Complex.re_add_im, Complex.I
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
rw :
  quasispectrum ℂ (cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ)) a) =
    (fun (x : ℂ) ↦ (↑x.re : ℂ)) '' quasispectrum ℂ a
rw₁ rw₂ :
  Eq (α := Set ℂ) ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' quasispectrum ℂ a) ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' quasispectrum ℂ a)
⊢ quasispectrum.{0, u_1} ℂ (A := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) =
    (fun (x : ℂ) ↦ (↑x.re : ℂ)) '' quasispectrum ℂ a

Tactic:
rw [← cfcₙ_re_id a, cfcₙ_map_quasispectrum ..]

Premises used: cfcₙ_re_id, cfcₙ_map_quasispectrum
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
⊢ quasispectrum.{0, u_1} ℝ (A := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) =
    re '' quasispectrum ℂ a

Tactic:
simp [← (ℜ a).2.quasispectrumRestricts.image, quasispectrum_realPart a, Set.image_image]

Premises used: IsSelfAdjoint.quasispectrumRestricts, Set.image_image, quasispectrum_realPart, QuasispectrumRestricts.image, realPart, DFunLike.coe, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
rw :
  quasispectrum ℂ (cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.im : ℂ)) a) =
    (fun (x : ℂ) ↦ (↑x.im : ℂ)) '' quasispectrum ℂ a
rw₁ rw₂ :
  Eq (α := Set ℂ) ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' quasispectrum ℂ a) ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' quasispectrum ℂ a)
⊢ quasispectrum.{0, u_1} ℂ (A := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) =
    (fun (x : ℂ) ↦ (↑x.im : ℂ)) '' quasispectrum ℂ a

Tactic:
rw [← cfcₙ_im_id a, cfcₙ_map_quasispectrum ..]

Premises used: cfcₙ_im_id, cfcₙ_map_quasispectrum
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
⊢ quasispectrum.{0, u_1} ℝ (A := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) =
    im '' quasispectrum ℂ a

Tactic:
simp [← (ℑ a).2.quasispectrumRestricts.image, quasispectrum_imaginaryPart a, Set.image_image]

Premises used: quasispectrum_imaginaryPart, IsSelfAdjoint.quasispectrumRestricts, Set.image_image, imaginaryPart, QuasispectrumRestricts.image, DFunLike.coe, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
inst_8 : ContinuousMapZero.UniqueHom ℂ A
f : ℂ → ℂ
a : A
hf :
  ContinuousOn f
    (quasispectrum.{0, u_1} ℂ (A := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))
hf0 : f 0 = 0
ha : IsStarNormal a
⊢ ContinuousOn f ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' quasispectrum ℂ a)

Tactic:
rw [quasispectrum_realPart a] at hf

Premises used: quasispectrum_realPart
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
inst_8 : ContinuousMapZero.UniqueHom ℂ A
f : ℂ → ℂ
a : A
hf :
  ContinuousOn f
    (quasispectrum.{0, u_1} ℂ (A := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))
hf0 : f 0 = 0
ha : IsStarNormal a
hf₁ : ContinuousOn f ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' quasispectrum ℂ a)
⊢ f 0 = 0

Tactic:
rw [quasispectrum_realPart a] at hf

Premises used: quasispectrum_realPart
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
inst_8 : ContinuousMapZero.UniqueHom ℂ A
f : ℂ → ℂ
a : A
hf :
  ContinuousOn f
    (quasispectrum.{0, u_1} ℂ (A := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))
hf0 : f 0 = 0
ha : IsStarNormal a
hf₁ : ContinuousOn f ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' quasispectrum ℂ a)
hf0₁ : f 0 = 0
⊢ IsStarNormal a

Tactic:
rw [quasispectrum_realPart a] at hf

Premises used: quasispectrum_realPart
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
inst_8 : ContinuousMapZero.UniqueHom ℂ A
f : ℂ → ℂ
a : A
hf : ContinuousOn f ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' quasispectrum ℂ a)
hf0 : f 0 = 0
ha : IsStarNormal a
rw :
  cfcₙ (p := IsStarNormal) f (cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ)) a) =
    cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ f (↑x.re : ℂ)) a
rw₁ rw₂ :
  cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ f (↑x.re : ℂ)) a = cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ f (↑x.re : ℂ)) a
⊢ cfcₙ (p := IsStarNormal) f (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) =
    cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ f (↑x.re : ℂ)) a

Tactic:
rw [← cfcₙ_re_id a, ← cfcₙ_comp' ..]

Premises used: cfcₙ_re_id, cfcₙ_comp'