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
a : A
rw : ¬IsUnit (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) 0 : A) a) ↔ ¬IsUnit a
rw₁ : ¬IsUnit (0 - a) ↔ ¬IsUnit a
rw₂ : ¬IsUnit (-a) ↔ ¬IsUnit a
⊢ 0 ∈ σ a ↔ ¬IsUnit a
have rw₃ : ¬IsUnit a ↔ ¬IsUnit a
Tactic: rw [mem_iff, map_zero, zero_sub, IsUnit.neg_iff]
-- 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
a : A
⊢ 0 ∉ σ a ↔ IsUnit a
have rw : ¬¬IsUnit a ↔ IsUnit a
Tactic: rw [zero_mem_iff, Classical.not_not]
-- 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
a : A
rw : ¬¬IsUnit a ↔ IsUnit a
⊢ 0 ∉ σ a ↔ IsUnit a
have rw₁ : IsUnit a ↔ IsUnit a
Tactic: rw [zero_mem_iff, Classical.not_not]
-- 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 : Subsingleton A
a : A
⊢ resolventSet R a = univ
have simp_rw : Eq.{u + 1} (α := Set R) {r : R | IsUnit (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)} univ
Tactic: simp_rw [resolventSet, Subsingleton.elim (algebraMap R A _ - a) 1, isUnit_one, Set.setOf_true]
-- 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 : Subsingleton A
a : A
simp_rw : Eq.{u + 1} (α := Set R) {r : R | IsUnit (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)} univ
⊢ resolventSet R a = univ
have simp_rw₁ : Eq.{u + 1} (α := Set R) {r : R | IsUnit.{v} (M := A) 1} univ
Tactic: simp_rw [resolventSet, Subsingleton.elim (algebraMap R A _ - a) 1, isUnit_one, Set.setOf_true]
-- 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 : Subsingleton A
a : A
simp_rw : Eq.{u + 1} (α := Set R) {r : R | IsUnit (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)} univ
simp_rw₁ : Eq.{u + 1} (α := Set R) {r : R | IsUnit.{v} (M := A) 1} univ
⊢ resolventSet R a = univ
have simp_rw₂ : Eq.{u + 1} (α := Set R) {r : R | True} univ
Tactic: simp_rw [resolventSet, Subsingleton.elim (algebraMap R A _ - a) 1, isUnit_one, Set.setOf_true]
-- 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 : Subsingleton A
a : A
⊢ σ a = ∅
have rw : (resolventSet R a)ᶜ = ∅
Tactic: rw [spectrum, resolventSet_of_subsingleton, Set.compl_univ]
-- 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 : Subsingleton A
a : A
rw : (resolventSet R a)ᶜ = ∅
⊢ σ a = ∅
have rw₁ : Eq.{u + 1} (α := Set R) univᶜ ∅
Tactic: rw [spectrum, resolventSet_of_subsingleton, Set.compl_univ]
-- 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 : Subsingleton A
a : A
rw : (resolventSet R a)ᶜ = ∅
rw₁ : Eq.{u + 1} (α := Set R) univᶜ ∅
⊢ σ a = ∅
have rw₂ : Eq.{u + 1} (α := Set R) ∅ ∅
Tactic: rw [spectrum, resolventSet_of_subsingleton, Set.compl_univ]
-- 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
r : Rˣ
s : R
a : A
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
have pos : ∀ (h : s ∈ σ a), r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
Tactic: by_cases h : s ∈ spectrum R a
-- 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
r : Rˣ
s : R
a : A
pos : ∀ (h : s ∈ σ a), r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
have neg : ∀ (h : s ∉ σ a), r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
Tactic: by_cases h : s ∈ spectrum R a
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
r : Rˣ
s : R
a : A
h : s ∈ σ a
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
have h₁ : ¬IsUnit (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) a)
Tactic: rw [mem_iff] at h
Cleared hypotheses: 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
r : Rˣ
s : R
a : A
h : ¬IsUnit (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) a)
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
have pos : ∀ (h : ¬IsUnit (HSMul.hSMul (β := A) s 1 - a)),
  r • (HSMul.hSMul (β := A) s 1 - a)⁻¹ʳ = (HSMul.hSMul (β := A) (r⁻¹ • s) 1 - r⁻¹ • a)⁻¹ʳ
