[GOAL]
J✝ : Type
inst✝⁴ : SmallCategory J✝
inst✝³ : FinCategory J✝
k : Type v
inst✝² : Field k
J : Type
inst✝¹ : Fintype J
Z : J → ModuleCat k
inst✝ : ∀ (j : J), FiniteDimensional k ↑(Z j)
⊢ FiniteDimensional k ↑(ModuleCat.of k ((j : J) → ↑(Z j)))
[PROOFSTEP]
unfold ModuleCat.of
[GOAL]
J✝ : Type
inst✝⁴ : SmallCategory J✝
inst✝³ : FinCategory J✝
k : Type v
inst✝² : Field k
J : Type
inst✝¹ : Fintype J
Z : J → ModuleCat k
inst✝ : ∀ (j : J), FiniteDimensional k ↑(Z j)
⊢ FiniteDimensional k ↑(ModuleCat.mk ((j : J) → ↑(Z j)))
[PROOFSTEP]
infer_instance
[GOAL]
J✝ : Type
inst✝⁴ : SmallCategory J✝
inst✝³ : FinCategory J✝
k : Type v
inst✝² : Field k
J : Type
inst✝¹ : Fintype J
Z : J → ModuleCat k
inst✝ : ∀ (j : J), FiniteDimensional k ↑(Z j)
this : FiniteDimensional k ↑(ModuleCat.of k ((j : J) → ↑(Z j)))
⊢ Mono (ModuleCat.piIsoPi fun j => Z j).hom
[PROOFSTEP]
infer_instance
[GOAL]
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
k : Type v
inst✝ : Field k
F : J ⥤ FGModuleCat k
⊢ ∀ (j : J), FiniteDimensional k ↑((F ⋙ forget₂ (FGModuleCat k) (ModuleCat k)).obj j)
[PROOFSTEP]
intro j
[GOAL]
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
k : Type v
inst✝ : Field k
F : J ⥤ FGModuleCat k
j : J
⊢ FiniteDimensional k ↑((F ⋙ forget₂ (FGModuleCat k) (ModuleCat k)).obj j)
[PROOFSTEP]
change FiniteDimensional k (F.obj j)
[GOAL]
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
k : Type v
inst✝ : Field k
F : J ⥤ FGModuleCat k
j : J
⊢ FiniteDimensional k ↑(F.obj j)
[PROOFSTEP]
infer_instance
