awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : TopologicalSpace A
inst_7 : ContinuousConstSMul 𝕜 A
inst_8 : StarModule 𝕜 A
inst_9 : IsTopologicalRing A
inst_10 : ContinuousStar A
inst_11 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
rw :
  (↑(NonUnitalStarAlgHom.range (F := ContinuousMapZero (↑(quasispectrum 𝕜 a) : Type u_1) 𝕜 →⋆ₙₐ[𝕜] A)
          (cfcₙHom (p := p) ha)) :
      Set A) =
    (↑(elemental 𝕜 a : NonUnitalStarSubalgebra 𝕜 A) : Set A)
⊢ (Set.range fun (x : 𝕜 → 𝕜) ↦ cfcₙ (p := p) x a) = (↑(elemental 𝕜 a : NonUnitalStarSubalgebra 𝕜 A) : Set A)
have rw₁ : (↑(elemental 𝕜 a : NonUnitalStarSubalgebra 𝕜 A) : Set A) = (↑(elemental 𝕜 a : NonUnitalStarSubalgebra 𝕜 A) : Set A)
Tactic: rw [range_cfcₙ_eq_range_cfcₙHom 𝕜 ha, range_cfcₙHom 𝕜 ha]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : TopologicalSpace A
inst_7 : ContinuousConstSMul 𝕜 A
inst_8 : StarModule 𝕜 A
inst_9 : IsTopologicalRing A
inst_10 : ContinuousStar A
inst_11 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
⊢ LE.le (α := NonUnitalStarSubalgebra 𝕜 A)
    (NonUnitalStarAlgHom.range (F := ContinuousMapZero (↑(quasispectrum 𝕜 a) : Type u_1) 𝕜 →⋆ₙₐ[𝕜] A)
        (cfcₙHom (p := p) ha) :
      NonUnitalStarSubalgebra 𝕜 A)
    (elemental 𝕜 a : NonUnitalStarSubalgebra 𝕜 A)
have grw : LE.le (α := NonUnitalStarSubalgebra 𝕜 A)
  (NonUnitalStarSubalgebra.topologicalClosure.{u_1, u_2} (A := A)
      (adjoin.{u_1, u_2} 𝕜 (A := A)
        (Set.image (α := ContinuousMapZero (↑(quasispectrum 𝕜 a) : Type u_1) 𝕜)
          (⇑(cfcₙHom (p := p) ha) : (a : ContinuousMapZero (↑(quasispectrum 𝕜 a) : Type u_1) 𝕜) → A)
          {ContinuousMapZero.id (quasispectrum 𝕜 a)})) :
    NonUnitalStarSubalgebra 𝕜 A)
  (elemental 𝕜 a : NonUnitalStarSubalgebra 𝕜 A)
Tactic: grw [← NonUnitalStarAlgebra.map_top, ← ContinuousMapZero.elemental_eq_top,
    NonUnitalStarAlgebra.elemental,
    NonUnitalStarSubalgebra.map_topologicalClosure_le (R := 𝕜) _ (cfcₙHom_continuous ha),
    NonUnitalStarAlgHom.map_adjoin]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : TopologicalSpace A
inst_7 : ContinuousConstSMul 𝕜 A
inst_8 : StarModule 𝕜 A
inst_9 : IsTopologicalRing A
inst_10 : ContinuousStar A
inst_11 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
⊢ (Set.range fun (x : 𝕜 → 𝕜) ↦ cfcₙ (p := p) x a) ⊆ (↑(elemental 𝕜 a : NonUnitalStarSubalgebra 𝕜 A) : Set A)
have grw : (↑(NonUnitalStarAlgHom.range (F := ContinuousMapZero (↑(quasispectrum 𝕜 a) : Type u_1) 𝕜 →⋆ₙₐ[𝕜] A)
        (cfcₙHom (p := p) ha)) :
    Set A) ⊆
  (↑(elemental 𝕜 a : NonUnitalStarSubalgebra 𝕜 A) : Set A)
Tactic: grw [range_cfcₙ_eq_range_cfcₙHom 𝕜 ha, range_cfcₙHom_le 𝕜 ha]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : TopologicalSpace A
inst_7 : ContinuousConstSMul 𝕜 A
inst_8 : StarModule 𝕜 A
inst_9 : IsTopologicalRing A
inst_10 : ContinuousStar A
inst_11 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
grw :
  (↑(NonUnitalStarAlgHom.range (F := ContinuousMapZero (↑(quasispectrum 𝕜 a) : Type u_1) 𝕜 →⋆ₙₐ[𝕜] A)
          (cfcₙHom (p := p) ha)) :
      Set A) ⊆
    (↑(elemental 𝕜 a : NonUnitalStarSubalgebra 𝕜 A) : Set A)
