mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
A : ι → Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalSemiring R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : (i : ι) → Ring (A i)
inst✝⁷ : (i : ι) → Algebra S (A i)
inst✝⁶ : (i : ι) → Algebra R (A i)
inst✝⁵ : ∀ (i : ι), IsScalarTower R S (A i)
hinst : IsScalarTower R S ((i : ι) → A i)
inst✝⁴ : (i : ι) → StarRing (A i)
inst✝³ : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst✝² : ContinuousFunctionalCalculus R ((i : ι) → A i) p
inst✝¹ : ∀ (i : ι), ContinuousFunctionalCalculus R (A i) (q i)
inst✝ : ∀ (i : ι), ContinuousMap.UniqueHom 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)
i : ι
⊢ cfc f a i = cfc f (a i)

Tactic:
let φ := Pi.evalStarAlgHom S A i

Goal state after:
ι : Type u_1
R : Type u_2
S : Type u_3
A : ι → Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalSemiring R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : (i : ι) → Ring (A i)
inst✝⁷ : (i : ι) → Algebra S (A i)
inst✝⁶ : (i : ι) → Algebra R (A i)
inst✝⁵ : ∀ (i : ι), IsScalarTower R S (A i)
hinst : IsScalarTower R S ((i : ι) → A i)
inst✝⁴ : (i : ι) → StarRing (A i)
inst✝³ : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst✝² : ContinuousFunctionalCalculus R ((i : ι) → A i) p
inst✝¹ : ∀ (i : ι), ContinuousFunctionalCalculus R (A i) (q i)
inst✝ : ∀ (i : ι), ContinuousMap.UniqueHom 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)
i : ι
φ : ((i : ι) → A i) →⋆ₐ[S] A i := Pi.evalStarAlgHom S A i
⊢ cfc f a i = cfc f (a i)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsStarNormal a
this : Isometry ⇑((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a))
f : C(↑(spectrum ℂ a), ℂ)
⊢ Commute (star (((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a)) f))
    (((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a)) f)

Tactic:
by rw [← map_star]; exact Commute.all (star f) f |>.map _

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric

Goal state before:
pp: A : Type u_1
inst✝¹⁰ : NonUnitalNormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : NormedSpace ℝ A
inst✝⁷ : IsScalarTower ℝ A A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : ContinuousStar A
inst✝ : CompleteSpace A
r : ℝ≥0
⊢ ContinuousOn (fun x ↦ x ^ r) {a | 0 ≤ a}

Tactic:
obtain (rfl | hr) := eq_zero_or_pos r

Goal state after:
case inl
A : Type u_1
inst✝¹⁰ : NonUnitalNormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : NormedSpace ℝ A
inst✝⁷ : IsScalarTower ℝ A A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : ContinuousStar A
inst✝ : CompleteSpace A
⊢ ContinuousOn (fun x ↦ x ^ 0) {a | 0 ≤ a}

case inr
A : Type u_1
inst✝¹⁰ : NonUnitalNormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : NormedSpace ℝ A
inst✝⁷ : IsScalarTower ℝ A A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : ContinuousStar A
inst✝ : CompleteSpace A
r : ℝ≥0
hr : 0 < r
⊢ ContinuousOn (fun x ↦ x ^ r) {a | 0 ≤ a}
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ a
⊢ a ^ 3 = a * a * a

Tactic:
simp only [nnrpow_def, NNReal.nnrpow_def, NNReal.coe_ofNat, NNReal.rpow_ofNat, pow_three]

Goal state after:
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ a
⊢ cfcₙ (fun x ↦ x * (x * x)) a = a * a * a
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝²⁵ : PartialOrder A
inst✝²⁴ : NonUnitalRing A
inst✝²³ : TopologicalSpace A
inst✝²² : StarRing A
inst✝²¹ : Module ℝ A
inst✝²⁰ : SMulCommClass ℝ A A
inst✝¹⁹ : IsScalarTower ℝ A A
inst✝¹⁸ : StarOrderedRing A
inst✝¹⁷ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹⁶ : NonnegSpectrumClass ℝ A
inst✝¹⁵ : IsSemitopologicalRing A
inst✝¹⁴ : T2Space A
B : Type u_2
inst✝¹³ : PartialOrder B
inst✝¹² : NonUnitalRing B
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : StarRing B
inst✝⁹ : Module ℝ B
inst✝⁸ : SMulCommClass ℝ B B
inst✝⁷ : IsScalarTower ℝ B B
inst✝⁶ : StarOrderedRing B
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst✝⁴ : NonUnitalContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst✝³ : IsSemitopologicalRing B
inst✝² : T2Space B
inst✝¹ : NonnegSpectrumClass ℝ B
inst✝ : NonnegSpectrumClass ℝ (A × B)
a : A
b : B
ha : 0 ≤ a
hb : 0 ≤ b
⊢ sqrt (a, b) = (sqrt a, sqrt b)

Tactic:
simp only [sqrt_eq_nnrpow]

Goal state after:
A : Type u_1
inst✝²⁵ : PartialOrder A
inst✝²⁴ : NonUnitalRing A
inst✝²³ : TopologicalSpace A
inst✝²² : StarRing A
inst✝²¹ : Module ℝ A
inst✝²⁰ : SMulCommClass ℝ A A
inst✝¹⁹ : IsScalarTower ℝ A A
inst✝¹⁸ : StarOrderedRing A
inst✝¹⁷ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹⁶ : NonnegSpectrumClass ℝ A
inst✝¹⁵ : IsSemitopologicalRing A
inst✝¹⁴ : T2Space A
B : Type u_2
inst✝¹³ : PartialOrder B
inst✝¹² : NonUnitalRing B
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : StarRing B
inst✝⁹ : Module ℝ B
inst✝⁸ : SMulCommClass ℝ B B
inst✝⁷ : IsScalarTower ℝ B B
inst✝⁶ : StarOrderedRing B
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst✝⁴ : NonUnitalContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst✝³ : IsSemitopologicalRing B
inst✝² : T2Space B
inst✝¹ : NonnegSpectrumClass ℝ B
inst✝ : NonnegSpectrumClass ℝ (A × B)
a : A
b : B
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a, b) ^ (1 / 2) = (a ^ (1 / 2), b ^ (1 / 2))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: ι : Type u_2
C : ι → Type u_3
inst✝¹⁴ : (i : ι) → PartialOrder (C i)
inst✝¹³ : (i : ι) → NonUnitalRing (C i)
inst✝¹² : (i : ι) → TopologicalSpace (C i)
inst✝¹¹ : (i : ι) → StarRing (C i)
inst✝¹⁰ : ∀ (i : ι), StarOrderedRing (C i)
inst✝⁹ : StarOrderedRing ((i : ι) → C i)
inst✝⁸ : (i : ι) → Module ℝ (C i)
inst✝⁷ : ∀ (i : ι), SMulCommClass ℝ (C i) (C i)
inst✝⁶ : ∀ (i : ι), IsScalarTower ℝ (C i) (C i)
inst✝⁵ : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus ℝ (C i) IsSelfAdjoint
inst✝⁴ : NonUnitalContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint
inst✝³ : ∀ (i : ι), IsSemitopologicalRing (C i)
inst✝² : ∀ (i : ι), T2Space (C i)
inst✝¹ : NonnegSpectrumClass ℝ ((i : ι) → C i)
inst✝ : ∀ (i : ι), NonnegSpectrumClass ℝ (C i)
c : (i : ι) → C i
hc : ∀ (i : ι), 0 ≤ c i
⊢ sqrt c = fun i ↦ sqrt (c i)

Tactic:
simp only [sqrt_eq_nnrpow]

