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 : 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}
hs : s ∈ ⋂₀ (powerset '' u ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' v)
⊢ ∃ x ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U},
    s ∈ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ∧
      {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ⊆ ⋂₀ (powerset '' u ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' v)

Tactic:
let U := ⋂₀ u

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}
hs : s ∈ ⋂₀ (powerset '' u ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' v)
U : Set α := ⋂₀ u
⊢ ∃ x ∈ {u | u.Finite ∧ ∀ U ∈ u, IsOpen[inst✝] U},
    s ∈ {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ∧
      {s | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty} ⊆ ⋂₀ (powerset '' u ∪ (fun V ↦ {s | (s ∩ V).Nonempty}) '' v)
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case right
α : Type u_1
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x✝¹ : Set α × Set α
s t : Set α
x✝ :
  (s, t) ∈
    (fun x ↦ (closure[inst✝.toTopologicalSpace] x.1, closure[inst✝.toTopologicalSpace] x.2)) ⁻¹' hausdorffEntourage V
hst : closure[inst✝.toTopologicalSpace] s ⊆ V.preimage (closure[inst✝.toTopologicalSpace] t)
hts : closure[inst✝.toTopologicalSpace] t ⊆ V.image (closure[inst✝.toTopologicalSpace] s)
⊢ t ⊆ SetRel.image U s

Tactic:
grw [subset_closure (s := t), hts, closure_subset_image hV s, ← hVU, SetRel.image_comp]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace α
f : Filter (Compacts α)
x✝ : Cauchy f
left✝¹ : f.NeBot
hf : ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
l : Filter α := f.lift' fun s ↦ ⋃ K ∈ s, ↑K
U : SetRel α α
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : ↑K ⊆ V.preimage t
K' : Compacts α
left✝ : (↑K, ↑K').1 ⊆ SetRel.preimage (Prod.swap ⁻¹' V) (↑K, ↑K').2
hK' : ↑K' ⊆ V.preimage ↑K
⊢ ↑K' ⊆ (V.comp V).preimage t

Tactic:
SetRel.preimage_comp,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace α
f : Filter (Compacts α)
x✝ : Cauchy f
left✝¹ : f.NeBot
hf : ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage U
l : Filter α := f.lift' fun s ↦ ⋃ K ∈ s, ↑K
U : SetRel α α
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, (↑K, ↑K') ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : ↑K ⊆ V.preimage t
K' : Compacts α
left✝ : (↑K, ↑K').1 ⊆ SetRel.preimage (Prod.swap ⁻¹' V) (↑K, ↑K').2
hK' : ↑K' ⊆ V.preimage ↑K
⊢ ↑K' ⊆ V.preimage (V.preimage t)
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : IsPreconnected s
t : Set α
hts : t ∈ s
ht : IsPreconnected t
hts' : t ⊆ ⋃₀ s
U : Set α
⊢ ∀ (v : Set α),
    IsOpen[inst✝] U →
      IsOpen[inst✝] v → ⋃₀ s ⊆ U ∪ v → (⋃₀ s ∩ U).Nonempty → (⋃₀ s ∩ v).Nonempty → (⋃₀ s ∩ (U ∩ v)).Nonempty

Tactic:
V

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : IsPreconnected s
t : Set α
hts : t ∈ s
ht : IsPreconnected t
hts' : t ⊆ ⋃₀ s
U V : Set α
⊢ IsOpen[inst✝] U →
    IsOpen[inst✝] V → ⋃₀ s ⊆ U ∪ V → (⋃₀ s ∩ U).Nonempty → (⋃₀ s ∩ V).Nonempty → (⋃₀ s ∩ (U ∩ V)).Nonempty
Module: Mathlib.Topology.Sets.VietorisTopology

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

Tactic:
apply hvV.mono

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

Goal state before:
pp: case neg
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
z : 𝕜
hz : z ∈ σ 𝕜 x
hz' : z ∉ σ 𝕜 ↑x
this : CompleteSpace ↥S
⊢ connectedComponentIn (σ 𝕜 ↑x)ᶜ z ⊆ σ 𝕜 x

Tactic:
spectrum_sUnion_connectedComponentIn S

Goal state after:
case neg
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
z : 𝕜
hz : z ∈ σ 𝕜 x
hz' : z ∉ σ 𝕜 ↑x
this : CompleteSpace ↥S
⊢ connectedComponentIn (σ 𝕜 ↑x)ᶜ z ⊆ σ 𝕜 ↑x ∪ ⋃ z ∈ σ 𝕜 x \ σ 𝕜 ↑x, connectedComponentIn (σ 𝕜 ↑x)ᶜ z
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²⁵ : Semifield R
inst✝²⁴ : StarRing R
inst✝²³ : MetricSpace R
inst✝²² : IsTopologicalSemiring R
inst✝²¹ : ContinuousStar R
inst✝²⁰ : Field S
inst✝¹⁹ : StarRing S
inst✝¹⁸ : MetricSpace S
inst✝¹⁷ : IsTopologicalRing S
inst✝¹⁶ : ContinuousStar S
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : StarRing A
inst✝¹³ : Module S A
inst✝¹² : IsScalarTower S A A
inst✝¹¹ : SMulCommClass S A A
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module R A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : StarModule R S
inst✝⁶ : ContinuousSMul R S
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : MetricSpace A
inst✝² : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
ha' : q a
haf : QuasispectrumRestricts a ⇑f
this : NonUnitalContinuousFunctionalCalculus R A p
g₁ g₂ : ContinuousMapZero (↑(σₙ R a)) R
x : ↑(σₙ R a)
⊢ dist (↑g₁ x) (↑g₂ x) ≤
    dist
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
        (g₁.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ }))
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
        (g₂.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ }))

Tactic:
let x' : σₙ S a := Subtype.map (algebraMap R S) (fun _ ↦ quasispectrum.algebraMap_mem S) x
      apply le_of_eq_of_le ?_ <| ContinuousMap.dist_apply_le_dist x'
      simp only [ContinuousMapZero.comp_apply, ContinuousMapZero.coe_mk,
        ContinuousMap.coe_mk, StarAlgHom.ofId_apply, halg.dist_eq, x']
      congr! 2
      all_goals ext; exact haf.left_inv _ |>.symm

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

Goal state before:
pp: A : Type u_1
inst✝⁷ : NormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : Nontrivial A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
⊢ IsGreatest (f '' σ ℝ≥0 a) ‖cfc f a‖₊

Tactic:
by
  rw [cfc_nnreal_eq_real ..]
  obtain ⟨-, ha'⟩ := nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts.mp ha
  rw [← SpectrumRestricts] at ha'
  convert! IsGreatest.nnnorm_cfc (fun x : ℝ ↦ (f x.toNNReal : ℝ)) a ?hf_cont
  case hf_cont => exact continuous_subtype_val.comp_continuousOn <|
    ContinuousOn.comp ‹_› continuous_real_toNNReal.continuousOn <| ha'.image ▸ Set.mapsTo_image ..
  simp [Set.image_image, ← ha'.image]

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

Goal state before:
pp: case e_u
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun n ↦ ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
h : ↑r ≤ p.radius
n : ℕ
⊢ (1 / if ‖a ^ n‖₊ = 0 ∧ 1 / ↑n < 0 then ∞ else ↑(‖a ^ n‖₊ ^ (1 / ↑n))) = 1 / ↑(‖a ^ n‖₊ ^ (1 / ↑n))

Tactic:
if_neg

Goal state after:
case e_u
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun n ↦ ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
h : ↑r ≤ p.radius
n : ℕ
⊢ 1 / ↑(‖a ^ n‖₊ ^ (1 / ↑n)) = 1 / ↑(‖a ^ n‖₊ ^ (1 / ↑n))

case e_u.hnc
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
r_pos : 0 < r
r_lt : ↑r < (spectralRadius ℂ a)⁻¹
p : FormalMultilinearSeries ℂ ℂ A := fun n ↦ ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
h : ↑r ≤ p.radius
n : ℕ
⊢ ¬(‖a ^ n‖₊ = 0 ∧ 1 / ↑n < 0)
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 : α → β
inst✝ : LocallyCompactSpace α
K : Compacts α
U : Set (Compacts α)
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝³] U
huU : {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty} ⊆ U
hKu₁ : ↑K ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, (↑K ∩ U).Nonempty
⊢ ∃ s ∈ 𝓝 K, s ⊆ U ∧ IsCompact s

Tactic:
grw [← huU]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyCompactSpace α
K : Compacts α
U : Set (Compacts α)
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝³] U
huU : {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty} ⊆ U
hKu₁ : ↑K ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, (↑K ∩ U).Nonempty
⊢ ∃ s ∈ 𝓝 K, s ⊆ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty} ∧ IsCompact s
Module: Mathlib.Analysis.LocallyConvex.WeakDual

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
f : F →ₗ[𝕜] 𝕜
g : E →ₗ[𝕜] F
⊢ f.toSeminorm.comp g = (f ∘ₗ g).toSeminorm

Tactic:
ext
  simp only [Seminorm.comp_apply, toSeminorm_apply, coe_comp, Function.comp_apply]

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
n : ℕ
x : X
hx : x ∈ c.C
⊢ approx n c x = 0

Tactic:
by
  induction n generalizing c with
  | zero => exact indicator_of_notMem (fun (hU : x ∈ c.Uᶜ) => hU <| c.subset hx) _
  | succ n ihn =>
    simp only [approx]
    rw [ihn, ihn, midpoint_self]
    exacts [c.subset_right_C hx, hx]

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∉ c.left.U
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ (n + 1)

Tactic:
replace hxl : x ∈ c.left.right.Cᶜ :=
        compl_subset_compl.2 c.left.right.subset hxl

Goal state after:
case neg
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∈ c.left.right.Cᶜ
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ (n + 1)
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:
Quotient.eq_zero_iff_mem.mpr ha,

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.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: case refine_3
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⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x ↦ ContinuousMap.realToNNReal x
⊢ SpectrumRestricts (2 • (↑(ℜ c) ^ 2 + ↑(ℑ c) ^ 2)) ⇑ContinuousMap.realToNNReal

Tactic:
· rw [← Nat.cast_smul_eq_nsmul ℝ]
      refine (ℜ c).2.sq_spectrumRestricts.nnreal_add ((ℜ c).2.pow 2) ((ℑ c).2.pow 2)
        (ℑ c).2.sq_spectrumRestricts |>.smul_of_nonneg <| by simp

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

Goal state before:
pp: case neg.inl
A : Type u_1
inst✝¹³ : NonUnitalCStarAlgebra A
R : Type u_2
inst✝¹² : Semifield R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : Algebra R ℂ
inst✝³ : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R A p
inst✝¹ : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst✝ : ContinuousMapZero.UniqueHom R (Unitization ℂ A)
hp : ∀ {a : A}, p' ↑a ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
h : ¬(ContinuousOn f (σₙ R a) ∧ p a)
hf : ¬ContinuousOn f (σₙ R a)
⊢ ↑(cfcₙ f a) = cfc f ↑a

Tactic:
rw [cfcₙ_apply_of_not_continuousOn a hf, inr_zero,
        cfc_apply_of_not_continuousOn _ (quasispectrum_eq_spectrum_inr' R ℂ a ▸ hf)]

Goal state after:
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
a : A
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
a✝ : Nontrivial A
h : IsUnit (cfc (fun x ↦ x ^ y) a)
hf : ContinuousOn (fun x ↦ x ^ y) (spectrum ℝ≥0 a)
⊢ IsUnit a

pp: case neg
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
a : A
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
a✝ : Nontrivial A
h : IsUnit (cfc (fun x ↦ x ^ y) a)
hf : ¬ContinuousOn (fun x ↦ x ^ y) (spectrum ℝ≥0 a)
⊢ IsUnit a

Tactic:
· rw [isUnit_cfc_iff _ a hf] at h
    refine spectrum.isUnit_of_zero_notMem ℝ≥0 ?_
    intro h0
    specialize h 0 h0
    simp only [ne_eq, NNReal.rpow_eq_zero_iff, true_and, Decidable.not_not] at h
    exact hy h

Goal state after:
case neg
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
a : A
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
a✝ : Nontrivial A
h : IsUnit (cfc (fun x ↦ x ^ y) a)
hf : ¬ContinuousOn (fun x ↦ x ^ y) (spectrum ℝ≥0 a)
⊢ IsUnit a
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 : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y

Tactic:
b

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 : ℝ
⊢ 0 ≤ a → 0 ≤ b → 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 : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)

Tactic:
b

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 : ℝ
⊢ 0 ≤ a → 0 ≤ b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)
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
a : A
ha : IsUnit a
⊢ 0 ≤ a⁻¹ʳ ↔ 0 ≤ a

Tactic:
grind [isStrictlyPositive_ringInverse_iff]

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
apos : IsStrictlyPositive a
⊢ ∀ ⦃b : A⦄, b ∈ {a | IsStrictlyPositive a} → a ≤ b → Ring.inverse b ≤ Ring.inverse a

Tactic:
b

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
apos : IsStrictlyPositive a
b : A
⊢ b ∈ {a | IsStrictlyPositive a} → a ≤ b → Ring.inverse b ≤ Ring.inverse a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b : A
ha : 0 ≤ a✝
hab : a✝ ≤ b
a : Unitization ℂ A
⊢ ∀ (b : Unitization ℂ A), 0 ≤ a → a ≤ b → ‖a‖ ≤ ‖b‖

Tactic:
b

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b✝ : A
ha : 0 ≤ a✝
hab : a✝ ≤ b✝
a b : Unitization ℂ A
⊢ 0 ≤ a → a ≤ b → ‖a‖ ≤ ‖b‖
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b : A
hb : IsSelfAdjoint b
a : Unitization ℂ A
⊢ ∀ (b : Unitization ℂ A), IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a)

