Defining Natural Transformations with Whiskers question

Stream: mathlib4

[Mason McBride]

open CategoryTheory Functor
open CategoryTheory NatTrans
variable {A : Type u₀} {Z : Type u₃} [Category.{v₀} A] [Category.{v₃} Z]

variable {F F' : C ⥤ D} {G : A ⥤ C} {E : D ⥤ Z}
variable {φ : NatTrans F F'}

def Eφ : F ⋙ E ⟶ F' ⋙ E := whiskerRight φ E
def Gφ : G ⋙ F ⟶ G ⋙ F' :=  whiskerLeft G φ

def Eφ_NatTrans : NatTrans (F ⋙ E) (F' ⋙ E) where
  app c := (whiskerRight φ E).app c
  naturality := Eφ.naturality

For def Eφ_NatTrans, this is the only configuration i can use that doesn't give me an error. I would ideally like to define def Eφ_NatTrans in terms of Eφ without having to construct it again. Any help?

[Mason McBride]

def φG_NatTrans : NatTrans (G ⋙ F) (G ⋙ F') where
  app b := φG.app b
  naturality := φG.naturality

The error it gives me when I define it like this for example: "don't know how to synthesize placeholder"

[Kim Morrison]

The problem is these are variables. Look at the signature of Eφ (e.g. by hovering). There's no "fixed" F F' G E in this file: in each declaration they could be different.

Solution: variable (F F' : C ⥤ D) (G : A ⥤ C) (E : D ⥤ Z) That is, don't use implicit arguments for non-inferrable arguments (unless you're planning to infer them from the expected type, as we often do for theorems).