mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : ProperSpace 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
⊢ UpperHemicontinuous (spectrum 𝕜)

Tactic:
rw [upperHemicontinuous_iff]
  refine fun a₀ ↦ .of_sequences
    (isCompact_closedBall 0 ((‖a₀‖ + 1) * ‖(1 : A)‖)).isSeqCompact ?_ <|
    fun a ha x hx_mem x₀ hx ↦ ?_
  /- We must show that `spectrum 𝕜 (a n)` is eventually contained in some fixed compact set
  (we've chosen `closedBall 0 ((‖a₀‖ + 1) * ‖(1 : A)‖)`). This follows since the spectrum of any
  `b` is bounded `‖b‖ * ‖1‖` and `a` converges to `a₀`.  -/
  · filter_upwards [Metric.closedBall_mem_nhds a₀ zero_lt_one] with a ha
    apply spectrum.subset_closedBall_norm_mul a |>.trans <| Metric.closedBall_subset_closedBall ?_
    gcongr
    apply norm_le_norm_add_norm_sub' a a₀ |>.trans
    gcongr
    simpa [dist_eq_norm] using ha
  /- Finally, `x₀ ∈ spectrum 𝕜 a₀` since `algebraMap 𝕜 A x₀ - a₀` is not invertible, being itself
  the limit of the non-invertible elements `algebraMap 𝕜 A (x n) - (a n)`. -/
  · exact nonunits.isClosed.mem_of_tendsto
      (continuous_algebraMap 𝕜 A |>.tendsto x₀ |>.comp hx |>.sub ha) <| .of_forall hx_mem

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : ProperSpace 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : CompleteSpace A
a : A
⊢ quasispectrum 𝕜 a = (spectrum 𝕜 ∘ fun x ↦ toLp 1 ↑x) a

Tactic:
rw [Unitization.quasispectrum_eq_spectrum_inr,
    ← AlgEquiv.spectrum_eq (unitizationAlgEquiv 𝕜 (𝕜 := 𝕜) (A := A) |>.symm)]

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : ProperSpace 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : CompleteSpace A
a : A
⊢ spectrum 𝕜 ((unitizationAlgEquiv 𝕜).symm ↑a) = (spectrum 𝕜 ∘ fun x ↦ toLp 1 ↑x) a
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
⊢ spectralRadius ℂ a ^ 2 = ↑‖a‖₊ ^ 2

Tactic:
have heq :
    (fun n : ℕ => (‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ (1 / n : ℝ)) =
      (fun x => x ^ 2) ∘ fun n : ℕ => (‖a ^ n‖₊ : ℝ≥0∞) ^ (1 / n : ℝ) := by
    funext n
    rw [Function.comp_apply, ← rpow_natCast, ← rpow_mul, mul_comm, rpow_mul, rpow_natCast, ←
      coe_pow, sq, ← nnnorm_star_mul_self, Commute.mul_pow (star_comm_self' a), star_pow]

Goal state after:
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
heq : (fun n ↦ ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) = (fun x ↦ x ^ 2) ∘ fun n ↦ ↑‖a ^ n‖₊ ^ (1 / ↑n)
⊢ spectralRadius ℂ a ^ 2 = ↑‖a‖₊ ^ 2
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
⊢ z = ↑z.re

Tactic:
by
  let +nondep : NormedAlgebra ℚ A := .restrictScalars ℚ ℂ A
  have hu := exp_mem_unitary_of_mem_skewAdjoint (ha.smul_mem_skewAdjoint conj_I)
  let Iu := Units.mk0 I I_ne_zero
  have : NormedSpace.exp (I • z) ∈ spectrum ℂ (NormedSpace.exp (I • a)) := by
    simpa only [Units.smul_def, Units.val_mk0] using!
      spectrum.exp_mem_exp (Iu • a) (smul_mem_smul_iff.mpr hz)
  exact Complex.ext (ofReal_re _) <| by
    simpa only [← Complex.exp_eq_exp_ℂ, mem_sphere_zero_iff_norm, norm_exp, Real.exp_eq_one_iff,
      smul_eq_mul, I_mul, neg_eq_zero] using!
      spectrum.subset_circle_of_unitary hu this

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K : Set α
hK : IsCompact K
⊢ IsCompact {L | ↑L ⊆ K}

Tactic:
rw [isEmbedding_coe.isCompact_iff]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
K : Set α
hK : IsCompact K
⊢ IsCompact (SetLike.coe '' {L | ↑L ⊆ K})
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝³] U
hKu₁ : ↑K ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, (↑K ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : ↑K ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : Set α → Set α
hM : ∀ U ∈ u, IsCompact (M U)
hML : ∀ U ∈ u, M U ⊆ L
hMU : ∀ U ∈ u, M U ⊆ U
hMK : ∀ U ∈ u, (↑K ∩ interior (M U)).Nonempty
⊢ IsCompact {K' | ↑K' ⊆ L ∧ ∀ U ∈ u, (↑K' ∩ M U).Nonempty}

Tactic:
rw [isEmbedding_coe.isCompact_iff]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝³] U
hKu₁ : ↑K ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, (↑K ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : ↑K ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : Set α → Set α
hM : ∀ U ∈ u, IsCompact (M U)
hML : ∀ U ∈ u, M U ⊆ L
hMU : ∀ U ∈ u, M U ⊆ U
hMK : ∀ U ∈ u, (↑K ∩ interior (M U)).Nonempty
⊢ IsCompact (SetLike.coe '' {K' | ↑K' ⊆ L ∧ ∀ U ∈ u, (↑K' ∩ M U).Nonempty})
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a✝ : A
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), NormedSpace.exp (x • a✝) * NormedSpace.exp (-x • star a✝) ∈ unitary A
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-x • a✝) * NormedSpace.exp (x • star a✝) =
      NormedSpace.exp (x • star a✝) * NormedSpace.exp (-x • a✝)
a b c : A
y : ℝ
⊢ deriv (fun x ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
    NormedSpace.exp (y • a) * a * c * NormedSpace.exp (y • b) +
      NormedSpace.exp (y • a) * c * b * NormedSpace.exp (y • b)

Tactic:
mul_assoc _ b

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a✝ : A
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
this : IsAddTorsionFree A
ha : ∀ (x : ℝ), NormedSpace.exp (x • a✝) * NormedSpace.exp (-x • star a✝) ∈ unitary A
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-x • a✝) * NormedSpace.exp (x • star a✝) =
      NormedSpace.exp (x • star a✝) * NormedSpace.exp (-x • a✝)
a b c : A
y : ℝ
⊢ deriv (fun x ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
    NormedSpace.exp (y • a) * a * c * NormedSpace.exp (y • b) +
      NormedSpace.exp (y • a) * c * (b * NormedSpace.exp (y • b))
Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : ContinuousSMul ℝ E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
⊢ 0 ∈ (t.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r ∧
    IsOpen[inst✝⁷] ((t.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r) ∧
      AbsConvex 𝕜 ((t.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r)

Tactic:
rw [Seminorm.ball_finset_sup_eq_iInter _ _ _ hr]

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : ContinuousSMul ℝ E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
⊢ 0 ∈ ⋂ i ∈ t, (gaugeSeminormFamily 𝕜 E i).ball 0 r ∧
    IsOpen[inst✝⁷] (⋂ i ∈ t, (gaugeSeminormFamily 𝕜 E i).ball 0 r) ∧
      AbsConvex 𝕜 (⋂ i ∈ t, (gaugeSeminormFamily 𝕜 E i).ball 0 r)
Module: Mathlib.Analysis.LocallyConvex.WeakDual

Goal state before:
pp: ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
t₂ : Finset ι → TopologicalSpace E := fun s ↦ ⨅ i, induced (⇑(f ↑i)) t𝕜
t₁_group : IsTopologicalAddGroup E
t₂_group : ∀ (s : Finset ι), IsTopologicalAddGroup E
t₁_smul : ContinuousSMul 𝕜 E
⊢ Continuous[t₁, t𝕜] ⇑φ ↔ ∃ s, Continuous[t₂ s, t𝕜] ⇑φ

Tactic:
have t₂_smul (s : Finset ι) : @ContinuousSMul 𝕜 E _ _ (t₂ s) :=
    continuousSMul_iInf fun _ ↦ continuousSMul_induced _

Goal state after:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
t₂ : Finset ι → TopologicalSpace E := fun s ↦ ⨅ i, induced (⇑(f ↑i)) t𝕜
t₁_group : IsTopologicalAddGroup E
t₂_group : ∀ (s : Finset ι), IsTopologicalAddGroup E
t₁_smul : ContinuousSMul 𝕜 E
t₂_smul : ∀ (s : Finset ι), ContinuousSMul 𝕜 E
⊢ Continuous[t₁, t𝕜] ⇑φ ↔ ∃ s, Continuous[t₂ s, t𝕜] ⇑φ
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∈ c.left.U
a✝ : X
hyl : a✝ ∈ c.left.U
hyd : dist (c.left.lim a✝) (c.left.lim x) ≤ (3 / 4) ^ n
⊢ dist (c.lim a✝) (c.lim x) ≤ 3 / 4 * (3 / 4) ^ n

Tactic:
c.lim_eq_midpoint,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∈ c.left.U
a✝ : X
hyl : a✝ ∈ c.left.U
hyd : dist (c.left.lim a✝) (c.left.lim x) ≤ (3 / 4) ^ n
⊢ dist (midpoint ℝ (c.left.lim a✝) (c.right.lim a✝)) (c.lim x) ≤ 3 / 4 * (3 / 4) ^ n
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∈ c.left.U
a✝ : X
hyl : a✝ ∈ c.left.U
hyd : dist (c.left.lim a✝) (c.left.lim x) ≤ (3 / 4) ^ n
⊢ dist (midpoint ℝ (c.left.lim a✝) (c.right.lim a✝)) (c.lim x) ≤ 3 / 4 * (3 / 4) ^ n

Tactic:
c.lim_eq_midpoint,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∈ c.left.U
a✝ : X
hyl : a✝ ∈ c.left.U
hyd : dist (c.left.lim a✝) (c.left.lim x) ≤ (3 / 4) ^ n
⊢ dist (midpoint ℝ (c.left.lim a✝) (c.right.lim a✝)) (midpoint ℝ (c.left.lim x) (c.right.lim x)) ≤ 3 / 4 * (3 / 4) ^ n
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
⊢ ∃ f, (∀ ⦃x : X⦄, x ∈ sᶜ → f x = 0) ∧ f x ≠ 0

Tactic:
obtain ⟨g, hgs, hgx : Set.EqOn g 1 {x}, -⟩ :=
    exists_continuous_zero_one_of_isClosed isClosed_closure isClosed_singleton
      (Set.disjoint_singleton_right.mpr hx)

Goal state after:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
g : C(X, ℝ)
hgs : Set.EqOn (⇑g) 0 (closure sᶜ)
hgx : Set.EqOn (⇑g) 1 {x}
⊢ ∃ f, (∀ ⦃x : X⦄, x ∈ sᶜ → f x = 0) ∧ f x ≠ 0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: case add
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a x y : A
x_mem : 0 ≤ x
y_mem : 0 ≤ y
hx : SpectrumRestricts x ⇑ContinuousMap.realToNNReal
hy : SpectrumRestricts y ⇑ContinuousMap.realToNNReal
⊢ SpectrumRestricts (x + y) ⇑ContinuousMap.realToNNReal

Tactic:
exact hx.nnreal_add (.of_nonneg x_mem) (.of_nonneg y_mem) hy

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : CStarRing A
inst✝⁵ : NormedSpace ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a b : A
hb : IsSelfAdjoint b
ha : 0 ≤ a
⊢ ‖b * a * b‖ = ‖sqrt a * b‖ ^ 2

Tactic:
by
  simpa [hb.star_eq] using norm_star_mul_mul_self_of_nonneg b ha

Goal state after:
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
x : ℝ
ha : IsStrictlyPositive a
⊢ a ^ (-x) * a ^ x = 1

Tactic:
rw [← rpow_add ha.isUnit, neg_add_cancel, rpow_zero a]

Goal state after:
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 : ι) → Ring (C i)
inst✝¹⁰ : (i : ι) → StarRing (C i)
inst✝⁹ : (i : ι) → TopologicalSpace (C i)
inst✝⁸ : ∀ (i : ι), StarOrderedRing (C i)
inst✝⁷ : StarOrderedRing ((i : ι) → C i)
inst✝⁶ : (i : ι) → Algebra ℝ (C i)
inst✝⁵ : ∀ (i : ι), ContinuousFunctionalCalculus ℝ (C i) IsSelfAdjoint
inst✝⁴ : ContinuousFunctionalCalculus ℝ ((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
x : ℝ
hc : ∀ (i : ι), IsUnit (c i)
hc' : ∀ (i : ι), 0 ≤ c i
hc'' : ∀ (i : ι), 0 ∉ spectrum ℝ≥0 (c i)
⊢ cfc (fun x_1 ↦ x_1 ^ x) c = fun i ↦ cfc (fun x_1 ↦ x_1 ^ x) (c i)

Tactic:
exact cfc_map_pi (S := ℝ) _ c

Goal state after:
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
⊢ sqrt a ^ x = a ^ (x / 2)

Tactic:
have : IsStrictlyPositive a := by grind
  rw [sqrt_eq_rpow, div_eq_mul_inv, one_mul,
      rpow_rpow _ _ _ (by simp), inv_mul_eq_div]

Goal state after:
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
⊢ ‖a‖₊ ≤ 1 ↔ a ≤ 1

Tactic:
by
  rw [← NNReal.coe_le_coe]
  exact norm_le_one_iff_of_nonneg a

Goal state after:
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
tfae_1_iff_8 : IsStrictlyPositive a ↔ 0 ≤ a ∧ IsUnit a
tfae_1_iff_9 : IsStrictlyPositive a ↔ IsSelfAdjoint a ∧ ∀ x ∈ spectrum ℝ a, 0 < x
tfae_1_to_2 : IsStrictlyPositive a → IsStrictlyPositive (sqrt a) ∧ a = sqrt a * sqrt a
tfae_2_to_3 : IsStrictlyPositive (sqrt a) ∧ a = sqrt a * sqrt a → IsUnit (sqrt a) ∧ a = sqrt a * sqrt a
tfae_3_to_4 : IsUnit (sqrt a) ∧ a = sqrt a * sqrt a → ∃ b, IsStrictlyPositive b ∧ a = b * b
tfae_4_to_5 : (∃ b, IsStrictlyPositive b ∧ a = b * b) → ∃ b, IsUnit b ∧ IsSelfAdjoint b ∧ a = b * b
tfae_5_to_6 : (∃ b, IsUnit b ∧ IsSelfAdjoint b ∧ a = b * b) → ∃ b, IsUnit b ∧ a = star b * b
tfae_6_to_7 : (∃ b, IsUnit b ∧ a = star b * b) → ∃ b, IsUnit b ∧ a = b * star b
⊢ [IsStrictlyPositive a, IsStrictlyPositive (sqrt a) ∧ a = sqrt a * sqrt a, IsUnit (sqrt a) ∧ a = sqrt a * sqrt a,
      ∃ b, IsStrictlyPositive b ∧ a = b * b, ∃ b, IsUnit b ∧ IsSelfAdjoint b ∧ a = b * b,
      ∃ b, IsUnit b ∧ a = star b * b, ∃ b, IsUnit b ∧ a = b * star b, 0 ≤ a ∧ IsUnit a,
      IsSelfAdjoint a ∧ ∀ x ∈ spectrum ℝ a, 0 < x].TFAE

Tactic:
tfae_have 7 → 8 := fun ⟨b, hb, hab⟩ => ⟨hab ▸ mul_star_self_nonneg _, hab ▸ hb.mul hb.star⟩

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
tfae_1_iff_8 : IsStrictlyPositive a ↔ 0 ≤ a ∧ IsUnit a
tfae_1_iff_9 : IsStrictlyPositive a ↔ IsSelfAdjoint a ∧ ∀ x ∈ spectrum ℝ a, 0 < x
tfae_1_to_2 : IsStrictlyPositive a → IsStrictlyPositive (sqrt a) ∧ a = sqrt a * sqrt a
tfae_2_to_3 : IsStrictlyPositive (sqrt a) ∧ a = sqrt a * sqrt a → IsUnit (sqrt a) ∧ a = sqrt a * sqrt a
tfae_3_to_4 : IsUnit (sqrt a) ∧ a = sqrt a * sqrt a → ∃ b, IsStrictlyPositive b ∧ a = b * b
tfae_4_to_5 : (∃ b, IsStrictlyPositive b ∧ a = b * b) → ∃ b, IsUnit b ∧ IsSelfAdjoint b ∧ a = b * b
tfae_5_to_6 : (∃ b, IsUnit b ∧ IsSelfAdjoint b ∧ a = b * b) → ∃ b, IsUnit b ∧ a = star b * b
tfae_6_to_7 : (∃ b, IsUnit b ∧ a = star b * b) → ∃ b, IsUnit b ∧ a = b * star b
tfae_7_to_8 : (∃ b, IsUnit b ∧ a = b * star b) → 0 ≤ a ∧ IsUnit a
⊢ [IsStrictlyPositive a, IsStrictlyPositive (sqrt a) ∧ a = sqrt a * sqrt a, IsUnit (sqrt a) ∧ a = sqrt a * sqrt a,
      ∃ b, IsStrictlyPositive b ∧ a = b * b, ∃ b, IsUnit b ∧ IsSelfAdjoint b ∧ a = b * b,
      ∃ b, IsUnit b ∧ a = star b * b, ∃ b, IsUnit b ∧ a = b * star b, 0 ≤ a ∧ IsUnit a,
      IsSelfAdjoint a ∧ ∀ x ∈ spectrum ℝ a, 0 < x].TFAE
Module: Mathlib.Analysis.CStarAlgebra.Module.Defs

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
h : x ≠ 0
a : A
⊢ a * (⟪x, x⟫_A * star a) - ‖x‖ ^ 2 •> (a * ⟪y, x⟫_A) -
      (‖x‖ ^ 2 •> (⟪x, y⟫_A * star a) - ‖x‖ ^ 2 •> ‖x‖ ^ 2 •> ⟪y, y⟫_A) =
    a * (⟪x, x⟫_A * star a) - ‖x‖ ^ 2 •> (a * ⟪y, x⟫_A) - ‖x‖ ^ 2 •> (⟪x, y⟫_A * star a) +
      ‖x‖ ^ 2 •> ‖x‖ ^ 2 •> ⟪y, y⟫_A

Tactic:
abel

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

Goal state before:
pp: X : Type u_1
A : Type u_2
inst✝¹¹ : NormedRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : NormedAlgebra ℝ A
inst✝⁸ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁷ : ContinuousStar A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : NonnegSpectrumClass ℝ A
inst✝³ : T2Space A
inst✝² : IsSemitopologicalRing A
inst✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
hs : s ∈ 𝓝ˢ (⋃ x, spectrum ℝ≥0 (a x))
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha' : ∀ (x : X), 0 ≤ a x
hf : ContinuousOn f s
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ cfc f (a x)

Tactic:
rw [← continuousOn_univ] at ha_cont ⊢
  exact ha_cont.cfc_nnreal_of_mem_nhdsSet f (by simpa) (by simpa)

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

Goal state before:
pp: case neg
α : Type u_5
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
h : ¬a = 0
⊢ ‖a‖ • 1 = (algebraMap ℝ α) ‖a‖

Tactic:
Algebra.algebraMap_eq_smul_one

Goal state after:
case neg
α : Type u_5
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
h : ¬a = 0
⊢ ‖a‖ • 1 = ‖a‖ • 1
Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap

Goal state before:
pp: case refine_2
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₂
hcontra : ∀ (C : ℝ≥0), ∃ a, 0 ≤ a ∧ ↑C * ‖a‖ < ‖f a‖
n : ℕ
x : A₁ := Classical.choose ⋯
hx₁ : 0 ≤ x
hx₂ : ↑(2 ^ (2 * n)) * ‖x‖ < ‖f x‖
hx : 0 < ‖x‖
⊢ 2 ^ (2 * n) < ‖f (‖x‖⁻¹ • x)‖

Tactic:
simpa [norm_smul] using (lt_inv_mul_iff₀' hx).mpr hx₂

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

Goal state before:
pp: case h₁
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝¹ m✝ : A
ε : ℝ≥0
hε : 0 < ε
x✝ : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := ⋯
hx₁ : cfc g (ε⁻¹ ^ 2 • m) ≤ x
hg : Continuous g
hg' : ContinuousOn (fun y ↦ (1 + ε⁻¹ ^ 2 • y)⁻¹) (σ ℝ≥0 m)
hx : x ∈ Set.Icc 0 1
hx' : x ∈ Set.Icc (cfc g (ε⁻¹ ^ 2 • m)) 1
this : star m * (1 - cfc g (ε⁻¹ ^ 2 • m)) * m = cfc (fun y ↦ y * (1 + ε⁻¹ ^ 2 • y)⁻¹ * y) m
y : ℝ≥0
hy : y ∈ σ ℝ≥0 m
⊢ y * ε ^ 2 ≤ ε ^ 2

Tactic:
apply mul_le_of_le_one_left'
          have hm' := hm₂.le
          rw [norm_le_one_iff_of_nonneg m hm₁, ← cfc_id' ℝ≥0 m, ← cfc_one (R := ℝ≥0) m,
            cfc_nnreal_le_iff _ _ _ (QuasispectrumRestricts.nnreal_of_nonneg hm₁)] at hm'
          exact hm' y hy

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

Goal state before:
pp: F : Type u_1
A₁ : Type u_2
A₂ : Type u_3
inst✝⁷ : NonUnitalCStarAlgebra A₁
inst✝⁶ : NonUnitalCStarAlgebra A₂
inst✝⁵ : PartialOrder A₁
inst✝⁴ : PartialOrder A₂
inst✝³ : StarOrderedRing A₁
inst✝² : StarOrderedRing A₂
inst✝¹ : FunLike F A₁ A₂
inst✝ : LinearMapClass F ℂ A₁ A₂
h : ∀ (φ : F) (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map ⇑φ
⊢ ∀ (f : F) (x : A₁), 0 ≤ x → 0 ≤ f x

Tactic:
by
  intro φ a ha
  simpa using! map_nonneg (toOneByOne (Fin 1) ℂ A₂).symm <|
    h φ 1 _ <| map_nonneg (toOneByOne (Fin 1) ℂ A₁) ha

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

Goal state before:
pp: case add
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra 𝕜 A
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f g : C(↑(spectrum 𝕜 a), 𝕜)
hf : Commute ((cfcHom ha) f) b
hg : Commute ((cfcHom ha) g) b
⊢ Commute ((cfcHom ha) f + (cfcHom ha) g) b

Tactic:
exact hf.add_left hg

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

Goal state before:
pp: case add
𝕜 : 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✝² : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f g : C(↑(quasispectrum 𝕜 a), 𝕜)₀
hf : Commute ((cfcₙHom ha) f) b
hg : Commute ((cfcₙHom ha) g) b
⊢ Commute ((cfcₙHom ha) f + (cfcₙHom ha) g) b

Tactic:
exact hf.add_left hg

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

Goal state before:
pp: A : Type u_1
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℂ A
inst✝¹ : StarModule ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
hp : IsStarNormal a
this : cfc (fun z ↦ ↑z.re) a + I • cfc (fun z ↦ ↑z.im) a = ↑(ℜ a) + I • ↑(ℑ a)
⊢ cfc (fun x ↦ ↑x.im) a = ↑(ℑ a)

Tactic:
cfc_re_id a

Goal state after:
A : Type u_1
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℂ A
inst✝¹ : StarModule ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
hp : IsStarNormal a
this : ↑(ℜ a) + I • cfc (fun z ↦ ↑z.im) a = ↑(ℜ a) + I • ↑(ℑ a)
⊢ cfc (fun x ↦ ↑x.im) a = ↑(ℑ a)