Policy/Preference on very long `simp only`s

Stream: lean4

[Robert Maxton]

What's the community preference on non-terminal simps when the alternative simp only is very long? I've got a simp whose replacement is a solid ten lines long, and I'm wondering if it's really worth replacing.

[Robert Maxton]

(There may or may not be a way to refactor this to be terminal -- though the relevant proof is difficult precisely because of a very long and highly dependent goal, so I kind of doubt it -- but for the sake of argument, assume there isn't. Is there a point where we draw the line, or alternatively is there some other consideration like "internally complex simp calls save disproportionately more time if converted to simp only" or something similar I don't know about?)

[Kim Morrison]

Is this asking about Mathlib or more generally?

More generally, there's no "policy". For Mathlib, I think we'd have to look at concrete examples to decide exceptions. have and suffices can nearly always --- for goals that appear in Mathlib --- help constrain the size of simp only.

[Kevin Buzzard]

Yes, before simp? the workflow (in the Lean 3 days) used to be
1) run simp
2) delete it and instead write suffices [the goal after simp] by simp

[Robert Maxton]

unfortunately in my case even the goal after simp is many lines long ^.^;
I'm currently cleaning it up a little, but I'll post it in a minute as I could use the advice
(It's making a docs#CategoryTheory.Pseudofunctor from ULift Cat to ULift Cat, so I have tangled n-morphisms everywhere >.>;)

[Robert Maxton]

Right, here's as minimal a #mwe as I can get.

import Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
import Mathlib.CategoryTheory.Category.Cat
import Mathlib.CategoryTheory.Category.ULift

-- import DiagrammaticMathlib.Bicategory.Basic
-- import DiagrammaticMathlib.Bicategory.Functor.Strict

namespace CategoryTheory
open CategoryTheory renaming ULiftHomULiftCategory.equiv → UHUC.equiv
open Bicategory ULift
universe w₂ w₁ w₀ v₂ v₁ v₀ u₂ u₁ u₀

attribute [pp_with_univ] Cat ULiftHom

variable (B : Type u₁) [Bicategory.{w₁, v₁} B] [Strict B]

@[simps!?]
instance (B : Type u₁) [Bicategory.{w₁, v₁} B] [Strict B] :
    Bicategory.{max w₂ w₁, max v₂ v₁} (ULiftHom.{v₂} (ULift.{u₂} B)) :=
  let homCategory (X Y : ULiftHom (ULift.{u₂} B)) : Category (X ⟶ Y) := {
    Hom f g := ULift.{w₂} <| (ULift.down f) ⟶ (ULift.down g)
    id f := ⟨𝟙 f.down⟩
    comp η ϑ := ⟨η.down ≫ ϑ.down⟩}
  have eqToHom_down {X Y : ULiftHom (ULift.{u₂} B)} {f g : X ⟶ Y} (η : f = g) :
      (eqToHom η).down = eqToHom (congrArg ULift.down η) := by
    cases η; rfl
  { __ := inferInstanceAs (Category <| ULiftHom.{v₂} <| ULift.{u₂} B)
    homCategory := homCategory
    whiskerLeft {X Y Z} f {g₁ g₂} η := ⟨f.down ◁ η.down⟩
    whiskerRight := fun ⟨η⟩ ⟨h⟩ ↦ ⟨η ▷ h⟩
    associator f g h := eqToIso (Category.assoc f g h)
    leftUnitor f := eqToIso (Category.id_comp f)
    rightUnitor f := eqToIso (Category.comp_id f)

    whiskerLeft_id := by intros; apply ULift.ext; unfold_projs; simp
    id_whiskerRight := by intros; apply ULift.ext; unfold_projs; simp
    comp_whiskerRight := by
      rintro _ _ _ _ _ _ ⟨η⟩ ⟨ϑ⟩ ⟨i⟩; apply ULift.ext; unfold_projs; simp
    id_whiskerLeft := by
      intros; apply ULift.ext; unfold_projs
      simp [Strict.leftUnitor_eqToIso, eqToHom_down]
    comp_whiskerLeft := by
      intros; apply ULift.ext; unfold_projs
      simp [Strict.associator_eqToIso, eqToHom_down]
    whiskerRight_id := by
      rintro _ _ _ _ ⟨η⟩; apply ULift.ext; unfold_projs
      simp [Strict.rightUnitor_eqToIso, eqToHom_down]
    whiskerRight_comp := by
      rintro _ _ _ _ _ _ ⟨η⟩ _ _; apply ULift.ext; unfold_projs
      simp [Strict.associator_eqToIso, eqToHom_down]
    whisker_assoc := by
      rintro _ _ _ _ _ _ _ ⟨η⟩ _; apply ULift.ext; unfold_projs
      simp [Strict.associator_eqToIso, eqToHom_down]
    whisker_exchange := by
      rintro _ _ _ ⟨f⟩ ⟨g⟩ ⟨h⟩ ⟨i⟩ ⟨η⟩ ⟨ϑ⟩; apply ULift.ext; unfold_projs
      simpa using Bicategory.whisker_exchange η ϑ }


#check ULiftHomULiftCategory.equiv
#synth Bicategory (ULiftHom <| ULift Cat)

namespace Cat
section uLiftEmbedding
variable {C D E : ULiftHom.{v₂} (ULift.{u₂} Cat.{v₁, u₁})}
         (F : C ⟶ D) {F₁ F₂ : C ⟶ D} (η : F₁ ⟶ F₂)
         {G₁ G₂ : D ⟶ E} (G : D ⟶ E) (ϑ : G₁ ⟶ G₂)


@[simps]
private def _prelax :
    CategoryTheory.PrelaxFunctor (ULiftHom.{v₂} <| ULift.{u₂} Cat.{v₁, u₁}) Cat.{max v₂ v₁, max u₂ u₁} where
  obj C := Cat.of (ULiftHom.{v₂} <| ULift.{u₂} ↑C.1)
  map {C D} F := (UHUC.equiv C.1).inverse ⋙ F.down ⋙ (UHUC.equiv D.1).functor
  map₂ η := whiskerLeft _ (whiskerRight η.down _)

private abbrev _mapId (C : ULiftHom.{v₂} <| ULift.{u₂} Cat.{v₁, u₁}) : _prelax.map (𝟙 C) ≅ 𝟙 (_prelax.obj C) :=
  isoWhiskerLeft (UHUC.equiv C.1).inverse (Functor.leftUnitor (UHUC.equiv C.1).functor)
      ≪≫ (UHUC.equiv C.1).counitIso

private abbrev _mapComp : _prelax.map ⟨F.1 ⋙ G.1⟩ ≅ _prelax.map F ⋙ _prelax.map G :=
  let ι₀ := (isoWhiskerRight (isoWhiskerLeft F.1 (UHUC.equiv.{v₂, u₂} D.1).unitIso.symm) G.down).symm
  let ι₁ := isoWhiskerRight (Functor.rightUnitor F.1).symm G.1 ≪≫ ι₀
    ≪≫ isoWhiskerRight (Functor.associator F.1 (UHUC.equiv ↑D.1).functor _).symm G.1
    ≪≫ (Functor.associator _ _ _)
  let ι₂ := isoWhiskerRight ι₁ _ ≪≫ (Functor.associator _ _ _) ≪≫ isoWhiskerLeft _ (Functor.associator _ _ _)
  isoWhiskerLeft _ ι₂ ≪≫ (Functor.associator _ _ _).symm


private lemma _map₂_whisker_left : _prelax.map₂ (F ◁ ϑ) = (_mapComp F G₁).hom ≫
      _prelax.map F ◁ _prelax.map₂ ϑ ≫ (_mapComp F G₂).inv := by
  revert C D E; rintro ⟨C⟩ ⟨D⟩ ⟨E⟩ ⟨F⟩ ⟨G₁⟩ ⟨G₂⟩ ⟨ϑ⟩
  unfold_projs; ext
  simp
  simp_rw [← (UHUC.equiv E.1).functor.map_comp]
  erw [ϑ.naturality_assoc]
  simp_rw [← G₂.map_comp, (UHUC.equiv D.1).unitIso.hom_inv_id_app]
  erw [G₂.map_id, Category.comp_id]

[Robert Maxton]

Offending nonterminal simp is in the last lemma; it expands into about ten lines of simp only on my screen, though probably two of those could be saved by giving certain long instance names shorter ones.

[Ruben Van de Velde]

You could use simp? says

[Robert Maxton]

How is that different from simp??