⊢ (Set.range fun (x : 𝕜 → 𝕜) ↦ cfcₙ (p := p) x a) ⊆ (↑(elemental 𝕜 a : NonUnitalStarSubalgebra 𝕜 A) : Set A)
have grw₁ : (↑(elemental 𝕜 a : NonUnitalStarSubalgebra 𝕜 A) : Set A) ⊆ (↑(elemental 𝕜 a : NonUnitalStarSubalgebra 𝕜 A) : Set A)
Tactic: grw [range_cfcₙ_eq_range_cfcₙHom 𝕜 ha, range_cfcₙHom_le 𝕜 ha]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ Eq.{u_1 + 1} (α := Set A) (Set.range fun (x : ℝ≥0 → ℝ≥0) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) x a)
    ((fun (x : ℝ → ℝ) ↦ cfcₙ (p := IsSelfAdjoint) x a) '' {f : ℝ → ℝ | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x})
have h : ∀ (x : A),
  Membership.mem (γ := Set A) (Set.range fun (x : ℝ≥0 → ℝ≥0) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) x a) x ↔
    Membership.mem (γ := Set A)
      ((fun (x : ℝ → ℝ) ↦ cfcₙ (p := IsSelfAdjoint) x a) '' {f : ℝ → ℝ | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
x : A
⊢ Membership.mem (γ := Set A) (Set.range fun (x : ℝ≥0 → ℝ≥0) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) x a) x ↔
    Membership.mem (γ := Set A)
      ((fun (x : ℝ → ℝ) ↦ cfcₙ (p := IsSelfAdjoint) x a) '' {f : ℝ → ℝ | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x}) x
have h : Membership.mem (γ := Set A) (Set.range fun (x : ℝ≥0 → ℝ≥0) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) x a) x →
  Membership.mem (γ := Set A)
    ((fun (x : ℝ → ℝ) ↦ cfcₙ (p := IsSelfAdjoint) x a) '' {f : ℝ → ℝ | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x}) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
x : A
h :
  Membership.mem (γ := Set A) (Set.range fun (x : ℝ≥0 → ℝ≥0) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) x a) x →
    Membership.mem (γ := Set A)
      ((fun (x : ℝ → ℝ) ↦ cfcₙ (p := IsSelfAdjoint) x a) '' {f : ℝ → ℝ | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x}) x
⊢ Membership.mem (γ := Set A) (Set.range fun (x : ℝ≥0 → ℝ≥0) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) x a) x ↔
    Membership.mem (γ := Set A)
      ((fun (x : ℝ → ℝ) ↦ cfcₙ (p := IsSelfAdjoint) x a) '' {f : ℝ → ℝ | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x}) x
have h₁ : Membership.mem (γ := Set A)
    ((fun (x : ℝ → ℝ) ↦ cfcₙ (p := IsSelfAdjoint) x a) '' {f : ℝ → ℝ | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x}) x →
  Membership.mem (γ := Set A) (Set.range fun (x : ℝ≥0 → ℝ≥0) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) x a) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ≥0 → ℝ≥0
⊢ Membership.mem (γ := Set A)
    ((fun (x : ℝ → ℝ) ↦ cfcₙ (p := IsSelfAdjoint) x a) '' {f : ℝ → ℝ | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x})
    ((fun (x : ℝ≥0 → ℝ≥0) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) x a) f)
have h : Membership.mem (γ := Set A)
  ((fun (x : ℝ → ℝ) ↦ cfcₙ (p := IsSelfAdjoint) x a) '' {f : ℝ → ℝ | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x})
  (cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a)
Tactic: simp only [cfcₙ_nnreal_eq_real f a]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : Membership.mem (γ := Set (ℝ → ℝ)) {f : ℝ → ℝ | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x} f
⊢ Membership.mem (γ := Set A) (Set.range fun (x : ℝ≥0 → ℝ≥0) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) x a)
    ((fun (x : ℝ → ℝ) ↦ cfcₙ (p := IsSelfAdjoint) x a) f)
have h : Membership.mem (γ := Set A) (Set.range fun (x : ℝ≥0 → ℝ≥0) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) x a)
  (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ (f (↑x : ℝ)).toNNReal) a)
