-- Mathlib/Algebra/Algebra/Spectrum.lean
/-- Conjugation by a unit preserves the spectrum, inverse on right. -/
@[simp]
lemma spectrum.units_conjugate {a : A} {u : Aˣ} :
    spectrum R (u * a * u⁻¹) = spectrum R a

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
u : Aˣ
this : ∀ (b : A) (v : Aˣ), spectrum R (↑v * b * ↑v⁻¹) ⊆ spectrum R b
⊢ spectrum R a ≤ spectrum R (↑u * a * ↑u⁻¹)

Tactic:
apply le_of_eq_of_le ?_ <| this (u * a * u⁻¹) u⁻¹

Result:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
u : Aˣ
this : ∀ (b : A) (v : Aˣ), spectrum R (↑v * b * ↑v⁻¹) ⊆ spectrum R b
⊢ spectrum R a = spectrum R (↑u⁻¹ * (↑u * a * ↑u⁻¹) * ↑u⁻¹⁻¹)

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a✝ : A
u✝ : Aˣ
a : A
u : Aˣ
μ : R
hμ : ¬IsUnit ((algebraMap R A) μ - ↑u * a * ↑u⁻¹)
⊢ ¬IsUnit ((algebraMap R A) μ - a)

Tactic:
contrapose! hμ

Result:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a✝ : A
u✝ : Aˣ
a : A
u : Aˣ
μ : R
hμ : IsUnit ((algebraMap R A) μ - a)
⊢ IsUnit ((algebraMap R A) μ - ↑u * a * ↑u⁻¹)

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a✝ : A
u✝ : Aˣ
a : A
u : Aˣ
μ : R
hμ : IsUnit ((algebraMap R A) μ - a)
⊢ IsUnit ((algebraMap R A) μ - ↑u * a * ↑u⁻¹)

Tactic:
simpa [mul_sub, sub_mul, Algebra.right_comm] using u.isUnit.mul hμ |>.mul u⁻¹.isUnit

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
u : Aˣ
⊢ spectrum R (↑u * a * ↑u⁻¹) = spectrum R a

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]

Result:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
u : Aˣ
⊢ ∀ (b : A) (v : Aˣ), spectrum R (↑v * b * ↑v⁻¹) ⊆ spectrum R b

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a✝ : A
u✝ : Aˣ
a : A
u : Aˣ
μ : R
hμ : μ ∈ spectrum R (↑u * a * ↑u⁻¹)
⊢ μ ∈ spectrum R a

Tactic:
rw [spectrum.mem_iff] at hμ ⊢

Result:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a✝ : A
u✝ : Aˣ
a : A
u : Aˣ
μ : R
hμ : ¬IsUnit ((algebraMap R A) μ - ↑u * a * ↑u⁻¹)
⊢ ¬IsUnit ((algebraMap R A) μ - a)

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
u : Aˣ
this : ∀ (b : A) (v : Aˣ), spectrum R (↑v * b * ↑v⁻¹) ⊆ spectrum R b
⊢ spectrum R (↑u * a * ↑u⁻¹) = spectrum R a

Tactic:
refine le_antisymm (this a u) ?_

Result:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
u : Aˣ
this : ∀ (b : A) (v : Aˣ), spectrum R (↑v * b * ↑v⁻¹) ⊆ spectrum R b
⊢ spectrum R a ≤ spectrum R (↑u * a * ↑u⁻¹)

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
u : Aˣ
⊢ ∀ (b : A) (v : Aˣ), spectrum R (↑v * b * ↑v⁻¹) ⊆ spectrum R b

Tactic:
intro a u μ hμ

Result:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a✝ : A
u✝ : Aˣ
a : A
u : Aˣ
μ : R
hμ : μ ∈ spectrum R (↑u * a * ↑u⁻¹)
⊢ μ ∈ spectrum R a

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
u : Aˣ
this : ∀ (b : A) (v : Aˣ), spectrum R (↑v * b * ↑v⁻¹) ⊆ spectrum R b
⊢ spectrum R a = spectrum R (↑u⁻¹ * (↑u * a * ↑u⁻¹) * ↑u⁻¹⁻¹)

Tactic:
simp [mul_assoc]

Result:
no goals