mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric

Goal state before:
pp: case inr
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
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
hx' : x ≤ 0
⊢ ‖x‖ = ‖x⁻‖

Tactic:
negPart_eq_neg.mpr hx',

Goal state after:
case inr
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
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
hx' : x ≤ 0
⊢ ‖x‖ = ‖-x‖
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
B : Type u_2
inst✝¹³ : PartialOrder B
inst✝¹² : NonUnitalRing B
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : StarRing B
inst✝⁹ : Module ℝ B
inst✝⁸ : SMulCommClass ℝ B B
inst✝⁷ : IsScalarTower ℝ B B
inst✝⁶ : NonUnitalContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst✝⁴ : IsSemitopologicalRing B
inst✝³ : T2Space B
inst✝² : NonnegSpectrumClass ℝ B
inst✝¹ : NonnegSpectrumClass ℝ (A × B)
inst✝ : StarOrderedRing B
a : A
b : B
x : ℝ≥0
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0.1 ≤ (a, b).1 ∧ 0.2 ≤ (a, b).2

Tactic:
constructor <;> simp [ha, hb]

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
⊢ sqrt a = a ^ (1 / 2)

Tactic:
by
  simp only [sqrt]
  congr
  ext
  exact_mod_cast NNReal.sqrt_eq_rpow _

Goal state after:
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
⊢ a ^ (x + y) = a ^ x * a ^ y

Tactic:
have ha' : 0 ∉ spectrum ℝ≥0 a := spectrum.zero_notMem _ ha
  simp only [rpow_def]
  rw [← cfc_mul _ _ a]
  refine cfc_congr ?_
  intro z hz
  have : z ≠ 0 := by aesop
  simp [NNReal.rpow_add this _ _]

Goal state after:
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
ha : 0 ≤ a
this : IsStrictlyPositive a
⊢ sqrt a ^ x = a ^ (x / 2)

Tactic:
rw [sqrt_eq_rpow, div_eq_mul_inv, one_mul,
      rpow_rpow _ _ _ (by simp), inv_mul_eq_div]

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
ha : IsSelfAdjoint a
hb : IsSelfAdjoint b
⊢ ↑a ≤ ↑b ↔ a ≤ b

Tactic:
rw [← sub_nonneg, ← sub_nonneg (a := b), StarOrderedRing.nonneg_iff_spectrum_nonneg (R := ℝ) _,
    ← inr_sub ℂ b a, ← Unitization.quasispectrum_eq_spectrum_inr' ℝ ℂ]
  exact StarOrderedRing.nonneg_iff_quasispectrum_nonneg _ |>.symm

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

Goal state before:
pp: 𝕜 : 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
s : Set 𝕜
x✝¹ : (𝕜 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] 𝕜) × A
f✝ : 𝕜 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] 𝕜
a✝ : A
x✝ : (f✝, a✝) ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s} ×ˢ {a | p a ∧ s ∈ 𝓝ˢ (spectrum 𝕜 a)}
hf : (f✝, a✝).1 ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s}
ha : p (f✝, a✝).2
has : s ∈ 𝓝ˢ (spectrum 𝕜 (f✝, a✝).2)
hs : IsCompact (spectrum 𝕜 a✝)
k : Set 𝕜
hks : id k ⊆ s
hka : k ∈ 𝓝ˢ (spectrum 𝕜 a✝)
hk : IsCompact k
this : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | k ∈ 𝓝ˢ (spectrum 𝕜 x)}
f : 𝕜 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] 𝕜
a : A
⊢ (f, a) ∈
      {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s} ×ˢ {a | p a ∧ s ∈ 𝓝ˢ (spectrum 𝕜 a)} ∩
        Set.univ ×ˢ {x | k ∈ 𝓝ˢ (spectrum 𝕜 x)} →
    (fun fa ↦ fa) (f, a) ∈ {f | ContinuousOn ((toFun {k}) f) k} ×ˢ {a | p a ∧ spectrum 𝕜 a ⊆ k}

Tactic:
⟨⟨hf, ha⟩, ⟨_, ha'⟩⟩

