-- Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
/-- In a one-dimensional space, any vector is a multiple of any nonzero vector -/
lemma exists_smul_eq_of_finrank_eq_one
    (h : finrank K V = 1) {x : V} (hx : x ≠ 0) (y : V) :
    ∃ (c : K), c • x = y

Proof state:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this✝ : span K {x} = ⊤
this : y ∈ span K {x}
⊢ ∃ c, c • x = y

Tactic:
exact mem_span_singleton.1 this

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : FiniteDimensional K V
⊢ span K {x} = ⊤

Tactic:
apply eq_top_of_finrank_eq

Result:
case h
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : FiniteDimensional K V
⊢ finrank K ↥(span K {x}) = finrank K V

Proof state:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : span K {x} = ⊤
⊢ ∃ c, c • x = y

Tactic:
have : y ∈ Submodule.span K {x} := by rw [this]; exact mem_top

Result:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this✝ : span K {x} = ⊤
this : y ∈ span K {x}
⊢ ∃ c, c • x = y

Proof state:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : span K {x} = ⊤
⊢ y ∈ ⊤

Tactic:
exact mem_top

Result:
no goals

Proof state:
case h
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : FiniteDimensional K V
⊢ finrank K ↥(span K {x}) = finrank K V

Tactic:
rw [h]

Result:
case h
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : FiniteDimensional K V
⊢ finrank K ↥(span K {x}) = 1

Proof state:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
⊢ span K {x} = ⊤

Tactic:
have : FiniteDimensional K V := .of_finrank_eq_succ h

Result:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : FiniteDimensional K V
⊢ span K {x} = ⊤

Proof state:
case h
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : FiniteDimensional K V
⊢ finrank K ↥(span K {x}) = 1

Tactic:
exact finrank_span_singleton hx

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
⊢ ∃ c, c • x = y

Tactic:
have : Submodule.span K {x} = ⊤ := by
  have : FiniteDimensional K V := .of_finrank_eq_succ h
  apply eq_top_of_finrank_eq
  rw [h]
  exact finrank_span_singleton hx

Result:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : span K {x} = ⊤
⊢ ∃ c, c • x = y

Proof state:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : span K {x} = ⊤
⊢ y ∈ span K {x}

Tactic:
rw [this]

Result:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : span K {x} = ⊤
⊢ y ∈ ⊤