awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi (goal)
Goal:
A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommRing S
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalSemiring R
inst_6 : ContinuousStar R
inst_7 : Algebra R S
inst_8 : NonUnitalRing A
inst_9 : NonUnitalRing B
inst_10 : Module S A
inst_11 : Module R A
inst_12 : Module R B
inst_13 : Module S B
inst_14 : SMulCommClass R A A
inst_15 : SMulCommClass R B B
inst_16 : IsScalarTower R A A
inst_17 : IsScalarTower R B B
inst_18 : StarRing A
inst_19 : StarRing B
inst_20 : TopologicalSpace A
inst_21 : TopologicalSpace B
inst_22 : IsScalarTower R S A
inst_23 : IsScalarTower R S B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst_24 : NonUnitalContinuousFunctionalCalculus R (A × B) pab
inst_25 : NonUnitalContinuousFunctionalCalculus R A pa
inst_26 : NonUnitalContinuousFunctionalCalculus R B pb
inst_27 : ContinuousMapZero.UniqueHom R A
inst_28 : ContinuousMapZero.UniqueHom R B
f : R → R
a : A
b : B
hf : ContinuousOn f (quasispectrum R a ∪ quasispectrum R b)
hab : pab (a, b)
ha : pa a
hb : pb b
hf₀ : f 0 = 0
ext : (cfcₙ (p := pab) f (a, b)).1 = (cfcₙ (p := pa) f a, cfcₙ (p := pb) f b).1
⊢ cfcₙ (p := pab) f (a, b) = (cfcₙ (p := pa) f a, cfcₙ (p := pb) f b)
have ext₁ : (cfcₙ (p := pab) f (a, b)).2 = (cfcₙ (p := pa) f a, cfcₙ (p := pb) f b).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi (goal)
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : CommRing S
inst_6 : Algebra R S
inst_7 : (i : ι) → Ring (A i)
inst_8 : (i : ι) → Algebra.{u_3, u_4} S (A i)
inst_9 : (i : ι) → Algebra.{u_2, u_4} R (A i)
inst_10 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R S (A i)
hinst : IsScalarTower R S ((i : ι) → A i)
inst_11 : (i : ι) → StarRing (A i)
inst_12 : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst_13 : ContinuousFunctionalCalculus R ((i : ι) → A i) p
inst_14 : ∀ (i : ι), ContinuousFunctionalCalculus R (A i) (q i)
inst_15 : ∀ (i : ι), ContinuousMap.UniqueHom.{u_2, u_4} R (A i)
f : R → R
a : (i : ι) → A i
hf : ContinuousOn f (⋃ (i : ι), spectrum R (a i))
ha : p a
ha' : ∀ (i : ι), q i (a i)
⊢ cfc (p := p) f a = fun (i : ι) ↦ cfc (p := q i) f (a i)
have h : ∀ (i : ι), cfc (p := p) f a i = cfc (p := q i) f (a i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi (goal)
Goal:
A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : CommRing S
inst_6 : Algebra R S
inst_7 : Ring A
inst_8 : Ring B
inst_9 : Algebra S A
inst_10 : Algebra S B
inst_11 : Algebra R A
inst_12 : Algebra R B
inst_13 : IsScalarTower R S A
inst_14 : IsScalarTower R S B
inst_15 : StarRing A
inst_16 : StarRing B
inst_17 : TopologicalSpace A
inst_18 : TopologicalSpace B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst_19 : ContinuousFunctionalCalculus R (A × B) pab
inst_20 : ContinuousFunctionalCalculus R A pa
inst_21 : ContinuousFunctionalCalculus R B pb
inst_22 : ContinuousMap.UniqueHom R A
inst_23 : ContinuousMap.UniqueHom R B
f : R → R
a : A
b : B
hf : ContinuousOn f (spectrum R a ∪ spectrum R b)
hab : pab (a, b)
ha : pa a
hb : pb b
⊢ cfc (p := pab) f (a, b) = (cfc (p := pa) f a, cfc (p := pb) f b)
have ext : (cfc (p := pab) f (a, b)).1 = (cfc (p := pa) f a, cfc (p := pb) f b).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi (goal)
Goal:
A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : CommRing S
inst_6 : Algebra R S
inst_7 : Ring A
inst_8 : Ring B
inst_9 : Algebra S A
inst_10 : Algebra S B
inst_11 : Algebra R A
inst_12 : Algebra R B
inst_13 : IsScalarTower R S A
inst_14 : IsScalarTower R S B
inst_15 : StarRing A
inst_16 : StarRing B
inst_17 : TopologicalSpace A
inst_18 : TopologicalSpace B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst_19 : ContinuousFunctionalCalculus R (A × B) pab
inst_20 : ContinuousFunctionalCalculus R A pa
inst_21 : ContinuousFunctionalCalculus R B pb
inst_22 : ContinuousMap.UniqueHom R A
inst_23 : ContinuousMap.UniqueHom R B
f : R → R
a : A
b : B
hf : ContinuousOn f (spectrum R a ∪ spectrum R b)
hab : pab (a, b)
ha : pa a
hb : pb b
ext : (cfc (p := pab) f (a, b)).1 = (cfc (p := pa) f a, cfc (p := pb) f b).1
⊢ cfc (p := pab) f (a, b) = (cfc (p := pa) f a, cfc (p := pb) f b)
have ext₁ : (cfc (p := pab) f (a, b)).2 = (cfc (p := pa) f a, cfc (p := pb) f b).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Field R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : Module R A
inst_9 : IsScalarTower R A A
inst_10 : SMulCommClass R A A
inst_11 : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
⊢ IsIdempotentElem a ↔ quasispectrum R a ⊆ {0, 1}
have refine : ∀ (h : quasispectrum R a ⊆ {0, 1}), IsIdempotentElem a
Tactic: refine ⟨IsIdempotentElem.quasispectrum_subset R, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Field R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : Module R A
inst_9 : IsScalarTower R A A
inst_10 : SMulCommClass R A A
inst_11 : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
h : quasispectrum R a ⊆ {0, 1}
⊢ IsIdempotentElem a
have rw : cfcₙ (p := p) (fun (x : R) ↦ x * x) a = cfcₙ (p := p) (fun (x : R) ↦ x) a
Tactic: rw [IsIdempotentElem, ← cfcₙ_id' R a, ← cfcₙ_mul _ _]
-- 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 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : StarModule 𝕜 A
inst_6 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p
inst_7 : IsTopologicalRing A
inst_8 : ContinuousStar A
a : A
ha : p a
⊢ Eq (α := StarSubalgebra 𝕜 A) (StarAlgHom.range (A := C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) (cfcHom (p := p) ha))
    (elemental 𝕜 a)
have rw : Eq (α := StarSubalgebra 𝕜 A)
  (StarSubalgebra.topologicalClosure
    (adjoin 𝕜
      (Set.image (α := C((↑(spectrum 𝕜 a) : Type u_1), 𝕜))
        (⇑(cfcHom (p := p) ha) : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
        {ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜)})))
  (elemental 𝕜 a)
Tactic: rw [StarAlgHom.range_eq_map_top, ← ContinuousMap.elemental_id_eq_top, StarAlgebra.elemental,
    ← StarSubalgebra.topologicalClosure_map _ _ (cfcHom_isClosedEmbedding ha (R := 𝕜)).isClosedMap
      (cfcHom_continuous ha), StarAlgHom.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 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : StarModule 𝕜 A
inst_6 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p
inst_7 : IsTopologicalRing A
inst_8 : ContinuousStar A
a : A
ha : p a
⊢ Eq (α := StarSubalgebra 𝕜 A)
    (StarSubalgebra.topologicalClosure
      (adjoin 𝕜
        (Set.image (α := C((↑(spectrum 𝕜 a) : Type u_1), 𝕜))
          (⇑(cfcHom (p := p) ha) : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
          {ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜)})))
    (elemental 𝕜 a)
have e_s : Eq (α := Set A)
  (Set.image (α := C((↑(spectrum 𝕜 a) : Type u_1), 𝕜))
    (⇑(cfcHom (p := p) ha) : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
    {ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜)})
  {a}
Tactic: congr
-- 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 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : StarModule 𝕜 A
inst_6 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p
inst_7 : IsTopologicalRing A
inst_8 : ContinuousStar A
a : A
ha : p a
⊢ (Set.range fun (x : 𝕜 → 𝕜) ↦ cfc (p := p) x a) = (↑(elemental 𝕜 a) : Set A)
have rw : (↑(StarAlgHom.range (A := C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) (cfcHom (p := p) ha)) : Set A) =
  (↑(elemental 𝕜 a) : Set A)
Tactic: rw [range_cfc_eq_range_cfcHom 𝕜 ha, range_cfcHom 𝕜 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 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : StarModule 𝕜 A
inst_6 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p
inst_7 : IsTopologicalRing A
inst_8 : ContinuousStar A
a : A
ha : p a
rw :
  (↑(StarAlgHom.range (A := C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) (cfcHom (p := p) ha)) : Set A) =
    (↑(elemental 𝕜 a) : Set A)
⊢ (Set.range fun (x : 𝕜 → 𝕜) ↦ cfc (p := p) x a) = (↑(elemental 𝕜 a) : Set A)
have rw₁ : (↑(elemental 𝕜 a) : Set A) = (↑(elemental 𝕜 a) : Set A)
Tactic: rw [range_cfc_eq_range_cfcHom 𝕜 ha, range_cfcHom 𝕜 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 : 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
⊢ LE.le (α := StarSubalgebra 𝕜 A) (StarAlgHom.range (A := C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) (cfcHom (p := p) ha))
    (elemental 𝕜 a)
have grw : LE.le (α := StarSubalgebra 𝕜 A)
  (StarSubalgebra.topologicalClosure
    (adjoin 𝕜
      (Set.image (α := C((↑(spectrum 𝕜 a) : Type u_1), 𝕜))
        (⇑(cfcHom (p := p) ha) : (a : C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) → A)
        {ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜)})))
  (elemental 𝕜 a)
Tactic: grw [StarAlgHom.range_eq_map_top, ← ContinuousMap.elemental_id_eq_top, StarAlgebra.elemental,
    StarSubalgebra.map_topologicalClosure_le _ _ (cfcHom_continuous ha (R := 𝕜)),
    StarAlgHom.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 : 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
⊢ (Set.range fun (x : 𝕜 → 𝕜) ↦ cfc (p := p) x a) ⊆ (↑(elemental 𝕜 a) : Set A)
have grw : (↑(StarAlgHom.range (A := C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) (cfcHom (p := p) ha)) : Set A) ⊆
  (↑(elemental 𝕜 a) : Set A)
Tactic: grw [range_cfc_eq_range_cfcHom 𝕜 ha, range_cfcHom_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 : 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
grw :
  (↑(StarAlgHom.range (A := C((↑(spectrum 𝕜 a) : Type u_1), 𝕜)) (cfcHom (p := p) ha)) : Set A) ⊆
    (↑(elemental 𝕜 a) : Set A)
⊢ (Set.range fun (x : 𝕜 → 𝕜) ↦ cfc (p := p) x a) ⊆ (↑(elemental 𝕜 a) : Set A)
have grw₁ : (↑(elemental 𝕜 a) : Set A) ⊆ (↑(elemental 𝕜 a) : Set A)
Tactic: grw [range_cfc_eq_range_cfcHom 𝕜 ha, range_cfcHom_le 𝕜 ha]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range (goal)
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
⊢ 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})
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 ∈ spectrum ℝ a, 0 ≤ f x}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range (goal)
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
⊢ 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
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 ∈ spectrum ℝ a, 0 ≤ f x}) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range (goal)
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})
    ((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 ∈ spectrum ℝ a, 0 ≤ f x})
  (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a)
