awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : StarModule 𝕜 A
inst_6 : ContinuousFunctionalCalculus 𝕜 A p
inst_7 : IsTopologicalRing A
inst_8 : ContinuousStar A
a : A
ha : p a
f : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)
⊢ Membership.mem (α := A) (γ := StarSubalgebra 𝕜 A) (elemental 𝕜 a)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A) f : A)

Tactic:
range_cfcHom_le 𝕜 ha ⟨f, rfl⟩

Premises used: range_cfcHom_le, Exists.intro, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : StarModule 𝕜 A
inst_6 : ContinuousFunctionalCalculus 𝕜 A p
inst_7 : IsTopologicalRing A
inst_8 : ContinuousStar A
f : 𝕜 → 𝕜
a : A
⊢ Membership.mem (γ := StarSubalgebra 𝕜 A) (elemental 𝕜 a) (cfc (p := p) f a)

Tactic:
cfc_cases _ a f (zero_mem _) fun hf ha ↦
    cfcHom_mem_elemental ha ⟨_, hf.restrict⟩

Premises used: cfcHom_mem_elemental, spectrum, ContinuousMap.mk, ContinuousOn.restrict, ZeroMemClass.zero_mem, Set.restrict, cfc_cases
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : StarModule 𝕜 A
inst_6 : ContinuousFunctionalCalculus 𝕜 A p
inst_7 : IsTopologicalRing A
inst_8 : ContinuousStar A
𝕜' : Type u_3
S : Type u_4
inst_9 : Monoid 𝕜'
inst_10 : MulAction 𝕜' A
inst_11 : SetLike S A
inst_12 : SubringClass S A
inst_13 : SMul 𝕜 𝕜'
inst_14 : IsScalarTower 𝕜 𝕜' A
inst_15 : SMulMemClass S 𝕜' A
inst_16 : StarMemClass S A
s : S
hs : IsClosed[inst_4] (↑s : Set A)
f : 𝕜 → 𝕜
a : A
has : a ∈ s
this : SMulMemClass S 𝕜 A
⊢ LE.le (α := StarSubalgebra 𝕜 A) (adjoin 𝕜 {a}) (StarSubalgebra.ofClass s)

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : StarModule 𝕜 A
inst_6 : ContinuousFunctionalCalculus 𝕜 A p
inst_7 : IsTopologicalRing A
inst_8 : ContinuousStar A
𝕜' : Type u_3
S : Type u_4
inst_9 : Monoid 𝕜'
inst_10 : MulAction 𝕜' A
inst_11 : SetLike S A
inst_12 : SubringClass S A
inst_13 : SMul 𝕜 𝕜'
inst_14 : IsScalarTower 𝕜 𝕜' A
inst_15 : SMulMemClass S 𝕜' A
inst_16 : StarMemClass S A
s : S
hs : IsClosed[inst_4] (↑s : Set A)
f : 𝕜 → 𝕜
a : A
has : a ∈ s
this : SMulMemClass S 𝕜 A
⊢ IsClosed[inst_4] (↑(StarSubalgebra.ofClass s) : Set A)

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalRing A
inst_5 : T2Space A
inst_6 : PartialOrder A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : StarOrderedRing A
inst_9 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
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 ∈ spectrum ℝ a, 0 ≤ f x}) x
⊢ 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 ∈ spectrum ℝ a, 0 ≤ f x})

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalRing A
inst_5 : T2Space A
inst_6 : PartialOrder A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : StarOrderedRing A
inst_9 : ContinuousFunctionalCalculus ℝ 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 ∈ spectrum ℝ a, 0 ≤ f x}) x
h₁ :
  Membership.mem (γ := Set A)
      ((fun (x : ℝ → ℝ) ↦ cfc (p := IsSelfAdjoint) x a) '' {f : ℝ → ℝ | ∀ x ∈ spectrum ℝ 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) (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 ∈ spectrum ℝ a, 0 ≤ f x}) x

Tactic:
constructor
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalRing A
inst_5 : T2Space A
inst_6 : PartialOrder A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : StarOrderedRing A
inst_9 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ≥0 → ℝ≥0
h :
  Membership.mem (γ := Set A)
    ((fun (x : ℝ → ℝ) ↦ cfc (p := IsSelfAdjoint) x a) '' {f : ℝ → ℝ | ∀ x ∈ spectrum ℝ a, 0 ≤ f x})
    (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a)