Goal state after:
𝕜 : 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
s : Set 𝕜
x✝¹ : (𝕜 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] 𝕜) × A
f✝ : 𝕜 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] 𝕜
a✝ : A
x✝ : (f✝, a✝) ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s} ×ˢ {a | p a ∧ s ∈ 𝓝ˢ (spectrum 𝕜 a)}
hf✝ : (f✝, a✝).1 ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s}
ha✝ : p (f✝, a✝).2
has : s ∈ 𝓝ˢ (spectrum 𝕜 (f✝, a✝).2)
hs : IsCompact (spectrum 𝕜 a✝)
k : Set 𝕜
hks : id k ⊆ s
hka : k ∈ 𝓝ˢ (spectrum 𝕜 a✝)
hk : IsCompact k
this : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | k ∈ 𝓝ˢ (spectrum 𝕜 x)}
f : 𝕜 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] 𝕜
a : A
hf : (f, a).1 ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s}
ha : (f, a).2 ∈ {a | p a ∧ s ∈ 𝓝ˢ (spectrum 𝕜 a)}
left✝ : (f, a).1 ∈ Set.univ
ha' : (f, a).2 ∈ {x | k ∈ 𝓝ˢ (spectrum 𝕜 x)}
⊢ (fun fa ↦ fa) (f, a) ∈ {f | ContinuousOn ((toFun {k}) f) k} ×ˢ {a | p a ∧ spectrum 𝕜 a ⊆ k}
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
⊢ star a * a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)

Tactic:
by
  have : star a * a ≤ algebraMap ℝ A ‖star a * a‖ := IsSelfAdjoint.le_algebraMap_norm_self
  rwa [CStarRing.norm_star_mul_self, ← pow_two] at this

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

Goal state before:
pp: 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
s : Set ℝ≥0
x✝¹ : (ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0) × A
f✝ : ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0
a✝ : A
x✝ : (f✝, a✝) ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s} ×ˢ {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (spectrum ℝ≥0 a)}
hf : (f✝, a✝).1 ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s}
ha : 0 ≤ (f✝, a✝).2
has : s ∈ 𝓝ˢ (spectrum ℝ≥0 (f✝, a✝).2)
hs : IsCompact (spectrum ℝ≥0 a✝)
k : Set ℝ≥0
hks : id k ⊆ s
hka : k ∈ 𝓝ˢ (spectrum ℝ≥0 a✝)
hk : IsCompact k
this : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | k ∈ 𝓝ˢ (spectrum ℝ≥0 x)}
f : ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0
a : A
⊢ (f, a) ∈
      {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s} ×ˢ {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (spectrum ℝ≥0 a)} ∩
        Set.univ ×ˢ {x | k ∈ 𝓝ˢ (spectrum ℝ≥0 x)} →
    (fun fa ↦ fa) (f, a) ∈ {f | ContinuousOn ((toFun {k}) f) k} ×ˢ {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ k}

Tactic:
⟨⟨hf, ha⟩, ⟨_, ha'⟩⟩

Goal state after:
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
s : Set ℝ≥0
x✝¹ : (ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0) × A
f✝ : ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0
a✝ : A
x✝ : (f✝, a✝) ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s} ×ˢ {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (spectrum ℝ≥0 a)}
hf✝ : (f✝, a✝).1 ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s}
ha✝ : 0 ≤ (f✝, a✝).2
has : s ∈ 𝓝ˢ (spectrum ℝ≥0 (f✝, a✝).2)
hs : IsCompact (spectrum ℝ≥0 a✝)
k : Set ℝ≥0
hks : id k ⊆ s
hka : k ∈ 𝓝ˢ (spectrum ℝ≥0 a✝)
hk : IsCompact k
this : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | k ∈ 𝓝ˢ (spectrum ℝ≥0 x)}
f : ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0
a : A
hf : (f, a).1 ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s}
ha : (f, a).2 ∈ {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (spectrum ℝ≥0 a)}
left✝ : (f, a).1 ∈ Set.univ
ha' : (f, a).2 ∈ {x | k ∈ 𝓝ˢ (spectrum ℝ≥0 x)}
⊢ (fun fa ↦ fa) (f, a) ∈ {f | ContinuousOn ((toFun {k}) f) k} ×ˢ {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ k}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ e✝ : A
he✝ : IsStarProjection e✝
ha✝ : 0 ≤ a✝
hae : a✝ ≤ e✝
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
⊢ a ≤ e → a * e = a

Tactic:
hae

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ e✝ : A
he✝ : IsStarProjection e✝
ha✝ : 0 ≤ a✝
hae✝ : a✝ ≤ e✝
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
⊢ a * e = a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a e : A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
⊢ a * e = a ∧ e * a = a

Tactic:
by
  suffices a * e = a from
    ⟨this, by simpa [ha.star_eq, he.isSelfAdjoint.star_eq] using congr(star $this)⟩
  suffices ∀ a e : A⁺¹, IsStarProjection e → 0 ≤ a → a ≤ e → a * e = a from
    mod_cast this a e he.inr ha.inr (inr_le_iff a e |>.mpr hae)
  intro a e he ha hae
  suffices sqrt a * (1 - e : A⁺¹) = 0 by
    simpa [← mul_assoc, sqrt_mul_sqrt_self a, mul_sub, sub_eq_zero, eq_comm (a := a)]
      using congr(sqrt a * $this)
  rw [← norm_eq_zero, ← sq_eq_zero_iff, ← norm_star_mul_mul_self_of_nonneg, norm_eq_zero]
  refine le_antisymm ?_ <| star_left_conjugate_nonneg ha _
  grw [star_left_conjugate_le_conjugate hae (1 - e), mul_assoc, he.mul_one_sub_self, mul_zero]

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