Tactic: simp only [cfcₙ_real_eq_nnreal a hf]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : StarModule ℝ A
inst_12 : ContinuousStar A
inst_13 : ContinuousConstSMul ℝ A
inst_14 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ Subset.{u_1} (α := Set A) (Set.range fun (x : ℝ≥0 → ℝ≥0) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) x a)
    {x : A |
      Membership.mem (γ := NonUnitalStarSubalgebra ℝ A)
          (NonUnitalStarAlgebra.elemental ℝ a : NonUnitalStarSubalgebra ℝ A) x ∧
        0 ≤ x}
have grw : Subset.{u_1} (α := Set A)
  ((fun (x : ℝ → ℝ) ↦ cfcₙ (p := IsSelfAdjoint) x a) '' {f : ℝ → ℝ | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x})
  ((fun (x : ℝ → ℝ) ↦ cfcₙ (p := IsSelfAdjoint) x a) ''
    Set.preimage.{0, u_1} (β := A) (fun (x : ℝ → ℝ) ↦ cfcₙ (p := IsSelfAdjoint) x a) {a : A | 0 ≤ a})
Tactic: grw [range_cfcₙ_nnreal_eq_image_cfcₙ_real a ha, Set.setOf_and, SetLike.setOf_mem_eq,
    ← range_cfcₙ_subset _ ha.isSelfAdjoint, Set.inter_comm, ← Set.image_preimage_eq_inter_range]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : StarModule ℝ A
inst_12 : ContinuousStar A
inst_13 : ContinuousConstSMul ℝ A
inst_14 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ Eq.{u_1 + 1} (α := Set A) (Set.range fun (x : ℝ≥0 → ℝ≥0) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) x a)
    {x : A |
      Membership.mem (γ := NonUnitalStarSubalgebra ℝ A)
          (NonUnitalStarAlgebra.elemental ℝ a : NonUnitalStarSubalgebra ℝ A) x ∧
        0 ≤ x}
have rw : Eq.{u_1 + 1} (α := Set A)
  ((fun (x : ℝ → ℝ) ↦ cfcₙ (p := IsSelfAdjoint) x a) '' {f : ℝ → ℝ | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x})
  ((fun (x : ℝ → ℝ) ↦ cfcₙ (p := IsSelfAdjoint) x a) ''
    Set.preimage.{0, u_1} (β := A) (fun (x : ℝ → ℝ) ↦ cfcₙ (p := IsSelfAdjoint) x a) {a : A | 0 ≤ a})
Tactic: rw [range_cfcₙ_nnreal_eq_image_cfcₙ_real a ha, Set.setOf_and, SetLike.setOf_mem_eq,
    ← range_cfcₙ _ ha.isSelfAdjoint, Set.inter_comm, ← Set.image_preimage_eq_inter_range]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : StarModule ℝ A
inst_12 : ContinuousStar A
inst_13 : ContinuousConstSMul ℝ A
inst_14 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ Eq.{u_1 + 1} (α := Set A)
    ((fun (x : ℝ → ℝ) ↦ cfcₙ (p := IsSelfAdjoint) x a) '' {f : ℝ → ℝ | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x})
    ((fun (x : ℝ → ℝ) ↦ cfcₙ (p := IsSelfAdjoint) x a) ''
      Set.preimage.{0, u_1} (β := A) (fun (x : ℝ → ℝ) ↦ cfcₙ (p := IsSelfAdjoint) x a) {a : A | 0 ≤ a})
have refine : Subset.{u_1} (α := Set A)
  ((fun (x : ℝ → ℝ) ↦ cfcₙ (p := IsSelfAdjoint) x a) ''
    Set.preimage.{0, u_1} (β := A) (fun (x : ℝ → ℝ) ↦ cfcₙ (p := IsSelfAdjoint) x a) {a : A | 0 ≤ a})
  ((fun (x : ℝ → ℝ) ↦ cfcₙ (p := IsSelfAdjoint) x a) '' {f : ℝ → ℝ | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x})
Tactic: refine Set.Subset.antisymm (Set.image_mono (fun _ ↦ cfcₙ_nonneg)) ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : StarModule ℝ A
inst_12 : ContinuousStar A
inst_13 : ContinuousConstSMul ℝ A
inst_14 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : 0 ≤ cfcₙ (p := IsSelfAdjoint) f a
⊢ ∃ (x : ℝ → ℝ), (∀ x_1 ∈ quasispectrum ℝ a, 0 ≤ x x_1) ∧ cfcₙ (p := IsSelfAdjoint) x a = cfcₙ (p := IsSelfAdjoint) f a
have inl : ∀ (h₁ : ContinuousOn f (quasispectrum ℝ a)) (h₂ : f 0 = 0) (h₃ : IsSelfAdjoint a),
  ∃ (x : ℝ → ℝ), (∀ x_1 ∈ quasispectrum ℝ a, 0 ≤ x x_1) ∧ cfcₙ (p := IsSelfAdjoint) x a = cfcₙ (p := IsSelfAdjoint) f a
Tactic: obtain (⟨h₁, h₂, h₃⟩ | h | h | h) := by
    simpa only [not_and_or] using
      em (ContinuousOn f (quasispectrum ℝ a) ∧ f 0 = 0 ∧ IsSelfAdjoint a)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : StarModule ℝ A
inst_12 : ContinuousStar A
inst_13 : ContinuousConstSMul ℝ A
inst_14 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : 0 ≤ cfcₙ (p := IsSelfAdjoint) f a
inl :
  ∀ (h₁ : ContinuousOn f (quasispectrum ℝ a)) (h₂ : f 0 = 0) (h₃ : IsSelfAdjoint a),
    ∃ (x : ℝ → ℝ),
      (∀ x_1 ∈ quasispectrum ℝ a, 0 ≤ x x_1) ∧ cfcₙ (p := IsSelfAdjoint) x a = cfcₙ (p := IsSelfAdjoint) f a
⊢ ∃ (x : ℝ → ℝ), (∀ x_1 ∈ quasispectrum ℝ a, 0 ≤ x x_1) ∧ cfcₙ (p := IsSelfAdjoint) x a = cfcₙ (p := IsSelfAdjoint) f a
have inr : ∀ (h : ¬ContinuousOn f (quasispectrum ℝ a)),
  ∃ (x : ℝ → ℝ), (∀ x_1 ∈ quasispectrum ℝ a, 0 ≤ x x_1) ∧ cfcₙ (p := IsSelfAdjoint) x a = cfcₙ (p := IsSelfAdjoint) f a
Tactic: obtain (⟨h₁, h₂, h₃⟩ | h | h | h) := by
    simpa only [not_and_or] using
      em (ContinuousOn f (quasispectrum ℝ a) ∧ f 0 = 0 ∧ IsSelfAdjoint a)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : StarModule ℝ A
inst_12 : ContinuousStar A
inst_13 : ContinuousConstSMul ℝ A
inst_14 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : 0 ≤ cfcₙ (p := IsSelfAdjoint) f a
inl :
  ∀ (h₁ : ContinuousOn f (quasispectrum ℝ a)) (h₂ : f 0 = 0) (h₃ : IsSelfAdjoint a),
    ∃ (x : ℝ → ℝ),
      (∀ x_1 ∈ quasispectrum ℝ a, 0 ≤ x x_1) ∧ cfcₙ (p := IsSelfAdjoint) x a = cfcₙ (p := IsSelfAdjoint) f a
inr :
  ∀ (h : ¬ContinuousOn f (quasispectrum ℝ a)),
    ∃ (x : ℝ → ℝ),
      (∀ x_1 ∈ quasispectrum ℝ a, 0 ≤ x x_1) ∧ cfcₙ (p := IsSelfAdjoint) x a = cfcₙ (p := IsSelfAdjoint) f a
⊢ ∃ (x : ℝ → ℝ), (∀ x_1 ∈ quasispectrum ℝ a, 0 ≤ x x_1) ∧ cfcₙ (p := IsSelfAdjoint) x a = cfcₙ (p := IsSelfAdjoint) f a
have inr₁ : ∀ (h : ¬f 0 = 0),
  ∃ (x : ℝ → ℝ), (∀ x_1 ∈ quasispectrum ℝ a, 0 ≤ x x_1) ∧ cfcₙ (p := IsSelfAdjoint) x a = cfcₙ (p := IsSelfAdjoint) f a
Tactic: obtain (⟨h₁, h₂, h₃⟩ | h | h | h) := by
    simpa only [not_and_or] using
      em (ContinuousOn f (quasispectrum ℝ a) ∧ f 0 = 0 ∧ IsSelfAdjoint a)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : StarModule ℝ A
