Lint

Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean

@@ -41,8 +41,8 @@ theorem measurableEquivRealProd_apply (a : ℂ) : measurableEquivRealProd a = (a
 theorem volume_preserving_equiv_pi : MeasurePreserving measurableEquivPi := by
   convert (measurableEquivPi.symm.measurable.measurePreserving volume).symm
   rw [← addHaarMeasure_eq_volume_pi, ← Basis.parallelepiped_basisFun, ← Basis.addHaar,
-    measurableEquivPi, Homeomorph.toMeasurableEquiv_symm_coe,
-    ContinuousLinearEquiv.coe_toHomeomorph_symm, ← LinearEquiv.coe_toContinuousLinearEquiv_symm',
+    measurableEquivPi, Homeomorph.toMeasurableEquiv_symm_coe]
+  rw [ContinuousLinearEquiv.symm_toHomeomorph, ContinuousLinearEquiv.coe_toHomeomorph,
     Basis.addHaar_map]
   exact Basis.addHaar_eq.mpr Complex.orthonormalBasisOneI.volume_parallelepiped
 #align complex.volume_preserving_equiv_pi Complex.volume_preserving_equiv_pi

Mathlib/Topology/Algebra/Module/Basic.lean

@@ -1890,10 +1890,6 @@ theorem coe_toHomeomorph (e : M₁ ≃SL[σ₁₂] M₂) : ⇑e.toHomeomorph = e
   rfl
 #align continuous_linear_equiv.coe_to_homeomorph ContinuousLinearEquiv.coe_toHomeomorph
 
-@[simp]
-theorem coe_toHomeomorph_symm (e : M₁ ≃SL[σ₁₂] M₂) : ⇑e.toHomeomorph.symm = e.symm :=
-  rfl
-
 theorem image_closure (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₁) : e '' closure s = closure (e '' s) :=
   e.toHomeomorph.image_closure s
 #align continuous_linear_equiv.image_closure ContinuousLinearEquiv.image_closure