chore(Logic/Equiv): golf entire trans_symm_eq_symm_trans_symm using rfl (#28565)

Co-authored-by: euprunin <euprunin@users.noreply.github.com>

Author: euprunin

Mathlib/Logic/Equiv/PartialEquiv.lean

@@ -602,8 +602,7 @@ theorem coe_trans_symm : ((e.trans e').symm : γ → α) = e.symm ∘ e'.symm :=
 theorem trans_apply {x : α} : (e.trans e') x = e' (e x) :=
   rfl
 
-theorem trans_symm_eq_symm_trans_symm : (e.trans e').symm = e'.symm.trans e.symm := by
-  cases e; cases e'; rfl
+theorem trans_symm_eq_symm_trans_symm : (e.trans e').symm = e'.symm.trans e.symm := rfl
 
 @[simp, mfld_simps]
 theorem trans_source : (e.trans e').source = e.source ∩ e ⁻¹' e'.source :=