V : Type (u + 1)
inst✝ : LargeCategory V
G : MonCat
A : Action V G
⊢ 1 = 𝟙 A.V
V : Type (u + 1)
inst✝ : LargeCategory V
G : MonCat
A : Action V G
⊢ ↑A.ρ 1 = 𝟙 A.V
rw [MonoidHom.map_one]
no goals
V : Type (u + 1)
inst✝ : LargeCategory V
G : MonCat
A : Action V G
⊢ 1 = 𝟙 A.V
rfl