Tactic: simp only [cfc_nnreal_eq_real f a ha]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range (goal)
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)
    ((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 : 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) (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}
have 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})
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 : 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
⊢ 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}
have 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)
Tactic: apply subset_antisymm (range_cfc_nnreal_subset a ha)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range (goal)
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
⊢ 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)
have 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})
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:
𝕜 : 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 (α := NonUnitalStarSubalgebra 𝕜 A)
    (NonUnitalStarAlgHom.range (F := ContinuousMapZero (↑(quasispectrum 𝕜 a) : Type u_1) 𝕜 →⋆ₙₐ[𝕜] A)
        (cfcₙHom (p := p) ha) :
      NonUnitalStarSubalgebra 𝕜 A)
    (elemental 𝕜 a : NonUnitalStarSubalgebra 𝕜 A)
have 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)
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]
-- 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
⊢ 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)
have 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}
Tactic: congr
-- 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
⊢ (Set.range fun (x : 𝕜 → 𝕜) ↦ cfcₙ (p := p) x a) = (↑(elemental 𝕜 a : NonUnitalStarSubalgebra 𝕜 A) : Set A)
have rw : (↑(NonUnitalStarAlgHom.range (F := ContinuousMapZero (↑(quasispectrum 𝕜 a) : Type u_1) 𝕜 →⋆ₙₐ[𝕜] A)
        (cfcₙHom (p := p) ha)) :
    Set A) =
  (↑(elemental 𝕜 a : NonUnitalStarSubalgebra 𝕜 A) : Set A)
Tactic: rw [range_cfcₙ_eq_range_cfcₙHom 𝕜 ha, range_cfcₙHom 𝕜 ha]