awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.RestrictScalars
Goal:
R : Type u_1
S : Type u_2
A : Type u_4
inst : Semiring A
inst_1 : CommSemiring S
inst_2 : Algebra S A
inst_3 : CommSemiring R
inst_4 : Algebra R S
r : R
⊢ Eq (α := A)
    ((ringEquiv R S A : (a : RestrictScalars R S A) → A)
        ((algebraMap R (RestrictScalars R S A) : (a : R) → RestrictScalars R S A) r : RestrictScalars R S A) :
      A)
    ((algebraMap S A : (a : S) → A) ((algebraMap R S : (a : R) → S) r : S) : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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) r ((↑ₐ : (a : R) → A) s : A) - a)
rw : r • (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) * (↑h.unit⁻¹ : A)) = 1
rw₁ : r • HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) * (↑h.unit⁻¹ : A) = 1
rw₂ : (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) s : A) - r • r⁻¹ • a) * (↑h.unit⁻¹ : A) = 1
rw₃ : (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) s : A) - a) * (↑h.unit⁻¹ : A) = 1
rw₄ rw₅ : Eq.{v + 1} (α := A) 1 1
⊢ HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) * r • (↑h.unit⁻¹ : A) = 1

Tactic:
rw [mul_smul_comm, ← smul_mul_assoc, smul_sub, smul_inv_smul, h.mul_val_inv]

Premises used: IsUnit.mul_val_inv, smul_mul_assoc, smul_inv_smul, smul_sub, mul_smul_comm
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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) r ((↑ₐ : (a : R) → A) s : A) - a)
rw : r • ((↑h.unit⁻¹ : A) * HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a)) = 1
rw₁ : (↑h.unit⁻¹ : A) * r • HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) = 1
rw₂ : (↑h.unit⁻¹ : A) * (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) s : A) - r • r⁻¹ • a) = 1
rw₃ : (↑h.unit⁻¹ : A) * (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) s : A) - a) = 1
rw₄ rw₅ : Eq.{v + 1} (α := A) 1 1
⊢ r • (↑h.unit⁻¹ : A) * HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) (r⁻¹ • a) = 1

Tactic:
rw [smul_mul_assoc, ← mul_smul_comm, smul_sub, smul_inv_smul, h.val_inv_mul]

Premises used: smul_mul_assoc, smul_inv_smul, smul_sub, mul_smul_comm, IsUnit.val_inv_mul
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
r : R
a : A
⊢ r ∈ σ a ↔ ¬IsUnit (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)

Tactic:
Iff.rfl

Premises used: spectrum, Set.Mem, Iff.rfl, setOf, IsUnit, resolventSet, Not
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
r : R
a : A
hr : r ∈ σ a
⊢ resolvent a r = 0

Tactic:
Ring.inverse_non_unit _ (mem_iff.mp hr)

Premises used: Ring.inverse_non_unit, spectrum.mem_iff, resolvent, Iff.mp
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Nontrivial A
r : R
a : A
⊢ r ∈ σ a ↔ resolvent a r = 0

Tactic:
⟨resolvent_zero_of_mem_spectrum, fun hr ↦ ?_⟩

Premises used: spectrum.resolvent_zero_of_mem_spectrum, Iff.intro
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Nontrivial A
r : R
a : A
refine : ∀ (hr : resolvent a r = 0), r ∈ σ a
⊢ r ∈ σ a ↔ resolvent a r = 0

Tactic:
refine ⟨resolvent_zero_of_mem_spectrum, fun hr ↦ ?_⟩
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Nontrivial A
r : R
a : A
hr : resolvent a r = 0
⊢ r ∈ σ a

Tactic:
simpa [mem_iff, Ring.not_isUnit_iff_inverse_eq_zero]

Premises used: spectrum.mem_iff, Ring.not_isUnit_iff_inverse_eq_zero
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
r : R
a : A
⊢ r ∉ σ a ↔ IsUnit (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)

Tactic:
simp [mem_iff]

Premises used: spectrum.mem_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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
rw₃ rw₄ : ¬IsUnit a ↔ ¬IsUnit a
⊢ 0 ∈ σ a ↔ ¬IsUnit a

Tactic:
rw [mem_iff, map_zero, zero_sub, IsUnit.neg_iff]

Premises used: map_zero, IsUnit.neg_iff, spectrum.mem_iff, zero_sub
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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
rw₁ rw₂ : IsUnit a ↔ IsUnit a
⊢ 0 ∉ σ a ↔ IsUnit a

Tactic:
rw [zero_mem_iff, Classical.not_not]

