awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
refine : ∀ (x : ℂ) (hx : x ∈ spectrum ℂ 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 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : StarModule ℂ A
inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
hp : IsStarNormal a
x : ℂ
hx : x ∈ spectrum ℂ 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 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : StarModule ℂ A
inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
hp : IsStarNormal a
x : ℂ
hx : x ∈ spectrum ℂ 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 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : StarModule ℂ A
inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
hp : 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_const_mul, 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
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 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : StarModule ℂ A
inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
hp : 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 : 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 (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: cfc_id', realPart_add_I_smul_imaginaryPart, mul_comm, Complex.re_add_im, Complex.I
-- 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
ha : IsStarNormal a
rw : spectrum ℂ (cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ)) a) = (fun (x : ℂ) ↦ (↑x.re : ℂ)) '' spectrum ℂ a
rw₁ rw₂ : Eq (α := Set ℂ) ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' spectrum ℂ a) ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' spectrum ℂ a)
⊢ spectrum.{0, u_1} ℂ (A := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) =
    (fun (x : ℂ) ↦ (↑x.re : ℂ)) '' spectrum ℂ a

Tactic:
rw [← cfc_re_id a, cfc_map_spectrum ..]

Premises used: cfc_map_spectrum, cfc_re_id
-- 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
ha : IsStarNormal a
⊢ spectrum.{0, u_1} ℝ (A := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) =
    re '' spectrum ℂ a

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

Premises used: Set.image_image, IsSelfAdjoint.spectrumRestricts, SpectrumRestricts.image, spectrum_realPart, realPart, DFunLike.coe, Subtype.property
-- 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
ha : IsStarNormal a
rw : spectrum ℂ (cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.im : ℂ)) a) = (fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a
rw₁ rw₂ : Eq (α := Set ℂ) ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a) ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a)
⊢ spectrum.{0, u_1} ℂ (A := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) =
    (fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a

Tactic:
rw [← cfc_im_id a, cfc_map_spectrum ..]

Premises used: cfc_im_id, cfc_map_spectrum
-- 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
ha : IsStarNormal a
⊢ spectrum.{0, u_1} ℝ (A := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) =
    im '' spectrum ℂ a

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

Premises used: Set.image_image, imaginaryPart, IsSelfAdjoint.spectrumRestricts, spectrum_imaginaryPart, SpectrumRestricts.image, DFunLike.coe, Subtype.property
-- 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
inst_6 : ContinuousMap.UniqueHom ℂ A
f : ℂ → ℂ
a : A
hf :
  ContinuousOn f (spectrum.{0, u_1} ℂ (A := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))
ha : IsStarNormal a
⊢ ContinuousOn f ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' spectrum ℂ a)

Tactic:
rw [spectrum_realPart a] at hf

Premises used: spectrum_realPart
-- 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
inst_6 : ContinuousMap.UniqueHom ℂ A
f : ℂ → ℂ
a : A
hf :
  ContinuousOn f (spectrum.{0, u_1} ℂ (A := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))
ha : IsStarNormal a
hf₁ : ContinuousOn f ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' spectrum ℂ a)
⊢ IsStarNormal a

Tactic:
rw [spectrum_realPart a] at hf

Premises used: spectrum_realPart
-- 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
inst_6 : ContinuousMap.UniqueHom ℂ A
f : ℂ → ℂ
a : A
hf : ContinuousOn f ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' spectrum ℂ a)
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_comp', cfc_re_id
-- 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
inst_6 : ContinuousMap.UniqueHom ℂ A
f : ℂ → ℂ
a : A
hf :
  ContinuousOn f (spectrum.{0, u_1} ℂ (A := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))
ha : IsStarNormal a
⊢ ContinuousOn f ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a)

Tactic:
rw [spectrum_imaginaryPart a] at hf

Premises used: spectrum_imaginaryPart
-- 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
inst_6 : ContinuousMap.UniqueHom ℂ A
f : ℂ → ℂ
a : A
hf :
  ContinuousOn f (spectrum.{0, u_1} ℂ (A := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))
ha : IsStarNormal a
hf₁ : ContinuousOn f ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a)
⊢ IsStarNormal a

Tactic:
rw [spectrum_imaginaryPart a] at hf

Premises used: spectrum_imaginaryPart
-- 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
inst_6 : ContinuousMap.UniqueHom ℂ A
f : ℂ → ℂ
a : A
hf : ContinuousOn f ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a)
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 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : StarModule ℂ A
inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst_6 : ContinuousMap.UniqueHom ℂ A
inst_7 : T2Space A
f : ℝ → ℝ
a : A
hf :
  ContinuousOn f (spectrum.{0, u_1} ℝ (A := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))
ha : IsStarNormal a
⊢ ContinuousOn f (re '' spectrum ℂ a)

