-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem finrank_le_one (v : M) (h : ∀ w : M, ∃ c : R, c • v = w) : finrank R M ≤ 1

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : StrongRankCondition R
v : M
h : ∀ (w : M), ∃ c, c • v = w
this : Nontrivial R
⊢ finrank R M ≤ 1

Tactic:
rcases eq_or_ne v 0 with (rfl | hn)

Result:
case inl
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : StrongRankCondition R
this : Nontrivial R
h : ∀ (w : M), ∃ c, c • 0 = w
⊢ finrank R M ≤ 1

case inr
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : StrongRankCondition R
v : M
h : ∀ (w : M), ∃ c, c • v = w
this : Nontrivial R
hn : v ≠ 0
⊢ finrank R M ≤ 1

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : StrongRankCondition R
v : M
h : ∀ (w : M), ∃ c, c • v = w
⊢ finrank R M ≤ 1

Tactic:
haveI := nontrivial_of_invariantBasisNumber R

Result:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : StrongRankCondition R
v : M
h : ∀ (w : M), ∃ c, c • v = w
this : Nontrivial R
⊢ finrank R M ≤ 1

Proof state:
case intro
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : StrongRankCondition R
this : Nontrivial R
h : ∀ (w : M), ∃ c, c • 0 = w
c : R
⊢ c • 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
case inl
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : StrongRankCondition R
this✝ : Nontrivial R
h : ∀ (w : M), ∃ c, c • 0 = w
this : Subsingleton M
⊢ 0 ≤ 1

Tactic:
exact zero_le_one

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : StrongRankCondition R
this : Nontrivial R
h : ∀ (w : M), ∃ c, c • 0 = w
w : M
⊢ w = 0

Tactic:
obtain ⟨c, rfl⟩ := h w

Result:
case intro
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : StrongRankCondition R
this : Nontrivial R
h : ∀ (w : M), ∃ c, c • 0 = w
c : R
⊢ c • 0 = 0

Proof state:
case inl
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : StrongRankCondition R
this✝ : Nontrivial R
h : ∀ (w : M), ∃ c, c • 0 = w
this : Subsingleton M
⊢ finrank R M ≤ 1

Tactic:
rw [finrank_zero_of_subsingleton]

Result:
case inl
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : StrongRankCondition R
this✝ : Nontrivial R
h : ∀ (w : M), ∃ c, c • 0 = w
this : Subsingleton M
⊢ 0 ≤ 1

Proof state:
case inl
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : StrongRankCondition R
this : Nontrivial R
h : ∀ (w : M), ∃ c, c • 0 = w
⊢ finrank R M ≤ 1

Tactic:
haveI :=
  _root_.subsingleton_of_forall_eq (0 : M) fun w => by
    obtain ⟨c, rfl⟩ := h w
    simp

Result:
case inl
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : StrongRankCondition R
this✝ : Nontrivial R
h : ∀ (w : M), ∃ c, c • 0 = w
this : Subsingleton M
⊢ finrank R M ≤ 1

Proof state:
case inr
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : StrongRankCondition R
v : M
h : ∀ (w : M), ∃ c, c • v = w
this : Nontrivial R
hn : v ≠ 0
⊢ finrank R M ≤ 1

Tactic:
exact (finrank_eq_one v hn h).le

Result:
no goals