mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r' : k
h : 0 < r' * (b - a)
⊢ f ((lineMap b a) r') ≤ (lineMap (f b) (f a)) r' ↔ slope f a b ≤ slope f ((lineMap b a) r') b

Tactic:
lineMap_apply,

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r' : k
h : 0 < r' * (b - a)
⊢ f (r' • (a -ᵥ b) +ᵥ b) ≤ r' • (f a -ᵥ f b) +ᵥ f b ↔ slope f a b ≤ slope f (r' • (a -ᵥ b) +ᵥ b) b
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
ht : IsClosed[inst✝²] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst✝²] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
P : Set X → Set X → Prop := fun C x ↦ IsCompact C
c u : Set X
c_comp : P c u
u_open : IsOpen[inst✝²] u
cu : c ⊆ u
⊢ ∃ v, IsOpen[inst✝²] v ∧ c ⊆ v ∧ closure[inst✝²] v ⊆ u ∧ P c v ∧ P (closure[inst✝²] v) u

Tactic:
rcases exists_compact_closed_between c_comp u_open cu with ⟨k, k_comp, k_closed, ck, ku⟩

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
k✝ : Set X
k_comp✝ : IsCompact k✝
k_closed✝ : IsClosed[inst✝²] k✝
sk : s ⊆ interior k✝
kt : k✝ ⊆ tᶜ
P : Set X → Set X → Prop := fun C x ↦ IsCompact C
c u : Set X
c_comp : P c u
u_open : IsOpen[inst✝²] u
cu : c ⊆ u
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst✝²] k
ck : c ⊆ interior k
ku : k ⊆ u
⊢ ∃ v, IsOpen[inst✝²] v ∧ c ⊆ v ∧ closure[inst✝²] v ⊆ u ∧ P c v ∧ P (closure[inst✝²] v) u
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : I.IsMaximal
a : A
ha : a ∈ I
⊢ ⋯.some = 0

Tactic:
exact Set.eq_of_mem_singleton (Set.singleton_nonempty (0 : ℂ)).some_mem

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
x : X
k : Set X
hk : IsCompact k
k_mem : k ∈ 𝓝 x
f : C(X, ℝ)
fk : EqOn (⇑f) 1 k
f_comp : HasCompactSupport ⇑f
hf : ∀ (x : X), f x ∈ Icc 0 1
this : f x = 1 x
⊢ f x ≠ 0

Tactic:
simp only [Pi.one_apply] at this

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
x : X
k : Set X
hk : IsCompact k
k_mem : k ∈ 𝓝 x
f : C(X, ℝ)
fk : EqOn (⇑f) 1 k
f_comp : HasCompactSupport ⇑f
hf : ∀ (x : X), f x ∈ Icc 0 1
this : f x = 1
⊢ f x ≠ 0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
ha₂ : SpectrumRestricts (-a) ⇑ContinuousMap.realToNNReal
⊢ a = 0

Tactic:
rw [SpectrumRestricts.nnreal_iff] at ha₁ ha₂

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : ∀ x ∈ spectrum ℝ a, 0 ≤ x
ha₂ : ∀ x ∈ spectrum ℝ (-a), 0 ≤ x
⊢ a = 0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: case neg
A : Type u_2
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
a✝ : Nontrivial A
x : ℝ
r : ℝˣ
hr : 0 ≤ ↑r
hx : x ∈ spectrum ℝ (↑r • a)
hr' : ¬↑r = 0
⊢ 0 ≤ x

Tactic:
rw [← Units.smul_def, spectrum.unit_smul_eq_smul, Set.mem_smul_set_iff_inv_smul_mem] at hx

Goal state after:
case neg
A : Type u_2
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
a✝ : Nontrivial A
x : ℝ
r : ℝˣ
hr : 0 ≤ ↑r
hx : r⁻¹ • x ∈ spectrum ℝ a
hr' : ¬↑r = 0
⊢ 0 ≤ x
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace ℝ A
inst✝³ : SMulCommClass ℝ A A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : StarRing A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
⊢ ‖a⁺‖ ≤ ‖a‖

Tactic:
by_cases ha : IsSelfAdjoint a
  case neg => simp [CFC.posPart_def, cfcₙ_apply_of_not_predicate a ha]
  refine norm_cfcₙ_le fun x hx ↦ ?_
  obtain (h | h) := le_or_gt x 0
  · simp [posPart_def, max_eq_right h]
  · simp only [posPart_def, max_eq_left h.le]
    exact NonUnitalIsometricContinuousFunctionalCalculus.norm_quasispectrum_le a hx ha

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

Goal state before:
pp: case frequently
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✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace ↑s
f : C(↑s, 𝕜)
hf :
  ∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f,
    Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcHomSuperset ⋯ ⋯) g
ε : ℝ
hε : 0 < ε
g : C(↑s, 𝕜)
g_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcHomSuperset ⋯ ⋯) g
hg : ‖f - g‖ ≤ ε
x : X
⊢ ‖(f - g).comp { toFun := Subtype.map id ⋯, continuous_toFun := ⋯ }‖ ≤ ε

