mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : CompactSpace α
f : Ultrafilter (Set α)
this : TopologicalSpace (Set α) := TopologicalSpace.vietoris α
⊢ ∃ x ∈ Set.univ, ↑f ≤ 𝓝 x

Tactic:
refine ⟨closure f.lim, Set.mem_univ _, ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompactSpace α
f : Ultrafilter (Set α)
this : TopologicalSpace (Set α) := TopologicalSpace.vietoris α
⊢ ↑f ≤ 𝓝 (closure[inst✝³.toTopologicalSpace] f.lim)
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : 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
⊢ (fun U ↦ {s | (s ∩ U).Nonempty}) '' T ⊆ S

Tactic:
grind [image_subset_iff]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
h : s ⤳ t
x : α
hx : x ∈ s
⊢ ∃ y ∈ t, x ⤳ y

Tactic:
obtain ⟨y, hyt, hxy⟩ := h.mem_closed (s := {u | (u ∩ closure {x}).Nonempty})
      (isClosed_inter_nonempty_of_isClosed isClosed_closure) ⟨x, hx, subset_closure rfl⟩
    exact ⟨y, hyt, specializes_iff_mem_closure.mpr hxy⟩

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

Goal state before:
pp: case refine_1
𝕜 : 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), 𝕜)₀
h₁ :
  (cfcₙAux ⋯ a ha) f ∈
    closure[Unitization.instUniformSpace.toTopologicalSpace]
      (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id (σₙ 𝕜 a)}))
⊢ NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id (σₙ 𝕜 a)} ≤
    NonUnitalStarSubalgebra.comap (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A))

Tactic:
apply NonUnitalStarAlgebra.adjoin_le

Goal state after:
case refine_1
𝕜 : 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), 𝕜)₀
h₁ :
  (cfcₙAux ⋯ a ha) f ∈
    closure[Unitization.instUniformSpace.toTopologicalSpace]
      (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id (σₙ 𝕜 a)}))
⊢ {ContinuousMapZero.id (σₙ 𝕜 a)} ⊆
    ↑(NonUnitalStarSubalgebra.comap (cfcₙAux ⋯ a ha)
        (NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A)))
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : IsPreconnected s
t : Set α
hts : t ∈ s
ht : IsPreconnected t
hts' : t ⊆ ⋃₀ s
U V : Set α
hU : IsOpen[inst✝] U
hV : IsOpen[inst✝] V
hUV : ⋃₀ s ⊆ U ∪ V
ht' : t ⊆ U ∨ t ⊆ V
htU : t ⊆ U
u : Set α
hus : u ∈ s
huV : (u ∩ V).Nonempty
⊢ (⋃₀ s ∩ (U ∩ V)).Nonempty

Tactic:
have : s ⊆ U.powerset ∪ {v | (v ∩ V).Nonempty} := by
      grind [=_ sdiff_subset_iff, =_ not_disjoint_iff_nonempty_inter]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : IsPreconnected s
t : Set α
hts : t ∈ s
ht : IsPreconnected t
hts' : t ⊆ ⋃₀ s
U V : Set α
hU : IsOpen[inst✝] U
hV : IsOpen[inst✝] V
hUV : ⋃₀ s ⊆ U ∪ V
ht' : t ⊆ U ∨ t ⊆ V
htU : t ⊆ U
u : Set α
hus : u ∈ s
huV : (u ∩ V).Nonempty
this : s ⊆ 𝒫 U ∪ {v | (v ∩ V).Nonempty}
⊢ (⋃₀ s ∩ (U ∩ V)).Nonempty
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

Goal state before:
pp: case refine_1
𝕜 : 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), 𝕜)₀
h₁ :
  (cfcₙAux ⋯ a ha) f ∈
    closure[Unitization.instUniformSpace.toTopologicalSpace]
      (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id (σₙ 𝕜 a)}))
⊢ ContinuousMapZero.id (σₙ 𝕜 a) ∈
    ↑(NonUnitalStarSubalgebra.comap (cfcₙAux ⋯ a ha)
        (NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A)))

