-- Mathlib/LinearAlgebra/Dimension/RankNullity.lean
theorem Submodule.exists_smul_not_mem_of_rank_lt {N : Submodule R M}
    (h : Module.rank R N < Module.rank 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
N : Submodule R M
h : Module.rank R ↥N < Module.rank R ↥N
e : Module.rank R (M ⧸ N) = 0
⊢ False

Tactic:
exact h.ne rfl

Result:
no goals

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
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
this : ¬∀ (x : M), ∃ a, a ≠ 0 ∧ a • Quotient.mk x = 0
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N

Tactic:
push_neg at this

Result:
R : Type u_1
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : HasRankNullity.{u, u_1} R
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
this : ∃ x, ∀ (a : R), a ≠ 0 → a • Quotient.mk x ≠ 0
⊢ ∃ 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
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
e : Module.rank R (M ⧸ N) = 0
⊢ False

Tactic:
rw [← rank_quotient_add_rank N, e, zero_add] at h

Result:
R : Type u_1
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : HasRankNullity.{u, u_1} R
N : Submodule R M
h : Module.rank R ↥N < Module.rank R ↥N
e : Module.rank R (M ⧸ N) = 0
⊢ False

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
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
this : ∃ x, ∀ (a : R), ¬a = 0 → a • x ∉ N
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N

Tactic:
exact this

Result:
no goals

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
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
⊢ Module.rank R (M ⧸ N) ≠ 0

Tactic:
intro e

Result:
R : Type u_1
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : HasRankNullity.{u, u_1} R
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
e : Module.rank R (M ⧸ N) = 0
⊢ False

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
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
this : ∃ x, ∀ (a : R), a ≠ 0 → a • Quotient.mk x ≠ 0
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N

Tactic:
simp_rw [← N.mkQ_apply, ← map_smul, N.mkQ_apply, ne_eq, Submodule.Quotient.mk_eq_zero] at this

Result:
R : Type u_1
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : HasRankNullity.{u, u_1} R
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
this : ∃ x, ∀ (a : R), ¬a = 0 → a • x ∉ N
⊢ ∃ 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
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N

Tactic:
have : Module.rank R (M ⧸ N) ≠ 0 := by
  intro e
  rw [← rank_quotient_add_rank N, e, zero_add] at h
  exact h.ne rfl

Result:
R : Type u_1
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : HasRankNullity.{u, u_1} R
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
this : Module.rank R (M ⧸ N) ≠ 0
⊢ ∃ 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
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
this : Module.rank R (M ⧸ N) ≠ 0
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N

Tactic:
rw [ne_eq, rank_eq_zero_iff, (Submodule.Quotient.mk_surjective N).forall] at this

Result:
R : Type u_1
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : HasRankNullity.{u, u_1} R
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
this : ¬∀ (x : M), ∃ a, a ≠ 0 ∧ a • Quotient.mk x = 0
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N