feat(Topology/Algebra/Module): call eta_expand in the default tactic of ContinuousLinearEquiv (leanprover-community#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.

Author: gasparattila

Mathlib/Analysis/Fourier/Notation.lean

@@ -264,8 +264,6 @@ variable (R E) in
 /-- The Fourier transform as a continuous linear equivalence. -/
 def fourierCLE : E ≃L[R] F where
   __ := fourierEquiv R E
-  continuous_toFun := continuous_fourier
-  continuous_invFun := continuous_fourierInv
 
 @[simp]
 lemma fourierCLE_apply (f : E) : fourierCLE R E f = 𝓕 f := rfl

Mathlib/Analysis/LocallyConvex/SeparatingDual.lean

@@ -222,9 +222,7 @@ theorem exists_continuousLinearEquiv_apply_eq
         smul_eq_mul, mul_sub, mul_one]
       rw [mul_comm _ (G y), ← mul_assoc, mul_inv_cancel₀ Gy]
       simp only [smul_sub, one_mul, add_sub_cancel]
-      abel
-    continuous_toFun := by fun_prop
-    continuous_invFun := by fun_prop }
+      abel }
   exact ⟨A, show x + G x • (y - x) = y by simp [Gx]⟩
 
 end Field

Mathlib/Analysis/Normed/Lp/PiLp.lean

@@ -1140,8 +1140,6 @@ variable [Semiring 𝕜] [∀ i, SeminormedAddCommGroup (β i)] [∀ i, Module 
 @[simps! apply symm_apply]
 def continuousLinearEquiv : PiLp p β ≃L[𝕜] ∀ i, β i where
   toLinearEquiv := WithLp.linearEquiv _ _ _
-  continuous_toFun := continuous_ofLp _ _
-  continuous_invFun := continuous_toLp p _
 
 lemma coe_continuousLinearEquiv :
     ⇑(PiLp.continuousLinearEquiv p 𝕜 β) = ofLp := rfl

Mathlib/Analysis/Normed/Module/FiniteDimension.lean

@@ -266,9 +266,6 @@ where `ι` is a finite type. -/
 def ContinuousLinearEquiv.piRing (ι : Type*) [Fintype ι] [DecidableEq ι] :
     ((ι → 𝕜) →L[𝕜] E) ≃L[𝕜] ι → E :=
   { LinearMap.toContinuousLinearMap.symm.trans (LinearEquiv.piRing 𝕜 E ι 𝕜) with
-    continuous_toFun := by
-      refine continuous_pi fun i ↦ ?_
-      exact (apply 𝕜 E (Pi.single i 1)).continuous
     continuous_invFun := by
       simp_rw [LinearEquiv.invFun_eq_symm, LinearEquiv.trans_symm, LinearEquiv.symm_symm]
       refine AddMonoidHomClass.continuous_of_bound

Mathlib/Topology/Algebra/Module/Equiv.lean

@@ -35,8 +35,8 @@ structure ContinuousLinearEquiv {R : Type*} {S : Type*} [Semiring R] [Semiring S
     {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (M : Type*) [TopologicalSpace M]
     [AddCommMonoid M] (M₂ : Type*) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M]
     [Module S M₂] extends M ≃ₛₗ[σ] M₂ where
-  continuous_toFun : Continuous toFun := by first | fun_prop | dsimp; fun_prop
-  continuous_invFun : Continuous invFun := by first | fun_prop | dsimp; fun_prop
+  continuous_toFun : Continuous toFun := by first | fun_prop | eta_expand; dsimp; fun_prop | skip
+  continuous_invFun : Continuous invFun := by first | fun_prop | eta_expand; dsimp; fun_prop | skip
 
 attribute [inherit_doc ContinuousLinearEquiv] ContinuousLinearEquiv.continuous_toFun
 ContinuousLinearEquiv.continuous_invFun
@@ -288,10 +288,8 @@ variable (R₁ M₁)
 
 /-- The identity map as a continuous linear equivalence. -/
 @[refl]
-protected def refl : M₁ ≃L[R₁] M₁ :=
-  { LinearEquiv.refl R₁ M₁ with
-    continuous_toFun := continuous_id
-    continuous_invFun := continuous_id }
+protected def refl : M₁ ≃L[R₁] M₁ where
+  __ := LinearEquiv.refl R₁ M₁
 
 @[simp]
 theorem refl_apply (x : M₁) :
@@ -346,10 +344,8 @@ theorem symm_map_nhds_eq (e : M₁ ≃SL[σ₁₂] M₂) (x : M₁) : map e.symm
 
 /-- The composition of two continuous linear equivalences as a continuous linear equivalence. -/
 @[trans]
-protected def trans (e₁ : M₁ ≃SL[σ₁₂] M₂) (e₂ : M₂ ≃SL[σ₂₃] M₃) : M₁ ≃SL[σ₁₃] M₃ :=
-  { e₁.toLinearEquiv.trans e₂.toLinearEquiv with
-    continuous_toFun := e₂.continuous_toFun.comp e₁.continuous_toFun
-    continuous_invFun := e₁.continuous_invFun.comp e₂.continuous_invFun }
+protected def trans (e₁ : M₁ ≃SL[σ₁₂] M₂) (e₂ : M₂ ≃SL[σ₂₃] M₃) : M₁ ≃SL[σ₁₃] M₃ where
+  __ := e₁.toLinearEquiv.trans e₂.toLinearEquiv
 
 @[simp]
 theorem trans_toLinearEquiv (e₁ : M₁ ≃SL[σ₁₂] M₂) (e₂ : M₂ ≃SL[σ₂₃] M₃) :
@@ -383,10 +379,8 @@ variable (R₁ M₁ M₂)
 
 /-- Product of modules is commutative up to continuous linear isomorphism. -/
 @[simps! apply toLinearEquiv]
-def prodComm [Module R₁ M₂] : (M₁ × M₂) ≃L[R₁] M₂ × M₁ :=
-  { LinearEquiv.prodComm R₁ M₁ M₂ with
-    continuous_toFun := continuous_swap
-    continuous_invFun := continuous_swap }
+def prodComm [Module R₁ M₂] : (M₁ × M₂) ≃L[R₁] M₂ × M₁ where
+  __ := LinearEquiv.prodComm R₁ M₁ M₂
 
 @[simp] lemma prodComm_symm [Module R₁ M₂] : (prodComm R₁ M₁ M₂).symm = prodComm R₁ M₂ M₁ := rfl
 
@@ -434,8 +428,6 @@ variable (R M₁ M₂ M₃ M₄ : Type*) [Semiring R]
 This is `LinearEquiv.prodProdProdComm` prodAssoc as a continuous linear equivalence. -/
 def prodProdProdComm : ((M₁ × M₂) × M₃ × M₄) ≃L[R] (M₁ × M₃) × M₂ × M₄ where
   toLinearEquiv := LinearEquiv.prodProdProdComm R M₁ M₂ M₃ M₄
-  continuous_toFun := by fun_prop
-  continuous_invFun := by fun_prop
 
 @[simp]
 theorem prodProdProdComm_symm :
@@ -468,12 +460,6 @@ variable (R M N : Type*) [Semiring R]
 This is `Equiv.prodUnique` as a continuous linear equivalence. -/
 def prodUnique : (M × N) ≃L[R] M where
   toLinearEquiv := LinearEquiv.prodUnique
-  continuous_toFun := by
-    change Continuous (Equiv.prodUnique M N)
-    dsimp; fun_prop
-  continuous_invFun := by
-    change Continuous fun x ↦ (x, default)
-    fun_prop
 
 @[simp]
 lemma coe_prodUnique : (prodUnique R M N).toEquiv = Equiv.prodUnique M N := rfl
@@ -488,12 +474,6 @@ lemma prodUnique_symm_apply (x : M) : (prodUnique R M N).symm x = (x, default) :
 This is `Equiv.uniqueProd` as a continuous linear equivalence. -/
 def uniqueProd : (N × M) ≃L[R] M where
   toLinearEquiv := LinearEquiv.uniqueProd
-  continuous_toFun := by
-    change Continuous (Equiv.uniqueProd M N)
-    dsimp; fun_prop
-  continuous_invFun := by
-    change Continuous fun x ↦ (default, x)
-    fun_prop
 
 @[simp]
 lemma coe_uniqueProd : (uniqueProd R M N).toEquiv = Equiv.uniqueProd M N := rfl
@@ -632,9 +612,7 @@ inverse of each other. See also `equivOfInverse'`. -/
 def equivOfInverse (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M₁) (h₁ : Function.LeftInverse f₂ f₁)
     (h₂ : Function.RightInverse f₂ f₁) : M₁ ≃SL[σ₁₂] M₂ :=
   { f₁ with
-    continuous_toFun := f₁.continuous
     invFun := f₂
-    continuous_invFun := f₂.continuous
     left_inv := h₁
     right_inv := h₂ }
 
@@ -700,10 +678,8 @@ variable {M₁} {R₄ : Type*} [Semiring R₄] [Module R₄ M₄] {σ₃₄ : R
 /-- The continuous linear equivalence between `ULift M₁` and `M₁`.
 
 This is a continuous version of `ULift.moduleEquiv`. -/
-def ulift : ULift M₁ ≃L[R₁] M₁ :=
-  { ULift.moduleEquiv with
-    continuous_toFun := continuous_uliftDown
-    continuous_invFun := continuous_uliftUp }
+def ulift : ULift M₁ ≃L[R₁] M₁ where
+  __ := ULift.moduleEquiv
 
 /-- A pair of continuous (semi)linear equivalences generates an equivalence between the spaces of
 continuous linear maps. See also `ContinuousLinearEquiv.arrowCongr`. -/
@@ -777,12 +753,8 @@ variable {ι : Type*} {M : ι → Type*} [∀ i, TopologicalSpace (M i)] [∀ i,
 
 /-- Combine a family of continuous linear equivalences into a continuous linear equivalence of
 pi-types. -/
-def piCongrRight : ((i : ι) → M i) ≃L[R₁] (i : ι) → N i :=
-  { LinearEquiv.piCongrRight fun i ↦ f i with
-    continuous_toFun := by
-      exact continuous_pi fun i ↦ (f i).continuous_toFun.comp (continuous_apply i)
-    continuous_invFun := by
-      exact continuous_pi fun i => (f i).continuous_invFun.comp (continuous_apply i) }
+def piCongrRight : ((i : ι) → M i) ≃L[R₁] (i : ι) → N i where
+  __ := LinearEquiv.piCongrRight fun i ↦ (f i).toLinearEquiv
 
 @[simp]
 theorem piCongrRight_apply (m : (i : ι) → M i) (i : ι) :
@@ -837,8 +809,6 @@ def ofUnit (f : (M →L[R] M)ˣ) : M ≃L[R] M where
         show (f.val * f.inv) x = x by
           rw [f.val_inv]
           simp }
-  continuous_toFun := f.val.continuous
-  continuous_invFun := f.inv.continuous
 
 /-- A continuous equivalence from `M` to itself determines an invertible continuous linear map. -/
 def toUnit (f : M ≃L[R] M) : (M →L[R] M)ˣ where
@@ -946,8 +916,6 @@ variable (R M) in
 @[simps!]
 def _root_.Fin.consEquivL : (M 0 × Π i, M (Fin.succ i)) ≃L[R] (Π i, M i) where
   __ := Fin.consLinearEquiv R M
-  continuous_toFun := continuous_id.fst.finCons continuous_id.snd
-  continuous_invFun := .prodMk (continuous_apply 0) (by fun_prop)
 
 /-- `Fin.cons` in the codomain of continuous linear maps. -/
 abbrev _root_.ContinuousLinearMap.finCons
@@ -971,15 +939,8 @@ variable [IsTopologicalAddGroup M₄]
 
 /-- Equivalence given by a block lower diagonal matrix. `e` and `e'` are diagonal square blocks,
   and `f` is a rectangular block below the diagonal. -/
-def skewProd (e : M ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) (f : M →L[R] M₄) : (M × M₃) ≃L[R] M₂ × M₄ :=
-  { e.toLinearEquiv.skewProd e'.toLinearEquiv ↑f with
-    continuous_toFun :=
-      (e.continuous_toFun.comp continuous_fst).prodMk
-        ((e'.continuous_toFun.comp continuous_snd).add <| f.continuous.comp continuous_fst)
-    continuous_invFun :=
-      (e.continuous_invFun.comp continuous_fst).prodMk
-        (e'.continuous_invFun.comp <|
-          continuous_snd.sub <| f.continuous.comp <| e.continuous_invFun.comp continuous_fst) }
+def skewProd (e : M ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) (f : M →L[R] M₄) : (M × M₃) ≃L[R] M₂ × M₄ where
+  __ := e.toLinearEquiv.skewProd e'.toLinearEquiv ↑f
 
 @[simp]
 theorem skewProd_apply (e : M ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) (f : M →L[R] M₄) (x) :
@@ -994,10 +955,8 @@ theorem skewProd_symm_apply (e : M ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) (f : M
 variable (R) in
 /-- The negation map as a continuous linear equivalence. -/
 def neg [ContinuousNeg M] :
-    M ≃L[R] M :=
-  { LinearEquiv.neg R with
-    continuous_toFun := continuous_neg
-    continuous_invFun := continuous_neg }
+    M ≃L[R] M where
+  __ := LinearEquiv.neg R
 
 @[simp]
 theorem coe_neg [ContinuousNeg M] :
@@ -1065,8 +1024,6 @@ def restrictScalars (R : Type*) {S : Type*} {M : Type*}
     [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [TopologicalSpace M]
     [LinearMap.CompatibleSMul M M R S] (f : M ≃L[S] M) : M ≃L[R] M where
   toLinearEquiv := f.toLinearEquiv.restrictScalars R
-  continuous_invFun := f.continuous_invFun
-  continuous_toFun := f.continuous_toFun
 
 end RestrictScalars
 

Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean

@@ -259,6 +259,11 @@ def compContinuousLinearMapL (f : ∀ i, E i →L[𝕜] E₁ i) :
       set φ : (∀ i, E i) →L[𝕜] (∀ i, E₁ i) := .piMap f
       exact ⟨(φ '' U, V), ⟨hU.image φ, hV⟩, fun g hg ↦ hg.comp (mapsTo_image _ _)⟩ }
 
+@[fun_prop]
+theorem continuous_precomp (f : ∀ i, E i →L[𝕜] E₁ i) :
+    Continuous fun g : ContinuousMultilinearMap 𝕜 E₁ F ↦ g.compContinuousLinearMap f :=
+  map_continuous (compContinuousLinearMapL f)
+
 end CompContinuousLinearMap
 
 variable [∀ i, ContinuousSMul 𝕜 (E i)]
@@ -386,6 +391,11 @@ theorem compContinuousMultilinearMapL_apply (g : F →L[𝕜] G) (f : Continuous
     compContinuousMultilinearMapL 𝕜 E F G g f = g.compContinuousMultilinearMap f :=
   rfl
 
+@[fun_prop]
+theorem _root_.ContinuousLinearMap.continuous_postcomp_continuousMultilinearMap (g : F →L[𝕜] G) :
+    Continuous (g.compContinuousMultilinearMap (M₁ := E)) :=
+  map_continuous (compContinuousMultilinearMapL 𝕜 E F G g)
+
 end ContinuousLinearMap
 
 namespace ContinuousLinearEquiv