Premises used: Classical.not_not, spectrum.zero_mem_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : Aˣ
⊢ 0 ∉ σ (↑a : A)

Tactic:
spectrum.zero_notMem R a.isUnit

Premises used: spectrum.zero_notMem, Units.isUnit
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
ha : IsUnit a
⊢ σ a ⊆ {0}ᶜ

Tactic:
Set.subset_compl_singleton_iff.mpr <| spectrum.zero_notMem R ha

Premises used: Iff.mpr, Set.subset_compl_singleton_iff, spectrum.zero_notMem
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
r : R
a b c : A
h₁ : HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a * b = 1
h₂ : c * HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a = 1
rwa rwa₁ rwa₂ rwa₃ : c * HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a = 1
⊢ b * HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a = 1

Tactic:
rwa [← left_inv_eq_right_inv h₂ h₁]

Premises used: left_inv_eq_right_inv
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
r : R
a : A
⊢ r ∈ resolventSet R a ↔ IsUnit (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) r : A) a)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, IsUnit, resolventSet
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
a : A
r : R
⊢ Membership.mem (α := S) (spectrum S a) ((algebraMap R S : (a : R) → S) r : S) ↔ r ∈ σ a

Tactic:
simp only [spectrum.mem_iff, Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]

Premises used: smul_assoc, one_smul, Algebra.algebraMap_eq_smul_one, spectrum.mem_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
a : A
⊢ (⇑(algebraMap R S) : (a : R) → S) ⁻¹' spectrum S a = σ a

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

Premises used: Set.ext, spectrum.algebraMap_mem_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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
simp_rw₂ : Eq.{u + 1} (α := Set R) {r : R | True} univ
⊢ resolventSet R a = univ

Tactic:
simp_rw [resolventSet, Subsingleton.elim (algebraMap R A _ - a) 1, isUnit_one, Set.setOf_true]

Premises used: Algebra.algebraMap, HSub.hSub, isUnit_one, Set.setOf_true, resolventSet, Subsingleton.elim, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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ᶜ ∅
rw₂ rw₃ : Eq.{u + 1} (α := Set R) ∅ ∅
⊢ σ a = ∅

Tactic:
rw [spectrum, resolventSet_of_subsingleton, Set.compl_univ]

Premises used: spectrum, Set.compl_univ, spectrum.resolventSet_of_subsingleton
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r : R
h : r ∈ resolventSet R a
⊢ resolvent a r = (↑(IsUnit.unit h)⁻¹ : A)

Tactic:
Ring.inverse_unit h.unit

Premises used: Ring.inverse_unit, resolvent, IsUnit.unit
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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)
neg : ∀ (h : s ∉ σ a), r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)

Tactic:
by_cases h : s ∈ spectrum R a

Premises used: spectrum
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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
⊢ ¬IsUnit (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) a)

Tactic:
rw [mem_iff] at h

Premises used: spectrum.mem_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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)
pos :
  ∀ (h : ¬IsUnit (HSMul.hSMul (β := A) s 1 - a)),
    r • (HSMul.hSMul (β := A) s 1 - a)⁻¹ʳ = (HSMul.hSMul (β := A) (r⁻¹ • s) 1 - r⁻¹ • a)⁻¹ʳ
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)

Tactic:
simp only [resolvent, Algebra.algebraMap_eq_smul_one] at *

Premises used: Algebra.algebraMap_eq_smul_one, resolvent
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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)
pos : r • (HSMul.hSMul (β := A) s 1 - a)⁻¹ʳ = (r⁻¹ • (HSMul.hSMul (β := A) s 1 - a))⁻¹ʳ
⊢ r • (HSMul.hSMul (β := A) s 1 - a)⁻¹ʳ = (HSMul.hSMul (β := A) (r⁻¹ • s) 1 - r⁻¹ • a)⁻¹ʳ

Tactic:
rw [smul_assoc, ← smul_sub]

Premises used: smul_assoc, smul_sub
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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)
hu : IsUnit (r⁻¹ • (HSMul.hSMul (β := A) s 1 - a))
⊢ IsUnit (HSMul.hSMul (β := A) s 1 - a)

Tactic:
simpa only [smul_inv_smul] using IsUnit.smul r hu

Premises used: smul_inv_smul, IsUnit.smul
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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)
⊢ ¬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)
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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)
h' : ¬IsUnit (r⁻¹ • (HSMul.hSMul (β := A) s 1 - a))
⊢ r • (HSMul.hSMul (β := A) s 1 - a)⁻¹ʳ = (r⁻¹ • (HSMul.hSMul (β := A) s 1 - a))⁻¹ʳ

