mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), (g x y) x = f x
w₂ : ∀ (x y : X), (g x y) y = f y
U : X → X → Set X := fun x y ↦ {z | f z - ε < (g x y) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x ↦ ⋯.choose
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ :=
  fun x ↦ Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhds_y x))
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := fun x ↦ ⟨(ys x).sup' ⋯ fun y ↦ g x y, ⋯⟩
lt_h : ∀ (x z : X), f z - ε < ↑(h x) z
h_eq : ∀ (x : X), ↑(h x) x = f x
W : X → Set X := fun x ↦ {z | ↑(h x) z < f z + ε}
W_nhds : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := ⋯.choose
xs_w : ⋃ x ∈ xs, W x = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhds)
⊢ ∃ x, dist x f < ε ∧ x ∈ L

Tactic:
have xs_nonempty : xs.Nonempty := Set.nonempty_of_union_eq_top_of_nonempty _ _ nX xs_w

Goal state after:
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), (g x y) x = f x
w₂ : ∀ (x y : X), (g x y) y = f y
U : X → X → Set X := fun x y ↦ {z | f z - ε < (g x y) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x ↦ ⋯.choose
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ :=
  fun x ↦ Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhds_y x))
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := fun x ↦ ⟨(ys x).sup' ⋯ fun y ↦ g x y, ⋯⟩
lt_h : ∀ (x z : X), f z - ε < ↑(h x) z
h_eq : ∀ (x : X), ↑(h x) x = f x
W : X → Set X := fun x ↦ {z | ↑(h x) z < f z + ε}
W_nhds : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := ⋯.choose
xs_w : ⋃ x ∈ xs, W x = ⊤ := Exists.choose_spec (CompactSpace.elim_nhds_subcover W W_nhds)
xs_nonempty : xs.Nonempty
⊢ ∃ x, dist x f < ε ∧ x ∈ L
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
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
key : (↑I).range ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure
f : C(X, 𝕜)
f_re : C(X, ℝ) := { toFun := ⇑re, continuous_toFun := ⋯ }.comp f
f_im : C(X, ℝ) := { toFun := ⇑im, continuous_toFun := ⋯ }.comp f
h_f_re : I f_re ∈ A.topologicalClosure
h_f_im : I f_im ∈ A.topologicalClosure
this : I f_re + RCLike.I • I f_im ∈ A.topologicalClosure.toSubalgebra
⊢ f ∈ A.topologicalClosure

Tactic:
rw [StarSubalgebra.mem_toSubalgebra] at this

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
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
key : (↑I).range ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure
f : C(X, 𝕜)
f_re : C(X, ℝ) := { toFun := ⇑re, continuous_toFun := ⋯ }.comp f
f_im : C(X, ℝ) := { toFun := ⇑im, continuous_toFun := ⋯ }.comp f
h_f_re : I f_re ∈ A.topologicalClosure
h_f_im : I f_im ∈ A.topologicalClosure
this : I f_re + RCLike.I • I f_im ∈ A.topologicalClosure
⊢ f ∈ A.topologicalClosure
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
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✝²¹ : NonUnitalRing A
inst✝²⁰ : StarRing A
inst✝¹⁹ : TopologicalSpace A
inst✝¹⁸ : Module R A
inst✝¹⁷ : IsScalarTower R A A
inst✝¹⁶ : SMulCommClass R A A
inst✝¹⁵ : NonUnitalRing B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Module R B
inst✝¹¹ : IsScalarTower R B B
inst✝¹⁰ : SMulCommClass R B B
inst✝⁹ : Module S A
inst✝⁸ : Module S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : NonUnitalContinuousFunctionalCalculus R A p
inst✝⁴ : NonUnitalContinuousFunctionalCalculus R B q
inst✝³ : ContinuousMapZero.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (quasispectrum R a)
hf₀ : f 0 = 0
hφ : Continuous[inst✝¹⁹, inst✝¹³] ⇑φ
ha : p a
hφa : q (φ a)
ψ : A →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R ↑φ
this : Continuous[inst✝¹⁹, inst✝¹³] ⇑ψ
h_spec : quasispectrum R (φ a) ⊆ quasispectrum R a
hψa : q (ψ a)
ι : C(↑(quasispectrum R (ψ a)), ↑(quasispectrum R a))₀ :=
  { toFun := Set.inclusion h_spec, continuous_toFun := ⋯, map_zero' := ⋯ }
⊢ (ψ.comp (cfcₙHom ha)) (ContinuousMapZero.id (quasispectrum R a)) =
    ((cfcₙHom hψa).comp (ContinuousMapZero.nonUnitalStarAlgHom_precomp R ι)) (ContinuousMapZero.id (quasispectrum R a))

Tactic:
case =>

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

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → 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✝¹⁵ : Ring B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Algebra R B
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : ContinuousFunctionalCalculus R A p
inst✝⁴ : ContinuousFunctionalCalculus R B q
inst✝³ : ContinuousMap.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hφ : Continuous[inst✝¹⁷, inst✝¹³] ⇑φ
ha : p a
hφa : q (φ a)
ψ : A →⋆ₐ[R] B := StarAlgHom.restrictScalars R ↑φ
this : Continuous[inst✝¹⁷, inst✝¹³] ⇑ψ
h_spec : spectrum R (ψ a) ⊆ spectrum R a
hψa : q (ψ a)
ι : C(↑(spectrum R (ψ a)), ↑(spectrum R a)) := { toFun := Set.inclusion h_spec, continuous_toFun := ⋯ }
⊢ (ψ.comp (cfcHom ha)) (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) =
    ((cfcHom hψa).comp (ContinuousMap.compStarAlgHom' R R ι))
      (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R))

Tactic:
case =>

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 β
⊢ ∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → (∀ᶠ (x' : α) in 𝓝[s] x, s_1 ∈ 𝓝ˢ (f x')) → ∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝ˢ (f x')

Tactic:
case =>

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 β
⊢ ∀ ⦃s_1 t : Set β⦄, s_1 ⊆ t → f ⁻¹' Iic s_1 ∈ 𝓝[s] x → f ⁻¹' Iic t ∈ 𝓝[s] x

Tactic:
case =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
⊢ LowerHemicontinuousAt (fun x ↦ {f x}) x ↔ ContinuousAt f x

Tactic:
simp [← lowerHemicontinuousWithinAt_univ_iff, continuousWithinAt_univ]

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

Goal state before:
pp: case neg
𝕜 : 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‖₊⁻¹
n : ℕ
h : ¬‖a‖₊ = 0
⊢ ‖a‖₊ ^ n.succ * r ^ (n + 1) ≤ 1

Tactic:
NNReal.lt_inv_iff_mul_lt h

Goal state after:
case neg
𝕜 : 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‖₊ < 1
n : ℕ
h : ¬‖a‖₊ = 0
⊢ ‖a‖₊ ^ n.succ * r ^ (n + 1) ≤ 1
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
y : 𝕜
hy : y ∈ Metric.eball 0 (↑‖a‖₊)⁻¹
h : ¬‖a‖₊ = 0
⊢ ‖y • a‖ < 1

Tactic:
· have nnnorm_lt : ‖y‖₊ < ‖a‖₊⁻¹ := by
            simpa only [← coe_inv h, mem_ball_zero_iff, Metric.eball_coe] using! hy
          rwa [← coe_nnnorm, ← Real.lt_toNNReal_iff_coe_lt, Real.toNNReal_one, nnnorm_smul,
            ← NNReal.lt_inv_iff_mul_lt h]

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

Goal state before:
pp: case pos
α : 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}
L : Set α
hL : L ∈ s
hLu : L ⊆ ⋃ i ∈ u, i
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q

Tactic:
obtain ⟨T, hTS, hT, hLT⟩ := (hs L hL).elim_finite_subcover_image (fun _ h => h.1) hLu

Goal state after:
case pos
α : 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}
L : Set α
hL : L ∈ s
hLu : L ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hLT : L ⊆ ⋃ i ∈ T, i
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : 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
⊢ lx.NeBot

Tactic:
rw [le_def, Filter.lift'_inf_principal_eq, Filter.lift'_neBot_iff fun _ _ h =>
        Set.inter_subset_inter_left _ <| Set.biUnion_subset_biUnion_left h]

Goal state after:
α : 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
⊢ ∀ s ∈ f, ((⋃ K ∈ s, ↑K) ∩ UniformSpace.ball x U).Nonempty
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case e'_4.a
𝕜 : 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)
⊢ ‖{ toFun := (σ 𝕜 a).domRestrict f, continuous_toFun := ⋯ }‖ ≤ (fun x ↦ ‖f x‖) x

Tactic:
apply ContinuousMap.norm_le _ (norm_nonneg _) |>.mpr
    rintro ⟨y, hy⟩
    exact hx.2 ⟨y, hy, rfl⟩

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₁
inst✝ : CompleteSpace A
f : C(↑(σₙ 𝕜 a), 𝕜)₀
⊢ (cfcₙAux ⋯ a ha) f ∈ NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A)

Tactic:
by
  have h₁ := (continuous_cfcₙAux hp₁ a ha).range_subset_closure_image_dense
    (ContinuousMapZero.adjoin_id_dense (σₙ 𝕜 a)) ⟨f, rfl⟩
  rw [← SetLike.mem_coe]
  refine closure_minimal ?_ ?_ h₁
  · rw [← NonUnitalStarSubalgebra.coe_map, SetLike.coe_subset_coe, NonUnitalStarSubalgebra.map_le]
    apply NonUnitalStarAlgebra.adjoin_le
    apply Set.singleton_subset_iff.mpr
    rw [SetLike.mem_coe, NonUnitalStarSubalgebra.mem_comap, cfcₙAux_id hp₁ a ha]
    exact ⟨a, rfl⟩
  · simp only [NonUnitalStarAlgHom.coe_range]
    convert! IsClosed.preimage (Unitization.continuous_fst (𝕜 := 𝕜)) isClosed_singleton
    aesop

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
K L : Compacts α
⊢ (K, L) ∈ {p | Disjoint ↑p.1 ↑p.2} → ∃ t ⊆ {p | Disjoint ↑p.1 ↑p.2}, IsOpen t ∧ (K, L) ∈ t

Tactic:
hKL

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
K L : Compacts α
hKL : (K, L) ∈ {p | Disjoint ↑p.1 ↑p.2}
⊢ ∃ t ⊆ {p | Disjoint ↑p.1 ↑p.2}, IsOpen t ∧ (K, L) ∈ t
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
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝¹ : CompleteSpace A
inst✝ : CStarRing A
a : A
ha : p a
ψ : C(↑(σₙ 𝕜 a), 𝕜)₀ →⋆ₙₐ[𝕜] A :=
  (↑(inrRangeEquiv 𝕜 A).symm).comp
    (codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)
coe_ψ : ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), ↑(ψ f) = (cfcₙAux ⋯ a ha) f
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑ψ

Tactic:
case =>

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
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝¹ : CompleteSpace A
inst✝ : CStarRing A
a : A
ha : p a
ψ : C(↑(σₙ 𝕜 a), 𝕜)₀ →⋆ₙₐ[𝕜] A :=
  (↑(inrRangeEquiv 𝕜 A).symm).comp
    (codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)
coe_ψ : ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), ↑(ψ f) = (cfcₙAux ⋯ a ha) f
⊢ Function.Injective ⇑ψ

Tactic:
case =>

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
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝¹ : CompleteSpace A
inst✝ : CStarRing A
a : A
ha : p a
ψ : C(↑(σₙ 𝕜 a), 𝕜)₀ →⋆ₙₐ[𝕜] A :=
  (↑(inrRangeEquiv 𝕜 A).symm).comp
    (codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)
coe_ψ : ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), ↑(ψ f) = (cfcₙAux ⋯ a ha) f
⊢ ψ { toContinuousMap := ContinuousMap.restrict (σₙ 𝕜 a) (ContinuousMap.id 𝕜), map_zero' := ⋯ } = a

Tactic:
case =>

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
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝¹ : CompleteSpace A
inst✝ : CStarRing A
a : A
ha : p a
ψ : C(↑(σₙ 𝕜 a), 𝕜)₀ →⋆ₙₐ[𝕜] A :=
  (↑(inrRangeEquiv 𝕜 A).symm).comp
    (codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)
coe_ψ : ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), ↑(ψ f) = (cfcₙAux ⋯ a ha) f
f : C(↑(σₙ 𝕜 a), 𝕜)₀
⊢ σₙ 𝕜 (ψ f) = Set.range ⇑f

Tactic:
case =>

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
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝¹ : CompleteSpace A
inst✝ : CStarRing A
a : A
ha : p a
ψ : C(↑(σₙ 𝕜 a), 𝕜)₀ →⋆ₙₐ[𝕜] A :=
  (↑(inrRangeEquiv 𝕜 A).symm).comp
    (codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)
coe_ψ : ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), ↑(ψ f) = (cfcₙAux ⋯ a ha) f
f : C(↑(σₙ 𝕜 a), 𝕜)₀
⊢ p (ψ f)

Tactic:
case =>

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

Goal state before:
pp: case e'_4.a
𝕜 : 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)
⊢ ‖{ toFun := (σₙ 𝕜 a).domRestrict f, continuous_toFun := ⋯, map_zero' := ⋯ }‖ ≤ (fun x ↦ ‖f x‖) x

Tactic:
apply ContinuousMap.norm_le _ (norm_nonneg _) |>.mpr
    rintro ⟨y, hy⟩
    exact hx.2 ⟨y, hy, rfl⟩

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
inst✝ : Nontrivial A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ ContinuousOn (fun x ↦ ↑(f x.toNNReal)) (σ ℝ a)

Tactic:
case =>

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

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

Tactic:
· refine cfc_cases (‖·‖₊ < c) a f (by simpa) fun hf ha ↦ ?_
    simp only [← cfc_apply f a, (IsGreatest.nnnorm_cfc_nnreal f a hf ha |>.lt_iff)]
    rintro - ⟨x, hx, rfl⟩
    exact h x hx

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
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
ha : 0 ≤ a
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ ContinuousOn (fun x ↦ ↑(f x.toNNReal)) (σₙ ℝ a)

Tactic:
case =>

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)ᶜ ∩ {a | 0 ≤ a.im ∨ a.im ≤ 0})
⊢ IsConnected ((σ ℂ a)ᶜ ∩ Set.univ)

Tactic:
convert this

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
this : IsConnected ((σ ℂ a)ᶜ ∩ {a | 0 ≤ a.im ∨ a.im ≤ 0})
⊢ Set.univ = {a | 0 ≤ a.im ∨ a.im ≤ 0}
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

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

Tactic:
case =>

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

Goal state before:
pp: F : Type u_1
A : Type u_2
inst✝¹ : CStarAlgebra A
inst✝ : FunLike F A ℂ
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
s : ↥(selfAdjoint A)
⊢ (φ ↑s)⋆ = φ ↑s

Tactic:
selfAdjoint.mem_spectrum_eq_re s (AlgHom.apply_mem_spectrum φ (s : A))

Goal state after:
F : Type u_1
A : Type u_2
inst✝¹ : CStarAlgebra A
inst✝ : FunLike F A ℂ
hF : AlgHomClass F ℂ A ℂ
φ : F
a : A
s : ↥(selfAdjoint A)
⊢ (↑(φ ↑s).re)⋆ = ↑(φ ↑s).re
Module: Mathlib.Analysis.CStarAlgebra.Exponential

Goal state before:
pp: A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : ↥(selfAdjoint A)
h : Commute ↑a ↑b
⊢ Commute (selfAdjoint.expUnitary a) (selfAdjoint.expUnitary b)

Tactic:
rw [Commute, SemiconjBy, ← h.expUnitary_add, ← h.symm.expUnitary_add, add_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
S : Set (Compacts α)
hS : IsCompact S
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst✝] (U i)
h : ∀ i ∈ S, ↑i ⊆ ⋃ i, U i
s : Finset (Finset ι)
hs : S ⊆ ⋃ i ∈ s, {K | ↑K ⊆ ⋃ i_1 ∈ i, U i_1}
⊢ ∀ i ∈ s, ∀ i_2 ∈ {K | ↑K ⊆ ⋃ i_3 ∈ i, U i_3}, ↑i_2 ⊆ ⋃ i ∈ s.biUnion id, U i

Tactic:
Finset.set_biUnion_biUnion

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
S : Set (Compacts α)
hS : IsCompact S
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst✝] (U i)
h : ∀ i ∈ S, ↑i ⊆ ⋃ i, U i
s : Finset (Finset ι)
hs : S ⊆ ⋃ i ∈ s, {K | ↑K ⊆ ⋃ i_1 ∈ i, U i_1}
⊢ ∀ i ∈ s, ∀ i_2 ∈ {K | ↑K ⊆ ⋃ i_3 ∈ i, U i_3}, ↑i_2 ⊆ ⋃ x ∈ s, ⋃ y ∈ id x, U y
Module: Mathlib.Analysis.LocallyConvex.Polar

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ (B.polar s).Nonempty

Tactic:
use 0
  exact zero_mem_polar B s

Goal state after: