awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
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)
l : Filter ↥S
a : ↥S
ha : IsUnit (↑a : A)
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
hla₂ : Tendsto Ring.inverse (map (⇑(val S) : (a : ↥S) → A) l) (𝓝 (↑ha.unit⁻¹ : A))
x : ↥S
hx : IsUnit x
⊢ (↑(IsUnit.unit (a :=
            ({ toFun := Subtype.val (p := fun (x : A) ↦ x ∈ S), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                  map_add' := ⋯, commutes' := ⋯ : ↥S →ₐ[𝕜] A } :
                (a : ↥S) → A)
              x)
            ⋯)⁻¹ :
      A) =
    ({ toFun := Subtype.val (p := fun (x : A) ↦ x ∈ S), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
          commutes' := ⋯ } :
        (a : ↥S) → A)
      (↑hx.unit⁻¹ : ↥S)
have apply : HMul.hMul (β := A)
    (↑(IsUnit.unit (a :=
          ({ toFun := Subtype.val (p := fun (x : A) ↦ x ∈ S), map_one' := sorry, map_mul' := sorry, map_zero' := sorry,
                map_add' := sorry, commutes' := sorry : ↥S →ₐ[𝕜] A } :
              (a : ↥S) → A)
            x)
          sorry) :
      A)
    (({ toFun := Subtype.val (p := fun (x : A) ↦ x ∈ S), map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry,
            commutes' := sorry : ↥S →ₐ[𝕜] A } :
          (a : ↥S) → A)
        (↑hx.unit⁻¹ : ↥S) :
      A) =
  1
Tactic: apply Units.mul_eq_one_iff_inv_eq.mp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
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
⊢ frontier (σ 𝕜 x) ⊆ σ 𝕜 (↑x : A)
have this : CompleteSpace.{u_4} ↥S
Tactic: have : CompleteSpace S := hS.completeSpace_coe
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
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μ : μ ∈ frontier (σ 𝕜 x)
⊢ μ ∈ σ 𝕜 (↑x : A)
have by_contra : ∀ (h : μ ∉ σ 𝕜 (↑x : A)), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
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μ : μ ∈ frontier (σ 𝕜 x)
h : μ ∉ σ 𝕜 (↑x : A)
⊢ False
have h₁ : IsUnit (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) μ : A) (↑x : A))
Tactic: rw [spectrum.notMem_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
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μ : μ ∈ frontier (σ 𝕜 x)
h : IsUnit (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) μ : A) (↑x : A))
⊢ False
have hμ₁ : μ ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x)ᶜ ∧ μ ∉ (σ 𝕜 x)ᶜ
Tactic: rw [← frontier_compl, (spectrum.isClosed _).isOpen_compl.frontier_eq, mem_diff] at hμ
Cleared hypotheses: hμ, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
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μ : μ ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x)ᶜ ∧ μ ∉ (σ 𝕜 x)ᶜ
h : IsUnit (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) μ : A) (↑x : A))
⊢ False
have hμ₁ : μ ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x)ᶜ
Tactic: obtain ⟨hμ₁, hμ₂⟩ := hμ
Cleared hypotheses: hμ
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
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μ : μ ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x)ᶜ ∧ μ ∉ (σ 𝕜 x)ᶜ
h : IsUnit (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) μ : A) (↑x : A))
hμ₁ : μ ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x)ᶜ
⊢ False
have hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
Tactic: obtain ⟨hμ₁, hμ₂⟩ := hμ
Cleared hypotheses: hμ
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
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μ₁ : μ ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x)ᶜ
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
⊢ False
have hμ₃ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
Tactic: rw [mem_closure_iff_clusterPt] at hμ₁
Cleared hypotheses: hμ₁, hμ₂
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
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)ᶜ
⊢ False
have apply : μ ∈ (σ 𝕜 x)ᶜ
Tactic: apply hμ₂
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
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)ᶜ
have rw : IsUnit (HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) μ : ↥S) x)
Tactic: rw [mem_compl_iff, spectrum.notMem_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
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)ᶜ
⊢ IsUnit (HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) μ : ↥S) x)
have refine_1 : 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: refine Subalgebra.isUnit_of_isUnit_val_of_eventually S h ?_ ?_ <| .map hμ₁ (algebraMap 𝕜 S · - x)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
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_1 :
  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)
⊢ IsUnit (HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) μ : ↥S) x)
have refine_2 : ∀ᶠ (x : ↥S) in
  map (fun (x_1 : 𝕜) ↦ HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) x_1 : ↥S) x) (𝓝 μ ⊓ 𝓟 (σ 𝕜 x)ᶜ), IsUnit x
Tactic: refine Subalgebra.isUnit_of_isUnit_val_of_eventually S h ?_ ?_ <| .map hμ₁ (algebraMap 𝕜 S · - x)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
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)
have rw : ContinuousAt.{u_3, u_4} (Y := ↥S) (fun (x_1 : 𝕜) ↦ HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) x_1 : ↥S) x) μ
Tactic: rw [← Filter.Tendsto, ← ContinuousAt]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
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) (𝓝 μ ⊓ 𝓟 (σ 𝕜 x)ᶜ) ≤
    𝓝 (HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) μ : ↥S) x)
have _ : 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: calc
      _ ≤ map _ (𝓝 μ) := map_mono (by simp)
      _ ≤ _ := by rw [← Filter.Tendsto, ← ContinuousAt]; fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
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 : ↥S) in
    map (fun (x_1 : 𝕜) ↦ HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) x_1 : ↥S) x) (𝓝 μ ⊓ 𝓟 (σ 𝕜 x)ᶜ), IsUnit x
have refine_2 : ∀ᶠ (a : 𝕜) in 𝓝 μ ⊓ 𝓟 (σ 𝕜 x)ᶜ, IsUnit (HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) a : ↥S) x)
Tactic: rw [eventually_map]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
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)ᶜ
⊢ ∀ᶠ (a : 𝕜) in 𝓝 μ ⊓ 𝓟 (σ 𝕜 x)ᶜ, IsUnit (HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) a : ↥S) x)
have refine_2 : ∀ᶠ (x_1 : 𝕜) in 𝓟 (σ 𝕜 x)ᶜ, IsUnit (HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) x_1 : ↥S) x)
Tactic: apply Eventually.filter_mono inf_le_right
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
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
⊢ frontier (σ 𝕜 x) ⊆ frontier (σ 𝕜 (↑x : A))
have rw : frontier (σ 𝕜 x) ⊆ σ 𝕜 (↑x : A) ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ
Tactic: rw [frontier_eq_closure_inter_closure (s := σ 𝕜 (x : A)),
    (spectrum.isClosed (x : A)).closure_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
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
⊢ frontier (σ 𝕜 x) ⊆ σ 𝕜 (↑x : A) ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ
have apply : frontier (σ 𝕜 x) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ
Tactic: apply subset_inter (frontier_spectrum S x)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
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
⊢ frontier (σ 𝕜 x) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ
have rw : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x) ∩
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x)ᶜ ⊆
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ
Tactic: rw [frontier_eq_closure_inter_closure]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
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))
⊢ σ 𝕜 x = σ 𝕜 (↑x : A) ∪ ⋃ z ∈ σ 𝕜 x \ σ 𝕜 (↑x : A), connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z
have rw : σ 𝕜 x = σ 𝕜 (↑x : A) ∪ σ 𝕜 x \ σ 𝕜 (↑x : A)
Tactic: rw [← this.biUnion_connectedComponentIn (diff_subset_compl _ _),
      union_diff_cancel (spectrum.subset_subalgebra x)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
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)
⊢ σ 𝕜 x = σ 𝕜 (↑x : A) ∪ ⋃ z ∈ σ 𝕜 x \ σ 𝕜 (↑x : A), connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z
have rw₁ : σ 𝕜 x = σ 𝕜 x
Tactic: rw [← this.biUnion_connectedComponentIn (diff_subset_compl _ _),
      union_diff_cancel (spectrum.subset_subalgebra x)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
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
⊢ σ 𝕜 x = σ 𝕜 (↑x : A) ∪ ⋃ z ∈ σ 𝕜 x \ σ 𝕜 (↑x : A), connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z
have suffices : IsClopen (X := (↑(σ 𝕜 (↑x : A))ᶜ : Type u_3)) ((σ 𝕜 (↑x : A))ᶜ ↓∩ σ 𝕜 x \ σ 𝕜 (↑x : A))
Tactic: suffices IsClopen ((σ 𝕜 (x : A))ᶜ ↓∩ (σ 𝕜 x \ σ 𝕜 (x : A))) by
    rw [← this.biUnion_connectedComponentIn (diff_subset_compl _ _),
      union_diff_cancel (spectrum.subset_subalgebra x)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
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
⊢ IsClopen (X := (↑(σ 𝕜 (↑x : A))ᶜ : Type u_3)) ((σ 𝕜 (↑x : A))ᶜ ↓∩ σ 𝕜 x \ σ 𝕜 (↑x : A))
have this : CompleteSpace.{u_4} ↥S
Tactic: have : CompleteSpace S := hS.completeSpace_coe
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
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))
have rw : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((σ 𝕜 (↑x : A))ᶜ ∩ interior (σ 𝕜 x))
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
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
⊢ IsClopen (X := (↑(σ 𝕜 (↑x : A))ᶜ : Type u_3)) ((σ 𝕜 (↑x : A))ᶜ ↓∩ σ 𝕜 x \ σ 𝕜 (↑x : A))
have h_open : 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
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))
⊢ IsClopen (X := (↑(σ 𝕜 (↑x : A))ᶜ : Type u_3)) ((σ 𝕜 (↑x : A))ᶜ ↓∩ σ 𝕜 x \ σ 𝕜 (↑x : A))
have apply : Disjoint (frontier (σ 𝕜 x \ σ 𝕜 (↑x : A))) (σ 𝕜 (↑x : A))ᶜ
Tactic: apply isClopen_preimage_val h_open
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
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))
⊢ Disjoint (frontier (σ 𝕜 x \ σ 𝕜 (↑x : A))) (σ 𝕜 (↑x : A))ᶜ
have suffices : frontier (σ 𝕜 x \ σ 𝕜 (↑x : A)) ⊆ frontier (σ 𝕜 (↑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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
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 \ σ 𝕜 (↑x : A)) ⊆ frontier (σ 𝕜 (↑x : A))
have rw : frontier ((σ 𝕜 (↑x : A))ᶜ ∩ σ 𝕜 x) ⊆ frontier (σ 𝕜 (↑x : A))
Tactic: rw [diff_eq_compl_inter]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
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 : A))ᶜ ∩ σ 𝕜 x) ⊆ frontier (σ 𝕜 (↑x : A))
have apply : frontier (σ 𝕜 (↑x : A))ᶜ ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x) ∪
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ ∩ frontier (σ 𝕜 x) ⊆
  frontier (σ 𝕜 (↑x : A))
Tactic: apply (frontier_inter_subset _ _).trans
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
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 : A))ᶜ ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x) ∪
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ ∩ frontier (σ 𝕜 x) ⊆
    frontier (σ 𝕜 (↑x : A))
have rw : frontier (σ 𝕜 (↑x : A)) ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x) ∪
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ ∩ frontier (σ 𝕜 x) ⊆
  frontier (σ 𝕜 (↑x : A))
Tactic: rw [frontier_compl]