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✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : NormOneClass A
a : A
⊢ spectralRadius 𝕜 a ≤ ↑‖a‖₊

Tactic:
refine iSup₂_le fun k hk => ?_
  exact mod_cast norm_le_norm_of_mem hk

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : ProperSpace 𝕜
a : A
ha : (σ a).Nonempty
⊢ ∃ k ∈ σ a, ↑‖k‖₊ = spectralRadius 𝕜 a

Tactic:
obtain ⟨k, hk, h⟩ := (spectrum.isCompact a).exists_isMaxOn ha continuous_nnnorm.continuousOn
  exact ⟨k, hk, le_antisymm (le_iSup₂ (α := ℝ≥0∞) k hk) (iSup₂_le <| mod_cast h)⟩

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
s K : Set α
hKs : K ∈ 𝒫 closure[inst✝] s
⊢ ∀ ⦃x : Set (Set α)⦄,
    x ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U} →
      K ∈ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} →
        ({s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ∩ {t | t.Finite ∧ t ⊆ s}).Nonempty

Tactic:
rintro u ⟨hu₁, hu₂⟩ ⟨ht₁, ht₂⟩

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
s K : Set α
hKs : K ∈ 𝒫 closure[inst✝] s
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝] U
ht₁ : K ⊆ ⋃₀ u
ht₂ : ∀ U ∈ u, (K ∩ U).Nonempty
⊢ ({s | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty} ∩ {t | t.Finite ∧ t ⊆ s}).Nonempty
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
h : (fun z ↦ resolvent (z⁻¹ • a) 1) =O[cobounded 𝕜] fun x ↦ 1
z : 𝕜
⊢ z ∈ {0}ᶜ → resolvent a z = z⁻¹ • resolvent (z⁻¹ • a) 1

Tactic:
hz

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
h : (fun z ↦ resolvent (z⁻¹ • a) 1) =O[cobounded 𝕜] fun x ↦ 1
z : 𝕜
hz : z ∈ {0}ᶜ
⊢ resolvent a z = z⁻¹ • resolvent (z⁻¹ • a) 1
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
x : 𝕜
hx : x ∈ σ 𝕜 a
ha : p a
⊢ ‖x‖₊ ≤ ‖a‖₊

Tactic:
simpa only [cfc_id 𝕜 a] using! nnnorm_apply_le_nnnorm_cfc (id : 𝕜 → 𝕜) a hx

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

Goal state before:
pp: A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
x : ℝ
hx : x ∈ spectrum ℝ a
⊢ ↑‖x‖₊ ≤ ↑t

Tactic:
NNReal.coe_le_coe,

Goal state after:
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
x : ℝ
hx : x ∈ spectrum ℝ a
⊢ ‖x‖₊ ≤ t
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case refine_1
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ < c
⊢ ‖0‖ < c

pp: case refine_2
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ < c
hf : ContinuousOn f (σₙ 𝕜 a)
hf0 : { toFun := (σₙ 𝕜 a).domRestrict f, continuous_toFun := ⋯ } 0 = 0
ha : p a
⊢ ‖(cfcₙHom ha) { toFun := (σₙ 𝕜 a).domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 }‖ < c

Tactic:
· simpa using (norm_nonneg _).trans_lt <| h 0 (quasispectrum.zero_mem 𝕜 a)

Goal state after:
case refine_2
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ < c
hf : ContinuousOn f (σₙ 𝕜 a)
hf0 : { toFun := (σₙ 𝕜 a).domRestrict f, continuous_toFun := ⋯ } 0 = 0
ha : p a
⊢ ‖(cfcₙHom ha) { toFun := (σₙ 𝕜 a).domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 }‖ < c
Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula

Goal state before:
pp: A : Type u_2
inst✝³ : NormedRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
inst✝ : Nontrivial A
a : A
n : ℕ
⊢ spectrum ℂ (a ^ n) = (fun x ↦ x ^ n) '' spectrum ℂ a

Tactic:
simpa only [aeval_X_pow, eval_X_pow] using map_polynomial_aeval a (X ^ n)

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : FunLike F α β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f g : α →C₀ β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by
    obtain ⟨⟨_, _⟩, _⟩ := f
    obtain ⟨⟨_, _⟩, _⟩ := g
    congr

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.HahnBanach

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹² : AddCommGroup E
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : IsRCLikeNormedField 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : PolynormableSpace 𝕜 E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : Module 𝕜 F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : T2Space F
S : Submodule 𝕜 E
f : ↥S →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(↑f).range
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
b : Basis (Fin (finrank 𝕜 ↥(↑f).range)) 𝕜 ↥(↑f).range := finBasis 𝕜 ↥(↑f).range
e : ↥(↑f).range ≃L[𝕜] Fin (finrank 𝕜 ↥(↑f).range) → 𝕜 := b.equivFunL
⊢ ∃ g, f = g ∘SL S.subtypeL

