awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
this : CompleteSpace.{u_4} ↥S
μ : 𝕜
h : IsUnit (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) μ : A) (↑x : A))
hμ₁ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
⊢ 𝓝 μ ⊓ 𝓟 (σ 𝕜 x)ᶜ ≤ 𝓝 μ

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
this : CompleteSpace.{u_4} ↥S
μ : 𝕜
h : IsUnit (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) μ : A) (↑x : A))
hμ₁ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
rw :
  ContinuousAt.{u_3, u_4} (Y := ↥S) (fun (x_1 : 𝕜) ↦ HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) x_1 : ↥S) x)
    μ
⊢ map (fun (x_1 : 𝕜) ↦ HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) x_1 : ↥S) x) (𝓝 μ) ≤
    𝓝 (HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) μ : ↥S) x)

Tactic:
rw [← Filter.Tendsto, ← ContinuousAt]

Premises used: ContinuousAt, Filter.Tendsto
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
this : CompleteSpace.{u_4} ↥S
μ : 𝕜
h : IsUnit (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) μ : A) (↑x : A))
hμ₁ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
⊢ ContinuousAt.{u_3, u_4} (Y := ↥S) (fun (x_1 : 𝕜) ↦ HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) x_1 : ↥S) x)
    μ

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
this : CompleteSpace.{u_4} ↥S
μ : 𝕜
h : IsUnit (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) μ : A) (↑x : A))
hμ₁ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
_ :
  map (fun (x_1 : 𝕜) ↦ HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) x_1 : ↥S) x) (𝓝 μ) ≤
    𝓝 (HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) μ : ↥S) x)
⊢ map (fun (x_1 : 𝕜) ↦ HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) x_1 : ↥S) x) (𝓝 μ ⊓ 𝓟 (σ 𝕜 x)ᶜ) ≤
    𝓝 (HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) μ : ↥S) x)

Tactic:
calc
      _ ≤ map _ (𝓝 μ) := map_mono (by simp)
      _ ≤ _ := by rw [← Filter.Tendsto, ← ContinuousAt]; fun_prop

Premises used: Filter.map_mono, Filter.map, nhds
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
this : CompleteSpace.{u_4} ↥S
μ : 𝕜
h : IsUnit (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) μ : A) (↑x : A))
hμ₁ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
refine_2 : ∀ᶠ (a : 𝕜) in 𝓝 μ ⊓ 𝓟 (σ 𝕜 x)ᶜ, IsUnit (HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) a : ↥S) x)
⊢ ∀ᶠ (x : ↥S) in
    map (fun (x_1 : 𝕜) ↦ HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) x_1 : ↥S) x) (𝓝 μ ⊓ 𝓟 (σ 𝕜 x)ᶜ), IsUnit x

Tactic:
rw [eventually_map]

Premises used: Filter.eventually_map
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
this : CompleteSpace.{u_4} ↥S
μ : 𝕜
h : IsUnit (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) μ : A) (↑x : A))
hμ₁ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
refine_2 : ∀ᶠ (x_1 : 𝕜) in 𝓟 (σ 𝕜 x)ᶜ, IsUnit (HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) x_1 : ↥S) x)
⊢ ∀ᶠ (a : 𝕜) in 𝓝 μ ⊓ 𝓟 (σ 𝕜 x)ᶜ, IsUnit (HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) a : ↥S) x)

Tactic:
apply Eventually.filter_mono inf_le_right

Premises used: Filter.Eventually.filter_mono, inf_le_right
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
this : CompleteSpace.{u_4} ↥S
μ : 𝕜
h : IsUnit (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) μ : A) (↑x : A))
hμ₁ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓟 (σ 𝕜 x)ᶜ, IsUnit (HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) x_1 : ↥S) x)

Tactic:
simp [spectrum.notMem_iff]

Premises used: spectrum.notMem_iff
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
rw : frontier (σ 𝕜 x) ⊆ σ 𝕜 (↑x : A) ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ
⊢ frontier (σ 𝕜 x) ⊆ frontier (σ 𝕜 (↑x : A))

Tactic:
rw [frontier_eq_closure_inter_closure (s := σ 𝕜 (x : A)),
    (spectrum.isClosed (x : A)).closure_eq]

Premises used: IsClosed.closure_eq, spectrum.isClosed, frontier_eq_closure_inter_closure, Subtype.val
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
apply : frontier (σ 𝕜 x) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ
⊢ frontier (σ 𝕜 x) ⊆ σ 𝕜 (↑x : A) ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ

Tactic:
apply subset_inter (frontier_spectrum S x)

Premises used: Set.subset_inter, Subalgebra.frontier_spectrum
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
rw :
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x) ∩
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x)ᶜ ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ
⊢ frontier (σ 𝕜 x) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ

Tactic:
rw [frontier_eq_closure_inter_closure]

Premises used: frontier_eq_closure_inter_closure
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x) ∩
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x)ᶜ ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ

Tactic:
inter_subset_right |>.trans <|
    closure_mono <| compl_subset_compl.mpr <| spectrum.subset_subalgebra x

Premises used: Iff.mpr, HasSubset.Subset.trans, spectrum.subset_subalgebra, closure_mono, Set.compl_subset_compl, Set.inter_subset_right
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x) ∩
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x)ᶜ ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ

Tactic:
exact inter_subset_right |>.trans <|
    closure_mono <| compl_subset_compl.mpr <| spectrum.subset_subalgebra x

Premises used: Iff.mpr, HasSubset.Subset.trans, spectrum.subset_subalgebra, closure_mono, Set.compl_subset_compl, Set.inter_subset_right
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
this : IsClopen (X := (↑(σ 𝕜 (↑x : A))ᶜ : Type u_3)) ((σ 𝕜 (↑x : A))ᶜ ↓∩ σ 𝕜 x \ σ 𝕜 (↑x : A))
rw : σ 𝕜 x = σ 𝕜 (↑x : A) ∪ σ 𝕜 x \ σ 𝕜 (↑x : A)
rw₁ rw₂ : σ 𝕜 x = σ 𝕜 x
⊢ σ 𝕜 x = σ 𝕜 (↑x : A) ∪ ⋃ z ∈ σ 𝕜 x \ σ 𝕜 (↑x : A), connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z

Tactic:
rw [← this.biUnion_connectedComponentIn (diff_subset_compl _ _),
      union_diff_cancel (spectrum.subset_subalgebra x)]

Premises used: spectrum.subset_subalgebra, Set.union_diff_cancel, IsClopen.biUnion_connectedComponentIn, Set.diff_subset_compl
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
suffices : IsClopen (X := (↑(σ 𝕜 (↑x : A))ᶜ : Type u_3)) ((σ 𝕜 (↑x : A))ᶜ ↓∩ σ 𝕜 x \ σ 𝕜 (↑x : A))
⊢ σ 𝕜 x = σ 𝕜 (↑x : A) ∪ ⋃ z ∈ σ 𝕜 x \ σ 𝕜 (↑x : A), connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z

Tactic:
suffices IsClopen ((σ 𝕜 (x : A))ᶜ ↓∩ (σ 𝕜 x \ σ 𝕜 (x : A))) by
    rw [← this.biUnion_connectedComponentIn (diff_subset_compl _ _),
      union_diff_cancel (spectrum.subset_subalgebra x)]
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
this : CompleteSpace.{u_4} ↥S
rw : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((σ 𝕜 (↑x : A))ᶜ ∩ interior (σ 𝕜 x))
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x \ σ 𝕜 (↑x : A))

Tactic:
rw [← (spectrum.isClosed (𝕜 := 𝕜) x).closure_eq, closure_eq_interior_union_frontier,
      union_diff_distrib, diff_eq_empty.mpr (frontier_spectrum S x),
      diff_eq_compl_inter, union_empty]

Premises used: Iff.mpr, Set.union_empty, IsClosed.closure_eq, Set.diff_eq_compl_inter, spectrum.isClosed, Set.union_diff_distrib, Subalgebra.frontier_spectrum, closure_eq_interior_union_frontier, Set.diff_eq_empty
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
this : CompleteSpace.{u_4} ↥S
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((σ 𝕜 (↑x : A))ᶜ ∩ interior (σ 𝕜 x))

Tactic:
(spectrum.isClosed _).isOpen_compl.inter isOpen_interior

Premises used: IsClosed.isOpen_compl, isOpen_interior, IsOpen.inter
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
this : CompleteSpace.{u_4} ↥S
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((σ 𝕜 (↑x : A))ᶜ ∩ interior (σ 𝕜 x))

Tactic:
exact (spectrum.isClosed _).isOpen_compl.inter isOpen_interior

Premises used: IsClosed.isOpen_compl, isOpen_interior, IsOpen.inter
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
this : CompleteSpace.{u_4} ↥S
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x \ σ 𝕜 (↑x : A))

Tactic:
have h_open : IsOpen (σ 𝕜 x \ σ 𝕜 (x : A)) := by
    rw [← (spectrum.isClosed (𝕜 := 𝕜) x).closure_eq, closure_eq_interior_union_frontier,
      union_diff_distrib, diff_eq_empty.mpr (frontier_spectrum S x),
      diff_eq_compl_inter, union_empty]
    exact (spectrum.isClosed _).isOpen_compl.inter isOpen_interior
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
this : CompleteSpace.{u_4} ↥S
h_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x \ σ 𝕜 (↑x : A))
apply : Disjoint (frontier (σ 𝕜 x \ σ 𝕜 (↑x : A))) (σ 𝕜 (↑x : A))ᶜ
⊢ IsClopen (X := (↑(σ 𝕜 (↑x : A))ᶜ : Type u_3)) ((σ 𝕜 (↑x : A))ᶜ ↓∩ σ 𝕜 x \ σ 𝕜 (↑x : A))

Tactic:
apply isClopen_preimage_val h_open

Premises used: isClopen_preimage_val
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
this : CompleteSpace.{u_4} ↥S
h_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x \ σ 𝕜 (↑x : A))
suffices : frontier (σ 𝕜 x \ σ 𝕜 (↑x : A)) ⊆ frontier (σ 𝕜 (↑x : A))
⊢ Disjoint (frontier (σ 𝕜 x \ σ 𝕜 (↑x : A))) (σ 𝕜 (↑x : A))ᶜ

Tactic:
suffices h_frontier : frontier (σ 𝕜 x \ σ 𝕜 (x : A)) ⊆ frontier (σ 𝕜 (x : A)) from
    disjoint_of_subset_left h_frontier <| disjoint_compl_right.frontier_left
      (spectrum.isClosed _).isOpen_compl
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
this : CompleteSpace.{u_4} ↥S
h_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x \ σ 𝕜 (↑x : A))
rw : frontier ((σ 𝕜 (↑x : A))ᶜ ∩ σ 𝕜 x) ⊆ frontier (σ 𝕜 (↑x : A))
⊢ frontier (σ 𝕜 x \ σ 𝕜 (↑x : A)) ⊆ frontier (σ 𝕜 (↑x : A))

Tactic:
rw [diff_eq_compl_inter]

Premises used: Set.diff_eq_compl_inter
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
this : CompleteSpace.{u_4} ↥S
h_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x \ σ 𝕜 (↑x : A))
apply :
  frontier (σ 𝕜 (↑x : A))ᶜ ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x) ∪
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ ∩ frontier (σ 𝕜 x) ⊆
    frontier (σ 𝕜 (↑x : A))
⊢ frontier ((σ 𝕜 (↑x : A))ᶜ ∩ σ 𝕜 x) ⊆ frontier (σ 𝕜 (↑x : A))

Tactic:
apply (frontier_inter_subset _ _).trans

Premises used: HasSubset.Subset.trans, frontier_inter_subset
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
this : CompleteSpace.{u_4} ↥S
h_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x \ σ 𝕜 (↑x : A))
rw :
  frontier (σ 𝕜 (↑x : A)) ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x) ∪
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ ∩ frontier (σ 𝕜 x) ⊆
    frontier (σ 𝕜 (↑x : A))
⊢ frontier (σ 𝕜 (↑x : A))ᶜ ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x) ∪
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ ∩ frontier (σ 𝕜 x) ⊆
    frontier (σ 𝕜 (↑x : A))

Tactic:
rw [frontier_compl]

Premises used: frontier_compl
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
this : CompleteSpace.{u_4} ↥S
h_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x \ σ 𝕜 (↑x : A))
apply :
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ ∩ frontier (σ 𝕜 x) ⊆
    frontier (σ 𝕜 (↑x : A))
⊢ frontier (σ 𝕜 (↑x : A)) ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x) ∪
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ ∩ frontier (σ 𝕜 x) ⊆
    frontier (σ 𝕜 (↑x : A))

Tactic:
apply union_subset <| inter_subset_left

Premises used: Set.inter_subset_left, Set.union_subset
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
this : CompleteSpace.{u_4} ↥S
h_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x \ σ 𝕜 (↑x : A))
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ ∩ frontier (σ 𝕜 x) ⊆
    frontier (σ 𝕜 (↑x : A))

Tactic:
inter_subset_inter_right _ ?_ |>.trans <| inter_subset_right

Premises used: Set.inter_subset_inter_right, HasSubset.Subset.trans, Set.inter_subset_right
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
this : CompleteSpace.{u_4} ↥S
h_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x \ σ 𝕜 (↑x : A))
refine : frontier (σ 𝕜 x) ⊆ frontier (σ 𝕜 (↑x : A))
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ ∩ frontier (σ 𝕜 x) ⊆
    frontier (σ 𝕜 (↑x : A))

Tactic:
refine inter_subset_inter_right _ ?_ |>.trans <| inter_subset_right

Premises used: Set.inter_subset_inter_right, HasSubset.Subset.trans, Set.inter_subset_right
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
this : CompleteSpace.{u_4} ↥S
h_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x \ σ 𝕜 (↑x : A))
⊢ frontier (σ 𝕜 x) ⊆ frontier (σ 𝕜 (↑x : A))

Tactic:
frontier_subset_frontier S x

Premises used: Subalgebra.frontier_subset_frontier
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
this : CompleteSpace.{u_4} ↥S
h_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x \ σ 𝕜 (↑x : A))
⊢ frontier (σ 𝕜 x) ⊆ frontier (σ 𝕜 (↑x : A))

Tactic:
exact frontier_subset_frontier S x

Premises used: Subalgebra.frontier_subset_frontier
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
z : 𝕜
hz : z ∈ σ 𝕜 x
pos : ∀ (hz' : z ∈ σ 𝕜 (↑x : A)), Bornology.IsBounded (connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z)
neg : ∀ (hz' : z ∉ σ 𝕜 (↑x : A)), Bornology.IsBounded (connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z)
⊢ Bornology.IsBounded (connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z)

Tactic:
by_cases hz' : z ∈ σ 𝕜 (x : A)

Premises used: spectrum, Subtype.val
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
z : 𝕜
hz : z ∈ σ 𝕜 x
hz' : z ∈ σ 𝕜 (↑x : A)
⊢ Bornology.IsBounded (connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z)

Tactic:
simp [connectedComponentIn_eq_empty (show z ∉ (σ 𝕜 (x : A))ᶜ from not_not.mpr hz')]

Premises used: Iff.mpr, Classical.not_not, connectedComponentIn_eq_empty
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
z : 𝕜
hz : z ∈ σ 𝕜 x
hz' : z ∉ σ 𝕜 (↑x : A)
⊢ CompleteSpace.{u_4} ↥S

Tactic:
have : CompleteSpace S := hS.completeSpace_coe