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
U W : Submodule K V
h : IsCompl U W
⊢ finrank K { x // x ∈ ⊤ } = 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
U W : Submodule K V
h : IsCompl U W
⊢ finrank K { x // x ∈ U } + finrank K { x // x ∈ W } = finrank K V
rw [← finrank_sup_add_finrank_inf_eq, h.codisjoint.eq_top, h.disjoint.eq_bot, finrank_bot,
  add_zero]
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
U W : Submodule K V
h : IsCompl U W
⊢ finrank K { x // x ∈ ⊤ } = finrank K V
exact finrank_top _ _