-- Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
theorem _root_.Submodule.eq_top_of_finrank_eq [FiniteDimensional K V] {S : Submodule K V}
    (h : finrank K S = finrank K V) : S = ⊤

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
this : IsNoetherian K V
⊢ S = ⊤

Tactic:
set bS := Basis.ofVectorSpace K S with bS_eq

Result:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
this : IsNoetherian K V
bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
⊢ S = ⊤

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
this✝ : IsNoetherian K V
bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this : LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K ↥S)
b : Basis (↑(this.extend ⋯)) K V := Basis.extend this
b_eq : b = Basis.extend this
i1 : Fintype ↑(this.extend ⋯) := ⋯.fintype
i2 : Fintype ↑(Subtype.val '' Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype
i3 : Fintype ↑(Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype
⊢ Fintype.card ↑(this.extend ⋯) ≤ Fintype.card ↑(Subtype.val '' Basis.ofVectorSpaceIndex K ↥S)

Tactic:
rw [Set.card_image_of_injective _ Subtype.coe_injective, ← finrank_eq_card_basis bS, ←
    finrank_eq_card_basis b, h]

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
this✝ : IsNoetherian K V
bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this : LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K ↥S)
b : Basis (↑(this.extend ⋯)) K V := Basis.extend this
b_eq : b = Basis.extend this
i1 : Fintype ↑(this.extend ⋯) := ⋯.fintype
i2 : Fintype ↑(Subtype.val '' Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype
⊢ LinearIndependent ?m.67073 Subtype.val

Tactic:
simpa [bS] using bS.linearIndependent

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
this✝² : IsNoetherian K V
bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this✝¹ : LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K ↥S)
b : Basis (↑(this✝¹.extend ⋯)) K V := Basis.extend this✝¹
b_eq : b = Basis.extend this✝¹
i1 : Fintype ↑(this✝¹.extend ⋯) := ⋯.fintype
i2 : Fintype ↑(Subtype.val '' Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype
i3 : Fintype ↑(Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype
this✝ : Subtype.val '' Basis.ofVectorSpaceIndex K ↥S = this✝¹.extend ⋯
this : span K (Set.range ⇑bS) = ⊤
⊢ S = Submodule.map S.subtype (span K (Basis.ofVectorSpaceIndex K ↥S))

Tactic:
rw [bS_eq, Basis.coe_ofVectorSpace, Subtype.range_coe] at this

Result:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
this✝² : IsNoetherian K V
bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this✝¹ : LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K ↥S)
b : Basis (↑(this✝¹.extend ⋯)) K V := Basis.extend this✝¹
b_eq : b = Basis.extend this✝¹
i1 : Fintype ↑(this✝¹.extend ⋯) := ⋯.fintype
i2 : Fintype ↑(Subtype.val '' Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype
i3 : Fintype ↑(Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype
this✝ : Subtype.val '' Basis.ofVectorSpaceIndex K ↥S = this✝¹.extend ⋯
this : span K (Basis.ofVectorSpaceIndex K ↥S) = ⊤
⊢ S = Submodule.map S.subtype (span K (Basis.ofVectorSpaceIndex K ↥S))

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
this✝² : IsNoetherian K V
bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this✝¹ : LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K ↥S)
b : Basis (↑(this✝¹.extend ⋯)) K V := Basis.extend this✝¹
b_eq : b = Basis.extend this✝¹
i1 : Fintype ↑(this✝¹.extend ⋯) := ⋯.fintype
i2 : Fintype ↑(Subtype.val '' Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype
i3 : Fintype ↑(Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype
this✝ : Subtype.val '' Basis.ofVectorSpaceIndex K ↥S = this✝¹.extend ⋯
this : span K (Basis.ofVectorSpaceIndex K ↥S) = ⊤
⊢ S = Submodule.map S.subtype (span K (Basis.ofVectorSpaceIndex K ↥S))

Tactic:
rw [this, Submodule.map_top (Submodule.subtype S), range_subtype]

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
this✝ : IsNoetherian K V
bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this : LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K ↥S)
⊢ S = ⊤

Tactic:
set b := Basis.extend this with b_eq

Result:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
this✝ : IsNoetherian K V
bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this : LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K ↥S)
b : Basis (↑(this.extend ⋯)) K V := Basis.extend this
b_eq : b = Basis.extend this
⊢ S = ⊤

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
this✝¹ : IsNoetherian K V
bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this✝ : LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K ↥S)
b : Basis (↑(this✝.extend ⋯)) K V := Basis.extend this✝
b_eq : b = Basis.extend this✝
i1 : Fintype ↑(this✝.extend ⋯) := ⋯.fintype
i2 : Fintype ↑(Subtype.val '' Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype
i3 : Fintype ↑(Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype
this : Subtype.val '' Basis.ofVectorSpaceIndex K ↥S = this✝.extend ⋯
⊢ S = ⊤

Tactic:
rw [← b.span_eq, b_eq, Basis.coe_extend, Subtype.range_coe, ← this, ← Submodule.coe_subtype,
  span_image]

Result:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
this✝¹ : IsNoetherian K V
bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this✝ : LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K ↥S)
b : Basis (↑(this✝.extend ⋯)) K V := Basis.extend this✝
b_eq : b = Basis.extend this✝
i1 : Fintype ↑(this✝.extend ⋯) := ⋯.fintype
i2 : Fintype ↑(Subtype.val '' Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype
i3 : Fintype ↑(Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype
this : Subtype.val '' Basis.ofVectorSpaceIndex K ↥S = this✝.extend ⋯
⊢ S = Submodule.map S.subtype (span K (Basis.ofVectorSpaceIndex K ↥S))