Tactic:
simp only [Ring.inverse_non_unit _ h, Ring.inverse_non_unit _ h', smul_zero]

Premises used: smul_zero, Ring.inverse_non_unit
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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
neg :
  r • (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) a)⁻¹ʳ =
    (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) (r⁻¹ • s) : A) (r⁻¹ • a))⁻¹ʳ
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)

Tactic:
simp only [resolvent]

Premises used: resolvent
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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
⊢ IsUnit (HSMul.hSMul (β := A) r ((↑ₐ : (a : R) → A) (r⁻¹ • s) : A) - a)

Tactic:
simpa [Algebra.algebraMap_eq_smul_one, smul_assoc] using notMem_iff.mp h

Premises used: smul_assoc, Algebra.algebraMap_eq_smul_one, Iff.mp, spectrum.notMem_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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
⊢ 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
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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)
neg : r • (↑⋯.unit⁻¹ : A) = r • (↑h'.unit⁻¹ : A)
⊢ r • (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) s : A) a)⁻¹ʳ =
    (HSub.hSub (α := A) ((↑ₐ : (a : R) → A) (r⁻¹ • s) : A) (r⁻¹ • a))⁻¹ʳ

Tactic:
rw [← h'.val_subInvSMul, ← (notMem_iff.mp h).unit_spec, Ring.inverse_unit, Ring.inverse_unit,
      h'.val_inv_subInvSMul]

Premises used: Ring.inverse_unit, IsUnit.val_subInvSMul, Iff.mp, IsUnit.val_inv_subInvSMul, IsUnit.unit_spec, spectrum.notMem_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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 • (↑⋯.unit⁻¹ : A) = r • (↑h'.unit⁻¹ : A)

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, smul_assoc, smul_inv_smul]

Premises used: smul_assoc, smul_inv_smul, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
r : Rˣ
a : A
⊢ r • resolvent a (↑r : R) = resolvent.{u, v} (R := R) (r⁻¹ • a) 1

Tactic:
simpa only [Units.smul_def, smul_eq_mul, Units.inv_mul] using
    @units_smul_resolvent _ _ _ _ _ r r a

Premises used: Units.inv_mul, Units.smul_def, smul_eq_mul, spectrum.units_smul_resolvent
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
r : R
a : A
⊢ r ∈ resolventSet R a ↔ IsUnit (resolvent a r)

Tactic:
isUnit_ringInverse.symm

Premises used: Set.Mem, setOf, IsUnit, resolvent, resolventSet, isUnit_ringInverse, Iff.symm
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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)
rw : ∀ (h : IsUnit (HSMul.hSMul (β := A) r 1 - (↑a : A))), IsUnit (HSMul.hSMul (β := A) r⁻¹ 1 - (↑a⁻¹ : A))
⊢ (↑r⁻¹ : R) ∈ resolventSet R (↑a⁻¹ : A)

Tactic:
rw [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one, ← Units.smul_def] at h ⊢

Premises used: spectrum.mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one, Units.smul_def
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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 : IsUnit (r • (↑a⁻¹ : A) - 1)
⊢ IsUnit (HSMul.hSMul (β := A) r⁻¹ 1 - (↑a⁻¹ : A))

Tactic:
rw [IsUnit.smul_sub_iff_sub_inv_smul, inv_inv, IsUnit.sub_iff]

Premises used: IsUnit.smul_sub_iff_sub_inv_smul, IsUnit.sub_iff, inv_inv
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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)
rw₃ rw₄ : HSMul.hSMul (β := A) r 1 - (↑a : A) = HSMul.hSMul (β := A) r 1 - (↑a : A)
⊢ (↑a : A) * (r • (↑a⁻¹ : A) - 1) = HSMul.hSMul (β := A) r 1 - (↑a : A)

Tactic:
rw [mul_sub, mul_smul_comm, a.mul_inv, mul_one]

Premises used: mul_sub, Units.mul_inv, mul_smul_comm, mul_one
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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)

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]
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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)
rw₃ rw₄ : HSMul.hSMul (β := A) r 1 - (↑a : A) = HSMul.hSMul (β := A) r 1 - (↑a : A)
⊢ (r • (↑a⁻¹ : A) - 1) * (↑a : A) = HSMul.hSMul (β := A) r 1 - (↑a : A)

Tactic:
rw [sub_mul, smul_mul_assoc, a.inv_mul, one_mul]

Premises used: Units.inv_mul, smul_mul_assoc, sub_mul, one_mul
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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)

