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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : ↑‖a‖₊ ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ IsSelfAdjoint a

Tactic:
apply IsSelfAdjoint.spectrumRestricts

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : ↑‖a‖₊ ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ IsSelfAdjoint a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x ↦ ContinuousMap.realToNNReal x
⊢ SpectrumRestricts (c * star c) ⇑ContinuousMap.realToNNReal

Tactic:
rw [eq_sub_iff_add_eq'.mpr <| star_mul_self_add_self_mul_star c, sub_eq_add_neg, ← sq, ← sq]

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x ↦ ContinuousMap.realToNNReal x
⊢ SpectrumRestricts (2 • (↑(ℜ c) ^ 2 + ↑(ℑ c) ^ 2) + -(star c * c)) ⇑ContinuousMap.realToNNReal
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x y z : A
hxy : IsSelfAdjoint ↑(y - x) ∧ SpectrumRestricts ↑(y - x) ⇑ContinuousMap.realToNNReal
hyz : IsSelfAdjoint ↑(z - y) ∧ SpectrumRestricts ↑(z - y) ⇑ContinuousMap.realToNNReal
⊢ IsSelfAdjoint ↑(z - x) ∧ SpectrumRestricts ↑(z - x) ⇑ContinuousMap.realToNNReal

Tactic:
exact ⟨by simpa using hyz.1.add hxy.1, by simpa using hyz.2.nnreal_add hyz.1 hxy.1 hxy.2⟩

Goal state after:
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✝¹ : T2Space A
inst✝ : IsSemitopologicalRing A
a : A
y : ℝ≥0
ha : 0 ≤ a
⊢ cfcₙ (fun x ↦ x.nnrpow y) a = cfcₙ (fun x ↦ x ^ ↑y) a

Tactic:
cfcₙ_nnreal_eq_real ..

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✝¹ : T2Space A
inst✝ : IsSemitopologicalRing A
a : A
y : ℝ≥0
ha : 0 ≤ a
⊢ cfcₙ (fun x ↦ ↑(x.toNNReal.nnrpow y)) a = cfcₙ (fun x ↦ x ^ ↑y) 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
a : A
ha : 0 ≤ a
this : cfcₙ (fun x ↦ √x * √x) a = cfcₙ (fun x ↦ x) a
⊢ sqrt a = cfcₙ Real.sqrt a

Tactic:
cfcₙ_mul ..,

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
a : A
ha : 0 ≤ a
this : cfcₙ Real.sqrt a * cfcₙ Real.sqrt a = cfcₙ (fun x ↦ x) a
⊢ sqrt a = cfcₙ Real.sqrt a
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 : ℝ
hx : x ≠ 0
ha : IsStrictlyPositive a
⊢ (a ^ x)⁻¹ʳ = a ^ (-x)

Tactic:
have : a ^ (-x) = (a ^ x) ^ (-1 : ℝ) := by
    rw [rpow_rpow (hx := hx) (ha := by grind)]
    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 : ℝ
hx : x ≠ 0
ha : IsStrictlyPositive a
this : a ^ (-x) = (a ^ x) ^ (-1)
⊢ (a ^ x)⁻¹ʳ = a ^ (-x)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
𝕜 : 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
inst✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : s ∈ 𝓝ˢ (⋃ x ∈ t, spectrum 𝕜 (a x))
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hs' : ∀ i ∈ t, s ∈ 𝓝ˢ (spectrum 𝕜 (a i))
S : ↑t → Set 𝕜
hS₁ : ∀ (x : ↑t), IsCompact (S x)
hS₂ : ∀ (x : ↑t), ∀ᶠ (x' : A) in 𝓝 (a ↑x), spectrum 𝕜 x' ⊆ S x
hS₃ : ∀ (x : ↑t), S x ⊆ s
⊢ ∀ x ∈ t, IsCompact (if hx : x ∈ t then S ⟨x, hx⟩ else ∅)

Tactic:
simpa +contextual using hS₁

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
inst✝ : Nontrivial A
a : A
ha : 0 ≤ a
this : IsSelfAdjoint a
⊢ (spectrum ℝ a).Nonempty

Tactic:
· exact this.spectrumRestricts.image ▸ (spectrum.nonempty a).image _

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

Goal state before:
pp: case pos
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
ha : ¬IsStrictlyPositive a
ha' : ¬IsUnit (sqrt a)
H : ¬0 ≤ a
hunit : IsUnit a
⊢ sqrt a⁻¹ʳ = 0

Tactic:
have h₂ : ¬0 ≤ inverse a := by grind [CFC.ringInverse_nonneg_iff_nonneg_of_isUnit]
        rw [sqrt_of_not_nonneg h₂]

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

Goal state before:
pp: X : Type u_1
𝕜 : 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
inst✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
hs : s ∈ 𝓝ˢ (⋃ x, spectrum 𝕜 (a x))
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha' : ∀ (x : X), p (a x)
hf : ContinuousOn f s
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ cfc f (a x)

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

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
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : ¬f 0 = 0
⊢ cfcₙ f = fun x ↦ 0

Tactic:
ext x

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : ¬f 0 = 0
x : A
⊢ cfcₙ f x = 0
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
t : Set X
hs : s ∈ 𝓝ˢ (⋃ x ∈ t, spectrum ℝ≥0 (a x))
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hs' : ∀ i ∈ t, s ∈ 𝓝ˢ (spectrum ℝ≥0 (a i))
S : ↑t → Set ℝ≥0
hS₁ : ∀ (x : ↑t), IsCompact (S x)
hS₂ : ∀ (x : ↑t), ∀ᶠ (x' : A) in 𝓝 (a ↑x), spectrum ℝ≥0 x' ⊆ S x
hS₃ : ∀ (x : ↑t), S x ⊆ s
⊢ ∀ x ∈ t, IsCompact (if hx : x ∈ t then S ⟨x, hx⟩ else ∅)

Tactic:
simpa +contextual using hS₁

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

Goal state before:
pp: A : Type u_1
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → Module ℂ (E i)
inst✝¹ : (i : ι) → SMul A (E i)
inst✝ : (i : ι) → CStarModule A (E i)
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
⊢ ‖x‖ ^ 2 ≤ (∑ i, ‖x i‖) ^ 2

Tactic:
calc ‖x‖ ^ 2 ≤ ∑ i, ‖⟪x i, x i⟫_A‖ := pi_norm_sq x ▸ norm_sum_le _ _
    _ = ∑ i, ‖x i‖ ^ 2 := by simp only [norm_sq_eq A]
    _ ≤ (∑ i, ‖x i‖) ^ 2 := sum_sq_le_sq_sum_of_nonneg (fun _ _ ↦ norm_nonneg _)

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
c : Unitization ℂ A
hc : 0 ≤ c
x : ℝ≥0
x✝ : x ∈ σ ℝ≥0 c
⊢ id (1 + x) ≠ 0

Tactic:
dsimp only [id]; positivity

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✝ : TopologicalSpace X
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum ℝ≥0 (a x) ⊆ s
hf : ContinuousOn f s
ha' : ∀ (x : X), 0 ≤ a x
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ cfc f (a x)

Tactic:
by
  rw [← continuousOn_univ] at ha_cont ⊢
  exact ha_cont.cfc_nnreal' hs f (fun x _ ↦ ha x) (fun x _ ↦ ha' x)

Goal state after:
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)⁻¹
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) ({x | 0 ≤ x} ∩ Metric.ball 0 1)

Tactic:
let g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹

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)⁻¹
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) ({x | 0 ≤ x} ∩ Metric.ball 0 1)
Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions

Goal state before:
pp: A : Type u_1
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℂ E
⊢ ∀ {x y z : E}, ⟪x, y + z⟫_ℂ = ⟪x, y⟫_ℂ + ⟪x, z⟫_ℂ

Tactic:
by simp [_root_.inner_add_right]

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

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖A‖ = ↑(Finset.univ.sup fun i ↦ ∑ j, ‖A i j‖₊)

Tactic:
change ‖fun i => toLp 1 (A i)‖ = _

Goal state after:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖fun i ↦ toLp 1 (A i)‖ = ↑(Finset.univ.sup fun i ↦ ∑ j, ‖A i j‖₊)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
𝕜 : 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
inst✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : s ∈ 𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ i ∈ t, s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))
S : ↑t → Set 𝕜
hS₁ : ∀ (x : ↑t), IsCompact (S x)
hS₂ : ∀ (x : ↑t), ∀ᶠ (x' : A) in 𝓝 (a ↑x), quasispectrum 𝕜 x' ⊆ S x
hS₃ : ∀ (x : ↑t), S x ⊆ s
⊢ ∀ x ∈ t, IsCompact (if hx : x ∈ t then S ⟨x, hx⟩ else ∅)

Tactic:
simpa +contextual using hS₁

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁴ : MeasurableSpace X
μ : Measure X
inst✝³ : TopologicalSpace Y
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : CompactSpace Y
inst✝ : Zero Y
f : X → C(Y, E)₀
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖(f x) y‖ ≤ bound x
⊢ 0 ≤ᵐ[μ] bound

Tactic:
filter_upwards [bound_ge] with x bound_x using le_trans (norm_nonneg _) (bound_x 0)

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

Goal state before:
pp: case pos
A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module ℝ A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : IsTopologicalRing A
inst✝³ : T2Space A
inst✝² : PartialOrder A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : StarOrderedRing A
a b : A
hb : Commute a b
f : ℝ≥0 → ℝ≥0
ha : 0 ≤ a
⊢ Commute (cfcₙ f a) b

Tactic:
cfcₙ_nnreal_eq_real ..

Goal state after:
case pos
A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module ℝ A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : IsTopologicalRing A
inst✝³ : T2Space A
inst✝² : PartialOrder A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : StarOrderedRing A
a b : A
hb : Commute a b
f : ℝ≥0 → ℝ≥0
ha : 0 ≤ a
⊢ Commute (cfcₙ (fun x ↦ ↑(f x.toNNReal)) a) b
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
A : Type u_2
inst✝¹³ : NonUnitalNormedRing A
inst✝¹² : StarRing A
inst✝¹¹ : NormedSpace ℝ A
inst✝¹⁰ : IsScalarTower ℝ A A
inst✝⁹ : SMulCommClass ℝ A A
inst✝⁸ : ContinuousStar A
inst✝⁷ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
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
t : Set X
hs : s ∈ 𝓝ˢ (⋃ x ∈ t, quasispectrum ℝ≥0 (a x))
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ i ∈ t, s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (a i))
S : ↑t → Set ℝ≥0
hS₁ : ∀ (x : ↑t), IsCompact (S x)
hS₂ : ∀ (x : ↑t), ∀ᶠ (x' : A) in 𝓝 (a ↑x), quasispectrum ℝ≥0 x' ⊆ S x
hS₃ : ∀ (x : ↑t), S x ⊆ s
⊢ ∀ x ∈ t, IsCompact (if hx : x ∈ t then S ⟨x, hx⟩ else ∅)

Tactic:
simpa +contextual using hS₁

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
⊢ (Set.range fun x ↦ cfcₙ x a) ⊆ ↑(elemental 𝕜 a)

Tactic:
by
  grw [range_cfcₙ_eq_range_cfcₙHom 𝕜 ha, range_cfcₙHom_le 𝕜 ha]

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
ha : IsStarNormal a
⊢ spectrum ℝ ↑(ℜ a) = re '' spectrum ℂ a

Tactic:
by
  simp [← (ℜ a).2.spectrumRestricts.image, spectrum_realPart a, Set.image_image]

Goal state after:
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module 𝕜 (M i)
s : (i : ι) → Set (M i)
⊢ extremePoints 𝕜 (univ.pi s) = univ.pi fun i ↦ extremePoints 𝕜 (s i)

Tactic:
ext x

Goal state after:
𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module 𝕜 (M i)
s : (i : ι) → Set (M i)
x : (i : ι) → M i
⊢ x ∈ extremePoints 𝕜 (univ.pi s) ↔ x ∈ univ.pi fun i ↦ extremePoints 𝕜 (s i)
Module: Mathlib.Analysis.InnerProductSpace.Completion

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ ((innerₛₗ 𝕜) 0).toAddMonoidHom = 0

Tactic:
ext x

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ ((innerₛₗ 𝕜) 0).toAddMonoidHom x = 0 x
Module: Mathlib.Analysis.Complex.Circle

Goal state before:
pp: h : exp Real.pi = 1
heq : -1 = 1
⊢ False

Tactic:
norm_num at heq

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Y'
eX eX' : OpenPartialHomeomorph X X'
eY eY' : OpenPartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
x : X
y : Y
this✝² : Nonempty X
this✝¹ : Nonempty X'
this✝ : Nonempty Y
this : Nonempty Y'
⊢ (∀ (x : X × Y), (↑eX x.1, ↑eY x.2) = (↑eX' x.1, ↑eY' x.2)) ∧
      (∀ (x : X' × Y'), (↑eX.symm x.1, ↑eY.symm x.2) = (↑eX'.symm x.1, ↑eY'.symm x.2)) ∧
        eX.source ×ˢ eY.source = eX'.source ×ˢ eY'.source ↔
    ((∀ (x : X), ↑eX x = ↑eX' x) ∧ (∀ (x : X'), ↑eX.symm x = ↑eX'.symm x) ∧ eX.source = eX'.source) ∧
      (∀ (x : Y), ↑eY x = ↑eY' x) ∧ (∀ (x : Y'), ↑eY.symm x = ↑eY'.symm x) ∧ eY.source = eY'.source

Tactic:
Prod.ext_iff,

Goal state after:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Y'
eX eX' : OpenPartialHomeomorph X X'
eY eY' : OpenPartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
x : X
y : Y
this✝² : Nonempty X
this✝¹ : Nonempty X'
this✝ : Nonempty Y
this : Nonempty Y'
⊢ (∀ (x : X × Y), ↑eX x.1 = ↑eX' x.1 ∧ ↑eY x.2 = ↑eY' x.2) ∧
      (∀ (x : X' × Y'), ↑eX.symm x.1 = ↑eX'.symm x.1 ∧ ↑eY.symm x.2 = ↑eY'.symm x.2) ∧
        eX.source ×ˢ eY.source = eX'.source ×ˢ eY'.source ↔
    ((∀ (x : X), ↑eX x = ↑eX' x) ∧ (∀ (x : X'), ↑eX.symm x = ↑eX'.symm x) ∧ eX.source = eX'.source) ∧
      (∀ (x : Y), ↑eY x = ↑eY' x) ∧ (∀ (x : Y'), ↑eY.symm x = ↑eY'.symm x) ∧ eY.source = eY'.source
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x : Z
ex : x ∈ e.source
⊢ ↑e.symm (proj x, (↑e x).2) = x

Tactic:
← e.coe_fst ex,

Goal state after:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x : Z
ex : x ∈ e.source
⊢ ↑e.symm ((↑e x).1, (↑e x).2) = x
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
⊢ ∀ ⦃x : B × F⦄,
    x ∈ (Z.baseSet i ∩ Z.baseSet j) ×ˢ univ →
      ((x.1, Z.coordChange i j x.1 x.2).1,
          Z.coordChange j i (x.1, Z.coordChange i j x.1 x.2).1 (x.1, Z.coordChange i j x.1 x.2).2) =
        x

Tactic:
by
    rintro ⟨x, v⟩ hx
    simp only [prodMk_mem_set_prod_eq, mem_inter_iff, and_true, mem_univ] at hx
    dsimp only
    rw [coordChange_comp, Z.coordChange_self]
    exacts [hx.1, ⟨⟨hx.1, hx.2⟩, hx.1⟩]

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: case left
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
⊢ ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source = (Z.trivChange i j).source

Tactic:
ext x

Goal state after:
case left
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B × F
⊢ x ∈ ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source ↔ x ∈ (Z.trivChange i j).source
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
x : Z
ex : x ∈ e.source
⊢ map proj (𝓝 x) = 𝓝 (proj x)

Tactic:
← e.coe_fst ex,

Goal state after:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
x : Z
ex : x ∈ e.source
⊢ map proj (𝓝 x) = 𝓝 (↑e x).1
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
Z' : Type u_5
inst✝ : TopologicalSpace Z'
h : Z' ≃ₜ Z
p : Z'
hp✝ : p ∈ (h.transOpenPartialHomeomorph e.toOpenPartialHomeomorph).source
hp : h p ∈ e.source
⊢ (↑(h.transOpenPartialHomeomorph e.toOpenPartialHomeomorph) p).1 = (proj ∘ ⇑h) p

Tactic:
simp [hp]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
⊢ ‖u - 1‖ ^ 2 = 2 * (1 - x)

Tactic:
by
  obtain (_ | _) := subsingleton_or_nontrivial A
  · exfalso; apply hz.nonempty.of_image.ne_empty; simp
  rw [← cfc_id' ℂ u, ← cfc_one ℂ u, ← cfc_sub ..]
  have h_eqOn : (spectrum ℂ u).EqOn (fun z ↦ ‖z - 1‖ ^ 2) (fun z ↦ 2 * (1 - z.re)) :=
    Complex.norm_sub_one_sq_eqOn_sphere.mono <| spectrum.subset_circle_of_unitary (𝕜 := ℂ) hu
  have h₂ : IsGreatest ((fun z ↦ 2 * (1 - z.re)) '' (spectrum ℂ u)) (2 * (1 - x)) := by
    have : Antitone (fun y : ℝ ↦ 2 * (1 - y)) := by intro _ _ _; simp only; gcongr
    simpa [Set.image_image] using this.map_isLeast hz
  have h₃ : IsGreatest ((‖· - 1‖ ^ 2) '' spectrum ℂ u) (‖cfc (· - 1 : ℂ → ℂ) u‖ ^ 2) := by
    have := pow_left_monotoneOn (n := 2) |>.mono (s₂ := ((‖· - 1‖) '' spectrum ℂ u)) (by simp)
    simpa [Set.image_image] using this.map_isGreatest (IsGreatest.norm_cfc (fun z : ℂ ↦ z - 1) u)
  exact h₃.unique (h_eqOn.image_eq ▸ h₂)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case h
x✝ : ℝ
⊢ (-↑x✝).toCircle = (↑x✝).toCircle⁻¹

Tactic:
← coe_neg,

Goal state after:
case h
x✝ : ℝ
⊢ (↑(-x✝)).toCircle = (↑x✝).toCircle⁻¹