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 : 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 :
  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)
⊢ 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)

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

Premises used: NonUnitalStarAlgebra.elemental, cfcₙHom_continuous, NonUnitalStarAlgebra.map_top, NonUnitalStarAlgHom.map_adjoin, ContinuousMapZero.elemental_eq_top, NonUnitalStarSubalgebra.map_topologicalClosure_le
-- 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 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
⊢ 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:
simp [cfcₙHom_id ha, elemental]

Premises used: cfcₙHom_id, NonUnitalStarAlgebra.elemental
-- 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 : 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)
grw₁ grw₂ :
  (↑(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:
grw [range_cfcₙ_eq_range_cfcₙHom 𝕜 ha, range_cfcₙHom_le 𝕜 ha]

Premises used: range_cfcₙ_eq_range_cfcₙHom, range_cfcₙHom_le
-- 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 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
f : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀
⊢ Membership.mem (α := A) (γ := NonUnitalStarSubalgebra 𝕜 A) (elemental 𝕜 a : NonUnitalStarSubalgebra 𝕜 A)
    ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum 𝕜 a) : Type u_1), 𝕜)₀) → A) f : A)

Tactic:
range_cfcₙHom_le 𝕜 ha ⟨f, rfl⟩

Premises used: Set.Mem, range_cfcₙHom_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 : 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
f : 𝕜 → 𝕜
a : A
⊢ Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 A) (elemental 𝕜 a : NonUnitalStarSubalgebra 𝕜 A) (cfcₙ (p := p) f a)

Tactic:
cfcₙ_cases _ a f (zero_mem _) fun hf hf₀ ha ↦
    cfcₙHom_mem_elemental ha ⟨⟨_, hf.restrict⟩, hf₀⟩

Premises used: cfcₙHom_mem_elemental, ContinuousMap.mk, quasispectrum, ContinuousOn.restrict, ContinuousMapZero.mk, 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 : 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
𝕜' : Type u_3
S : Type u_4
inst_12 : Monoid 𝕜'
inst_13 : MulAction 𝕜' A
inst_14 : SetLike S A
inst_15 : NonUnitalSubringClass S A
inst_16 : SMul 𝕜 𝕜'
inst_17 : IsScalarTower 𝕜 𝕜' A
inst_18 : SMulMemClass S 𝕜' A
inst_19 : StarMemClass S A
s : S
hs : IsClosed[inst_6] (↑s : Set A)
f : 𝕜 → 𝕜
a : A
has : a ∈ s
this : SMulMemClass S 𝕜 A
⊢ LE.le (α := NonUnitalStarSubalgebra 𝕜 A) (adjoin 𝕜 (A := A) {a} : NonUnitalStarSubalgebra 𝕜 A)
    (NonUnitalStarSubalgebra.ofClass s : NonUnitalStarSubalgebra 𝕜 A)

Tactic:
simpa
-- 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 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
𝕜' : Type u_3
S : Type u_4
inst_12 : Monoid 𝕜'
inst_13 : MulAction 𝕜' A
inst_14 : SetLike S A
inst_15 : NonUnitalSubringClass S A
inst_16 : SMul 𝕜 𝕜'
inst_17 : IsScalarTower 𝕜 𝕜' A
inst_18 : SMulMemClass S 𝕜' A
inst_19 : StarMemClass S A
s : S
hs : IsClosed[inst_6] (↑s : Set A)
f : 𝕜 → 𝕜
a : A
has : a ∈ s
this : SMulMemClass S 𝕜 A
⊢ IsClosed[inst_6] (↑(NonUnitalStarSubalgebra.ofClass s) : Set A)

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
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
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
⊢ 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})

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
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
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
⊢ 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
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
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
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)
⊢ 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)

Tactic:
simp only [cfcₙ_nnreal_eq_real f a]

Premises used: cfcₙ_nnreal_eq_real
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
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
x : ℝ
h : x ∈ quasispectrum ℝ a
⊢ 0 ≤ (↑(f x.toNNReal) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
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})
    (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 : 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
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 : 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)
    (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 : 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)
    (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 : 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
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})
⊢ 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}

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: Set.setOf_and, LE.le.isSelfAdjoint, SetLike.setOf_mem_eq, Set.image_preimage_eq_inter_range, range_cfcₙ_nnreal_eq_image_cfcₙ_real, Set.inter_comm, range_cfcₙ_subset
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
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)
    ((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:
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 : 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)
    ((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:
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 : 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
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})
⊢ 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}

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, range_cfcₙ, Set.image_preimage_eq_inter_range, range_cfcₙ_nnreal_eq_image_cfcₙ_real, Set.inter_comm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
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})

Tactic:
Set.Subset.antisymm (Set.image_mono (fun _ ↦ cfcₙ_nonneg)) ?_

Premises used: Set.Subset.antisymm, Set.image_mono, cfcₙ_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
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
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})
⊢ 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:
refine Set.Subset.antisymm (Set.image_mono (fun _ ↦ cfcₙ_nonneg)) ?_

Premises used: Set.Subset.antisymm, Set.image_mono, cfcₙ_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
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
⊢ ContinuousOn f (quasispectrum ℝ a) ∧ f 0 = 0 ∧ IsSelfAdjoint a ∨
    ¬ContinuousOn f (quasispectrum ℝ a) ∨ ¬f 0 = 0 ∨ ¬IsSelfAdjoint a

Tactic:
simpa only [not_and_or] using
      em (ContinuousOn f (quasispectrum ℝ a) ∧ f 0 = 0 ∧ IsSelfAdjoint a)

Premises used: IsSelfAdjoint, Real, quasispectrum, em, And, not_and_or, ContinuousOn, OfNat.ofNat, Eq
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
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
inr₂ :
  ∀ (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

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)