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

Goal state before:
pp: case inr
X : Type u_1
inst✝⁵ : TopologicalSpace X
A : Type u_2
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
r : ℝ
hr : r ≤ 0
⊢ φ ((algebraMap ℝ C(X, ℝ)) (- -r)).toNNReal - φ (-(algebraMap ℝ C(X, ℝ)) (- -r)).toNNReal = (algebraMap ℝ A) (- -r)

Tactic:
← map_neg,

Goal state after:
case inr
X : Type u_1
inst✝⁵ : TopologicalSpace X
A : Type u_2
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
r : ℝ
hr : r ≤ 0
⊢ φ ((algebraMap ℝ C(X, ℝ)) (- -r)).toNNReal - φ ((algebraMap ℝ C(X, ℝ)) (- - -r)).toNNReal = (algebraMap ℝ A) (- -r)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝⁶ : TopologicalSpace X
A : Type u_2
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra ℝ A
inst✝² : TopologicalSpace A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
φ ψ : C(↑s, ℝ≥0) →⋆ₐ[ℝ≥0] A
hφ : Continuous[_, inst✝²] ⇑φ
hψ : Continuous[_, inst✝²] ⇑ψ
h : φ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) = ψ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
⊢ φ = ψ

Tactic:
by
    let s' : Set ℝ := (↑) '' s
    let e : s ≃ₜ s' := NNReal.isEmbedding_coe.homeomorphImage s
    have (ξ : C(s, ℝ≥0) →⋆ₐ[ℝ≥0] A) (hξ : Continuous ξ) :
        (let ξ' := ξ.realContinuousMapOfNNReal.comp <| ContinuousMap.compStarAlgHom' ℝ ℝ e
        Continuous ξ' ∧ ξ' (.restrict s' <| .id ℝ) = ξ (.restrict s <| .id ℝ≥0)) := by
      intro ξ'
      refine ⟨ξ.continuous_realContinuousMapOfNNReal hξ |>.comp <|
        ContinuousMap.continuous_precomp _, ?_⟩
      exact ξ.realContinuousMapOfNNReal_apply_comp_toReal (.restrict s <| .id ℝ≥0)
    obtain ⟨hφ', hφ_id⟩ := this φ hφ
    obtain ⟨hψ', hψ_id⟩ := this ψ hψ
    have hs' : CompactSpace s' := e.compactSpace
    have h' := ContinuousMap.UniqueHom.eq_of_continuous_of_map_id s' _ _ hφ' hψ'
      (hφ_id ▸ hψ_id ▸ h)
    have h'' := congr($(h').comp <| ContinuousMap.compStarAlgHom' ℝ ℝ (e.symm : C(s', s)))
    have : (ContinuousMap.compStarAlgHom' ℝ ℝ (e : C(s, s'))).comp
        (ContinuousMap.compStarAlgHom' ℝ ℝ (e.symm : C(s', s))) = StarAlgHom.id _ _ := by
      ext1; simp
    simp only [StarAlgHom.comp_assoc, this, StarAlgHom.comp_id] at h''
    exact StarAlgHom.realContinuousMapOfNNReal_injective h''

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

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
⊢ ∃ g ∈ A, ∀ x ∈ K, ‖g x - f x‖ < ε

Tactic:
let restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C(K, ℝ) :=
    ContinuousMap.compStarAlgHom' ℝ ℝ ⟨(Subtype.val), continuous_subtype_val⟩

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C(↑K, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
⊢ ∃ g ∈ A, ∀ x ∈ K, ‖g x - f x‖ < ε
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
⊢ A.topologicalClosure = ⊤

Tactic:
StarSubalgebra.eq_top_iff

Goal state after:
𝕜 : Type u_1
X : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
⊢ ∀ (x : C(X, 𝕜)), x ∈ A.topologicalClosure
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: case h₁
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
y : E
hy : y ∈ Metric.closedBall 0 1
⊢ ‖(x⋆ * x).toProd.1‖ * ‖↑1 y‖ ≤ ‖(x⋆ * x).toProd.1‖

Tactic:
simpa only [mul_one] using!
        mul_le_mul_of_nonneg_left (mem_closedBall_zero_iff.1 hy) (norm_nonneg (star x * x).fst)

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
s : Set α
x : α
inst✝ : TopologicalSpace β
⊢ UpperHemicontinuousWithinAt f s x ↔ ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝[s] x

Tactic:
simp_rw [upperHemicontinuousWithinAt_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
s : Set α
x : α
inst✝ : TopologicalSpace β
⊢ (∀ t ∈ 𝓝ˢ (f x), ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')) ↔ ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝[s] x
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
hf : UpperHemicontinuous f
hg : UpperHemicontinuous g
⊢ UpperHemicontinuous fun x ↦ f x ∪ g x

Tactic:
by
  rw [upperHemicontinuous_iff] at hf hg ⊢
  exact fun x ↦ (hf x).union (hg x)

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ inst✝ = generateFrom ((fun a ↦ {a_1 | a_1 ∈ a}) '' {U | IsOpen[inst✝] U})

Tactic:
ofPred_mem_eq,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ inst✝ = generateFrom ((fun a ↦ a) '' {U | IsOpen[inst✝] U})
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul : exp a = exp (a - ↑ₐ z) * ↑ₐ (exp z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
hb : Summable fun n ↦ (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
h₀ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = (a - ↑ₐ z) * b
h₁ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = b * (a - ↑ₐ z)
h₃ : exp (a - ↑ₐ z) = 1 + (a - ↑ₐ z) * b
⊢ ¬IsUnit (exp a - 1 * ↑ₐ (exp z))

Tactic:
hexpmul,

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul : exp a = exp (a - ↑ₐ z) * ↑ₐ (exp z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
hb : Summable fun n ↦ (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
h₀ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = (a - ↑ₐ z) * b
h₁ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = b * (a - ↑ₐ z)
h₃ : exp (a - ↑ₐ z) = 1 + (a - ↑ₐ z) * b
⊢ ¬IsUnit (exp (a - ↑ₐ z) * ↑ₐ (exp z) - 1 * ↑ₐ (exp z))
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
l : Filter ↥S
a : ↥S
ha : IsUnit ↑a
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
hla₂ : Tendsto Ring.inverse (map (⇑(val S)) l) (𝓝 ↑ha.unit⁻¹)
x : ↥S
hx : IsUnit x
⊢ Ring.inverse ↑⋯.unit = (val S) ↑hx.unit⁻¹

Tactic:
Ring.inverse_unit (hx.map (val S)).unit,

Goal state after:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
l : Filter ↥S
a : ↥S
ha : IsUnit ↑a
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
hla₂ : Tendsto Ring.inverse (map (⇑(val S)) l) (𝓝 ↑ha.unit⁻¹)
x : ↥S
hx : IsUnit x
⊢ ↑⋯.unit⁻¹ = (val S) ↑hx.unit⁻¹
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case refine_1
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
this : spectrum ℝ a ⊆ Set.Icc (-↑t) ↑t
h : ∀ x ∈ spectrum ℝ a, 0 ≤ x
y : ℝ
hy : y ∈ spectrum ℝ a
hx : ↑t - y ∈ {↑t} - spectrum ℝ a
⊢ ↑‖↑t - y‖₊ ≤ ↑t

Tactic:
obtain ⟨hty, hyt⟩ := Set.mem_Icc.mp <| this hy

Goal state after:
case refine_1
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
this : spectrum ℝ a ⊆ Set.Icc (-↑t) ↑t
h : ∀ x ∈ spectrum ℝ a, 0 ≤ x
y : ℝ
hy : y ∈ spectrum ℝ a
hx : ↑t - y ∈ {↑t} - spectrum ℝ a
hty : -↑t ≤ y
hyt : y ≤ ↑t
⊢ ↑‖↑t - y‖₊ ≤ ↑t
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
⊢ (spectralRadius ℂ (a * a⋆)).toReal = (spectralRadius ℂ (a⋆⋆ * a⋆)).toReal

Tactic:
star_star

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
⊢ (spectralRadius ℂ (a * a⋆)).toReal = (spectralRadius ℂ (a * a⋆)).toReal
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
h : CompactSpace (Compacts α)
⊢ ⋃ K ∈ univ, ↑K = univ

Tactic:
biUnion_univ,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
h : CompactSpace (Compacts α)
⊢ ⋃ x, ↑x = univ
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: case neg
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 x : α
hx : x ∉ K
⊢ f x ∈ closedBall 0 (max C 1)

Tactic:
exact (mem_closedBall.mp <| mem_preimage.mp (hK₂ hx)).trans (le_max_right _ _)

Goal state after:
Module: Mathlib.Analysis.Convex.TotallyBounded

Goal state before:
pp: E : Type u_1
s : Set E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : ∀ U ∈ nhds 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
U : Set E
hU : U ∈ nhds 0
W : Set E
hW₁ : W ∈ nhds 0
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : V ∈ nhds 0
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
t : Set E
htf : t.Finite
hts : s ⊆ ⋃ y ∈ t, y +ᵥ V
t' : Set E
htf' : t'.Finite
hts' : (convexHull ℝ) t ⊆ ⋃ y ∈ t', y +ᵥ V
⊢ ∃ t, t.Finite ∧ (convexHull ℝ) s ⊆ ⋃ y ∈ t, y +ᵥ U

Tactic:
use t', htf'

Goal state after:
case right
E : Type u_1
s : Set E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : ∀ U ∈ nhds 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
U : Set E
hU : U ∈ nhds 0
W : Set E
hW₁ : W ∈ nhds 0
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : V ∈ nhds 0
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
t : Set E
htf : t.Finite
hts : s ⊆ ⋃ y ∈ t, y +ᵥ V
t' : Set E
htf' : t'.Finite
hts' : (convexHull ℝ) t ⊆ ⋃ y ∈ t', y +ᵥ V
⊢ (convexHull ℝ) s ⊆ ⋃ y ∈ t', y +ᵥ U
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
h : CompactSpace (NonemptyCompacts α)
⊢ ⋃ K ∈ univ, ↑K = univ

Tactic:
biUnion_univ,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
h : CompactSpace (NonemptyCompacts α)
⊢ ⋃ x, ↑x = univ
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x✝ : LocallyCompactSpace (NonemptyCompacts α)
x : α
U : Set α
hU : U ∈ 𝓝 x
⊢ ∃ s ∈ 𝓝 x, s ⊆ U ∧ IsCompact s

Tactic:
rw [← mem_interior_iff_mem_nhds, ← singleton_subset_iff, ← coe_singleton] at hU

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
x✝ : LocallyCompactSpace (NonemptyCompacts α)
x : α
U : Set α
hU : ↑{x} ⊆ interior U
⊢ ∃ s ∈ 𝓝 x, s ⊆ U ∧ IsCompact s
Module: Mathlib.Analysis.Normed.Module.Dual

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : StrongDual 𝕜 E
c : 𝕜
hc : ∀ z ∈ s, ‖x' z‖ ≤ ‖c‖
c_zero : c = 0
⊢ 0 ∈ polar 𝕜 s

Tactic:
exact (topDualPairing 𝕜 E).flip.zero_mem_polar _

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

Goal state before:
pp: ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous[inst✝¹, _] ⇑(p i)
bdd : ∀ (x : E), BddAbove (range fun i ↦ (p i) x)
⊢ LowerSemicontinuous (⨆ i, ⇑(p i))

Tactic:
convert! lowerSemicontinuous_ciSup (f := fun i x ↦ p i x) bdd (fun i ↦ (hp i).lowerSemicontinuous)

Goal state after:
case e'_5
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous[inst✝¹, _] ⇑(p i)
bdd : ∀ (x : E), BddAbove (range fun i ↦ (p i) x)
x✝ : E
⊢ (⨆ i, ⇑(p i)) x✝ = ⨆ i, (p i) x✝
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ∈ Icc (approx n c.right x) (approx n c.left x)
c : CU P
⊢ midpoint ℝ (approx n c.right.left x) (approx n c.right.right x) ≤
      midpoint ℝ (approx n c.left x) (approx n c.right x) ∧
    midpoint ℝ (approx n c.left x) (approx n c.right x) ≤ midpoint ℝ (approx n c.left.left x) (approx n c.left.right x)

Tactic:
refine ⟨midpoint_le_midpoint ?_ (ihn _).1, midpoint_le_midpoint (ihn _).2 ?_⟩

Goal state after:
case succ.refine_1
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ∈ Icc (approx n c.right x) (approx n c.left x)
c : CU P
⊢ approx n c.right.left x ≤ approx n c.left x

case succ.refine_2
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ∈ Icc (approx n c.right x) (approx n c.left x)
c : CU P
⊢ approx n c.right x ≤ approx n c.left.right x
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
⊢ Bornology.IsBounded s

Tactic:
obtain ⟨C, hC⟩ := banach_steinhaus (g := fun i : s ↦ WeakDual.toStrongDual i.val) fun x ↦
      let ⟨M, _, hM⟩ := h_ptwise x
      ⟨M, fun i ↦ le_of_lt (hM i.val i.property)⟩

Goal state after:
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
⊢ Bornology.IsBounded s
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
A : ι → Type u_4
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalSemiring R
inst✝¹³ : ContinuousStar R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : (i : ι) → NonUnitalRing (A i)
inst✝⁹ : (i : ι) → Module S (A i)
inst✝⁸ : (i : ι) → Module R (A i)
inst✝⁷ : ∀ (i : ι), IsScalarTower R S (A i)
inst✝⁶ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝⁵ : ∀ (i : ι), IsScalarTower R (A i) (A i)
inst✝⁴ : (i : ι) → StarRing (A i)
inst✝³ : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R ((i : ι) → A i) p
inst✝¹ : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus R (A i) (q i)
inst✝ : ∀ (i : ι), ContinuousMapZero.UniqueHom R (A i)
f : R → R
a : (i : ι) → A i
hf : ContinuousOn f (⋃ i, quasispectrum R (a i))
ha : p a
ha' : ∀ (i : ι), q i (a i)
hf₀ : f 0 = 0
i : ι
this : Nonempty ι
φ : ((i : ι) → A i) →⋆ₙₐ[S] A i := Pi.evalNonUnitalStarAlgHom S A i
⊢ ContinuousOn f (quasispectrum R a)

Tactic:
rwa [Pi.quasispectrum_eq]

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

Goal state before:
pp: case neg
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
a : A
ha : ¬IsSelfAdjoint a
⊢ (-a)⁺ = a⁻

Tactic:
· have ha' : ¬ IsSelfAdjoint (-a) := fun h ↦ ha (by simpa using h.neg)
    rw [posPart_def, negPart_def, cfcₙ_apply_of_not_predicate a ha,
      cfcₙ_apply_of_not_predicate _ ha']

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

Goal state before:
pp: case neg
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 : ℝ≥0
a : A
ha : ¬IsSelfAdjoint a
⊢ (r • a)⁺ = r • a⁺

Tactic:
obtain (rfl | hr) := eq_or_ne r 0

Goal state after:
case neg.inl
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
a : A
ha : ¬IsSelfAdjoint a
⊢ (0 • a)⁺ = 0 • a⁺

case neg.inr
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 : ℝ≥0
a : A
ha : ¬IsSelfAdjoint a
hr : r ≠ 0
⊢ (r • a)⁺ = r • a⁺
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✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
⊢ a⁺ = b ∧ a⁻ = c

Tactic:
have hc' : IsSelfAdjoint (-c) := .neg <| .of_nonneg hc

Goal state after:
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✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
⊢ a⁺ = b ∧ a⁻ = c
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : PseudoEMetricSpace β
x : α
f : α →ᵤ β
⊢ ∀ (y : α →ᵤ β), edist ((fun f ↦ toFun f x) f) ((fun f ↦ toFun f x) y) ≤ ↑1 * edist f y

Tactic:
g

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : PseudoEMetricSpace β
x : α
f g : α →ᵤ β
⊢ edist ((fun f ↦ toFun f x) f) ((fun f ↦ toFun f x) g) ≤ ↑1 * edist f g
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst✝¹ : PseudoEMetricSpace β
inst✝ : Finite ↑𝔖
x : α
hx : x ∈ ⋃₀ 𝔖
f : α →ᵤ[𝔖] β
⊢ ∀ (y : α →ᵤ[𝔖] β), edist ((fun f ↦ (toFun 𝔖) f x) f) ((fun f ↦ (toFun 𝔖) f x) y) ≤ ↑1 * edist f y

Tactic:
g

Goal state after:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst✝¹ : PseudoEMetricSpace β
inst✝ : Finite ↑𝔖
x : α
hx : x ∈ ⋃₀ 𝔖
f g : α →ᵤ[𝔖] β
⊢ edist ((fun f ↦ (toFun 𝔖) f x) f) ((fun f ↦ (toFun 𝔖) f x) g) ≤ ↑1 * edist f g
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

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

Tactic:
rw [SpectrumRestricts.nnreal_iff] at ha₁ ha₂
  apply CFC.eq_zero_of_spectrum_subset_zero (R := ℝ) a
  rw [Set.subset_singleton_iff]
  simp only [← spectrum.neg_eq, Set.mem_neg] at ha₂
  peel ha₁ with x hx _
  linarith [ha₂ (-x) ((neg_neg x).symm ▸ hx)]

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : CStarRing A
inst✝⁵ : NormedSpace ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a b : A
ha : 0 ≤ a
| ‖star (star b) * a * star b‖

Tactic:
star_star

Goal state after:
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : CStarRing A
inst✝⁵ : NormedSpace ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a b : A
ha : 0 ≤ a
| ‖b * a * star b‖
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✝¹ : T2Space A
inst✝ : IsSemitopologicalRing A
a : A
y : ℝ≥0
ha : 0 ≤ a
⊢ a ^ y = cfcₙ (fun x ↦ x ^ ↑y) a

Tactic:
by
  rw [nnrpow_def, cfcₙ_nnreal_eq_real ..]
  refine cfcₙ_congr ?_
  intro x hx
  have : 0 ≤ x := by grind
  simp [this]

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:
simp only [sqrt]

Goal state after:
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
⊢ cfcₙ (⇑NNReal.sqrt) a = a ^ (1 / 2)