simp lemma doesn't fire

Stream: general

[Robert Maxton]

Sorry I can't give a more useful title/problem description, hopefully I can edit one in later ^.^;

Suppose I define the WalkingQuiver the usual way (full #mwe at the end):

inductive WalkingQuiver where | zero | one deriving Inhabited

inductive WalkingQuiver.Hom : WalkingQuiver → WalkingQuiver → Type
| id X : WalkingQuiver.Hom X X
| source : WalkingQuiver.Hom .one .zero
| target: WalkingQuiver.Hom .one .zero

...

[Robert Maxton]

I can now express any quiver as a functor of the appropriate universe level, and this transformation is functorial; for later convenience I introduce an third universe level w, at the cost of having to supply explicit universe levels everywhere (but I'll need that anyway later):

def asFunctor_obj' (Q : Quiv.{v, u}) : WalkingQuiver ⥤ Type max w v u where
  obj
  | 0 => ULift.{max w v} Q.α
  | 1 => (s t : ULift.{max w v} Q.α) × (Q.str.Hom s.1 t.1)
  map
  | .id _ => ↾id
  | .source => ↾(·.1)
  | .target => ↾(·.2.1)
...

def asFunctor_map' {X Y : Quiv.{v, u}} (f : X ⟶ Y) :
    (asFunctor_obj' X ⟶ asFunctor_obj' Y) where
  app
  | 0 => ULift.map f.obj
  | 1 => ↾(fun ⟨s, t, hom⟩ ↦ ⟨ULift.map f.obj s, ULift.map f.obj t, f.map hom⟩)
  naturality m m' f' := by sorry

attribute [reducible] asFunctor_obj' asFunctor_map'

/-- Interpreting a quiver as a co-presheaf on the walking quiver, as a functor to the
category of presheaves. -/
@[simps]
def asFunctor : Quiv.{v, u} ⥤ WalkingQuiver ⥤ Type max w v u where
  obj := asFunctor_obj'
  map := asFunctor_map'
  map_id U := by
    simp [asFunctor_obj', asFunctor_map']
    rcongr m x
    cases m <;> aesop_cat

unif_hint hom_eq_asFunctor1 (X : Quiv.{v, u}) where
  ⊢ (s t : ULift.{max w v} X) × (s.1 ⟶ t.1) ≟ (asFunctor.{w}.obj X).obj 1

[Robert Maxton]

Now I define the src and tgt of an "edge" -- internally, of any element of type F.obj 1 for any F : WalkingQuiv ⥤ Type w -- and note that these are the components of a natural transformation:

def src {F : WalkingQuiver ⥤ Type w} (e : F.obj 1) : F.obj 0 :=
  F.map WalkingQuiver.Hom.source e

def tgt {F : WalkingQuiver ⥤ Type w} (e : F.obj 1) : F.obj 0 :=
  F.map WalkingQuiver.Hom.target e

section naturality
variable {F G : WalkingQuiver ⥤ Type w}
         (μ : F ⟶ G)

/-- Naturality of `src`. -/
@[simp]
lemma naturality_src {f : F.obj 1} : src (μ.app 1 f) = (μ.app 0 (src f)) := by
  simpa using congrFun (μ.naturality WalkingQuiver.Hom.source).symm f

/-- Naturality of `tgt`. -/
@[simp]
lemma naturality_tgt {f : F.obj 1} : tgt (μ.app 1 f) = (μ.app 0 (tgt f)) := by
  simpa using congrFun (μ.naturality WalkingQuiver.Hom.target).symm f
end naturality

[Robert Maxton]

However, these last simp lemmas don't fire properly:

instance : asFunctor.{w, v, u}.Full := ⟨fun {U V : Quiv.{v, u}} μ ↦ ⟨
  ⟨fun x => (μ.app 0 ⟨x⟩).down, fun f => asFunctor.natTransEdge μ f⟩, by
    ext q₀ x
    cases q₀ with
    | zero => sorry
    | one =>
      rcases x with ⟨⟨s⟩, ⟨t⟩, f⟩
      simp [asFunctor, asHom]
      ext <;> simp
      · -- simp [naturality_src] -- Makes no progress
        rw [naturality_src]; apply ULift.ext; simp
      · simp only [naturality_tgt] --magically works??
      ⟩⟩

• naturality_src works under rw, but not under simp
• naturality_tgt works under simp, but only after solving the first goal

[Robert Maxton]

Here's the full #mwe, and sorry it's not very "minimal"; since it kind of depends on the WalkingQuiver to Type construction I wasn't sure how much further I could reduce it. I'll keep at it, though.

import Mathlib.CategoryTheory.Category.Quiv

namespace CategoryTheory.Quiv
universe w v u

open CategoryTheory

inductive WalkingQuiver where | zero | one deriving Inhabited

inductive WalkingQuiver.Hom : WalkingQuiver → WalkingQuiver → Type
| id X : WalkingQuiver.Hom X X
| source : WalkingQuiver.Hom .one .zero
| target: WalkingQuiver.Hom .one .zero

def WalkingQuiver.forget : WalkingQuiver → Type
  | .zero => Bool
  | .one => Unit

instance (X Y : WalkingQuiver) :
    FunLike (WalkingQuiver.Hom X Y) (WalkingQuiver.forget X) (WalkingQuiver.forget Y) where
  coe
  | .id X => id
  | .source => fun _ => false
  | .target => fun _ => true
  coe_injective' X Y f := by
    cases X <;> cases Y <;> simp_all [funext_iff, WalkingQuiver.forget]


instance : Category WalkingQuiver where
  Hom := WalkingQuiver.Hom
  id := WalkingQuiver.Hom.id
  comp
    | WalkingQuiver.Hom.id _, g => g
    | f, WalkingQuiver.Hom.id _ => f
  id_comp f := by cases f <;> rfl
  comp_id f := by cases f <;> rfl
  assoc {W X Y Z} f g h := by sorry

instance : Zero WalkingQuiver := ⟨WalkingQuiver.zero⟩
instance : One WalkingQuiver := ⟨WalkingQuiver.one⟩

/-- Convenience recursor for `WalkingQuiver` in terms of the notation `0` and `1`. -/
@[elab_as_elim, cases_eliminator]
def casesOn' {motive : WalkingQuiver → Sort*}
    (m : WalkingQuiver) (zero : motive 0) (one : motive 1) : motive m :=
  match m with | 0 => zero | 1 => one

def src {F : WalkingQuiver ⥤ Type w} (e : F.obj 1) : F.obj 0 :=
  F.map WalkingQuiver.Hom.source e

def tgt {F : WalkingQuiver ⥤ Type w} (e : F.obj 1) : F.obj 0 :=
  F.map WalkingQuiver.Hom.target e

section naturality

variable {F G : WalkingQuiver ⥤ Type w}
         (μ : F ⟶ G)

/-- Naturality of `src`. -/
@[simp]
lemma naturality_src {f : F.obj 1} : src (μ.app 1 f) = (μ.app 0 (src f)) := by
  simpa using congrFun (μ.naturality WalkingQuiver.Hom.source).symm f


/-- Naturality of `tgt`. -/
@[simp]
lemma naturality_tgt {f : F.obj 1} : tgt (μ.app 1 f) = (μ.app 0 (tgt f)) := by
  simpa using congrFun (μ.naturality WalkingQuiver.Hom.target).symm f

end naturality

def asFunctor_obj' (Q : Quiv.{v, u}) : WalkingQuiver ⥤ Type max w v u where
  obj
  | 0 => ULift.{max w v} Q.α
  | 1 => (s t : ULift.{max w v} Q.α) × (Q.str.Hom s.1 t.1)
  map
  | .id _ => ↾id
  | .source => ↾(·.1)
  | .target => ↾(·.2.1)
  map_id m := by cases m <;> {unfold_projs; simp}
  map_comp {X Y Z} f g := by sorry

def asFunctor_map' {X Y : Quiv.{v, u}} (f : X ⟶ Y) :
    (asFunctor_obj' X ⟶ asFunctor_obj' Y) where
  app
  | 0 => ULift.map f.obj
  | 1 => ↾(fun ⟨s, t, hom⟩ ↦ ⟨ULift.map f.obj s, ULift.map f.obj t, f.map hom⟩)
  naturality m m' f' := by sorry


attribute [reducible] asFunctor_obj' asFunctor_map'

/-- Interpreting a quiver as a co-presheaf on the walking quiver, as a functor to the
category of presheaves. -/
@[simps]
def asFunctor : Quiv.{v, u} ⥤ WalkingQuiver ⥤ Type max w v u where
  obj := asFunctor_obj'
  map := asFunctor_map'
  map_id U := by
    simp [asFunctor_obj', asFunctor_map']
    rcongr m x
    cases m <;> aesop_cat

unif_hint hom_eq_asFunctor1 (X : Quiv.{v, u}) where
  ⊢ (s t : ULift.{max w v} X) × (s.1 ⟶ t.1) ≟ (asFunctor.{w}.obj X).obj 1

@[ext]
lemma asFunctor.hom_ext {X : Quiv} (f g : (s t :  ULift X) × (s.1 ⟶ t.1))
    (hs : src f = src g) (ht : tgt f = tgt g) (he : HEq f.2.2 g.2.2) : f = g := by
  rcases f with ⟨fs, ft, fe⟩
  rcases g with ⟨gs, gt, ge⟩
  simp_all only [src, tgt, asFunctor_obj_map, asHom, ULift.up_inj]
  cases hs; cases ht
  congr
  exact heq_iff_eq.mp he

@[simp] lemma src_asFunctor {X : Quiv.{v, u}} {s t : ULift X} (e : (s.1 ⟶ t.1)) :
  @src (asFunctor.{w}.obj X) (⟨s, t, e⟩ : (asFunctor.{w}.obj X).obj 1) = s := rfl

def asFunctor.natTransEdge {X Y : Quiv.{v, u}}
    (μ : asFunctor.{w}.obj X ⟶ asFunctor.{w}.obj Y) {s t : X} (f : s ⟶ t) :
    Y.str.Hom (μ.app 0 ⟨s⟩).1 (μ.app 0 ⟨t⟩).1 :=
  Quiver.homOfEq (μ.app 1 ⟨⟨s⟩, ⟨t⟩, f⟩).2.2
    (congrArg ULift.down <| naturality_src μ) (congrArg ULift.down <| naturality_tgt μ)

instance : asFunctor.{w, v, u}.Full := ⟨fun {U V : Quiv.{v, u}} μ ↦ ⟨
  ⟨fun x => (μ.app 0 ⟨x⟩).down, fun f => asFunctor.natTransEdge μ f⟩, by
    -- This is a simplification of what's happening in the actual code
    ext q₀ x
    cases q₀ with
    | zero => sorry
    | one =>
      rcases x with ⟨⟨s⟩, ⟨t⟩, f⟩
      simp [asFunctor, asHom]
      ext <;> simp [naturality_src]
      · -- simp -- Makes no progress
        rw [naturality_src]; apply ULift.ext; simp
      · simp only [naturality_tgt] --magically works??
      ⟩⟩


#min_imports

[Robert Maxton]

As you might expect, the behavior is symmetric; it doesn't matter which of src or tgt I solve first, once I solve one with a rw the other can be simplified normally