Goal state after:
ι : Type u_2
C : ι → Type u_3
inst✝¹⁴ : (i : ι) → PartialOrder (C i)
inst✝¹³ : (i : ι) → NonUnitalRing (C i)
inst✝¹² : (i : ι) → TopologicalSpace (C i)
inst✝¹¹ : (i : ι) → StarRing (C i)
inst✝¹⁰ : ∀ (i : ι), StarOrderedRing (C i)
inst✝⁹ : StarOrderedRing ((i : ι) → C i)
inst✝⁸ : (i : ι) → Module ℝ (C i)
inst✝⁷ : ∀ (i : ι), SMulCommClass ℝ (C i) (C i)
inst✝⁶ : ∀ (i : ι), IsScalarTower ℝ (C i) (C i)
inst✝⁵ : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus ℝ (C i) IsSelfAdjoint
inst✝⁴ : NonUnitalContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint
inst✝³ : ∀ (i : ι), IsSemitopologicalRing (C i)
inst✝² : ∀ (i : ι), T2Space (C i)
inst✝¹ : NonnegSpectrumClass ℝ ((i : ι) → C i)
inst✝ : ∀ (i : ι), NonnegSpectrumClass ℝ (C i)
c : (i : ι) → C i
hc : ∀ (i : ι), 0 ≤ c i
⊢ c ^ (1 / 2) = fun i ↦ c i ^ (1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ
h : IsUnit a
ha : 0 ≤ a
this : IsStrictlyPositive a
⊢ (a ^ 2⁻¹) ^ x = a ^ (x / 2)

Tactic:
rpow_rpow _ _ _ (by simp),

Goal state after:
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ
h : IsUnit a
ha : 0 ≤ a
this : IsStrictlyPositive a
⊢ a ^ (2⁻¹ * x) = a ^ (x / 2)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: 𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : ContinuousStar A
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
x : ↑{a | p a ∧ spectrum 𝕜 a ⊆ s}
⊢ {a | p a ∧ spectrum 𝕜 a ⊆ s}.domRestrict (cfc f) x =
    (cfcHom ⋯)
      ({ toFun := s.domRestrict f, continuous_toFun := ⋯ }.comp { toFun := Subtype.map id ⋯, continuous_toFun := ⋯ })

Tactic:
Set.domRestrict_apply,

Goal state after:
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : ContinuousStar A
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
x : ↑{a | p a ∧ spectrum 𝕜 a ⊆ s}
⊢ cfc f ↑x =
    (cfcHom ⋯)
      ({ toFun := s.domRestrict f, continuous_toFun := ⋯ }.comp { toFun := Subtype.map id ⋯, continuous_toFun := ⋯ })
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : StarOrderedRing A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : IsStrictlyPositive a
⊢ IsStrictlyPositive a⁻¹ʳ

Tactic:
by
  rw [CFC.inverse_eq_rpow_neg_one]
  cfc_tac

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ IsClosed {a | 0 ≤ a}

Tactic:
suffices IsClosed {a : A⁺¹ | 0 ≤ a} by
    rw [Unitization.isometry_inr (𝕜 := ℂ) |>.isClosedEmbedding.isClosed_iff_image_isClosed]
    convert! this.inter <| (Unitization.isometry_inr (𝕜 := ℂ)).isClosedEmbedding.isClosed_range
    ext a
    simp only [Set.mem_image, Set.mem_ofPred_eq, Set.mem_inter_iff, Set.mem_range,
      ← exists_and_left]
    congr! 2 with x
    exact and_congr_left fun h ↦ by simp [← h]
  simp only [nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts,
    and_congr_right (SpectrumRestricts.nnreal_iff_nnnorm · le_rfl), Set.ofPred_and]
  refine isClosed_eq ?_ ?_ |>.inter <| isClosed_le ?_ ?_
  all_goals fun_prop

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a e : A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
⊢ a * e = a

Tactic:
suffices ∀ a e : A⁺¹, IsStarProjection e → 0 ≤ a → a ≤ e → a * e = a from
    mod_cast this a e he.inr ha.inr (inr_le_iff a e |>.mpr hae)

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a e : A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
⊢ ∀ (a e : Unitization ℂ A), IsStarProjection e → 0 ≤ a → a ≤ e → a * e = a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ e✝ : A
he✝ : IsStarProjection e✝
ha✝ : 0 ≤ a✝
hae✝ : a✝ ≤ e✝
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
⊢ ‖star (1 - e) * a * (1 - e)‖ = 0

Tactic:
norm_eq_zero

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ e✝ : A
he✝ : IsStarProjection e✝
ha✝ : 0 ≤ a✝
hae✝ : a✝ ≤ e✝
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
⊢ star (1 - e) * a * (1 - e) = 0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 1 ≤ a
ha' : 0 ≤ a
n m : ℕ
⊢ n ≤ m → (fun x ↦ a ^ x) n ≤ (fun x ↦ a ^ x) m

Tactic:
hnm

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 1 ≤ a
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
⊢ (fun x ↦ a ^ x) n ≤ (fun x ↦ a ^ x) m
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
n m : ℕ
⊢ n ≤ m → (fun x ↦ a ^ x) m ≤ (fun x ↦ a ^ x) n

Tactic:
hnm

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
n m : ℕ
hnm : n ≤ m
⊢ (fun x ↦ a ^ x) m ≤ (fun x ↦ a ^ x) n
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
⊢ cfcₙ (fun x ↦ 1 - (1 + x)⁻¹) a = cfcₙ (fun x ↦ 1 - (1 + x)⁻¹) a

Tactic:
cfcₙ_nnreal_eq_real _ _ ha

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
⊢ cfcₙ (fun x ↦ 1 - (1 + x)⁻¹) a = cfcₙ (fun x ↦ ↑(1 - (1 + x.toNNReal)⁻¹)) a
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x ↦ x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
| a

Tactic:
← cfcₙ_id ℝ≥0 a

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x ↦ x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
| cfcₙ id a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: case neg
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : Nontrivial R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)
hF0 : ∀ᶠ (x : X) in l, F x 0 = 0
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
hf0 : f 0 = 0
ha : ¬p a
⊢ Tendsto (fun x ↦ cfcₙ (F x) a) l (𝓝 (cfcₙ f a))