Tactic:
have h₂ : (r • (↑a⁻¹ : A) - 1) * a = r • (1 : A) - a := by
    rw [sub_mul, smul_mul_assoc, a.inv_mul, one_mul]
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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)
rwa rwa₁ rwa₂ 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)
⊢ Commute (↑a : A) (r • (↑a⁻¹ : A) - 1)

Tactic:
rwa [← h₂] at h₁
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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)

Tactic:
have hcomm : Commute (a : A) (r • (↑a⁻¹ : A) - 1) := by rwa [← h₂] at h₁
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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)
hcomm : Commute (↑a : A) (r • (↑a⁻¹ : A) - 1)
⊢ IsUnit (r • (↑a⁻¹ : A) - 1)

Tactic:
(hcomm.isUnit_mul_iff.mp (h₁.symm ▸ h)).2

Premises used: Eq.rec, And.right, Commute.isUnit_mul_iff, Iff.mp, Eq.symm
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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)
hcomm : Commute (↑a : A) (r • (↑a⁻¹ : A) - 1)
⊢ IsUnit (r • (↑a⁻¹ : A) - 1)

Tactic:
exact (hcomm.isUnit_mul_iff.mp (h₁.symm ▸ h)).2

Premises used: Eq.rec, And.right, Commute.isUnit_mul_iff, Iff.mp, Eq.symm
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
r : Rˣ
a : Aˣ
⊢ (↑r : R) ∈ σ (↑a : A) ↔ (↑r⁻¹ : R) ∈ σ (↑a⁻¹ : A)

Tactic:
not_iff_not.2 <| ⟨inv_mem_resolventSet, inv_mem_resolventSet⟩

Premises used: not_iff_not, Iff.mpr, spectrum, Set.Mem, setOf, Iff.intro, spectrum.inv_mem_resolventSet, Not
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : Aˣ
⊢ 0 ∈ resolventSet R (↑a : A)

Tactic:
simpa only [mem_resolventSet_iff, ← notMem_iff, zero_notMem_iff] using a.isUnit

Premises used: spectrum.zero_notMem_iff, spectrum.mem_resolventSet_iff, Units.isUnit, spectrum.notMem_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : Aˣ
r : R
hr : r ∈ σ (↑a : A)
⊢ r ≠ 0

Tactic:
fun hn =>
  (hn ▸ hr) (zero_mem_resolventSet_of_unit a)

Premises used: Not
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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 ∈ σ a ↔ r ∈ σ (HAdd.hAdd (α := A) (-(↑ₐ : (a : R) → A) s : A) a)

Tactic:
simp only [mem_iff, sub_neg_eq_add, ← sub_sub, map_add]

Premises used: map_add, sub_sub, spectrum.mem_iff, sub_neg_eq_add
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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
rw₁ rw₂ : r ∈ σ a ↔ r ∈ σ a
⊢ r + s ∈ σ (HAdd.hAdd (α := A) ((↑ₐ : (a : R) → A) s : A) a) ↔ r ∈ σ a

Tactic:
rw [add_mem_iff, neg_add_cancel_left]

Premises used: spectrum.add_mem_iff, neg_add_cancel_left
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
s : R
r : Rˣ
⊢ r • s ∈ σ (r • a) ↔ s ∈ σ a

Tactic:
simp only [mem_iff, Algebra.algebraMap_eq_smul_one, smul_assoc, ← smul_sub, isUnit_smul_iff]

Premises used: smul_assoc, isUnit_smul_iff, Algebra.algebraMap_eq_smul_one, smul_sub, spectrum.mem_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
r : Rˣ
h : ∀ (x : R), x ∈ σ (r • a) ↔ x ∈ r • σ a
⊢ σ (r • a) = r • σ a

Tactic:
ext x
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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 • r⁻¹ • x

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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 • r⁻¹ • x

Tactic:
have x_eq : x = r • r⁻¹ • x := by simp
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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 • r⁻¹ • x ∈ σ (r • a) ↔ x ∈ r • σ a
⊢ x ∈ σ (r • a) ↔ x ∈ r • σ a

Tactic:
nth_rw 1 [x_eq]
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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 • r⁻¹ • x ∈ σ (r • a) ↔ x ∈ r • σ a

Tactic:
rw [smul_mem_smul_iff]

Premises used: spectrum.smul_mem_smul_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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
h₁ : x ∈ r • σ a → r⁻¹ • x ∈ σ a
⊢ r⁻¹ • x ∈ σ a ↔ x ∈ r • σ a

Tactic:
constructor
-- Module: Mathlib.Algebra.Algebra.Spectrum.Basic
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
⊢ r • r⁻¹ • x = x

Tactic:
simp