mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.WeakDual

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
s : Set (WeakDual 𝕜 E)
h_vN : IsVonNBounded 𝕜 s
h_ptwise : ∀ (i : E), ∃ r > 0, ∀ x ∈ s, (seminormFamily 𝕜 E i) x < r
C : ℝ
hC : ∀ (i : ↑s), ‖toStrongDual ↑i‖ ≤ C
⊢ ∃ C, ∀ x ∈ ⇑StrongDual.toWeakDual ⁻¹' s, ‖x‖ ≤ C

Tactic:
exact ⟨C, fun f hf ↦ hC ⟨StrongDual.toWeakDual f, hf⟩⟩

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

Goal state before:
pp: A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (fun x ↦ x⁺ - x⁻) a = cfcₙ id a

Tactic:
congr! 2 with

Goal state after:
case e'_17
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x✝ : ℝ
⊢ x✝⁺ - x✝⁻ = id x✝
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi

Goal state before:
pp: A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst✝²⁸ : CommSemiring R
inst✝²⁷ : CommRing S
inst✝²⁶ : Nontrivial R
inst✝²⁵ : StarRing R
inst✝²⁴ : MetricSpace R
inst✝²³ : IsTopologicalSemiring R
inst✝²² : ContinuousStar R
inst✝²¹ : Algebra R S
inst✝²⁰ : NonUnitalRing A
inst✝¹⁹ : NonUnitalRing B
inst✝¹⁸ : Module S A
inst✝¹⁷ : Module R A
inst✝¹⁶ : Module R B
inst✝¹⁵ : Module S B
inst✝¹⁴ : SMulCommClass R A A
inst✝¹³ : SMulCommClass R B B
inst✝¹² : IsScalarTower R A A
inst✝¹¹ : IsScalarTower R B B
inst✝¹⁰ : StarRing A
inst✝⁹ : StarRing B
inst✝⁸ : TopologicalSpace A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : IsScalarTower R S B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst✝⁴ : NonUnitalContinuousFunctionalCalculus R (A × B) pab
inst✝³ : NonUnitalContinuousFunctionalCalculus R A pa
inst✝² : NonUnitalContinuousFunctionalCalculus R B pb
inst✝¹ : ContinuousMapZero.UniqueHom R A
inst✝ : ContinuousMapZero.UniqueHom R B
f : R → R
a : A
b : B
hf : ContinuousOn f (quasispectrum R a ∪ quasispectrum R b)
hab : pab (a, b)
ha : pa a
hb : pb b
hf₀ : ¬f 0 = 0
⊢ cfcₙ f (a, b) = (cfcₙ f a, cfcₙ f b)

Tactic:
simp [cfcₙ_apply_of_not_map_zero _ hf₀, eqComm]

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

Goal state before:
pp: A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : T2Space A
inst✝ : StarModule ℝ A
r : ℝ
hr : r ≤ 0
a : A
⊢ (r • a)⁺ = -r • a⁻

Tactic:
by
  nth_rw 1 [← neg_neg r]
  rw [neg_smul, ← smul_neg, posPart_smul_of_nonneg (neg_nonneg.mpr hr), posPart_neg]

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
K V : Set X
hK : IsCompact K
hV : IsOpen[inst✝²] V
hKV : K ⊆ V
⊢ ∃ f, EqOn (⇑f) 1 K ∧ IsCompact (tsupport ⇑f) ∧ tsupport ⇑f ⊆ V ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
obtain ⟨U, hU1, hU2, hU3, hU4⟩ := exists_open_between_and_isCompact_closure hK hV hKV
  obtain ⟨f, hf1, hf2, hf3⟩ := exists_tsupport_one_of_isOpen_isClosed hU1 hU4
    isClosed_closure (hK.closure_subset_of_isOpen hU1 hU2)
  have hfU : tsupport f ⊆ closure U := hf1.trans subset_closure
  exact ⟨f, hf2.mono subset_closure,
    .of_isClosed_subset hU4 isClosed_closure hfU, hfU.trans hU3, hf3⟩