inst_12 : ContinuousStar A
inst_13 : ContinuousConstSMul ℝ A
inst_14 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : 0 ≤ cfcₙ (p := IsSelfAdjoint) f a
inl :
  ∀ (h₁ : ContinuousOn f (quasispectrum ℝ a)) (h₂ : f 0 = 0) (h₃ : IsSelfAdjoint a),
    ∃ (x : ℝ → ℝ),
      (∀ x_1 ∈ quasispectrum ℝ a, 0 ≤ x x_1) ∧ cfcₙ (p := IsSelfAdjoint) x a = cfcₙ (p := IsSelfAdjoint) f a
inr :
  ∀ (h : ¬ContinuousOn f (quasispectrum ℝ a)),
    ∃ (x : ℝ → ℝ),
      (∀ x_1 ∈ quasispectrum ℝ a, 0 ≤ x x_1) ∧ cfcₙ (p := IsSelfAdjoint) x a = cfcₙ (p := IsSelfAdjoint) f a
inr₁ :
  ∀ (h : ¬f 0 = 0),
    ∃ (x : ℝ → ℝ),
      (∀ x_1 ∈ quasispectrum ℝ a, 0 ≤ x x_1) ∧ cfcₙ (p := IsSelfAdjoint) x a = cfcₙ (p := IsSelfAdjoint) f a
⊢ ∃ (x : ℝ → ℝ), (∀ x_1 ∈ quasispectrum ℝ a, 0 ≤ x x_1) ∧ cfcₙ (p := IsSelfAdjoint) x a = cfcₙ (p := IsSelfAdjoint) f a
have inr₂ : ∀ (h : ¬IsSelfAdjoint a),
  ∃ (x : ℝ → ℝ), (∀ x_1 ∈ quasispectrum ℝ a, 0 ≤ x x_1) ∧ cfcₙ (p := IsSelfAdjoint) x a = cfcₙ (p := IsSelfAdjoint) f a
Tactic: obtain (⟨h₁, h₂, h₃⟩ | h | h | h) := by
    simpa only [not_and_or] using
      em (ContinuousOn f (quasispectrum ℝ a) ∧ f 0 = 0 ∧ IsSelfAdjoint a)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : StarModule ℝ A
inst_12 : ContinuousStar A
inst_13 : ContinuousConstSMul ℝ A
inst_14 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : 0 ≤ cfcₙ (p := IsSelfAdjoint) f a
h₁ : ContinuousOn f (quasispectrum ℝ a)
h₂ : f 0 = 0
h₃ : IsSelfAdjoint a
⊢ ∃ (x : ℝ → ℝ), (∀ x_1 ∈ quasispectrum ℝ a, 0 ≤ x x_1) ∧ cfcₙ (p := IsSelfAdjoint) x a = cfcₙ (p := IsSelfAdjoint) f a
have inl : ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x
Tactic: refine ⟨f, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : Module ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : TopologicalSpace A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : PartialOrder A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : StarOrderedRing A
inst_11 : StarModule ℝ A
inst_12 : ContinuousStar A
inst_13 : ContinuousConstSMul ℝ A
inst_14 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : 0 ≤ cfcₙ (p := IsSelfAdjoint) f a
h₁ : ContinuousOn f (quasispectrum ℝ a)
h₂ : f 0 = 0
h₃ : IsSelfAdjoint a
⊢ ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x
have inl : ∀ (hf : ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x) (h₁ : ContinuousOn f (quasispectrum ℝ a)) (h₂ : f 0 = 0)
  (h₃ : IsSelfAdjoint a), ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x
Tactic: rwa [cfcₙ_nonneg_iff f a] at hf
Cleared hypotheses: hf, h₁, h₂, h₃
-- 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
| (↑(((ℜ : 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 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
⊢ cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ)) a =
    (↑(((ℜ : 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 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
⊢ cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ (↑x.re : ℂ)) a =
    cfcₙ (p := IsStarNormal) (fun (x : ℂ) ↦ HSMul.hSMul (α := ℝ) 2⁻¹ (x + star x)) a
have refine : ∀ (x : ℂ) (hx : x ∈ quasispectrum ℂ 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 : NonUnitalRing A
inst_2 : StarRing A
inst_3 : Module ℂ A
inst_4 : IsScalarTower ℂ A A
inst_5 : SMulCommClass ℂ A A
inst_6 : StarModule ℂ A
inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
x : ℂ
hx : x ∈ quasispectrum ℂ a
⊢ (↑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⁻¹]