awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (hypothesis)
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)
⊢ 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 : 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.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 : 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) =
    (fun (x : ℂ) ↦ (↑x.re : ℂ)) '' quasispectrum ℂ a
have rw : quasispectrum ℂ (cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ)) a) =
  (fun (x : ℂ) ↦ (↑x.re : ℂ)) '' quasispectrum ℂ a
Tactic: rw [← cfcₙ_re_id a, cfcₙ_map_quasispectrum ..]
-- 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
a : A
ha : IsStarNormal a
rw :
  quasispectrum ℂ (cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ)) 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
have rw₁ : Eq (α := Set ℂ) ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' quasispectrum ℂ a) ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' quasispectrum ℂ a)
Tactic: rw [← cfcₙ_re_id a, cfcₙ_map_quasispectrum ..]
-- 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
a : A
ha : IsStarNormal a
⊢ quasispectrum.{0, u_1} ℂ (A := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A) =
    (fun (x : ℂ) ↦ (↑x.im : ℂ)) '' quasispectrum ℂ a
have rw : quasispectrum ℂ (cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.im : ℂ)) a) =
  (fun (x : ℂ) ↦ (↑x.im : ℂ)) '' quasispectrum ℂ a
Tactic: rw [← cfcₙ_im_id a, cfcₙ_map_quasispectrum ..]
-- 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
a : A
ha : IsStarNormal a
rw :
  quasispectrum ℂ (cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.im : ℂ)) 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
have rw₁ : Eq (α := Set ℂ) ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' quasispectrum ℂ a) ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' quasispectrum ℂ a)
Tactic: rw [← cfcₙ_im_id a, cfcₙ_map_quasispectrum ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (hypothesis)
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
⊢ 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 : ℂ)) '' quasispectrum ℂ a)
Tactic: rw [quasispectrum_realPart a] at hf
Cleared hypotheses: hf, hf0, ha
-- 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
f : ℂ → ℂ
a : A
hf : ContinuousOn f ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' quasispectrum ℂ a)
hf0 : f 0 = 0
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 : 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
⊢ 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 : 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
⊢ 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 : ℂ)) '' quasispectrum ℂ a)
Tactic: rw [quasispectrum_imaginaryPart a] at hf
Cleared hypotheses: hf, hf0, ha
-- 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
f : ℂ → ℂ
a : A
hf : ContinuousOn f ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' quasispectrum ℂ a)
hf0 : f 0 = 0
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 : 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
⊢ 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 : 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)
have hf₁ : ContinuousOn f (re '' quasispectrum ℂ a)
Tactic: rw [quasispectrum_realPart' a] at hf
Cleared hypotheses: hf, hf0, ha
-- 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 (re '' quasispectrum ℂ a)
hf0 : f 0 = 0
ha : IsStarNormal a
⊢ ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' quasispectrum ℂ a)
have refine : Set.MapsTo re ((fun (x : ℂ) ↦ (↑x.re : ℂ)) '' quasispectrum ℂ a) (re '' quasispectrum ℂ 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 : 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
⊢ 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 : ℂ)) '' 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 ..
-- 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.re : ℂ)) '' quasispectrum ℂ 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 : 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)
| 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 : 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)
| 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 : 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)
⊢ 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 : 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)
⊢ 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 : 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)
have hf₁ : ContinuousOn f (im '' quasispectrum ℂ a)
Tactic: rw [quasispectrum_imaginaryPart' a] at hf
Cleared hypotheses: hf, hf0, ha
-- 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 (im '' quasispectrum ℂ a)
hf0 : f 0 = 0
ha : IsStarNormal a
⊢ ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' quasispectrum ℂ a)
have refine : Set.MapsTo re ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' quasispectrum ℂ a) (im '' quasispectrum ℂ 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 : 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
⊢ cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) 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.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 ..
-- 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 : ℂ).re) : ℂ)) a
Tactic: rw [cfcₙ_real_eq_complex, ← 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 : 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 : ℂ).re) : ℂ)) a
have simp : cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a
Tactic: simp