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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
r : ℝ
hr : 0 < r
⊢ {a | 0 ≤ a} ⊆ ↑(span ℂ ({x | 0 ≤ x} ∩ Metric.closedBall 0 r))

Tactic:
intro x

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
r : ℝ
hr : 0 < r
x : A
⊢ x ∈ {a | 0 ≤ a} → x ∈ ↑(span ℂ ({x | 0 ≤ x} ∩ Metric.closedBall 0 r))
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
y : ℝ
ha : 0 ≤ a
⊢ Set.EqOn (fun x ↦ ↑(x.toNNReal ^ y)) (fun x ↦ x ^ y) (spectrum ℝ a)

Tactic:
intro x

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
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
y : ℝ
ha : 0 ≤ a
x : ℝ
⊢ x ∈ spectrum ℝ a → (fun x ↦ ↑(x.toNNReal ^ y)) x = (fun x ↦ x ^ y) x
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
⊢ ∀ (i : ℝ),
    0 < i →
      ∃ F,
        Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
          ∀ (y : X), ((cfcHomSuperset ⋯ ⋯) f, F y) ∈ {p | dist p.1 p.2 ≤ i}

Tactic:
intro ε hε

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 < ε
⊢ ∃ F,
    Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
      ∀ (y : X), ((cfcHomSuperset ⋯ ⋯) f, F y) ∈ {p | dist p.1 p.2 ≤ ε}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConvexOn ℝ s (inr ∘ f)
⊢ ∀ ⦃x : A⦄, x ∈ s → ∀ ⦃y : A⦄, y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y

Tactic:
intro x

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConvexOn ℝ s (inr ∘ f)
x : A
⊢ x ∈ s → ∀ ⦃y : A⦄, y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConcaveOn ℝ s (inr ∘ f)
⊢ ∀ ⦃x : A⦄, x ∈ s → ∀ ⦃y : A⦄, y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)

Tactic:
intro x

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConcaveOn ℝ s (inr ∘ f)
x : A
⊢ x ∈ s → ∀ ⦃y : A⦄, y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝³ : CStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Nontrivial A
a : A
ha : 0 ≤ a
this : IsSelfAdjoint a
⊢ (spectrum ℝ a).Nonempty

