Commit 2026-05-25 09:15 327a72be

feat(Topology/Algebra/Module): call eta_expand in the default tactic of ContinuousLinearEquiv (#39766) This PR adds a call to eta_expand in the default tactic for the fields of ContinuousLinearEquiv, so that dsimp can also use lemmas written in applied form. This is the same default tactic that is already used for Homeomorph and ContinuousLinearMap. Most of the proofs which are solved by this default tactic are also removed. A skip is also added to show the goal instead of "dsimp made no progress" when this default tactic fails.