Tactic:
· simpa [cfcₙ_apply_of_not_predicate a ha] using tendsto_const_nhds

Goal state after:
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: case e_f.refine_2
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
i : n
⊢ ‖v i‖₊ ≤ Finset.univ.sup fun b ↦ ‖diagonal v i b‖₊

Tactic:
· refine Eq.trans_le ?_ (Finset.le_sup (Finset.mem_univ i))
    rw [diagonal_apply_eq]

Goal state after:
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i ↦ (i, i), inj' := ⋯ } Finset.univ
i : n × n
_hi : i ∈ Finset.univ
his : i ∉ s
this : i.1 ≠ i.2
⊢ ‖diagonal v i.1 i.2‖₊ ^ 2 = 0

Tactic:
diagonal_apply_ne _ this,

Goal state after:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i ↦ (i, i), inj' := ⋯ } Finset.univ
i : n × n
_hi : i ∈ Finset.univ
his : i ∉ s
this : i.1 ≠ i.2
⊢ ‖0‖₊ ^ 2 = 0
Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap

Goal state before:
pp: A₁ : Type u_1
A₂ : Type u_2
inst✝⁵ : NonUnitalCStarAlgebra A₁
inst✝⁴ : NonUnitalCStarAlgebra A₂
inst✝³ : PartialOrder A₁
inst✝² : StarOrderedRing A₁
inst✝¹ : PartialOrder A₂
inst✝ : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
h_nonneg : ∃ C, ∀ (a : A₁), 0 ≤ a → ‖f a‖ ≤ ↑C * ‖a‖
⊢ ∃ C, ∀ (a : A₁), ‖f a‖ ≤ ↑C * ‖a‖

