V : Type (u + 1)
inst✝ : LargeCategory V
G : MonCat
M N : Action V G
f : M ≅ N
g : ↑G
⊢ ((forget V G).mapIso f).hom ≫ ↑N.ρ g = ↑M.ρ g ≫ ((forget V G).mapIso f).hom
V : Type (u + 1)
inst✝ : LargeCategory V
G : MonCat
M N : Action V G
f : M ≅ N
g : ↑G
⊢ ↑N.ρ g = ↑(Iso.conj ((forget V G).mapIso f)) (↑M.ρ g)
rw [Iso.conj_apply, Iso.eq_inv_comp]
no goals
V : Type (u + 1)
inst✝ : LargeCategory V
G : MonCat
M N : Action V G
f : M ≅ N
g : ↑G
⊢ ((forget V G).mapIso f).hom ≫ ↑N.ρ g = ↑M.ρ g ≫ ((forget V G).mapIso f).hom
simp [f.hom.comm]