⊢ Membership.mem (γ := Set A)
    ((fun (x : ℝ → ℝ) ↦ cfc (p := IsSelfAdjoint) x a) '' {f : ℝ → ℝ | ∀ x ∈ spectrum ℝ a, 0 ≤ f x})
    ((fun (x : ℝ≥0 → ℝ≥0) ↦ cfc (p := fun (x : A) ↦ 0 ≤ x) x a) f)

Tactic:
simp only [cfc_nnreal_eq_real f a ha]

Premises used: cfc_nnreal_eq_real
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalRing A
inst_5 : T2Space A
inst_6 : PartialOrder A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : StarOrderedRing A
inst_9 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ≥0 → ℝ≥0
x : ℝ
h : x ∈ spectrum ℝ a
⊢ 0 ≤ (↑(f x.toNNReal) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalRing A
inst_5 : T2Space A
inst_6 : PartialOrder A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : StarOrderedRing A
inst_9 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ≥0 → ℝ≥0
⊢ Membership.mem (γ := Set A)
    ((fun (x : ℝ → ℝ) ↦ cfc (p := IsSelfAdjoint) x a) '' {f : ℝ → ℝ | ∀ x ∈ spectrum ℝ a, 0 ≤ f x})
    (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a)

Tactic:
exact ⟨_, fun _ _ ↦ by positivity, rfl⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalRing A
inst_5 : T2Space A
inst_6 : PartialOrder A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : StarOrderedRing A
inst_9 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : Membership.mem (γ := Set (ℝ → ℝ)) {f : ℝ → ℝ | ∀ x ∈ spectrum ℝ a, 0 ≤ f x} f
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)
⊢ 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)

Tactic:
simp only [cfc_real_eq_nnreal a hf]

Premises used: cfc_real_eq_nnreal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalRing A
inst_5 : T2Space A
inst_6 : PartialOrder A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : StarOrderedRing A
inst_9 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : Membership.mem (γ := Set (ℝ → ℝ)) {f : ℝ → ℝ | ∀ x ∈ spectrum ℝ a, 0 ≤ f x} f
⊢ 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:
⟨_, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalRing A
inst_5 : T2Space A
inst_6 : PartialOrder A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : StarOrderedRing A
inst_9 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : Membership.mem (γ := Set (ℝ → ℝ)) {f : ℝ → ℝ | ∀ x ∈ spectrum ℝ a, 0 ≤ f x} f
⊢ 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:
exact ⟨_, rfl⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalRing A
inst_5 : T2Space A
inst_6 : PartialOrder A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : StarOrderedRing A
inst_9 : ContinuousStar A
inst_10 : StarModule ℝ A
inst_11 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
grw :
  Subset.{u_1} (α := Set A)
    ((fun (x : ℝ → ℝ) ↦ cfc (p := IsSelfAdjoint) x a) '' {f : ℝ → ℝ | ∀ x ∈ spectrum ℝ 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})
⊢ Subset.{u_1} (α := Set A) (Set.range fun (x : ℝ≥0 → ℝ≥0) ↦ cfc (p := fun (x : A) ↦ 0 ≤ x) x a)
    {x : A | Membership.mem (γ := StarSubalgebra ℝ A) (StarAlgebra.elemental ℝ a) x ∧ 0 ≤ x}

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]

