awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : InvolutiveStar R
inst_4 : StarRing A
inst_5 : StarModule R A
r : R
a : A
⊢ star r ∈ resolventSet R a ↔ r ∈ resolventSet R (star a)
have refine_1 : ∀ (h : star r ∈ resolventSet R a), r ∈ resolventSet R (star a)
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : InvolutiveStar R
inst_4 : StarRing A
inst_5 : StarModule R A
r : R
a : A
refine_1 : ∀ (h : star r ∈ resolventSet R a), r ∈ resolventSet R (star a)
⊢ star r ∈ resolventSet R a ↔ r ∈ resolventSet R (star a)
have refine_2 : ∀ (h : r ∈ resolventSet R (star a)), star r ∈ resolventSet R a
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : InvolutiveStar R
inst_4 : StarRing A
inst_5 : StarModule R A
a : A
⊢ σ (star a) = star (σ a)
have h : ∀ (x : R), x ∈ σ (star a) ↔ x ∈ star (σ a)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r x : R
⊢ x ∈ {r} + σ a ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
have rw : Membership.mem (γ := Set R) ((fun (x : R) ↦ r + x) '' σ a) x ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
Tactic: rw [singleton_add, image_add_left, mem_preimage, add_comm, add_mem_iff, map_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r x : R
rw :
  Membership.mem (γ := Set R) ((fun (x : R) ↦ r + x) '' σ a) x ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
⊢ x ∈ {r} + σ a ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
have rw₁ : Membership.mem (γ := Set R) ((fun (x : R) ↦ -r + x) ⁻¹' σ a) x ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
Tactic: rw [singleton_add, image_add_left, mem_preimage, add_comm, add_mem_iff, map_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r x : R
rw :
  Membership.mem (γ := Set R) ((fun (x : R) ↦ r + x) '' σ a) x ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₁ :
  Membership.mem (γ := Set R) ((fun (x : R) ↦ -r + x) ⁻¹' σ a) x ↔
    x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
⊢ x ∈ {r} + σ a ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
have rw₂ : -r + x ∈ σ a ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
Tactic: rw [singleton_add, image_add_left, mem_preimage, add_comm, add_mem_iff, map_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r x : R
rw :
  Membership.mem (γ := Set R) ((fun (x : R) ↦ r + x) '' σ a) x ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₁ :
  Membership.mem (γ := Set R) ((fun (x : R) ↦ -r + x) ⁻¹' σ a) x ↔
    x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₂ : -r + x ∈ σ a ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
⊢ x ∈ {r} + σ a ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
have rw₃ : x + -r ∈ σ a ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
Tactic: rw [singleton_add, image_add_left, mem_preimage, add_comm, add_mem_iff, map_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r x : R
rw :
  Membership.mem (γ := Set R) ((fun (x : R) ↦ r + x) '' σ a) x ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₁ :
  Membership.mem (γ := Set R) ((fun (x : R) ↦ -r + x) ⁻¹' σ a) x ↔
    x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₂ : -r + x ∈ σ a ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₃ : x + -r ∈ σ a ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
⊢ x ∈ {r} + σ a ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
have rw₄ : x ∈ σ (HAdd.hAdd (α := A) (-(↑ₐ : (a : R) → A) (-r) : A) a) ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
Tactic: rw [singleton_add, image_add_left, mem_preimage, add_comm, add_mem_iff, map_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r x : R
rw :
  Membership.mem (γ := Set R) ((fun (x : R) ↦ r + x) '' σ a) x ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₁ :
  Membership.mem (γ := Set R) ((fun (x : R) ↦ -r + x) ⁻¹' σ a) x ↔
    x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₂ : -r + x ∈ σ a ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₃ : x + -r ∈ σ a ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₄ :
  x ∈ σ (HAdd.hAdd (α := A) (-(↑ₐ : (a : R) → A) (-r) : A) a) ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
⊢ x ∈ {r} + σ a ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
have rw₅ : x ∈ σ (HAdd.hAdd (α := A) (- -(↑ₐ : (a : R) → A) r : A) a) ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
Tactic: rw [singleton_add, image_add_left, mem_preimage, add_comm, add_mem_iff, map_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r x : R
rw :
  Membership.mem (γ := Set R) ((fun (x : R) ↦ r + x) '' σ a) x ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₁ :
  Membership.mem (γ := Set R) ((fun (x : R) ↦ -r + x) ⁻¹' σ a) x ↔
    x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₂ : -r + x ∈ σ a ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₃ : x + -r ∈ σ a ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₄ :
  x ∈ σ (HAdd.hAdd (α := A) (-(↑ₐ : (a : R) → A) (-r) : A) a) ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₅ :
  x ∈ σ (HAdd.hAdd (α := A) (- -(↑ₐ : (a : R) → A) r : A) a) ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
⊢ x ∈ {r} + σ a ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
have rw₆ : x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a) ↔ x ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) a)
Tactic: rw [singleton_add, image_add_left, mem_preimage, add_comm, add_mem_iff, map_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
⊢ -σ a = σ (-a)
have rw : -(resolventSet R a)ᶜ = σ (-a)
Tactic: rw [spectrum, Set.compl_neg, spectrum, resolventSet_neg]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
rw : -(resolventSet R a)ᶜ = σ (-a)
⊢ -σ a = σ (-a)
have rw₁ : (-resolventSet R a)ᶜ = σ (-a)
Tactic: rw [spectrum, Set.compl_neg, spectrum, resolventSet_neg]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
rw : -(resolventSet R a)ᶜ = σ (-a)
rw₁ : (-resolventSet R a)ᶜ = σ (-a)
⊢ -σ a = σ (-a)
have rw₂ : (-resolventSet R a)ᶜ = (resolventSet R (-a))ᶜ
Tactic: rw [spectrum, Set.compl_neg, spectrum, resolventSet_neg]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
rw : -(resolventSet R a)ᶜ = σ (-a)
rw₁ : (-resolventSet R a)ᶜ = σ (-a)
rw₂ : (-resolventSet R a)ᶜ = (resolventSet R (-a))ᶜ
⊢ -σ a = σ (-a)
have rw₃ : (-resolventSet R a)ᶜ = (-resolventSet R a)ᶜ
Tactic: rw [spectrum, Set.compl_neg, spectrum, resolventSet_neg]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r : R
⊢ {r} - σ a = σ (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)
have rw : {r} + -σ a = σ (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)
Tactic: rw [sub_eq_add_neg, neg_eq, singleton_add_eq, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r : R
rw : {r} + -σ a = σ (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)
⊢ {r} - σ a = σ (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)
have rw₁ : {r} + σ (-a) = σ (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)
Tactic: rw [sub_eq_add_neg, neg_eq, singleton_add_eq, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r : R
rw : {r} + -σ a = σ (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₁ : {r} + σ (-a) = σ (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)
⊢ {r} - σ a = σ (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)
have rw₂ : σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) (-a)) = σ (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)
Tactic: rw [sub_eq_add_neg, neg_eq, singleton_add_eq, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r : R
rw : {r} + -σ a = σ (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₁ : {r} + σ (-a) = σ (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)
rw₂ : σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) (-a)) = σ (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)
⊢ {r} - σ a = σ (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)
have rw₃ : σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) (-a)) = σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) r : A) (-a))
Tactic: rw [sub_eq_add_neg, neg_eq, singleton_add_eq, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : Semifield R
inst_1 : Ring A
inst_2 : Algebra R A
r : R
a : Aˣ
⊢ r⁻¹ ∈ spectrum R (↑a : A) ↔ r ∈ spectrum R (↑a⁻¹ : A)
have inl : 0⁻¹ ∈ spectrum R (↑a : A) ↔ 0 ∈ spectrum R (↑a⁻¹ : A)
Tactic: obtain (rfl | hr) := eq_or_ne r 0
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : Semifield R
inst_1 : Ring A
inst_2 : Algebra R A
r : R
a : Aˣ
inl : 0⁻¹ ∈ spectrum R (↑a : A) ↔ 0 ∈ spectrum R (↑a⁻¹ : A)
⊢ r⁻¹ ∈ spectrum R (↑a : A) ↔ r ∈ spectrum R (↑a⁻¹ : A)
have inr : ∀ (hr : r ≠ 0), r⁻¹ ∈ spectrum R (↑a : A) ↔ r ∈ spectrum R (↑a⁻¹ : A)
Tactic: obtain (rfl | hr) := eq_or_ne r 0
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u
A : Type v
inst : Semifield R
inst_1 : Ring A
inst_2 : Algebra R A
r : R
a : Aˣ
hr : r ≠ 0
⊢ r⁻¹ ∈ spectrum R (↑a : A) ↔ r ∈ spectrum R (↑a⁻¹ : A)
have inr : ∀ (r : Rˣ) (hr : (↑r : R) ≠ 0), (↑r : R)⁻¹ ∈ spectrum R (↑a : A) ↔ (↑r : R) ∈ spectrum R (↑a⁻¹ : A)
Tactic: lift r to Rˣ using hr.isUnit
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
⊢ spectrum.{u, v} 𝕜 (A := A) 0 = {0}
have refine : spectrum.{u, v} 𝕜 (A := A) 0 ⊆ {0}
Tactic: refine Set.Subset.antisymm ?_ (by simp [Algebra.algebraMap_eq_smul_one, mem_iff])
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
⊢ spectrum.{u, v} 𝕜 (A := A) 0 ⊆ {0}
have rw : {0}ᶜ ⊆ resolventSet.{u, v} 𝕜 (A := A) 0
Tactic: rw [spectrum, Set.compl_subset_comm]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (hypothesis)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
k : 𝕜
hk : Membership.mem (γ := Set 𝕜) {0}ᶜ k
⊢ k ∈ resolventSet.{u, v} 𝕜 (A := A) 0
have hk₁ : k ≠ 0
Tactic: rw [Set.mem_compl_singleton_iff] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (hypothesis)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
k : 𝕜
hk : k ≠ 0
⊢ k ∈ resolventSet.{u, v} 𝕜 (A := A) 0
have this : IsUnit (HSMul.hSMul (α := 𝕜ˣ) (β := A) (Units.mk0 k hk) 1)
Tactic: have : IsUnit (Units.mk0 k hk • (1 : A)) := IsUnit.smul (Units.mk0 k hk) isUnit_one
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
k : 𝕜
⊢ spectrum.{u, v} 𝕜 (A := A) ((↑ₐ : (a : 𝕜) → A) k : A) = {k}
have rw : σ (HAdd.hAdd (α := A) (β := A) ((↑ₐ : (a : 𝕜) → A) k : A) (0 : A)) = {k}
Tactic: rw [← add_zero (↑ₐ k), ← singleton_add_eq, zero_eq, Set.singleton_add_singleton, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
k : 𝕜
rw : σ (HAdd.hAdd (α := A) (β := A) ((↑ₐ : (a : 𝕜) → A) k : A) (0 : A)) = {k}
⊢ spectrum.{u, v} 𝕜 (A := A) ((↑ₐ : (a : 𝕜) → A) k : A) = {k}
have rw₁ : {k} + spectrum.{u, v} 𝕜 (A := A) 0 = {k}
Tactic: rw [← add_zero (↑ₐ k), ← singleton_add_eq, zero_eq, Set.singleton_add_singleton, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
k : 𝕜
rw : σ (HAdd.hAdd (α := A) (β := A) ((↑ₐ : (a : 𝕜) → A) k : A) (0 : A)) = {k}
rw₁ : {k} + spectrum.{u, v} 𝕜 (A := A) 0 = {k}
⊢ spectrum.{u, v} 𝕜 (A := A) ((↑ₐ : (a : 𝕜) → A) k : A) = {k}
have rw₂ : HAdd.hAdd (α := Set 𝕜) {k} {0} = {k}
Tactic: rw [← add_zero (↑ₐ k), ← singleton_add_eq, zero_eq, Set.singleton_add_singleton, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
k : 𝕜
rw : σ (HAdd.hAdd (α := A) (β := A) ((↑ₐ : (a : 𝕜) → A) k : A) (0 : A)) = {k}
rw₁ : {k} + spectrum.{u, v} 𝕜 (A := A) 0 = {k}
rw₂ : HAdd.hAdd (α := Set 𝕜) {k} {0} = {k}
⊢ spectrum.{u, v} 𝕜 (A := A) ((↑ₐ : (a : 𝕜) → A) k : A) = {k}
have rw₃ : Eq (α := Set 𝕜) {k + 0} {k}
Tactic: rw [← add_zero (↑ₐ k), ← singleton_add_eq, zero_eq, Set.singleton_add_singleton, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
k : 𝕜
rw : σ (HAdd.hAdd (α := A) (β := A) ((↑ₐ : (a : 𝕜) → A) k : A) (0 : A)) = {k}
rw₁ : {k} + spectrum.{u, v} 𝕜 (A := A) 0 = {k}
rw₂ : HAdd.hAdd (α := Set 𝕜) {k} {0} = {k}
rw₃ : Eq (α := Set 𝕜) {k + 0} {k}
⊢ spectrum.{u, v} 𝕜 (A := A) ((↑ₐ : (a : 𝕜) → A) k : A) = {k}
have rw₄ : Eq (α := Set 𝕜) {k} {k}
Tactic: rw [← add_zero (↑ₐ k), ← singleton_add_eq, zero_eq, Set.singleton_add_singleton, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
⊢ spectrum.{u, v} 𝕜 (A := A) 1 = spectrum.{u, v} 𝕜 (A := A) ((↑ₐ : (a : 𝕜) → A) 1 : A)
have rw : spectrum.{u, v} 𝕜 (A := A) 1 = σ (HSMul.hSMul.{u, v, v} (α := 𝕜) (β := A) 1 1)
Tactic: rw [Algebra.algebraMap_eq_smul_one, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
rw : spectrum.{u, v} 𝕜 (A := A) 1 = σ (HSMul.hSMul.{u, v, v} (α := 𝕜) (β := A) 1 1)
⊢ spectrum.{u, v} 𝕜 (A := A) 1 = spectrum.{u, v} 𝕜 (A := A) ((↑ₐ : (a : 𝕜) → A) 1 : A)
have rw₁ : spectrum.{u, v} 𝕜 (A := A) 1 = spectrum.{u, v} 𝕜 (A := A) 1
Tactic: rw [Algebra.algebraMap_eq_smul_one, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
k : 𝕜
a : A
ha : (σ a).Nonempty
⊢ σ (k • a) = k • σ a
have inl : σ (HSMul.hSMul.{u, v, v} (α := 𝕜) 0 a) = HSMul.hSMul (α := 𝕜) 0 (σ a)
Tactic: rcases eq_or_ne k 0 with (rfl | h)
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
inst_3 : Nontrivial A
k : 𝕜
a : A
ha : (σ a).Nonempty
inl : σ (HSMul.hSMul.{u, v, v} (α := 𝕜) 0 a) = HSMul.hSMul (α := 𝕜) 0 (σ a)
⊢ σ (k • a) = k • σ a
have inr : ∀ (h : k ≠ 0), σ (k • a) = k • σ a
Tactic: rcases eq_or_ne k 0 with (rfl | h)
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a b : A
⊢ σ (a * b) \ {0} = σ (b * a) \ {0}
have suffices : ∀ (x y : A), σ (x * y) \ {0} ⊆ σ (y * x) \ {0}
Tactic: suffices h : ∀ x y : A, σ (x * y) \ {0} ⊆ σ (y * x) \ {0} from
    Set.eq_of_subset_of_subset (h a b) (h b a)
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (hypothesis)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a b x y : A
k : 𝕜
k_mem : k ∈ σ (x * y)
k_ne : k ∉ {0}
⊢ k ∈ σ (y * x) \ {0}
have k_mem₁ : (↑(Units.mk0 k k_ne) : 𝕜) ∈ σ (x * y)
Tactic: change ((Units.mk0 k k_ne) : 𝕜) ∈ _ at k_mem
Cleared hypotheses: k_mem
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
𝕜 : Type u
A : Type v
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : Aˣ
⊢ (σ (↑a : A))⁻¹ = σ (↑a⁻¹ : A)
have h : ∀ (x : 𝕜), x ∈ (σ (↑a : A))⁻¹ ↔ x ∈ σ (↑a⁻¹ : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (hypothesis)
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : FunLike F A R
inst_4 : AlgHomClass F R A R
inst_5 : Nontrivial R
φ : F
a : A
⊢ Membership.mem (α := R) (σ a) ((φ : (a : A) → R) a : R)
have h : Membership.mem (γ := Ideal A) (RingHom.ker (F := A →+* R) (↑φ : A →+* R))
  (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) ((φ : (a : A) → R) a : R) : A) a)
Tactic: have h : ↑ₐ (φ a) - a ∈ RingHom.ker (φ : A →+* R) := by
    simp only [RingHom.mem_ker, map_sub, RingHom.coe_coe, AlgHomClass.commutes,
      Algebra.algebraMap_self, RingHom.id_apply, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
u : Aˣ
this : ∀ (b : A) (v : Aˣ), spectrum R ((↑v : A) * b * (↑v⁻¹ : A)) ⊆ spectrum R b
⊢ spectrum R ((↑u : A) * a * (↑u⁻¹ : A)) = spectrum R a
have refine : spectrum R a ≤ spectrum R ((↑u : A) * a * (↑u⁻¹ : A))
Tactic: refine le_antisymm (this a u) ?_
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
u : Aˣ
this : ∀ (b : A) (v : Aˣ), spectrum R ((↑v : A) * b * (↑v⁻¹ : A)) ⊆ spectrum R b
⊢ spectrum R a ≤ spectrum R ((↑u : A) * a * (↑u⁻¹ : A))
have apply : spectrum R a = spectrum R ((↑u⁻¹ : A) * ((↑u : A) * a * (↑u⁻¹ : A)) * (↑u⁻¹⁻¹ : A))
Tactic: apply le_of_eq_of_le ?_ <| this (u * a * u⁻¹) u⁻¹
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
u : Aˣ
⊢ spectrum R ((↑u : A) * a * (↑u⁻¹ : A)) = spectrum R a
have suffices : ∀ (b : A) (v : Aˣ), spectrum R ((↑v : A) * b * (↑v⁻¹ : A)) ⊆ spectrum R b
Tactic: suffices ∀ (b : A) (v : Aˣ), spectrum R (v * b * v⁻¹) ⊆ spectrum R b by
    refine le_antisymm (this a u) ?_
    apply le_of_eq_of_le ?_ <| this (u * a * u⁻¹) u⁻¹
    simp [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a_1 : A
u_1 : Aˣ
a : A
u : Aˣ
μ : R
hμ : μ ∈ spectrum R ((↑u : A) * a * (↑u⁻¹ : A))
⊢ μ ∈ spectrum R a
have hμ₁ : ¬IsUnit (HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) μ : A) ((↑u : A) * a * (↑u⁻¹ : A)))
Tactic: rw [spectrum.mem_iff] at hμ ⊢
Cleared hypotheses: hμ
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a_1 : A
u_1 : Aˣ
a : A
u : Aˣ
μ : R
hμ : ¬IsUnit (HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) μ : A) ((↑u : A) * a * (↑u⁻¹ : A)))
⊢ ¬IsUnit (HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) μ : A) a)
have contrapose : ∀ (hμ : IsUnit (HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) μ : A) a)),
  IsUnit (HSub.hSub (α := A) ((algebraMap R A : (a : R) → A) μ : A) ((↑u : A) * a * (↑u⁻¹ : A)))
Tactic: contrapose hμ
Cleared hypotheses: hμ
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
Goal:
ι : Type u_1
κ : ι → Type u_5
inst : (i : ι) → NonUnitalSemiring (κ i)
x : (i : ι) → κ i
⊢ IsQuasiregular x ↔ ∀ (i : ι), IsQuasiregular (x i)
have simp : (∀ (i : ι),
    IsUnit.{u_5} (M := PreQuasiregular (κ i))
      ((PreQuasiregular.toPi κ : (a : PreQuasiregular ((i : ι) → κ i)) → (i : ι) → PreQuasiregular (κ i))
          ((PreQuasiregular.equiv : (a : (i : ι) → κ i) → PreQuasiregular ((i : ι) → κ i)) x :
            PreQuasiregular ((i : ι) → κ i))
          i :
        PreQuasiregular (κ i))) ↔
  ∀ (i : ι),
    IsUnit (M := PreQuasiregular (κ i))
      ((PreQuasiregular.equiv : (a : κ i) → PreQuasiregular (κ i)) (x i) : PreQuasiregular (κ i))
Tactic: simp only [isQuasiregular_iff', ← isUnit_map_iff (PreQuasiregular.toPi κ), Pi.isUnit_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
Goal:
A : Type u_2
B : Type u_3
inst : NonUnitalSemiring A
inst_1 : NonUnitalSemiring B
a : A
b : B
⊢ IsQuasiregular (a, b) ↔ IsQuasiregular a ∧ IsQuasiregular b
have simp : IsUnit.{u_2} (M := PreQuasiregular A)
      ((PreQuasiregular.toProd A B : (a : PreQuasiregular (A × B)) → PreQuasiregular A × PreQuasiregular B)
          ((PreQuasiregular.equiv : (a : A × B) → PreQuasiregular (A × B)) (a, b))).1 ∧
    IsUnit.{u_3} (M := PreQuasiregular B)
      ((PreQuasiregular.toProd A B : (a : PreQuasiregular (A × B)) → PreQuasiregular A × PreQuasiregular B)
          ((PreQuasiregular.equiv : (a : A × B) → PreQuasiregular (A × B)) (a, b))).2 ↔
  IsUnit (M := PreQuasiregular A) ((PreQuasiregular.equiv : (a : A) → PreQuasiregular A) a : PreQuasiregular A) ∧
    IsUnit (M := PreQuasiregular B) ((PreQuasiregular.equiv : (a : B) → PreQuasiregular B) b : PreQuasiregular B)
Tactic: simp only [isQuasiregular_iff', ← isUnit_map_iff (PreQuasiregular.toProd A B), Prod.isUnit_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
Goal:
ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → Ring (κ i)
inst_2 : (i : ι) → Algebra.{u_4, u_5} R (κ i)
a : (i : ι) → κ i
⊢ spectrum R a = ⋃ (i : ι), spectrum R (a i)
have a₁ : (spectrum R a)ᶜ = (⋃ (i : ι), spectrum R (a i))ᶜ
Tactic: apply compl_injective
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
Goal:
ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → Ring (κ i)
inst_2 : (i : ι) → Algebra.{u_4, u_5} R (κ i)
a : (i : ι) → κ i
⊢ (spectrum R a)ᶜ = (⋃ (i : ι), spectrum R (a i))ᶜ
have a₁ : (resolventSet R a)ᶜᶜ = (⋃ (i : ι), (resolventSet R (a i))ᶜ)ᶜ
Tactic: simp_rw [spectrum, Set.compl_iUnion, compl_compl, resolventSet, Set.iInter_setOf,
    Pi.isUnit_iff, sub_apply, algebraMap_apply]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Pi (goal)
Goal:
ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → Ring (κ i)
inst_2 : (i : ι) → Algebra.{u_4, u_5} R (κ i)
a : (i : ι) → κ i
a₁ : (resolventSet R a)ᶜᶜ = (⋃ (i : ι), (resolventSet R (a i))ᶜ)ᶜ
⊢ (spectrum R a)ᶜ = (⋃ (i : ι), spectrum R (a i))ᶜ
have a₂ : (resolventSet R a)ᶜᶜ = ⋂ (i : ι), (resolventSet R (a i))ᶜᶜ
Tactic: simp_rw [spectrum, Set.compl_iUnion, compl_compl, resolventSet, Set.iInter_setOf,
    Pi.isUnit_iff, sub_apply, algebraMap_apply]