Tactic:
rw [ContinuousMap.norm_le _ hε.le] at hg ⊢

Goal state after:
case frequently
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✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace ↑s
f : C(↑s, 𝕜)
hf :
  ∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f,
    Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcHomSuperset ⋯ ⋯) g
ε : ℝ
hε : 0 < ε
g : C(↑s, 𝕜)
g_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcHomSuperset ⋯ ⋯) g
hg : ∀ (x : ↑s), ‖(f - g) x‖ ≤ ε
x : X
⊢ ∀ (x_1 : ↑(spectrum 𝕜 (a x))), ‖((f - g).comp { toFun := Subtype.map id ⋯, continuous_toFun := ⋯ }) x_1‖ ≤ ε
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
hab : a ≤ b
h : IsStrictlyPositive a
a✝ : Nontrivial A
⊢ 0 ∉ spectrum ℝ b

Tactic:
obtain ⟨r, hr, hr_le⟩ : ∃ r > 0, (algebraMap ℝ A) r ≤ a :=
    (exists_pos_algebraMap_le_iff h.isSelfAdjoint).2 fun x hx ↦ h.spectrum_pos hx

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a ≤ b
h : IsStrictlyPositive a
a✝ : Nontrivial A
r : ℝ
hr : r > 0
hr_le : (algebraMap ℝ A) r ≤ a
⊢ 0 ∉ spectrum ℝ b
Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalCStarAlgebra A
inst✝⁸ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : Module ℂ E
inst✝⁵ : SMul A E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : Module ℂ F
inst✝² : SMul A F
inst✝¹ : CStarModule A E
inst✝ : CStarModule A F
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ‖⟪x.1, x.1⟫_A‖ + ‖⟪x.2, x.2⟫_A‖ = ‖x.1‖ ^ 2 + 0 + ‖x.2‖ ^ 2

Tactic:
simp [norm_sq_eq A]

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)
inst✝¹ : StarOrderedRing A
inst✝ : DecidableEq ι
i : ι
y : E i
x✝ : NormedAddCommGroup C⋆ᵐᵒᵈ(A, (i : ι) → E i) := normedAddCommGroup A
⊢ ‖(equiv A ((j : ι) → E j)).symm (Pi.single i y)‖ ^ 2 = ‖y‖ ^ 2

Tactic:
simp [norm_sq_eq A]

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)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
⊢ ‖x i‖ ≤ ‖x‖

Tactic:
by
  let _ : NormedAddCommGroup C⋆ᵐᵒᵈ(A, Π i, E i) := normedAddCommGroup A
  refine abs_le_of_sq_le_sq' ?_ (by positivity) |>.2
  rw [pi_norm_sq, norm_sq_eq A]
  refine CStarAlgebra.norm_le_norm_of_nonneg_of_le inner_self_nonneg ?_
  exact Finset.single_le_sum (fun j _ ↦ inner_self_nonneg (A := A) (x := x j)) (Finset.mem_univ i)

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

