awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
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)
| cfcₙ (p := IsSelfAdjoint) f (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
have rw : cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a
Tactic: rw [cfcₙ_real_eq_complex, ← cfcₙ_im_id a, ← cfcₙ_comp' ..]
    simp
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
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)
⊢ cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a =
    cfcₙ (p := IsSelfAdjoint) f (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
have conv_rhs : 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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
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)
⊢ cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a =
    cfcₙ (p := IsSelfAdjoint) f (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
have conv_rhs₁ : cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a = cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a
Tactic: conv_rhs =>
    rw [cfcₙ_real_eq_complex, ← cfcₙ_im_id a, ← cfcₙ_comp' ..]
    simp
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
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
| (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
have rw : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ HSMul.hSMul (α := ℝ) 2⁻¹ (x + star x)) a
Tactic: rw [realPart_apply_coe, ← cfc_id' ℂ a, ← cfc_star, ← cfc_add .., ← cfc_smul ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
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 =
    (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
have conv_rhs : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ)) a =
  cfc (p := IsStarNormal) (fun (x : ℂ) ↦ HSMul.hSMul (α := ℝ) 2⁻¹ (x + star x)) a
Tactic: conv_rhs => rw [realPart_apply_coe, ← cfc_id' ℂ a, ← cfc_star, ← cfc_add .., ← cfc_smul ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
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
have refine : ∀ (x : ℂ) (hx : x ∈ spectrum ℂ a), (↑x.re : ℂ) = HSMul.hSMul (α := ℝ) 2⁻¹ (x + star x)
Tactic: refine cfc_congr fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
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
⊢ (↑x.re : ℂ) = HSMul.hSMul (α := ℝ) 2⁻¹ (x + star x)
have rw : HAdd.hAdd (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) / 2 = HSMul.hSMul (α := ℝ) (β := ℂ) 2⁻¹ 1 • (x + star x)
Tactic: rw [Complex.re_eq_add_conj, ← smul_one_smul ℂ 2⁻¹]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (hypothesis)
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)
⊢ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.im : ℂ)) a =
    (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
have 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)
Tactic: rw [cfc_add .., cfc_const_mul .., cfc_re_id a] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
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.im : ℂ)) a =
    (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
have 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)
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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
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) =
    (fun (x : ℂ) ↦ (↑x.re : ℂ)) '' spectrum ℂ a
have rw : spectrum ℂ (cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ)) a) = (fun (x : ℂ) ↦ (↑x.re : ℂ)) '' spectrum ℂ a
Tactic: rw [← cfc_re_id a, cfc_map_spectrum ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
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
⊢ spectrum.{0, u_1} ℂ (A := A) (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) =
    (fun (x : ℂ) ↦ (↑x.re : ℂ)) '' spectrum ℂ a
have rw₁ : Eq (α := Set ℂ) ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' spectrum ℂ a) ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' spectrum ℂ a)
Tactic: rw [← cfc_re_id a, cfc_map_spectrum ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
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) =
    (fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a
have rw : spectrum ℂ (cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.im : ℂ)) a) = (fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a
Tactic: rw [← cfc_im_id a, cfc_map_spectrum ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
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
⊢ spectrum.{0, u_1} ℂ (A := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) =
    (fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a
have rw₁ : Eq (α := Set ℂ) ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a) ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a)
Tactic: rw [← cfc_im_id a, cfc_map_spectrum ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (hypothesis)
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
⊢ cfc (p := IsStarNormal) f (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ f (↑x.re : ℂ)) a
have hf₁ : ContinuousOn f ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' spectrum ℂ a)
Tactic: rw [spectrum_realPart a] at hf
Cleared hypotheses: hf, ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
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
⊢ cfc (p := IsStarNormal) f (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ f (↑x.re : ℂ)) a
have rw : cfc (p := IsStarNormal) f (cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ)) a) =
  cfc (p := IsStarNormal) (fun (x : ℂ) ↦ f (↑x.re : ℂ)) a
Tactic: rw [← cfc_re_id a, ← cfc_comp' ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
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
⊢ cfc (p := IsStarNormal) f (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ f (↑x.re : ℂ)) a
have rw₁ : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ f (↑x.re : ℂ)) a = cfc (p := IsStarNormal) (fun (x : ℂ) ↦ f (↑x.re : ℂ)) a
Tactic: rw [← cfc_re_id a, ← cfc_comp' ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (hypothesis)
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
⊢ cfc (p := IsStarNormal) f (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ f (↑x.im : ℂ)) a
have hf₁ : ContinuousOn f ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a)
Tactic: rw [spectrum_imaginaryPart a] at hf
Cleared hypotheses: hf, ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
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
⊢ cfc (p := IsStarNormal) f (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ f (↑x.im : ℂ)) a
have rw : cfc (p := IsStarNormal) f (cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.im : ℂ)) a) =
  cfc (p := IsStarNormal) (fun (x : ℂ) ↦ f (↑x.im : ℂ)) a
Tactic: rw [← cfc_im_id a, ← cfc_comp' ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
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
⊢ cfc (p := IsStarNormal) f (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) =
    cfc (p := IsStarNormal) (fun (x : ℂ) ↦ f (↑x.im : ℂ)) a
have rw₁ : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ f (↑x.im : ℂ)) a = cfc (p := IsStarNormal) (fun (x : ℂ) ↦ f (↑x.im : ℂ)) a
Tactic: rw [← cfc_im_id a, ← cfc_comp' ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (hypothesis)
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)
have hf₁ : ContinuousOn f (re '' spectrum ℂ a)
Tactic: rw [spectrum_realPart' a] at hf
Cleared hypotheses: hf, ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
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 (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' spectrum ℂ a)
have refine : Set.MapsTo re ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' spectrum ℂ a) (re '' spectrum ℂ a)
Tactic: refine continuous_ofReal.comp_continuousOn <| hf.comp (by fun_prop) ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (hypothesis)
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
⊢ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) a =
    cfc (p := IsSelfAdjoint) f (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
have this : 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 ..
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
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)
| cfc (p := IsSelfAdjoint) f (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
have rw : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f (↑x.re : ℂ).re) : ℂ)) a
Tactic: rw [cfc_real_eq_complex, ← cfc_re_id a, ← cfc_comp' ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
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)
| cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f (↑x.re : ℂ).re) : ℂ)) a
have simp : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) a
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
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)
| cfc (p := IsSelfAdjoint) f (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
have rw : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) a
Tactic: rw [cfc_real_eq_complex, ← cfc_re_id a, ← cfc_comp' ..]
    simp
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
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)
⊢ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) a =
    cfc (p := IsSelfAdjoint) f (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
have conv_rhs : 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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
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)
⊢ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) a =
    cfc (p := IsSelfAdjoint) f (↑(((ℜ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
have conv_rhs₁ : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) a = cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) a
Tactic: conv_rhs =>
    rw [cfc_real_eq_complex, ← cfc_re_id a, ← cfc_comp' ..]
    simp
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (hypothesis)
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)
have hf₁ : ContinuousOn f (im '' spectrum ℂ a)
Tactic: rw [spectrum_imaginaryPart' a] at hf
Cleared hypotheses: hf, ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
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 (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a)
have refine : Set.MapsTo re ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a) (im '' spectrum ℂ a)
Tactic: refine continuous_ofReal.comp_continuousOn <| hf.comp (by fun_prop) ?_