fix(Simps): don't reduce the type of the equality (leanprover-community#36656)

This PR fixes a small problem with `simps`, that the type in the generated equality lemmas is unnecessarily reduced. This can result in raw projections, which we typically don't want in our lemmas. This doesn't affect how these lemmas behave in `simp`.

This problem confused `to_dual` a bit in `CategoryTheory.Iso`. This PR lets us remove the `respectTansparency` option there.

Author: JovanGerb

Mathlib/CategoryTheory/Iso.lean

@@ -118,7 +118,6 @@ def refl (X : C) : X ≅ X where
   hom := 𝟙 X
   inv := 𝟙 X
 
-set_option backward.isDefEq.respectTransparency false in
 set_option linter.existingAttributeWarning false in
 attribute [to_dual existing refl_inv] refl_hom
 
@@ -135,7 +134,6 @@ def trans (α : X ≅ Y) (β : Y ≅ Z) : X ≅ Z where
   hom := α.hom ≫ β.hom
   inv := β.inv ≫ α.inv
 
-set_option backward.isDefEq.respectTransparency false in
 set_option linter.existingAttributeWarning false in
 attribute [to_dual existing trans_inv] trans_hom
 
@@ -480,7 +478,6 @@ def mapIso (F : C ⥤ D) {X Y : C} (i : X ≅ Y) : F.obj X ≅ F.obj Y where
   hom := F.map i.hom
   inv := F.map i.inv
 
-set_option backward.isDefEq.respectTransparency false in
 set_option linter.existingAttributeWarning false in
 attribute [to_dual existing mapIso_inv] mapIso_hom
 

Mathlib/CategoryTheory/Whiskering.lean

@@ -43,7 +43,7 @@ variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
 
 set_option backward.isDefEq.respectTransparency false in
 /-- If `α : G ⟶ H` then `whiskerLeft F α : F ⋙ G ⟶ F ⋙ H` has components `α.app (F.obj X)`. -/
-@[to_dual self, simps (attr := to_dual self (reorder := G H))]
+@[to_dual self, simps (attr := to_dual self)]
 def whiskerLeft (F : C ⥤ D) {G H : D ⥤ E} (α : G ⟶ H) :
     F ⋙ G ⟶ F ⋙ H where
   app X := α.app (F.obj X)
@@ -56,7 +56,7 @@ lemma id_hcomp (F : C ⥤ D) {G H : D ⥤ E} (α : G ⟶ H) : 𝟙 F ◫ α = wh
 
 set_option backward.isDefEq.respectTransparency false in
 /-- If `α : G ⟶ H` then `whiskerRight α F : G ⋙ F ⟶ H ⋙ F` has components `F.map (α.app X)`. -/
-@[to_dual self, simps (attr := to_dual self (reorder := G H))]
+@[to_dual self, simps (attr := to_dual self)]
 def whiskerRight {G H : C ⥤ D} (α : G ⟶ H) (F : D ⥤ E) :
     G ⋙ F ⟶ H ⋙ F where
   app X := F.map (α.app X)

Mathlib/Tactic/Simps/Basic.lean

@@ -1051,12 +1051,14 @@ private partial def addProjections (nm : NameStruct) (type lhs rhs : Expr)
   trace[simps.debug] "Type of the Expression before normalizing: {type}"
   withTransparency cfg.typeMd <| forallTelescopeReducing type fun typeArgs tgt ↦ withDefault do
   trace[simps.debug] "Type after removing pi's: {tgt}"
-  let tgt ← whnfD tgt
-  trace[simps.debug] "Type after reduction: {tgt}"
+  -- TODO: consider reducing the type less aggressively.
+  -- See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Simps.20and.20.60def.60/near/560586075
+  let tgtWhnf ← whnfD tgt
+  trace[simps.debug] "Type after reduction: {tgtWhnf}"
   let newArgs := args ++ typeArgs
   let lhsAp := lhs.instantiateLambdasOrApps typeArgs
   let rhsAp := rhs.instantiateLambdasOrApps typeArgs
-  let str := tgt.getAppFn.constName
+  let str := tgtWhnf.getAppFn.constName
   trace[simps.debug] "todo: {todo}, toApply: {toApply}"
   -- We want to generate the current projection if it is in `todo`
   let todoNext := todo.filter (·.1 ≠ "")
@@ -1142,7 +1144,7 @@ private partial def addProjections (nm : NameStruct) (type lhs rhs : Expr)
     return #[nm.toName]
   -- if the value is a constructor application
   trace[simps.debug] "Generating raw projection information..."
-  let projInfo ← getProjectionExprs ref tgt rhsWhnf cfg
+  let projInfo ← getProjectionExprs ref tgtWhnf rhsWhnf cfg
   trace[simps.debug] "Raw projection information:{indentD m!"{projInfo}"}"
   -- If we are in the middle of a composite projection.
   if let idx :: rest := toApply then

MathlibTest/Simps.lean

@@ -1272,3 +1272,20 @@ example : foo.1 = 2 := by
   rfl
 
 end Grind
+
+def MyNat := Nat
+
+def MyNat.zero : MyNat := Nat.zero
+
+structure MyNatStruct where
+  n : MyNat
+
+@[simps]
+def zero : MyNatStruct where
+  n := MyNat.zero
+
+-- Verify that the equality type is not reduced from `MyNat` to `Nat`:
+set_option pp.explicit true in
+/-- info: zero_n : @Eq MyNat zero.n MyNat.zero -/
+#guard_msgs in
+#check zero_n