Goal state before:

Tactic:
‖x‖ ≤ ∑ i, ‖x i‖ := pi_norm_le_sum_norm x
      _ ≤ ∑ _, ‖⇑x‖ := Finset.sum_le_sum fun _ _ ↦ norm_le_pi_norm ..
      _ ≤ Fintype.card ι * ‖⇑x‖ := by simp

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

Goal state before:
pp: case pos
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✝⁴ : MetricSpace A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
⊢ LipschitzOnWith 1 (fun f ↦ cfcₙ ((toFun {quasispectrum R a}) f) a)
    {f | ContinuousOn ((toFun {quasispectrum R a}) f) (quasispectrum R a) ∧ f 0 = 0}

Tactic:
rintro f ⟨hf, hf0⟩ g ⟨hg, hg0⟩

Goal state after:
case pos
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✝⁴ : MetricSpace A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
f : R →ᵤ[{quasispectrum R a}] R
hf : ContinuousOn ((toFun {quasispectrum R a}) f) (quasispectrum R a)
hf0 : f 0 = 0
g : R →ᵤ[{quasispectrum R a}] R
hg : ContinuousOn ((toFun {quasispectrum R a}) g) (quasispectrum R a)
hg0 : g 0 = 0
⊢ edist ((fun f ↦ cfcₙ ((toFun {quasispectrum R a}) f) a) f) ((fun f ↦ cfcₙ ((toFun {quasispectrum R a}) f) a) g) ≤
    ↑1 * edist f g
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: case e_f.refine_2
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
i : n
⊢ ‖v i‖₊ ≤ Finset.univ.sup fun b ↦ ‖diagonal v i b‖₊

Tactic:
refine Eq.trans_le ?_ (Finset.le_sup (Finset.mem_univ i))
    rw [diagonal_apply_eq]

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

Goal state before:
pp: case inr
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
i : m
x✝ : i ∈ Finset.univ
h✝ : Nonempty n
x : n → α := fun j ↦ unitOf (A i j)
hxn : ‖x‖₊ = 1
hN : ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x i‖₊ ≤ N
⊢ ∑ j, ‖A i j‖₊ ≤ N

Tactic:
dsimp [mulVec, dotProduct] at hN

Goal state after:
case inr
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
i : m
x✝ : i ∈ Finset.univ
h✝ : Nonempty n
x : n → α := fun j ↦ unitOf (A i j)
hxn : ‖x‖₊ = 1
hN : ‖∑ i_1, A i i_1 * x i_1‖₊ ≤ N
⊢ ∑ j, ‖A i j‖₊ ≤ N
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: case pos
𝕜 : 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:
continuousOn_iff_continuous_domRestrict

Goal state after:
case pos
𝕜 : 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
⊢ Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ({a | p a ∧ quasispectrum 𝕜 a ⊆ s}.domRestrict fun x ↦ cfcₙ f x)
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: case e_a.e_a
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
y : ℝ≥0
x✝ : y ∈ σ ℝ≥0 m
⊢ 1 y - g (ε⁻¹ ^ 2 • y) = (1 + ε⁻¹ ^ 2 • y)⁻¹

