-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem units_smul_resolvent {r : Rˣ} {s : R} {a : A} :
    r • resolvent a (s : R) = resolvent (r⁻¹ • a) (r⁻¹ • s : R)

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
hu : IsUnit (r⁻¹ • (s • 1 - a))
⊢ IsUnit (s • 1 - a)

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

Result:
no goals

Proof state:
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∉ σ a
h' : IsUnit (r • ↑ₐ (r⁻¹ • s) - a)
⊢ r • Ring.inverse (↑ₐ s - a) = Ring.inverse (↑ₐ (r⁻¹ • s) - r⁻¹ • a)

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

Result:
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∉ σ a
h' : IsUnit (r • ↑ₐ (r⁻¹ • s) - a)
⊢ r • ↑⋯.unit⁻¹ = r • ↑h'.unit⁻¹

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)

Tactic:
by_cases h : s ∈ spectrum R a

Result:
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∈ σ a
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)

case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∉ σ a
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∉ σ a
⊢ IsUnit (r • ↑ₐ (r⁻¹ • s) - a)

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

Result:
no goals

Proof state:
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∉ σ a
⊢ r • Ring.inverse (↑ₐ s - a) = Ring.inverse (↑ₐ (r⁻¹ • s) - r⁻¹ • a)

Tactic:
have h' : IsUnit (r • algebraMap R A (r⁻¹ • s) - a) := by
  simpa [Algebra.algebraMap_eq_smul_one, smul_assoc] using not_mem_iff.mp h

Result:
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∉ σ a
h' : IsUnit (r • ↑ₐ (r⁻¹ • s) - a)
⊢ r • Ring.inverse (↑ₐ s - a) = Ring.inverse (↑ₐ (r⁻¹ • s) - r⁻¹ • a)

Proof state:
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∉ σ a
h' : IsUnit (r • ↑ₐ (r⁻¹ • s) - a)
⊢ r • ↑⋯.unit⁻¹ = r • ↑h'.unit⁻¹

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

Result:
no goals

Proof state:
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
⊢ r • Ring.inverse (s • 1 - a) = Ring.inverse (r⁻¹ • (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)

Result:
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
h' : ¬IsUnit (r⁻¹ • (s • 1 - a))
⊢ r • Ring.inverse (s • 1 - a) = Ring.inverse (r⁻¹ • (s • 1 - a))

Proof state:
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (↑ₐ s - a)
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)

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

Result:
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
⊢ r • Ring.inverse (s • 1 - a) = Ring.inverse ((r⁻¹ • s) • 1 - r⁻¹ • a)

Proof state:
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
h' : ¬IsUnit (r⁻¹ • (s • 1 - a))
⊢ r • Ring.inverse (s • 1 - a) = Ring.inverse (r⁻¹ • (s • 1 - a))

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

Result:
no goals

Proof state:
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
⊢ r • Ring.inverse (s • 1 - a) = Ring.inverse ((r⁻¹ • s) • 1 - r⁻¹ • a)

Tactic:
rw [smul_assoc, ← smul_sub]

Result:
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (s • 1 - a)
⊢ r • Ring.inverse (s • 1 - a) = Ring.inverse (r⁻¹ • (s • 1 - a))

Proof state:
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∉ σ a
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)

Tactic:
simp only [resolvent]

Result:
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∉ σ a
⊢ r • Ring.inverse (↑ₐ s - a) = Ring.inverse (↑ₐ (r⁻¹ • s) - r⁻¹ • a)

Proof state:
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∈ σ a
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)

Tactic:
rw [mem_iff] at h

Result:
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (↑ₐ s - a)
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)