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

Goal state before:
pp: X : Type u_1
inst✝⁹ : TopologicalSpace X
inst✝⁸ : Zero X
A : Type u_2
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : TopologicalSpace A
inst✝³ : IsSemitopologicalRing A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : SMulCommClass ℝ A A
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
h0 : Fact (0 ∈ s)
φ ψ : C(↑s, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hφ : Continuous[_, inst✝⁴] ⇑φ
hψ : Continuous[_, inst✝⁴] ⇑ψ
h : φ (ContinuousMapZero.id s) = ψ (ContinuousMapZero.id s)
s' : Set ℝ := toReal '' s
e : ↑s ≃ₜ ↑s' := isEmbedding_coe.homeomorphImage s
this✝¹ : Fact (0 ∈ s')
e0 : e 0 = 0
e0' : e.symm 0 = 0
this✝ :
  ∀ (ξ : C(↑s, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A),
    Continuous[_, inst✝⁴] ⇑ξ →
      let ξ' :=
        ξ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 });
      Continuous[_, inst✝⁴] ⇑ξ' ∧ ξ' (ContinuousMapZero.id s') = ξ (ContinuousMapZero.id s)
hφ' :
  Continuous[_, inst✝⁴]
    ⇑(φ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }))
hφ_id :
  (φ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }))
      (ContinuousMapZero.id s') =
    φ (ContinuousMapZero.id s)
hψ' :
  Continuous[_, inst✝⁴]
    ⇑(ψ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }))
hψ_id :
  (ψ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }))
      (ContinuousMapZero.id s') =
    ψ (ContinuousMapZero.id s)
hs' : CompactSpace ↑s'
this : ContinuousMapZero.UniqueHom ℝ A
h' :
  φ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }) =
    ψ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 })
h'' :
  (φ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 })).comp
      (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e.symm, map_zero' := e0' }) =
    (ψ.realContinuousMapZeroOfNNReal.comp
          (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 })).comp
      (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e.symm, map_zero' := e0' })
x✝¹ : C(↑s, ℝ)₀
x✝ : ↑s
⊢ (((nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }).comp
          (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e.symm, map_zero' := e0' }))
        x✝¹)
      x✝ =
    ((NonUnitalStarAlgHom.id ℝ C(↑s, ℝ)₀) x✝¹) x✝

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C(↑s, 𝕜)
⊢ f ∈ ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) → f ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))

Tactic:
hf

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C(↑s, 𝕜)
hf : f ∈ ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
⊢ f ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case id
𝕜 : Type u_2
A : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalSemiring A
inst✝⁷ : Star A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : SeparatelyContinuousMul A
inst✝⁴ : T2Space A
inst✝³ : DistribMulAction 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : φ (ContinuousMapZero.id s) * a = 0
hmul_star_id : φ (star (ContinuousMapZero.id s)) * a = 0
hφ : Continuous ⇑φ
⊢ φ (ContinuousMapZero.id s) * a = 0

Tactic:
exact hmul_id

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

Goal state before:
pp: case id
𝕜 : Type u_2
A : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalSemiring A
inst✝⁷ : Star A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : SeparatelyContinuousMul A
inst✝⁴ : T2Space A
inst✝³ : DistribMulAction 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : a * φ (ContinuousMapZero.id s) = 0
hmul_star_id : a * φ (star (ContinuousMapZero.id s)) = 0
hφ : Continuous ⇑φ
⊢ a * φ (ContinuousMapZero.id s) = 0

Tactic:
exact hmul_id

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 : Set β), IsOpen[inst✝] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ u

