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

Goal state before:
pp: case e'_5.e_6
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : Zero X
A : Type u_2
inst✝² : NonUnitalRing A
inst✝¹ : StarRing A
inst✝ : Module ℝ A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
f : C(X, ℝ≥0)₀
⊢ ({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ }.comp f).toNNReal = f

Tactic:
ext x

Goal state after:
case e'_5.e_6
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : Zero X
A : Type u_2
inst✝² : NonUnitalRing A
inst✝¹ : StarRing A
inst✝ : Module ℝ A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
f : C(X, ℝ≥0)₀
x : X
⊢ ↑(({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ }.comp f).toNNReal x) = ↑(f x)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: case e'_6.e_6
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : Zero X
A : Type u_2
inst✝² : NonUnitalRing A
inst✝¹ : StarRing A
inst✝ : Module ℝ A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
f : C(X, ℝ≥0)₀
⊢ (-{ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ }.comp f).toNNReal = 0

Tactic:
ext x

Goal state after:
case e'_6.e_6
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : Zero X
A : Type u_2
inst✝² : NonUnitalRing A
inst✝¹ : StarRing A
inst✝ : Module ℝ A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
f : C(X, ℝ≥0)₀
x : X
⊢ ↑((-{ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ }.comp f).toNNReal x) = ↑(0 x)
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : DenselyNormedField 𝕜
inst✝⁸ : NonUnitalNormedRing E
inst✝⁷ : StarRing E
inst✝⁶ : CStarRing E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : IsScalarTower 𝕜 E E
inst✝³ : SMulCommClass 𝕜 E E
inst✝² : StarRing 𝕜
inst✝¹ : StarModule 𝕜 E
inst✝ : CStarRing 𝕜
x✝ x : Unitization 𝕜 E
h : (algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2 = 0
⊢ ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2‖ ≤
    ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1⋆ + (mul 𝕜 E) x.toProd.2⋆‖

Tactic:
simp only [h, norm_zero]
        exact norm_nonneg _

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
y : F
⊢ (fun x ↦ (B x) (-y)) = fun a ↦ ((fun x y ↦ (B x) y) ∘ fun a ↦ -a) a y

Tactic:
ext x

Goal state after:
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
y : F
x : WeakBilin B
⊢ (B x) (-y) = ((fun x y ↦ (B x) y) ∘ fun a ↦ -a) x y
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
⊢ ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) =
    ↑(span 𝕜 ({1} ∪ ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})))

Tactic:
ext x

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
x : C(↑s, 𝕜)
⊢ x ∈ ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) ↔
    x ∈ ↑(span 𝕜 ({1} ∪ ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})))
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
⊢ ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) = ↑(𝕜 ∙ 1) + ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})

Tactic:
ext x

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
x : C(↑s, 𝕜)
⊢ x ∈ ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) ↔
    x ∈ ↑(𝕜 ∙ 1) + ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
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 : f ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))
⊢ r • f ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))

Tactic:
rw [SetLike.mem_coe, RingHom.mem_ker] at hf ⊢
    rw [map_smul, hf, smul_zero]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : RingHom.ker φ = RingHom.ker ψ
⊢ φ = ψ

Tactic:
ext x

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : RingHom.ker φ = RingHom.ker ψ
x : A
⊢ φ x = ψ x
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

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

Tactic:
rw [add_apply, this, add_zero, smul_apply, one_apply, smul_eq_mul, mul_one] at hf₂

Goal state after:
case mp
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
r : 𝕜
f : C(↑s, 𝕜)
hf : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf₂ : r = 0
this : f ⟨0, h0⟩ = 0
⊢ r • 1 + f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2.inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h✝ : s.Nonempty
u : Set (Set α)
hu₁ : u ⊆ {U | IsOpen[inst✝] U}
hu₂ : u.Finite
hu : powerset '' u ⊆ powerset '' {U | IsOpen[inst✝] U}
v : Set (Set α)
hv₁ : v ⊆ {U | IsOpen[inst✝] U}
hv₂ : v.Finite
hv : (fun V ↦ {s | (s ∩ V).Nonempty}) '' v ⊆ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝] U}
ht₁ : (powerset '' u).Finite ∧ ((fun V ↦ {s | (s ∩ V).Nonempty}) '' v).Finite
ht₂ :
  powerset '' u ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' v ⊆
    powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
U : Set α := ⋂₀ u
hU : IsOpen[inst✝] U
hs : s ⊆ U ∧ ∀ i ∈ v, s ∈ {s | (s ∩ i).Nonempty}
⊢ (((fun x ↦ U ∩ x) '' v).Finite ∧ ∀ U_1 ∈ insert U ((fun x ↦ U ∩ x) '' v), IsOpen[inst✝] U_1) ∧
    (s ⊆ U ∧ ∀ U_1 ∈ insert U ((fun x ↦ U ∩ x) '' v), (s ∩ U_1).Nonempty) ∧
      {s | s ⊆ U ∧ ∀ U_1 ∈ insert U ((fun x ↦ U ∩ x) '' v), (s ∩ U_1).Nonempty} ⊆ 𝒫 U ∩ ⋂ a ∈ v, {s | (s ∩ a).Nonempty}

Tactic:
forall_mem_insert,

Goal state after:
case refine_2.inr
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h✝ : s.Nonempty
u : Set (Set α)
hu₁ : u ⊆ {U | IsOpen[inst✝] U}
hu₂ : u.Finite
hu : powerset '' u ⊆ powerset '' {U | IsOpen[inst✝] U}
v : Set (Set α)
hv₁ : v ⊆ {U | IsOpen[inst✝] U}
hv₂ : v.Finite
hv : (fun V ↦ {s | (s ∩ V).Nonempty}) '' v ⊆ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {U | IsOpen[inst✝] U}
ht₁ : (powerset '' u).Finite ∧ ((fun V ↦ {s | (s ∩ V).Nonempty}) '' v).Finite
ht₂ :
  powerset '' u ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' v ⊆
    powerset '' {U | IsOpen[inst✝] U} ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' {V | IsOpen[inst✝] V}
U : Set α := ⋂₀ u
hU : IsOpen[inst✝] U
hs : s ⊆ U ∧ ∀ i ∈ v, s ∈ {s | (s ∩ i).Nonempty}
⊢ (((fun x ↦ U ∩ x) '' v).Finite ∧ IsOpen[inst✝] U ∧ ∀ x ∈ (fun x ↦ U ∩ x) '' v, IsOpen[inst✝] x) ∧
    (s ⊆ U ∧ (s ∩ U).Nonempty ∧ ∀ x ∈ (fun x ↦ U ∩ x) '' v, (s ∩ x).Nonempty) ∧
      {s | s ⊆ U ∧ (s ∩ U).Nonempty ∧ ∀ x ∈ (fun x ↦ U ∩ x) '' v, (s ∩ x).Nonempty} ⊆
        𝒫 U ∩ ⋂ a ∈ v, {s | (s ∩ a).Nonempty}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ IsTopologicalBasis
    ((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})

Tactic:
by
  refine isTopologicalBasis.isTopologicalBasis_of_exists_subset ?_ ?_ <;>
    rw [forall_mem_image]
  · intro ⟨V, u⟩ ⟨hV, hu, huB, _⟩
    simp_rw [ofPred_and, ofPred_forall]
    exact hV.powerset_vietoris.inter <|
      hu.isOpen_biInter fun V hV => isOpen_inter_nonempty_of_isOpen <| hB.isOpen <| huB hV
  · intro u ⟨hu₁, hu₂⟩ s ⟨hs₁, hs₂⟩
    choose! f hfB hfU hfs using show ∀ U ∈ u, ∃ W ∈ B, W ⊆ U ∧ (s ∩ W).Nonempty by
      intro U hU
      obtain ⟨x, hxs, hxU⟩ := hs₂ U hU
      obtain ⟨W, hWB, hxW, hW⟩ := hB.exists_subset_of_mem_open hxU <| hu₂ U hU
      exact ⟨W, hWB, hW, x, hxs, hxW⟩
    rw [exists_mem_image]
    refine ⟨⟨⋃₀ u, f '' u⟩, ⟨isOpen_sUnion hu₂, hu₁.image _, by grind⟩, by grind,
      fun t ⟨ht₁, ht₂⟩ => ⟨ht₁, fun U hU => ?_⟩⟩
    rw [forall_mem_image] at ht₂
    grw [← hfU U hU]
    exact ht₂ hU

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
s t : Set α
inst✝ : T1Space α
⊢ (∀ x ∈ s, x ∈ t ∧ True) ∧ t ⊆ closure[inst✝¹] s ↔ s ⊆ t ∧ t ⊆ closure[inst✝¹] s

Tactic:
and_true,

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
s t : Set α
inst✝ : T1Space α
⊢ (∀ x ∈ s, x ∈ t) ∧ t ⊆ closure[inst✝¹] s ↔ s ⊆ t ∧ t ⊆ closure[inst✝¹] s
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
⊢ IsPreconnected (⋃₀ s)

Tactic:
have hts' := subset_sUnion_of_mem hts

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
⊢ IsPreconnected (⋃₀ s)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

Goal state before:
pp: case right.right
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
⊢ cfcₙ (fun x ↦ √x * √x) a = a

Tactic:
← cfcₙ_id ℝ a

Goal state after:
case right.right
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
⊢ cfcₙ (fun x ↦ √x * √x) a = cfcₙ id a
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
f : ℝ → ℝ
a : A
hf_nonneg : ∀ x ∈ σₙ ℝ a, 0 ≤ f x
ha : 0 ≤ a
⊢ cfcₙ f a = cfcₙ (fun x ↦ (f ↑x).toNNReal) a

Tactic:
cfcₙ_nnreal_eq_real ..

Goal state after:
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
f : ℝ → ℝ
a : A
hf_nonneg : ∀ x ∈ σₙ ℝ a, 0 ≤ f x
ha : 0 ≤ a
⊢ cfcₙ f a = cfcₙ (fun x ↦ ↑(f ↑x.toNNReal).toNNReal) a
Module: Mathlib.Analysis.Complex.Convex

Goal state before:
pp: r : ℝ
⊢ {0}ᶜ = {c | 0 < c.im} ∪ {c | 0 < c.re} ∪ ({c | c.im < 0} ∪ {c | c.re < 0})

Tactic:
ext x

Goal state after:
r : ℝ
x : ℂ
⊢ x ∈ {0}ᶜ ↔ x ∈ {c | 0 < c.im} ∪ {c | 0 < c.re} ∪ ({c | c.im < 0} ∪ {c | c.re < 0})
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
this : NormedAlgebra ℚ A
⊢ z = ↑z.re

Tactic:
have hu := exp_mem_unitary_of_mem_skewAdjoint (ha.smul_mem_skewAdjoint conj_I)

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
this : NormedAlgebra ℚ A
hu : NormedSpace.exp (I • a) ∈ unitary A
⊢ z = ↑z.re
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
ha : 0 ≤ a
⊢ IsGreatest (f '' σₙ ℝ≥0 a) ‖cfcₙ f a‖₊

Tactic:
cfcₙ_nnreal_eq_real ..

Goal state after:
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
ha : 0 ≤ a
⊢ IsGreatest (f '' σₙ ℝ≥0 a) ‖cfcₙ (fun x ↦ ↑(f x.toNNReal)) a‖₊
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case refine_1
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f : ℝ≥0 → ℝ≥0
a : A
c : ℝ≥0
h : ∀ x ∈ σₙ ℝ≥0 a, f x < c
⊢ ‖0‖₊ < c

Tactic:
simpa using (h 0 (quasispectrum.zero_mem ℝ≥0 _)).pos

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
⊢ {a | a ≠ ⊥} ∩ {a | ↑a ⊆ s} ⊆ closure ({a | a ≠ ⊥} ∩ {a | (↑a).Finite ∧ ↑a ⊆ s})

Tactic:
← compl_singleton_eq

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
⊢ {⊥}ᶜ ∩ {a | ↑a ⊆ s} ⊆ closure ({⊥}ᶜ ∩ {a | (↑a).Finite ∧ ↑a ⊆ s})
Module: Mathlib.Topology.ContinuousMap.ZeroAtInfty

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : Zero β
f g : α →C₀ β
h : f.toBCF = g.toBCF
⊢ f = g

Tactic:
ext x

Goal state after:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : Zero β
f g : α →C₀ β
h : f.toBCF = g.toBCF
x : α
⊢ f x = g x
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 '' {F | F.Finite ∧ F ⊆ s}) = B.polar s

Tactic:
ext x

Goal state after:
𝕜 : 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
x : F
⊢ x ∈ ⋂₀ (B.polar '' {F | F.Finite ∧ F ⊆ s}) ↔ x ∈ B.polar s
Module: Mathlib.Analysis.LocallyConvex.AbsConvex

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x ↦ r • x) y ∈ balancedHull ℝ s
this✝ : 0 ≤ 1 + r
this : 0 ≤ 1 - r
⊢ ((1 + r) / 2) • y + -(((1 - r) / 2) • y) = (fun x ↦ r • x) y

Tactic:
← sub_eq_add_neg,

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x ↦ r • x) y ∈ balancedHull ℝ s
this✝ : 0 ≤ 1 + r
this : 0 ≤ 1 - r
⊢ ((1 + r) / 2) • y - ((1 - r) / 2) • y = (fun x ↦ r • x) y
Module: Mathlib.Analysis.LocallyConvex.HahnBanach

Goal state before:
pp: case h
𝕜 : Type u_1
E : Type u_2
inst✝¹² : AddCommGroup E
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : IsRCLikeNormedField 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : PolynormableSpace 𝕜 E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : Module 𝕜 F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : T2Space F
S : Submodule 𝕜 E
f : ↥S →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(↑f).range
this : RCLike 𝕜 := ⋯
b : Basis (Fin (finrank 𝕜 ↥(↑f).range)) 𝕜 ↥(↑f).range := ⋯
e : ↥(↑f).range ≃L[𝕜] Fin (finrank 𝕜 ↥(↑f).range) → 𝕜 := ⋯
fi : Fin (finrank 𝕜 ↥(↑f).range) → ↥S →L[𝕜] 𝕜 := ⋯
gi : Fin (finrank 𝕜 ↥(↑f).range) → StrongDual 𝕜 E
hgf : ∀ (i : Fin (finrank 𝕜 ↥(↑f).range)) (x : ↥S), (gi i) ↑x = (fi i) x
⊢ f = ((↑f).range.subtypeL ∘SL ↑e.symm ∘SL pi gi) ∘SL S.subtypeL

Tactic:
ext x

Goal state after:
case h
𝕜 : Type u_1
E : Type u_2
inst✝¹² : AddCommGroup E
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : IsRCLikeNormedField 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : PolynormableSpace 𝕜 E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : Module 𝕜 F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : T2Space F
S : Submodule 𝕜 E
f : ↥S →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 ↥(↑f).range
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
b : Basis (Fin (finrank 𝕜 ↥(↑f).range)) 𝕜 ↥(↑f).range := finBasis 𝕜 ↥(↑f).range
e : ↥(↑f).range ≃L[𝕜] Fin (finrank 𝕜 ↥(↑f).range) → 𝕜 := b.equivFunL
fi : Fin (finrank 𝕜 ↥(↑f).range) → ↥S →L[𝕜] 𝕜 :=
  fun i ↦ LinearMap.toContinuousLinearMap (b.coord i) ∘SL f.codRestrict (↑f).range ⋯
gi : Fin (finrank 𝕜 ↥(↑f).range) → StrongDual 𝕜 E
hgf : ∀ (i : Fin (finrank 𝕜 ↥(↑f).range)) (x : ↥S), (gi i) ↑x = (fi i) x
x : ↥S
⊢ f x = (((↑f).range.subtypeL ∘SL ↑e.symm ∘SL pi gi) ∘SL S.subtypeL) x
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
x' : StrongDual 𝕜 E
c : 𝕜
hc : ∀ z ∈ s, ‖x' z‖ ≤ ‖c‖
⊢ c⁻¹ • x' ∈ polar 𝕜 s

Tactic:
by_cases c_zero : c = 0
  · simp only [c_zero, inv_zero, zero_smul]
    exact (topDualPairing 𝕜 E).flip.zero_mem_polar _
  have eq : ∀ z, ‖c⁻¹ • x' z‖ = ‖c⁻¹‖ * ‖x' z‖ := fun z => norm_smul c⁻¹ _
  have le : ∀ z, z ∈ s → ‖c⁻¹ • x' z‖ ≤ ‖c⁻¹‖ * ‖c‖ := by
    intro z hzs
    rw [eq z]
    apply mul_le_mul (le_of_eq rfl) (hc z hzs) (norm_nonneg _) (norm_nonneg _)
  have cancel : ‖c⁻¹‖ * ‖c‖ = 1 := by
    simp only [c_zero, norm_eq_zero, Ne, not_false_iff, inv_mul_cancel₀, norm_inv]
  rwa [cancel] at le

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

Goal state before:
pp: X : Type u_1
R : Type u_3
𝕜 : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedField 𝕜
inst✝² : NormedDivisionRing R
inst✝¹ : Algebra 𝕜 R
inst✝ : CompleteSpace R
f : C(X, R)
⊢ spectrum 𝕜 f = ⇑(algebraMap 𝕜 R) ⁻¹' Set.range ⇑f

Tactic:
ext x

Goal state after:
X : Type u_1
R : Type u_3
𝕜 : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedField 𝕜
inst✝² : NormedDivisionRing R
inst✝¹ : Algebra 𝕜 R
inst✝ : CompleteSpace R
f : C(X, R)
x : 𝕜
⊢ x ∈ spectrum 𝕜 f ↔ x ∈ ⇑(algebraMap 𝕜 R) ⁻¹' Set.range ⇑f
Module: Mathlib.Analysis.Normed.Affine.AddTorsor

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : Invertible 2
p₁ p₂ : P
⊢ dist (midpoint 𝕜 p₁ p₂) p₁ = ‖2‖⁻¹ * dist p₁ p₂

Tactic:
rw [dist_comm, dist_left_midpoint]

Goal state after:
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
a : A
ha : IsSelfAdjoint a
| a

Tactic:
← cfcₙ_id ℝ 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
a : A
ha : IsSelfAdjoint a
| cfcₙ id a
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 : 0 ≤ a
| a

Tactic:
← cfcₙ_id ℝ 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 : 0 ≤ a
| cfcₙ id a
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 : 0 ≤ -a
x✝ : IsSelfAdjoint a
| a

Tactic:
← cfcₙ_id ℝ 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 : 0 ≤ -a
x✝ : IsSelfAdjoint a
| cfcₙ id a
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:
by
  refine ⟨fun φ ψ h => starAlgHomClass_ext ℂ ?_ ?_ ?_, ?_⟩
  · exact (map_continuous φ)
  · exact (map_continuous ψ)
  · simpa only [characterSpaceToSpectrum, Subtype.mk_eq_mk,
      ContinuousMap.coe_mk] using h
  · rintro ⟨z, hz⟩
    have hz' := (StarSubalgebra.spectrum_eq (hS := isClosed ℂ a)
      (a := ⟨a, self_mem ℂ a⟩) ▸ hz)
    rw [CharacterSpace.mem_spectrum_iff_exists] at hz'
    obtain ⟨φ, rfl⟩ := hz'
    exact ⟨φ, rfl⟩

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℝ a ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ SpectrumRestricts ((algebraMap ℝ A) ↑t - a) ⇑Complex.reCLM

Tactic:
apply IsSelfAdjoint.spectrumRestricts

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℝ a ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℂ a ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ SpectrumRestricts a ⇑Complex.reCLM

Tactic:
apply IsSelfAdjoint.spectrumRestricts

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℂ a ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ IsSelfAdjoint a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℂ a ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)

Tactic:
apply IsSelfAdjoint.spectrumRestricts

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℂ a ≤ ↑t
this : IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)
⊢ IsSelfAdjoint ((algebraMap ℝ A) ↑t - a)