K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
⊢ (∃ v₀, ∀ (v : { x // x ∈ s }), ∃ r, r • v₀ = v) ↔ ∃ v₀, v₀ ∈ s ∧ ∀ (v : V), v ∈ s → ∃ r, r • v₀ = v
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
⊢ Module.rank K { x // x ∈ s } ≤ 1 ↔ ∃ v₀, v₀ ∈ s ∧ s ≤ span K {v₀}
simp_rw [rank_le_one_iff, le_span_singleton_iff]
case mp
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
⊢ (∃ v₀, ∀ (v : { x // x ∈ s }), ∃ r, r • v₀ = v) → ∃ v₀, v₀ ∈ s ∧ ∀ (v : V), v ∈ s → ∃ r, r • v₀ = v

case mpr
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
⊢ (∃ v₀, v₀ ∈ s ∧ ∀ (v : V), v ∈ s → ∃ r, r • v₀ = v) → ∃ v₀, ∀ (v : { x // x ∈ s }), ∃ r, r • v₀ = v
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
⊢ (∃ v₀, ∀ (v : { x // x ∈ s }), ∃ r, r • v₀ = v) ↔ ∃ v₀, v₀ ∈ s ∧ ∀ (v : V), v ∈ s → ∃ r, r • v₀ = v
constructor
case mp.intro.mk
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : { x // x ∈ s }), ∃ r, r • { val := v₀, property := hv₀ } = v
⊢ ∃ v₀, v₀ ∈ s ∧ ∀ (v : V), v ∈ s → ∃ r, r • v₀ = v
case mp
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
⊢ (∃ v₀, ∀ (v : { x // x ∈ s }), ∃ r, r • v₀ = v) → ∃ v₀, v₀ ∈ s ∧ ∀ (v : V), v ∈ s → ∃ r, r • v₀ = v
rintro ⟨⟨v₀, hv₀⟩, h⟩
case mp.intro.mk
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : { x // x ∈ s }), ∃ r, r • { val := v₀, property := hv₀ } = v
⊢ ∀ (v : V), v ∈ s → ∃ r, r • v₀ = v
case mp.intro.mk
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : { x // x ∈ s }), ∃ r, r • { val := v₀, property := hv₀ } = v
⊢ ∃ v₀, v₀ ∈ s ∧ ∀ (v : V), v ∈ s → ∃ r, r • v₀ = v
use v₀, hv₀
case mp.intro.mk
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : { x // x ∈ s }), ∃ r, r • { val := v₀, property := hv₀ } = v
v : V
hv : v ∈ s
⊢ ∃ r, r • v₀ = v
case mp.intro.mk
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : { x // x ∈ s }), ∃ r, r • { val := v₀, property := hv₀ } = v
⊢ ∀ (v : V), v ∈ s → ∃ r, r • v₀ = v
intro v hv
case mp.intro.mk.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : { x // x ∈ s }), ∃ r, r • { val := v₀, property := hv₀ } = v
v : V
hv : v ∈ s
r : K
hr : r • { val := v₀, property := hv₀ } = { val := v, property := hv }
⊢ ∃ r, r • v₀ = v
case mp.intro.mk
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : { x // x ∈ s }), ∃ r, r • { val := v₀, property := hv₀ } = v
v : V
hv : v ∈ s
⊢ ∃ r, r • v₀ = v
obtain ⟨r, hr⟩ := h ⟨v, hv⟩
case mp.intro.mk.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : { x // x ∈ s }), ∃ r, r • { val := v₀, property := hv₀ } = v
v : V
hv : v ∈ s
r : K
hr : r • { val := v₀, property := hv₀ } = { val := v, property := hv }
⊢ r • v₀ = v
case mp.intro.mk.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : { x // x ∈ s }), ∃ r, r • { val := v₀, property := hv₀ } = v
v : V
hv : v ∈ s
r : K
hr : r • { val := v₀, property := hv₀ } = { val := v, property := hv }
⊢ ∃ r, r • v₀ = v
use r
case mp.intro.mk.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : { x // x ∈ s }), ∃ r, r • { val := v₀, property := hv₀ } = v
v : V
hv : v ∈ s
r : K
hr : r • v₀ = v
⊢ r • v₀ = v
case mp.intro.mk.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : { x // x ∈ s }), ∃ r, r • { val := v₀, property := hv₀ } = v
v : V
hv : v ∈ s
r : K
hr : r • { val := v₀, property := hv₀ } = { val := v, property := hv }
⊢ r • v₀ = v
simp_rw [Subtype.ext_iff, coe_smul] at hr
no goals
case mp.intro.mk.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : { x // x ∈ s }), ∃ r, r • { val := v₀, property := hv₀ } = v
v : V
hv : v ∈ s
r : K
hr : r • v₀ = v
⊢ r • v₀ = v
exact hr
case mpr.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : V), v ∈ s → ∃ r, r • v₀ = v
⊢ ∃ v₀, ∀ (v : { x // x ∈ s }), ∃ r, r • v₀ = v
case mpr
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
⊢ (∃ v₀, v₀ ∈ s ∧ ∀ (v : V), v ∈ s → ∃ r, r • v₀ = v) → ∃ v₀, ∀ (v : { x // x ∈ s }), ∃ r, r • v₀ = v
rintro ⟨v₀, hv₀, h⟩
case mpr.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : V), v ∈ s → ∃ r, r • v₀ = v
⊢ ∀ (v : { x // x ∈ s }), ∃ r, r • { val := v₀, property := hv₀ } = v
case mpr.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : V), v ∈ s → ∃ r, r • v₀ = v
⊢ ∃ v₀, ∀ (v : { x // x ∈ s }), ∃ r, r • v₀ = v
use ⟨v₀, hv₀⟩
case mpr.intro.intro.mk
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : V), v ∈ s → ∃ r, r • v₀ = v
v : V
hv : v ∈ s
⊢ ∃ r, r • { val := v₀, property := hv₀ } = { val := v, property := hv }
case mpr.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : V), v ∈ s → ∃ r, r • v₀ = v
⊢ ∀ (v : { x // x ∈ s }), ∃ r, r • { val := v₀, property := hv₀ } = v
rintro ⟨v, hv⟩
case mpr.intro.intro.mk.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : V), v ∈ s → ∃ r, r • v₀ = v
v : V
hv : v ∈ s
r : K
hr : r • v₀ = v
⊢ ∃ r, r • { val := v₀, property := hv₀ } = { val := v, property := hv }
case mpr.intro.intro.mk
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : V), v ∈ s → ∃ r, r • v₀ = v
v : V
hv : v ∈ s
⊢ ∃ r, r • { val := v₀, property := hv₀ } = { val := v, property := hv }
obtain ⟨r, hr⟩ := h v hv
case mpr.intro.intro.mk.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : V), v ∈ s → ∃ r, r • v₀ = v
v : V
hv : v ∈ s
r : K
hr : r • v₀ = v
⊢ r • { val := v₀, property := hv₀ } = { val := v, property := hv }
case mpr.intro.intro.mk.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : V), v ∈ s → ∃ r, r • v₀ = v
v : V
hv : v ∈ s
r : K
hr : r • v₀ = v
⊢ ∃ r, r • { val := v₀, property := hv₀ } = { val := v, property := hv }
use r
case mpr.intro.intro.mk.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : V), v ∈ s → ∃ r, r • v₀ = v
v : V
hv : v ∈ s
r : K
hr : r • v₀ = v
⊢ r • v₀ = v
case mpr.intro.intro.mk.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : V), v ∈ s → ∃ r, r • v₀ = v
v : V
hv : v ∈ s
r : K
hr : r • v₀ = v
⊢ r • { val := v₀, property := hv₀ } = { val := v, property := hv }
simp_rw [Subtype.ext_iff, coe_smul]
no goals
case mpr.intro.intro.mk.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1061352
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
s : Submodule K V
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : V), v ∈ s → ∃ r, r • v₀ = v
v : V
hv : v ∈ s
r : K
hr : r • v₀ = v
⊢ r • v₀ = v
exact hr