Goal state after:
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
inst✝ : PseudoEMetricSpace β
⊢ 𝓤 (α →ᵤ β) = ⨅ i, ⨅ (_ : 0 < i), 𝓟 ((fun x ↦ edist x.1 x.2) ⁻¹' Set.Iic i)

Tactic:
rw [UniformFun.hasBasis_uniformity_of_basis α β uniformity_basis_edist_le |>.eq_biInf]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
inst✝ : PseudoEMetricSpace β
⊢ ⨅ i, ⨅ (_ : 0 < i), 𝓟 ((UniformFun.gen α β ∘ fun ε ↦ {p | edist p.1 p.2 ≤ ε}) i) =
    ⨅ i, ⨅ (_ : 0 < i), 𝓟 ((fun x ↦ edist x.1 x.2) ⁻¹' Set.Iic i)
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace γ
inst✝¹ : PseudoMetricSpace β
inst✝ : BoundedSpace β
⊢ Metric.ediam Set.univ ≠ ∞

Tactic:
← lt_top_iff_ne_top

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace γ
inst✝¹ : PseudoMetricSpace β
inst✝ : BoundedSpace β
⊢ Metric.ediam Set.univ < ∞
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst✝¹ : PseudoEMetricSpace β
inst✝ : Finite ↑𝔖
x✝ : Fintype ↑𝔖 := Fintype.ofFinite ↑𝔖
⊢ 𝓤 (α →ᵤ[𝔖] β) = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}

Tactic:
simp_rw [← isUniformInducing_pi_restrict.comap_uniformity,
      PseudoEMetricSpace.uniformity_edist, comap_iInf, comap_principal, edist_eq_pi_restrict,
      Set.preimage_ofPred_eq]

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
⊢ ∃ φ,
    Continuous ⇑φ ∧
      Function.Injective ⇑φ ∧
        φ (ContinuousMap.restrict (spectrum ℂ a) (ContinuousMap.id ℂ)) = a ∧
          (∀ (f : C(↑(spectrum ℂ a), ℂ)), spectrum ℂ (φ f) = Set.range ⇑f) ∧
            ∀ (f : C(↑(spectrum ℂ a), ℂ)), IsStarNormal (φ f)

Tactic:
have : Isometry ((StarAlgebra.elemental ℂ a).subtype.comp <| continuousFunctionalCalculus a :
        C(spectrum ℂ a, ℂ) →⋆ₐ[ℂ] A) :=
      isometry_subtype_coe.comp <| StarAlgEquiv.isometry (continuousFunctionalCalculus a)
    refine ⟨_, this.continuous, this.injective, ?hom_id, ?hom_map_spectrum, ?predicate_hom⟩
    case hom_id => exact congr_arg Subtype.val <| continuousFunctionalCalculus_map_id a
    case hom_map_spectrum =>
      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]
    case predicate_hom => exact fun f ↦ ⟨by rw [← map_star]; exact Commute.all (star f) f |>.map _⟩

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

Goal state before:
pp: case h₁
A : Type u_1
inst✝ : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hb₂ : SpectrumRestricts b ⇑ContinuousMap.realToNNReal
⊢ ‖(algebraMap ℝ A) ↑‖a‖₊ - a‖₊ ≤ ‖a‖₊

pp: case h₂
A : Type u_1
inst✝ : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hb₂ : SpectrumRestricts b ⇑ContinuousMap.realToNNReal
⊢ ‖(algebraMap ℝ A) ↑‖b‖₊ - b‖₊ ≤ ‖b‖₊

Tactic:
all_goals rw [← SpectrumRestricts.nnreal_iff_nnnorm] <;> first | rfl | assumption

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

Goal state before:
pp: case mpr.add
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x✝¹ : PartialOrder A := spectralOrder A
x✝ p x y : A
hx✝ : x ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
hy✝ : y ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
hx : IsSelfAdjoint x ∧ QuasispectrumRestricts x ⇑ContinuousMap.realToNNReal
hy : IsSelfAdjoint y ∧ QuasispectrumRestricts y ⇑ContinuousMap.realToNNReal
⊢ IsSelfAdjoint (x + y) ∧ QuasispectrumRestricts (x + y) ⇑ContinuousMap.realToNNReal

Tactic:
| add x y _ _ hx hy =>

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
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x y : ℝ≥0
ha : 0 ≤ a
⊢ (a ^ x) ^ y = a ^ (x * y)

Tactic:
obtain (rfl | hx) := eq_zero_or_pos x <;> obtain (rfl | hy) := eq_zero_or_pos y
    all_goals try simp
    simp only [nnrpow_def]
    rw [← cfcₙ_comp _ _ a]
    congr! 2 with u
    ext
    simp [Real.rpow_mul]

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
⊢ Set.EqOn (fun a ↦ a ^ 0) (fun x ↦ 1) (Set.Ici 0)

