fix: grind term preprocessor (#6659)

This PR fixes a bug in the `grind` term preprocessor. It was abstracting
nested proofs **before** reducible constants were unfolded.

---------

Co-authored-by: Kim Morrison <[email protected]>

src/Lean/Meta/Tactic/Grind/Simp.lean

@@ -28,9 +28,9 @@ def simp (e : Expr) : GoalM Simp.Result := do
   let e ← instantiateMVars e
   let r ← simpCore e
   let e' := r.expr
+  let e' ← unfoldReducible e'
   let e' ← abstractNestedProofs e'
   let e' ← markNestedProofs e'
-  let e' ← unfoldReducible e'
   let e' ← eraseIrrelevantMData e'
   let e' ← foldProjs e'
   let e' ← normalizeLevels e'

tests/lean/run/grind_cat.lean

@@ -36,6 +36,8 @@ structure Functor (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.
   /-- A functor preserves composition. -/
   map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = (map f) ≫ (map g) := by cat_tac
 
+scoped infixr:26 " ⥤ " => Functor
+
 attribute [simp] Functor.map_id Functor.map_comp
 
 attribute [grind =] Functor.map_id
@@ -51,6 +53,8 @@ def comp (F : Functor C D) (G : Functor D E) : Functor C E where
   map f := G.map (F.map f)
   -- Note `map_id` and `map_comp` are handled by `cat_tac`.
 
+infixr:80 " ⋙ " => Functor.comp
+
 variable {X Y : C} {G : Functor D E}
 
 @[simp, grind =] theorem comp_obj : (F.comp G).obj X = G.obj (F.obj X) := rfl
@@ -73,7 +77,7 @@ variable {X : C}
 
 protected def id (F : Functor C D) : NatTrans F F where app X := 𝟙 (F.obj X)
 
-@[simp, grind =] theorem id_app : (NatTrans.id F).app X = 𝟙 (F.obj X) := rfl
+@[simp, grind =] theorem id_app' : (NatTrans.id F).app X = 𝟙 (F.obj X) := rfl
 
 protected def vcomp (α : NatTrans F G) (β : NatTrans G H) : NatTrans F H where
   app X := α.app X ≫ β.app X
@@ -96,6 +100,11 @@ instance Functor.category : Category.{max u₁ v₂} (Functor C D) where
   comp α β := NatTrans.vcomp α β
   -- Here we're okay: all the proofs are handled by `cat_tac`.
 
+namespace NatTrans
+
+@[ext]
+theorem ext' {α β : F ⟶ G} (w : α.app = β.app) : α = β := NatTrans.ext w
+
 @[simp, grind =]
 theorem id_app (F : Functor C D) (X : C) : (𝟙 F : F ⟶ F).app X = 𝟙 (F.obj X) := rfl
 
@@ -122,6 +131,30 @@ def hcomp {H I : Functor D E} (α : F ⟶ G) (β : H ⟶ I) : F.comp H ⟶ G.com
   -- rw [Functor.comp_map, Functor.comp_map, ← assoc, naturality, assoc, ← I.map_comp, naturality,
   --   map_comp, assoc]
 
+/-- Notation for horizontal composition of natural transformations. -/
+infixl:80 " ◫ " => hcomp
+
+@[simp] theorem hcomp_app {H I : Functor D E} (α : F ⟶ G) (β : H ⟶ I) (X : C) :
+    (α ◫ β).app X = β.app (F.obj X) ≫ I.map (α.app X) := rfl
+
+attribute [grind =] hcomp_app
+
+theorem hcomp_id_app {H : D ⥤ E} (α : F ⟶ G) (X : C) : (α ◫ 𝟙 H).app X = H.map (α.app X) := by
+  cat_tac
+
+theorem id_hcomp_app {H : E ⥤ C} (α : F ⟶ G) (X : E) : (𝟙 H ◫ α).app X = α.app _ := by cat_tac
+
+-- Note that we don't yet prove a `hcomp_assoc` lemma here: even stating it is painful, because we
+-- need to use associativity of functor composition. (It's true without the explicit associator,
+-- because functor composition is definitionally associative,
+-- but relying on the definitional equality causes bad problems with elaboration later.)
+theorem exchange {I J K : D ⥤ E} (α : F ⟶ G) (β : G ⟶ H) (γ : I ⟶ J) (δ : J ⟶ K) :
+    (α ≫ β) ◫ (γ ≫ δ) = (α ◫ γ) ≫ β ◫ δ := by
+  ext X
+  cat_tac
+
+end NatTrans
+
 structure Iso {C : Type u} [Category.{v} C] (X Y : C) where
   hom : X ⟶ Y
   inv : Y ⟶ X
@@ -179,4 +212,88 @@ def homToEquiv (α : X ≅ Y) {Z : C} : (Z ⟶ X) ≃ (Z ⟶ Y) where
   right_inv := sorry
 
 end Iso
+
+section Mathlib.CategoryTheory.Functor.Category
+
+
+open NatTrans Category CategoryTheory.Functor
+
+variable (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]
+
+attribute [local simp] vcomp_app
+
+variable {C D} {E : Type u₃} [Category.{v₃} E]
+variable {E' : Type u₄} [Category.{v₄} E']
+variable {F G H I : C ⥤ D}
+
+
+namespace NatTrans
+
+@[simp]
+theorem vcomp_eq_comp (α : F ⟶ G) (β : G ⟶ H) : NatTrans.vcomp α β = α ≫ β := rfl
+
+theorem vcomp_app' (α : F ⟶ G) (β : G ⟶ H) (X : C) : (α ≫ β).app X = α.app X ≫ β.app X := rfl
+
+theorem congr_app {α β : F ⟶ G} (h : α = β) (X : C) : α.app X = β.app X := by rw [h]
+
+theorem naturality_app_app {F G : C ⥤ D ⥤ E ⥤ E'}
+    (α : F ⟶ G) {X₁ Y₁ : C} (f : X₁ ⟶ Y₁) (X₂ : D) (X₃ : E) :
+    ((F.map f).app X₂).app X₃ ≫ ((α.app Y₁).app X₂).app X₃ =
+      ((α.app X₁).app X₂).app X₃ ≫ ((G.map f).app X₂).app X₃ :=
+  congr_app (NatTrans.naturality_app α X₂ f) X₃
+
+end NatTrans
+
+open NatTrans
+
+namespace Functor
+
+/-- Flip the arguments of a bifunctor. See also `Currying.lean`. -/
+protected def flip (F : C ⥤ D ⥤ E) : D ⥤ C ⥤ E where
+  obj k :=
+    { obj := fun j => (F.obj j).obj k,
+      map := fun f => (F.map f).app k, }
+  map f := { app := fun j => (F.obj j).map f }
+  map_id k := by cat_tac
+  map_comp f g := sorry
+
+@[simp] theorem flip_obj_obj (F : C ⥤ D ⥤ E) (k : D) : (F.flip.obj k).obj = fun j => (F.obj j).obj k := rfl
+@[simp] theorem flip_obj_map (F : C ⥤ D ⥤ E) (k : D) {X Y : C}(f : X ⟶ Y) : (F.flip.obj k).map f = (F.map f).app k := rfl
+@[simp] theorem flip_map_app (F : C ⥤ D ⥤ E) {X Y : D} (f : X ⟶ Y) (k : C) : (F.flip.map f).app k = (F.obj k).map f := rfl
+
+attribute [grind =] flip_obj_obj flip_obj_map flip_map_app
+
+end Functor
+
+variable (C D E) in
+/-- The functor `(C ⥤ D ⥤ E) ⥤ D ⥤ C ⥤ E` which flips the variables. -/
+def flipFunctor : (C ⥤ D ⥤ E) ⥤ D ⥤ C ⥤ E where
+  obj F := F.flip
+  map {F₁ F₂} φ :=
+    { app := fun Y =>
+      { app := fun X => (φ.app X).app Y
+        naturality := fun X₁ X₂ f => by
+          dsimp
+          simp only [← NatTrans.comp_app, naturality] }
+      naturality := sorry }
+  map_id := sorry
+  map_comp := sorry
+
+namespace Iso
+
+@[simp]
+theorem map_hom_inv_id_app {X Y : C} (e : X ≅ Y) (F : C ⥤ D ⥤ E) (Z : D) :
+    (F.map e.hom).app Z ≫ (F.map e.inv).app Z = 𝟙 _ := by
+  cat_tac
+
+@[simp]
+theorem map_inv_hom_id_app {X Y : C} (e : X ≅ Y) (F : C ⥤ D ⥤ E) (Z : D) :
+    (F.map e.inv).app Z ≫ (F.map e.hom).app Z = 𝟙 _ := by
+  cat_tac
+
+end Iso
+
+
+end Mathlib.CategoryTheory.Functor.Category
+
 end CategoryTheory