case mk
M : Type u_1
inst✝¹ : Monoid M
X : Type u
inst✝ : MulAction M X
fst✝ : SingleObj M
snd✝ : (actionAsFunctor M X).obj fst✝
⊢ { fst := (), snd := ActionCategory.back { fst := fst✝, snd := snd✝ } } = { fst := fst✝, snd := snd✝ }
M : Type u_1
inst✝¹ : Monoid M
X : Type u
inst✝ : MulAction M X
x : ActionCategory M X
⊢ { fst := (), snd := ActionCategory.back x } = x
cases x
no goals
case mk
M : Type u_1
inst✝¹ : Monoid M
X : Type u
inst✝ : MulAction M X
fst✝ : SingleObj M
snd✝ : (actionAsFunctor M X).obj fst✝
⊢ { fst := (), snd := ActionCategory.back { fst := fst✝, snd := snd✝ } } = { fst := fst✝, snd := snd✝ }
rfl