Tactic:
SetLike.mem_coe,

Goal state after:
case refine_1
𝕜 : 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), 𝕜)₀
h₁ :
  (cfcₙAux ⋯ a ha) f ∈
    closure[Unitization.instUniformSpace.toTopologicalSpace]
      (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id (σₙ 𝕜 a)}))
⊢ ContinuousMapZero.id (σₙ 𝕜 a) ∈
    NonUnitalStarSubalgebra.comap (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A))
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case right
α : 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 : ClusterPt x l
⊢ l ≤ 𝓟 (U.image ↑K)

Tactic:
rw [Filter.le_principal_iff]

Goal state after:
case right
α : 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 : ClusterPt x l
⊢ U.image ↑K ∈ l
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
⊢ frontier (σ 𝕜 x) ⊆ frontier (σ 𝕜 ↑x)

Tactic:
rw [frontier_eq_closure_inter_closure (s := σ 𝕜 (x : A)),
    (spectrum.isClosed (x : A)).closure_eq]
  apply subset_inter (frontier_spectrum S x)
  rw [frontier_eq_closure_inter_closure]
  grw [inter_subset_right, spectrum.subset_subalgebra]

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

Goal state before:
pp: A : Type u_4
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
x : ℝ
hx₁ : x ∈ spectrum ℝ a
hx₂ : ↑‖x‖₊ = spectralRadius ℝ a
⊢ |x| ∈ spectrum ℝ a ∨ -|x| ∈ spectrum ℝ a

Tactic:
exact abs_choice x |>.imp (fun h ↦ by rwa [h]) (fun h ↦ by simpa [h])

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' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ IsGreatest (f '' σ ℝ≥0 a) ‖cfc (fun x ↦ ↑(f x.toNNReal)) a‖₊

Tactic:
rw [← SpectrumRestricts] at ha'

Goal state after:
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
⊢ IsGreatest (f '' σ ℝ≥0 a) ‖cfc (fun x ↦ ↑(f x.toNNReal)) a‖₊
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected (σ ℂ a)ᶜ

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

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im} ∪ (σ ℂ a)ᶜ ∩ {z | z.im ≤ 0})
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

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

Tactic:
obtain ⟨C, hC⟩ := (hK₁.image (map_continuous f)).isBounded.subset_closedBall (0 : β)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : ContinuousSMul ℝ E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
S : AbsConvexOpenSets 𝕜 E
x✝ : S ∈ t
⊢ r = ‖↑r‖ * 1

Tactic:
simp [abs_of_pos hr]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
⊢ ContinuousSup (NonemptyCompacts α)

Tactic:
by
  constructor
  simp_rw [isEmbedding_toCompacts.continuous_iff, Function.comp_def, toCompacts_sup]
  fun_prop

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

Goal state before:
pp: ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
t₂ : Finset ι → TopologicalSpace E := fun s ↦ ⨅ i, induced (⇑(f ↑i)) t𝕜
⊢ Continuous[t₁, t𝕜] ⇑φ ↔ ∃ s, Continuous[t₂ s, t𝕜] ⇑φ

Tactic:
have t₁_group : @IsTopologicalAddGroup E t₁ _ :=
    topologicalAddGroup_iInf fun _ ↦ topologicalAddGroup_induced _

Goal state after:
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t₁ : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
t₂ : Finset ι → TopologicalSpace E := fun s ↦ ⨅ i, induced (⇑(f ↑i)) t𝕜
t₁_group : IsTopologicalAddGroup E
⊢ Continuous[t₁, t𝕜] ⇑φ ↔ ∃ s, Continuous[t₂ s, t𝕜] ⇑φ
Module: Mathlib.Analysis.Normed.Module.Dual

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ ⋂₀ (polar 𝕜 '' {F | F.Finite ∧ F ⊆ closedBall 0 r⁻¹}) = closedBall 0 r

