case h.e'_4
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₂
n : ℕ
inst✝ : Fact (finrank K V = n + 1)
⊢ finrank K V = Nat.succ n
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₂
n : ℕ
inst✝ : Fact (finrank K V = n + 1)
⊢ 0 < finrank K V
convert Nat.succ_pos n
no goals
case h.e'_4
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₂
n : ℕ
inst✝ : Fact (finrank K V = n + 1)
⊢ finrank K V = Nat.succ n
apply Fact.out