V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
H : GroupCat
X : Action V ((forget₂ GroupCat MonCat).obj H)
inst✝ : RightRigidCategory V
h : ↑H
⊢ ↑Xᘁ.ρ h = ↑X.ρ (inv h)ᘁ

case x
V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
H : GroupCat
X : Action V ((forget₂ GroupCat MonCat).obj H)
inst✝ : RightRigidCategory V
h : ↑H
⊢ SingleObj H.1

case y
V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
H : GroupCat
X : Action V ((forget₂ GroupCat MonCat).obj H)
inst✝ : RightRigidCategory V
h : ↑H
⊢ SingleObj H.1
V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
H : GroupCat
X : Action V ((forget₂ GroupCat MonCat).obj H)
inst✝ : RightRigidCategory V
h : ↑H
⊢ ↑Xᘁ.ρ h = ↑X.ρ h⁻¹ᘁ
rw [← SingleObj.inv_as_inv]
no goals
V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
H : GroupCat
X : Action V ((forget₂ GroupCat MonCat).obj H)
inst✝ : RightRigidCategory V
h : ↑H
⊢ ↑Xᘁ.ρ h = ↑X.ρ (inv h)ᘁ

case x
V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
H : GroupCat
X : Action V ((forget₂ GroupCat MonCat).obj H)
inst✝ : RightRigidCategory V
h : ↑H
⊢ SingleObj H.1

case y
V : Type (u + 1)
inst✝² : LargeCategory V
G : MonCat
inst✝¹ : MonoidalCategory V
H : GroupCat
X : Action V ((forget₂ GroupCat MonCat).obj H)
inst✝ : RightRigidCategory V
h : ↑H
⊢ SingleObj H.1
rfl