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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝¹ : CompleteSpace A
inst✝ : CStarRing A
a : A
ha : p a
⊢ (inrNonUnitalStarAlgHom 𝕜 A).comp (cfcₙHom ha) = cfcₙAux ⋯ a ha

Tactic:
let _ := RCLike.nonUnitalContinuousFunctionalCalculus hp₁
  apply ContinuousMapZero.UniqueHom.eq_of_continuous_of_map_id _ _ _
    (Unitization.continuous_inr.comp <| cfcₙHom_continuous ha)
    (continuous_cfcₙAux hp₁ a ha)
    (by simp [cfcₙHom_id ha, cfcₙAux_id hp₁ a ha])
  all_goals infer_instance

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

Goal state before:
pp: E : Type u_1
s : Set E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
⊢ TotallyBounded ((convexHull ℝ) s)

Tactic:
rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero] at ⊢ hs

Goal state after:
E : Type u_1
s : Set E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : ∀ U ∈ nhds 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
⊢ ∀ U ∈ nhds 0, ∃ t, t.Finite ∧ (convexHull ℝ) s ⊆ ⋃ y ∈ t, y +ᵥ U
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K L : NonemptyCompacts α
hL : IsPreconnected ↑L
⊢ IsPreconnected (Icc K L)

Tactic:
rw [← isEmbedding_toCompacts.isPreconnected_image, ← coe_toCompactsOrderEmbedding,
    OrderEmbedding.image_Icc _ (by simpa [← Set.Ioi_bot] using ordConnected_Ioi)]
  exact Compacts.isPreconnected_Icc (Compacts.coe_nonempty.mp K.nonempty) hL

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

Goal state before:
pp: case refine_2
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
h_deriv :
  ∀ (a b c : A) (y : ℝ),
    deriv (fun x ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
      NormedSpace.exp (y • a) * (a * c + c * b) * NormedSpace.exp (y • b)
h_deriv₂ :
  ∀ (a b : A),
    deriv (fun y ↦ deriv (fun x ↦ NormedSpace.exp (x • a) * NormedSpace.exp (x • b)) y) 0 = a ^ 2 + 2 • (a * b) + b ^ 2
h₄ : a ^ 2 + 2 • (-a * star a) + star a ^ 2 - (star a ^ 2 + 2 • (star a * -a) + a ^ 2) = 0
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-(x • a)) * NormedSpace.exp (x • star a) =
      NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))
h₃ :
  deriv (fun y ↦ deriv (fun x ↦ NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))) y) 0 =
    a ^ 2 + 2 • (-a * star a) + star a ^ 2
⊢ (fun a ↦ 2 • a) (star a * a) - (fun a ↦ 2 • a) (a * star a) = 0

Tactic:
rw [← h₄]

Goal state after:
case refine_2
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
h_deriv :
  ∀ (a b c : A) (y : ℝ),
    deriv (fun x ↦ NormedSpace.exp (x • a) * c * NormedSpace.exp (x • b)) y =
      NormedSpace.exp (y • a) * (a * c + c * b) * NormedSpace.exp (y • b)
h_deriv₂ :
  ∀ (a b : A),
    deriv (fun y ↦ deriv (fun x ↦ NormedSpace.exp (x • a) * NormedSpace.exp (x • b)) y) 0 = a ^ 2 + 2 • (a * b) + b ^ 2
h₄ : a ^ 2 + 2 • (-a * star a) + star a ^ 2 - (star a ^ 2 + 2 • (star a * -a) + a ^ 2) = 0
key :
  ∀ (x : ℝ),
    NormedSpace.exp (-(x • a)) * NormedSpace.exp (x • star a) =
      NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))
h₃ :
  deriv (fun y ↦ deriv (fun x ↦ NormedSpace.exp (x • star a) * NormedSpace.exp (-(x • a))) y) 0 =
    a ^ 2 + 2 • (-a * star a) + star a ^ 2
⊢ (fun a ↦ 2 • a) (star a * a) - (fun a ↦ 2 • a) (a * star a) =
    a ^ 2 + 2 • (-a * star a) + star a ^ 2 - (star a ^ 2 + 2 • (star a * -a) + a ^ 2)
Module: Mathlib.Analysis.LocallyConvex.Barrelled

Goal state before:
pp: α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁷ : NontriviallyNormedField 𝕜₁
inst✝¹⁶ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁵ : RingHomIsometric σ₁₂
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜₁ E
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformSpace F
inst✝⁸ : IsUniformAddGroup E
inst✝⁷ : IsUniformAddGroup F
inst✝⁶ : ContinuousSMul 𝕜₁ E
inst✝⁵ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst✝⁴ : PolynormableSpace 𝕜₂ F
inst✝³ : ContinuousSMul 𝕜₂ F
inst✝² : T2Space F
l : Filter α
inst✝¹ : l.IsCountablyGenerated
inst✝ : l.NeBot
g : α → E →SL[σ₁₂] F
f : E → F
h : Tendsto (fun n x ↦ (g n) x) l (𝓝 f)
u : ℕ → α
hu : Tendsto u atTop l
x : E
⊢ IsVonNBounded 𝕜₂ (range fun i ↦ (g (u i)) x)

Tactic:
rw [tendsto_pi_nhds] at h

Goal state after:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁷ : NontriviallyNormedField 𝕜₁
inst✝¹⁶ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁵ : RingHomIsometric σ₁₂
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜₁ E
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformSpace F
inst✝⁸ : IsUniformAddGroup E
inst✝⁷ : IsUniformAddGroup F
inst✝⁶ : ContinuousSMul 𝕜₁ E
inst✝⁵ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst✝⁴ : PolynormableSpace 𝕜₂ F
inst✝³ : ContinuousSMul 𝕜₂ F
inst✝² : T2Space F
l : Filter α
inst✝¹ : l.IsCountablyGenerated
inst✝ : l.NeBot
g : α → E →SL[σ₁₂] F
f : E → F
h✝ : Tendsto (fun n x ↦ (g n) x) l (𝓝 f)
h : ∀ (x : E), Tendsto (fun i ↦ (g i) x) l (𝓝 (f x))
__LinearMap✝ : E →ₛₗ[σ₁₂] F := linearMapOfTendsto f (fun a ↦ ↑(g a)) h✝
u : ℕ → α
hu : Tendsto u atTop l
x : E
⊢ IsVonNBounded 𝕜₂ (range fun i ↦ (g (u i)) x)
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
x : X
⊢ x ∈ (setOfIdeal I)ᶜ ↔ ∀ ⦃f : C(X, R)⦄, f ∈ I → f x = 0

Tactic:
setOfIdeal,

Goal state after:
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
x : X
⊢ x ∈ {x | ∀ f ∈ I, f x = 0}ᶜᶜ ↔ ∀ ⦃f : C(X, R)⦄, f ∈ I → f x = 0
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
x : X
⊢ x ∈ setOfIdeal I ↔ ∃ f ∈ I, f x ≠ 0

Tactic:
setOfIdeal,

Goal state after:
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
x : X
⊢ x ∈ {x | ∀ f ∈ I, f x = 0}ᶜ ↔ ∃ f ∈ I, f x ≠ 0
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: case refine_1
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : setOfIdeal I ⊆ s
f : C(X, R)
hf : f ∈ I
⊢ f ∈ idealOfSet R s

Tactic:
by_contra h'

Goal state after:
case refine_1
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : setOfIdeal I ⊆ s
f : C(X, R)
hf : f ∈ I
h' : f ∉ idealOfSet R s
⊢ False
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hU : s = ⋂ n, U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
f : ℕ → C(X, ℝ)
fs : ∀ (n : ℕ), EqOn (⇑(f n)) 1 s
fm : ∀ (n : ℕ), EqOn (⇑(f n)) 0 (U n ∩ interior m)ᶜ
_hf : ∀ (n : ℕ), HasCompactSupport ⇑(f n)
f_range : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1
u : ℕ → ℝ
u_pos : ∀ (i : ℕ), 0 < u i
u_sum : Summable u
hu : ∑' (i : ℕ), u i = 1
g : X → ℝ := fun x ↦ ∑' (n : ℕ), u n * (f n) x
hgmc : EqOn g 0 mᶜ
I : ∀ (n : ℕ) (x : X), u n * (f n) x ≤ u n
S : ∀ (x : X), Summable fun n ↦ u n * (f n) x
x : X
hx : x ∈ sᶜ
⊢ x ∈ (⇑{ toFun := g, continuous_toFun := ⋯ } ⁻¹' {1})ᶜ

Tactic:
obtain ⟨n, hn⟩ : ∃ n, x ∉ U n := by simpa [hU] using hx

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hU : s = ⋂ n, U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
f : ℕ → C(X, ℝ)
fs : ∀ (n : ℕ), EqOn (⇑(f n)) 1 s
fm : ∀ (n : ℕ), EqOn (⇑(f n)) 0 (U n ∩ interior m)ᶜ
_hf : ∀ (n : ℕ), HasCompactSupport ⇑(f n)
f_range : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1
u : ℕ → ℝ
u_pos : ∀ (i : ℕ), 0 < u i
u_sum : Summable u
hu : ∑' (i : ℕ), u i = 1
g : X → ℝ := fun x ↦ ∑' (n : ℕ), u n * (f n) x
hgmc : EqOn g 0 mᶜ
I : ∀ (n : ℕ) (x : X), u n * (f n) x ≤ u n
S : ∀ (x : X), Summable fun n ↦ u n * (f n) x
x : X
hx : x ∈ sᶜ
n : ℕ
hn : x ∉ U n
⊢ x ∈ (⇑{ toFun := g, continuous_toFun := ⋯ } ⁻¹' {1})ᶜ
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a b : A
ha : IsSelfAdjoint a
hb : IsSelfAdjoint b
hab : a * b = 0
⊢ Commute a b

Tactic:
by grind [commute_of_mul_eq_zero]

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s t : Set X
hs : IsOpen[inst✝¹] s
hscp : IsCompact (closure[inst✝¹] sᶜᶜ)
ht : IsClosed[inst✝¹] t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen[inst✝¹] u
hvIsOpen : IsOpen[inst✝¹] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
huvc : closure[inst✝¹] u ⊆ vᶜ
P : Set X → Set X → Prop := ⋯
c : Urysohns.CU P := ⋯
⊢ tsupport c.lim ⊆ uᶜ

Tactic:
rw [← IsClosed.closure_eq (isClosed_compl_iff.mpr huIsOpen)]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s t : Set X
hs : IsOpen[inst✝¹] s
hscp : IsCompact (closure[inst✝¹] sᶜᶜ)
ht : IsClosed[inst✝¹] t
hst : t ⊆ s
u v : Set X
huIsOpen : IsOpen[inst✝¹] u
hvIsOpen : IsOpen[inst✝¹] v
hscompl_subset_u : sᶜ ⊆ u
ht_subset_v : t ⊆ v
hDisjointuv : u ⊆ vᶜ
huvc : closure[inst✝¹] u ⊆ vᶜ
P : Set X → Set X → Prop := fun C x ↦ sᶜ ⊆ C
c : Urysohns.CU P := { C := closure[inst✝¹] u, U := tᶜ, P_C_U := ⋯, closed_C := ⋯, open_U := ⋯, subset := ⋯, hP := ⋯ }
⊢ tsupport c.lim ⊆ closure[inst✝¹] uᶜ
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: case refine_4
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
z : ℂ
hz : z ∈ spectrum ℂ a
hz' : z ∈ spectrum ℂ ⟨a, ⋯⟩
⊢ ∃ a_1, characterSpaceToSpectrum a a_1 = ⟨z, hz⟩

Tactic:
CharacterSpace.mem_spectrum_iff_exists

Goal state after:
case refine_4
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
z : ℂ
hz : z ∈ spectrum ℂ a
hz' : ∃ f, f ⟨a, ⋯⟩ = z
⊢ ∃ a_1, characterSpaceToSpectrum a a_1 = ⟨z, hz⟩
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: case refine_4
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
⊢ Function.Surjective (characterSpaceToSpectrum a)

Tactic:
rintro ⟨z, hz⟩
    have hz' := (StarSubalgebra.spectrum_eq (hS := isClosed ℂ a)
      (a := ⟨a, self_mem ℂ a⟩) ▸ hz)
    rw [CharacterSpace.mem_spectrum_iff_exists] at hz'
    obtain ⟨φ, rfl⟩ := hz'
    exact ⟨φ, rfl⟩

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

Goal state before:
pp: A : Type u_1
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : Module ℝ A
inst✝⁹ : SMulCommClass ℝ A A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace ↑s
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
this : Fact (0 ∈ s)
mul₁ : ∀ (f g : C(↑s, ℝ)₀), (cfcₙHomSuperset hb' hbs) f * (cfcₙHomSuperset hc' hcs) g = 0
mul₂ : ∀ (f g : C(↑s, ℝ)₀), (cfcₙHomSuperset hc' hcs) f * (cfcₙHomSuperset hb' hbs) g = 0
ψ : C(↑s, ℝ)₀ →⋆ₙₐ[ℝ] A :=
  let __src := ↑(cfcₙHomSuperset hb' hbs) + ↑(cfcₙHomSuperset hc' hcs);
  { toFun := ⇑(cfcₙHomSuperset hb' hbs) + ⇑(cfcₙHomSuperset hc' hcs), map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
    map_mul' := ⋯, map_star' := ⋯ }
f : C(↑s, ℝ)₀ := { toFun := fun x ↦ (↑x)⁺, continuous_toFun := ⋯, map_zero' := ⋯ }
key :
  cfcₙ
      (Function.extend Subtype.val ⇑(f.comp { toFun := Subtype.map id has, continuous_toFun := ⋯, map_zero' := ⋯ })
        fun x ↦ x⁺)
      a =
    cfcₙ
        (Function.extend Subtype.val ⇑(f.comp { toFun := Subtype.map id hbs, continuous_toFun := ⋯, map_zero' := ⋯ })
          fun x ↦ x⁺)
        b +
      cfcₙ
        (Function.extend Subtype.val ⇑(f.comp { toFun := Subtype.map id hcs, continuous_toFun := ⋯, map_zero' := ⋯ })
          fun x ↦ x⁺)
        (-c)
⊢ cfcₙ id b + cfcₙ 0 (-c) =
    cfcₙ
        (Function.extend Subtype.val ⇑(f.comp { toFun := Subtype.map id hbs, continuous_toFun := ⋯, map_zero' := ⋯ })
          fun x ↦ x⁺)
        b +
      cfcₙ
        (Function.extend Subtype.val ⇑(f.comp { toFun := Subtype.map id hcs, continuous_toFun := ⋯, map_zero' := ⋯ })
          fun x ↦ x⁺)
        (-c)

Tactic:
by
      congr! 1
      all_goals
        refine cfcₙ_congr fun x hx ↦ Eq.symm ?_
        lift x to σₙ ℝ _ using hx
        simp only [Subtype.val_injective.extend_apply, comp_apply, coe_mk,
          ContinuousMap.coe_mk, Subtype.map_coe, id_eq, _root_.posPart_eq_self, f, Pi.zero_apply,
          posPart_eq_zero]
      · exact quasispectrum_nonneg_of_nonneg b hb x.val x.property
      · obtain ⟨x, hx⟩ := x
        simp only [← neg_nonneg]
        rw [Unitization.quasispectrum_eq_spectrum_inr ℝ (-c), Unitization.inr_neg,
          ← spectrum.neg_eq, Set.mem_neg, ← Unitization.quasispectrum_eq_spectrum_inr ℝ c]
          at hx
        exact quasispectrum_nonneg_of_nonneg c hc _ hx

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

Goal state before:
pp: A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
n : ℕ
⊢ (↑n)⁺ = ↑n

Tactic:
rw [← map_natCast (algebraMap ℝ≥0 A), posPart_algebraMap_nnreal]

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

Goal state before:
pp: A : Type u_2
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
x : ℝ
ha : IsSelfAdjoint a
⊢ ↑x ∈ spectrum ℂ a ↔ x ∈ spectrum ℝ a

Tactic:
simp [← ha.spectrumRestricts.algebraMap_image]

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

Goal state before:
pp: case neg.inr
A : Type u_1
inst✝¹³ : NonUnitalCStarAlgebra A
R : Type u_2
inst✝¹² : Semifield R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : Algebra R ℂ
inst✝³ : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R A p
inst✝¹ : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst✝ : ContinuousMapZero.UniqueHom R (Unitization ℂ A)
hp : ∀ {a : A}, p' ↑a ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
h : ¬(ContinuousOn f (σₙ R a) ∧ p a)
ha : ¬p a
⊢ 0 = cfc f ↑a

Tactic:
cfc_apply_of_not_predicate _ (not_iff_not.mpr hp |>.mpr ha)

Goal state after:
case neg.inr
A : Type u_1
inst✝¹³ : NonUnitalCStarAlgebra A
R : Type u_2
inst✝¹² : Semifield R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : Algebra R ℂ
inst✝³ : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R A p
inst✝¹ : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst✝ : ContinuousMapZero.UniqueHom R (Unitization ℂ A)
hp : ∀ {a : A}, p' ↑a ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
h : ¬(ContinuousOn f (σₙ R a) ∧ p a)
ha : ¬p a
⊢ 0 = 0
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
⊢ cfcₙ (fun z ↦ id z * (id z * id z)) a = a * a * a

Tactic:
rw [cfcₙ_mul id _ a, cfcₙ_mul id _ a, ← mul_assoc, cfcₙ_id ℝ≥0 a]

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
this : a * star a ≤ (algebraMap ℝ A) ‖a * star a‖
⊢ a * star a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)

Tactic:
rwa [CStarRing.norm_self_mul_star, ← pow_two] at this

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 b : A
h : IsStrictlyPositive a ∧ 0 ≤ b ∨ 0 ≤ a ∧ IsStrictlyPositive b
⊢ IsStrictlyPositive (a + b)

Tactic:
grind [IsStrictlyPositive.add_nonneg, IsStrictlyPositive.nonneg_add]

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

Goal state before:

Tactic:
‖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.Matrix.Normed

Goal state before:
pp: case h
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : RCLike α
A : Matrix l m α
B : Matrix m n α
i : l
a✝¹ : i ∈ Finset.univ
j : n
a✝ : j ∈ Finset.univ
⊢ ‖∑ j_1, A i j_1 * B j_1 j‖₊ ≤ (∑ j, ‖A i j‖₊ ^ 2) ^ (1 / 2) * (∑ x, ‖B x j‖₊ ^ 2) ^ (1 / 2)

Tactic:
simpa only [PiLp.toLp_apply, PiLp.inner_apply, RCLike.inner_apply', starRingEnd_apply,
    Pi.nnnorm_def, PiLp.nnnorm_eq_of_L2, star_star, nnnorm_star, NNReal.sqrt_eq_rpow,
    NNReal.rpow_two] using nnnorm_inner_le_nnnorm (𝕜 := α) (toLp 2 (star <| A i ·)) (toLp 2 (B · j))

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

Goal state before:
pp: A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
hb : Commute a b
f : ℝ → ℝ
hf : ContinuousOn f (spectrum ℝ a)
ha : IsSelfAdjoint a
⊢ Commute ((cfcHom ha) { toFun := (spectrum ℝ a).domRestrict f, continuous_toFun := ⋯ }) b

Tactic:
by
    rw [← cfc_apply ..]
    exact hb.cfc (ha.star_eq.symm ▸ hb) _

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✝⁸ : 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
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) t

Tactic:
refine ha_cont.cfcₙ (s := fun x : X ↦ if hx : x ∈ t then S ⟨x, hx⟩ else ∅) f
    (by simpa +contextual using hS₁) ?_ ha' ?_
  all_goals simp +contextual only [↓reduceDIte]
  · exact fun x₀ hx₀ ↦ ha_cont.continuousWithinAt hx₀ |>.eventually <| hS₂ ⟨x₀, hx₀⟩
  · exact fun x hx ↦ hf.mono <| hS₃ ⟨x, hx⟩

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

Goal state before:
pp: 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
a b : A
hb : Commute a b
f : ℝ → ℝ
hf : ContinuousOn f (quasispectrum ℝ a)
hf0 : { toFun := (quasispectrum ℝ a).domRestrict f, continuous_toFun := ⋯ } 0 = 0
ha : IsSelfAdjoint a
⊢ Commute ((cfcₙHom ha) { toFun := (quasispectrum ℝ a).domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 }) b

Tactic:
by
      rw [← cfcₙ_apply ..]
      exact hb.cfcₙ (ha.star_eq.symm ▸ hb) _

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪b i, x⟫ = ⟪b i, y⟫
⊢ x = y

Tactic:
apply (toDualMap 𝕜 E).map_eq_iff.mp

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪b i, x⟫ = ⟪b i, y⟫
⊢ (toDualMap 𝕜 E) x = (toDualMap 𝕜 E) y
Module: Mathlib.Analysis.InnerProductSpace.Dual

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ).ker
htriv : Y = ⊤
h' : ↑ℓ = 0
⊢ ℓ = 0

Tactic:
norm_cast at h'

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

Goal state before:
pp: z : Circle
⊢ (starRingEnd ℂ) ↑z * ↑(normSq ↑z)⁻¹ = (starRingEnd ℂ) ↑z

Tactic:
normSq_coe,

Goal state after:
z : Circle
⊢ (starRingEnd ℂ) ↑z * ↑1⁻¹ = (starRingEnd ℂ) ↑z
Module: Mathlib.Analysis.Complex.Circle

Goal state before:
pp: x : ℝ
z : ℤ
⊢ exp (↑z * x) = exp x ^ z

Tactic:
by
  rw [← zsmul_eq_mul, exp_zsmul]

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

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
⊢ ‖diagonal v‖ = ‖v‖

Tactic:
rw [← l2_opNorm_toEuclideanCLM]

Goal state after:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
⊢ ‖toEuclideanCLM (diagonal v)‖ = ‖v‖