-- Mathlib/LinearAlgebra/Dimension/RankNullity.lean
lemma Submodule.exists_of_finrank_lt (N : Submodule R M) (h : finrank R N < finrank R M) :
    ∃ m : M, ∀ r : R, r ≠ 0 → r • m ∉ N

Proof state:
R : Type u_1
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : HasRankNullity.{u, u_1} R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
h : finrank R ↥N < finrank R M
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N

Tactic:
obtain ⟨s, hs, hs'⟩ :=
  exists_finset_linearIndependent_of_le_finrank (R := R) (M := M ⧸ N) le_rfl

Result:
case intro.intro
R : Type u_1
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : HasRankNullity.{u, u_1} R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N

Proof state:
case intro.intro.intro.intro
R : Type u_1
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : HasRankNullity.{u, u_1} R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M
hv : N.mkQ v ∈ s
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N

Tactic:
refine ⟨v, fun r hr ↦ mt ?_ hr⟩

Result:
case intro.intro.intro.intro
R : Type u_1
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : HasRankNullity.{u, u_1} R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M
hv : N.mkQ v ∈ s
r : R
hr : r ≠ 0
⊢ r • v ∈ N → r = 0

Proof state:
case intro.intro.intro.intro
R : Type u_1
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : HasRankNullity.{u, u_1} R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M
hv : N.mkQ v ∈ s
r : R
hr : r ≠ 0
⊢ r • v ∈ N → r = 0

Tactic:
have := linearIndependent_iff.mp hs' (Finsupp.single ⟨_, hv⟩ r)

Result:
case intro.intro.intro.intro
R : Type u_1
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : HasRankNullity.{u, u_1} R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M
hv : N.mkQ v ∈ s
r : R
hr : r ≠ 0
this :
  (Finsupp.linearCombination R Subtype.val) (Finsupp.single ⟨N.mkQ v, hv⟩ r) = 0 → Finsupp.single ⟨N.mkQ v, hv⟩ r = 0
⊢ r • v ∈ N → r = 0

Proof state:
case intro.intro.intro
R : Type u_1
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : HasRankNullity.{u, u_1} R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M ⧸ N
hv : v ∈ s
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N

Tactic:
obtain ⟨v, rfl⟩ := N.mkQ_surjective v

Result:
case intro.intro.intro.intro
R : Type u_1
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : HasRankNullity.{u, u_1} R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M
hv : N.mkQ v ∈ s
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N

Proof state:
R : Type u_1
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : HasRankNullity.{u, u_1} R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
⊢ s.Nonempty

Tactic:
rwa [Finset.nonempty_iff_ne_empty, ne_eq, ← Finset.card_eq_zero,
hs, finrank_quotient, tsub_eq_zero_iff_le, not_le]

Result:
no goals

Proof state:
case intro.intro.intro.intro
R : Type u_1
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : HasRankNullity.{u, u_1} R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M
hv : N.mkQ v ∈ s
r : R
hr : r ≠ 0
this :
  (Finsupp.linearCombination R Subtype.val) (Finsupp.single ⟨N.mkQ v, hv⟩ r) = 0 → Finsupp.single ⟨N.mkQ v, hv⟩ r = 0
⊢ r • v ∈ N → r = 0

Tactic:
rwa [Finsupp.linearCombination_single, Finsupp.single_eq_zero, ← LinearMap.map_smul,
  Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero] at this

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : HasRankNullity.{u, u_1} R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N

Tactic:
obtain ⟨v, hv⟩ : s.Nonempty := by rwa [Finset.nonempty_iff_ne_empty, ne_eq, ← Finset.card_eq_zero,
  hs, finrank_quotient, tsub_eq_zero_iff_le, not_le]

Result:
case intro.intro.intro
R : Type u_1
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : HasRankNullity.{u, u_1} R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M ⧸ N
hv : v ∈ s
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N