Tactic:
conv_rhs => rw [← inv_inv r]
  rw [← polar_closedBall (inv_pos_of_pos hr), StrongDual.polar,
    (topDualPairing 𝕜 E).flip.sInter_polar_finite_subset_eq_polar (closedBall (0 : E) r⁻¹)]

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

Goal state before:
pp: case mp
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
this✝ : IsTopologicalAddGroup E
this : WithSeminorms fun i ↦ (f i).toSeminorm
H : Continuous[⨅ i, induced (⇑(f i)) inferInstance, _] ⇑((normSeminorm 𝕜 𝕜).comp φ)
s : Finset ι
C : ℝ≥0
hC : (normSeminorm 𝕜 𝕜).comp φ ≤ C • s.sup fun i ↦ (f i).toSeminorm
⊢ ∃ s c, φ.toSeminorm ≤ c • s.sup fun i ↦ (f i).toSeminorm

Tactic:
exact ⟨s, C, hC⟩

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

Goal state before:
pp: case refine_2
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : I ≤ idealOfSet R s
x : X
hx : x ∈ setOfIdeal I
f : C(X, R)
hf : f ∈ I
hfx : f x ≠ 0
hx' : x ∉ s
⊢ False

Tactic:
exact notMem_idealOfSet.mpr ⟨x, hx', hfx⟩ (h hf)

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

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g : C(X, ℝ≥0)
hgI : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I
hg : ∀ (x : X), g x ≤ 1
hgt : Set.EqOn (⇑g) 1 t
⊢ ∃ b ∈ ↑I, nndist f b < ε

Tactic:
refine ⟨f * (algebraMapCLM ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g, I.mul_mem_left f hgI, ?_⟩

Goal state after:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g : C(X, ℝ≥0)
hgI : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I
hg : ∀ (x : X), g x ≤ 1
hgt : Set.EqOn (⇑g) 1 t
⊢ nndist f (f * (↑(algebraMapCLM ℝ≥0 𝕜)).comp g) < ε
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Opens X
I : Ideal C(X, 𝕜)
hI : IsCoatom I
⊢ idealOfSet 𝕜 ↑(opensOfIdeal I) = I

Tactic:
← Ideal.isMaximal_def

Goal state after:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Opens X
I : Ideal C(X, 𝕜)
hI : I.IsMaximal
⊢ idealOfSet 𝕜 ↑(opensOfIdeal I) = I
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
x : X
k : Set X
hk : IsCompact k
k_mem : k ∈ 𝓝 x
f : C(X, ℝ)
fk : EqOn (⇑f) 1 k
f_comp : HasCompactSupport ⇑f
hf : ∀ (x : X), f x ∈ Icc 0 1
⊢ ∃ f, HasCompactSupport ⇑f ∧ 0 ≤ ⇑f ∧ f x ≠ 0

Tactic:
refine ⟨f, f_comp, fun x ↦ (hf x).1, ?_⟩

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
x : X
k : Set X
hk : IsCompact k
k_mem : k ∈ 𝓝 x
f : C(X, ℝ)
fk : EqOn (⇑f) 1 k
f_comp : HasCompactSupport ⇑f
hf : ∀ (x : X), f x ∈ Icc 0 1
⊢ f x ≠ 0
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
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace ↑s
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
this : Fact (0 ∈ s)
mul₁ : ∀ (f g : C(↑s, ℝ)₀), (cfcₙHomSuperset hb' hbs) f * (cfcₙHomSuperset hc' hcs) g = 0
mul₂ : ∀ (f g : C(↑s, ℝ)₀), (cfcₙHomSuperset hc' hcs) f * (cfcₙHomSuperset hb' hbs) g = 0
ψ : C(↑s, ℝ)₀ →⋆ₙₐ[ℝ] A :=
  let __src := ↑(cfcₙHomSuperset hb' hbs) + ↑(cfcₙHomSuperset hc' hcs);
  { toFun := ⇑(cfcₙHomSuperset hb' hbs) + ⇑(cfcₙHomSuperset hc' hcs), map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
    map_mul' := ⋯, map_star' := ⋯ }
f : C(↑s, ℝ)₀ := { toFun := fun x ↦ (↑x)⁺, continuous_toFun := ⋯, map_zero' := ⋯ }
key :
  cfcₙ
      (Function.extend Subtype.val ⇑(f.comp { toFun := Subtype.map id has, continuous_toFun := ⋯, map_zero' := ⋯ })
        fun x ↦ x⁺)
      a =
    cfcₙ
        (Function.extend Subtype.val ⇑(f.comp { toFun := Subtype.map id hbs, continuous_toFun := ⋯, map_zero' := ⋯ })
          fun x ↦ x⁺)
        b +
      cfcₙ
        (Function.extend Subtype.val ⇑(f.comp { toFun := Subtype.map id hcs, continuous_toFun := ⋯, map_zero' := ⋯ })
          fun x ↦ x⁺)
        (-c)
⊢ cfcₙ
      (Function.extend Subtype.val ⇑(f.comp { toFun := Subtype.map id has, continuous_toFun := ⋯, map_zero' := ⋯ })
        fun x ↦ x⁺)
      a =
    a⁺

Tactic:
refine cfcₙ_congr fun x hx ↦ ?_
      lift x to σₙ ℝ a using hx
      simp [f]

Goal state after:
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)
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcHomSuperset ⋯ ⋯) f

Tactic:
have : CompactSpace s := by rwa [isCompact_iff_compactSpace] at hs

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 : 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)
this : CompactSpace ↑s
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcHomSuperset ⋯ ⋯) f
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
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
a₀ : A
l : Filter X
ha_tendsto : Tendsto a l (𝓝 a₀)
ha : ∀ᶠ (x : X) in l, spectrum 𝕜 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in l, p (a x)
ha₀ : spectrum 𝕜 a₀ ⊆ s
ha₀' : p a₀
hf : ContinuousOn f s
⊢ Tendsto (fun x ↦ cfc f (a x)) l (𝓝 (cfc f a₀))

Tactic:
apply continuousOn_cfc A hs f |>.continuousWithinAt ⟨ha₀', ha₀⟩ |>.tendsto.comp
  rw [tendsto_nhdsWithin_iff]
  exact ⟨ha_tendsto, ha'.and ha⟩

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
hab : a ≤ b
h : IsStrictlyPositive a
a✝ : Nontrivial A
⊢ IsUnit b

Tactic:
← spectrum.zero_notMem_iff ℝ

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a ≤ b
h : IsStrictlyPositive a
a✝ : Nontrivial A
⊢ 0 ∉ spectrum ℝ b
Module: Mathlib.Analysis.CStarAlgebra.Module.Defs

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul A E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℂ
x y : E
⊢ ⟪z •> x, y⟫ = star z •> ⟪x, y⟫

Tactic:
by
  rw [← star_inner]
  simp

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
this : IsClosed {a | 0 ≤ a}
⊢ IsClosed {a | 0 ≤ a}

Tactic:
Unitization.isometry_inr (𝕜 := ℂ) |>.isClosedEmbedding.isClosed_iff_image_isClosed

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
this : IsClosed {a | 0 ≤ a}
⊢ IsClosed (Unitization.inr '' {a | 0 ≤ a})
Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions

Goal state before:
pp: case left.refine_1
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)
⊢ 0 ≤ ⟪x.1, x.1⟫_A

pp: case left.refine_2
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)
⊢ ⟪x.1, x.1⟫_A ≤ ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A

Tactic:
all_goals
      aesop (add safe apply CStarModule.inner_self_nonneg)

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

Goal state before:
pp: case right.refine_1
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)
⊢ 0 ≤ ⟪x.2, x.2⟫_A

pp: case right.refine_2
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)
⊢ ⟪x.2, x.2⟫_A ≤ ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A

Tactic:
all_goals
      aesop (add safe apply CStarModule.inner_self_nonneg)

Goal state after: