awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.im : ℂ)) '' quasispectrum ℂ a)

Tactic:
rw [quasispectrum_imaginaryPart a] at hf

Premises used: quasispectrum_imaginaryPart
-- 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.im : ℂ)) '' quasispectrum ℂ a)
⊢ f 0 = 0

Tactic:
rw [quasispectrum_imaginaryPart a] at hf

Premises used: quasispectrum_imaginaryPart
-- 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.im : ℂ)) '' quasispectrum ℂ a)
hf0₁ : f 0 = 0
⊢ IsStarNormal a

Tactic:
rw [quasispectrum_imaginaryPart a] at hf

Premises used: quasispectrum_imaginaryPart
-- 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.im : ℂ)) '' quasispectrum ℂ a)
hf0 : f 0 = 0
ha : IsStarNormal a
rw :
  cfcₙ (p := IsStarNormal) f (cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.im : ℂ)) a) =
    cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ f (↑x.im : ℂ)) a
rw₁ rw₂ :
  cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ f (↑x.im : ℂ)) a = cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ f (↑x.im : ℂ)) a
⊢ cfcₙ (p := IsStarNormal) f (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) =
    cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ f (↑x.im : ℂ)) a

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

Premises used: cfcₙ_im_id, cfcₙ_comp'
-- 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
inst_9 : T2Space 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 (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
inst_9 : T2Space 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 (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
inst_9 : T2Space 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 (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
inst_9 : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (re '' quasispectrum ℂ a)
hf0 : f 0 = 0
ha : IsStarNormal a
⊢ ContinuousOn re ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' quasispectrum ℂ a)

Tactic:
fun_prop
-- 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
inst_9 : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (re '' quasispectrum ℂ a)
hf0 : f 0 = 0
ha : IsStarNormal a
refine : Set.MapsTo re ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' quasispectrum ℂ a) (re '' quasispectrum ℂ a)
⊢ ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' quasispectrum ℂ a)

Tactic:
refine continuous_ofReal.comp_continuousOn <| hf.comp (by fun_prop) ?_

Premises used: Continuous.comp_continuousOn, ContinuousOn.comp, Complex.continuous_ofReal
-- 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
inst_9 : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (re '' quasispectrum ℂ a)
hf0 : f 0 = 0
ha : IsStarNormal a
⊢ Set.MapsTo re ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' quasispectrum ℂ a) (re '' quasispectrum ℂ a)

Tactic:
simpa [Set.mapsTo_image_iff, Function.comp_def] using Set.mapsTo_image ..

Premises used: Set.mapsTo_image, Function.comp_def, Set.mapsTo_image_iff
-- 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
inst_9 : T2Space 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 (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' quasispectrum ℂ a)

Tactic:
have : ContinuousOn (fun x ↦ (f x.re) : ℂ → ℂ) ((re · : ℂ → ℂ) '' quasispectrum ℂ a) := by
    rw [quasispectrum_realPart' a] at hf
    refine continuous_ofReal.comp_continuousOn <| hf.comp (by fun_prop) ?_
    simpa [Set.mapsTo_image_iff, Function.comp_def] using Set.mapsTo_image ..
-- 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
inst_9 : T2Space 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
this : ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' quasispectrum ℂ a)
rw : cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f (↑x.re : ℂ).re) : ℂ)) a
| cfcₙ (p := IsSelfAdjoint) f (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)

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

Premises used: cfcₙ_re_id, cfcₙ_real_eq_complex, cfcₙ_comp'
-- 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
inst_9 : T2Space 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
this : ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' quasispectrum ℂ a)
simp : cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) a
| cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f (↑x.re : ℂ).re) : ℂ)) a

Tactic:
simp
-- 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
inst_9 : T2Space 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
this : ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' quasispectrum ℂ a)
rw : cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) a
| cfcₙ (p := IsSelfAdjoint) f (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)

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

Premises used: cfcₙ_re_id, cfcₙ_real_eq_complex, cfcₙ_comp'
-- 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
inst_9 : T2Space 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
this : ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' quasispectrum ℂ a)
conv_rhs :
  cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) a =
    cfcₙ (p := IsSelfAdjoint) f (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
conv_rhs₁ :
  cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) a =
    cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) a
⊢ cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) a =
    cfcₙ (p := IsSelfAdjoint) f (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)

Tactic:
conv_rhs =>
    rw [cfcₙ_real_eq_complex, ← cfcₙ_re_id a, ← cfcₙ_comp' ..]
    simp

Premises used: cfcₙ_re_id, cfcₙ_real_eq_complex, cfcₙ_comp'
-- 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
inst_9 : T2Space 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 (im '' quasispectrum ℂ a)

Tactic:
rw [quasispectrum_imaginaryPart' a] at hf

Premises used: quasispectrum_imaginaryPart'
-- 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
inst_9 : T2Space 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 (im '' quasispectrum ℂ a)
⊢ f 0 = 0

Tactic:
rw [quasispectrum_imaginaryPart' a] at hf

Premises used: quasispectrum_imaginaryPart'
-- 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
inst_9 : T2Space 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 (im '' quasispectrum ℂ a)
hf0₁ : f 0 = 0
⊢ IsStarNormal a

Tactic:
rw [quasispectrum_imaginaryPart' a] at hf

Premises used: quasispectrum_imaginaryPart'
-- 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
inst_9 : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (im '' quasispectrum ℂ a)
hf0 : f 0 = 0
ha : IsStarNormal a
⊢ ContinuousOn re ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' quasispectrum ℂ a)

Tactic:
fun_prop
-- 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
inst_9 : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (im '' quasispectrum ℂ a)
hf0 : f 0 = 0
ha : IsStarNormal a
refine : Set.MapsTo re ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' quasispectrum ℂ a) (im '' quasispectrum ℂ a)
⊢ ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' quasispectrum ℂ a)

Tactic:
refine continuous_ofReal.comp_continuousOn <| hf.comp (by fun_prop) ?_

Premises used: Continuous.comp_continuousOn, ContinuousOn.comp, Complex.continuous_ofReal
-- 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
inst_9 : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (im '' quasispectrum ℂ a)
hf0 : f 0 = 0
ha : IsStarNormal a
⊢ Set.MapsTo re ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' quasispectrum ℂ a) (im '' quasispectrum ℂ a)

Tactic:
simpa [Set.mapsTo_image_iff, Function.comp_def] using Set.mapsTo_image ..

Premises used: Set.mapsTo_image, Function.comp_def, Set.mapsTo_image_iff
-- 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
inst_9 : T2Space 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 (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' quasispectrum ℂ a)

Tactic:
have : ContinuousOn (fun x ↦ (f x.re) : ℂ → ℂ) ((im · : ℂ → ℂ) '' quasispectrum ℂ a) := by
    rw [quasispectrum_imaginaryPart' a] at hf
    refine continuous_ofReal.comp_continuousOn <| hf.comp (by fun_prop) ?_
    simpa [Set.mapsTo_image_iff, Function.comp_def] using Set.mapsTo_image ..
-- 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
inst_9 : T2Space 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
this : ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' quasispectrum ℂ a)
rw : cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f (↑x.im : ℂ).re) : ℂ)) a
| cfcₙ (p := IsSelfAdjoint) f (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)

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

Premises used: cfcₙ_real_eq_complex, cfcₙ_im_id, cfcₙ_comp'
-- 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
inst_9 : T2Space 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
this : ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' quasispectrum ℂ a)
simp : cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a
| cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f (↑x.im : ℂ).re) : ℂ)) a

Tactic:
simp
-- 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
inst_9 : T2Space 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
this : ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' quasispectrum ℂ a)
rw : cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a
| cfcₙ (p := IsSelfAdjoint) f (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)

Tactic:
rw [cfcₙ_real_eq_complex, ← cfcₙ_im_id a, ← cfcₙ_comp' ..]
    simp

Premises used: cfcₙ_real_eq_complex, cfcₙ_im_id, cfcₙ_comp'
-- 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
inst_9 : T2Space 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
this : ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' quasispectrum ℂ a)
conv_rhs :
  cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a =
    cfcₙ (p := IsSelfAdjoint) f (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
conv_rhs₁ :
  cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a =
    cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a
⊢ cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a =
    cfcₙ (p := IsSelfAdjoint) f (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)

Tactic:
conv_rhs =>
    rw [cfcₙ_real_eq_complex, ← cfcₙ_im_id a, ← cfcₙ_comp' ..]
    simp

Premises used: cfcₙ_real_eq_complex, cfcₙ_im_id, cfcₙ_comp'
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : StarModule ℂ A
inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
hp : 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_id', cfc_smul, realPart_apply_coe, Complex, cfc_star, cfc_add
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : StarModule ℂ A
inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
hp : 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_id', cfc_smul, realPart_apply_coe, Complex, cfc_star, cfc_add
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : StarModule ℂ A
inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
hp : 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