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✝ : FiniteDimensional K V
v : ι → V
h : LinearIndependent K v
⊢ lift (#ι) < lift ℵ₀
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✝ : FiniteDimensional K V
v : ι → V
h : LinearIndependent K v
⊢ (#ι) < ℵ₀
apply Cardinal.lift_lt.1
case a
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✝ : FiniteDimensional K V
v : ι → V
h : LinearIndependent K v
⊢ lift (#ι) ≤ ?b

case a
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✝ : FiniteDimensional K V
v : ι → V
h : LinearIndependent K v
⊢ ?b < lift ℵ₀

case b
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✝ : FiniteDimensional K V
v : ι → V
h : LinearIndependent K v
⊢ Cardinal
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✝ : FiniteDimensional K V
v : ι → V
h : LinearIndependent K v
⊢ lift (#ι) < lift ℵ₀
apply lt_of_le_of_lt
case a
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✝ : FiniteDimensional K V
v : ι → V
h : LinearIndependent K v
⊢ lift (Module.rank K V) < lift ℵ₀
case a
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✝ : FiniteDimensional K V
v : ι → V
h : LinearIndependent K v
⊢ lift (#ι) ≤ ?b

case a
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✝ : FiniteDimensional K V
v : ι → V
h : LinearIndependent K v
⊢ ?b < lift ℵ₀

case b
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✝ : FiniteDimensional K V
v : ι → V
h : LinearIndependent K v
⊢ Cardinal
apply cardinal_lift_le_rank_of_linearIndependent h
case a
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✝ : FiniteDimensional K V
v : ι → V
h : LinearIndependent K v
⊢ ↑(finrank K V) < ℵ₀
case a
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✝ : FiniteDimensional K V
v : ι → V
h : LinearIndependent K v
⊢ lift (Module.rank K V) < lift ℵ₀
rw [← finrank_eq_rank, Cardinal.lift_aleph0, Cardinal.lift_natCast]
no goals
case a
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✝ : FiniteDimensional K V
v : ι → V
h : LinearIndependent K v
⊢ ↑(finrank K V) < ℵ₀
apply Cardinal.nat_lt_aleph0