Premises used: Real, Set.setOf_and, LE.le.isSelfAdjoint, SetLike.setOf_mem_eq, range_cfc_subset, Set.image_preimage_eq_inter_range, Set.inter_comm, range_cfc_nnreal_eq_image_cfc_real
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalRing A
inst_5 : T2Space A
inst_6 : PartialOrder A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : StarOrderedRing A
inst_9 : ContinuousStar A
inst_10 : StarModule ℝ A
inst_11 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ Subset.{u_1} (α := Set A)
    ((fun (x : ℝ → ℝ) ↦ cfc (p := IsSelfAdjoint) x a) '' {f : ℝ → ℝ | ∀ x ∈ spectrum ℝ 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:
Set.image_mono fun _ ↦ cfc_nonneg

Premises used: Set.image_mono, cfc_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalRing A
inst_5 : T2Space A
inst_6 : PartialOrder A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : StarOrderedRing A
inst_9 : ContinuousStar A
inst_10 : StarModule ℝ A
inst_11 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ Subset.{u_1} (α := Set A)
    ((fun (x : ℝ → ℝ) ↦ cfc (p := IsSelfAdjoint) x a) '' {f : ℝ → ℝ | ∀ x ∈ spectrum ℝ 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:
exact Set.image_mono fun _ ↦ cfc_nonneg

Premises used: Set.image_mono, cfc_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalRing A
inst_5 : T2Space A
inst_6 : PartialOrder A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : StarOrderedRing A
inst_9 : ContinuousStar A
inst_10 : StarModule ℝ A
inst_11 : ClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
apply :
  Subset.{u_1} (α := Set A) {x : A | Membership.mem (γ := StarSubalgebra ℝ A) (StarAlgebra.elemental ℝ a) x ∧ 0 ≤ x}
    (Set.range fun (x : ℝ≥0 → ℝ≥0) ↦ cfc (p := fun (x : A) ↦ 0 ≤ x) x 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 (γ := StarSubalgebra ℝ A) (StarAlgebra.elemental ℝ a) x ∧ 0 ≤ x}

Tactic:
apply subset_antisymm (range_cfc_nnreal_subset a ha)

Premises used: subset_antisymm, range_cfc_nnreal_subset
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalRing A
inst_5 : T2Space A
inst_6 : PartialOrder A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : StarOrderedRing A
inst_9 : ContinuousStar A
inst_10 : StarModule ℝ A
inst_11 : ClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
rw :
  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 ∈ spectrum ℝ a, 0 ≤ f x})
⊢ Subset.{u_1} (α := Set A) {x : A | Membership.mem (γ := StarSubalgebra ℝ A) (StarAlgebra.elemental ℝ a) x ∧ 0 ≤ x}
    (Set.range fun (x : ℝ≥0 → ℝ≥0) ↦ cfc (p := fun (x : A) ↦ 0 ≤ x) x 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]

Premises used: Set.setOf_and, LE.le.isSelfAdjoint, SetLike.setOf_mem_eq, Set.image_preimage_eq_inter_range, Set.inter_comm, range_cfc_nnreal_eq_image_cfc_real, range_cfc
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalRing A
inst_5 : T2Space A
inst_6 : PartialOrder A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : StarOrderedRing A
inst_9 : ContinuousStar A
inst_10 : StarModule ℝ A
inst_11 : ClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf :
  Membership.mem (γ := Set (ℝ → ℝ))
    (Set.preimage.{0, u_1} (β := A) (fun (x : ℝ → ℝ) ↦ cfc (p := IsSelfAdjoint) x a) {a : A | 0 ≤ a}) f
⊢ Membership.mem (γ := Set (ℝ → ℝ)) {f : ℝ → ℝ | ∀ x ∈ spectrum ℝ a, 0 ≤ f x} 0

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalRing A
inst_5 : T2Space A
inst_6 : PartialOrder A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : StarOrderedRing A
inst_9 : ContinuousStar A
inst_10 : StarModule ℝ A
inst_11 : ClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf :
  Membership.mem (γ := Set (ℝ → ℝ))
    (Set.preimage.{0, u_1} (β := A) (fun (x : ℝ → ℝ) ↦ cfc (p := IsSelfAdjoint) x a) {a : A | 0 ≤ a}) f
⊢ Eq.{u_1 + 1} (α := A) ((fun (x : ℝ → ℝ) ↦ cfc (p := IsSelfAdjoint) x a) 0) 0

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalRing A
inst_5 : T2Space A
inst_6 : PartialOrder A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : StarOrderedRing A
inst_9 : ContinuousStar A
inst_10 : StarModule ℝ A
inst_11 : ClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf :
  Membership.mem (γ := Set (ℝ → ℝ))
    (Set.preimage.{0, u_1} (β := A) (fun (x : ℝ → ℝ) ↦ cfc (p := IsSelfAdjoint) x a) {a : A | 0 ≤ a}) f
hf' : ContinuousOn f (spectrum ℝ a)
ha' : IsSelfAdjoint a
⊢ 0 ≤ cfc (p := IsSelfAdjoint) f a

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalRing A
inst_5 : T2Space A
inst_6 : PartialOrder A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : StarOrderedRing A
inst_9 : ContinuousStar A
inst_10 : StarModule ℝ A
inst_11 : ClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf :
  Membership.mem (γ := Set (ℝ → ℝ))
    (Set.preimage.{0, u_1} (β := A) (fun (x : ℝ → ℝ) ↦ cfc (p := IsSelfAdjoint) x a) {a : A | 0 ≤ a}) f
hf' : ContinuousOn f (spectrum ℝ a)
ha' : IsSelfAdjoint a
⊢ Eq (α := A) ((fun (x : ℝ → ℝ) ↦ cfc (p := IsSelfAdjoint) x a) f : A)
    ((cfcHom (p := IsSelfAdjoint) ha' : (a : C((↑(spectrum ℝ a) : Type), ℝ)) → A)
        { toFun := (spectrum ℝ a).restrict (π := fun (a : ℝ) ↦ ℝ) f, continuous_toFun := ⋯ :
          C((↑(spectrum ℝ a) : Type), ℝ) } :
      A)

Tactic:
simp [cfc_apply f a ha' hf']

Premises used: cfc_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
Goal:
A : Type u_1
inst : Ring A
inst_1 : StarRing A
inst_2 : Algebra ℝ A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalRing A
inst_5 : T2Space A
inst_6 : PartialOrder A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : StarOrderedRing A
inst_9 : ContinuousStar A
inst_10 : StarModule ℝ A
inst_11 : ClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf :
  Membership.mem (γ := Set (ℝ → ℝ))
    (Set.preimage.{0, u_1} (β := A) (fun (x : ℝ → ℝ) ↦ cfc (p := IsSelfAdjoint) x a) {a : A | 0 ≤ a}) f
⊢ Membership.mem (γ := Set A)
    ((fun (x : ℝ → ℝ) ↦ cfc (p := IsSelfAdjoint) x a) '' {f : ℝ → ℝ | ∀ x ∈ spectrum ℝ a, 0 ≤ f x})
    ((fun (x : ℝ → ℝ) ↦ cfc (p := IsSelfAdjoint) x a) f)

Tactic:
exact cfc_cases _ a f ⟨0, by simp, by simp⟩ fun hf' ha' ↦
    ⟨f, (cfc_nonneg_iff f a hf' ha').mp (by simpa), by simp [cfc_apply f a ha' hf']⟩

Premises used: cfc_cases
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
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 :
  Eq (α := 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)
⊢ Eq (α := NonUnitalStarSubalgebra 𝕜 A)
    (NonUnitalStarAlgHom.range (F := ContinuousMapZero (↑(quasispectrum 𝕜 a) : Type u_1) 𝕜 →⋆ₙₐ[𝕜] A)
        (cfcₙHom (p := p) ha) :
      NonUnitalStarSubalgebra 𝕜 A)
    (elemental 𝕜 a : NonUnitalStarSubalgebra 𝕜 A)

Tactic:
rw [← NonUnitalStarAlgebra.map_top, ← ContinuousMapZero.elemental_eq_top,
    NonUnitalStarAlgebra.elemental, ← NonUnitalStarSubalgebra.topologicalClosure_map _
    (cfcₙHom_isClosedEmbedding ha (R := 𝕜)).isClosedMap (cfcₙHom_continuous ha),
    NonUnitalStarAlgHom.map_adjoin]

Premises used: Topology.IsClosedEmbedding.isClosedMap, NonUnitalStarAlgebra.elemental, cfcₙHom_isClosedEmbedding, cfcₙHom_continuous, NonUnitalStarAlgebra.map_top, NonUnitalStarAlgHom.map_adjoin, NonUnitalStarSubalgebra.topologicalClosure_map, ContinuousMapZero.elemental_eq_top
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
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
e_s :
  Eq (α := Set 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)})
    {a}
⊢ Eq (α := 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:
congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
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
⊢ Eq (α := Set 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)})
    {a}

Tactic:
simpa using cfcₙHom_id ha

Premises used: cfcₙHom_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
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)
rw₁ rw₂ :
  (↑(elemental 𝕜 a : NonUnitalStarSubalgebra 𝕜 A) : Set A) = (↑(elemental 𝕜 a : NonUnitalStarSubalgebra 𝕜 A) : Set A)
⊢ (Set.range fun (x : 𝕜 → 𝕜) ↦ cfcₙ (p := p) x a) = (↑(elemental 𝕜 a : NonUnitalStarSubalgebra 𝕜 A) : Set A)

Tactic:
rw [range_cfcₙ_eq_range_cfcₙHom 𝕜 ha, range_cfcₙHom 𝕜 ha]

Premises used: range_cfcₙHom, range_cfcₙ_eq_range_cfcₙHom