Tactic:
simp [g, tsub_tsub_cancel_of_le]

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✝ : NormedSpace ℝ A
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 a)
hf₂ : Integrable (fun x ↦ mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
key₁ : ∀ (z : ↑(spectrum 𝕜 a)), ∫ (x : X), f x ↑z ∂μ = (∫ (x : X), mkD ((spectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z
z : ↑(spectrum 𝕜 a)
⊢ ContinuousOn (fun z ↦ ∫ (x : X), f x z ∂μ) (spectrum 𝕜 a)

Tactic:
continuousOn_iff_continuous_domRestrict

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✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : CompleteSpace A
inst✝ : NormedSpace ℝ A
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 a)
hf₂ : Integrable (fun x ↦ mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
key₁ : ∀ (z : ↑(spectrum 𝕜 a)), ∫ (x : X), f x ↑z ∂μ = (∫ (x : X), mkD ((spectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z
z : ↑(spectrum 𝕜 a)
⊢ Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ((spectrum 𝕜 a).domRestrict fun z ↦ ∫ (x : X), f x z ∂μ)
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✝ : NormedSpace ℝ A
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 a)
hf₂ : Integrable (fun x ↦ mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
⊢ cfc (fun z ↦ ∫ (x : X), f x z ∂μ) a = ∫ (x : X), cfc (f x) a ∂μ

Tactic:
by
  have key₁ (z : spectrum 𝕜 a) :
      ∫ x, f x z ∂μ = (∫ x, mkD ((spectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z := by
    rw [integral_apply hf₂]
    refine integral_congr_ae ?_
    filter_upwards [hf₁] with x cont_x
    rw [mkD_apply_of_continuousOn cont_x]
  have key₂ (z : spectrum 𝕜 a) :
      ∫ x, f x z ∂μ = mkD ((spectrum 𝕜 a).domRestrict (fun z ↦ ∫ x, f x z ∂μ)) 0 z := by
    rw [mkD_apply_of_continuousOn]
    rw [continuousOn_iff_continuous_domRestrict]
    refine continuous_congr key₁ |>.mpr ?_
    exact map_continuous (∫ x, mkD ((spectrum 𝕜 a).domRestrict (f x)) 0 ∂μ)
  simp_rw [cfc_eq_cfcL_mkD _ a, cfcL_integral a _ hf₂ ha]
  congr
  ext z
  rw [← key₁, key₂]

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

Goal state before:
pp: 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✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace 𝕜 A
inst✝⁶ : IsScalarTower 𝕜 A A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝³ : CompleteSpace A
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)
hf : ContinuousOn (uncurry f) (univ ×ˢ quasispectrum 𝕜 a)
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound μ
ha : p a
⊢ AEStronglyMeasurable (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ

pp: 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✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace 𝕜 A
inst✝⁶ : IsScalarTower 𝕜 A A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝³ : CompleteSpace A
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)
hf : ContinuousOn (uncurry f) (univ ×ˢ quasispectrum 𝕜 a)
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound μ
ha : p a
⊢ HasFiniteIntegral (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ

Tactic:
· exact aeStronglyMeasurable_mkD_restrict_of_uncurry _ _ hf f_zero

Goal state after:
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✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace 𝕜 A
inst✝⁶ : IsScalarTower 𝕜 A A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝³ : CompleteSpace A
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)
hf : ContinuousOn (uncurry f) (univ ×ˢ quasispectrum 𝕜 a)
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound μ
ha : p a
⊢ HasFiniteIntegral (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: A : Type u_1
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
m : Type u_2
n : Type u_3
inst✝¹ : Fintype m
inst✝ : Fintype n
M : CStarMatrix n n A
v : C⋆ᵐᵒᵈ(A, n → A)
⊢ ‖toCLM Mᴴ ∘SL toCLM M‖ * ‖v‖ ^ 2 = ‖M * star M‖ * ‖v‖ ^ 2

Tactic:
by
                    congr
                    apply MulOpposite.op_injective
                    simp only [← toCLMNonUnitalAlgHom_eq_toCLM, map_mul]
                    rfl

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

Goal state before:
pp: case hf
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
key₁ :
  ∀ (z : ↑(quasispectrum 𝕜 a)), ∫ (x : X), f x ↑z ∂μ = (∫ (x : X), mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z
z : ↑(quasispectrum 𝕜 a)
⊢ ContinuousOn (fun z ↦ ∫ (x : X), f x z ∂μ) (quasispectrum 𝕜 a)

Tactic:
continuousOn_iff_continuous_domRestrict

Goal state after:
case hf
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
key₁ :
  ∀ (z : ↑(quasispectrum 𝕜 a)), ∫ (x : X), f x ↑z ∂μ = (∫ (x : X), mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z
z : ↑(quasispectrum 𝕜 a)
⊢ Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ((quasispectrum 𝕜 a).domRestrict fun z ↦ ∫ (x : X), f x z ∂μ)