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

case inr
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
v : V
h : ∀ (w : V), ∃ c, c • v = w
this : Nontrivial K
hn : v ≠ 0
⊢ finrank K V ≤ 1
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
v : V
h : ∀ (w : V), ∃ c, c • v = w
this : Nontrivial K
⊢ finrank K V ≤ 1
rcases eq_or_ne v 0 with (rfl | hn)
case inl
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
this✝ : Nontrivial K
h : ∀ (w : V), ∃ c, c • 0 = w
this : Subsingleton V
⊢ finrank K V ≤ 1
case inl
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
this : Nontrivial K
h : ∀ (w : V), ∃ c, c • 0 = w
⊢ finrank K V ≤ 1
haveI :=
  subsingleton_of_forall_eq (0 : V) fun w => by
    obtain ⟨c, rfl⟩ := h w
    simp
case inl
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
this✝ : Nontrivial K
h : ∀ (w : V), ∃ c, c • 0 = w
this : Subsingleton V
⊢ 0 ≤ 1
case inl
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
this✝ : Nontrivial K
h : ∀ (w : V), ∃ c, c • 0 = w
this : Subsingleton V
⊢ finrank K V ≤ 1
rw [finrank_zero_of_subsingleton]
no goals
case inl
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
this✝ : Nontrivial K
h : ∀ (w : V), ∃ c, c • 0 = w
this : Subsingleton V
⊢ 0 ≤ 1
exact zero_le_one
case intro
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
this : Nontrivial K
h : ∀ (w : V), ∃ c, c • 0 = w
c : K
⊢ c • 0 = 0
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
this : Nontrivial K
h : ∀ (w : V), ∃ c, c • 0 = w
w : V
⊢ w = 0
obtain ⟨c, rfl⟩ := h w
no goals
case intro
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
this : Nontrivial K
h : ∀ (w : V), ∃ c, c • 0 = w
c : K
⊢ c • 0 = 0
simp
no goals
case inr
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
v : V
h : ∀ (w : V), ∃ c, c • v = w
this : Nontrivial K
hn : v ≠ 0
⊢ finrank K V ≤ 1
exact (finrank_eq_one v hn h).le