awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Algebra R S
inst_4 : Module S A
inst_5 : IsScalarTower S A A
inst_6 : SMulCommClass S A A
inst_7 : Module R A
inst_8 : IsScalarTower R S A
a : A
r : R
this : {0} ⊆ spectrum R (A := Unitization S A) (↑a : Unitization S A)
apply :
  ∀ (x : IsUnit r),
    ¬IsQuasiregular (-(x.unit⁻¹ • a)) ↔
      ¬IsQuasiregular (-HSMul.hSMul (β := Unitization S A) x.unit⁻¹ (↑a : Unitization S A))
⊢ r ∈ quasispectrum R a ↔ r ∈ quasispectrum R (A := Unitization S A) (↑a : Unitization S A)

Tactic:
apply forall_congr' fun x ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Algebra R S
inst_4 : Module S A
inst_5 : IsScalarTower S A A
inst_6 : SMulCommClass S A A
inst_7 : Module R A
inst_8 : IsScalarTower R S A
a : A
r : R
this : {0} ⊆ spectrum R (A := Unitization S A) (↑a : Unitization S A)
x : IsUnit r
rw :
  IsQuasiregular (-(x.unit⁻¹ • a)) ↔
    IsQuasiregular (-HSMul.hSMul (β := Unitization S A) x.unit⁻¹ (↑a : Unitization S A))
rw₁ :
  IsQuasiregular (-((↑x.unit⁻¹ : R) • a)) ↔
    IsQuasiregular (-HSMul.hSMul (β := Unitization S A) x.unit⁻¹ (↑a : Unitization S A))
rw₂ :
  IsQuasiregular (-((↑x.unit⁻¹ : R) • a)) ↔
    IsQuasiregular (-HSMul.hSMul (β := Unitization S A) (↑x.unit⁻¹ : R) (↑a : Unitization S A))
rw₃ :
  IsQuasiregular (-((↑x.unit⁻¹ : R) • a)) ↔
    IsQuasiregular (R := Unitization S A) (-(↑((↑x.unit⁻¹ : R) • a) : Unitization S A))
rw₄ :
  IsQuasiregular (-((↑x.unit⁻¹ : R) • a)) ↔
    IsQuasiregular (R := Unitization S A) (↑(-((↑x.unit⁻¹ : R) • a)) : Unitization S A)
rw₅ rw₆ : IsQuasiregular (-((↑x.unit⁻¹ : R) • a)) ↔ IsQuasiregular (-((↑x.unit⁻¹ : R) • a))
⊢ ¬IsQuasiregular (-(x.unit⁻¹ • a)) ↔
    ¬IsQuasiregular (-HSMul.hSMul (β := Unitization S A) x.unit⁻¹ (↑a : Unitization S A))

Tactic:
rw [not_iff_not, Units.smul_def, Units.smul_def, ← inr_smul, ← inr_neg, isQuasiregular_inr_iff]

Premises used: Unitization.inr_neg, not_iff_not, Unitization.isQuasiregular_inr_iff, Unitization.inr_smul, Units.smul_def
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Algebra R S
inst_4 : Module S A
inst_5 : IsScalarTower S A A
inst_6 : SMulCommClass S A A
inst_7 : Module R A
inst_8 : IsScalarTower R S A
a : A
rw :
  spectrum R (A := Unitization S A) (↑a : Unitization S A) ∪ {0} =
    spectrum R (A := Unitization S A) (↑a : Unitization S A)
⊢ quasispectrum R (A := Unitization S A) (↑a : Unitization S A) = quasispectrum R a

Tactic:
rw [quasispectrum_eq_spectrum_union_zero, quasispectrum_eq_spectrum_inr' R S]

Premises used: Unitization.quasispectrum_eq_spectrum_inr', quasispectrum_eq_spectrum_union_zero
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Algebra R S
inst_4 : Module S A
inst_5 : IsScalarTower S A A
inst_6 : SMulCommClass S A A
inst_7 : Module R A
inst_8 : IsScalarTower R S A
a : A
⊢ spectrum R (A := Unitization S A) (↑a : Unitization S A) ∪ {0} =
    spectrum R (A := Unitization S A) (↑a : Unitization S A)

Tactic:
simpa using zero_mem_spectrum_inr _ _ _

Premises used: Unitization.zero_mem_spectrum_inr
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a b : A
rw :
  quasispectrum R (a * b) ∩ {r : R | IsUnit r} ∪ quasispectrum R (a * b) ∩ {r : R | IsUnit r}ᶜ =
    quasispectrum R (b * a) ∩ {r : R | IsUnit r} ∪ quasispectrum R (b * a) ∩ {r : R | IsUnit r}ᶜ
⊢ quasispectrum R (a * b) = quasispectrum R (b * a)

Tactic:
rw [← Set.inter_union_compl (quasispectrum R (a * b)) {r | IsUnit r},
    ← Set.inter_union_compl (quasispectrum R (b * a)) {r | IsUnit r}]

Premises used: HMul.hMul, setOf, quasispectrum, IsUnit, Set.inter_union_compl
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a b : A
h : quasispectrum R (a * b) ∩ {r : R | IsUnit r} = quasispectrum R (b * a) ∩ {r : R | IsUnit r}
h₁ : quasispectrum R (a * b) ∩ {r : R | IsUnit r}ᶜ = quasispectrum R (b * a) ∩ {r : R | IsUnit r}ᶜ
⊢ quasispectrum R (a * b) ∩ {r : R | IsUnit r} ∪ quasispectrum R (a * b) ∩ {r : R | IsUnit r}ᶜ =
    quasispectrum R (b * a) ∩ {r : R | IsUnit r} ∪ quasispectrum R (b * a) ∩ {r : R | IsUnit r}ᶜ

Tactic:
congr! 1
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a b : A
⊢ quasispectrum R (a * b) ∩ {r : R | IsUnit r} = quasispectrum R (b * a) ∩ {r : R | IsUnit r}

Tactic:
simpa [Set.inter_comm _ {r | IsUnit r}, Unitization.quasispectrum_eq_spectrum_inr,
      Unitization.inr_mul] using spectrum.setOf_isUnit_inter_mul_comm _ _

Premises used: setOf, IsUnit, Unitization.inr_mul, Set.inter_comm, spectrum.setOf_isUnit_inter_mul_comm, Unitization.quasispectrum_eq_spectrum_inr
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a b : A
h : {r : R | IsUnit r}ᶜ ⊆ quasispectrum R (b * a)
h₁ : {r : R | IsUnit r}ᶜ ⊆ quasispectrum R (a * b)
⊢ quasispectrum R (a * b) ∩ {r : R | IsUnit r}ᶜ = quasispectrum R (b * a) ∩ {r : R | IsUnit r}ᶜ

Tactic:
rw [Set.inter_eq_right.mpr, Set.inter_eq_right.mpr]

Premises used: Iff.mpr, Set.inter_eq_right
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a b : A
⊢ {r : R | IsUnit r}ᶜ ⊆ quasispectrum R (b * a)

Tactic:
fun _ ↦ quasispectrum.not_isUnit_mem _

Premises used: HMul.hMul, Set.Mem, setOf, IsUnit, Set.Subset, quasispectrum.not_isUnit_mem, Not
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a b : A
⊢ {r : R | IsUnit r}ᶜ ⊆ quasispectrum R (b * a)

Tactic:
exact fun _ ↦ quasispectrum.not_isUnit_mem _

Premises used: quasispectrum.not_isUnit_mem
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a b : A
⊢ {r : R | IsUnit r}ᶜ ⊆ quasispectrum R (a * b)

Tactic:
fun _ ↦ quasispectrum.not_isUnit_mem _

Premises used: HMul.hMul, Set.Mem, setOf, IsUnit, Set.Subset, quasispectrum.not_isUnit_mem, Not
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a b : A
⊢ {r : R | IsUnit r}ᶜ ⊆ quasispectrum R (a * b)

Tactic:
exact fun _ ↦ quasispectrum.not_isUnit_mem _

Premises used: quasispectrum.not_isUnit_mem
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
𝕜 : Type u_3
A : Type u_4
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : Ring A
inst_3 : PartialOrder A
inst_4 : Algebra 𝕜 A
⊢ NonnegSpectrumClass 𝕜 A ↔ ∀ (a : A), 0 ≤ a → ∀ x ∈ spectrum 𝕜 a, 0 ≤ x

Tactic:
simp [show NonnegSpectrumClass 𝕜 A ↔ _ from ⟨fun ⟨h⟩ ↦ h, (⟨·⟩)⟩,
    quasispectrum_eq_spectrum_union_zero]

Premises used: NonnegSpectrumClass.mk, Iff.intro, quasispectrum_eq_spectrum_union_zero
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
A : Type u_2
inst : NonUnitalRing A
𝕜 : Type u_3
inst_1 : CommSemiring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : PartialOrder A
inst_4 : Module 𝕜 A
inst_5 : NonnegSpectrumClass 𝕜 A
a : A
ha : 0 ≤ a
x : 𝕜
hx : x ∈ quasispectrum 𝕜 a
⊢ 0 ≤ x

Tactic:
quasispectrum_nonneg_of_nonneg a ha x hx

Premises used: NonnegSpectrumClass.quasispectrum_nonneg_of_nonneg
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
𝕜 : Type u_3
A : Type u_4
inst : CommSemiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Ring A
inst_3 : PartialOrder A
inst_4 : Algebra 𝕜 A
inst_5 : NonnegSpectrumClass 𝕜 A
a : A
ha : 0 ≤ a
x : 𝕜
hx : x ∈ spectrum 𝕜 a
⊢ 0 ≤ x

Tactic:
NonnegSpectrumClass.quasispectrum_nonneg_of_nonneg a ha x (spectrum_subset_quasispectrum 𝕜 a hx)

Premises used: spectrum_subset_quasispectrum, NonnegSpectrumClass.quasispectrum_nonneg_of_nonneg
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : NonUnitalRing A
inst_3 : Module R A
inst_4 : Module S A
inst_5 : Algebra R S
a : A
f : S → R
⊢ QuasispectrumRestricts a f ↔
    Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (quasispectrum S a) ∧
      Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S)

Tactic:
⟨fun ⟨h₁, h₂⟩ ↦ ⟨h₁, h₂⟩, fun ⟨h₁, h₂⟩ ↦ ⟨h₁, h₂⟩⟩

Premises used: Function.LeftInverse, Algebra.algebraMap, quasispectrum, Set.RightInvOn, QuasispectrumRestricts.mk, _private.0.quasispectrumRestricts_iff.match_1, And, QuasispectrumRestricts, And.intro, Iff.intro, _private.0.quasispectrumRestricts_iff.match_2, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
S : Type u_3
R : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Algebra R S
inst_4 : Module S A
inst_5 : IsScalarTower S A A
inst_6 : SMulCommClass S A A
inst_7 : Module R A
inst_8 : IsScalarTower R S A
a : A
r : R
simp_rw :
  Membership.mem (α := S) (spectrum S (A := Unitization S A) (↑a : Unitization S A))
      ((algebraMap R S : (a : R) → S) r : S) ↔
    r ∈ spectrum R (A := Unitization S A) (↑a : Unitization S A)
⊢ Membership.mem (α := S) (quasispectrum S a) ((algebraMap R S : (a : R) → S) r : S) ↔ r ∈ quasispectrum R a

Tactic:
simp_rw [Unitization.quasispectrum_eq_spectrum_inr' _ S a, spectrum.algebraMap_mem_iff]

Premises used: spectrum.algebraMap_mem_iff, Unitization.quasispectrum_eq_spectrum_inr'
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
S : Type u_3
R : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Algebra R S
inst_4 : Module S A
inst_5 : IsScalarTower S A A
inst_6 : SMulCommClass S A A
inst_7 : Module R A
inst_8 : IsScalarTower R S A
a : A
⊢ (⇑(algebraMap R S) : (a : R) → S) ⁻¹' quasispectrum S a = quasispectrum R a

Tactic:
Set.ext fun _ => quasispectrum.algebraMap_mem_iff _

Premises used: Set.ext, quasispectrum.algebraMap_mem_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Module R A
inst_4 : Module S A
inst_5 : Algebra R S
a : A
f : S → R
h : QuasispectrumRestricts a f
rw : f 0 = f ((algebraMap R S : (a : R) → S) 0)
rw₁ rw₂ : f 0 = f 0
⊢ f 0 = 0

Tactic:
rw [← h.left_inv 0, map_zero (algebraMap R S)]

Premises used: Algebra.algebraMap, map_zero, OfNat.ofNat, QuasispectrumRestricts.left_inv
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Module R A
inst_4 : Module S A
inst_5 : Algebra R S
a : A
f : S → R
hf : Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S)
h : quasispectrum S a ⊆ Set.range.{u_4, u_3 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S)
s : S
hs : s ∈ quasispectrum S a
obtain :
  ∀ (r : R) (hs : Membership.mem (α := S) (quasispectrum S a) ((algebraMap R S : (a : R) → S) r : S)),
    Eq.{u_4 + 1} (α := S) ((algebraMap R S : (a : R) → S) (f ((algebraMap R S : (a : R) → S) r)) : S)
      ((algebraMap R S : (a : R) → S) r : S)
⊢ (algebraMap R S : (a : R) → S) (f s) = s

Tactic:
obtain ⟨r, rfl⟩ := h hs

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Module R A
inst_4 : Module S A
inst_5 : Algebra R S
a : A
f : S → R
hf : Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S)
h : quasispectrum S a ⊆ Set.range.{u_4, u_3 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S)
r : R
hs : Membership.mem (α := S) (quasispectrum S a) ((algebraMap R S : (a : R) → S) r : S)
rw rw₁ : Eq.{u_4 + 1} (α := S) ((algebraMap R S : (a : R) → S) r : S) ((algebraMap R S : (a : R) → S) r : S)
⊢ Eq.{u_4 + 1} (α := S) ((algebraMap R S : (a : R) → S) (f ((algebraMap R S : (a : R) → S) r)) : S)
    ((algebraMap R S : (a : R) → S) r : S)

Tactic:
rw [hf r]
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Module R A
inst_4 : Module S A
inst_5 : Algebra R S
inst_6 : IsScalarTower S A A
inst_7 : SMulCommClass S A A
f : S → R
a b : A
⊢ QuasispectrumRestricts (a * b) f ↔ QuasispectrumRestricts (b * a) f

Tactic:
simp only [quasispectrumRestricts_iff, quasispectrum.mul_comm]

Premises used: quasispectrumRestricts_iff, quasispectrum.mul_comm
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Module R A
inst_4 : Module S A
inst_5 : Algebra R S
a : A
f : S → R
inst_6 : IsScalarTower S A A
inst_7 : SMulCommClass S A A
inst_8 : IsScalarTower R S A
h : QuasispectrumRestricts a f
⊢ (⇑(algebraMap R S) : (a : R) → S) '' quasispectrum R a = quasispectrum S a

Tactic:
Set.eq_of_subset_of_subset ?_ fun s hs => ⟨f s, ?_⟩

Premises used: Exists.intro, Set.eq_of_subset_of_subset
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Module R A
inst_4 : Module S A
inst_5 : Algebra R S
a : A
f : S → R
inst_6 : IsScalarTower S A A
inst_7 : SMulCommClass S A A
inst_8 : IsScalarTower R S A
h : QuasispectrumRestricts a f
refine_1 : (⇑(algebraMap R S) : (a : R) → S) '' quasispectrum R a ⊆ quasispectrum S a
refine_2 : ∀ (s : S) (hs : s ∈ quasispectrum S a), f s ∈ quasispectrum R a ∧ (algebraMap R S : (a : R) → S) (f s) = s
⊢ (⇑(algebraMap R S) : (a : R) → S) '' quasispectrum R a = quasispectrum S a

Tactic:
refine Set.eq_of_subset_of_subset ?_ fun s hs => ⟨f s, ?_⟩
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Module R A
inst_4 : Module S A
inst_5 : Algebra R S
a : A
f : S → R
inst_6 : IsScalarTower S A A
inst_7 : SMulCommClass S A A
inst_8 : IsScalarTower R S A
h : QuasispectrumRestricts a f
⊢ (⇑(algebraMap R S) : (a : R) → S) '' quasispectrum R a ⊆ quasispectrum S a

Tactic:
simpa only [quasispectrum.preimage_algebraMap] using
      (quasispectrum S a).image_preimage_subset (algebraMap R S)

Premises used: Algebra.algebraMap, quasispectrum, Set.image_preimage_subset, quasispectrum.preimage_algebraMap, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Module R A
inst_4 : Module S A
inst_5 : Algebra R S
a : A
f : S → R
inst_6 : IsScalarTower S A A
inst_7 : SMulCommClass S A A
inst_8 : IsScalarTower R S A
h : QuasispectrumRestricts a f
s : S
hs : s ∈ quasispectrum S a
⊢ f s ∈ quasispectrum R a ∧ (algebraMap R S : (a : R) → S) (f s) = s

Tactic:
⟨quasispectrum.of_algebraMap_mem S ((h.rightInvOn hs).symm ▸ hs), h.rightInvOn hs⟩

Premises used: quasispectrum.of_algebraMap_mem, QuasispectrumRestricts.rightInvOn, And.intro
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Module R A
inst_4 : Module S A
inst_5 : Algebra R S
a : A
f : S → R
inst_6 : IsScalarTower S A A
inst_7 : SMulCommClass S A A
inst_8 : IsScalarTower R S A
h : QuasispectrumRestricts a f
s : S
hs : s ∈ quasispectrum S a
⊢ f s ∈ quasispectrum R a ∧ (algebraMap R S : (a : R) → S) (f s) = s

Tactic:
exact ⟨quasispectrum.of_algebraMap_mem S ((h.rightInvOn hs).symm ▸ hs), h.rightInvOn hs⟩
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Module R A
inst_4 : Module S A
inst_5 : Algebra R S
a : A
f : S → R
inst_6 : IsScalarTower S A A
inst_7 : SMulCommClass S A A
inst_8 : IsScalarTower R S A
h : QuasispectrumRestricts a f
⊢ f '' quasispectrum S a = quasispectrum R a

Tactic:
simp only [← h.algebraMap_image, Set.image_image, h.left_inv _, Set.image_id']

Premises used: Set.image_image, Set.image_id', QuasispectrumRestricts.algebraMap_image, QuasispectrumRestricts.left_inv
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Module R A
inst_4 : Module S A
inst_5 : Algebra R S
a : A
f : S → R
inst_6 : IsScalarTower S A A
inst_7 : SMulCommClass S A A
inst_8 : IsScalarTower R S A
h : QuasispectrumRestricts a f
s : S
hs : s ∈ quasispectrum S a
⊢ f s ∈ quasispectrum R a

Tactic:
h.image ▸ ⟨s, hs, rfl⟩

Premises used: Eq.rec, And.intro, QuasispectrumRestricts.image, Exists.intro, rfl
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Module R A
inst_4 : Module S A
inst_5 : Algebra R S
a : A
f : S → R
inst_6 : IsScalarTower S A A
inst_7 : SMulCommClass S A A
inst_8 : IsScalarTower R S A
h : QuasispectrumRestricts a f
⊢ quasispectrum S a ⊆ f ⁻¹' quasispectrum R a

Tactic:
h.image ▸ (quasispectrum S a).subset_preimage_image f

Premises used: quasispectrum, Eq.rec, QuasispectrumRestricts.image, Set.subset_preimage_image
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R₁ : Type u_6
R₂ : Type u_7
R₃ : Type u_8
A : Type u_9
inst : Semifield R₁
inst_1 : Field R₂
inst_2 : Field R₃
inst_3 : NonUnitalRing A
inst_4 : Module R₁ A
inst_5 : Module R₂ A
inst_6 : Module R₃ A
inst_7 : Algebra R₁ R₂
inst_8 : Algebra R₂ R₃
inst_9 : Algebra R₁ R₃
inst_10 : IsScalarTower R₁ R₂ R₃
inst_11 : IsScalarTower R₂ R₃ A
inst_12 : IsScalarTower R₃ A A
inst_13 : SMulCommClass R₃ A A
a : A
f : R₃ → R₂
g : R₂ → R₁
e : R₃ → R₁
hfge : g ∘ f = e
hf : QuasispectrumRestricts a f
hg : QuasispectrumRestricts a g
h :
  Eq (α := R₁ → R₃) (⇑(algebraMap R₁ R₃) : (a : R₁) → R₃)
    (Function.comp.{u_6 + 1, u_7 + 1, u_8 + 1} (β := R₂) (⇑(algebraMap R₂ R₃) : (a : R₂) → R₃)
      (⇑(algebraMap R₁ R₂) : (a : R₁) → R₂))
⊢ Set.RightInvOn e (⇑(algebraMap R₁ R₃) : (a : R₁) → R₃) (quasispectrum R₃ a)

Tactic:
convert! hfge ▸ hg.rightInvOn.comp hf.rightInvOn fun _ ↦ hf.apply_mem
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R₁ : Type u_6
R₂ : Type u_7
R₃ : Type u_8
A : Type u_9
inst : Semifield R₁
inst_1 : Field R₂
inst_2 : Field R₃
inst_3 : NonUnitalRing A
inst_4 : Module R₁ A
inst_5 : Module R₂ A
inst_6 : Module R₃ A
inst_7 : Algebra R₁ R₂
inst_8 : Algebra R₂ R₃
inst_9 : Algebra R₁ R₃
inst_10 : IsScalarTower R₁ R₂ R₃
inst_11 : IsScalarTower R₂ R₃ A
inst_12 : IsScalarTower R₃ A A
inst_13 : SMulCommClass R₃ A A
a : A
f : R₃ → R₂
g : R₂ → R₁
e : R₃ → R₁
hfge : g ∘ f = e
hf : QuasispectrumRestricts a f
hg : QuasispectrumRestricts a g
⊢ Eq (α := R₁ → R₃) (⇑(algebraMap R₁ R₃) : (a : R₁) → R₃)
    (Function.comp.{u_6 + 1, u_7 + 1, u_8 + 1} (β := R₂) (⇑(algebraMap R₂ R₃) : (a : R₂) → R₃)
      (⇑(algebraMap R₁ R₂) : (a : R₁) → R₂))

Tactic:
congrm (⇑$(IsScalarTower.algebraMap_eq R₁ R₂ R₃))
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R₁ : Type u_6
R₂ : Type u_7
R₃ : Type u_8
A : Type u_9
inst : Semifield R₁
inst_1 : Field R₂
inst_2 : Field R₃
inst_3 : NonUnitalRing A
inst_4 : Module R₁ A
inst_5 : Module R₂ A
inst_6 : Module R₃ A
inst_7 : Algebra R₁ R₂
inst_8 : Algebra R₂ R₃
inst_9 : Algebra R₁ R₃
inst_10 : IsScalarTower R₁ R₂ R₃
inst_11 : IsScalarTower R₂ R₃ A
inst_12 : IsScalarTower R₃ A A
inst_13 : SMulCommClass R₃ A A
a : A
f : R₃ → R₂
g : R₂ → R₁
e : R₃ → R₁
hfge : g ∘ f = e
hf : QuasispectrumRestricts a f
hg : QuasispectrumRestricts a g
h :
  Eq (α := R₁ → R₃) (⇑(algebraMap R₁ R₃) : (a : R₁) → R₃)
    (Function.comp.{u_6 + 1, u_7 + 1, u_8 + 1} (β := R₂) (⇑(algebraMap R₂ R₃) : (a : R₂) → R₃)
      (⇑(algebraMap R₁ R₂) : (a : R₁) → R₂))
⊢ Function.LeftInverse e (⇑(algebraMap R₁ R₃) : (a : R₁) → R₃)

Tactic:
convert! hfge ▸ hf.left_inv.comp hg.left_inv
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
a : A
f : S → R
h : SpectrumRestricts a f
⊢ Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (spectrum S a)

Tactic:
(QuasispectrumRestricts.rightInvOn h).mono <| spectrum_subset_quasispectrum _ _

Premises used: spectrum_subset_quasispectrum, QuasispectrumRestricts.rightInvOn, Set.RightInvOn.mono
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
a : A
f : S → R
h₁ : Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S)
h₂ : Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (spectrum S a)
x : S
hx : x ∈ quasispectrum S a
inl : ∀ (hx : 0 ∈ quasispectrum S a), Eq.{u_4 + 1} (α := S) ((algebraMap R S : (a : R) → S) (f 0) : S) (0 : S)
inr : ∀ (hx : x ∈ spectrum S a), (algebraMap R S : (a : R) → S) (f x) = x
⊢ (algebraMap R S : (a : R) → S) (f x) = x

Tactic:
obtain (rfl | hx) := mem_quasispectrum_iff.mp hx

Premises used: mem_quasispectrum_iff, Iff.mp, rfl
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
a : A
f : S → R
h₁ : Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S)
h₂ : Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (spectrum S a)
hx : 0 ∈ quasispectrum S a
⊢ Eq.{u_4 + 1} (α := S) ((algebraMap R S : (a : R) → S) (f 0) : S) (0 : S)

Tactic:
simpa using h₁ 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
a : A
f : S → R
h₁ : Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S)
h₂ : Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (spectrum S a)
x : S
hx_1 : x ∈ quasispectrum S a
hx : x ∈ spectrum S a
⊢ (algebraMap R S : (a : R) → S) (f x) = x

Tactic:
h₂ hx
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
a : A
f : S → R
h₁ : Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S)
h₂ : Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (spectrum S a)
x : S
hx_1 : x ∈ quasispectrum S a
hx : x ∈ spectrum S a
⊢ (algebraMap R S : (a : R) → S) (f x) = x

Tactic:
exact h₂ hx