mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2.inr
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x✝ : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst✝] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst✝] s
U : Set α
hU : U ∈ {U | IsOpen[inst✝] U}
hs : t ∈ (fun V ↦ {s | (s ∩ V).Nonempty}) U
⊢ ⨅
      s_1 ∈
        {s_2 |
          s ∈ s_2 ∧
            s_2 ∈ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}},
      Filter.principal s_1 ≤
    Filter.principal ((fun V ↦ {s | (s ∩ V).Nonempty}) U)

Tactic:
obtain ⟨x, hxt, hxU⟩ := hs

Goal state after:
case refine_2.inr
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x✝ : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst✝] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst✝] s
U : Set α
hU : U ∈ {U | IsOpen[inst✝] U}
x : α
hxt : x ∈ t
hxU : x ∈ U
⊢ ⨅
      s_1 ∈
        {s_2 |
          s ∈ s_2 ∧
            s_2 ∈ powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}},
      Filter.principal s_1 ≤
    Filter.principal ((fun V ↦ {s | (s ∩ V).Nonempty}) U)
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⁻¹)
⊢ ∀ᶠ (x : A) in map (⇑(val S)) l, Ring.inverse x ∈ ↑S

Tactic:
Filter.eventually_map

Goal state after:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
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⁻¹)
⊢ ∀ᶠ (a : ↥S) in l, Ring.inverse ((val S) a) ∈ ↑S
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

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

Tactic:
by
  rw [cfcₙAux, NonUnitalStarAlgHom.comp_assoc, NonUnitalStarAlgHom.comp_apply]
  simp only [NonUnitalStarAlgHom.comp_apply, NonUnitalStarAlgHom.coe_coe]
  rw [cfcHom_map_spectrum (hp₁.mpr ha) (R := 𝕜) _]
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → Set β
hs : IsPreconnected s
hf : ContinuousOn f s
h : ∃ x ∈ s, IsPreconnected (f x)
⊢ IsPreconnected (⋃ x ∈ s, f x)

Tactic:
by
  rw [← sUnion_image]
  exact isPreconnected_sUnion (hs.image _ hf) (by grind)

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

Goal state before:
pp: case refine_2
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : QuasispectrumRestricts a ⇑Complex.reCLM
⊢ star a = cfcₙ id a

Tactic:
rw [← cfcₙ_star_id a (R := ℂ)]

Goal state after:
case refine_2
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : QuasispectrumRestricts a ⇑Complex.reCLM
⊢ cfcₙ (fun x ↦ star x) a = cfcₙ id a
Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ resolventSet 𝕜 a
H₁ :
  HasFDerivAt Ring.inverse (-((ContinuousLinearMap.mulLeftRight 𝕜 A) ↑(IsUnit.unit hk)⁻¹) ↑(IsUnit.unit hk)⁻¹)
    ((algebraMap 𝕜 A) k - a)
H₂ : HasFDerivAt (fun a ↦ (algebraMap 𝕜 A) k - a) (-ContinuousLinearMap.id 𝕜 A) a
⊢ HasFDerivAt (fun x ↦ resolvent x k) (((ContinuousLinearMap.mulLeftRight 𝕜 A) (resolvent a k)) (resolvent a k)) a

Tactic:
simpa [resolvent_eq hk] using! H₁.comp a H₂

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 : α → β
⊢ Continuous fun p ↦ p.1 ⊔ p.2

Tactic:
simp_rw [isEmbedding_coe.continuous_iff, Function.comp_def, coe_sup]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
⊢ Continuous[_, TopologicalSpace.vietoris α] fun x ↦ ↑x.1 ∪ ↑x.2
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}
⊢ ∃ t, ⋃ K ∈ S, ↑K ⊆ ⋃ i ∈ t, U i

Tactic:
refine ⟨s.biUnion id, (biUnion_subset_biUnion_left hs).trans ?_⟩
  simp_rw [biUnion_iUnion, iUnion_subset_iff, Finset.set_biUnion_biUnion]
  exact fun t ht K hK => subset_iUnion₂_of_subset t ht hK

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

Goal state after:
case h
𝕜 : 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
⊢ 0 ∈ B.polar s
Module: Mathlib.Analysis.LocallyConvex.HahnBanach

Goal state before:
pp: E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : PolynormableSpace 𝕜 E
S : Submodule 𝕜 E
f : StrongDual 𝕜 ↥S
⊢ ∃ g, ∀ (x : ↥S), g ↑x = f x

Tactic:
obtain ⟨q, hq_cont, hq⟩ := Seminorm.exists_le_comp_of_isInducing (f := S.subtype)
    (p := f.toSeminorm) f.continuous.norm IsInducing.subtypeVal

Goal state after:
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : PolynormableSpace 𝕜 E
S : Submodule 𝕜 E
f : StrongDual 𝕜 ↥S
q : Seminorm 𝕜 E
hq_cont : Continuous[inst✝⁴, _] ⇑q
hq : (↑f).toSeminorm ≤ q.comp S.subtype
⊢ ∃ g, ∀ (x : ↥S), g ↑x = f x
Module: Mathlib.Analysis.Normed.Module.HahnBanach

Goal state before:
pp: case neg
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : ¬x = 0
⊢ ∃ g, ‖g‖ = 1 ∧ g x = ↑‖x‖

Tactic:
exact exists_dual_vector 𝕜 x (norm_ne_zero_iff.mpr hx)

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Completeness

Goal state before:
pp: case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
Fₗ : Type u_5
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup Fₗ
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜 Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
f✝ g : E →SL[σ₁₂] F
E' : Type u_6
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : RingHomIsometric σ₁₂
f : E' → F
s : Set (E' →SL[σ₁₂] F)
hs : Bornology.IsBounded s
hf : f ∈ closure[Pi.topologicalSpace] (DFunLike.coe '' s)
C : ℝ
hC : ∀ x ∈ s, ‖x‖ ≤ C
⊢ ∃ C, ∀ (x : E'), ‖(linearMapOfMemClosureRangeCoe f ⋯) x‖ ≤ C * ‖x‖

Tactic:
have : ∀ x, IsClosed { g : E' → F | ‖g x‖ ≤ C * ‖x‖ } := fun x =>
      isClosed_Iic.preimage (@continuous_apply E' (fun _ => F) _ x).norm

Goal state after:
case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
Fₗ : Type u_5
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup Fₗ
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜 Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
f✝ g : E →SL[σ₁₂] F
E' : Type u_6
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : RingHomIsometric σ₁₂
f : E' → F
s : Set (E' →SL[σ₁₂] F)
hs : Bornology.IsBounded s
hf : f ∈ closure[Pi.topologicalSpace] (DFunLike.coe '' s)
C : ℝ
hC : ∀ x ∈ s, ‖x‖ ≤ C
this : ∀ (x : E'), IsClosed[Pi.topologicalSpace] {g | ‖g x‖ ≤ C * ‖x‖}
⊢ ∃ C, ∀ (x : E'), ‖(linearMapOfMemClosureRangeCoe f ⋯) x‖ ≤ C * ‖x‖
Module: Mathlib.LinearAlgebra.AffineSpace.Ordered

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < r * (b - a)
⊢ f (r * (b - a) + a) ≤ r • (f b - f a) + f a ↔
    f (r * (b - a) + a) ≤ (r * (b - a) * (b - a)⁻¹) • (f b - f a + r⁻¹ • f a)

Tactic:
mul_inv_cancel_right₀ (right_ne_zero_of_mul h.ne'),

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : LinearOrder k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
inst✝ : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < r * (b - a)
⊢ f (r * (b - a) + a) ≤ r • (f b - f a) + f a ↔ f (r * (b - a) + a) ≤ r • (f b - f a + r⁻¹ • f a)
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: A : Type u_1
inst✝ : CommCStarAlgebra A
a : A
⊢ star ((gelfandTransform ℂ A).toRingHom a) ∈ (gelfandTransform ℂ A).range.carrier

Tactic:
use star a

Goal state after:
case h
A : Type u_1
inst✝ : CommCStarAlgebra A
a : A
⊢ (gelfandTransform ℂ A).toRingHom (star a) = star ((gelfandTransform ℂ A).toRingHom a)
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCommCStarAlgebra A
ι : Type u_2
f : ι → A
h0 : Pairwise ((fun x1 x2 ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : ‖∑ i ∈ s, f i‖₊ = s.sup fun x ↦ ‖f x‖₊
this : f j * ∑ i ∈ s, f i = 0
⊢ ‖∑ i ∈ insert j s, f i‖₊ = (insert j s).sup fun x ↦ ‖f x‖₊

Tactic:
simp_all [nnnorm_add_eq_max this]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
A : ι → Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalSemiring R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : (i : ι) → Ring (A i)
inst✝⁷ : (i : ι) → Algebra S (A i)
inst✝⁶ : (i : ι) → Algebra R (A i)
inst✝⁵ : ∀ (i : ι), IsScalarTower R S (A i)
hinst : IsScalarTower R S ((i : ι) → A i)
inst✝⁴ : (i : ι) → StarRing (A i)
inst✝³ : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst✝² : ContinuousFunctionalCalculus R ((i : ι) → A i) p
inst✝¹ : ∀ (i : ι), ContinuousFunctionalCalculus R (A i) (q i)
inst✝ : ∀ (i : ι), ContinuousMap.UniqueHom R (A i)
f : R → R
a : (i : ι) → A i
hf : ContinuousOn f (⋃ i, spectrum R (a i))
ha : p a
ha' : ∀ (i : ι), q i (a i)
i : ι
φ : ((i : ι) → A i) →⋆ₐ[S] A i := Pi.evalStarAlgHom S A i
⊢ ContinuousOn f (spectrum R a)

Tactic:
rwa [Pi.spectrum_eq]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
R : Type u_3
S : Type u_4
inst✝²³ : CommSemiring R
inst✝²² : StarRing R
inst✝²¹ : MetricSpace R
inst✝²⁰ : IsTopologicalSemiring R
inst✝¹⁹ : ContinuousStar R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
inst✝¹⁶ : Ring A
inst✝¹⁵ : Ring B
inst✝¹⁴ : Algebra S A
inst✝¹³ : Algebra S B
inst✝¹² : Algebra R A
inst✝¹¹ : Algebra R B
inst✝¹⁰ : IsScalarTower R S A
inst✝⁹ : IsScalarTower R S B
inst✝⁸ : StarRing A
inst✝⁷ : StarRing B
inst✝⁶ : TopologicalSpace A
inst✝⁵ : TopologicalSpace B
pab : A × B → Prop
pa : A → Prop
pb : B → Prop
inst✝⁴ : ContinuousFunctionalCalculus R (A × B) pab
inst✝³ : ContinuousFunctionalCalculus R A pa
inst✝² : ContinuousFunctionalCalculus R B pb
inst✝¹ : ContinuousMap.UniqueHom R A
inst✝ : ContinuousMap.UniqueHom R B
f : R → R
a : A
b : B
hf : ContinuousOn f (spectrum R a ∪ spectrum R b)
hab : pab (a, b)
ha : pa a
hb : pb b
⊢ cfc f (a, b) = (cfc f a, cfc f b)

Tactic:
ext
  case fst =>
    let φ := StarAlgHom.fst S A B
    exact φ.map_cfc f (a, b) (by rwa [Prod.spectrum_eq]) continuous_fst hab ha
  case snd =>
    let φ := StarAlgHom.snd S A B
    exact φ.map_cfc f (a, b) (by rwa [Prod.spectrum_eq]) continuous_snd hab hb

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 β
inst✝ : Finite ↑𝔖
⊢ 𝓤 (α →ᵤ[𝔖] β) = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}

Tactic:
by
    let _ := Fintype.ofFinite 𝔖;
    simp_rw [← isUniformInducing_pi_restrict.comap_uniformity,
      PseudoEMetricSpace.uniformity_edist, comap_iInf, comap_principal, edist_eq_pi_restrict,
      Set.preimage_ofPred_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst✝¹ : PseudoEMetricSpace β
inst✝ : Finite ↑𝔖
f g : α →ᵤ[𝔖] β
C : ℝ≥0∞
⊢ ⨆ x ∈ ⋃₀ 𝔖, edist ((toFun 𝔖) f x) ((toFun 𝔖) g x) ≤ C ↔ ∀ x ∈ ⋃₀ 𝔖, edist ((toFun 𝔖) f x) ((toFun 𝔖) g x) ≤ C

Tactic:
iSup₂_le_iff

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
⊢ Function.Bijective (characterSpaceToSpectrum a)

Tactic:
refine ⟨fun φ ψ h => starAlgHomClass_ext ℂ ?_ ?_ ?_, ?_⟩

Goal state after:
case refine_1
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
φ ψ : ↑(characterSpace ℂ ↥(elemental ℂ a))
h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ
⊢ Continuous ⇑φ

case refine_2
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
φ ψ : ↑(characterSpace ℂ ↥(elemental ℂ a))
h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ
⊢ Continuous ⇑ψ

case refine_3
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
φ ψ : ↑(characterSpace ℂ ↥(elemental ℂ a))
h : characterSpaceToSpectrum a φ = characterSpaceToSpectrum a ψ
⊢ φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩

case refine_4
A : Type u_1
inst✝¹ : CStarAlgebra A
a : A
inst✝ : IsStarNormal a
⊢ Function.Surjective (characterSpaceToSpectrum a)
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
ha : IsSelfAdjoint a
⊢ ‖cfcₙ (fun x ↦ x) a‖ ≤ max ‖a⁺‖ ‖a⁻‖

Tactic:
norm_cfcₙ_le_iff ..

Goal state after:
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
ha : IsSelfAdjoint a
⊢ ∀ x ∈ quasispectrum ℝ a, ‖x‖ ≤ max ‖a⁺‖ ‖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' : s ∈ 𝓝ˢ (⋃ x ∈ t, spectrum 𝕜 (a x))
⊢ ContinuousOn (fun x ↦ cfc f (a x)) t

Tactic:
simp only [nhdsSet_iUnion, mem_iSup] 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✝¹ : 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))
⊢ ContinuousOn (fun x ↦ cfc f (a x)) t
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: case pos
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
ha : IsStrictlyPositive a
⊢ sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ

Tactic:
rw [sqrt_eq_rpow, sqrt_eq_rpow, inverse_rpow _ _ (by grind),
        inverse_eq_rpow_neg_one, rpow_rpow _ _ _ (by grind)]
    grind only

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

Goal state before:
pp: X : Type u_1
A : Type u_2
inst✝¹¹ : NormedRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : NormedAlgebra ℝ A
inst✝⁸ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁷ : ContinuousStar A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : NonnegSpectrumClass ℝ A
inst✝³ : T2Space A
inst✝² : IsSemitopologicalRing A
inst✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : s ∈ 𝓝ˢ (⋃ x ∈ t, spectrum ℝ≥0 (a x))
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hs' : s ∈ 𝓝ˢ (⋃ x ∈ t, spectrum ℝ≥0 (a x))
⊢ ContinuousOn (fun x ↦ cfc f (a x)) t

Tactic:
simp only [nhdsSet_iUnion, mem_iSup] at hs'

Goal state after:
X : Type u_1
A : Type u_2
inst✝¹¹ : NormedRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : NormedAlgebra ℝ A
inst✝⁸ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁷ : ContinuousStar A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : NonnegSpectrumClass ℝ A
inst✝³ : T2Space A
inst✝² : IsSemitopologicalRing A
inst✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : s ∈ 𝓝ˢ (⋃ x ∈ t, spectrum ℝ≥0 (a x))
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hs' : ∀ i ∈ t, s ∈ 𝓝ˢ (spectrum ℝ≥0 (a i))
⊢ ContinuousOn (fun x ↦ cfc f (a x)) t
Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions

Goal state before:
pp: A : Type u_1
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℂ E
x : E
⊢ ‖x‖ = √‖⟪x, x⟫_ℂ‖

Tactic:
simpa only [← inner_self_re_eq_norm] using norm_eq_sqrt_re_inner x

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✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : TopologicalSpace X
s : X → Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ContinuousOn a t
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, quasispectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) t

Tactic:
rw [ContinuousOn] at ha_cont ⊢
  refine fun x hx ↦ (ha_cont x hx).cfcₙ (hs x hx) f hx ?_ ?_ (hf x hx)
  all_goals filter_upwards [ha x hx, self_mem_nhdsWithin] with x hx hxt
  exacts [hx, ha' x hxt]

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✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : ContinuousStar A
inst✝² : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : s ∈ 𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : s ∈ 𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) t

Tactic:
simp only [nhdsSet_iUnion, mem_iSup] at hs'

Goal state after:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : ContinuousStar A
inst✝² : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : s ∈ 𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ i ∈ t, s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) t
Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : MeasurableSpace X
μ : Measure X
inst✝² : TopologicalSpace Y
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompactSpace Y
f : X → C(Y, E)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖(f x) y‖ ≤ bound x
h : Nonempty Y
bound_nonneg : 0 ≤ᵐ[μ] bound
x : X
bound_ge_x : ∀ (y : Y), ‖(f x) y‖ ≤ bound x
⊢ 0 x ≤ bound x → ‖f x‖ ≤ bound x

Tactic:
bound_nonneg_x

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : MeasurableSpace X
μ : Measure X
inst✝² : TopologicalSpace Y
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompactSpace Y
f : X → C(Y, E)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖(f x) y‖ ≤ bound x
h : Nonempty Y
bound_nonneg : 0 ≤ᵐ[μ] bound
x : X
bound_ge_x : ∀ (y : Y), ‖(f x) y‖ ≤ bound x
bound_nonneg_x : 0 x ≤ bound x
⊢ ‖f x‖ ≤ bound x
Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁴ : MeasurableSpace X
μ : Measure X
inst✝³ : TopologicalSpace Y
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : CompactSpace Y
inst✝ : Zero Y
f : X → C(Y, E)₀
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖(f x) y‖ ≤ bound x
bound_nonneg : 0 ≤ᵐ[μ] bound
x : X
bound_ge_x : ∀ (y : Y), ‖(f x) y‖ ≤ bound x
⊢ 0 x ≤ bound x → ‖f x‖ ≤ bound x

Tactic:
bound_nonneg_x

Goal state after:
X : Type u_1
Y : Type u_2
inst✝⁴ : MeasurableSpace X
μ : Measure X
inst✝³ : TopologicalSpace Y
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : CompactSpace Y
inst✝ : Zero Y
f : X → C(Y, E)₀
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖(f x) y‖ ≤ bound x
bound_nonneg : 0 ≤ᵐ[μ] bound
x : X
bound_ge_x : ∀ (y : Y), ‖(f x) y‖ ≤ bound x
bound_nonneg_x : 0 x ≤ bound x
⊢ ‖f x‖ ≤ bound x