Rewrite by defeq yields "motive not type correct"

Stream: general

[Junyan Xu]

#mwe

import category_theory.functor_category
open category_theory
variables {C D E F G : Type*} [category C] [category D] [category E] [category F] [category G]
(H : C ⥤ D) (I : D ⥤ E) (J₁ J₂ : E ⥤ F) (α : J₁ ⟶ J₂) (K : F ⥤ G) (c : C) (g : G)
(f : K.obj (J₂.obj (I.obj (H.obj c))) ⟶ g)

example : α.app (I.obj (H.obj c)) = α.app ((H ⋙ I).obj c) :=
by { rw H.comp_obj } /- motive not type correct -/

example : α.app (I.obj (H.obj c)) = α.app ((H ⋙ I).obj c) :=
by { erw H.comp_obj } /- goals accomplished -/

example : K.map (α.app (I.obj (H.obj c))) = K.map (α.app ((H ⋙ I).obj c)) :=
by { erw H.comp_obj } /- goals accomplished -/

example : K.map (α.app (I.obj (H.obj c))) ≫ f = K.map (α.app ((H ⋙ I).obj c)) ≫ f :=
by { erw H.comp_obj } /- motive not type correct !! -/

All goals can actually be solved by rfl, but not being able to use rw means I have to write down the whole equality. Is there any way to improve rw to work in these circumstances? Or maybe another eerw tactic? The last example naturally arises in my attempt to show that a family of adjunctions (e.g. presheaf pullback-pushforward adjunction for each morphism in Top) transfers a pseudofunctor to a pseudofunctor, using results in adjunction/mates.

[Junyan Xu]

just tried dsimp only [H.comp_obj] and it fails to simplify ...

[Reid Barton]

dsimp works alone or with only [category_theory.functor.comp_obj], not sure why it doesn't work with only [H.comp_obj]. Also not sure why erw ever would work.

[Reid Barton]

Maybe we should have some kind of drw or dsimp_rw

[Reid Barton]

This also doesn't work

example {n : ℕ} : n + 0 = n := by { dsimp [nat.add_zero n], }

Maybe passing arguments to lemmas for dsimp messes up its rfl-lemma thing?

[Reid Barton]

My strategy for this kind of reasoning was normally to get into a state where something like simp, dsimp, simp would work (= close the goal)

[Reid Barton]

another style that would work is

example : K.map (α.app (I.obj (H.obj c))) ≫ f = K.map (α.app ((H ⋙ I).obj c)) ≫ f :=
by { change I.obj (H.obj c) with (H ⋙ I).obj c, sorry }

[Junyan Xu]

dsimp works with only [category_theory.functor.comp_obj]

Thank you! This is gonna be a life saver. I didn't even know change can be used with with to specify where to change; I tried change once but it didn't work. Here I actually need to rewrite in the reverse direction then apply naturality (can't rw or erw naturality directly) in the reverse direction, and after that still need to rewrite by map_comp, assoc, and a triangle identity, and those can be done by simp (if it doesn't undo the rw <- naturality). Unfortuantley I don't have time to complete the proofs until ~7 hours later.

[Junyan Xu]

The relevant part of the goal at this step is

((adj f').unit.app ((Rmap f').obj ((Rmap (𝟙 X)).obj x)) ≫
(Rmap f').map ((L.map_id X).app ((L.to_prefunctor.map f').obj ((Rmap f').obj ((Rmap (𝟙 X)).obj x))) ≫ (
L.to_prefunctor.map (𝟙 X)).map ((adj f').counit.app ((Rmap (𝟙 X)).obj x)) ≫
(adj (𝟙 X)).counit.app x))

The middle two lines are gonna be rewritten by naturality, and then cancel with the first line by triangle identity. The (Rmap f').obj ((Rmap (𝟙 X)).obj came from Rmap (𝟙 X) ⋙ Rmap f' via dsimp.

[Junyan Xu]

I guess it would go smoothly with simps after rewriting the right hand side with triangle identity ...