Tactic:
rw [upperHemicontinuousWithinAt_iff, hasBasis_nhdsSet _ |>.forall_iff ?mono]
  case mono => exact fun t₁ t₂ ht h ↦ h.mp <| .of_forall fun x' ↦ by gcongr
  simp only [and_imp]
  apply forall₂_congr
  simp +contextual [← subset_interior_iff_mem_nhdsSet, IsOpen.interior_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
inst✝ : TopologicalSpace β
⊢ UpperHemicontinuous f ↔ ∀ (x : α) (u : Set β), IsOpen[inst✝] u → f x ⊆ u → ∀ᶠ (x' : α) in 𝓝 x, f x' ⊆ u

Tactic:
by
  simp [upperHemicontinuous_iff, upperHemicontinuousAt_iff_forall_isOpen]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
inst✝ : (𝓝 x₀).IsCountablyGenerated
h : ∀ (x : ℕ → α), Tendsto x atTop (𝓝 x₀) → ∀ y₀ ∈ f x₀, ∃ y, (∀ (n : ℕ), y n ∈ f (x n)) ∧ Tendsto y atTop (𝓝 y₀)
U : Set β
hU : IsOpen[inst✝¹] U
y₀ : β
hy₀f : y₀ ∈ f x₀
hy₀U : y₀ ∈ U
hc : ∃ᶠ (x : α) in 𝓝 x₀, ¬(f x ∩ U).Nonempty
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
hxU : ∀ (n : ℕ), ¬(f (x n) ∩ U).Nonempty
y : ℕ → β
hy_mem : ∀ (n : ℕ), y n ∈ f (x n)
hy_lim : Tendsto y atTop (𝓝 y₀)
⊢ False

Tactic:
obtain ⟨n, hn⟩ := (hy_lim.eventually (hU.mem_nhds hy₀U)).exists

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
inst✝ : (𝓝 x₀).IsCountablyGenerated
h : ∀ (x : ℕ → α), Tendsto x atTop (𝓝 x₀) → ∀ y₀ ∈ f x₀, ∃ y, (∀ (n : ℕ), y n ∈ f (x n)) ∧ Tendsto y atTop (𝓝 y₀)
U : Set β
hU : IsOpen[inst✝¹] U
y₀ : β
hy₀f : y₀ ∈ f x₀
hy₀U : y₀ ∈ U
hc : ∃ᶠ (x : α) in 𝓝 x₀, ¬(f x ∩ U).Nonempty
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
hxU : ∀ (n : ℕ), ¬(f (x n) ∩ U).Nonempty
y : ℕ → β
hy_mem : ∀ (n : ℕ), y n ∈ f (x n)
hy_lim : Tendsto y atTop (𝓝 y₀)
n : ℕ
hn : U (y n)
⊢ False
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h✝ : s.Nonempty
u : Set (Set α)
hu₁ : u ⊆ {U | IsOpen[inst✝] U}
hu₂ : u.Finite
hu : powerset '' u ⊆ powerset '' {U | IsOpen[inst✝] U}
v : Set (Set α)
hv₁ : v ⊆ {U | IsOpen[inst✝] U}
hv₂ : v.Finite
hv : (fun V ↦ {s | (s ∩ V).Nonempty}) '' v ⊆ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝] U}
ht₁ : (powerset '' u).Finite ∧ ((fun V ↦ {s | (s ∩ V).Nonempty}) '' v).Finite
ht₂ :
  powerset '' u ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' v ⊆
    powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
U : Set α := ⋂₀ u
hU : IsOpen[inst✝] U
hs : s ⊆ U ∧ ∀ i ∈ v, s ∈ {s | (s ∩ i).Nonempty}
⊢ ⋃₀ insert U ((fun x ↦ U ∩ x) '' v) = U

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
n : ℕ
hn : n ≠ 0
x : 𝕜
hx : x ∈ σ a
⊢ ↑‖x‖₊ ^ n ≤ ↑‖x ^ n‖₊

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case zero
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
a : A
⊢ spectralRadius 𝕜 a ^ 0 ≤ spectralRadius 𝕜 (a ^ 0)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
a : A
n✝ : ℕ
⊢ n✝ + 1 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case zero
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
⊢ ‖a ^ 0‖₊ * r ^ 0 ≤ max 1 ‖1‖₊

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case inl
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : IsCompact s
U : Set α
hU : U ∈ {U | IsOpen[inst✝.toTopologicalSpace] U}
hs' : s ∈ 𝒫 U
⊢ 𝒫 U ∈ 𝓝 s

