diff --git a/Mathlib/Analysis/Complex/Spectrum.lean b/Mathlib/Analysis/Complex/Spectrum.lean
index 168d635d3eb05a..8abea04b731c9b 100644
--- a/Mathlib/Analysis/Complex/Spectrum.lean
+++ b/Mathlib/Analysis/Complex/Spectrum.lean
@@ -17,13 +17,9 @@ public section
 namespace SpectrumRestricts
 variable {A : Type*} [Ring A]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma real_iff [Algebra ℂ A] {a : A} :
     SpectrumRestricts a Complex.reCLM ↔ ∀ x ∈ spectrum ℂ a, x = x.re := by
-  refine ⟨fun h x hx ↦ ?_, fun h ↦ ?_⟩
-  · obtain ⟨x, -, rfl⟩ := h.algebraMap_image.symm ▸ hx
-    simp
-  · exact .of_subset_range_algebraMap Complex.ofReal_re fun x hx ↦ ⟨x.re, (h x hx).symm⟩
+  simp [spectrumRestricts_iff, Set.LeftInvOn, Function.LeftInverse, eq_comm]
 
 end SpectrumRestricts