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)
l : Filter ↥S
a : ↥S
ha : IsUnit (↑a : A)
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
⊢ Tendsto Ring.inverse (map (⇑(val S) : (a : ↥S) → A) l) (𝓝 (Ring.inverse (↑ha.unit : A)))

Tactic:
(NormedRing.inverse_continuousAt _).tendsto.comp <|
      continuousAt_subtype_val.tendsto.comp <| map_mono hla

Premises used: Filter.map_mono, continuousAt_subtype_val, Ring.inverse, dite, ContinuousAt.tendsto, NormedRing.inverse_continuousAt, Filter.Tendsto.comp
-- 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)
l : Filter ↥S
a : ↥S
ha : IsUnit (↑a : A)
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
⊢ Tendsto Ring.inverse (map (⇑(val S) : (a : ↥S) → A) l) (𝓝 (Ring.inverse (↑ha.unit : A)))

Tactic:
exact (NormedRing.inverse_continuousAt _).tendsto.comp <|
      continuousAt_subtype_val.tendsto.comp <| map_mono hla

Premises used: Filter.map_mono, continuousAt_subtype_val, ContinuousAt.tendsto, NormedRing.inverse_continuousAt, Filter.Tendsto.comp
-- 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)
l : Filter ↥S
a : ↥S
ha : IsUnit (↑a : A)
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
⊢ Tendsto Ring.inverse (map (⇑(val S) : (a : ↥S) → A) l) (𝓝 (↑ha.unit⁻¹ : A))

Tactic:
have hla₂ : Tendsto Ring.inverse (map (val S) l) (𝓝 (↑ha.unit⁻¹ : A)) := by
    rw [← Ring.inverse_unit]
    exact (NormedRing.inverse_continuousAt _).tendsto.comp <|
      continuousAt_subtype_val.tendsto.comp <| map_mono hla
-- 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)
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))
mem : (↑ha.unit⁻¹ : A) ∈ S
⊢ IsUnit a

Tactic:
⟨⟨a, ⟨(↑ha.unit⁻¹ : A), mem⟩, ?_, ?_⟩, rfl⟩

Premises used: Units.val, IsUnit, Subtype.mk, Inv.inv, Units.mk, Exists.intro, IsUnit.unit, rfl
-- 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)
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))
mem : (↑ha.unit⁻¹ : A) ∈ S
refine_1 : a * Subtype.mk (p := fun (x : A) ↦ x ∈ S) (↑ha.unit⁻¹ : A) mem = 1
refine_2 : Subtype.mk (p := fun (x : A) ↦ x ∈ S) (↑ha.unit⁻¹ : A) mem * a = 1
⊢ IsUnit a

Tactic:
refine ⟨⟨a, ⟨(↑ha.unit⁻¹ : A), mem⟩, ?_, ?_⟩, rfl⟩
-- 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)
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))
mem : (↑ha.unit⁻¹ : A) ∈ S
refine_1 : (↑(a * Subtype.mk (p := fun (x : A) ↦ x ∈ S) (↑ha.unit⁻¹ : A) mem) : A) = (↑1 : A)
⊢ a * Subtype.mk (p := fun (x : A) ↦ x ∈ S) (↑ha.unit⁻¹ : A) mem = 1

Tactic:
ext
-- 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)
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))
mem : (↑ha.unit⁻¹ : A) ∈ S
⊢ (↑(a * Subtype.mk (p := fun (x : A) ↦ x ∈ S) (↑ha.unit⁻¹ : A) mem) : A) = (↑1 : A)

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)
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))
mem : (↑ha.unit⁻¹ : A) ∈ S
refine_2 : (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ S) (↑ha.unit⁻¹ : A) mem * a) : A) = (↑1 : A)
⊢ Subtype.mk (p := fun (x : A) ↦ x ∈ S) (↑ha.unit⁻¹ : A) mem * a = 1

Tactic:
ext
-- 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)
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))
mem : (↑ha.unit⁻¹ : A) ∈ S
⊢ (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ S) (↑ha.unit⁻¹ : A) mem * a) : A) = (↑1 : A)

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)
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))
suffices : (↑ha.unit⁻¹ : A) ∈ S
⊢ IsUnit a

Tactic:
suffices mem : (↑ha.unit⁻¹ : A) ∈ S by
    refine ⟨⟨a, ⟨(↑ha.unit⁻¹ : A), mem⟩, ?_, ?_⟩, rfl⟩
    all_goals ext; 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)
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))
apply : ∀ᶠ (x : A) in map (⇑(val S) : (a : ↥S) → A) l, Ring.inverse x ∈ (↑S : Set A)
⊢ (↑ha.unit⁻¹ : A) ∈ S

Tactic:
apply hS.mem_of_tendsto hla₂

Premises used: IsClosed.mem_of_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)
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))
rw : ∀ᶠ (a : ↥S) in l, Membership.mem (α := A) (↑S : Set A) (Ring.inverse ((val S : (a : ↥S) → A) a) : A)
⊢ ∀ᶠ (x : A) in map (⇑(val S) : (a : ↥S) → A) l, Ring.inverse x ∈ (↑S : Set A)

Tactic:
rw [Filter.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)
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))
apply : ∀ (x : ↥S) (hx : IsUnit x), Membership.mem (α := A) (↑S : Set A) (Ring.inverse ((val S : (a : ↥S) → A) x) : A)
⊢ ∀ᶠ (a : ↥S) in l, Membership.mem (α := A) (↑S : Set A) (Ring.inverse ((val S : (a : ↥S) → A) a) : A)

Tactic:
apply hl.mono fun x hx ↦ ?_

Premises used: Filter.Eventually.mono
-- 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)
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
suffices : Eq (α := A) (Ring.inverse ((val S : (a : ↥S) → A) x) : A) ((val S : (a : ↥S) → A) (↑hx.unit⁻¹ : ↥S) : A)
⊢ Membership.mem (α := A) (↑S : Set A) (Ring.inverse ((val S : (a : ↥S) → A) x) : A)

Tactic:
suffices Ring.inverse (val S x) = (val S ↑hx.unit⁻¹) from this ▸ Subtype.property _
-- 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)
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
rw :
  (↑(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)
⊢ Eq (α := A) (Ring.inverse ((val S : (a : ↥S) → A) x) : A) ((val S : (a : ↥S) → A) (↑hx.unit⁻¹ : ↥S) : A)

Tactic:
rw [← (hx.map (val S)).unit_spec, Ring.inverse_unit (hx.map (val S)).unit, val]

Premises used: Ring.inverse_unit, IsUnit.unit, IsUnit.map, IsUnit.unit_spec, SubalgebraClass.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)
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
apply :
  HMul.hMul (β := A)
      (↑(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' := ⋯ : ↥S →ₐ[𝕜] A } :
            (a : ↥S) → A)
          (↑hx.unit⁻¹ : ↥S) :
        A) =
    1
⊢ (↑(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)

Tactic:
apply Units.mul_eq_one_iff_inv_eq.mp

Premises used: Iff.mp, Units.mul_eq_one_iff_inv_eq
-- 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)
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
⊢ HMul.hMul (β := A)
      (↑(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' := ⋯ : ↥S →ₐ[𝕜] A } :
            (a : ↥S) → A)
          (↑hx.unit⁻¹ : ↥S) :
        A) =
    1

Tactic:
simpa [-IsUnit.mul_val_inv] using congr(($hx.mul_val_inv : A))

Premises used: IsUnit.mul_val_inv
-- 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
⊢ CompleteSpace.{u_4} ↥S

Tactic:
have : CompleteSpace S := hS.completeSpace_coe
-- 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μ : μ ∈ frontier (σ 𝕜 x)
by_contra : ∀ (h : μ ∉ σ 𝕜 (↑x : A)), False
⊢ μ ∈ σ 𝕜 (↑x : A)

Tactic:
by_contra h
-- 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μ : μ ∈ frontier (σ 𝕜 x)
h : μ ∉ σ 𝕜 (↑x : A)
⊢ IsUnit (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) μ : A) (↑x : A))

Tactic:
rw [spectrum.notMem_iff] at h

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
this : CompleteSpace.{u_4} ↥S
μ : 𝕜
hμ : μ ∈ frontier (σ 𝕜 x)
h : IsUnit (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) μ : A) (↑x : A))
⊢ μ ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x)ᶜ ∧ μ ∉ (σ 𝕜 x)ᶜ

Tactic:
rw [← frontier_compl, (spectrum.isClosed _).isOpen_compl.frontier_eq, mem_diff] at hμ

Premises used: frontier_compl, IsClosed.isOpen_compl, Set.mem_diff, IsOpen.frontier_eq
-- 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μ : μ ∈ frontier (σ 𝕜 x)
h : IsUnit (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) μ : A) (↑x : A))
hμ₁ : μ ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x)ᶜ ∧ μ ∉ (σ 𝕜 x)ᶜ
⊢ IsUnit (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) μ : A) (↑x : A))

Tactic:
rw [← frontier_compl, (spectrum.isClosed _).isOpen_compl.frontier_eq, mem_diff] at hμ

Premises used: frontier_compl, IsClosed.isOpen_compl, Set.mem_diff, IsOpen.frontier_eq
-- 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μ : μ ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x)ᶜ ∧ μ ∉ (σ 𝕜 x)ᶜ
h : IsUnit (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) μ : A) (↑x : A))
⊢ μ ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x)ᶜ

Tactic:
obtain ⟨hμ₁, hμ₂⟩ := hμ
-- 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μ : μ ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x)ᶜ ∧ μ ∉ (σ 𝕜 x)ᶜ
h : IsUnit (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) μ : A) (↑x : A))
hμ₁ : μ ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x)ᶜ
⊢ μ ∉ (σ 𝕜 x)ᶜ

Tactic:
obtain ⟨hμ₁, hμ₂⟩ := hμ
-- 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μ₁ : μ ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x)ᶜ
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
⊢ ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)

Tactic:
rw [mem_closure_iff_clusterPt] at hμ₁

Premises used: mem_closure_iff_clusterPt
-- 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μ₁ : μ ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x)ᶜ
hμ₂ : μ ∉ (σ 𝕜 x)ᶜ
hμ₃ : ClusterPt μ (𝓟 (σ 𝕜 x)ᶜ)
⊢ μ ∉ (σ 𝕜 x)ᶜ

Tactic:
rw [mem_closure_iff_clusterPt] at hμ₁

Premises used: mem_closure_iff_clusterPt
-- 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)ᶜ
apply : μ ∈ (σ 𝕜 x)ᶜ
⊢ False

Tactic:
apply hμ₂
-- 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 : IsUnit (HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) μ : ↥S) x)
⊢ μ ∈ (σ 𝕜 x)ᶜ

Tactic:
rw [mem_compl_iff, spectrum.notMem_iff]

Premises used: Set.mem_compl_iff, 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
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)

Tactic:
Subalgebra.isUnit_of_isUnit_val_of_eventually S h ?_ ?_ <| .map hμ₁ (algebraMap 𝕜 S · - x)

Premises used: Algebra.algebraMap, HSub.hSub, Membership.mem, Subtype, Filter.NeBot.map, Subalgebra.isUnit_of_isUnit_val_of_eventually, DFunLike.coe
-- 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_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)
refine_2 :
  ∀ᶠ (x : ↥S) in
    map (fun (x_1 : 𝕜) ↦ HSub.hSub (α := ↥S) ((algebraMap 𝕜 ↥S : (a : 𝕜) → ↥S) x_1 : ↥S) x) (𝓝 μ ⊓ 𝓟 (σ 𝕜 x)ᶜ), IsUnit x
⊢ IsUnit (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)

Premises used: Subalgebra.isUnit_of_isUnit_val_of_eventually