Tactic:
let fi := fun i ↦ (LinearMap.toContinuousLinearMap (b.coord i)).comp
    (f.codRestrict _ <| LinearMap.mem_range_self _)

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝¹² : AddCommGroup E
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : IsRCLikeNormedField 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : PolynormableSpace 𝕜 E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : Module 𝕜 F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : T2Space F
S : Submodule 𝕜 E
f : ↥S →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(↑f).range
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
b : Basis (Fin (finrank 𝕜 ↥(↑f).range)) 𝕜 ↥(↑f).range := finBasis 𝕜 ↥(↑f).range
e : ↥(↑f).range ≃L[𝕜] Fin (finrank 𝕜 ↥(↑f).range) → 𝕜 := b.equivFunL
fi : Fin (finrank 𝕜 ↥(↑f).range) → ↥S →L[𝕜] 𝕜 :=
  fun i ↦ LinearMap.toContinuousLinearMap (b.coord i) ∘SL f.codRestrict (↑f).range ⋯
⊢ ∃ g, f = g ∘SL S.subtypeL
Module: Mathlib.Analysis.Normed.Module.Dual

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
s_nhds : s ∈ 𝓝 0
⊢ IsBounded (polar 𝕜 s)

Tactic:
obtain ⟨a, ha⟩ : ∃ a : 𝕜, 1 < ‖a‖ := NormedField.exists_one_lt_norm 𝕜

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
s_nhds : s ∈ 𝓝 0
a : 𝕜
ha : 1 < ‖a‖
⊢ IsBounded (polar 𝕜 s)
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case zero
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
hx : x ∉ c.U
⊢ approx 0 c x = 1

Tactic:
rw [← mem_compl_iff] at hx

Goal state after:
case zero
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
hx : x ∈ c.Uᶜ
⊢ approx 0 c x = 1
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 y : ℝ
ha : IsUnit a
ha' : 0 ∉ spectrum ℝ≥0 a
z : ℝ≥0
⊢ z ∈ spectrum ℝ≥0 a → (fun x_1 ↦ x_1 ^ (x + y)) z = (fun x_1 ↦ x_1 ^ x * x_1 ^ y) z

Tactic:
hz

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
a : A
x y : ℝ
ha : IsUnit a
ha' : 0 ∉ spectrum ℝ≥0 a
z : ℝ≥0
hz : z ∈ spectrum ℝ≥0 a
⊢ (fun x_1 ↦ x_1 ^ (x + y)) z = (fun x_1 ↦ x_1 ^ x * x_1 ^ y) z
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: case neg.refine_1
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬IsSelfAdjoint a
h : 0 ≤ ↑a
⊢ IsSelfAdjoint a

Tactic:
exact isSelfAdjoint_inr (R := ℂ) |>.mp <| .of_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
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
⊢ ContinuousOn (fun x ↦ cfc f (a x)) t

Tactic:
have hs' := hs
  simp only [nhdsSet_iUnion, mem_iSup] at hs'
  have (x : t) : ∃ S, IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a x), spectrum 𝕜 x' ⊆ S) ∧ S ⊆ s := by
    obtain ⟨S, ⟨hS₁, hS₂⟩, hS₃⟩ :=
      spectrum.isCompact (𝕜 := 𝕜) (a x) |>.nhdsSet_basis_isCompact.mem_iff.mp (hs' x x.2)
    refine ⟨S, hS₂, ?_, hS₃⟩
    exact upperHemicontinuous_spectrum 𝕜 A |>.upperHemicontinuousAt (a x) _ hS₁ |>.mono
      fun _ ↦ subset_of_mem_nhdsSet
  choose S hS₁ hS₂ hS₃ using this
  classical
  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.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
x : E
hx : x ≠ 0
H : ⟪x, x⟫ = 0
⊢ False

Tactic:
inner_self

Goal state after:
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
x : E
hx : x ≠ 0
H : x = 0
⊢ False
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hb : IsSelfAdjoint b
this : ∀ (a b : Unitization ℂ A), IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a)
⊢ star a * b * a ≤ ‖b‖ • (star a * a)

Tactic:
rw [← Unitization.inr_le_iff _ _ (by aesop) ((IsSelfAdjoint.all _).smul (.star_mul_self a))]
    simpa [Unitization.norm_inr] using this a b <| hb.inr ℂ

