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

Goal state before:
pp: case neg.inr.inl.hf
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
hfg : Set.EqOn f g (σₙ R a)
hg : ¬ContinuousOn g (σₙ R a)
⊢ ¬ContinuousOn f (σₙ R a)

Tactic:
exact fun hf ↦ hg (hf.congr hfg.symm)

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

Goal state before:
pp: case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
ha : p a
⊢ cfcₙ (fun x ↦ f x * g x) a = cfcₙ f a * cfcₙ g a

Tactic:
rw [cfcₙ_apply f a, cfcₙ_apply g a, ← map_mul, cfcₙ_apply _ a]
    congr

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
n k ν : ℕ
⊢ k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n (ν + 1))) = 0

Tactic:
induction k generalizing n ν with

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

Goal state before:
pp: ⊢ (polynomialFunctions I).topologicalClosure = ⊤

Tactic:
apply top_unique
  rintro f -
  refine mem_closure_of_tendsto (bernsteinApproximation_uniform f) <| .of_forall fun n ↦ ?_
  apply Subalgebra.sum_mem
  rintro i -
  rw [← SetLike.mem_coe, polynomialFunctions_coe]
  use bernsteinPolynomial ℝ n i * .C (f (bernstein.z i))
  ext
  simp [bernstein]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)
mem_closure : p ∈ (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).topologicalClosure
frequently_mem_polynomials :
  ∃ᶠ (x : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)) in nhds p, x ∈ ↑(polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).toSubsemiring
⊢ ∀ x ∈ ↑(polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).toSubsemiring,
    (compRightContinuousMap ℝ (↑f).attachBound) x ∈ ↑A.toSubsemiring

Tactic:
rintro _ ⟨g, ⟨-, rfl⟩⟩

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)
mem_closure : p ∈ (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).topologicalClosure
frequently_mem_polynomials :
  ∃ᶠ (x : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)) in nhds p, x ∈ ↑(polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).toSubsemiring
g : ℝ[X]
⊢ (compRightContinuousMap ℝ (↑f).attachBound) (↑(Polynomial.toContinuousMapOnAlgHom (Set.Icc (-‖f‖) ‖f‖)) g) ∈
    ↑A.toSubsemiring
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
⊢ (comap (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) (restrictScalars ℝ A.toSubalgebra)).SeparatesPoints

Tactic:
intro x₁

Goal state after:
𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ : X
⊢ ∀ ⦃y : X⦄,
    x₁ ≠ y →
      ∃ f ∈ (fun f ↦ ⇑f) '' ↑(comap (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) (restrictScalars ℝ A.toSubalgebra)),
        f x₁ ≠ f y
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case smul
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f✝ : C(↑s, 𝕜)
r : 𝕜
f : C(↑s, 𝕜)
hx✝ : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf : (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩) f = 0
⊢ (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩) (r • f) = 0

Tactic:
rw [map_smul, hf, smul_zero]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
frequently : ∀ (f : C(↑s, 𝕜)₀), (∃ᶠ (g : C(↑s, 𝕜)₀) in 𝓝 f, p g) → p f
f✝ : C(↑s, 𝕜)₀
h : ∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id s}, p f
f : C(↑s, 𝕜)₀
⊢ ∃ᶠ (g : C(↑s, 𝕜)₀) in 𝓝 f, p g

Tactic:
have := (ContinuousMapZero.adjoin_id_dense s).closure_eq ▸ Set.mem_univ (x := f)

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
frequently : ∀ (f : C(↑s, 𝕜)₀), (∃ᶠ (g : C(↑s, 𝕜)₀) in 𝓝 f, p g) → p f
f✝ : C(↑s, 𝕜)₀
h : ∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id s}, p f
f : C(↑s, 𝕜)₀
this : f ∈ closure ↑(adjoin 𝕜 {ContinuousMapZero.id s})
⊢ ∃ᶠ (g : C(↑s, 𝕜)₀) in 𝓝 f, p g
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
⊢ LowerHemicontinuousWithinAt (fun x ↦ {f x}) s x → ContinuousWithinAt f s x

Tactic:
simp only [lowerHemicontinuousWithinAt_iff, Set.singleton_inter_nonempty,
    ContinuousWithinAt, tendsto_iff_forall_eventually_mem]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
⊢ (∀ (u : Set β), IsOpen[inst✝] u → f x ∈ u → ∀ᶠ (x' : α) in 𝓝[s] x, f x' ∈ u) →
    ∀ s_1 ∈ 𝓝 (f x), ∀ᶠ (x : α) in 𝓝[s] x, f x ∈ s_1
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NormedField 𝕜
B : Type u_3
inst✝⁵ : NonUnitalNormedRing B
inst✝⁴ : NormedSpace 𝕜 B
inst✝³ : CompleteSpace B
inst✝² : IsScalarTower 𝕜 B B
inst✝¹ : SMulCommClass 𝕜 B B
inst✝ : ProperSpace 𝕜
a : B
⊢ IsCompact (quasispectrum 𝕜 a)

Tactic:
by
  rw [Unitization.quasispectrum_eq_spectrum_inr' 𝕜 𝕜,
    ← AlgEquiv.spectrum_eq (WithLp.unitizationAlgEquiv 𝕜).symm (a : Unitization 𝕜 B)]
  exact spectrum.isCompact _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_4
inst✝ : Finite ι
⊢ Continuous[Pi.topologicalSpace, TopologicalSpace.vietoris α] range

Tactic:
by
  simp_rw [continuous_iff, powerset, preimage_ofPred_eq, range_subset_iff, ofPred_forall]
  exact ⟨
    fun U hU => isOpen_iInter_of_finite fun i => hU.preimage <| continuous_apply i,
    fun F hF => isClosed_iInter fun i => hF.preimage <| continuous_apply i⟩

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⟩

Goal state after:
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

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
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀ u ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B}, IsOpen u

Tactic:
simp_rw [forall_mem_image]

Goal state after:
case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀ ⦃x : Set (Set α)⦄, x ∈ {u | u.Finite ∧ u ⊆ B} → IsOpen {K | ↑K ⊆ ⋃₀ x ∧ ∀ U ∈ x, (↑K ∩ U).Nonempty}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀
    u ∈
      preimage SetLike.coe ''
        (fun p ↦ {s | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
          {p | IsOpen[inst✝] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1},
    ∀ x ∈ u, ∃ v ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B}, x ∈ v ∧ v ⊆ u

Tactic:
simp_rw [forall_mem_image]

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀ ⦃x : Set α × Set (Set α)⦄,
    x ∈ {p | IsOpen[inst✝] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1} →
      ∀ x_1 ∈ SetLike.coe ⁻¹' {s | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty},
        ∃ v ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B},
          x_1 ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

Goal state before:
pp: A : Type u_1
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarRing A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : IsSemitopologicalRing A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : SMulCommClass ℝ A A
inst✝² : T2Space A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ a
⊢ cfcₙHom ha = QuasispectrumRestricts.nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯

Tactic:
apply (QuasispectrumRestricts.nnreal_of_nonneg ha).cfcₙHom_eq_restrict _

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

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

Tactic:
by
  rw [(IsSelfAdjoint.star_mul_self a).toReal_spectralRadius_complex_eq_norm,
    CStarRing.norm_star_mul_self, ← pow_two]

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

Goal state before:
pp: A : Type u_2
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra ℂ A
hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0
a : A
z : ℂ
h : z ∈ spectrum ℂ a
⊢ (algebraMap ℂ A) z = a

Tactic:
rwa [mem_iff, hA, Classical.not_not, sub_eq_zero] at h

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ IsOpen (range toCompacts)

Tactic:
by
    rw [range_toCompacts]
    exact Compacts.isClopen_singleton_bot.compl.isOpen

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀ u ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u.Nonempty ∧ u ⊆ B}, IsOpen u

Tactic:
simp_rw [forall_mem_image]

Goal state after:
case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀ ⦃x : Set (Set α)⦄, x ∈ {u | u.Finite ∧ u.Nonempty ∧ u ⊆ B} → IsOpen {K | ↑K ⊆ ⋃₀ x ∧ ∀ U ∈ x, (↑K ∩ U).Nonempty}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀ u ∈ preimage toCompacts '' (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B},
    ∀ x ∈ u,
      ∃ v ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u.Nonempty ∧ u ⊆ B}, x ∈ v ∧ v ⊆ u

Tactic:
simp_rw [forall_mem_image]

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀ ⦃x : Set (Set α)⦄,
    x ∈ {u | u.Finite ∧ u ⊆ B} →
      ∀ x_1 ∈ toCompacts ⁻¹' {K | ↑K ⊆ ⋃₀ x ∧ ∀ U ∈ x, (↑K ∩ U).Nonempty},
        ∃ v ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u.Nonempty ∧ u ⊆ B},
          x_1 ∈ v ∧ v ⊆ toCompacts ⁻¹' {K | ↑K ⊆ ⋃₀ x ∧ ∀ U ∈ x, (↑K ∩ U).Nonempty}
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : PartialOrder 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : LocallyConvexSpace 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : FirstCountableTopology E
u : ℕ → Set E
hu_basis : (𝓝 0).HasAntitoneBasis u
hu_zero : ∀ (n : ℕ), 0 ∈ interior (u n)
v : ℕ → Set E := fun n ↦ (absConvexHull 𝕜) (interior (u n))
hv_open : ∀ (n : ℕ), IsOpen[inst✝⁵] (v n)
hv_nhds : ∀ (n : ℕ), v n ∈ 𝓝 0
n : ℕ
a✝ : True
W : Set E
hWn : id W ⊆ u ?m.227
hW_nhds : W ∈ 𝓝 0
hW_abs : AbsConvex 𝕜 W
⊢ ∃ i', True ∧ v i' ⊆ u n

Tactic:
obtain ⟨m, hm⟩ := hu_basis.mem_iff.mp hW_nhds

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : PartialOrder 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : LocallyConvexSpace 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : FirstCountableTopology E
u : ℕ → Set E
hu_basis : (𝓝 0).HasAntitoneBasis u
hu_zero : ∀ (n : ℕ), 0 ∈ interior (u n)
v : ℕ → Set E := fun n ↦ (absConvexHull 𝕜) (interior (u n))
hv_open : ∀ (n : ℕ), IsOpen[inst✝⁵] (v n)
hv_nhds : ∀ (n : ℕ), v n ∈ 𝓝 0
n : ℕ
a✝ : True
W : Set E
hWn : id W ⊆ u ?m.227
hW_nhds : W ∈ 𝓝 0
hW_abs : AbsConvex 𝕜 W
m : ℕ
hm : u m ⊆ W
⊢ ∃ i', True ∧ v i' ⊆ u n
Module: Mathlib.Analysis.Normed.Module.Dual

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed[ContinuousLinearMap.topologicalSpace] ((topDualPairing 𝕜 E).flip.polar s)

Tactic:
simp only [LinearMap.polar_eq_iInter, LinearMap.flip_apply]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed[ContinuousLinearMap.topologicalSpace] (⋂ x ∈ s, {y | ‖((topDualPairing 𝕜 E) y) x‖ ≤ 1})
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ GaloisConnection setOfIdeal (idealOfSet R)

Tactic:
by
  refine fun I s => ⟨fun h f hf => ?_, fun h x hx => ?_⟩
  · by_contra h'
    rcases notMem_idealOfSet.mp h' with ⟨x, hx, hfx⟩
    exact hfx (notMem_setOfIdeal.mp (mt (@h x) hx) hf)
  · obtain ⟨f, hf, hfx⟩ := mem_setOfIdeal.mp hx
    by_contra hx'
    exact notMem_idealOfSet.mpr ⟨x, hx', hfx⟩ (h hf)

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

Goal state before:
pp: A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : I.IsMaximal
a : A
ha : a ∈ I
⊢ ⋯.some = 0

Tactic:
spectrum.zero_eq

Goal state after:
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : I.IsMaximal
a : A
ha : a ∈ I
⊢ ⋯.some = 0
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: case refine_2
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
f : ↑(characterSpace ℂ A)
⊢ f a ∈ spectrum ℂ a

Tactic:
exact AlgHom.apply_mem_spectrum f a

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

Goal state before:
pp: A : Type u_1
inst✝ : CommCStarAlgebra A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) :=
  let __Subalgebra := (gelfandTransform ℂ A).range;
  { toSubalgebra := __Subalgebra, star_mem' := ⋯ }
⊢ Function.Surjective ⇑(gelfandTransform ℂ A)

Tactic:
suffices rng = ⊤ from
    fun x => show x ∈ rng from this.symm ▸ StarSubalgebra.mem_top

Goal state after:
A : Type u_1
inst✝ : CommCStarAlgebra A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) :=
  let __Subalgebra := (gelfandTransform ℂ A).range;
  { toSubalgebra := __Subalgebra, star_mem' := ⋯ }
⊢ rng = ⊤
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
a : A
ha : IsSelfAdjoint a
⊢ a⁻ = 0 ↔ 0 ≤ a

Tactic:
rw [← posPart_eq_self, eq_comm (b := a)]

Goal state after:
A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : IsSelfAdjoint a
⊢ a⁻ = 0 ↔ a = a⁺
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: case neg
A : Type u_2
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : ∀ x ∈ spectrum ℝ a, 0 ≤ x
r : ℝ
hr : 0 ≤ r
a✝ : Nontrivial A
x : ℝ
hx : x ∈ spectrum ℝ (r • a)
hr' : ¬r = 0
⊢ 0 ≤ x

Tactic:
· lift r to ℝˣ using IsUnit.mk0 r hr'
    rw [← Units.smul_def, spectrum.unit_smul_eq_smul, Set.mem_smul_set_iff_inv_smul_mem] at hx
    refine le_of_smul_le_smul_left ?_ (inv_pos.mpr <| lt_of_le_of_ne hr <| ne_comm.mpr hr')
    simpa [Units.smul_def] using ha _ hx

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
⊢ -(star c * c) = -a⁻ * a * a⁻

Tactic:
by
      simp only [star_mul, c, mul_assoc, ← mul_assoc (star b), ← a_def, CFC.negPart_def,
        neg_mul, IsSelfAdjoint.cfcₙ (f := (·⁻)).star_eq]

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
x : ℂ
⊢ x ∈ σₙ ℂ a → 0 ≤ x

Tactic:
rw [mem_quasispectrum_iff]
    refine (Or.elim · ge_of_eq fun hx ↦ ?_)
    obtain ⟨y, hy, rfl⟩ := (IsSelfAdjoint.of_nonneg ha).spectrumRestricts.algebraMap_image ▸ hx
    simpa using spectrum_nonneg_of_nonneg ha hy

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

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace ℝ A
inst✝³ : SMulCommClass ℝ A A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : StarRing A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
⊢ ‖a⁻‖ ≤ ‖a‖

Tactic:
by
  simpa [CFC.negPart_neg] using norm_posPart_le (-a)

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
⊢ sqrt a = cfc (⇑NNReal.sqrt) a

Tactic:
unfold sqrt
  rw [cfcₙ_eq_cfc]

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
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConvexOn ℝ s (inr ∘ f)
x : A
hx : x ∈ s
y : A
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ a • f x + b • f y

Tactic:
rw [← Unitization.inr_le_iff _ _]

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConvexOn ℝ s (inr ∘ f)
x : A
hx : x ∈ s
y : A
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ↑(f (a • x + b • y)) ≤ ↑(a • f x + b • f y)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConcaveOn ℝ s (inr ∘ f)
x : A
hx : x ∈ s
y : A
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ≤ f (a • x + b • y)

Tactic:
rw [← Unitization.inr_le_iff _ _]

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConcaveOn ℝ s (inr ∘ f)
x : A
hx : x ∈ s
y : A
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ↑(a • f x + b • f y) ≤ ↑(f (a • x + b • y))
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: case neg
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬0 ≤ a
ha' : ¬0 ≤ ↑a
⊢ CFC.sqrt ↑a = ↑(CFC.sqrt a)

Tactic:
· rw [CFC.sqrt, CFC.sqrt, cfcₙ_apply_of_not_predicate _ ha,
      cfcₙ_apply_of_not_predicate _ ha', inr_zero]

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 : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
ha_cont : ContinuousOn a Set.univ
hs : ∀ (x : X), IsCompact (s x)
ha : ∀ (x₀ : X), ∀ᶠ (x : X) in 𝓝 x₀, spectrum 𝕜 (a x) ⊆ s x₀
hf : ∀ (x : X), ContinuousOn f (s x)
ha' : ∀ (x : X), p (a x)
⊢ ContinuousOn (fun x ↦ cfc f (a x)) Set.univ

Tactic:
exact ha_cont.cfc f (fun x _ ↦ hs x) (fun x _ ↦ by simpa using ha x) (fun x _ ↦ ha' x)

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 : A
b : Aˣ
ha : 0 ≤ a
hb : 0 ≤ ↑b
⊢ a ≤ ↑b ↔ ‖sqrt a * sqrt ↑b⁻¹‖ ≤ 1

Tactic:
rw [CFC.sqrt_eq_rpow (a := (↑b⁻¹ : A)), ← CFC.rpow_neg_one_eq_inv b,
    CFC.rpow_rpow (b : A) _ _ (by simp),
    le_iff_norm_sqrt_mul_rpow a (hb := b.isUnit.isStrictlyPositive hb)]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
b : Aˣ
ha : 0 ≤ a
hb : 0 ≤ ↑b
⊢ ‖sqrt a * ↑b ^ (-(1 / 2))‖ ≤ 1 ↔ ‖sqrt a * ↑b ^ (-1 * (1 / 2))‖ ≤ 1