mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hF : ∀ (n : ι), LowerHemicontinuousOn (F n) s
⊢ LowerHemicontinuousOn f s

Tactic:
lowerHemicontinuousOn_iff

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
s : Set α
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformlyOn F f l s
hF : ∀ (n : ι), LowerHemicontinuousOn (F n) s
⊢ ∀ x ∈ s, LowerHemicontinuousWithinAt f s x
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformly F f l
hF : ∀ (n : ι), LowerHemicontinuous (F n)
⊢ LowerHemicontinuous f

Tactic:
rw [← lowerHemicontinuousOn_univ_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformly F f l
hF : ∀ (n : ι), LowerHemicontinuous (F n)
⊢ LowerHemicontinuousOn f univ
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
⊢ ∀ᶠ (z : 𝕜) in cobounded 𝕜, IsUnit (resolvent a z)

Tactic:
rw [atTop_basis_Ioi.cobounded_of_norm.eventually_iff]
  exact ⟨‖a‖ * ‖(1 : A)‖, trivial, fun _ ↦ isUnit_resolvent.mp ∘ mem_resolventSet_of_norm_lt_mul⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsOpen[instTopologicalSpaceProd] U
⊢ {a | s ⊆ U.preimage a} ∩ {a | a ⊆ U.image s} ∈ 𝓝 s

Tactic:
have : U.IsRefl := ⟨fun _ => refl_mem_uniformity hU₁⟩

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsOpen[instTopologicalSpaceProd] U
this : U.IsRefl
⊢ {a | s ⊆ U.preimage a} ∩ {a | a ⊆ U.image s} ∈ 𝓝 s
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
x : α
hx : x ∈ s
t : Set α
ht₁ : t.Nonempty
ht₂ : t.Finite
hts : t ⊆ s
⊢ t ∈ ⋃ n, range '' univ.pi fun x ↦ s

Tactic:
obtain ⟨n, f, -, rfl⟩ := ht₂.fin_param

Goal state after:
case inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
x : α
hx : x ∈ s
n : ℕ
f : Fin n → α
ht₁ : (range f).Nonempty
ht₂ : (range f).Finite
hts : range f ⊆ s
⊢ range f ∈ ⋃ n, range '' univ.pi fun x ↦ s
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
F : Set α
h : IsClosed[inst✝] F
⊢ IsClosed {K | (↑K ∩ F).Nonempty}

Tactic:
← compl_compl F,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
F : Set α
h : IsClosed[inst✝] F
⊢ IsClosed {K | (↑K ∩ Fᶜᶜ).Nonempty}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
⊢ IsOpen {p | Disjoint ↑p.1 ↑p.2}

Tactic:
rw [isOpen_iff_forall_mem_open]

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
⊢ ∀ x ∈ {p | Disjoint ↑p.1 ↑p.2}, ∃ t ⊆ {p | Disjoint ↑p.1 ↑p.2}, IsOpen t ∧ x ∈ t
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case e'_4
𝕜 : 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)
⊢ ‖cfcₙ f a‖ = (fun x ↦ ‖f x‖) x

Tactic:
rw [cfcₙ_apply f a, norm_cfcₙHom a _]

Goal state after:
case e'_4
𝕜 : 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
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case refine_1
𝕜 : 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
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ ≤ c
⊢ ‖0‖ ≤ c

Tactic:
simpa using (norm_nonneg _).trans <| h 0 (quasispectrum.zero_mem 𝕜 a)

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

Goal state before:
pp: A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module ℝ A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : SMulCommClass ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ ∃ x, IsSelfAdjoint x ∧ QuasispectrumRestricts x ⇑ContinuousMap.realToNNReal ∧ x * x = a

Tactic:
use cfcₙ (√·) a, cfcₙ_predicate (√·) a
  constructor
  · simpa only [QuasispectrumRestricts.nnreal_iff, cfcₙ_map_quasispectrum (√·) a,
      Set.mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
        using fun x _ ↦ Real.sqrt_nonneg x
  · rw [← cfcₙ_mul ..]
    nth_rw 2 [← cfcₙ_id ℝ a]
    apply cfcₙ_congr fun x hx ↦ ?_
    rw [QuasispectrumRestricts.nnreal_iff] at ha₂
    apply ha₂ x at hx
    simp [← sq, Real.sq_sqrt hx]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝¹⁰ : Semifield R
inst✝⁹ : Field S
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Algebra R S
inst✝⁶ : Module R A
inst✝⁵ : Module S A
inst✝⁴ : IsScalarTower S A A
inst✝³ : SMulCommClass S A A
inst✝² : IsScalarTower R S A
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSpace S
a : A
f : C(S, R)
h : QuasispectrumRestricts a ⇑f
h_cpct : CompactSpace ↑(σₙ S a)
⊢ CompactSpace ↑(σₙ R a)

Tactic:
rw [← isCompact_iff_compactSpace] at h_cpct ⊢

Goal state after:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝¹⁰ : Semifield R
inst✝⁹ : Field S
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Algebra R S
inst✝⁶ : Module R A
inst✝⁵ : Module S A
inst✝⁴ : IsScalarTower S A A
inst✝³ : SMulCommClass S A A
inst✝² : IsScalarTower R S A
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSpace S
a : A
f : C(S, R)
h : QuasispectrumRestricts a ⇑f
h_cpct : IsCompact (σₙ S a)
⊢ IsCompact (σₙ R a)
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
heq : (fun n ↦ ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) = (fun x ↦ x ^ 2) ∘ fun n ↦ ↑‖a ^ n‖₊ ^ (1 / ↑n)
h₂ : Tendsto (fun n ↦ ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) atTop (𝓝 (spectralRadius ℂ a ^ 2))
⊢ ↑‖a‖₊ * ↑‖a‖₊ = ↑(‖a‖₊ * ‖a‖₊)

Tactic:
coe_mul

Goal state after:
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
heq : (fun n ↦ ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) = (fun x ↦ x ^ 2) ∘ fun n ↦ ↑‖a ^ n‖₊ ^ (1 / ↑n)
h₂ : Tendsto (fun n ↦ ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) atTop (𝓝 (spectralRadius ℂ a ^ 2))
⊢ ↑‖a‖₊ * ↑‖a‖₊ = ↑‖a‖₊ * ↑‖a‖₊
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
U : Set (α × β)
hU : U ∈ {U | IsOpen[instTopologicalSpaceProd] U}
⊢ IsOpen ((SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) ⁻¹' 𝒫 U)

Tactic:
rw [isOpen_iff_forall_mem_open]

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
U : Set (α × β)
hU : U ∈ {U | IsOpen[instTopologicalSpaceProd] U}
⊢ ∀ x ∈ (SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) ⁻¹' 𝒫 U, ∃ t ⊆ (SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) ⁻¹' 𝒫 U, IsOpen t ∧ x ∈ t
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

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

pp: case lower
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z | z.im ≤ 0})

Tactic:
case' lower => apply Complex.isConnected_of_lowerHalfPlane ?_ <| Set.inter_subset_right

Goal state after:
case lower
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
⊢ {z | z.im < 0} ⊆ (σ ℂ a)ᶜ ∩ {z | z.im ≤ 0}

case upper
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
⊢ {z | 0 < z.im} ⊆ (σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
U : Set (α × β)
hU : U ∈ {V | IsOpen[instTopologicalSpaceProd] V}
⊢ IsOpen ((SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) ⁻¹' (fun V ↦ {s | (s ∩ V).Nonempty}) U)

Tactic:
rw [isOpen_iff_forall_mem_open]

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
U : Set (α × β)
hU : U ∈ {V | IsOpen[instTopologicalSpaceProd] V}
⊢ ∀ x ∈ (SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) ⁻¹' (fun V ↦ {s | (s ∩ V).Nonempty}) U,
    ∃ t ⊆ (SetLike.coe ∘ fun p ↦ p.1 ×ˢ p.2) ⁻¹' (fun V ↦ {s | (s ∩ V).Nonempty}) U, IsOpen t ∧ x ∈ t
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ Continuous fun p ↦ p.1 ×ˢ p.2

Tactic:
by
  rw [continuous_induced_rng, continuous_generateFrom_iff]
  rintro _ (⟨U, hU, rfl⟩ | ⟨U, hU, rfl⟩)
  · rw [isOpen_iff_forall_mem_open]
    intro ⟨K, L⟩ (hKL : (K : Set α) ×ˢ (L : Set β) ⊆ U)
    obtain ⟨V, W, hV, hW, hK, hL, hVW⟩ := generalized_tube_lemma K.isCompact L.isCompact hU hKL
    exact ⟨_, fun ⟨K', L'⟩ ⟨hK', hL'⟩ => (Set.prod_mono hK' hL').trans hVW,
      (isOpen_subsets_of_isOpen hV).prod (isOpen_subsets_of_isOpen hW), hK, hL⟩
  · rw [isOpen_iff_forall_mem_open]
    intro ⟨K, L⟩ ⟨⟨x, y⟩, ⟨(hx : x ∈ K), (hy : y ∈ L)⟩, hxy⟩
    obtain ⟨V, W, hV, hW, hxV, hyW, hVW⟩ := isOpen_prod_iff.mp hU x y hxy
    grw [preimage_ofPred_eq, ← hVW]
    simp_rw [Function.comp_apply, coe_prod, prod_inter_prod, prod_nonempty_iff]
    exact ⟨_, .rfl,
      (isOpen_inter_nonempty_of_isOpen hV).prod (isOpen_inter_nonempty_of_isOpen hW),
      ⟨x, hx, hxV⟩, ⟨y, hy, hyW⟩⟩

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

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
x : α
R : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : IsTopologicalSemiring β
inst✝² : Module R β
inst✝¹ : ContinuousConstSMul R β
inst✝ : SMulCommClass R β β
r : R
f g : α →C₀ β
⊢ r • f • g = f • r • g

Tactic:
by
    ext
    simp only [smul_eq_mul, coe_smul, coe_mul, Pi.smul_apply, Pi.mul_apply]
    rw [← smul_eq_mul, ← smul_eq_mul, smul_comm]

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

Goal state before:
pp: ι : Type u_2
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹³ : NontriviallyNormedField 𝕜₁
inst✝¹² : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹¹ : RingHomIsometric σ₁₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : UniformSpace E
inst✝⁵ : UniformSpace F
inst✝⁴ : IsUniformAddGroup E
inst✝³ : IsUniformAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst✝ : PolynormableSpace 𝕜₂ F
hp : WithSeminorms fun p ↦ ↑p
H : ∀ (x : E) (i : { p // Continuous[inst✝⁵.toTopologicalSpace, _] ⇑p }), BddAbove (⇑↑i '' range fun i ↦ (𝓕 i) x)
⊢ ∀ (k : { p // Continuous[inst✝⁵.toTopologicalSpace, _] ⇑p }) (x : E), BddAbove (range fun i ↦ ↑k ((𝓕 i) x))

Tactic:
← range_comp

Goal state after:
ι : Type u_2
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹³ : NontriviallyNormedField 𝕜₁
inst✝¹² : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹¹ : RingHomIsometric σ₁₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : UniformSpace E
inst✝⁵ : UniformSpace F
inst✝⁴ : IsUniformAddGroup E
inst✝³ : IsUniformAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
inst✝ : PolynormableSpace 𝕜₂ F
hp : WithSeminorms fun p ↦ ↑p
H : ∀ (x : E) (i : { p // Continuous[inst✝⁵.toTopologicalSpace, _] ⇑p }), BddAbove (range (⇑↑i ∘ fun i ↦ (𝓕 i) x))
⊢ ∀ (k : { p // Continuous[inst✝⁵.toTopologicalSpace, _] ⇑p }) (x : E), BddAbove (range fun i ↦ ↑k ((𝓕 i) x))
Module: Mathlib.Analysis.Normed.Module.WeakDual

Goal state before:
pp: 𝕜 : Type u_1
M : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : Module 𝕜 M
s : Set M
⊢ IsClosed (polar 𝕜 s)

Tactic:
simp only [polar_def, ofPred_forall]

Goal state after:
𝕜 : Type u_1
M : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : Module 𝕜 M
s : Set M
⊢ IsClosed (⋂ i ∈ s, {x | ‖x i‖ ≤ 1})
Module: Mathlib.Analysis.Normed.Module.WeakDual

Goal state before:
pp: 𝕜✝ : Type u_1
M : Type u_2
E✝ : Type u_3
inst✝¹⁵ : NontriviallyNormedField 𝕜✝
inst✝¹⁴ : AddCommGroup M
inst✝¹³ : TopologicalSpace M
inst✝¹² : Module 𝕜✝ M
inst✝¹¹ : SeminormedAddCommGroup E✝
inst✝¹⁰ : NormedSpace 𝕜✝ E✝
α : Type u_4
𝕜 : Type u_5
E : Type u_6
F : Type u_7
inst✝⁹ : TopologicalSpace α
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : TopologicalSpace F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
x : F
⊢ Continuous fun a ↦ re (((↑(toStrongDual ≪≫ₗ extendRCLikeₗ ≪≫ₗ LinearEquiv.restrictScalars ℝ toWeakDual)).toFun a) x)

Tactic:
simpa [extendRCLikeₗ_apply] using eval_continuous x

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‖₊}
⊢ ∃ b ∈ ↑I, nndist f b < ε

Tactic:
have ht : IsClosed t := isClosed_le continuous_const (map_continuous f).nnnorm

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
⊢ ∃ b ∈ ↑I, nndist f b < ε
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCommCStarAlgebra A
a b : A
h : a * b = 0
f : A → C(↑(characterSpace ℂ (Unitization ℂ A)), ℂ) :=
  ⇑(gelfandStarTransform (Unitization ℂ A)) ∘ ⇑(inrNonUnitalAlgHom ℂ A)
hf : Isometry f
⊢ ‖f a + f b‖ = max ‖f a‖ ‖f b‖

Tactic:
exact ContinuousMap.norm_add_eq_max <| by simpa [f] using congr(f $h)

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
ι : Type u_2
f : ι → A
s : Finset ι
h : ∀ i ∈ s, IsSelfAdjoint (f i)
h0 : Pairwise ((fun x1 x2 ↦ x1 * x2 = 0) on f)
⊢ ‖∑ i ∈ s, f i‖₊ = s.sup fun x ↦ ‖f x‖₊

Tactic:
by
  classical
  induction s using Finset.induction with
  | empty => simp
  | insert j s hj ih =>
    suffices f j * ∑ i ∈ s, f i = 0 by
      simp_all [(h j (by simp)).nnnorm_add_eq_max (by cfc_tac) this]
    simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h0 (by grind)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
𝔖 : Set (Set α)
inst✝ : PseudoEMetricSpace β
f : γ → α →ᵤ[𝔖] β
K : Set α → ℝ≥0
h : ∀ s ∈ 𝔖, ∀ c ∈ s, LipschitzWith (K s) fun x ↦ (toFun 𝔖) (f x) c
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, topologicalSpace α β 𝔖] f

Tactic:
by
  rw [UniformOnFun.continuous_rng_iff]
  refine fun s hs ↦ LipschitzWith.continuous (K := K s) ?_
  rw [UniformFun.lipschitzWith_iff]
  rintro ⟨y, hy⟩
  exact h s hs y hy

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

Goal state before:
pp: A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
r : ℝ≥0
⊢ cfc (fun x ↦ x⁺) ((algebraMap ℝ≥0 A) r) = (algebraMap ℝ≥0 A) r

Tactic:
IsScalarTower.algebraMap_apply ℝ≥0 ℝ A

Goal state after:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
r : ℝ≥0
⊢ cfc (fun x ↦ x⁺) ((algebraMap ℝ A) ((algebraMap ℝ≥0 ℝ) r)) = (algebraMap ℝ A) ((algebraMap ℝ≥0 ℝ) r)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

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

Tactic:
refine fun x hx ↦ continuousWithinAt_cfc_fun (h_cont x hx) ?_

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

Goal state before:
pp: case id
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
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 ⋯ ⋯) (ContinuousMap.restrict s (ContinuousMap.id 𝕜))

Tactic:
simp only [cfcHomSuperset_id]

Goal state after:
case id
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
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 ↦ a x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: case frequently
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
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
f : C(↑s, 𝕜)
hf :
  ∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f,
    Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcHomSuperset ⋯ ⋯) g
⊢ ∀ (i : ℝ),
    0 < i →
      ∃ F,
        Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
          ∀ (y : X), ((cfcHomSuperset ⋯ ⋯) f, F y) ∈ {p | dist p.1 p.2 ≤ i}

Tactic:
intro ε

Goal state after:
case frequently
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
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
f : C(↑s, 𝕜)
hf :
  ∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f,
    Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcHomSuperset ⋯ ⋯) g
ε : ℝ
⊢ 0 < ε →
    ∃ F,
      Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F ∧
        ∀ (y : X), ((cfcHomSuperset ⋯ ⋯) f, F y) ∈ {p | dist p.1 p.2 ≤ ε}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: case neg.refine_1
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬IsSelfAdjoint a
h : 0 ≤ ↑a
⊢ IsSelfAdjoint a

pp: case neg.refine_2
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬IsSelfAdjoint a
h : 0 ≤ a
⊢ IsSelfAdjoint a

Tactic:
· exact isSelfAdjoint_inr (R := ℂ) |>.mp <| .of_nonneg h

Goal state after:
case neg.refine_2
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬IsSelfAdjoint a
h : 0 ≤ a
⊢ IsSelfAdjoint a
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✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : s ∈ 𝓝ˢ (⋃ x ∈ t, spectrum 𝕜 (a x))
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hs' : ∀ i ∈ t, s ∈ 𝓝ˢ (spectrum 𝕜 (a i))
x : ↑t
⊢ ∃ S, IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a ↑x), spectrum 𝕜 x' ⊆ S) ∧ S ⊆ s

Tactic:
obtain ⟨S, ⟨hS₁, hS₂⟩, hS₃⟩ :=
      spectrum.isCompact (𝕜 := 𝕜) (a x) |>.nhdsSet_basis_isCompact.mem_iff.mp (hs' x x.2)

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✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : s ∈ 𝓝ˢ (⋃ x ∈ t, spectrum 𝕜 (a x))
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hs' : ∀ i ∈ t, s ∈ 𝓝ˢ (spectrum 𝕜 (a i))
x : ↑t
S : Set 𝕜
hS₃ : id S ⊆ s
hS₁ : S ∈ 𝓝ˢ (spectrum 𝕜 (a ↑x))
hS₂ : IsCompact S
⊢ ∃ S, IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a ↑x), spectrum 𝕜 x' ⊆ S) ∧ S ⊆ s