-- Mathlib/Algebra/Algebra/Quasispectrum.lean
lemma quasispectrum.mul_comm {R A : Type*} [CommRing R] [NonUnitalRing A] [Module R A]
    [IsScalarTower R A A] [SMulCommClass R A A] (a b : A) :
    quasispectrum R (a * b) = quasispectrum R (b * a)

Proof state:
case h.e'_4
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ quasispectrum R (a * b) ∩ {r | IsUnit r}ᶜ = quasispectrum R (b * a) ∩ {r | IsUnit r}ᶜ

Tactic:
rw [Set.inter_eq_right.mpr, Set.inter_eq_right.mpr]

Result:
case h.e'_4
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ {r | IsUnit r}ᶜ ⊆ quasispectrum R (b * a)

case h.e'_4
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ {r | IsUnit r}ᶜ ⊆ quasispectrum R (a * b)

Proof state:
case h.e'_4
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ {r | IsUnit r}ᶜ ⊆ quasispectrum R (b * a)

case h.e'_4
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ {r | IsUnit r}ᶜ ⊆ quasispectrum R (a * b)

Tactic:
all_goals exact fun _ ↦ quasispectrum.not_isUnit_mem _

Result:
no goals

Proof state:
case h.e'_3
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ quasispectrum R (a * b) ∩ {r | IsUnit r} = quasispectrum R (b * a) ∩ {r | IsUnit r}

Tactic:
simpa [Set.inter_comm _ {r | IsUnit r}, Unitization.quasispectrum_eq_spectrum_inr,
  Unitization.inr_mul] using spectrum.setOf_isUnit_inter_mul_comm _ _

Result:
no goals

Proof state:
case h.e'_4
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ {r | IsUnit r}ᶜ ⊆ quasispectrum R (a * b)

Tactic:
exact fun _ ↦ quasispectrum.not_isUnit_mem _

Result:
no goals

Proof state:
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ quasispectrum R (a * b) = quasispectrum R (b * a)

Tactic:
rw [← Set.inter_union_compl (quasispectrum R (a * b)) {r | IsUnit r},
  ← Set.inter_union_compl (quasispectrum R (b * a)) {r | IsUnit r}]

Result:
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ quasispectrum R (a * b) ∩ {r | IsUnit r} ∪ quasispectrum R (a * b) ∩ {r | IsUnit r}ᶜ =
    quasispectrum R (b * a) ∩ {r | IsUnit r} ∪ quasispectrum R (b * a) ∩ {r | IsUnit r}ᶜ

Proof state:
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ quasispectrum R (a * b) ∩ {r | IsUnit r} ∪ quasispectrum R (a * b) ∩ {r | IsUnit r}ᶜ =
    quasispectrum R (b * a) ∩ {r | IsUnit r} ∪ quasispectrum R (b * a) ∩ {r | IsUnit r}ᶜ

Tactic:
congr! 1

Result:
case h.e'_3
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ quasispectrum R (a * b) ∩ {r | IsUnit r} = quasispectrum R (b * a) ∩ {r | IsUnit r}

case h.e'_4
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ quasispectrum R (a * b) ∩ {r | IsUnit r}ᶜ = quasispectrum R (b * a) ∩ {r | IsUnit r}ᶜ