Tactic:
b

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b✝ : A
hb : IsSelfAdjoint b✝
a b : Unitization ℂ A
⊢ IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a)
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : a ∈ Set.Ici 0
⊢ ∀ ⦃b : A⦄, b ∈ Set.Ici 0 → a ≤ b → cfcₙ (fun x ↦ 1 - (1 + x)⁻¹) a ≤ cfcₙ (fun x ↦ 1 - (1 + x)⁻¹) b

Tactic:
b

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : a ∈ Set.Ici 0
b : A
⊢ b ∈ Set.Ici 0 → a ≤ b → cfcₙ (fun x ↦ 1 - (1 + x)⁻¹) a ≤ cfcₙ (fun x ↦ 1 - (1 + x)⁻¹) b
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
⊢ ∀ ⦃b : A⦄, b ∈ Set.Ici 0 → a ≤ b → cfcₙ (fun x ↦ 1 - (1 + x)⁻¹) a ≤ cfcₙ (fun x ↦ 1 - (1 + x)⁻¹) b

Tactic:
b

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : A
⊢ b ∈ Set.Ici 0 → a ≤ b → cfcₙ (fun x ↦ 1 - (1 + x)⁻¹) a ≤ cfcₙ (fun x ↦ 1 - (1 + x)⁻¹) b
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: R : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : Nontrivial R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : MetricSpace A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus R A p
a : A
s : Set R
hs : quasispectrum R a ⊆ s
h₂ : LipschitzWith 1 (⇑(ofFun {quasispectrum R a}) ∘ ⇑(toFun {s}))
⊢ LipschitzOnWith 1 (fun f ↦ cfcₙ ((toFun {s}) f) a) {f | ContinuousOn ((toFun {s}) f) s ∧ f 0 = 0}

Tactic:
have h₃ := h₂.lipschitzOnWith (s := {f | ContinuousOn (toFun {s} f) (s) ∧ f 0 = 0})

Goal state after:
R : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : Nontrivial R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : MetricSpace A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus R A p
a : A
s : Set R
hs : quasispectrum R a ⊆ s
h₂ : LipschitzWith 1 (⇑(ofFun {quasispectrum R a}) ∘ ⇑(toFun {s}))
h₃ : LipschitzOnWith 1 (⇑(ofFun {quasispectrum R a}) ∘ ⇑(toFun {s})) {f | ContinuousOn ((toFun {s}) f) s ∧ f 0 = 0}
⊢ LipschitzOnWith 1 (fun f ↦ cfcₙ ((toFun {s}) f) a) {f | ContinuousOn ((toFun {s}) f) s ∧ f 0 = 0}
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: case e_f.refine_1
m : Type u_3
α : Type u_5
inst✝² : Fintype m
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
i j : m
_hj : j ∈ Finset.univ
hij : j ≠ i
⊢ ‖diagonal v i j‖₊ = 0

Tactic:
diagonal_apply_ne' _ hij,

Goal state after:
case e_f.refine_1
m : Type u_3
α : Type u_5
inst✝² : Fintype m
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
i j : m
_hj : j ∈ Finset.univ
hij : j ≠ i
⊢ ‖0‖₊ = 0
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝ m : A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
ε : ℝ≥0
hε : 0 < ε
x : A
hx₁ : ↑(cfcₙ (fun y ↦ 1 - (1 + y)⁻¹) (ε⁻¹ ^ 2 • m)) ≤ ↑x
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
⊢ 1 - (1 + 0)⁻¹ = 0

Tactic:
by simp [tsub_self]

Goal state after: