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

Goal state before:
pp: case inr.hwK
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst✝] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, (↑K ∩ U).Nonempty
w : Set (Set α)
hKV : ↑K ⊆ ⋃ i ∈ w, i
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, (↑K ∩ W).Nonempty
this :
  ∀ (w : Set (Set α)),
    ↑K ⊆ ⋃₀ w →
      w ⊆ B →
        ⋃₀ w ⊆ V →
          (∀ W ∈ w, (↑K ∩ W).Nonempty) →
            w.Finite →
              ∃ v ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B},
                K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
hw : ¬w.Finite
w' : Set (Set α)
h✝ : w' ⊆ w ∧ w'.Finite ∧ ↑K ⊆ ⋃ i ∈ w', i
⊢ ∀ W ∈ w', (↑K ∩ W).Nonempty

Tactic:
grind [sUnion_eq_biUnion]

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

Goal state before:
pp: case inr.hw
α : Type u_1
inst✝ : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst✝] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, (↑K ∩ U).Nonempty
w : Set (Set α)
hKV : ↑K ⊆ ⋃ i ∈ w, i
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, (↑K ∩ W).Nonempty
this :
  ∀ (w : Set (Set α)),
    ↑K ⊆ ⋃₀ w →
      w ⊆ B →
        ⋃₀ w ⊆ V →
          (∀ W ∈ w, (↑K ∩ W).Nonempty) →
            w.Finite →
              ∃ v ∈ (fun u ↦ {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B},
                K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
hw : ¬w.Finite
w' : Set (Set α)
h✝ : w' ⊆ w ∧ w'.Finite ∧ ↑K ⊆ ⋃ i ∈ w', i
⊢ w'.Finite

Tactic:
grind [sUnion_eq_biUnion]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CStarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : ↥(unitary E)
⊢ σ 𝕜 ↑u ⊆ Metric.sphere 0 1

Tactic:
nontriviality E

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CStarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : ↥(unitary E)
a✝ : Nontrivial E
⊢ σ 𝕜 ↑u ⊆ Metric.sphere 0 1
Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula

Goal state before:
pp: A : Type u_2
inst✝³ : NormedRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
inst✝ : Nontrivial A
a : A
h : spectrum ℂ a = ∅
⊢ False

Tactic:
have H₀ : resolventSet ℂ a = Set.univ := by rwa [spectrum, Set.compl_empty_iff] at h

Goal state after:
A : Type u_2
inst✝³ : NormedRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
inst✝ : Nontrivial A
a : A
h : spectrum ℂ a = ∅
H₀ : resolventSet ℂ a = Set.univ
⊢ False
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✝ : SecondCountableTopology α
⊢ SecondCountableTopology (Compacts α)

Tactic:
by
  obtain ⟨b, hb₁, -, hb₂⟩ := exists_countable_basis α
  exact hb₂.compacts.secondCountableTopology <| (countable_ofPred_finite_subset hb₁).image _

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : AddCommMonoid E
inst✝ : PartialOrder 𝕜
s : Set E
⊢ ((absConvexHull 𝕜) s).Nonempty ↔ s.Nonempty

Tactic:
by
  rw [nonempty_iff_ne_empty, nonempty_iff_ne_empty, Ne, Ne]
  exact not_congr absConvexHull_eq_empty

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ IsClosed {⊥}ᶜ

Tactic:
exact Compacts.isClopen_singleton_bot.compl.isClosed

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : ContinuousSMul ℝ E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
⊢ 0 ∈ ⋂ i ∈ t, (gaugeSeminormFamily 𝕜 E i).ball 0 r ∧
    IsOpen[inst✝⁷] (⋂ i ∈ t, (gaugeSeminormFamily 𝕜 E i).ball 0 r) ∧
      AbsConvex 𝕜 (⋂ i ∈ t, (gaugeSeminormFamily 𝕜 E i).ball 0 r)

Tactic:
refine
    ⟨mem_iInter₂.mpr fun _ _ => by simp [hr],
      isOpen_biInter_finset fun S _ => ?_,
      balanced_iInter₂ fun _ _ => Seminorm.balanced_ball_zero _ _,
      convex_iInter₂ fun _ _ => (convex_of_nonneg_surjective_algebraMap _
        (fun _ => RCLike.nonneg_iff_exists_ofReal.mp) (Seminorm.convex_ball _ _ _) ..)⟩

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : ContinuousSMul ℝ E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
S : AbsConvexOpenSets 𝕜 E
x✝ : S ∈ t
⊢ IsOpen[inst✝⁷] ((gaugeSeminormFamily 𝕜 E S).ball 0 r)
Module: Mathlib.Analysis.Normed.Module.HahnBanach

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : StrongDual 𝕜 ↥p
⊢ Continuous ⇑(‖f‖₊ • normSeminorm 𝕜 E)

Tactic:
exact continuous_norm.const_smul ‖f‖₊

Goal state after:
Module: Mathlib.Analysis.Normed.Module.HahnBanach

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : StrongDual 𝕜 ↥p
g : StrongDual 𝕜 E
hg : ∀ (x : ↥p), g ↑x = ↑f x
hl : ∀ (x : E), ‖g x‖ ≤ (‖f‖₊ • normSeminorm 𝕜 E) x
x : ↥p
⊢ ‖f x‖ ≤ ‖g‖ * ‖x‖

Tactic:
by simpa [hg x] using g.le_opNorm x

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Extend

Goal state before:
pp: 𝕜✝ : Type u_1
E : Type u_2
F✝ : Type u_3
inst✝⁷ : RCLike 𝕜✝
𝕜 : Type u_4
F : Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 F
inst✝² : ContinuousSMul 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
⊢ Continuous (↑extendRCLikeₗ).toFun

Tactic:
rw [(ContinuousLinearMap.isEmbedding_restrictScalars ℝ).continuous_iff]
    let smulI : F →L[ℝ] F := (I : 𝕜) • ContinuousLinearMap.id 𝕜 F |>.restrictScalars ℝ
    let mulI : 𝕜 →L[ℝ] 𝕜 := ContinuousLinearMap.mul ℝ 𝕜 (I : 𝕜)
    exact ofRealCLM.postcomp F - mulI.postcomp F ∘L smulI.precomp 𝕜 ∘L ofRealCLM.postcomp F
      |>.continuous

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ⇑p
h₁ : ∀ (n : ℕ), IsClosed[inst✝³] (p.closedBall 0 ↑n)
h₂ : ⋃ n, p.closedBall 0 ↑n = univ
n : ℕ
x : E
hxn : x ∈ interior {y | p y ≤ ↑n}
⊢ {y | p y ≤ ↑n + ↑n} ∈ 𝓝 0

Tactic:
have hxn' : p x ≤ n := by convert! interior_subset hxn

Goal state after:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ⇑p
h₁ : ∀ (n : ℕ), IsClosed[inst✝³] (p.closedBall 0 ↑n)
h₂ : ⋃ n, p.closedBall 0 ↑n = univ
n : ℕ
x : E
hxn : x ∈ interior {y | p y ≤ ↑n}
hxn' : p x ≤ ↑n
⊢ {y | p y ≤ ↑n + ↑n} ∈ 𝓝 0
Module: Mathlib.Analysis.Normed.Affine.AddTorsor

Goal state before:
pp: W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 W
p₁ p₂ : Q
h : p₁ ≠ p₂
c₁ c₂ : 𝕜
⊢ dist c₁ c₂ ≤ ↑(nndist p₁ p₂)⁻¹ * dist ((lineMap p₁ p₂) c₁) ((lineMap p₁ p₂) c₂)

Tactic:
dist_lineMap_lineMap,

Goal state after:
W : Type u_3
Q : Type u_4
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 W
p₁ p₂ : Q
h : p₁ ≠ p₂
c₁ c₂ : 𝕜
⊢ dist c₁ c₂ ≤ ↑(nndist p₁ p₂)⁻¹ * (dist c₁ c₂ * dist p₁ p₂)
Module: Mathlib.Analysis.Normed.Module.WeakDual

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ NormedSpace ?m.32 ?m.33

Tactic:
by assumption

Goal state after:
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:
by simp_all [nnnorm_add_eq_max this]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst✝¹ : PseudoEMetricSpace β
inst✝ : Finite ↑𝔖
x : α
hx : x ∈ ⋃₀ 𝔖
⊢ LipschitzWith 1 fun f ↦ (toFun 𝔖) f x

Tactic:
by
  intro f g
  simpa only [ENNReal.coe_one, one_mul] using edist_eval_le hx

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsStarNormal a
⊢ cfcHom ha = (elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a)

Tactic:
refine cfcHom_eq_of_continuous_of_map_id ha _ ?_ ?_
  · exact continuous_subtype_val.comp <|
      (StarAlgEquiv.isometry (continuousFunctionalCalculus a)).continuous
  · simp [continuousFunctionalCalculus_map_id a]

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
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace ↑s
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
this : Fact (0 ∈ s)
mul₁ : ∀ (f g : C(↑s, ℝ)₀), (cfcₙHomSuperset hb' hbs) f * (cfcₙHomSuperset hc' hcs) g = 0
mul₂ : ∀ (f g : C(↑s, ℝ)₀), (cfcₙHomSuperset hc' hcs) f * (cfcₙHomSuperset hb' hbs) g = 0
ψ : C(↑s, ℝ)₀ →⋆ₙₐ[ℝ] A :=
  let __src := ↑(cfcₙHomSuperset hb' hbs) + ↑(cfcₙHomSuperset hc' hcs);
  { toFun := ⇑(cfcₙHomSuperset hb' hbs) + ⇑(cfcₙHomSuperset hc' hcs), map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
    map_mul' := ⋯, map_star' := ⋯ }
f : C(↑s, ℝ)₀ := { toFun := fun x ↦ (↑x)⁺, continuous_toFun := ⋯, map_zero' := ⋯ }
key :
  cfcₙ
      (Function.extend Subtype.val ⇑(f.comp { toFun := Subtype.map id has, continuous_toFun := ⋯, map_zero' := ⋯ })
        fun x ↦ x⁺)
      a =
    cfcₙ
        (Function.extend Subtype.val ⇑(f.comp { toFun := Subtype.map id hbs, continuous_toFun := ⋯, map_zero' := ⋯ })
          fun x ↦ x⁺)
        b +
      cfcₙ
        (Function.extend Subtype.val ⇑(f.comp { toFun := Subtype.map id hcs, continuous_toFun := ⋯, map_zero' := ⋯ })
          fun x ↦ x⁺)
        (-c)
⊢ cfcₙ
      (Function.extend Subtype.val ⇑(f.comp { toFun := Subtype.map id has, continuous_toFun := ⋯, map_zero' := ⋯ })
        fun x ↦ x⁺)
      a =
    a⁺

Tactic:
by
      refine cfcₙ_congr fun x hx ↦ ?_
      lift x to σₙ ℝ a using hx
      simp [f]

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

Goal state before:
pp: A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
⊢ 1⁻ = 0

Tactic:
rw [CFC.negPart_def, cfcₙ_eq_cfc]

Goal state after:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
⊢ cfc (fun x ↦ x⁻) 1 = 0
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
r : ℝ
⊢ ((algebraMap ℝ A) r)⁻ = (algebraMap ℝ A) r⁻

Tactic:
rw [CFC.negPart_def, cfcₙ_eq_cfc]

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

Goal state before:
pp: case mpr.add
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x✝¹ : PartialOrder A := spectralOrder A
x✝ p x y : A
hx✝ : x ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
hy✝ : y ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
hx : IsSelfAdjoint ↑x ∧ SpectrumRestricts ↑x ⇑ContinuousMap.realToNNReal
hy : IsSelfAdjoint ↑y ∧ SpectrumRestricts ↑y ⇑ContinuousMap.realToNNReal
⊢ IsSelfAdjoint ↑(x + y) ∧ SpectrumRestricts ↑(x + y) ⇑ContinuousMap.realToNNReal

Tactic:
Unitization.inr_add

Goal state after:
case mpr.add
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x✝¹ : PartialOrder A := spectralOrder A
x✝ p x y : A
hx✝ : x ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
hy✝ : y ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
hx : IsSelfAdjoint ↑x ∧ SpectrumRestricts ↑x ⇑ContinuousMap.realToNNReal
hy : IsSelfAdjoint ↑y ∧ SpectrumRestricts ↑y ⇑ContinuousMap.realToNNReal
⊢ IsSelfAdjoint (↑x + ↑y) ∧ SpectrumRestricts (↑x + ↑y) ⇑ContinuousMap.realToNNReal
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : CStarRing A
inst✝⁵ : NormedSpace ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a b : A
hb : IsSelfAdjoint b
ha : 0 ≤ a
⊢ ‖b * a * b‖ = ‖sqrt a * b‖ ^ 2

Tactic:
simpa [hb.star_eq] using norm_star_mul_mul_self_of_nonneg b ha

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart

Goal state before:
pp: case h.right
A : Type u_2
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ a = ∑ i, I ^ ↑i • ![(↑(realPart a))⁺, (↑(imaginaryPart a))⁺, (↑(realPart a))⁻, (↑(imaginaryPart a))⁻] i

Tactic:
nth_rw 1 [← CStarAlgebra.linear_combination_nonneg a]

Goal state after:
case h.right
A : Type u_2
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ (↑(realPart a))⁺ - (↑(realPart a))⁻ + (I • (↑(imaginaryPart a))⁺ - I • (↑(imaginaryPart a))⁻) =
    ∑ i, I ^ ↑i • ![(↑(realPart a))⁺, (↑(imaginaryPart a))⁺, (↑(realPart a))⁻, (↑(imaginaryPart a))⁻] i
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
x : ℝ
⊢ 1 ^ x = 1

Tactic:
by simp [rpow_def]

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

Goal state before:
pp: 𝕜 : 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
s : Set 𝕜
⊢ ContinuousOn (fun fa ↦ cfc ((toFun {s}) fa.1) fa.2)
    ({f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s} ×ˢ {a | p a ∧ s ∈ 𝓝ˢ (spectrum 𝕜 a)})

Tactic:
refine continuousOn_of_locally_continuousOn fun (f, a) ⟨hf, ha, has⟩ ↦ ?_

Goal state after:
𝕜 : 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
s : Set 𝕜
x✝¹ : (𝕜 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] 𝕜) × A
f : 𝕜 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] 𝕜
a : A
x✝ : (f, a) ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s} ×ˢ {a | p a ∧ s ∈ 𝓝ˢ (spectrum 𝕜 a)}
hf : (f, a).1 ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s}
ha : p (f, a).2
has : s ∈ 𝓝ˢ (spectrum 𝕜 (f, a).2)
⊢ ∃ t,
    IsOpen[instTopologicalSpaceProd] t ∧
      (f, a) ∈ t ∧
        ContinuousOn (fun fa ↦ cfc ((toFun {s}) fa.1) fa.2)
          ({f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s} ×ˢ {a | p a ∧ s ∈ 𝓝ˢ (spectrum 𝕜 a)} ∩ t)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: 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
s : Set ℝ≥0
⊢ ContinuousOn (fun fa ↦ cfc ((toFun {s}) fa.1) fa.2)
    ({f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s} ×ˢ {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (spectrum ℝ≥0 a)})

Tactic:
refine continuousOn_of_locally_continuousOn fun (f, a) ⟨hf, ha, has⟩ ↦ ?_

Goal state after:
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
s : Set ℝ≥0
x✝¹ : (ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0) × A
f : ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0
a : A
x✝ : (f, a) ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s} ×ˢ {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (spectrum ℝ≥0 a)}
hf : (f, a).1 ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s}
ha : 0 ≤ (f, a).2
has : s ∈ 𝓝ˢ (spectrum ℝ≥0 (f, a).2)
⊢ ∃ t,
    IsOpen[instTopologicalSpaceProd] t ∧
      (f, a) ∈ t ∧
        ContinuousOn (fun fa ↦ cfc ((toFun {s}) fa.1) fa.2)
          ({f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s} ×ˢ {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (spectrum ℝ≥0 a)} ∩ t)
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
⊢ [IsStrictlyPositive a, IsStrictlyPositive (sqrt a) ∧ a = sqrt a * sqrt a, IsUnit (sqrt a) ∧ a = sqrt a * sqrt a,
      ∃ b, IsStrictlyPositive b ∧ a = b * b, ∃ b, IsUnit b ∧ IsSelfAdjoint b ∧ a = b * b,
      ∃ b, IsUnit b ∧ a = star b * b, ∃ b, IsUnit b ∧ a = b * star b, 0 ≤ a ∧ IsUnit a,
      IsSelfAdjoint a ∧ ∀ x ∈ spectrum ℝ a, 0 < x].TFAE

Tactic:
by
  tfae_have 1 ↔ 8 := IsStrictlyPositive.iff_of_unital
  tfae_have 1 ↔ 9 := ⟨fun h => ⟨h.isSelfAdjoint,
      StarOrderedRing.isStrictlyPositive_iff_spectrum_pos a |>.mp h⟩,
    fun h => (StarOrderedRing.isStrictlyPositive_iff_spectrum_pos a).mpr h.2⟩
  tfae_have 1 → 2 := fun h => ⟨h.sqrt, sqrt_mul_sqrt_self a |>.symm⟩
  tfae_have 2 → 3 := fun h => ⟨h.1.isUnit, h.2⟩
  tfae_have 3 → 4 := fun h => ⟨sqrt a, h.1.isStrictlyPositive (sqrt_nonneg _), h.2⟩
  tfae_have 4 → 5 := fun ⟨b, hb, hab⟩ => ⟨b, hb.isUnit, hb.isSelfAdjoint, hab⟩
  tfae_have 5 → 6 := fun ⟨b, hb, hbsa, hab⟩ => ⟨b, hb, hbsa.symm ▸ hab⟩
  tfae_have 6 → 7 := fun ⟨b, hb, hab⟩ => ⟨star b, hb.star, star_star b |>.symm ▸ hab⟩
  tfae_have 7 → 8 := fun ⟨b, hb, hab⟩ => ⟨hab ▸ mul_star_self_nonneg _, hab ▸ hb.mul hb.star⟩
  tfae_finish

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' : ∀ i ∈ t, s ∈ 𝓝ˢ (spectrum ℝ≥0 (a i))
⊢ ContinuousOn (fun x ↦ cfc f (a x)) t

Tactic:
have (x : t) : ∃ S, IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a x), spectrum ℝ≥0 x' ⊆ S) ∧ S ⊆ s := by
    obtain ⟨S, ⟨hS₁, hS₂⟩, hS₃⟩ :=
      spectrum.isCompact_nnreal (a x) |>.nhdsSet_basis_isCompact.mem_iff.mp (hs' x x.2)
    refine ⟨S, hS₂, ?_, hS₃⟩
    exact upperHemicontinuous_spectrum_nnreal A |>.upperHemicontinuousAt (a x) _ hS₁ |>.mono
      fun _ ↦ subset_of_mem_nhdsSet

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))
this : ∀ (x : ↑t), ∃ S, IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a ↑x), spectrum ℝ≥0 x' ⊆ S) ∧ S ⊆ s
⊢ ContinuousOn (fun x ↦ cfc f (a x)) t
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ MonotoneOn (cfcₙ fun x ↦ 1 - (1 + x)⁻¹) (Set.Ici 0)

Tactic:
intro a (ha : 0 ≤ a) b (hb : 0 ≤ b) hab
  calc _ = cfcₙ (fun x : ℝ≥0 => 1 - (1 + x)⁻¹) a := by
          rw [cfcₙ_nnreal_eq_real _ _ ha]
          refine cfcₙ_congr ?_
          intro x hx
          have hx' : 0 ≤ x := by grind
          simp [hx']
    _ ≤ cfcₙ (fun x : ℝ≥0 => 1 - (1 + x)⁻¹) b :=
          CFC.monotoneOn_one_sub_one_add_inv ha hb hab
    _ = cfcₙ (fun x : ℝ => 1 - (1 + x)⁻¹) b := by
          rw [cfcₙ_nnreal_eq_real _ _ hb]
          refine cfcₙ_congr ?_
          intro x hx
          have hx' : 0 ≤ x := by grind
          simp [hx']

Goal state after: