perf: make Equiv transfer instances more reduced (leanprover-community#41002)

This pr speeds up the instances that are tranferred through `Equiv`s by using the projections `.toFun` and `.invFun` directly in the data.

I think that we should eventually deprecate these instances, and instead have a metaprogram that creates these instances for us in each use case.

Author: JovanGerb

Mathlib/Algebra/Algebra/TransferInstance.lean

@@ -22,6 +22,7 @@ variable {R α β : Type*} [CommSemiring R]
 namespace Equiv
 variable (e : α ≃ β)
 
+-- See note [instance transfer via equivalence]
 variable (R) in
 /-- Transfer `Algebra` across an `Equiv` -/
 protected abbrev algebra (e : α ≃ β) [Semiring β] :
@@ -30,7 +31,7 @@ protected abbrev algebra (e : α ≃ β) [Semiring β] :
   letI := Equiv.semiring e
   letI := e.smul R
   { algebraMap :=
-    { toFun r := e.symm (algebraMap R β r)
+    { toFun r := e.invFun (algebraMap R β r)
       __ := e.ringEquiv.symm.toRingHom.comp (algebraMap R β) }
     commutes' r x :=
       show e.symm ((e (e.symm (algebraMap R β r)) * e x)) =

Mathlib/Algebra/Category/MonCat/Limits.lean

@@ -180,8 +180,7 @@ noncomputable instance forget_createsLimit :
       simp only [Types.Small.limitCone_pt, Functor.comp_obj, Functor.mapCone_pt,
         Types.Small.limitConeIsLimit_lift, Functor.const_obj_obj, Functor.mapCone_π_app,
         ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, map_mul]
-      congr
-      simp only [Functor.comp_obj, Equiv.symm_apply_apply]
+      rw [← equivShrink_mul]
       rfl
   · exact fun _ ↦ rfl
 

Mathlib/Algebra/Field/TransferInstance.lean

@@ -21,11 +21,12 @@ assert_not_exists Module
 namespace Equiv
 variable {α β : Type*} (e : α ≃ β)
 
+-- See note [instance transfer via equivalence]
 /-- Transfer `NNRatCast` across an `Equiv` -/
-protected abbrev nnratCast [NNRatCast β] : NNRatCast α where nnratCast q := e.symm q
+protected abbrev nnratCast [NNRatCast β] : NNRatCast α where nnratCast q := e.invFun q
 
 /-- Transfer `RatCast` across an `Equiv` -/
-protected abbrev ratCast [RatCast β] : RatCast α where ratCast n := e.symm n
+protected abbrev ratCast [RatCast β] : RatCast α where ratCast n := e.invFun n
 
 /-- Transfer `DivisionRing` across an `Equiv` -/
 protected abbrev divisionRing [DivisionRing β] : DivisionRing α := by

Mathlib/Algebra/Group/TransferInstance.lean

@@ -25,12 +25,25 @@ When adding new definitions that transfer type-classes across an equivalence, pl
 
 assert_not_exists MonoidWithZero MulAction
 
+library_note «instance transfer via equivalence» /--
+For many type classes, we have a definition that lets us transfer instances from one type to another
+using an equivalence, such as `Equiv.mul` for `Mul`.
+Constructing data instances in this way is discouraged because the resulting data is inefficient
+to unfold. To somewhat mitigate this problem, in these definitions we don't write the
+projections on `Equiv` in the usual way using `Equiv.symm` and `DFunLike.coe`, and instead use
+`Equiv.toFun` and `Equiv.invFun` directly. As a result, unification has to do less unfolding.
+
+Note also that when constructing data instances in this way, it usually helps to use
+`fast_instance%` to get a faster instance.
+-/
+
 namespace Equiv
 variable {M α β : Type*} (e : α ≃ β)
 
+-- See note [instance transfer via equivalence]
 /-- Transfer `One` across an `Equiv` -/
 @[to_additive /-- Transfer `Zero` across an `Equiv` -/]
-protected abbrev one [One β] : One α where one := e.symm 1
+protected abbrev one [One β] : One α where one := e.invFun 1
 
 @[to_additive]
 lemma one_def [One β] :
@@ -39,7 +52,7 @@ lemma one_def [One β] :
 
 /-- Transfer `Mul` across an `Equiv` -/
 @[to_additive /-- Transfer `Add` across an `Equiv` -/]
-protected abbrev mul [Mul β] : Mul α where mul x y := e.symm (e x * e y)
+protected abbrev mul [Mul β] : Mul α where mul x y := e.invFun (e.toFun x * e.toFun y)
 
 @[to_additive]
 lemma mul_def [Mul β] (x y : α) :
@@ -49,7 +62,7 @@ lemma mul_def [Mul β] (x y : α) :
 /-- Transfer `Div` across an `Equiv` -/
 @[to_additive /-- Transfer `Sub` across an `Equiv` -/]
 protected abbrev div [Div β] : Div α :=
-  ⟨fun x y => e.symm (e x / e y)⟩
+  ⟨fun x y => e.invFun (e.toFun x / e.toFun y)⟩
 
 @[to_additive]
 lemma div_def [Div β] (x y : α) :
@@ -60,7 +73,7 @@ lemma div_def [Div β] (x y : α) :
 -- but we already have an `Equiv.inv` (which perhaps should move to `Perm.inv`?)
 /-- Transfer `Inv` across an `Equiv` -/
 @[to_additive /-- Transfer `Neg` across an `Equiv` -/]
-protected abbrev Inv [Inv β] : Inv α where inv x := e.symm (e x)⁻¹
+protected abbrev Inv [Inv β] : Inv α where inv x := e.invFun (e.toFun x)⁻¹
 
 @[to_additive]
 lemma inv_def [Inv β] (x : α) :
@@ -71,7 +84,7 @@ variable (M) in
 /-- Transfer `Pow` across an `Equiv` -/
 @[to_additive (attr := to_additive /-- Transfer `VAdd` across an `Equiv` -/) smul
 /-- Transfer `SMul` across an `Equiv` -/]
-protected abbrev pow [Pow β M] : Pow α M where pow x n := e.symm (e x ^ n)
+protected abbrev pow [Pow β M] : Pow α M where pow x n := e.invFun (e.toFun x ^ n)
 
 @[to_additive (attr := to_additive) smul_def]
 lemma pow_def [Pow β M] (n : M) (x : α) :

Mathlib/Algebra/Ring/TransferInstance.lean

@@ -64,21 +64,22 @@ protected abbrev nonUnitalSemiring [NonUnitalSemiring β] : NonUnitalSemiring α
   let nsmul := e.smul ℕ
   apply e.injective.nonUnitalSemiring _ <;> intros <;> exact e.apply_symm_apply _
 
+-- See note [instance transfer via equivalence]
 /-- Transfer `AddMonoidWithOne` across an `Equiv` -/
 protected abbrev addMonoidWithOne [AddMonoidWithOne β] : AddMonoidWithOne α :=
   { e.addMonoid, e.one with
-    natCast := fun n => e.symm n
+    natCast := fun n => e.invFun n
     natCast_zero := e.injective (by simp [zero_def])
     natCast_succ := fun n => e.injective (by simp [add_def, one_def]) }
 
 /-- Transfer `AddGroupWithOne` across an `Equiv` -/
 protected abbrev addGroupWithOne [AddGroupWithOne β] : AddGroupWithOne α :=
   { e.addMonoidWithOne,
     e.addGroup with
-    intCast := fun n => e.symm n
+    intCast := fun n => e.invFun n
     intCast_ofNat := fun n => by simp only [Int.cast_natCast]; rfl
     intCast_negSucc := fun _ =>
-      congr_arg e.symm <| (Int.cast_negSucc _).trans <| congr_arg _ (e.apply_symm_apply _).symm }
+      congr_arg e.invFun <| (Int.cast_negSucc _).trans <| congr_arg _ (e.apply_symm_apply _).symm }
 
 /-- Transfer `NonAssocSemiring` across an `Equiv` -/
 protected abbrev nonAssocSemiring [NonAssocSemiring β] : NonAssocSemiring α := by

Mathlib/Algebra/Star/TransferInstance.lean

@@ -21,11 +21,12 @@ namespace Equiv
 
 variable (e : R ≃ S)
 
+-- See note [instance transfer via equivalence]
 /-- Transfer `Star` across an `Equiv`. See note [reducible non-instances].
 
 For `star : R → R` bundled as an `Equiv`, see `Equiv.Perm.star`. -/
 protected abbrev star [Star S] : Star R where
-  star r := e.symm (star (e r))
+  star r := e.invFun (star (e.toFun r))
 
 /-- Transfer `InvolutiveStar` across an `Equiv`. See note [reducible non-instances]. -/
 protected abbrev involutiveStar [InvolutiveStar S] : InvolutiveStar R :=

Mathlib/RingTheory/PicardGroup.lean

@@ -472,14 +472,14 @@ instance : Free R (1 : Pic R) := mk_eq_one_iff_free.mp mk_eq_self
 
 theorem mk_tensor : Pic.mk R (M ⊗[R] N) = Pic.mk R M * Pic.mk R N :=
   congr_arg (equivShrink _) <| Units.ext <| by
-    simp_rw [Pic.mk, Equiv.symm_apply_apply]
+    simp_rw [Pic.mk, Equiv.toFun_as_coe, Equiv.symm_apply_apply]
     refine (Quotient.sound ?_).trans (Skeleton.toSkeleton_tensorObj ..)
     exact ⟨(Finite.reprEquivₛ R _ ≪≫ₗ TensorProduct.congr
       (Finite.reprEquivₛ R M).symm (Finite.reprEquivₛ R N).symm).toModuleIsoₛ⟩
 
 theorem mk_dual : Pic.mk R (Dual R M) = (Pic.mk R M)⁻¹ :=
   congr_arg (equivShrink _) <| Units.ext <| by
-    rw [Pic.mk, Equiv.symm_apply_apply]
+    rw [Pic.mk, Equiv.toFun_as_coe, Equiv.symm_apply_apply]
     exact Quotient.sound ⟨(Finite.reprEquivₛ R _ ≪≫ₗ (Finite.reprEquivₛ R _).dualMap).toModuleIsoₛ⟩
 
 theorem inv_eq_dual (M : Pic R) : M⁻¹ = Pic.mk R (Dual R M) := by

Mathlib/Topology/Algebra/Module/TransferInstance.lean

@@ -50,7 +50,7 @@ def continuousLinearEquiv (e : α ≃ β) :
   { toLinearEquiv := e.linearEquiv _
     continuous_toFun := continuous_induced_dom
     continuous_invFun := by
-      simp +instances only [Equiv.topologicalSpace, ← @coinduced_symm]
+      simp +instances only [Equiv.topologicalSpace, toFun_as_coe, ← coinduced_symm]
       exact continuous_coinduced_rng }
 
 @[simp]

Mathlib/Topology/Homeomorph/TransferInstance.lean

@@ -21,10 +21,11 @@ variable {R α β : Type*}
 
 namespace Equiv
 
+-- See note [instance transfer via equivalence]
 /-- Transfer a `TopologicalSpace` across an `Equiv` -/
 protected abbrev topologicalSpace [TopologicalSpace β] (e : α ≃ β) :
     TopologicalSpace α :=
-  .induced e ‹_›
+  .induced e.toFun ‹_›
 
 /-- An equivalence `e : α ≃ β` gives a homeomorphism `α ≃ₜ β` where the topological space structure
 on `α` is the one obtained by transporting the topological space structure on `β` back along `e`. -/
@@ -37,6 +38,7 @@ def homeomorph [TopologicalSpace β] (e : α ≃ β) :
     continuous_invFun := by
       simp only [Equiv.invFun_as_coe]
       convert! continuous_coinduced_rng
-      rw [e.coinduced_symm] }
+      rw [e.coinduced_symm]
+      rfl }
 
 end Equiv

Mathlib/Topology/MetricSpace/TransferInstance.lean

@@ -22,15 +22,16 @@ namespace Equiv
 
 variable (e : α ≃ β)
 
+-- See note [instance transfer via equivalence]
 /-- Transfer a `Dist` across an `Equiv` -/
-protected abbrev dist (e : α ≃ β) [Dist β] : Dist α := ⟨fun x y ↦ dist (e x) (e y)⟩
+protected abbrev dist (e : α ≃ β) [Dist β] : Dist α := ⟨fun x y ↦ dist (e.toFun x) (e.toFun y)⟩
 
 /-- Transfer a `PseudoMetricSpace` across an `Equiv` -/
 protected abbrev pseudometricSpace [PseudoMetricSpace β] (e : α ≃ β) : PseudoMetricSpace α :=
-  .induced e ‹_›
+  .induced e.toFun ‹_›
 
 /-- Transfer a `MetricSpace` across an `Equiv` -/
 protected abbrev metricSpace [MetricSpace β] (e : α ≃ β) : MetricSpace α :=
-  .induced e e.injective ‹_›
+  .induced e.toFun e.injective ‹_›
 
 end Equiv