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✝ : FiniteDimensional K V
ι : Type w
p : ι → Submodule K V
hp : CompleteLattice.Independent p
⊢ lift (#{ i // p i ≠ ⊥ }) ≤ lift ↑(finrank 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₂
inst✝ : FiniteDimensional K V
ι : Type w
p : ι → Submodule K V
hp : CompleteLattice.Independent p
⊢ (#{ i // p i ≠ ⊥ }) ≤ ↑(finrank K V)
suffices Cardinal.lift.{v} (#{ i // p i ≠ ⊥ }) ≤ Cardinal.lift.{v} (finrank K V : Cardinal.{w}) by
  rwa [Cardinal.lift_le] at this
no goals
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✝ : FiniteDimensional K V
ι : Type w
p : ι → Submodule K V
hp : CompleteLattice.Independent p
⊢ lift (#{ i // p i ≠ ⊥ }) ≤ lift ↑(finrank K V)
calc
  Cardinal.lift.{v} (#{ i // p i ≠ ⊥ }) ≤ Cardinal.lift.{w} (Module.rank K V) :=
    hp.subtype_ne_bot_le_rank
  _ = Cardinal.lift.{w} (finrank K V : Cardinal.{v}) := by rw [finrank_eq_rank]
  _ = Cardinal.lift.{v} (finrank K V : Cardinal.{w}) := by simp
no goals
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✝ : FiniteDimensional K V
ι : Type w
p : ι → Submodule K V
hp : CompleteLattice.Independent p
this : lift (#{ i // p i ≠ ⊥ }) ≤ lift ↑(finrank K V)
⊢ (#{ i // p i ≠ ⊥ }) ≤ ↑(finrank K V)
rwa [Cardinal.lift_le] at this
no goals
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✝ : FiniteDimensional K V
ι : Type w
p : ι → Submodule K V
hp : CompleteLattice.Independent p
⊢ lift (Module.rank K V) = lift ↑(finrank K V)
rw [finrank_eq_rank]
no goals
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✝ : FiniteDimensional K V
ι : Type w
p : ι → Submodule K V
hp : CompleteLattice.Independent p
⊢ lift ↑(finrank K V) = lift ↑(finrank K V)
simp