Tactic: simp only [resolvent, Algebra.algebraMap_eq_smul_one] at *
Cleared hypotheses: 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
r : Rˣ
s : R
a : A
h : ¬IsUnit (HSMul.hSMul (β := A) s 1 - a)
⊢ r • (HSMul.hSMul (β := A) s 1 - a)⁻¹ʳ = (HSMul.hSMul (β := A) (r⁻¹ • s) 1 - r⁻¹ • a)⁻¹ʳ
have pos : r • (HSMul.hSMul (β := A) s 1 - a)⁻¹ʳ = (r⁻¹ • (HSMul.hSMul (β := A) s 1 - a))⁻¹ʳ
Tactic: rw [smul_assoc, ← smul_sub]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (HSMul.hSMul (β := A) s 1 - a)
⊢ r • (HSMul.hSMul (β := A) s 1 - a)⁻¹ʳ = (r⁻¹ • (HSMul.hSMul (β := A) s 1 - a))⁻¹ʳ
have h' : ¬IsUnit (r⁻¹ • (HSMul.hSMul (β := A) s 1 - a))
Tactic: have h' : ¬IsUnit (r⁻¹ • (s • (1 : A) - a)) := fun hu =>
      h (by simpa only [smul_inv_smul] using IsUnit.smul r hu)
-- 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
r : Rˣ
s : R
a : A
h : s ∉ σ a
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
have neg : r • (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) a)⁻¹ʳ =
  (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) (r⁻¹ • s) : A) (r⁻¹ • a))⁻¹ʳ
Tactic: simp only [resolvent]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
r : Rˣ
s : R
a : A
h : s ∉ σ a
⊢ r • (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) a)⁻¹ʳ =
    (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) (r⁻¹ • s) : A) (r⁻¹ • a))⁻¹ʳ
have h' : IsUnit (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) (r⁻¹ • s) : A) - a)
Tactic: have h' : IsUnit (r • algebraMap R A (r⁻¹ • s) - a) := by
      simpa [Algebra.algebraMap_eq_smul_one, smul_assoc] using notMem_iff.mp 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
r : Rˣ
s : R
a : A
h : s ∉ σ a
h' : IsUnit (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) (r⁻¹ • s) : A) - a)
⊢ r • (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) a)⁻¹ʳ =
    (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) (r⁻¹ • s) : A) (r⁻¹ • a))⁻¹ʳ
have neg : r • (↑sorry.unit⁻¹ : A) = r • (↑h'.unit⁻¹ : A)
Tactic: rw [← h'.val_subInvSMul, ← (notMem_iff.mp h).unit_spec, Ring.inverse_unit, Ring.inverse_unit,
      h'.val_inv_subInvSMul]
-- 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
r : Rˣ
a : Aˣ
h : (↑r : R) ∈ resolventSet R (↑a : A)
⊢ (↑r⁻¹ : R) ∈ resolventSet R (↑a⁻¹ : A)
have rw : ∀ (h : IsUnit (HSMul.hSMul (β := A) r 1 - (↑a : A))), IsUnit (HSMul.hSMul (β := A) r⁻¹ 1 - (↑a⁻¹ : A))
Tactic: rw [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one, ← Units.smul_def] at h ⊢
Cleared hypotheses: 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
r : Rˣ
a : Aˣ
h : IsUnit (HSMul.hSMul (β := A) r 1 - (↑a : A))
⊢ IsUnit (HSMul.hSMul (β := A) r⁻¹ 1 - (↑a⁻¹ : A))
have rw : IsUnit (r • (↑a⁻¹ : A) - 1)
Tactic: rw [IsUnit.smul_sub_iff_sub_inv_smul, inv_inv, IsUnit.sub_iff]
-- 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
r : Rˣ
a : Aˣ
h : IsUnit (HSMul.hSMul (β := A) r 1 - (↑a : A))
⊢ (↑a : A) * (r • (↑a⁻¹ : A) - 1) = HSMul.hSMul (β := A) r 1 - (↑a : A)
have rw : (↑a : A) * r • (↑a⁻¹ : A) - (↑a : A) * 1 = HSMul.hSMul (β := A) r 1 - (↑a : A)
Tactic: rw [mul_sub, mul_smul_comm, a.mul_inv, mul_one]
-- 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
r : Rˣ
a : Aˣ
h : IsUnit (HSMul.hSMul (β := A) r 1 - (↑a : A))
rw : (↑a : A) * r • (↑a⁻¹ : A) - (↑a : A) * 1 = HSMul.hSMul (β := A) r 1 - (↑a : A)
⊢ (↑a : A) * (r • (↑a⁻¹ : A) - 1) = HSMul.hSMul (β := A) r 1 - (↑a : A)
have rw₁ : r • ((↑a : A) * (↑a⁻¹ : A)) - (↑a : A) * 1 = HSMul.hSMul (β := A) r 1 - (↑a : A)
Tactic: rw [mul_sub, mul_smul_comm, a.mul_inv, mul_one]
-- 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
r : Rˣ
a : Aˣ
h : IsUnit (HSMul.hSMul (β := A) r 1 - (↑a : A))
rw : (↑a : A) * r • (↑a⁻¹ : A) - (↑a : A) * 1 = HSMul.hSMul (β := A) r 1 - (↑a : A)
rw₁ : r • ((↑a : A) * (↑a⁻¹ : A)) - (↑a : A) * 1 = HSMul.hSMul (β := A) r 1 - (↑a : A)
⊢ (↑a : A) * (r • (↑a⁻¹ : A) - 1) = HSMul.hSMul (β := A) r 1 - (↑a : A)
have rw₂ : HSMul.hSMul (β := A) r 1 - (↑a : A) * 1 = HSMul.hSMul (β := A) r 1 - (↑a : A)
Tactic: rw [mul_sub, mul_smul_comm, a.mul_inv, mul_one]
-- 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
r : Rˣ
a : Aˣ
h : IsUnit (HSMul.hSMul (β := A) r 1 - (↑a : A))
rw : (↑a : A) * r • (↑a⁻¹ : A) - (↑a : A) * 1 = HSMul.hSMul (β := A) r 1 - (↑a : A)
rw₁ : r • ((↑a : A) * (↑a⁻¹ : A)) - (↑a : A) * 1 = HSMul.hSMul (β := A) r 1 - (↑a : A)
rw₂ : HSMul.hSMul (β := A) r 1 - (↑a : A) * 1 = HSMul.hSMul (β := A) r 1 - (↑a : A)
⊢ (↑a : A) * (r • (↑a⁻¹ : A) - 1) = HSMul.hSMul (β := A) r 1 - (↑a : A)
have rw₃ : HSMul.hSMul (β := A) r 1 - (↑a : A) = HSMul.hSMul (β := A) r 1 - (↑a : A)
Tactic: rw [mul_sub, mul_smul_comm, a.mul_inv, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (HSMul.hSMul (β := A) r 1 - (↑a : A))
⊢ IsUnit (r • (↑a⁻¹ : A) - 1)
have h₁ : (↑a : A) * (r • (↑a⁻¹ : A) - 1) = HSMul.hSMul (β := A) r 1 - (↑a : A)
Tactic: have h₁ : (a : A) * (r • (↑a⁻¹ : A) - 1) = r • (1 : A) - a := by
    rw [mul_sub, mul_smul_comm, a.mul_inv, mul_one]
-- 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
r : Rˣ
a : Aˣ
h : IsUnit (HSMul.hSMul (β := A) r 1 - (↑a : A))
h₁ : (↑a : A) * (r • (↑a⁻¹ : A) - 1) = HSMul.hSMul (β := A) r 1 - (↑a : A)
⊢ (r • (↑a⁻¹ : A) - 1) * (↑a : A) = HSMul.hSMul (β := A) r 1 - (↑a : A)
have rw : r • (↑a⁻¹ : A) * (↑a : A) - 1 * (↑a : A) = HSMul.hSMul (β := A) r 1 - (↑a : A)
Tactic: rw [sub_mul, smul_mul_assoc, a.inv_mul, one_mul]
-- 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
r : Rˣ
a : Aˣ
h : IsUnit (HSMul.hSMul (β := A) r 1 - (↑a : A))
h₁ : (↑a : A) * (r • (↑a⁻¹ : A) - 1) = HSMul.hSMul (β := A) r 1 - (↑a : A)
rw : r • (↑a⁻¹ : A) * (↑a : A) - 1 * (↑a : A) = HSMul.hSMul (β := A) r 1 - (↑a : A)
⊢ (r • (↑a⁻¹ : A) - 1) * (↑a : A) = HSMul.hSMul (β := A) r 1 - (↑a : A)
have rw₁ : r • ((↑a⁻¹ : A) * (↑a : A)) - 1 * (↑a : A) = HSMul.hSMul (β := A) r 1 - (↑a : A)
Tactic: rw [sub_mul, smul_mul_assoc, a.inv_mul, one_mul]
-- 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
r : Rˣ
a : Aˣ
h : IsUnit (HSMul.hSMul (β := A) r 1 - (↑a : A))
h₁ : (↑a : A) * (r • (↑a⁻¹ : A) - 1) = HSMul.hSMul (β := A) r 1 - (↑a : A)
rw : r • (↑a⁻¹ : A) * (↑a : A) - 1 * (↑a : A) = HSMul.hSMul (β := A) r 1 - (↑a : A)
rw₁ : r • ((↑a⁻¹ : A) * (↑a : A)) - 1 * (↑a : A) = HSMul.hSMul (β := A) r 1 - (↑a : A)
⊢ (r • (↑a⁻¹ : A) - 1) * (↑a : A) = HSMul.hSMul (β := A) r 1 - (↑a : A)
have rw₂ : HSMul.hSMul (β := A) r 1 - 1 * (↑a : A) = HSMul.hSMul (β := A) r 1 - (↑a : A)
Tactic: rw [sub_mul, smul_mul_assoc, a.inv_mul, one_mul]
-- 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
r : Rˣ
a : Aˣ
h : IsUnit (HSMul.hSMul (β := A) r 1 - (↑a : A))
h₁ : (↑a : A) * (r • (↑a⁻¹ : A) - 1) = HSMul.hSMul (β := A) r 1 - (↑a : A)
rw : r • (↑a⁻¹ : A) * (↑a : A) - 1 * (↑a : A) = HSMul.hSMul (β := A) r 1 - (↑a : A)
rw₁ : r • ((↑a⁻¹ : A) * (↑a : A)) - 1 * (↑a : A) = HSMul.hSMul (β := A) r 1 - (↑a : A)
rw₂ : HSMul.hSMul (β := A) r 1 - 1 * (↑a : A) = HSMul.hSMul (β := A) r 1 - (↑a : A)
⊢ (r • (↑a⁻¹ : A) - 1) * (↑a : A) = HSMul.hSMul (β := A) r 1 - (↑a : A)
have rw₃ : HSMul.hSMul (β := A) r 1 - (↑a : A) = HSMul.hSMul (β := A) r 1 - (↑a : A)
Tactic: rw [sub_mul, smul_mul_assoc, a.inv_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (HSMul.hSMul (β := A) r 1 - (↑a : A))
h₁ : (↑a : A) * (r • (↑a⁻¹ : A) - 1) = HSMul.hSMul (β := A) r 1 - (↑a : A)
⊢ IsUnit (r • (↑a⁻¹ : A) - 1)
have h₂ : (r • (↑a⁻¹ : A) - 1) * (↑a : A) = HSMul.hSMul (β := A) r 1 - (↑a : A)
Tactic: have h₂ : (r • (↑a⁻¹ : A) - 1) * a = r • (1 : A) - a := by
    rw [sub_mul, smul_mul_assoc, a.inv_mul, one_mul]
-- 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
r : Rˣ
a : Aˣ
h : IsUnit (HSMul.hSMul (β := A) r 1 - (↑a : A))
h₁ : (↑a : A) * (r • (↑a⁻¹ : A) - 1) = HSMul.hSMul (β := A) r 1 - (↑a : A)
h₂ : (r • (↑a⁻¹ : A) - 1) * (↑a : A) = HSMul.hSMul (β := A) r 1 - (↑a : A)
⊢ Commute (↑a : A) (r • (↑a⁻¹ : A) - 1)
have rwa : ∀ (h₁ : (↑a : A) * (r • (↑a⁻¹ : A) - 1) = (r • (↑a⁻¹ : A) - 1) * (↑a : A))
  (h₂ : (r • (↑a⁻¹ : A) - 1) * (↑a : A) = HSMul.hSMul (β := A) r 1 - (↑a : A)), Commute (↑a : A) (r • (↑a⁻¹ : A) - 1)
Tactic: rwa [← h₂] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (HSMul.hSMul (β := A) r 1 - (↑a : A))
h₁ : (↑a : A) * (r • (↑a⁻¹ : A) - 1) = HSMul.hSMul (β := A) r 1 - (↑a : A)
h₂ : (r • (↑a⁻¹ : A) - 1) * (↑a : A) = HSMul.hSMul (β := A) r 1 - (↑a : A)
⊢ IsUnit (r • (↑a⁻¹ : A) - 1)
have hcomm : Commute (↑a : A) (r • (↑a⁻¹ : A) - 1)
Tactic: have hcomm : Commute (a : A) (r • (↑a⁻¹ : A) - 1) := by rwa [← h₂] at 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
a : A
r s : R
⊢ r + s ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) s : A) a) ↔ r ∈ σ a
have rw : r ∈ σ (HAdd.hAdd (α := A) (-(↑ₐ : (a : R) → A) s : A) (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) s : A) a)) ↔ r ∈ σ a
Tactic: rw [add_mem_iff, neg_add_cancel_left]
-- 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
a : A
r s : R
rw : r ∈ σ (HAdd.hAdd (α := A) (-(↑ₐ : (a : R) → A) s : A) (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) s : A) a)) ↔ r ∈ σ a
⊢ r + s ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) s : A) a) ↔ r ∈ σ a
have rw₁ : r ∈ σ a ↔ r ∈ σ a
Tactic: rw [add_mem_iff, neg_add_cancel_left]
-- 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
a : A
r : Rˣ
⊢ σ (r • a) = r • σ a
have h : ∀ (x : R), x ∈ σ (r • a) ↔ x ∈ r • σ a
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r : Rˣ
x : R
⊢ x ∈ σ (r • a) ↔ x ∈ r • σ a
have x_eq : x = r • r⁻¹ • x
Tactic: have x_eq : x = r • r⁻¹ • x := by simp
-- 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
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
⊢ x ∈ σ (r • a) ↔ x ∈ r • σ a
have h : r • r⁻¹ • x ∈ σ (r • a) ↔ x ∈ r • σ a
Tactic: nth_rw 1 [x_eq]
-- 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
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
⊢ r • r⁻¹ • x ∈ σ (r • a) ↔ x ∈ r • σ a
have h : r⁻¹ • x ∈ σ a ↔ x ∈ r • σ a
Tactic: rw [smul_mem_smul_iff]
-- 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
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
⊢ r⁻¹ • x ∈ σ a ↔ x ∈ r • σ a
have h : r⁻¹ • x ∈ σ a → x ∈ r • σ a
Tactic: constructor
-- 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
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
h : r⁻¹ • x ∈ σ a → x ∈ r • σ a
⊢ r⁻¹ • x ∈ σ a ↔ x ∈ r • σ a
have h₁ : x ∈ r • σ a → r⁻¹ • x ∈ σ a
Tactic: constructor
-- 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
a b : A
r : Rˣ
⊢ ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
have refine_1 : ∀ (x y : A) (h : IsUnit (1 - x * y)), (1 - y * x) * (1 + y * h.unit.inv * x) = 1
Tactic: refine fun x y h => ⟨⟨1 - y * x, 1 + y * h.unit.inv * x, ?_, ?_⟩, rfl⟩
-- 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
a b : A
r : Rˣ
refine_1 : ∀ (x y : A) (h : IsUnit (1 - x * y)), (1 - y * x) * (1 + y * h.unit.inv * x) = 1
⊢ ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
have refine_2 : ∀ (x y : A) (h : IsUnit (1 - x * y)), (1 + y * h.unit.inv * x) * (1 - y * x) = 1
Tactic: refine fun x y h => ⟨⟨1 - y * x, 1 + y * h.unit.inv * x, ?_, ?_⟩, rfl⟩
-- 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
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 - y * x) * (1 + y * h.unit.inv * x) = 1
have y₁ : (1 - y * x) * (1 + y * h.unit.inv * x) = 1 - y * x + y * ((1 - x * y) * h.unit.inv) * x
Tactic: calc
        (1 - y * x) * (1 + y * (IsUnit.unit h).inv * x) =
            1 - y * x + y * ((1 - x * y) * h.unit.inv) * x := by noncomm_ring
        _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.mul_val_inv, mul_one, sub_add_cancel]
-- 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
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
y₁ : (1 - y * x) * (1 + y * h.unit.inv * x) = 1 - y * x + y * ((1 - x * y) * h.unit.inv) * x
⊢ (1 - y * x) * (1 + y * h.unit.inv * x) = 1
have y₂ : 1 - y * x + y * ((1 - x * y) * h.unit.inv) * x = 1
Tactic: calc
        (1 - y * x) * (1 + y * (IsUnit.unit h).inv * x) =
            1 - y * x + y * ((1 - x * y) * h.unit.inv) * x := by noncomm_ring
        _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.mul_val_inv, mul_one, sub_add_cancel]
-- 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
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 + y * h.unit.inv * x) * (1 - y * x) = 1 - y * x + y * (h.unit.inv * (1 - x * y)) * x
have noncomm_ring : 1 + y * (sorry.unit.inv * x) + -(y * x + y * (sorry.unit.inv * (x * (y * x)))) =
  1 + -(y * x) + (y * (sorry.unit.inv * x) + -(y * (sorry.unit.inv * (x * (y * x)))))
Tactic: noncomm_ring
-- 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
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 + y * h.unit.inv * x) * (1 - y * x) = 1
have y₁ : (1 + y * h.unit.inv * x) * (1 - y * x) = 1 - y * x + y * (h.unit.inv * (1 - x * y)) * x
Tactic: calc
        (1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) =
            1 - y * x + y * (h.unit.inv * (1 - x * y)) * x := by noncomm_ring
        _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.val_inv_mul, mul_one, sub_add_cancel]
-- 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
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
y₁ : (1 + y * h.unit.inv * x) * (1 - y * x) = 1 - y * x + y * (h.unit.inv * (1 - x * y)) * x
⊢ (1 + y * h.unit.inv * x) * (1 - y * x) = 1
have y₂ : 1 - y * x + y * (h.unit.inv * (1 - x * y)) * x = 1
Tactic: calc
        (1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) =
            1 - y * x + y * (h.unit.inv * (1 - x * y)) * x := by noncomm_ring
        _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.val_inv_mul, mul_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a b : A
r : Rˣ
⊢ (↑r : R) ∈ σ (a * b) ↔ (↑r : R) ∈ σ (b * a)
have h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
Tactic: have h₁ : ∀ x y : A, IsUnit (1 - x * y) → IsUnit (1 - y * x) := by
    refine fun x y h => ⟨⟨1 - y * x, 1 + y * h.unit.inv * x, ?_, ?_⟩, rfl⟩
    · calc
        (1 - y * x) * (1 + y * (IsUnit.unit h).inv * x) =
            1 - y * x + y * ((1 - x * y) * h.unit.inv) * x := by noncomm_ring
        _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.mul_val_inv, mul_one, sub_add_cancel]
    · calc
        (1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) =
            1 - y * x + y * (h.unit.inv * (1 - x * y)) * x := by noncomm_ring
        _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.val_inv_mul, mul_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a b : A
r : Rˣ
h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
⊢ (↑r : R) ∈ σ (a * b) ↔ (↑r : R) ∈ σ (b * a)
have this : IsUnit (1 - r⁻¹ • a * b) ↔ IsUnit (1 - b * r⁻¹ • a)
Tactic: have := Iff.intro (h₁ (r⁻¹ • a) b) (h₁ b (r⁻¹ • a))
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a b : A
r : Rˣ
h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
this : IsUnit (1 - r⁻¹ • a * b) ↔ IsUnit (1 - b * r⁻¹ • a)
⊢ (↑r : R) ∈ σ (a * b) ↔ (↑r : R) ∈ σ (b * a)
have this₁ : IsUnit (1 - r⁻¹ • a * b) ↔ IsUnit (1 - r⁻¹ • (b * a))
Tactic: rw [mul_smul_comm r⁻¹ b a] at this
Cleared hypotheses: this
-- 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
a b : A
⊢ {r : R | IsUnit r} ∩ σ (a * b) = {r : R | IsUnit r} ∩ σ (b * a)
have h : ∀ (r : R), r ∈ {r : R | IsUnit r} ∩ σ (a * b) ↔ r ∈ {r : R | IsUnit r} ∩ σ (b * a)
Tactic: ext r