Goal state after:
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 : E
⊢ 0 ≤ ↑(RCLike.re ⟪x, x⟫_ℂ)

Tactic:
RCLike.ofReal_nonneg

Goal state after:
A : Type u_1
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℂ E
x : E
⊢ 0 ≤ RCLike.re ⟪x, x⟫_ℂ
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i ↦ (i, i), inj' := ⋯ } Finset.univ
⊢ (∑ x, ‖diagonal v x.1 x.2‖₊ ^ 2) ^ (1 / 2) = NNReal.sqrt (∑ x, ‖v x‖₊ ^ 2)

Tactic:
rw [← Finset.sum_subset (Finset.subset_univ s) fun i _hi his => ?_]

Goal state after:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i ↦ (i, i), inj' := ⋯ } Finset.univ
⊢ (∑ x ∈ s, ‖diagonal v x.1 x.2‖₊ ^ 2) ^ (1 / 2) = NNReal.sqrt (∑ x, ‖v x‖₊ ^ 2)

n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i ↦ (i, i), inj' := ⋯ } Finset.univ
i : n × n
_hi : i ∈ Finset.univ
his : i ∉ s
⊢ ‖diagonal v i.1 i.2‖₊ ^ 2 = 0
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✝ : TopologicalSpace X
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
ha_cont : ContinuousOn a t
ha : ∀ x ∈ t, quasispectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) t

Tactic:
refine ContinuousOn.cfcₙ_nnreal _ (fun _ _ ↦ hs) ha_cont (fun _ _ ↦ ?_) ha'
  filter_upwards [self_mem_nhdsWithin] with x hx
  exact ha x hx

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

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : MeasurableSpace X
μ : Measure X
inst✝⁷ : NormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedAlgebra 𝕜 A
inst✝⁴ : ContinuousFunctionalCalculus 𝕜 A p
inst✝³ : CompleteSpace A
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)
hf : ContinuousOn (Function.uncurry f) (s ×ˢ spectrum 𝕜 a)
bound_ge : ∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound (μ.restrict s)
ha : p a
⊢ IntegrableOn (fun x ↦ cfc (f x) a) s μ

Tactic:
refine integrableOn_cfc' _ _ ⟨?_, ?_⟩ ha

Goal state after:
case refine_1
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : MeasurableSpace X
μ : Measure X
inst✝⁷ : NormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedAlgebra 𝕜 A
inst✝⁴ : ContinuousFunctionalCalculus 𝕜 A p
inst✝³ : CompleteSpace A
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)
hf : ContinuousOn (Function.uncurry f) (s ×ˢ spectrum 𝕜 a)
bound_ge : ∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound (μ.restrict s)
ha : p a
⊢ AEStronglyMeasurable (fun x ↦ mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) (μ.restrict s)

case refine_2
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : MeasurableSpace X
μ : Measure X
inst✝⁷ : NormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedAlgebra 𝕜 A
inst✝⁴ : ContinuousFunctionalCalculus 𝕜 A p
inst✝³ : CompleteSpace A
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)
hf : ContinuousOn (Function.uncurry f) (s ×ˢ spectrum 𝕜 a)
bound_ge : ∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound (μ.restrict s)
ha : p a
⊢ HasFiniteIntegral (fun x ↦ mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) (μ.restrict s)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

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

Tactic:
← range_cfc_subset ℝ ha.isSelfAdjoint,

Goal state after:
A : Type u_1
inst✝¹¹ : Ring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra ℝ A
inst✝⁸ : TopologicalSpace A
inst✝⁷ : IsTopologicalRing A
inst✝⁶ : T2Space A
inst✝⁵ : PartialOrder A
inst✝⁴ : NonnegSpectrumClass ℝ A
inst✝³ : StarOrderedRing A
inst✝² : ContinuousStar A
inst✝¹ : StarModule ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ (fun x ↦ cfc x a) '' {f | ∀ x ∈ spectrum ℝ a, 0 ≤ f x} ⊆ (Set.range fun x ↦ cfc x a) ∩ {a | 0 ≤ a}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : MeasurableSpace X
μ : Measure X
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : CompleteSpace A
inst✝ : NormedSpace ℝ A
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)
hf₂ : ∀ᵐ (x : X) ∂μ, f x 0 = 0
hf₃ : Integrable (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
z : ↑(quasispectrum 𝕜 a)
⊢ ∫ (x : X), f x ↑z ∂μ = (∫ (x : X), mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z

Tactic:
integral_apply hf₃

Goal state after:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : MeasurableSpace X
μ : Measure X
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : CompleteSpace A
inst✝ : NormedSpace ℝ A
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)
hf₂ : ∀ᵐ (x : X) ∂μ, f x 0 = 0
hf₃ : Integrable (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
z : ↑(quasispectrum 𝕜 a)
⊢ ∫ (x : X), f x ↑z ∂μ = ∫ (x : X), (mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) z ∂μ
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 + I * ↑z.im) a = ↑(ℜ a) + I • ↑(ℑ a)
⊢ cfc (fun x ↦ ↑x.im) a = ↑(ℑ a)

Tactic:
rw [cfc_add .., cfc_const_mul .., cfc_re_id a] at this
    simpa

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

Goal state before:
pp: x : Circle
⊢ ↑x = 1 ↔ x = 1

Tactic:
rw [← coe_inj, coe_one]

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
Z : Type u_5
Z' : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace X'
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : TopologicalSpace Y'
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace Z'
e✝ e e' : OpenPartialHomeomorph X Y
inst✝¹ : (x : X) → Decidable (x ∈ e.source)
inst✝ : (y : Y) → Decidable (y ∈ e.target)
Hs : Disjoint e.source e'.source
Ht : Disjoint e.target e'.target
⊢ EqOn (↑e) (↑e') (e.source ∩ frontier e.source)

Tactic:
rw [e.open_source.inter_frontier_eq]
          exact eqOn_empty _ _

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

Goal state before:
pp: B : Type u_2
F : Type u_3
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
E : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F E)
inst✝¹ : (b : B) → TopologicalSpace (E b)
inst✝ : FiberBundle F E
s : (x : B) → E x
a : Set B
x₀ : B
⊢ ContinuousWithinAt (fun x ↦ TotalSpace.mk' F x (s x)) a x₀ ↔
    ContinuousWithinAt (fun x ↦ (↑(trivializationAt F E x₀) { proj := x, snd := s x }).2) a x₀

Tactic:
simp_rw [continuousWithinAt_totalSpace, and_iff_right_iff_imp]

Goal state after:
B : Type u_2
F : Type u_3
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
E : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F E)
inst✝¹ : (b : B) → TopologicalSpace (E b)
inst✝ : FiberBundle F E
s : (x : B) → E x
a : Set B
x₀ : B
⊢ ContinuousWithinAt (fun x ↦ (↑(trivializationAt F E x₀) (TotalSpace.mk' F x (s x))).2) a x₀ →
    ContinuousWithinAt (fun x ↦ x) a 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
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
x✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
⊢ ContinuousOn (↑e.toPartialEquiv) e.source

Tactic:
refine continuousOn_iff'.mpr fun s hs => ⟨e ⁻¹' s ∩ e.source,
        isOpen_iSup_iff.mpr fun e' => ?_, by rw [inter_assoc, inter_self]; rfl⟩

Goal state after:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
x✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
s : Set (B × F)
hs : IsOpen[instTopologicalSpaceProd] s
e' : Pretrivialization F TotalSpace.proj
⊢ IsOpen[⨆ (_ : e' ∈ a.pretrivializationAtlas), coinduced e'.setSymm instTopologicalSpaceSubtype] (↑e ⁻¹' s ∩ e.source)
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst✝³] s
hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
z : TotalSpace F E
⊢ z ∈ TotalSpace.proj ⁻¹' s → ContinuousWithinAt f (TotalSpace.proj ⁻¹' s) z

Tactic:
hz

Goal state after:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst✝³] s
hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
z : TotalSpace F E
hz : z ∈ TotalSpace.proj ⁻¹' s
⊢ ContinuousWithinAt f (TotalSpace.proj ⁻¹' s) z
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
ha₁ : IsSelfAdjoint a
ha₂' : ContinuousOn Real.log (spectrum ℝ a)
ha₂'' : ContinuousOn Real.log ((fun x ↦ x ^ n) '' spectrum ℝ a)
⊢ cfc (fun x ↦ ↑n * Real.log x) a = n • cfc Real.log a

Tactic:
← Nat.cast_smul_eq_nsmul ℝ n,

Goal state after:
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
ha₁ : IsSelfAdjoint a
ha₂' : ContinuousOn Real.log (spectrum ℝ a)
ha₂'' : ContinuousOn Real.log ((fun x ↦ x ^ n) '' spectrum ℝ a)
⊢ cfc (fun x ↦ ↑n * Real.log x) a = ↑n • cfc Real.log a