Tactic:
obtain ⟨V : SetRel α α, hV₁, hV₂⟩ :=
      hs.nhdsSet_basis_uniformity (𝓤 α).basis_sets |>.mem_iff.mp (hU.mem_nhdsSet.mpr hs')

Goal state after:
case inl
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : IsCompact s
U : Set α
hU : U ∈ {U | IsOpen[inst✝.toTopologicalSpace] U}
hs' : s ∈ 𝒫 U
V : SetRel α α
hV₁ : V ∈ 𝓤 α
hV₂ : ⋃ x ∈ s, UniformSpace.ball x (id V) ⊆ U
⊢ 𝒫 U ∈ 𝓝 s
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case e'_3
α : Type u_1
inst✝ : UniformSpace α
x✝ : Closeds α
⊢ x✝ ∈ {⊥} ↔ x✝ ∈ SetLike.coe ⁻¹' {∅}

Tactic:
simp

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

Goal state before:
pp: case neg.inl
α : Type u_1
inst✝ : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS : S ⊆ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
hKS : {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U | IsOpen[inst✝] U ∧ {s | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ L ∈ s, (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : U ∈ {U | IsOpen[inst✝] U}
hUS : 𝒫 U ∈ S
hUu : K \ U ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hKT : K \ U ⊆ ⋃ i ∈ T, i
t : Set α
htU : t ∉ 𝒫 U
htK : t ⊆ K
⊢ t ∈ ⋃ a ∈ T, {s | (s ∩ a).Nonempty}

Tactic:
rw [mem_powerset_iff, not_subset] at htU

Goal state after:
case neg.inl
α : Type u_1
inst✝ : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS : S ⊆ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
hKS : {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U | IsOpen[inst✝] U ∧ {s | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ L ∈ s, (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : U ∈ {U | IsOpen[inst✝] U}
hUS : 𝒫 U ∈ S
hUu : K \ U ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hKT : K \ U ⊆ ⋃ i ∈ T, i
t : Set α
htU : ∃ a ∈ t, a ∉ U
htK : t ⊆ K
⊢ t ∈ ⋃ a ∈ T, {s | (s ∩ a).Nonempty}
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 - ↑ₐ z) * ↑ₐ (exp z) - 1 * ↑ₐ (exp z))

Tactic:
← _root_.sub_mul,

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) - 1) * ↑ₐ (exp z))
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case refine_1
𝕜 : 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⁻¹)
mem : ↑ha.unit⁻¹ ∈ S
⊢ ↑(a * ⟨↑ha.unit⁻¹, mem⟩) = ↑1

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case refine_2
𝕜 : 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⁻¹)
mem : ↑ha.unit⁻¹ ∈ S
⊢ ↑(⟨↑ha.unit⁻¹, mem⟩ * a) = ↑1

Tactic:
simp

Goal state after:
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⁻¹)
mem : ↑ha.unit⁻¹ ∈ S
⊢ IsUnit a

Tactic:
refine ⟨⟨a, ⟨(↑ha.unit⁻¹ : A), mem⟩, ?_, ?_⟩, rfl⟩
    all_goals ext; simp

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : IsScalarTower 𝕜 A A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
a : A
ha : p a
inst✝ : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
f : C(↑(σₙ 𝕜 a), 𝕜)₀
⊢ Set.range ⇑((Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯)) (ContinuousMapZero.toContinuousMapHom f)) =
    Set.range ⇑f

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace α
f : Filter (Compacts α)
x✝ : Cauchy f
left✝ : f.NeBot
hf : ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
l : Filter α := f.lift' fun s ↦ ⋃ K ∈ s, ↑K
hl : l.TotallyBounded
L : Compacts α := { carrier := {x | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
x : α
hx : x ∈ ↑K
lx : Filter α := l ⊓ 𝓟 (UniformSpace.ball x U)
le_def : lx = l ⊓ 𝓟 (UniformSpace.ball x U)
hlx : lx.TotallyBounded
this : lx.NeBot
y : α
hy : ClusterPt y lx
hy₁ : ClusterPt y l
hy₂ : y ∈ UniformSpace.ball x U
⊢ x ∈ U.preimage ↑L

Tactic:
exact ⟨y, hy₁, hy₂⟩

Goal state after:
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
x : ↥S
this : CompleteSpace ↥S
μ : 𝕜
h : IsUnit ((algebraMap 𝕜 A) μ - ↑x)
hμ₁ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
⊢ 𝓝 μ ⊓ 𝓟 (σ 𝕜 x)ᶜ ≤ 𝓝 μ

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
x✝ : CompleteSpace (NonemptyCompacts α)
f : Filter α
hf : Cauchy f
K : NonemptyCompacts α
hK : Filter.map (fun x ↦ {x}) f ≤ 𝓝 K
x : α
hx : x ∈ ↑K
U : Set α
hxU : x ∈ U
hU : IsOpen[inst✝.toTopologicalSpace] U
⊢ ∀ a ∈ (fun x ↦ {x}) ⁻¹' {K | (↑K ∩ U).Nonempty}, a ∈ U

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
⊢ CompleteSpace (NonemptyCompacts α) ↔ CompleteSpace α

Tactic:
refine ⟨fun _ => ⟨fun {f} hf => ?_⟩, fun _ => inferInstance⟩
  obtain ⟨K, hK⟩ := CompleteSpace.complete <| hf.map uniformContinuous_singleton
  obtain ⟨x, hx⟩ := K.nonempty
  exists x
  rw [(nhds_basis_opens x).ge_iff]
  intro U ⟨hxU, hU⟩
  filter_upwards [hK <| (isOpen_inter_nonempty_of_isOpen hU).mem_nhds ⟨x, hx, hxU⟩]
  simp

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
x : 𝕜
hx' : x ∈ σ 𝕜 a
hx : IsGreatest ((fun x ↦ ‖f x‖) '' σ 𝕜 a) ((fun x ↦ ‖f x‖) x)
⊢ (fun x ↦ ‖f x‖) x ≤ ‖{ toFun := (σ 𝕜 a).domRestrict f, continuous_toFun := ⋯ } ⟨x, hx'⟩‖

Tactic:
simp

Goal state after:
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
x : ↥S
this : IsClopen ((σ 𝕜 ↑x)ᶜ ↓∩ σ 𝕜 x \ σ 𝕜 ↑x)
⊢ σ 𝕜 x = σ 𝕜 ↑x ∪ ⋃ z ∈ σ 𝕜 x \ σ 𝕜 ↑x, connectedComponentIn (σ 𝕜 ↑x)ᶜ z

Tactic:
← this.biUnion_connectedComponentIn (sdiff_subset_compl _ _),

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
x : ↥S
this : IsClopen ((σ 𝕜 ↑x)ᶜ ↓∩ σ 𝕜 x \ σ 𝕜 ↑x)
⊢ σ 𝕜 x = σ 𝕜 ↑x ∪ σ 𝕜 x \ σ 𝕜 ↑x
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✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
h : IsPreconnected (σ 𝕜 ↑x)ᶜ
this : σ 𝕜 x \ σ 𝕜 ↑x = ∅
⊢ σ 𝕜 ↑x ∪ ⋃ z ∈ ∅, connectedComponentIn (σ 𝕜 ↑x)ᶜ z = σ 𝕜 ↑x

Tactic:
simp

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

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✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σₙ ℂ a
this : Set.EqOn (fun x ↦ star (id x)) id (σₙ ℂ a)
⊢ (starRingEnd ℂ) x = x

Tactic:
simpa using this hx

Goal state after:
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
x : 𝕜
hx' : x ∈ σₙ 𝕜 a
hx : IsGreatest ((fun x ↦ ‖f x‖) '' σₙ 𝕜 a) ((fun x ↦ ‖f x‖) x)
⊢ (fun x ↦ ‖f x‖) x ≤ ‖↑{ toFun := (σₙ 𝕜 a).domRestrict f, continuous_toFun := ⋯, map_zero' := ⋯ } ⟨x, hx'⟩‖

Tactic:
simp

Goal state after:
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 : ℝ≥0
hy : ↑y ∈ spectrum ℝ a
hx : ↑t - ↑y ∈ {↑t} - spectrum ℝ a
hty : -↑t ≤ ↑y
hyt : ↑y ≤ ↑t
⊢ ↑‖↑(t - y)‖₊ ≤ ↑t

Tactic:
simp

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

Goal state before:
pp: s t : Set ℝ
⊢ ⇑equivRealProdLm ⁻¹' (convexHull ℝ) (s ×ˢ t) = (convexHull ℝ) s ×ℂ (convexHull ℝ) t

Tactic:
rw [convexHull_prod]

Goal state after:
s t : Set ℝ
⊢ ⇑equivRealProdLm ⁻¹' (convexHull ℝ) s ×ˢ (convexHull ℝ) t = (convexHull ℝ) s ×ℂ (convexHull ℝ) t
Module: Mathlib.Analysis.Complex.Convex

Goal state before:
pp: r : ℝ
s : Set ℂ
hs₁ : {z | r < z.im} ⊆ s
hs₂ : s ⊆ {z | r ≤ z.im}
⊢ (↑r + 1) * I ∈ {c | r < c.im}

Tactic:
simp

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

Goal state before:
pp: r : ℝ
s : Set ℂ
hs₁ : {z | z.im < r} ⊆ s
hs₂ : s ⊆ {z | z.im ≤ r}
⊢ (↑r - 1) * I ∈ {c | c.im < r}

Tactic:
simp

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

Goal state before:
pp: r : ℝ
⊢ I ∈ {c | 0 < c.im}

Tactic:
simp

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

Goal state before:
pp: r : ℝ
⊢ 1 ∈ {c | 0 < c.re}

Tactic:
simp

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

Goal state before:
pp: r : ℝ
⊢ 1 + I ∈ {c | 0 < c.im} ∩ {c | 0 < c.re}

Tactic:
simp

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

Goal state before:
pp: r : ℝ
⊢ -I ∈ {c | c.im < 0}

Tactic:
simp

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

Goal state before:
pp: r : ℝ
⊢ -1 ∈ {c | c.re < 0}

Tactic:
simp

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

Goal state before:
pp: r : ℝ
⊢ -1 - I ∈ {c | c.im < 0} ∩ {c | c.re < 0}

Tactic:
simp

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

Goal state before:
pp: r : ℝ
⊢ 1 - I ∈ ({c | 0 < c.im} ∪ {c | 0 < c.re}) ∩ ({c | c.im < 0} ∪ {c | c.re < 0})

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n ↦ ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
n : ℕ
⊢ ↑‖a‖₊ = ↑‖a‖₊ ^ (↑(2 ^ n) * (1 / ↑(2 ^ n)))

Tactic:
simp

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

Goal state before:
pp: case inl
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
c : ℝ≥0
h : ∀ x ∈ σ ℝ≥0 a, f x ≤ c
h✝ : Subsingleton A
⊢ ‖0‖₊ ≤ c

Tactic:
simp

Goal state after:
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
c : ℝ≥0
h : ∀ x ∈ σ ℝ≥0 a, f x ≤ c
h✝ : Nontrivial A
⊢ ‖0‖₊ ≤ c

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula

Goal state before:
pp: A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
x✝ : ℕ
⊢ 0 ≤ 1 / ↑x✝

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x ≤ c
⊢ ‖0‖₊ ≤ c

Tactic:
simp

Goal state after: