awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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))
⊢ ¬IsQuasiregular (-(x.unit⁻¹ • a)) ↔
    ¬IsQuasiregular (-HSMul.hSMul (β := Unitization S A) x.unit⁻¹ (↑a : Unitization S A))
have rw₃ : IsQuasiregular (-((↑x.unit⁻¹ : R) • a)) ↔
  IsQuasiregular (R := Unitization S A) (-(↑((↑x.unit⁻¹ : R) • a) : Unitization S A))
Tactic: rw [not_iff_not, Units.smul_def, Units.smul_def, ← inr_smul, ← inr_neg, isQuasiregular_inr_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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))
⊢ ¬IsQuasiregular (-(x.unit⁻¹ • a)) ↔
    ¬IsQuasiregular (-HSMul.hSMul (β := Unitization S A) x.unit⁻¹ (↑a : Unitization S A))
have rw₄ : IsQuasiregular (-((↑x.unit⁻¹ : R) • a)) ↔
  IsQuasiregular (R := Unitization S A) (↑(-((↑x.unit⁻¹ : R) • a)) : Unitization S A)
Tactic: rw [not_iff_not, Units.smul_def, Units.smul_def, ← inr_smul, ← inr_neg, isQuasiregular_inr_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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)
⊢ ¬IsQuasiregular (-(x.unit⁻¹ • a)) ↔
    ¬IsQuasiregular (-HSMul.hSMul (β := Unitization S A) x.unit⁻¹ (↑a : Unitization S A))
have rw₅ : IsQuasiregular (-((↑x.unit⁻¹ : R) • a)) ↔ IsQuasiregular (-((↑x.unit⁻¹ : R) • a))
Tactic: rw [not_iff_not, Units.smul_def, Units.smul_def, ← inr_smul, ← inr_neg, isQuasiregular_inr_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
⊢ quasispectrum R (A := Unitization S A) (↑a : Unitization S A) = quasispectrum R a
have rw : spectrum R (A := Unitization S A) (↑a : Unitization S A) ∪ {0} =
  spectrum R (A := Unitization S A) (↑a : Unitization S A)
Tactic: rw [quasispectrum_eq_spectrum_union_zero, quasispectrum_eq_spectrum_inr' R S]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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) = quasispectrum R (b * a)
have 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}ᶜ
Tactic: rw [← Set.inter_union_compl (quasispectrum R (a * b)) {r | IsUnit r},
    ← Set.inter_union_compl (quasispectrum R (b * a)) {r | IsUnit r}]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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 (a * b) ∩ {r : R | IsUnit r}ᶜ =
    quasispectrum R (b * a) ∩ {r : R | IsUnit r} ∪ quasispectrum R (b * a) ∩ {r : R | IsUnit r}ᶜ
have h : quasispectrum R (a * b) ∩ {r : R | IsUnit r} = quasispectrum R (b * a) ∩ {r : R | IsUnit r}
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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}
⊢ 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}ᶜ
have h₁ : quasispectrum R (a * b) ∩ {r : R | IsUnit r}ᶜ = quasispectrum R (b * a) ∩ {r : R | IsUnit r}ᶜ
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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}ᶜ
have h : {r : R | IsUnit r}ᶜ ⊆ quasispectrum R (b * a)
Tactic: rw [Set.inter_eq_right.mpr, Set.inter_eq_right.mpr]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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)
⊢ quasispectrum R (a * b) ∩ {r : R | IsUnit r}ᶜ = quasispectrum R (b * a) ∩ {r : R | IsUnit r}ᶜ
have h₁ : {r : R | IsUnit r}ᶜ ⊆ quasispectrum R (a * b)
Tactic: rw [Set.inter_eq_right.mpr, Set.inter_eq_right.mpr]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
⊢ Membership.mem (α := S) (quasispectrum S a) ((algebraMap R S : (a : R) → S) r : S) ↔ r ∈ quasispectrum R a
have 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)
Tactic: simp_rw [Unitization.quasispectrum_eq_spectrum_inr' _ S a, spectrum.algebraMap_mem_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
⊢ f 0 = 0
have rw : f 0 = f ((algebraMap R S : (a : R) → S) 0)
Tactic: rw [← h.left_inv 0, map_zero (algebraMap R S)]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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)
⊢ f 0 = 0
have rw₁ : f 0 = f 0
Tactic: rw [← h.left_inv 0, map_zero (algebraMap R S)]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
⊢ (algebraMap R S : (a : R) → S) (f s) = s
have 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)
Tactic: obtain ⟨r, rfl⟩ := h hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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)
⊢ 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)
have rw : Eq.{u_4 + 1} (α := S) ((algebraMap R S : (a : R) → S) r : S) ((algebraMap R S : (a : R) → S) r : S)
Tactic: rw [hf r]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
have refine_1 : (⇑(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, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
⊢ (⇑(algebraMap R S) : (a : R) → S) '' quasispectrum R a = quasispectrum S a
have refine_2 : ∀ (s : S) (hs : s ∈ quasispectrum S a), f s ∈ quasispectrum R a ∧ (algebraMap R S : (a : R) → S) (f s) = s
Tactic: refine Set.eq_of_subset_of_subset ?_ fun s hs => ⟨f s, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
⊢ Set.RightInvOn e (⇑(algebraMap R₁ R₃) : (a : R₁) → R₃) (quasispectrum R₃ a)
have 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₂))
Tactic: convert! hfge ▸ hg.rightInvOn.comp hf.rightInvOn fun _ ↦ hf.apply_mem
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
⊢ Function.LeftInverse e (⇑(algebraMap R₁ R₃) : (a : R₁) → R₃)
have 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₂))
Tactic: convert! hfge ▸ hf.left_inv.comp hg.left_inv
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
⊢ (algebraMap R S : (a : R) → S) (f x) = x
have inl : ∀ (hx : 0 ∈ quasispectrum S a), Eq.{u_4 + 1} (α := S) ((algebraMap R S : (a : R) → S) (f 0) : S) (0 : S)
Tactic: obtain (rfl | hx) := mem_quasispectrum_iff.mp hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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)
⊢ (algebraMap R S : (a : R) → S) (f x) = x
have inr : ∀ (hx : x ∈ spectrum S a), (algebraMap R S : (a : R) → S) (f x) = x
Tactic: obtain (rfl | hx) := mem_quasispectrum_iff.mp hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (hypothesis)
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
hf : Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S)
h : spectrum S a ⊆ Set.range.{u_4, u_3 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S)
s : S
hs : s ∈ quasispectrum S a
⊢ (algebraMap R S : (a : R) → S) (f s) = s
have hs₁ : s = 0 ∨ s ∈ spectrum S a
Tactic: rw [mem_quasispectrum_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
hf : Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S)
h : spectrum S a ⊆ Set.range.{u_4, u_3 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S)
s : S
hs : s = 0 ∨ s ∈ spectrum S a
⊢ (algebraMap R S : (a : R) → S) (f s) = s
have inl : Eq.{u_4 + 1} (α := S) ((algebraMap R S : (a : R) → S) (f 0) : S) (0 : S)
Tactic: obtain (rfl | hs) := hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
hf : Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S)
h : spectrum S a ⊆ Set.range.{u_4, u_3 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S)
s : S
hs : s = 0 ∨ s ∈ spectrum S a
inl : Eq.{u_4 + 1} (α := S) ((algebraMap R S : (a : R) → S) (f 0) : S) (0 : S)
⊢ (algebraMap R S : (a : R) → S) (f s) = s
have inr : ∀ (hs : s ∈ spectrum S a), (algebraMap R S : (a : R) → S) (f s) = s
Tactic: obtain (rfl | hs) := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
hf : Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S)
h : spectrum S a ⊆ Set.range.{u_4, u_3 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S)
s : S
hs : s ∈ spectrum S a
⊢ (algebraMap R S : (a : R) → S) (f s) = s
have inr : ∀ (r : R) (hs : Membership.mem (α := S) (spectrum 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)
Tactic: obtain ⟨r, rfl⟩ := h hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
hf : Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S)
h : spectrum S a ⊆ Set.range.{u_4, u_3 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S)
r : R
hs : Membership.mem (α := S) (spectrum 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)
have inr : Eq.{u_4 + 1} (α := S) ((algebraMap R S : (a : R) → S) r : S) ((algebraMap R S : (a : R) → S) r : S)
Tactic: rw [hf r]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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 b : A
f : S → R
ha : SpectrumRestricts a f
h : spectrum S a = spectrum S b
⊢ Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (quasispectrum S b)
have rw : Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (quasispectrum S a)
Tactic: rw [quasispectrum_eq_spectrum_union_zero, ← h, ← quasispectrum_eq_spectrum_union_zero]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
inst_6 : IsScalarTower R S A
h : SpectrumRestricts a f
⊢ (⇑(algebraMap R S) : (a : R) → S) '' spectrum R a = spectrum S a
have refine_1 : (⇑(algebraMap R S) : (a : R) → S) '' spectrum R a ⊆ spectrum S a
Tactic: refine Set.eq_of_subset_of_subset ?_ fun s hs => ⟨f s, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
inst_6 : IsScalarTower R S A
h : SpectrumRestricts a f
refine_1 : (⇑(algebraMap R S) : (a : R) → S) '' spectrum R a ⊆ spectrum S a
⊢ (⇑(algebraMap R S) : (a : R) → S) '' spectrum R a = spectrum S a
have refine_2 : ∀ (s : S) (hs : s ∈ spectrum S a), f s ∈ spectrum R a ∧ (algebraMap R S : (a : R) → S) (f s) = s
Tactic: refine Set.eq_of_subset_of_subset ?_ fun s hs => ⟨f s, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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 R A
inst_5 : Module S A
inst_6 : IsScalarTower S A A
inst_7 : SMulCommClass S A A
inst_8 : IsScalarTower R S A
a : A
f : S → R
⊢ QuasispectrumRestricts a f ↔ SpectrumRestricts (A := Unitization S A) (↑a : Unitization S A) f
have rw : Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (quasispectrum S a) ∧
    Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S) ↔
  SpectrumRestricts (A := Unitization S A) (↑a : Unitization S A) f
Tactic: rw [quasispectrumRestricts_iff, spectrumRestricts_iff,
    ← Unitization.quasispectrum_eq_spectrum_inr']
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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 R A
inst_5 : Module S A
inst_6 : IsScalarTower S A A
inst_7 : SMulCommClass S A A
inst_8 : IsScalarTower R S A
a : A
f : S → R
rw :
  Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (quasispectrum S a) ∧
      Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S) ↔
    SpectrumRestricts (A := Unitization S A) (↑a : Unitization S A) f
⊢ QuasispectrumRestricts a f ↔ SpectrumRestricts (A := Unitization S A) (↑a : Unitization S A) f
have rw₁ : Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (quasispectrum S a) ∧
    Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S) ↔
  Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (spectrum S (A := Unitization S A) (↑a : Unitization S A)) ∧
    Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S)
Tactic: rw [quasispectrumRestricts_iff, spectrumRestricts_iff,
    ← Unitization.quasispectrum_eq_spectrum_inr']
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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 R A
inst_5 : Module S A
inst_6 : IsScalarTower S A A
inst_7 : SMulCommClass S A A
inst_8 : IsScalarTower R S A
a : A
f : S → R
rw :
  Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (quasispectrum S a) ∧
      Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S) ↔
    SpectrumRestricts (A := Unitization S A) (↑a : Unitization S A) f
rw₁ :
  Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (quasispectrum S a) ∧
      Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S) ↔
    Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (spectrum S (A := Unitization S A) (↑a : Unitization S A)) ∧
      Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S)
⊢ QuasispectrumRestricts a f ↔ SpectrumRestricts (A := Unitization S A) (↑a : Unitization S A) f
have rw₂ : Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (quasispectrum S a) ∧
    Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S) ↔
  Set.RightInvOn f (⇑(algebraMap R S) : (a : R) → S) (quasispectrum S a) ∧
    Function.LeftInverse f (⇑(algebraMap R S) : (a : R) → S)
Tactic: rw [quasispectrumRestricts_iff, spectrumRestricts_iff,
    ← Unitization.quasispectrum_eq_spectrum_inr']
-- Lean 4 proof step from Mathlib.Algebra.Algebra.StrictPositivity (goal)
Goal:
A : Type u_1
inst : Semiring A
inst_1 : StarRing A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
u a : A
hu : IsUnit u
⊢ IsStrictlyPositive (u * a * star u) ↔ IsStrictlyPositive a
have simp_rw : 0 ≤ a ∧ IsUnit (u * a * star u) ↔ 0 ≤ a ∧ IsUnit a
Tactic: simp_rw [IsStrictlyPositive.iff_of_unital, hu.star_right_conjugate_nonneg_iff]