no goals
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₂
s t : Submodule K V
le : s ≤ t
lt : finrank K { x // x ∈ s } < finrank K { x // x ∈ t }
h : s = t
⊢ finrank K { x // x ∈ s } = finrank K { x // x ∈ t }
rw [h]