Tactic:
obtain ⟨C, hmain⟩ := h_nonneg
    refine ⟨4 * C, fun x ↦ ?_⟩
    obtain ⟨y, hy_nonneg, hy_norm, hy⟩ := CStarAlgebra.exists_sum_four_nonneg x
    conv_lhs => rw [hy]
    simp only [map_sum, map_smul]
    apply norm_sum_le _ _ |>.trans
    simp only [norm_smul, norm_pow, norm_I, one_pow, one_mul]
    apply Finset.sum_le_sum (g := fun _ ↦ C * ‖x‖) (fun i _ ↦ ?_) |>.trans <| by simp [mul_assoc]
    apply hmain _ (hy_nonneg i) |>.trans
    gcongr
    exact hy_norm i

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: 𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : IsScalarTower 𝕜 A A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : ContinuousStar A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
hf0 : f 0 = 0
hs0 : 0 ∈ s
x : ↑{a | p a ∧ quasispectrum 𝕜 a ⊆ s}
⊢ {a | p a ∧ quasispectrum 𝕜 a ⊆ s}.domRestrict (fun x ↦ cfcₙ f x) x =
    (cfcₙHom ⋯)
      ({ toFun := s.domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 }.comp
        { toFun := Subtype.map id ⋯, continuous_toFun := ⋯, map_zero' := ⋯ })

Tactic:
Set.domRestrict_apply,

Goal state after:
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : IsScalarTower 𝕜 A A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : ContinuousStar A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
hf0 : f 0 = 0
hs0 : 0 ∈ s
x : ↑{a | p a ∧ quasispectrum 𝕜 a ⊆ s}
⊢ cfcₙ f ↑x =
    (cfcₙHom ⋯)
      ({ toFun := s.domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 }.comp
        { toFun := Subtype.map id ⋯, continuous_toFun := ⋯, map_zero' := ⋯ })
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Field R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
h : quasispectrum R a ⊆ {0, 1}
⊢ IsIdempotentElem a

Tactic:
IsIdempotentElem,

Goal state after:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Field R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
h : quasispectrum R a ⊆ {0, 1}
⊢ a * a = a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart

Goal state before:
pp: A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : Module ℂ A
inst✝³ : IsScalarTower ℂ A A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : StarModule ℂ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
this : cfcₙ (fun z ↦ ↑z.re + I * ↑z.im) a = ↑(ℜ a) + I • ↑(ℑ a)
⊢ cfcₙ (fun x ↦ ↑x.im) a = ↑(ℑ a)

Tactic:
rw [cfcₙ_add .., cfcₙ_const_mul .., cfcₙ_re_id a] at this

Goal state after:
A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : Module ℂ A
inst✝³ : IsScalarTower ℂ A A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : StarModule ℂ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
this : ↑(ℜ a) + I • cfcₙ (fun z ↦ ↑z.im) a = ↑(ℜ a) + I • ↑(ℑ a)
⊢ cfcₙ (fun x ↦ ↑x.im) a = ↑(ℑ a)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Goal state before:
pp: A : Type u_1
inst✝¹¹ : Ring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra ℝ A
inst✝⁸ : TopologicalSpace A
inst✝⁷ : IsTopologicalRing A
inst✝⁶ : T2Space A
inst✝⁵ : PartialOrder A
inst✝⁴ : NonnegSpectrumClass ℝ A
inst✝³ : StarOrderedRing A
inst✝² : ContinuousStar A
inst✝¹ : StarModule ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ (Set.range fun x ↦ cfc x a) ⊆ {x | x ∈ StarAlgebra.elemental ℝ a ∧ 0 ≤ x}

Tactic:
by
  grw [range_cfc_nnreal_eq_image_cfc_real a ha, Set.ofPred_and, SetLike.setOfPred_mem_eq,
    ← range_cfc_subset ℝ ha.isSelfAdjoint, Set.inter_comm, ← Set.image_preimage_eq_inter_range]
  exact Set.image_mono fun _ ↦ cfc_nonneg

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : RCLike 𝕜
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : Module 𝕜 A
inst✝⁷ : IsScalarTower 𝕜 A A
inst✝⁶ : SMulCommClass 𝕜 A A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousConstSMul 𝕜 A
inst✝³ : StarModule 𝕜 A
inst✝² : IsTopologicalRing A
inst✝¹ : ContinuousStar A
inst✝ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
⊢ NonUnitalStarAlgHom.range (cfcₙHom ha) ≤ elemental 𝕜 a

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

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Completion

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : Completion E
a : E
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [norm_coe, inner_coe, inner_self_eq_norm_sq]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Hom

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CStarAlgebra A
inst✝³ : CStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective ⇑φ
h_spec : spectrum ℝ ((StarAlgHom.restrictScalars ℝ ↑φ) a) ⊆ spectrum ℝ a
x : ℝ
hx : x ∈ spectrum ℝ a
hx' : x ∉ spectrum ℝ (φ a)
f : C(ℝ, ℝ)
h_eqOn : Set.EqOn (⇑f) 0 (spectrum ℝ (φ a))
h_eqOn_x : Set.EqOn (⇑f) 1 {x}
this : φ (cfc (⇑f) a) = 0
⊢ False

Tactic:
rw [map_eq_zero_iff φ hφ, ← cfc_zero ℝ a, cfc_eq_cfc_iff_eqOn] at this
    exact zero_ne_one <| calc
      0 = f x := (this hx).symm
      _ = 1 := h_eqOn_x <| Set.mem_singleton x

Goal state after: