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
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:
← map_star

Goal state after:
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 (((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a)) (star f))
    (((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a)) f)
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 : cfc 0 a = cfc (fun x ↦ x⁻ ^ 3) a
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x ↦ ContinuousMap.realToNNReal x
h_c_spec₁ : SpectrumRestricts (c * star c) ⇑ContinuousMap.realToNNReal
h_eqOn : Set.EqOn 0 (fun x ↦ x⁻ ^ 3) (spectrum ℝ a)
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Tactic:
exact fun x hx ↦ negPart_eq_zero.mp <| eq_zero_of_pow_eq_zero (h_eqOn hx).symm

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

Goal state before:
pp: A : Type u_1
inst✝⁸ : NormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedAlgebra ℝ A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : ContinuousStar A
inst✝ : CompleteSpace A
r : ℝ
⊢ {0}ᶜ ∈ nhdsSet (⋃ x ∈ {a | IsStrictlyPositive a}, spectrum ℝ≥0 (id x))

Tactic:
nhdsSet_iUnion,

Goal state after:
A : Type u_1
inst✝⁸ : NormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedAlgebra ℝ A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : ContinuousStar A
inst✝ : CompleteSpace A
r : ℝ
⊢ {0}ᶜ ∈ ⨆ i ∈ {a | IsStrictlyPositive a}, nhdsSet (spectrum ℝ≥0 (id i))
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
ha : 0 ≤ a
⊢ ‖star b * a * b‖ = ‖star b * sqrt a * (sqrt a * b)‖

Tactic:
← mul_assoc _ (CFC.sqrt a),

Goal state after:
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
ha : 0 ≤ a
⊢ ‖star b * a * b‖ = ‖star b * sqrt a * sqrt a * b‖
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
ha : 0 ≤ a
| ‖b * sqrt a‖ ^ 2

Tactic:
rw [← (CFC.sqrt_nonneg a).star_eq, ← star_star b, ← star_mul, norm_star,
    ← norm_star_mul_mul_self_of_nonneg _ ha, star_star]

Goal state after:
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
ha : 0 ≤ a
| ‖b * a * star b‖
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
⊢ sqrt a = 0 ↔ a = 0

Tactic:
rw [sqrt_eq_iff a _, mul_zero, eq_comm]

Goal state after:
Module: Mathlib.Topology.ApproximateUnit

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MulOneClass α
inst✝ : SeparatelyContinuousMul α
m : α
⊢ Tendsto (fun x ↦ x * m) (𝓝 1) (𝓝 m)

Tactic:
simpa using tendsto_id (x := 𝓝 1) |>.mul_const m

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

Goal state before:
pp: 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✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x | ContinuousOn (F x) (spectrum R a)}
| Tendsto ((fun x ↦ cfc (F x) a) ∘ Subtype.val) (comap Subtype.val l) (𝓝 (cfc f a))

Tactic:
conv =>

Goal state after:
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✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (spectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)
hl : l.NeBot
hf : ContinuousOn f (spectrum R a)
ha : p a
s : Set X := {x | ContinuousOn (F x) (spectrum R a)}
x : { x // x ∈ s }
| (cfcHom ha) { toFun := (spectrum R a).domRestrict (F ↑x), 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
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ
h : IsUnit a
hx : x ≠ 0
⊢ sqrt (a ^ x) = a ^ (x / 2)

Tactic:
by_cases hnonneg : 0 ≤ a

Goal state after:
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
x : ℝ
h : IsUnit a
hx : x ≠ 0
hnonneg : 0 ≤ a
⊢ sqrt (a ^ x) = a ^ (x / 2)

case neg
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
hx : x ≠ 0
hnonneg : ¬0 ≤ a
⊢ sqrt (a ^ x) = a ^ (x / 2)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: case refine_2
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 : X) (a : x ∈ t), ContinuousOn f (S ⟨x, ⋯⟩)

Tactic:
exact fun x hx ↦ hf.mono <| hS₃ ⟨x, hx⟩

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

Goal state before:
pp: case refine_2
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 : X) (a : x ∈ t), ContinuousOn f (S ⟨x, ⋯⟩)

Tactic:
exact fun x hx ↦ hf.mono <| hS₃ ⟨x, hx⟩

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

Goal state before:
pp: 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
s : Set X := {x | ContinuousOn (F x) (quasispectrum R a) ∧ F x 0 = 0}
hs : s ∈ l
| Tendsto ((fun x ↦ cfcₙ (F x) a) ∘ Subtype.val) (comap Subtype.val l) (𝓝 (cfcₙ f a))

Tactic:
conv =>

Goal state after:
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
s : Set X := {x | ContinuousOn (F x) (quasispectrum R a) ∧ F x 0 = 0}
hs : s ∈ l
x : { x // x ∈ s }
| (cfcₙHom ha) { toFun := (quasispectrum R a).domRestrict (F ↑x), continuous_toFun := ⋯, map_zero' := ⋯ }
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Unique ι
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
⊢ α

Tactic:
by classical exact if a = 0 then 1 else ‖a‖ • a⁻¹

Goal state after:
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₂
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‖
⊢ ∃ x, 0 ≤ x ∧ ‖x‖ = 1 ∧ 2 ^ (2 * n) < ‖f x‖

Tactic:
have hx := (eq_zero_or_norm_pos x).resolve_left (fun hx ↦ by simp_all)

Goal state after:
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‖
⊢ ∃ x, 0 ≤ x ∧ ‖x‖ = 1 ∧ 2 ^ (2 * n) < ‖f x‖
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: case neg
𝕜 : 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
⊢ ContinuousOn (fun x ↦ cfcₙ f x) {a | p a ∧ quasispectrum 𝕜 a ⊆ s}

Tactic:
convert! continuousOn_empty _
    rw [Set.eq_empty_iff_forall_notMem]
    exact fun a ha ↦ hs0 <| ha.2 <| quasispectrum.zero_mem 𝕜 a

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
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 := fun y ↦ 1 - (1 + y)⁻¹
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 * (1 + ε⁻¹ ^ 2 • y)⁻¹ * y ≤ ε ^ 2

Tactic:
calc
      y * (1 + ε⁻¹ ^ 2 • y)⁻¹ * y = y * ε ^ 2 * (y / (ε ^ 2 + y)) := by simp [field]
      _ ≤ ε ^ 2 * 1 := by
        gcongr
        · 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
        · exact div_le_one (by positivity) |>.mpr le_add_self
      _ = ε ^ 2 := mul_one _

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

Goal state before:
pp: 𝕜 : 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
r : 𝕜
| Commute ((cfcHom ha) (ContinuousMap.const (↑(spectrum 𝕜 a)) r)) b

Tactic:
conv =>

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

Goal state before:
pp: case inr
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
f : X → C(Y, E)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖(f x) y‖ ≤ bound x
h : Nonempty Y
bound_nonneg : 0 ≤ᵐ[μ] bound
⊢ HasFiniteIntegral f μ

Tactic:
refine .mono' bound_int ?_

Goal state after:
case inr
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
f : X → C(Y, E)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖(f x) y‖ ≤ bound x
h : Nonempty Y
bound_nonneg : 0 ≤ᵐ[μ] bound
⊢ ∀ᵐ (a : X) ∂μ, ‖f a‖ ≤ bound a
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
bound_nonneg : 0 ≤ᵐ[μ] bound
⊢ HasFiniteIntegral f μ

Tactic:
refine .mono' bound_int ?_

Goal state after:
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
bound_nonneg : 0 ≤ᵐ[μ] bound
⊢ ∀ᵐ (a : X) ∂μ, ‖f a‖ ≤ bound a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: case refine_2
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 : X) (a : x ∈ t), ContinuousOn f (S ⟨x, ⋯⟩)

Tactic:
exact fun x hx ↦ hf.mono <| hS₃ ⟨x, hx⟩

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

Goal state before:
pp: case refine_2
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 : X) (a : x ∈ t), ContinuousOn f (S ⟨x, ⋯⟩)

Tactic:
exact fun x hx ↦ hf.mono <| hS₃ ⟨x, hx⟩

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
inst✝¹ : ContinuousMap.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (spectrum ℝ ↑(ℜ a))
ha : IsStarNormal a
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.re) '' spectrum ℂ a)
⊢ cfc (fun x ↦ ↑(f x.re)) a = cfc f ↑(ℜ a)

Tactic:
conv_rhs =>
    rw [cfc_real_eq_complex, ← cfc_re_id a, ← cfc_comp' ..]
    simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
⊢ x ∈ A ∧ x ∉ (convexHull 𝕜) (A \ {x}) ↔ x ∈ A \ (convexHull 𝕜) (A \ {x})

Tactic:
mem_sdiff

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
⊢ x ∈ A ∧ x ∉ (convexHull 𝕜) (A \ {x}) ↔ x ∈ A ∧ x ∉ (convexHull 𝕜) (A \ {x})
Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Goal state before:
pp: A : Type u_2
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : A →ₚ[ℂ] ℂ
⊢ f.gnsNonUnitalStarAlgHom 1 = 1

Tactic:
by
  ext b
  induction b using induction_on with
  | hp => apply isClosed_eq <;> fun_prop
  | ih b => simp [gnsNonUnitalStarAlgHom]

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty ↥s
⊢ (e.subtypeRestr hs).target ⊆ e.target

Tactic:
by
  rw [← e.image_source_eq_target, ← OpenPartialHomeomorph.image_source_eq_target,
    e.subtypeRestr_source]
  rintro z ⟨z₀, hz₀, rfl⟩
  use z₀.val
  simpa

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U : Opens X
hU : Nonempty ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
this : ↑(e.subtypeRestr hU).symm y ∈ (e.subtypeRestr hU).source
⊢ (Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y ∈ e.source

Tactic:
rwa [e.subtypeRestr_source] at this

Goal state after:
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₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ (b, e₁.coordChange e₂ b x).1 = (↑e₂ (↑e₁.symm (b, x))).1

Tactic:
rw [e₂.coe_fst', ← e₁.coe_fst', e₁.apply_symm_apply' h₁]

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₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ proj (↑e₁.symm (b, x)) ∈ e₁.baseSet

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₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ proj (↑e₁.symm (b, x)) ∈ e₂.baseSet
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: case mk
𝕜 : Type u
A : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
b : 𝓜(𝕜, A)
toProd✝ : (A →L[𝕜] A) × (A →L[𝕜] A)
central✝ : ∀ (x y : A), toProd✝.2 x * y = x * toProd✝.1 y
h : { toProd := toProd✝, central := central✝ }.toProd = b.toProd
⊢ { toProd := toProd✝, central := central✝ } = b

Tactic:
cases b

Goal state after:
case mk.mk
𝕜 : Type u
A : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
toProd✝¹ : (A →L[𝕜] A) × (A →L[𝕜] A)
central✝¹ : ∀ (x y : A), toProd✝¹.2 x * y = x * toProd✝¹.1 y
toProd✝ : (A →L[𝕜] A) × (A →L[𝕜] A)
central✝ : ∀ (x y : A), toProd✝.2 x * y = x * toProd✝.1 y
h : { toProd := toProd✝¹, central := central✝¹ }.toProd = { toProd := toProd✝, central := central✝ }.toProd
⊢ { toProd := toProd✝¹, central := central✝¹ } = { toProd := toProd✝, central := central✝ }
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
hgf : IsLocalHomeomorphOn (g ∘ f) s
hg : IsLocalHomeomorphOn g (f '' s)
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
⊢ ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source

Tactic:
obtain ⟨g, hxg, rfl⟩ := hg (f x) ⟨x, hx, rfl⟩

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : OpenPartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf : IsLocalHomeomorphOn (↑g ∘ f) s
hg : IsLocalHomeomorphOn (↑g) (f '' s)
⊢ ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source