case intro
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : _root_.Finite K
inst✝ : FiniteDimensional K V
val✝ : Fintype K
⊢ _root_.Finite V
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : _root_.Finite K
inst✝ : FiniteDimensional K V
⊢ _root_.Finite V
cases nonempty_fintype K
case intro
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : _root_.Finite K
inst✝ : FiniteDimensional K V
val✝ : Fintype K
this : Fintype V
⊢ _root_.Finite V
case intro
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : _root_.Finite K
inst✝ : FiniteDimensional K V
val✝ : Fintype K
⊢ _root_.Finite V
haveI := fintypeOfFintype K V
no goals
case intro
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : _root_.Finite K
inst✝ : FiniteDimensional K V
val✝ : Fintype K
this : Fintype V
⊢ _root_.Finite V
infer_instance