K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K { x // x ∈ s }
inst✝ : FiniteDimensional K { x // x ∈ t }
key :
  Module.rank K { x // x ∈ s ⊔ t } + Module.rank K { x // x ∈ s ⊓ t } =
    Module.rank K { x // x ∈ s } + Module.rank K { x // x ∈ t }
⊢ finrank K { x // x ∈ s ⊔ t } + finrank K { x // x ∈ s ⊓ t } = finrank K { x // x ∈ s } + finrank K { x // x ∈ t }
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K { x // x ∈ s }
inst✝ : FiniteDimensional K { x // x ∈ t }
⊢ finrank K { x // x ∈ s ⊔ t } + finrank K { x // x ∈ s ⊓ t } = finrank K { x // x ∈ s } + finrank K { x // x ∈ t }
have key : Module.rank K ↑(s ⊔ t) + Module.rank K ↑(s ⊓ t) = Module.rank K s + Module.rank K t :=
  rank_sup_add_rank_inf_eq s t
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K { x // x ∈ s }
inst✝ : FiniteDimensional K { x // x ∈ t }
key :
  ↑(finrank K { x // x ∈ s ⊔ t }) + ↑(finrank K { x // x ∈ s ⊓ t }) =
    ↑(finrank K { x // x ∈ s }) + ↑(finrank K { x // x ∈ t })
⊢ finrank K { x // x ∈ s ⊔ t } + finrank K { x // x ∈ s ⊓ t } = finrank K { x // x ∈ s } + finrank K { x // x ∈ t }
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K { x // x ∈ s }
inst✝ : FiniteDimensional K { x // x ∈ t }
key :
  Module.rank K { x // x ∈ s ⊔ t } + Module.rank K { x // x ∈ s ⊓ t } =
    Module.rank K { x // x ∈ s } + Module.rank K { x // x ∈ t }
⊢ finrank K { x // x ∈ s ⊔ t } + finrank K { x // x ∈ s ⊓ t } = finrank K { x // x ∈ s } + finrank K { x // x ∈ t }
repeat' rw [← finrank_eq_rank] at key
no goals
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K { x // x ∈ s }
inst✝ : FiniteDimensional K { x // x ∈ t }
key :
  ↑(finrank K { x // x ∈ s ⊔ t }) + ↑(finrank K { x // x ∈ s ⊓ t }) =
    ↑(finrank K { x // x ∈ s }) + ↑(finrank K { x // x ∈ t })
⊢ finrank K { x // x ∈ s ⊔ t } + finrank K { x // x ∈ s ⊓ t } = finrank K { x // x ∈ s } + finrank K { x // x ∈ t }
norm_cast at key
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K { x // x ∈ s }
inst✝ : FiniteDimensional K { x // x ∈ t }
key :
  ↑(finrank K { x // x ∈ s ⊔ t }) + ↑(finrank K { x // x ∈ s ⊓ t }) =
    ↑(finrank K { x // x ∈ s }) + ↑(finrank K { x // x ∈ t })
⊢ finrank K { x // x ∈ s ⊔ t } + finrank K { x // x ∈ s ⊓ t } = finrank K { x // x ∈ s } + finrank K { x // x ∈ t }
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K { x // x ∈ s }
inst✝ : FiniteDimensional K { x // x ∈ t }
key :
  ↑(finrank K { x // x ∈ s ⊔ t }) + ↑(finrank K { x // x ∈ s ⊓ t }) =
    ↑(finrank K { x // x ∈ s }) + ↑(finrank K { x // x ∈ t })
⊢ finrank K { x // x ∈ s ⊔ t } + finrank K { x // x ∈ s ⊓ t } = finrank K { x // x ∈ s } + finrank K { x // x ∈ t }
rw [← finrank_eq_rank] at key