Tactic:
rw [spectrum_realPart' a] at hf

Premises used: spectrum_realPart'
-- 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
inst_6 : ContinuousMap.UniqueHom ℂ A
inst_7 : T2Space A
f : ℝ → ℝ
a : A
hf :
  ContinuousOn f (spectrum.{0, u_1} ℝ (A := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))
ha : IsStarNormal a
hf₁ : ContinuousOn f (re '' spectrum ℂ a)
⊢ IsStarNormal a

Tactic:
rw [spectrum_realPart' a] at hf

Premises used: spectrum_realPart'
-- 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
inst_6 : ContinuousMap.UniqueHom ℂ A
inst_7 : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (re '' spectrum ℂ a)
ha : IsStarNormal a
⊢ ContinuousOn re ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' spectrum ℂ a)

Tactic:
fun_prop
-- 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
inst_6 : ContinuousMap.UniqueHom ℂ A
inst_7 : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (re '' spectrum ℂ a)
ha : IsStarNormal a
refine : Set.MapsTo re ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' spectrum ℂ a) (re '' spectrum ℂ a)
⊢ ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' spectrum ℂ 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 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : StarModule ℂ A
inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst_6 : ContinuousMap.UniqueHom ℂ A
inst_7 : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (re '' spectrum ℂ a)
ha : IsStarNormal a
⊢ Set.MapsTo re ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' spectrum ℂ a) (re '' spectrum ℂ 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 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : StarModule ℂ A
inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst_6 : ContinuousMap.UniqueHom ℂ A
inst_7 : T2Space A
f : ℝ → ℝ
a : A
hf :
  ContinuousOn f (spectrum.{0, u_1} ℝ (A := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))
ha : IsStarNormal a
⊢ ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' spectrum ℂ a)

Tactic:
have : ContinuousOn (fun x ↦ (f x.re) : ℂ → ℂ) ((re · : ℂ → ℂ) '' spectrum ℂ a) := by
    rw [spectrum_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 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : StarModule ℂ A
inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst_6 : ContinuousMap.UniqueHom ℂ A
inst_7 : T2Space A
f : ℝ → ℝ
a : A
hf :
  ContinuousOn f (spectrum.{0, u_1} ℝ (A := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))
ha : IsStarNormal a
this : ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' spectrum ℂ 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_comp', cfc_re_id, cfc_real_eq_complex
-- 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
inst_6 : ContinuousMap.UniqueHom ℂ A
inst_7 : T2Space A
f : ℝ → ℝ
a : A
hf :
  ContinuousOn f (spectrum.{0, u_1} ℝ (A := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))
ha : IsStarNormal a
this : ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' spectrum ℂ 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 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : StarModule ℂ A
inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst_6 : ContinuousMap.UniqueHom ℂ A
inst_7 : T2Space A
f : ℝ → ℝ
a : A
hf :
  ContinuousOn f (spectrum.{0, u_1} ℝ (A := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))
ha : IsStarNormal a
this : ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' spectrum ℂ 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_comp', cfc_re_id, cfc_real_eq_complex
-- 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
inst_6 : ContinuousMap.UniqueHom ℂ A
inst_7 : T2Space A
f : ℝ → ℝ
a : A
hf :
  ContinuousOn f (spectrum.{0, u_1} ℝ (A := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))
ha : IsStarNormal a
this : ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' spectrum ℂ 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_comp', cfc_re_id, cfc_real_eq_complex
-- 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
inst_6 : ContinuousMap.UniqueHom ℂ A
inst_7 : T2Space A
f : ℝ → ℝ
a : A
hf :
  ContinuousOn f (spectrum.{0, u_1} ℝ (A := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))
ha : IsStarNormal a
⊢ ContinuousOn f (im '' spectrum ℂ a)

Tactic:
rw [spectrum_imaginaryPart' a] at hf

Premises used: spectrum_imaginaryPart'
-- 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
inst_6 : ContinuousMap.UniqueHom ℂ A
inst_7 : T2Space A
f : ℝ → ℝ
a : A
hf :
  ContinuousOn f (spectrum.{0, u_1} ℝ (A := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))
ha : IsStarNormal a
hf₁ : ContinuousOn f (im '' spectrum ℂ a)
⊢ IsStarNormal a

Tactic:
rw [spectrum_imaginaryPart' a] at hf

Premises used: spectrum_imaginaryPart'
-- 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
inst_6 : ContinuousMap.UniqueHom ℂ A
inst_7 : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (im '' spectrum ℂ a)
ha : IsStarNormal a
⊢ ContinuousOn re ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a)

Tactic:
fun_prop
-- 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
inst_6 : ContinuousMap.UniqueHom ℂ A
inst_7 : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (im '' spectrum ℂ a)
ha : IsStarNormal a
refine : Set.MapsTo re ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a) (im '' spectrum ℂ a)
⊢ ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ 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 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : StarModule ℂ A
inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst_6 : ContinuousMap.UniqueHom ℂ A
inst_7 : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (im '' spectrum ℂ a)
ha : IsStarNormal a
⊢ Set.MapsTo re ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a) (im '' spectrum ℂ 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 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : StarModule ℂ A
inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst_6 : ContinuousMap.UniqueHom ℂ A
inst_7 : T2Space A
f : ℝ → ℝ
a : A
hf :
  ContinuousOn f (spectrum.{0, u_1} ℝ (A := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))
ha : IsStarNormal a
⊢ ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a)

Tactic:
have : ContinuousOn (fun x ↦ (f x.re) : ℂ → ℂ) ((im · : ℂ → ℂ) '' spectrum ℂ a) := by
    rw [spectrum_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 ..