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₂
ι : Type w
inst✝ : _root_.Finite ι
h : Basis ι K V
val✝ : Fintype ι
⊢ FiniteDimensional K 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₂
ι : Type w
inst✝ : _root_.Finite ι
h : Basis ι K V
⊢ FiniteDimensional K V
cases nonempty_fintype ι
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₂
ι : Type w
inst✝ : _root_.Finite ι
h : Basis ι K V
val✝ : Fintype ι
⊢ FiniteDimensional K V
exact ⟨⟨Finset.univ.image h, by
  convert h.span_eq
  simp⟩⟩
case h.e'_2.h.e'_6
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₂
ι : Type w
inst✝ : _root_.Finite ι
h : Basis ι K V
val✝ : Fintype ι
⊢ ↑(Finset.image (↑h) Finset.univ) = Set.range ↑h
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₂
ι : Type w
inst✝ : _root_.Finite ι
h : Basis ι K V
val✝ : Fintype ι
⊢ span K ↑(Finset.image (↑h) Finset.univ) = ⊤
convert h.span_eq
no goals
case h.e'_2.h.e'_6
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₂
ι : Type w
inst✝ : _root_.Finite ι
h : Basis ι K V
val✝ : Fintype ι
⊢ ↑(Finset.image (↑h) Finset.univ) = Set.range ↑h
simp