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

Goal state before:
pp: 𝕜 : 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
hf : ContinuousOn f (σₙ 𝕜 a)
hf₀ : f 0 = 0
ha : p a
⊢ IsGreatest ((fun x ↦ ‖f x‖) '' σₙ 𝕜 a) ‖cfcₙ f a‖

Tactic:
by
  obtain ⟨x, hx⟩ := NonUnitalContinuousFunctionalCalculus.isCompact_quasispectrum a
      |>.image_of_continuousOn hf.norm |>.exists_isGreatest <|
      (quasispectrum.nonempty 𝕜 a).image _
  obtain ⟨x, hx', rfl⟩ := hx.1
  convert! hx
  rw [cfcₙ_apply f a, norm_cfcₙHom a _]
  apply le_antisymm
  · apply ContinuousMap.norm_le _ (norm_nonneg _) |>.mpr
    rintro ⟨y, hy⟩
    exact hx.2 ⟨y, hy, rfl⟩
  · exact le_trans (by simp) <| ContinuousMap.norm_coe_le_norm _ (⟨x, hx'⟩ : σₙ 𝕜 a)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²⁵ : Semifield R
inst✝²⁴ : StarRing R
inst✝²³ : MetricSpace R
inst✝²² : IsTopologicalSemiring R
inst✝²¹ : ContinuousStar R
inst✝²⁰ : Field S
inst✝¹⁹ : StarRing S
inst✝¹⁸ : MetricSpace S
inst✝¹⁷ : IsTopologicalRing S
inst✝¹⁶ : ContinuousStar S
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : StarRing A
inst✝¹³ : Module S A
inst✝¹² : IsScalarTower S A A
inst✝¹¹ : SMulCommClass S A A
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module R A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : StarModule R S
inst✝⁶ : ContinuousSMul R S
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : MetricSpace A
inst✝² : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
ha' : q a
haf : QuasispectrumRestricts a ⇑f
this : NonUnitalContinuousFunctionalCalculus R A p
g₁ g₂ : ContinuousMapZero (↑(σₙ R a)) R
x : ↑(σₙ R a)
x' : ↑(σₙ S a) := Subtype.map ⇑(algebraMap R S) ⋯ x
⊢ dist (↑g₁ x) (↑g₂ x) =
    dist
      (↑({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
            (g₁.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ }))
        x')
      (↑({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
            (g₂.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ }))
        x')

Tactic:
simp only [ContinuousMapZero.comp_apply, ContinuousMapZero.coe_mk,
        ContinuousMap.coe_mk, StarAlgHom.ofId_apply, halg.dist_eq, x']

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²⁵ : Semifield R
inst✝²⁴ : StarRing R
inst✝²³ : MetricSpace R
inst✝²² : IsTopologicalSemiring R
inst✝²¹ : ContinuousStar R
inst✝²⁰ : Field S
inst✝¹⁹ : StarRing S
inst✝¹⁸ : MetricSpace S
inst✝¹⁷ : IsTopologicalRing S
inst✝¹⁶ : ContinuousStar S
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : StarRing A
inst✝¹³ : Module S A
inst✝¹² : IsScalarTower S A A
inst✝¹¹ : SMulCommClass S A A
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module R A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : StarModule R S
inst✝⁶ : ContinuousSMul R S
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : MetricSpace A
inst✝² : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
ha' : q a
haf : QuasispectrumRestricts a ⇑f
this : NonUnitalContinuousFunctionalCalculus R A p
g₁ g₂ : ContinuousMapZero (↑(σₙ R a)) R
x : ↑(σₙ R a)
x' : ↑(σₙ S a) := Subtype.map ⇑(algebraMap R S) ⋯ x
⊢ dist (g₁ x) (g₂ x) =
    dist (g₁ (Subtype.map ⇑f ⋯ (Subtype.map ⇑(algebraMap R S) ⋯ x)))
      (g₂ (Subtype.map ⇑f ⋯ (Subtype.map ⇑(algebraMap R S) ⋯ x)))
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
x : ℝ≥0
hx : x ∈ σ ℝ≥0 a
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
⊢ f x ≤ ‖cfc f a‖₊

Tactic:
by
  revert hx
  nontriviality A
  exact (IsGreatest.nnnorm_cfc_nnreal f a hf ha |>.2 ⟨x, ·, rfl⟩)

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
this : IsConnected ((σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im} ∪ (σ ℂ a)ᶜ ∩ {z | z.im ≤ 0})
⊢ IsConnected (σ ℂ a)ᶜ

Tactic:
by
    rw [← Set.inter_union_distrib_left, ← Set.ofPred_or] at this
    rw [← Set.inter_univ (σ ℂ a)ᶜ]
    convert this
    exact Eq.symm <| Set.eq_univ_of_forall (fun z ↦ le_total 0 z.im)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝³] U
hKu₁ : ↑K ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, (↑K ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : ↑K ⊆ interior L
hLu : L ⊆ ⋃₀ u
U : Set α
hU : U ∈ u
x : α
hxK : x ∈ ↑K
hxU : x ∈ U
M : Set α
hM : IsCompact M
right✝ : x ∈ interior M ∧ M ⊆ U ∩ interior L
⊢ ∃ M, IsCompact M ∧ M ⊆ L ∧ M ⊆ U ∧ (↑K ∩ interior M).Nonempty

Tactic:
exact ⟨M, hM, by grind [interior_subset], by grind, x, by grind⟩

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

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : Zero β
inst✝¹ : FunLike F α β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ ⇑f ⁻¹' closedBall 0 1
C : ℝ
hC : ⇑f '' K ⊆ closedBall 0 C
⊢ ∃ C, ∀ (x y : α), dist (f x) (f y) ≤ C

Tactic:
refine ⟨max C 1 + max C 1, fun x y => ?_⟩

Goal state after:
F : Type u_1
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : Zero β
inst✝¹ : FunLike F α β
inst✝ : ZeroAtInftyContinuousMapClass F α β
f : F
K : Set α
hK₁ : IsCompact K
hK₂ : Kᶜ ⊆ ⇑f ⁻¹' closedBall 0 1
C : ℝ
hC : ⇑f '' K ⊆ closedBall 0 C
x y : α
⊢ dist (f x) (f y) ≤ max C 1 + max C 1
Module: Mathlib.Analysis.CStarAlgebra.Fuglede

Goal state before:
pp: case e'_5
A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
⊢ NormedSpace.exp (z • star b) * NormedSpace.exp (-((starRingEnd ℂ) z • b)) =
    NormedSpace.exp (z • star b + -((starRingEnd ℂ) z • b))

Tactic:
grind [exp_add_of_commute, Commute.smul_right, Commute.neg_right]

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

Goal state before:
pp: case e'_6
A : Type u_1
inst✝² : CStarAlgebra A
a b x : A
inst✝¹ : IsStarNormal a
inst✝ : IsStarNormal b
h : SemiconjBy x a b
z : ℂ
x✝ : NormedAlgebra ℚ A := NormedAlgebra.restrictScalars ℚ ℂ A
⊢ NormedSpace.exp ((starRingEnd ℂ) z • a) * NormedSpace.exp (-(z • star a)) =
    NormedSpace.exp ((starRingEnd ℂ) z • a + -(z • star a))

Tactic:
grind [exp_add_of_commute, Commute.smul_right, Commute.neg_right]

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

Goal state before:
pp: E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : PolynormableSpace 𝕜 E
S : Submodule 𝕜 E
f : StrongDual 𝕜 ↥S
⊢ ∃ g, ∀ (x : ↥S), g ↑x = f x

Tactic:
obtain ⟨q, hq_cont, hq⟩ := Seminorm.exists_le_comp_of_isInducing (f := S.subtype)
    (p := f.toSeminorm) f.continuous.norm IsInducing.subtypeVal
  obtain ⟨g, hg, _⟩ := Dual.exists_continuous_extension_of_le_seminorm S f.toLinearMap hq_cont hq
  exact ⟨g, hg⟩

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

Goal state before:
pp: 𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : ‖x‖ ≠ 0
⊢ ∃ g, ‖g‖ = 1 ∧ g x = ↑‖x‖

Tactic:
by
  have hhomothety := LinearEquiv.toSpanNonzeroSingleton_homothety 𝕜 x (ne_zero_of_norm_ne_zero h)
  let coord : span 𝕜 {x} →L[𝕜] 𝕜 := (ofHomothety _ _ (by positivity) hhomothety).symm
  obtain ⟨g, hg⟩ := exists_extension_norm_eq (span 𝕜 {x}) ((‖x‖ : 𝕜) • coord)
  have hval : g x = ‖x‖ := by
    have hgx : g x = g (⟨x, by simp⟩ : span 𝕜 {x}) := by rw [Submodule.coe_mk]
    have hcx : coord ⟨x, _⟩ = 1 := LinearEquiv.coord_self 𝕜 E x (ne_zero_of_norm_ne_zero h)
    simp [-algebraMap_smul, hgx, ↓hg.left, hcx]
  refine ⟨g, le_antisymm ?_ ?_, hval⟩
  · simp only [hg.right, norm_smul, norm_algebraMap', norm_norm]
    grw [coord.opNorm_le_bound (by positivity)
      (fun y ↦ (homothety_inverse _ (by positivity) _ hhomothety y).le), mul_inv_cancel₀ h]
  · have hle := g.le_opNorm x
    simp only [hval, norm_algebraMap', norm_norm] at hle
    exact one_le_of_le_mul_right₀ (by positivity) hle

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Extend

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : StrongDual ℝ F
x : F
⊢ ‖fr.extendRCLike x‖ ≤ ‖fr‖ * ‖x‖

Tactic:
by
  refine Module.Dual.norm_extendRCLike_le_seminorm (p := ‖fr‖₊ • normSeminorm 𝕜 F)
    fr.toLinearMap ?_ x
  simp [← Real.norm_eq_abs, NNReal.smul_def, le_opNorm]

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
n : ℕ
x : X
hx : x ∈ c.C
⊢ approx n c x = 0

Tactic:
induction n generalizing c with
  | zero => exact indicator_of_notMem (fun (hU : x ∈ c.Uᶜ) => hU <| c.subset hx) _
  | succ n ihn =>
    simp only [approx]
    rw [ihn, ihn, midpoint_self]
    exacts [c.subset_right_C hx, hx]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁸ : Field k
inst✝⁷ : LinearOrder k
inst✝⁶ : IsStrictOrderedRing k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
a b : E
r r' : k
h : r < r'
⊢ (1 - r) • a ≤ (1 - r') • a + (r' • b - r • b) ↔ a ≤ b

Tactic:
← sub_le_iff_le_add',

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁸ : Field k
inst✝⁷ : LinearOrder k
inst✝⁶ : IsStrictOrderedRing k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
a b : E
r r' : k
h : r < r'
⊢ (1 - r) • a - (1 - r') • a ≤ r' • b - r • b ↔ a ≤ 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
h's : IsGδ s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hU : s = ⋂ n, U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
n : ℕ
⊢ Disjoint s (U n ∩ interior m)ᶜ

Tactic:
rw [disjoint_compl_right_iff_subset]

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
h's : IsGδ s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
U : ℕ → Set X
U_open : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hU : s = ⋂ n, U n
m : Set X
m_comp : IsCompact m
sm : s ⊆ interior m
mt : m ⊆ tᶜ
n : ℕ
⊢ s ⊆ U n ∩ interior m
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
inst✝ : PseudoEMetricSpace β
this : 𝓤 (α →ᵤ β) = comap (fun x ↦ edist x.1 x.2) (𝓝 0)
⊢ 𝓤 (α →ᵤ β) = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}

Tactic:
by
      simp [this, ENNReal.nhds_zero_basis.comap _ |>.eq_biInf, Set.Iio]

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

Goal state before:
pp: case refine_3
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
φ ψ : ↑(characterSpace ℂ ↥(elemental ℂ a))
h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ
⊢ φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩

Tactic:
simpa only [characterSpaceToSpectrum, Subtype.mk_eq_mk,
      ContinuousMap.coe_mk] using h

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsStarNormal a
this : Isometry ⇑((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a))
⊢ ∀ (f : C(↑(spectrum ℂ a), ℂ)),
    spectrum ℂ (((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a)) f) = Set.range ⇑f

Tactic:
intro f
      simp only [StarAlgHom.comp_apply, StarAlgHom.coe_coe, StarSubalgebra.coe_subtype]
      rw [← StarSubalgebra.spectrum_eq (hS := StarAlgebra.elemental.isClosed ℂ a),
        AlgEquiv.spectrum_eq (continuousFunctionalCalculus a), ContinuousMap.spectrum_eq_range]

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 : ℝ
ha : IsStrictlyPositive a
⊢ a ^ x * a ^ (-x) = 1

Tactic:
← rpow_add ha.isUnit,

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 : ℝ
ha : IsStrictlyPositive a
⊢ a ^ (x + -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 : ℝ
ha : IsStrictlyPositive a
⊢ a ^ (-x) * a ^ x = 1

Tactic:
← rpow_add ha.isUnit,

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 : ℝ
ha : IsStrictlyPositive a
⊢ a ^ (-x + x) = 1
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: case inr
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 : ℝ≥0
htriv : 0 ≤ a
h₁ : 0 < x
h₂ : ↑x / 2 = ↑(x / 2)
h₃ : 0 < x / 2
⊢ sqrt (a ^ x) = a ^ ↑(x / 2)

Tactic:
← nnrpow_eq_rpow h₃,

Goal state after:
case inr
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 : ℝ≥0
htriv : 0 ≤ a
h₁ : 0 < x
h₂ : ↑x / 2 = ↑(x / 2)
h₃ : 0 < x / 2
⊢ sqrt (a ^ x) = a ^ (x / 2)
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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
⊢ Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ({a | p a ∧ spectrum 𝕜 a ⊆ s}.domRestrict (cfc f))

Tactic:
by
    convert!
      continuous_cfcHomSuperset_left hs ⟨_, hf.domRestrict⟩
        ((↑) : {a | p a ∧ spectrum 𝕜 a ⊆ s} → A)
        continuous_subtype_val (fun x ↦ x.2.2) with
      x
    rw [cfcHomSuperset_apply, Set.domRestrict_apply, cfc_apply _ _ x.2.1 (hf.mono x.2.2)]
    congr!

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)}
⊢ ∃ t,
    IsOpen[instTopologicalSpaceProd] t ∧
      (f, a) ∈ t ∧
        ContinuousOn (fun fa ↦ cfc ((toFun {s}) fa.1) fa.2)
          ({f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s} ×ˢ {a | p a ∧ s ∈ 𝓝ˢ (spectrum 𝕜 a)} ∩ t)

Tactic:
refine ⟨Set.univ ×ˢ {x | k ∈ 𝓝ˢ (spectrum 𝕜 x)}, isOpen_univ.prod this, by simpa, ?_⟩

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)}
⊢ ContinuousOn (fun fa ↦ cfc ((toFun {s}) fa.1) fa.2)
    ({f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s} ×ˢ {a | p a ∧ s ∈ 𝓝ˢ (spectrum 𝕜 a)} ∩
      Set.univ ×ˢ {x | k ∈ 𝓝ˢ (spectrum 𝕜 x)})
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
ha : IsSelfAdjoint a
⊢ -(algebraMap ℝ A) ‖a‖ ≤ a

Tactic:
rw [neg_le, ← norm_neg]
  exact ha.neg.le_algebraMap_norm_self

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

Goal state before:
pp: case neg.inr
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
ha : ¬IsStrictlyPositive a
ha' : ¬IsUnit (sqrt a)
H : ¬IsUnit a
⊢ sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ

Tactic:
· simp [inverse_non_unit _ ha', inverse_non_unit _ H]

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
hb✝ : IsSelfAdjoint b✝
a b : Unitization ℂ A
hb : IsSelfAdjoint b
⊢ star a * (algebraMap ℝ (Unitization ℂ A)) ‖b‖ * a = ‖b‖ • (star a * a)

Tactic:
by simp [Algebra.algebraMap_eq_smul_one]

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
hb : IsSelfAdjoint b
⊢ star a * b * a ≤ ‖b‖ • (star a * a)

Tactic:
suffices ∀ a b : A⁺¹, IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a) by
    rw [← Unitization.inr_le_iff _ _ (by aesop) ((IsSelfAdjoint.all _).smul (.star_mul_self a))]
    simpa [Unitization.norm_inr] using this a b <| hb.inr ℂ
  intro a b hb
  calc
    star a * b * a ≤ star a * (algebraMap ℝ A⁺¹ ‖b‖) * a :=
      star_left_conjugate_le_conjugate hb.le_algebraMap_norm_self _
    _ = ‖b‖ • (star a * a) := by simp [Algebra.algebraMap_eq_smul_one]

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
f : ℝ≥0 → ℝ≥0 := fun x ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x ↦ x * (1 - x)⁻¹
this : ∀ (a b : A), 0 ≤ a → 0 ≤ b → ‖a‖ < 1 → ‖b‖ < 1 → a ≤ cfcₙ f (cfcₙ g a + cfcₙ g b)
a : A
ha₁ : 0 ≤ a
ha₂ : a ∈ Metric.ball 0 1
b : A
hb₁ : 0 ≤ b
hb₂ : b ∈ Metric.ball 0 1
⊢ ∃ z ∈ {x | 0 ≤ x} ∩ Metric.ball 0 1, (fun x1 x2 ↦ x1 ≤ x2) a z ∧ (fun x1 x2 ↦ x1 ≤ x2) b z

Tactic:
simp only [Metric.mem_ball, dist_zero_right] at ha₂ hb₂

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x ↦ x * (1 - x)⁻¹
this : ∀ (a b : A), 0 ≤ a → 0 ≤ b → ‖a‖ < 1 → ‖b‖ < 1 → a ≤ cfcₙ f (cfcₙ g a + cfcₙ g b)
a : A
ha₁ : 0 ≤ a
b : A
hb₁ : 0 ≤ b
ha₂ : ‖a‖ < 1
hb₂ : ‖b‖ < 1
⊢ ∃ z ∈ {x | 0 ≤ x} ∩ Metric.ball 0 1, (fun x1 x2 ↦ x1 ≤ x2) a z ∧ (fun x1 x2 ↦ x1 ≤ x2) b z
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x ↦ x * (1 - x)⁻¹
this : ∀ (a b : A), 0 ≤ a → 0 ≤ b → ‖a‖ < 1 → ‖b‖ < 1 → a ≤ cfcₙ f (cfcₙ g a + cfcₙ g b)
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) ({x | 0 ≤ x} ∩ Metric.ball 0 1)

Tactic:
by
    rintro a ⟨(ha₁ : 0 ≤ a), ha₂⟩ b ⟨(hb₁ : 0 ≤ b), hb₂⟩
    simp only [Metric.mem_ball, dist_zero_right] at ha₂ hb₂
    refine ⟨cfcₙ f (cfcₙ g a + cfcₙ g b), ⟨by simp, ?_⟩, ?_, ?_⟩
    · simpa only [Metric.mem_ball, dist_zero_right] using norm_cfcₙ_one_sub_one_add_inv_lt_one _
    · exact this a b ha₁ hb₁ ha₂ hb₂
    · exact add_comm (cfcₙ g a) (cfcₙ g b) ▸ this b a hb₁ ha₁ hb₂ ha₂

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

Goal state before:
pp: A : Type u_2
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ c ^ 2
⊢ ‖1 * z - y * z‖₊ ≤ sqrt (c ^ 2)

Tactic:
le_sqrt_iff_sq_le,

Goal state after:
A : Type u_2
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ c ^ 2
⊢ ‖1 * z - y * z‖₊ ^ 2 ≤ c ^ 2
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
ε : ℝ≥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
⊢ Continuous g

Tactic:
rw [← continuousOn_univ]

Goal state after:
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
⊢ ContinuousOn g Set.univ