Tactic:
intro a ha
  simp [rpow_zero a ha]

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

Goal state before:
pp: X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst✝¹⁰ : CommSemiring R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : TopologicalSpace X
f : X → R → R
a : A
s : Set X
h_cont : ContinuousOn (fun x ↦ (ofFun {spectrum R a}) (f x)) s
hf : ∀ x ∈ s, ContinuousOn (f x) (spectrum R a)
⊢ ContinuousOn (fun x ↦ cfc (f x) a) s

Tactic:
rw [ContinuousOn] at h_cont ⊢

Goal state after:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst✝¹⁰ : CommSemiring R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R A p
inst✝ : TopologicalSpace X
f : X → R → R
a : A
s : Set X
h_cont : ∀ x ∈ s, ContinuousWithinAt (fun x ↦ (ofFun {spectrum R a}) (f x)) s x
hf : ∀ x ∈ s, ContinuousOn (f x) (spectrum R a)
⊢ ∀ x ∈ s, ContinuousWithinAt (fun x ↦ cfc (f x) a) s x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: R : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : MetricSpace A
inst✝¹ : Algebra R A
inst✝ : IsometricContinuousFunctionalCalculus R A p
a : A
s : Set R
hs : spectrum R a ⊆ s
⊢ LipschitzOnWith 1 (fun f ↦ cfc ((toFun {s}) f) a) {f | ContinuousOn ((toFun {s}) f) s}

Tactic:
have h₁ := lipschitzOnWith_cfc_fun R a

Goal state after:
R : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : MetricSpace A
inst✝¹ : Algebra R A
inst✝ : IsometricContinuousFunctionalCalculus R A p
a : A
s : Set R
hs : spectrum R a ⊆ s
h₁ :
  LipschitzOnWith 1 (fun f ↦ cfc ((toFun {spectrum R a}) f) a)
    {f | ContinuousOn ((toFun {spectrum R a}) f) (spectrum R a)}
⊢ LipschitzOnWith 1 (fun f ↦ cfc ((toFun {s}) f) a) {f | ContinuousOn ((toFun {s}) f) s}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : ContinuousStar A
inst✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
f : C(↑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)
⊢ CompactSpace ↑s

Tactic:
isCompact_iff_compactSpace

Goal state after:
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 : CompactSpace ↑s
f : C(↑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)
⊢ CompactSpace ↑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
ha : 0 ≤ a
⊢ sqrt (a ^ 2) = a

Tactic:
rw [pow_two, sqrt_mul_self (A := A) a]

Goal state after:
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ˣ
ha : 0 ≤ ↑a
hab : ‖star (sqrt ↑a * sqrt ↑b⁻¹) * (sqrt ↑a * sqrt ↑b⁻¹)‖ ≤ 1
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ‖sqrt ↑b⁻¹ * sqrt ↑a‖ * ‖sqrt ↑b⁻¹ * sqrt ↑a‖ ≤ 1

Tactic:
← CStarRing.norm_self_mul_star

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ‖star (sqrt ↑a * sqrt ↑b⁻¹) * (sqrt ↑a * sqrt ↑b⁻¹)‖ ≤ 1
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ‖sqrt ↑b⁻¹ * sqrt ↑a * star (sqrt ↑b⁻¹ * sqrt ↑a)‖ ≤ 1
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), IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a)

Tactic:
intro a b hb

Goal state after:
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 * b * a ≤ ‖b‖ • (star a * a)
Module: Mathlib.Analysis.CStarAlgebra.Module.Defs

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
⊢ ‖x‖ ^ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2

Tactic:
by simp only [add_pow_two, add_left_inj]; ring

Goal state after:
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 : 1 ≤ a
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
⊢ ∀ x ∈ spectrum ℝ a, x ^ n ≤ x ^ m

Tactic:
rw [CFC.one_le_iff (R := ℝ) a] at ha

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ∀ x ∈ spectrum ℝ a, 1 ≤ x
ha' : 0 ≤ a
n m : ℕ
hnm : n ≤ m
⊢ ∀ x ∈ spectrum ℝ a, x ^ n ≤ x ^ m
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
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ max ‖x.1‖ ‖x.2‖ ≤ ‖x‖

Tactic:
rw [prod_norm]

