change in behaviour with `simps`

Stream: mathlib4

[Kevin Buzzard]

I don't know anything about Kan extensions but I've traced back a failure with simp in !4#3703 (which I haven't yet fixed) to the following issue:

import Mathlib.CategoryTheory.Limits.KanExtension


#check CategoryTheory.lan_map_app
/-
⊢ ∀ {S : Type u₁} {L : Type u₂} {D : Type u₃} [inst : CategoryTheory.Category S] [inst_1 : CategoryTheory.Category L]
  [inst_2 : CategoryTheory.Category D] (ι : S ⥤ L)
  [inst_3 : ∀ (X : L), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.CostructuredArrow ι X) D] {X X' : S ⥤ D}
  (f : X ⟶ X') (x : L),
  ((CategoryTheory.lan ι).map f).app x =
    CategoryTheory.Limits.colimit.desc (CategoryTheory.Lan.diagram ι X x)
      { pt := CategoryTheory.Limits.colimit (CategoryTheory.Lan.diagram ι X' x),
        ι :=
          CategoryTheory.NatTrans.mk fun i ↦
            (f.app i.left ≫
+                (↑(CategoryTheory.Lan.equiv ι X' (CategoryTheory.Lan.loc ι X')) (𝟙 (CategoryTheory.Lan.loc ι X'))).app
+                  i.left) ≫
              CategoryTheory.Limits.colimit.pre (CategoryTheory.Lan.diagram ι X' x)
                (CategoryTheory.CostructuredArrow.map i.hom) }
                -/

/-
Lean 3:

category_theory.Lan_map_app :
  ∀ (ι : ?M_1 ⥤ ?M_2)
  [_inst_4 :
    ∀ (X : ?M_2), category_theory.limits.has_colimits_of_shape (category_theory.costructured_arrow ι X) ?M_3]
  (X X' : ?M_1 ⥤ ?M_3) (f : X ⟶ X') (x : ?M_2),
    ((category_theory.Lan ι).map f).app x =
      category_theory.limits.colimit.desc (category_theory.Lan.diagram ι X x)
        {X := category_theory.limits.colimit (category_theory.Lan.diagram ι X' x) _,
         ι := {app := λ (i : category_theory.costructured_arrow ι x),
                        (f.app i.left ≫
+                             category_theory.limits.colimit.ι (category_theory.Lan.diagram ι X' (ι.obj i.left))
+                                 (category_theory.costructured_arrow.mk (𝟙 (ι.obj i.left))) ≫
+                               𝟙
+                                 (category_theory.limits.colimit
+                                    (category_theory.Lan.diagram ι X' (ι.obj i.left)))) ≫
                          category_theory.limits.colimit.pre (category_theory.Lan.diagram ι X' x)
                            (category_theory.costructured_arrow.map i.hom),
               naturality' := _}}

-/

I've posted both the Lean 4 and Lean 3 types of lan_map_app and noted the lines where they differ definitionally with + on the left. I tried to prove the equality of these two subterms with simp but I couldn't get it to work so I'm stuck, but I am prepared to work more on this if someone can suggest anything productive to investigate.

[Kevin Buzzard]

Aah, progress: the proof that the two marked areas are equal is not rfl but Category.comp_id. This should get me through.