Tactic:
exact this.spectrumRestricts.image ▸ (spectrum.nonempty a).image _

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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
this : Set.EqOn (cfc f) (cfc fun x ↦ ↑(f x.toNNReal)) {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
⊢ Set.MapsTo (Real.toNNReal ∘ NNReal.toReal) s s

Tactic:
intro x

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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
this : Set.EqOn (cfc f) (cfc fun x ↦ ↑(f x.toNNReal)) {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
x : ℝ≥0
⊢ x ∈ s → (Real.toNNReal ∘ NNReal.toReal) x ∈ s
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
tfae_1_iff_8 : IsStrictlyPositive a ↔ 0 ≤ a ∧ IsUnit a
tfae_1_iff_9 : IsStrictlyPositive a ↔ IsSelfAdjoint a ∧ ∀ x ∈ spectrum ℝ a, 0 < x
tfae_1_to_2 : IsStrictlyPositive a → IsStrictlyPositive (sqrt a) ∧ a = sqrt a * sqrt a
tfae_2_to_3 : IsStrictlyPositive (sqrt a) ∧ a = sqrt a * sqrt a → IsUnit (sqrt a) ∧ a = sqrt a * sqrt a
⊢ [IsStrictlyPositive a, IsStrictlyPositive (sqrt a) ∧ a = sqrt a * sqrt a, IsUnit (sqrt a) ∧ a = sqrt a * sqrt a,
      ∃ b, IsStrictlyPositive b ∧ a = b * b, ∃ b, IsUnit b ∧ IsSelfAdjoint b ∧ a = b * b,
      ∃ b, IsUnit b ∧ a = star b * b, ∃ b, IsUnit b ∧ a = b * star b, 0 ≤ a ∧ IsUnit a,
      IsSelfAdjoint a ∧ ∀ x ∈ spectrum ℝ a, 0 < x].TFAE

Tactic:
tfae_have 3 → 4 := fun h => ⟨sqrt a, h.1.isStrictlyPositive (sqrt_nonneg _), h.2⟩

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
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
tfae_1_iff_8 : IsStrictlyPositive a ↔ 0 ≤ a ∧ IsUnit a
tfae_1_iff_9 : IsStrictlyPositive a ↔ IsSelfAdjoint a ∧ ∀ x ∈ spectrum ℝ a, 0 < x
tfae_1_to_2 : IsStrictlyPositive a → IsStrictlyPositive (sqrt a) ∧ a = sqrt a * sqrt a
tfae_2_to_3 : IsStrictlyPositive (sqrt a) ∧ a = sqrt a * sqrt a → IsUnit (sqrt a) ∧ a = sqrt a * sqrt a
tfae_3_to_4 : IsUnit (sqrt a) ∧ a = sqrt a * sqrt a → ∃ b, IsStrictlyPositive b ∧ a = b * b
⊢ [IsStrictlyPositive a, IsStrictlyPositive (sqrt a) ∧ a = sqrt a * sqrt a, IsUnit (sqrt a) ∧ a = sqrt a * sqrt a,
      ∃ b, IsStrictlyPositive b ∧ a = b * b, ∃ b, IsUnit b ∧ IsSelfAdjoint b ∧ a = b * b,
      ∃ b, IsUnit b ∧ a = star b * b, ∃ b, IsUnit b ∧ a = b * star b, 0 ≤ a ∧ IsUnit a,
      IsSelfAdjoint a ∧ ∀ x ∈ spectrum ℝ a, 0 < x].TFAE
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: case pos
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : f 0 = 0
h₁ : inr ∘ cfcₙ f = fun x ↦ ↑(cfcₙ f x)
h₂ : (fun x ↦ ↑(cfcₙ f x)) = fun x ↦ cfc f ↑x
h₃ : ConvexOn ℝ (⇑inrl ⁻¹' ⇑inrl '' s) (cfc f ∘ ⇑inrl)
⊢ ConvexOn ℝ s fun x ↦ cfc f ↑x

Tactic:
rwa [Set.preimage_image_eq _ inrHom_injective] at h₃

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
⊢ Set.EqOn (fun x ↦ 1 - (1 + x)⁻¹) (fun x ↦ ↑(1 - (1 + x.toNNReal)⁻¹)) (σₙ ℝ a)

Tactic:
intro x

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
x : ℝ
⊢ x ∈ σₙ ℝ a → (fun x ↦ 1 - (1 + x)⁻¹) x = (fun x ↦ ↑(1 - (1 + x.toNNReal)⁻¹)) x
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
x : ℝ
hx : x ∈ σₙ ℝ a
hx' : 0 ≤ x
⊢ (fun x ↦ 1 - (1 + x)⁻¹) x = (fun x ↦ ↑(1 - (1 + x.toNNReal)⁻¹)) x

Tactic:
simp [hx']

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
⊢ Set.EqOn (fun x ↦ ↑(1 - (1 + x.toNNReal)⁻¹)) (fun x ↦ 1 - (1 + x)⁻¹) (σₙ ℝ b)

Tactic:
intro x

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
x : ℝ
⊢ x ∈ σₙ ℝ b → (fun x ↦ ↑(1 - (1 + x.toNNReal)⁻¹)) x = (fun x ↦ 1 - (1 + x)⁻¹) x
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
x : ℝ
hx : x ∈ σₙ ℝ b
hx' : 0 ≤ x
⊢ (fun x ↦ ↑(1 - (1 + x.toNNReal)⁻¹)) x = (fun x ↦ 1 - (1 + x)⁻¹) x

Tactic:
simp [hx']

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

Goal state before:
pp: case left
this : (fun x ↦ x * (1 + x)⁻¹) = fun x ↦ 1 - (1 + x)⁻¹
⊢ LeftInvOn (fun x ↦ x * (1 + x)⁻¹) (fun x ↦ x * (1 - x)⁻¹) {x | x < 1}

Tactic:
intro x

Goal state after:
case left
this : (fun x ↦ x * (1 + x)⁻¹) = fun x ↦ 1 - (1 + x)⁻¹
x : ℝ≥0
⊢ x ∈ {x | x < 1} → (fun x ↦ x * (1 + x)⁻¹) ((fun x ↦ x * (1 - x)⁻¹) x) = x
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: case right
this : (fun x ↦ x * (1 + x)⁻¹) = fun x ↦ 1 - (1 + x)⁻¹
⊢ RightInvOn (fun x ↦ x * (1 + x)⁻¹) (fun x ↦ x * (1 - x)⁻¹) {x | x < 1}

Tactic:
intro x

Goal state after:
case right
this : (fun x ↦ x * (1 + x)⁻¹) = fun x ↦ 1 - (1 + x)⁻¹
x : ℝ≥0
⊢ x ∈ {x | x < 1} → (fun x ↦ x * (1 - x)⁻¹) ((fun x ↦ x * (1 + x)⁻¹) x) = x
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝ m : A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
⊢ ∀ (ib : ℝ), 0 < ib → ∃ ia, (0 ≤ ia ∧ ‖ia‖ < 1) ∧ ∀ x ∈ {x | ia ≤ x} ∩ closedBall 0 1, x * m ∈ closedBall m ib

Tactic:
intro ε hε

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝ m : A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
ε : ℝ
hε : 0 < ε
⊢ ∃ ia, (0 ≤ ia ∧ ‖ia‖ < 1) ∧ ∀ x ∈ {x | ia ≤ x} ∩ closedBall 0 1, x * m ∈ closedBall m ε
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✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (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 ↦ (cfcₙHomSuperset ⋯ ⋯) g
⊢ ∀ (i : ℝ),
    0 < i →
      ∃ F,
        Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
          ∀ (y : X), ((cfcₙHomSuperset ⋯ ⋯) f, F y) ∈ {p | dist p.1 p.2 ≤ i}

Tactic:
intro ε hε

Goal state after:
case frequently
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✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (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 ↦ (cfcₙHomSuperset ⋯ ⋯) g
ε : ℝ
hε : 0 < ε
⊢ ∃ F,
    Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
      ∀ (y : X), ((cfcₙHomSuperset ⋯ ⋯) f, F y) ∈ {p | dist p.1 p.2 ≤ ε}
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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
hf0 : f 0 = 0
this : Set.EqOn (cfcₙ f) (cfcₙ fun x ↦ ↑(f x.toNNReal)) {a | 0 ≤ a ∧ quasispectrum ℝ≥0 a ⊆ s}
⊢ Set.MapsTo (Real.toNNReal ∘ NNReal.toReal) s s

Tactic:
intro x

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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
hf0 : f 0 = 0
this : Set.EqOn (cfcₙ f) (cfcₙ fun x ↦ ↑(f x.toNNReal)) {a | 0 ≤ a ∧ quasispectrum ℝ≥0 a ⊆ s}
x : ℝ≥0
⊢ x ∈ s → (Real.toNNReal ∘ NNReal.toReal) x ∈ s
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
z : ↑(spectrum 𝕜 a)
x : X
cont_x : ContinuousOn (f x) (spectrum 𝕜 a)
⊢ f x ↑z = (mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) z

Tactic:
rw [mkD_apply_of_continuousOn cont_x]

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

Goal state before:
pp: A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : Module ℂ A
inst✝³ : IsScalarTower ℂ A A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : StarModule ℂ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
x : ℂ
hx : x ∈ quasispectrum ℂ a
⊢ ↑x.re = 2⁻¹ • (x + star x)

Tactic:
Complex.re_eq_add_conj,

Goal state after:
A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : Module ℂ A
inst✝³ : IsScalarTower ℂ A A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : StarModule ℂ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
x : ℂ
hx : x ∈ quasispectrum ℂ a
⊢ (x + (starRingEnd ℂ) x) / 2 = 2⁻¹ • (x + star x)
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
f : X → 𝕜 → 𝕜
a : A
hf : Integrable (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
x : X
| cfcₙ (f x) a

Tactic:
cfcₙ_eq_cfcₙL_mkD _ a

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
f : X → 𝕜 → 𝕜
a : A
hf : Integrable (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
x : X
| (cfcₙL ha) (mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0)
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
x : ℂ
hx : x ∈ spectrum ℂ a
⊢ ↑x.re = 2⁻¹ • (x + star x)

Tactic:
Complex.re_eq_add_conj,

Goal state after:
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
x : ℂ
hx : x ∈ spectrum ℂ a
⊢ (x + (starRingEnd ℂ) x) / 2 = 2⁻¹ • (x + star x)
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
⊢ cfcₙ (fun z ↦ ∫ (x : X), f x z ∂μ) a = ∫ (x : X), cfcₙ (f x) a ∂μ

Tactic:
have key₁ (z : quasispectrum 𝕜 a) :
      ∫ x, f x z ∂μ = (∫ x, mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z := by
    rw [integral_apply hf₃]
    refine integral_congr_ae ?_
    filter_upwards [hf₁, hf₂] with x cont_x zero_x
    rw [mkD_apply_of_continuousOn cont_x zero_x]

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
key₁ :
  ∀ (z : ↑(quasispectrum 𝕜 a)), ∫ (x : X), f x ↑z ∂μ = (∫ (x : X), mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z
⊢ cfcₙ (fun z ↦ ∫ (x : X), f x z ∂μ) a = ∫ (x : X), cfcₙ (f x) a ∂μ
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart

Goal state before:
pp: A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra ℂ A
inst✝² : StarModule ℂ A
inst✝¹ : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝ : ContinuousMap.UniqueHom ℂ A
f : ℂ → ℂ
a : A
hf : ContinuousOn f (spectrum ℂ ↑(ℜ a))
ha : IsStarNormal a
⊢ cfc f ↑(ℜ a) = cfc (fun x ↦ f ↑x.re) a

Tactic:
rw [spectrum_realPart a] at hf

Goal state after:
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra ℂ A
inst✝² : StarModule ℂ A
inst✝¹ : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝ : ContinuousMap.UniqueHom ℂ A
f : ℂ → ℂ
a : A
hf : ContinuousOn f ((fun x ↦ ↑x.re) '' spectrum ℂ a)
ha : IsStarNormal a
⊢ cfc f ↑(ℜ a) = cfc (fun x ↦ f ↑x.re) a
Module: Mathlib.Analysis.InnerProductSpace.Dual

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := ⋯
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
intro x

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ).ker
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x : E
y : F
hx : (x, y) ∈ s ×ˢ t
h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → (x, y) ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y)
⊢ ∀ ⦃x₁ : E⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → (x, y).1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).1

Tactic:
rintro x₁ hx₁ x₂ hx₂ hx_fst
    refine congrArg Prod.fst (h (mk_mem_prod hx₁ hx.2) (mk_mem_prod hx₂ hx.2) ?_)
    rw [← Prod.image_mk_openSegment_left]
    exact mem_image_of_mem _ hx_fst

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
a : A
⊢ ∀ (x y : Completion f.PreGNS),
    ⟪(f.leftMulMapPreGNS (star a)).completion x, y⟫_ℂ = ⟪x, (f.leftMulMapPreGNS a).completion y⟫_ℂ

Tactic:
intro x

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
a : A
x : Completion f.PreGNS
⊢ ∀ (y : Completion f.PreGNS),
    ⟪(f.leftMulMapPreGNS (star a)).completion x, y⟫_ℂ = ⟪x, (f.leftMulMapPreGNS a).completion y⟫_ℂ
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: case a
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
⊢ ∀ x ∈ Multiset.map (fun x ↦ ‖U i x‖ ^ 2) Finset.univ.val, 0 ≤ x

Tactic:
intro x

Goal state after:
case a
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
x : ℝ
⊢ x ∈ Multiset.map (fun x ↦ ‖U i x‖ ^ 2) Finset.univ.val → 0 ≤ x