Goal state before:
pp: X : Type u_1
A : Type u_2
inst✝¹⁰ : NormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : NormedAlgebra ℝ A
inst✝⁷ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁶ : ContinuousStar A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : TopologicalSpace X
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
ha_cont : ContinuousOn a t
ha : ∀ x ∈ t, spectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
⊢ 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.Matrix.Normed

Goal state before:
pp: 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✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
i : l
_hi : i ∈ Finset.univ
⊢ ∑ j, ‖A i j‖₊ * ∑ k, ‖B j k‖₊ ≤ ∑ j, ‖A i j‖₊ * Finset.univ.sup fun i ↦ ∑ j, ‖B i j‖₊

Tactic:
gcongr with j hj

Goal state after:
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✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
i : l
_hi : i ∈ Finset.univ
j : m
hj : j ∈ Finset.univ
⊢ ∑ k, ‖B j k‖₊ ≤ Finset.univ.sup fun i ↦ ∑ j, ‖B i j‖₊
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: 𝕜 : 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
s : Set 𝕜
x✝¹ : (𝕜 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] 𝕜) × A
f✝ : 𝕜 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] 𝕜
a✝ : A
x✝ :
  (f✝, a✝) ∈
    {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ {a | p a ∧ s ∈ 𝓝ˢ (quasispectrum 𝕜 a)}
hf : (f✝, a✝).1 ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0}
ha : p (f✝, a✝).2
has : s ∈ 𝓝ˢ (quasispectrum 𝕜 (f✝, a✝).2)
hs : IsCompact (quasispectrum 𝕜 a✝)
k : Set 𝕜
hks : id k ⊆ s
hka : k ∈ 𝓝ˢ (quasispectrum 𝕜 a✝)
hk : IsCompact k
this : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | k ∈ 𝓝ˢ (quasispectrum 𝕜 x)}
f : 𝕜 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] 𝕜
a : A
⊢ (f, a) ∈
      {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ {a | p a ∧ s ∈ 𝓝ˢ (quasispectrum 𝕜 a)} ∩
        Set.univ ×ˢ {x | k ∈ 𝓝ˢ (quasispectrum 𝕜 x)} →
    (fun fa ↦ fa) (f, a) ∈ {f | ContinuousOn ((toFun {k}) f) k ∧ f 0 = 0} ×ˢ {a | p a ∧ quasispectrum 𝕜 a ⊆ k}

Tactic:
⟨⟨hf, ha⟩, ⟨_, ha'⟩⟩

Goal state after:
𝕜 : 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
s : Set 𝕜
x✝¹ : (𝕜 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] 𝕜) × A
f✝ : 𝕜 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] 𝕜
a✝ : A
x✝ :
  (f✝, a✝) ∈
    {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ {a | p a ∧ s ∈ 𝓝ˢ (quasispectrum 𝕜 a)}
hf✝ : (f✝, a✝).1 ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0}
ha✝ : p (f✝, a✝).2
has : s ∈ 𝓝ˢ (quasispectrum 𝕜 (f✝, a✝).2)
hs : IsCompact (quasispectrum 𝕜 a✝)
k : Set 𝕜
hks : id k ⊆ s
hka : k ∈ 𝓝ˢ (quasispectrum 𝕜 a✝)
hk : IsCompact k
this : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | k ∈ 𝓝ˢ (quasispectrum 𝕜 x)}
f : 𝕜 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] 𝕜
a : A
hf : (f, a).1 ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0}
ha : (f, a).2 ∈ {a | p a ∧ s ∈ 𝓝ˢ (quasispectrum 𝕜 a)}
left✝ : (f, a).1 ∈ Set.univ
ha' : (f, a).2 ∈ {x | k ∈ 𝓝ˢ (quasispectrum 𝕜 x)}
⊢ (fun fa ↦ fa) (f, a) ∈ {f | ContinuousOn ((toFun {k}) f) k ∧ f 0 = 0} ×ˢ {a | p a ∧ quasispectrum 𝕜 a ⊆ k}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute

Goal state before:
pp: case pos
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
inst✝² : PartialOrder A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : StarOrderedRing A
a b : A
hb : Commute a b
f : ℝ≥0 → ℝ≥0
ha : 0 ≤ a
⊢ Commute (cfc f a) b

pp: case neg
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
inst✝² : PartialOrder A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : StarOrderedRing A
a b : A
hb : Commute a b
f : ℝ≥0 → ℝ≥0
ha : ¬0 ≤ a
⊢ Commute (cfc f a) b

Tactic:
· rw [cfc_nnreal_eq_real ..]
    exact hb.cfc_real _