Goal state after:
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
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ max ‖x.1‖ ‖x.2‖ ≤ √‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
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✝⁵ : TopologicalSpace A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : TopologicalSpace X
f : X → R → R
a : A
s : Set X
h_cont : ContinuousOn (fun x ↦ (ofFun {quasispectrum R a}) (f x)) s
hf : ∀ x ∈ s, ContinuousOn (f x) (quasispectrum R a)
hf0 : ∀ x ∈ s, f x 0 = 0
⊢ ContinuousOn (fun x ↦ cfcₙ (f x) a) s

Tactic:
rw [ContinuousOn] at h_cont ⊢

Goal state after:
X : Type u_1
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✝⁵ : TopologicalSpace A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : TopologicalSpace X
f : X → R → R
a : A
s : Set X
h_cont : ∀ x ∈ s, ContinuousWithinAt (fun x ↦ (ofFun {quasispectrum R a}) (f x)) s x
hf : ∀ x ∈ s, ContinuousOn (f x) (quasispectrum R a)
hf0 : ∀ x ∈ s, f x 0 = 0
⊢ ∀ x ∈ s, ContinuousWithinAt (fun x ↦ cfcₙ (f x) a) s x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : 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)
f : C(↑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)
⊢ CompactSpace ↑s

Tactic:
isCompact_iff_compactSpace

Goal state after:
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 : CompactSpace ↑s
hs0 : Fact (0 ∈ s)
f : C(↑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)
⊢ CompactSpace ↑s
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖A‖ = ↑(Finset.univ.sup fun i ↦ ∑ j, ‖A i j‖₊)

Tactic:
change ‖fun i => toLp 1 (A i)‖ = _
  simp [Pi.norm_def, PiLp.nnnorm_eq_of_L1]

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

Goal state before:
pp: n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i ↦ (i, i), inj' := ⋯ } Finset.univ
i : n × n
_hi : i ∈ Finset.univ
his : i ∉ s
this : i.1 ≠ i.2
⊢ 0 ^ 2 = 0

Tactic:
NNReal.zero_rpow two_ne_zero

Goal state after:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i ↦ (i, i), inj' := ⋯ } Finset.univ
i : n × n
_hi : i ∈ Finset.univ
his : i ∉ s
this : i.1 ≠ i.2
⊢ 0 = 0
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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
hf0 : f 0 = 0
hs0 : 0 ∈ s
x : ↑{a | p a ∧ quasispectrum 𝕜 a ⊆ s}
⊢ cfcₙ f ↑x =
    (cfcₙHom ⋯)
      ({ toFun := s.domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 }.comp
        { toFun := Subtype.map id ⋯, continuous_toFun := ⋯, map_zero' := ⋯ })

Tactic:
cfcₙ_apply _ _ (hf.mono x.2.2) hf0 x.2.1

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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
hf0 : f 0 = 0
hs0 : 0 ∈ s
x : ↑{a | p a ∧ quasispectrum 𝕜 a ⊆ s}
⊢ (cfcₙHom ⋯) { toFun := (quasispectrum 𝕜 ↑x).domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 } =
    (cfcₙHom ⋯)
      ({ toFun := s.domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 }.comp
        { toFun := Subtype.map id ⋯, continuous_toFun := ⋯, map_zero' := ⋯ })
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: case h₁
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
this : star m * (1 - cfc g (ε⁻¹ ^ 2 • m)) * m = cfc (fun y ↦ y * (1 + ε⁻¹ ^ 2 • y)⁻¹ * y) m
y : ℝ≥0
hy : y ∈ σ ℝ≥0 m
hm' : ‖m‖ ≤ 1
⊢ y ≤ 1

Tactic:
norm_le_one_iff_of_nonneg m hm₁,

Goal state after:
case h₁
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
this : star m * (1 - cfc g (ε⁻¹ ^ 2 • m)) * m = cfc (fun y ↦ y * (1 + ε⁻¹ ^ 2 • y)⁻¹ * y) m
y : ℝ≥0
hy : y ∈ σ ℝ≥0 m
hm' : m ≤ 1
⊢ y ≤ 1
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute

Goal state before:
pp: case frequently
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f : C(↑(quasispectrum 𝕜 a), 𝕜)₀
hf : ∃ᶠ (g : C(↑(quasispectrum 𝕜 a), 𝕜)₀) in nhds f, Commute ((cfcₙHom ha) g) b
⊢ Filter.Tendsto (⇑(cfcₙHom ha)) (nhds f) (nhds ((cfcₙHom ha) f))

Tactic:
exact cfcₙHom_continuous ha |>.tendsto _

Goal state after: