case mp
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
⊢ finrank K V ≤ 1 → ∃ v, ∀ (w : V), ∃ c, c • v = w

case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
⊢ (∃ v, ∀ (w : V), ∃ c, c • v = w) → finrank K V ≤ 1
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
⊢ finrank K V ≤ 1 ↔ ∃ v, ∀ (w : V), ∃ c, c • v = w
constructor
case mp
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
h : finrank K V ≤ 1
⊢ ∃ v, ∀ (w : V), ∃ c, c • v = w
case mp
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
⊢ finrank K V ≤ 1 → ∃ v, ∀ (w : V), ∃ c, c • v = w
intro h
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
h : finrank K V ≤ 1
h' : finrank K V = 0
⊢ ∃ v, ∀ (w : V), ∃ c, c • v = w

case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
h : finrank K V ≤ 1
h' : ¬finrank K V = 0
⊢ ∃ v, ∀ (w : V), ∃ c, c • v = w
case mp
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
h : finrank K V ≤ 1
⊢ ∃ v, ∀ (w : V), ∃ c, c • v = w
by_cases h' : finrank K V = 0
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
h : finrank K V ≤ 1
h' : finrank K V = 0
⊢ ∀ (w : V), ∃ c, c • 0 = w
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
h : finrank K V ≤ 1
h' : finrank K V = 0
⊢ ∃ v, ∀ (w : V), ∃ c, c • v = w
use 0
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
h : finrank K V ≤ 1
h' : finrank K V = 0
w : V
⊢ ∃ c, c • 0 = w
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
h : finrank K V ≤ 1
h' : finrank K V = 0
⊢ ∀ (w : V), ∃ c, c • 0 = w
intro w
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
h : finrank K V ≤ 1
h' : finrank K V = 0
w : V
⊢ 0 • 0 = w
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
h : finrank K V ≤ 1
h' : finrank K V = 0
w : V
⊢ ∃ c, c • 0 = w
use 0
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
h : finrank K V ≤ 1
h' : finrank K V = 0
w : V
this : Subsingleton V
⊢ 0 • 0 = w
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
h : finrank K V ≤ 1
h' : finrank K V = 0
w : V
⊢ 0 • 0 = w
haveI := finrank_zero_iff.mp h'
no goals
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
h : finrank K V ≤ 1
h' : finrank K V = 0
w : V
this : Subsingleton V
⊢ 0 • 0 = w
apply Subsingleton.elim
case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
h : finrank K V ≤ 1
h' : 0 < finrank K V
⊢ ∃ v, ∀ (w : V), ∃ c, c • v = w
case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
h : finrank K V ≤ 1
h' : ¬finrank K V = 0
⊢ ∃ v, ∀ (w : V), ∃ c, c • v = w
replace h' := zero_lt_iff.mpr h'
case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
h : finrank K V ≤ 1
h' : 0 < finrank K V
this : finrank K V = 1
⊢ ∃ v, ∀ (w : V), ∃ c, c • v = w
case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
h : finrank K V ≤ 1
h' : 0 < finrank K V
⊢ ∃ v, ∀ (w : V), ∃ c, c • v = w
have : finrank K V = 1 := by linarith
case neg.intro.intro
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
h : finrank K V ≤ 1
h' : 0 < finrank K V
this : finrank K V = 1
v : V
p : ∀ (w : V), ∃ c, c • v = w
⊢ ∃ v, ∀ (w : V), ∃ c, c • v = w
case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
h : finrank K V ≤ 1
h' : 0 < finrank K V
this : finrank K V = 1
⊢ ∃ v, ∀ (w : V), ∃ c, c • v = w
obtain ⟨v, -, p⟩ := finrank_eq_one_iff'.mp this
no goals
case neg.intro.intro
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
h : finrank K V ≤ 1
h' : 0 < finrank K V
this : finrank K V = 1
v : V
p : ∀ (w : V), ∃ c, c • v = w
⊢ ∃ v, ∀ (w : V), ∃ c, c • v = w
exact ⟨v, p⟩
no goals
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
h : finrank K V ≤ 1
h' : 0 < finrank K V
⊢ finrank K V = 1
linarith
case mpr.intro
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
v : V
p : ∀ (w : V), ∃ c, c • v = w
⊢ finrank K V ≤ 1
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
⊢ (∃ v, ∀ (w : V), ∃ c, c • v = w) → finrank K V ≤ 1
rintro ⟨v, p⟩
no goals
case mpr.intro
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
v : V
p : ∀ (w : V), ∃ c, c • v = w
⊢ finrank K V ≤ 1
exact finrank_le_one v p