case hc
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : n < finrank K V
⊢ ↑n < ℵ₀

case hd
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : n < finrank K V
⊢ Module.rank K V < ℵ₀
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : n < finrank K V
⊢ ↑n < Module.rank K V
rwa [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0, toNat_cast]
no goals
case hc
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : n < finrank K V
⊢ ↑n < ℵ₀
exact nat_lt_aleph0 n
case hd
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : ℵ₀ ≤ Module.rank K V
⊢ finrank K V ≤ n
case hd
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : n < finrank K V
⊢ Module.rank K V < ℵ₀
contrapose! h
case hd
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : ℵ₀ ≤ Module.rank K V
⊢ 0 ≤ n
case hd
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : ℵ₀ ≤ Module.rank K V
⊢ finrank K V ≤ n
rw [finrank, Cardinal.toNat_apply_of_aleph0_le h]
no goals
case hd
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : ℵ₀ ≤ Module.rank K V
⊢ 0 ≤ n
exact n.zero_le