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₂
S₁ S₂ : Submodule K V
inst✝ : FiniteDimensional K { x // x ∈ S₂ }
hle : S₁ ≤ S₂
hd : finrank K { x // x ∈ S₂ } ≤ finrank K { x // x ∈ comap (Submodule.subtype S₂) S₁ }
⊢ S₁ = S₂
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₂
S₁ S₂ : Submodule K V
inst✝ : FiniteDimensional K { x // x ∈ S₂ }
hle : S₁ ≤ S₂
hd : finrank K { x // x ∈ S₂ } ≤ finrank K { x // x ∈ S₁ }
⊢ S₁ = S₂
rw [← LinearEquiv.finrank_eq (Submodule.comapSubtypeEquivOfLe hle)] at hd
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₂
S₁ S₂ : Submodule K V
inst✝ : FiniteDimensional K { x // x ∈ S₂ }
hle : S₁ ≤ S₂
hd : finrank K { x // x ∈ S₂ } ≤ finrank K { x // x ∈ comap (Submodule.subtype S₂) S₁ }
⊢ S₁ = S₂
exact le_antisymm hle (Submodule.comap_subtype_eq_top.1
  (eq_top_of_finrank_eq (le_antisymm (comap (Submodule.subtype S₂) S₁).finrank_le hd)))