Goal state after:
case neg
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
inst✝² : PartialOrder A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : StarOrderedRing A
a b : A
hb : Commute a b
f : ℝ≥0 → ℝ≥0
ha : ¬0 ≤ a
⊢ Commute (cfc f a) b
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: 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
s : Set ℝ≥0
x✝¹ : (ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0) × A
f✝ : ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0
a✝ : A
x✝ :
  (f✝, a✝) ∈
    {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)}
hf : (f✝, a✝).1 ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0}
ha : 0 ≤ (f✝, a✝).2
has : s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (f✝, a✝).2)
hs : IsCompact (quasispectrum ℝ≥0 a✝)
k : Set ℝ≥0
hks : id k ⊆ s
hka : k ∈ 𝓝ˢ (quasispectrum ℝ≥0 a✝)
hk : IsCompact k
this : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | k ∈ 𝓝ˢ (quasispectrum ℝ≥0 x)}
f : ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0
a : A
⊢ (f, a) ∈
      {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ
          {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)} ∩
        Set.univ ×ˢ {x | k ∈ 𝓝ˢ (quasispectrum ℝ≥0 x)} →
    (fun fa ↦ fa) (f, a) ∈ {f | ContinuousOn ((toFun {k}) f) k ∧ f 0 = 0} ×ˢ {a | 0 ≤ a ∧ quasispectrum ℝ≥0 a ⊆ k}

Tactic:
⟨⟨hf, ha⟩, ⟨_, ha'⟩⟩

Goal state after:
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
s : Set ℝ≥0
x✝¹ : (ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0) × A
f✝ : ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0
a✝ : A
x✝ :
  (f✝, a✝) ∈
    {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)}
hf✝ : (f✝, a✝).1 ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0}
ha✝ : 0 ≤ (f✝, a✝).2
has : s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (f✝, a✝).2)
hs : IsCompact (quasispectrum ℝ≥0 a✝)
k : Set ℝ≥0
hks : id k ⊆ s
hka : k ∈ 𝓝ˢ (quasispectrum ℝ≥0 a✝)
hk : IsCompact k
this : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | k ∈ 𝓝ˢ (quasispectrum ℝ≥0 x)}
f : ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0
a : A
hf : (f, a).1 ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0}
ha : (f, a).2 ∈ {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)}
left✝ : (f, a).1 ∈ Set.univ
ha' : (f, a).2 ∈ {x | k ∈ 𝓝ˢ (quasispectrum ℝ≥0 x)}
⊢ (fun fa ↦ fa) (f, a) ∈ {f | ContinuousOn ((toFun {k}) f) k ∧ f 0 = 0} ×ˢ {a | 0 ≤ a ∧ quasispectrum ℝ≥0 a ⊆ k}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral

Goal state before:
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:
· refine hasFiniteIntegral_mkD_restrict_of_bound f _ ?_ f_zero bound bound_int bound_ge
    exact .of_forall fun x ↦
      hf.comp (Continuous.prodMk_right x).continuousOn fun _ hz ↦ ⟨Set.mem_univ _, hz⟩

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
x✝¹ x✝ : A
c : Completion f.PreGNS
⊢ (f.leftMulMapPreGNS (x✝¹ + x✝)).completion c =
    ((f.leftMulMapPreGNS x✝¹).completion + (f.leftMulMapPreGNS x✝).completion) c

Tactic:
induction c using induction_on with

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
x✝¹ x✝ : A
c : Completion f.PreGNS
⊢ (f.leftMulMapPreGNS (x✝¹ * x✝)).completion c =
    ((f.leftMulMapPreGNS x✝¹).completion * (f.leftMulMapPreGNS x✝).completion) c

Tactic:
induction c using induction_on with

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

Goal state before:
pp: case refine_2
e : AddChar ℝ Circle
x : ℝ
h : ↑⟨↑(e x), ?refine_1⟩⁻¹ = (starRingEnd ℂ) ↑⟨↑(e x), ?refine_1⟩
⊢ star ↑(e x) = ↑(e (-x))

pp: case refine_1
e : AddChar ℝ Circle
x : ℝ
⊢ ↑(e x) ∈ Submonoid.unitSphere ℂ

Tactic:
· simp [← h, e.map_neg_eq_inv]

Goal state after:
case refine_1
e : AddChar ℝ Circle
x : ℝ
⊢ ↑(e x) ∈ Submonoid.unitSphere ℂ
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: case refine_3
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
e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯
⊢ (↑e z).1 ∈ s ∩ (a.pretrivializationAt z.proj).baseSet

Tactic:
e.coe_fst

Goal state after:
case refine_3
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
e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯
⊢ z.proj ∈ s ∩ (a.pretrivializationAt z.proj).baseSet

case refine_3
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
e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯
⊢ z ∈ e.source