K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
⊢ Module.rank K V ≤ 1 ↔ ∃ v₀, ∀ (v : V), ∃ 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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
⊢ Module.rank K V ≤ 1 ↔ ∃ v₀, ∀ (v : V), ∃ r, r • v₀ = v
let b := Basis.ofVectorSpace K 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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
⊢ Module.rank K V ≤ 1 → ∃ v₀, ∀ (v : V), ∃ 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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
⊢ (∃ v₀, ∀ (v : V), ∃ r, r • v₀ = v) → Module.rank K V ≤ 1
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
⊢ Module.rank K V ≤ 1 ↔ ∃ v₀, ∀ (v : V), ∃ r, r • v₀ = v
constructor
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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
hd : Module.rank K V ≤ 1
⊢ ∃ v₀, ∀ (v : V), ∃ 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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
⊢ Module.rank K V ≤ 1 → ∃ v₀, ∀ (v : V), ∃ r, r • v₀ = v
intro hd
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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
hd : Set.Subsingleton (ofVectorSpaceIndex K V)
⊢ ∃ v₀, ∀ (v : V), ∃ 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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
hd : Module.rank K V ≤ 1
⊢ ∃ v₀, ∀ (v : V), ∃ r, r • v₀ = v
rw [← b.mk_eq_rank'', Cardinal.le_one_iff_subsingleton, subsingleton_coe] at hd
case mp.inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
hd : Set.Subsingleton (ofVectorSpaceIndex K V)
hb : ofVectorSpaceIndex K V = ∅
⊢ ∃ v₀, ∀ (v : V), ∃ r, r • v₀ = v

case mp.inr.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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
hd : Set.Subsingleton (ofVectorSpaceIndex K V)
v₀ : V
hv₀ : v₀ ∈ ofVectorSpaceIndex K V
⊢ ∃ v₀, ∀ (v : V), ∃ 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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
hd : Set.Subsingleton (ofVectorSpaceIndex K V)
⊢ ∃ v₀, ∀ (v : V), ∃ r, r • v₀ = v
rcases eq_empty_or_nonempty (ofVectorSpaceIndex K V) with (hb | ⟨⟨v₀, hv₀⟩⟩)
case mp.inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
hd : Set.Subsingleton (ofVectorSpaceIndex K V)
hb : ofVectorSpaceIndex K V = ∅
⊢ ∀ (v : V), ∃ r, r • 0 = v
case mp.inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
hd : Set.Subsingleton (ofVectorSpaceIndex K V)
hb : ofVectorSpaceIndex K V = ∅
⊢ ∃ v₀, ∀ (v : V), ∃ r, r • v₀ = v
use 0
case mp.inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
hd : Set.Subsingleton (ofVectorSpaceIndex K V)
hb : ofVectorSpaceIndex K V = ∅
h' : ∀ (v : V), v = 0
⊢ ∀ (v : V), ∃ r, r • 0 = v
case mp.inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
hd : Set.Subsingleton (ofVectorSpaceIndex K V)
hb : ofVectorSpaceIndex K V = ∅
⊢ ∀ (v : V), ∃ r, r • 0 = v
have h' : ∀ v : V, v = 0 := by simpa [hb, Submodule.eq_bot_iff] using b.span_eq.symm
case mp.inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
hd : Set.Subsingleton (ofVectorSpaceIndex K V)
hb : ofVectorSpaceIndex K V = ∅
h' : ∀ (v : V), v = 0
v : V
⊢ ∃ r, r • 0 = v
case mp.inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
hd : Set.Subsingleton (ofVectorSpaceIndex K V)
hb : ofVectorSpaceIndex K V = ∅
h' : ∀ (v : V), v = 0
⊢ ∀ (v : V), ∃ r, r • 0 = v
intro v
no goals
case mp.inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
hd : Set.Subsingleton (ofVectorSpaceIndex K V)
hb : ofVectorSpaceIndex K V = ∅
h' : ∀ (v : V), v = 0
v : V
⊢ ∃ r, r • 0 = v
simp [h' v]
no goals
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
hd : Set.Subsingleton (ofVectorSpaceIndex K V)
hb : ofVectorSpaceIndex K V = ∅
⊢ ∀ (v : V), v = 0
simpa [hb, Submodule.eq_bot_iff] using b.span_eq.symm
case mp.inr.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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
hd : Set.Subsingleton (ofVectorSpaceIndex K V)
v₀ : V
hv₀ : v₀ ∈ ofVectorSpaceIndex K V
⊢ ∀ (v : V), ∃ r, r • v₀ = v
case mp.inr.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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
hd : Set.Subsingleton (ofVectorSpaceIndex K V)
v₀ : V
hv₀ : v₀ ∈ ofVectorSpaceIndex K V
⊢ ∃ v₀, ∀ (v : V), ∃ r, r • v₀ = v
use v₀
case mp.inr.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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
hd : Set.Subsingleton (ofVectorSpaceIndex K V)
v₀ : V
hv₀ : v₀ ∈ ofVectorSpaceIndex K V
h' : span K {v₀} = ⊤
⊢ ∀ (v : V), ∃ r, r • v₀ = v
case mp.inr.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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
hd : Set.Subsingleton (ofVectorSpaceIndex K V)
v₀ : V
hv₀ : v₀ ∈ ofVectorSpaceIndex K V
⊢ ∀ (v : V), ∃ r, r • v₀ = v
have h' : (K ∙ v₀) = ⊤ := by simpa [hd.eq_singleton_of_mem hv₀] using b.span_eq
case mp.inr.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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
hd : Set.Subsingleton (ofVectorSpaceIndex K V)
v₀ : V
hv₀ : v₀ ∈ ofVectorSpaceIndex K V
h' : span K {v₀} = ⊤
v : V
⊢ ∃ r, r • v₀ = v
case mp.inr.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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
hd : Set.Subsingleton (ofVectorSpaceIndex K V)
v₀ : V
hv₀ : v₀ ∈ ofVectorSpaceIndex K V
h' : span K {v₀} = ⊤
⊢ ∀ (v : V), ∃ r, r • v₀ = v
intro v
case mp.inr.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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
hd : Set.Subsingleton (ofVectorSpaceIndex K V)
v₀ : V
hv₀ : v₀ ∈ ofVectorSpaceIndex K V
h' : span K {v₀} = ⊤
v : V
hv : v ∈ ⊤
⊢ ∃ r, r • v₀ = v
case mp.inr.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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
hd : Set.Subsingleton (ofVectorSpaceIndex K V)
v₀ : V
hv₀ : v₀ ∈ ofVectorSpaceIndex K V
h' : span K {v₀} = ⊤
v : V
⊢ ∃ r, r • v₀ = v
have hv : v ∈ (⊤ : Submodule K V) := mem_top
no goals
case mp.inr.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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
hd : Set.Subsingleton (ofVectorSpaceIndex K V)
v₀ : V
hv₀ : v₀ ∈ ofVectorSpaceIndex K V
h' : span K {v₀} = ⊤
v : V
hv : v ∈ ⊤
⊢ ∃ r, r • v₀ = v
rwa [← h', mem_span_singleton] at hv
no goals
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
hd : Set.Subsingleton (ofVectorSpaceIndex K V)
v₀ : V
hv₀ : v₀ ∈ ofVectorSpaceIndex K V
⊢ span K {v₀} = ⊤
simpa [hd.eq_singleton_of_mem hv₀] using b.span_eq
case mpr.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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
v₀ : V
hv₀ : ∀ (v : V), ∃ r, r • v₀ = v
⊢ Module.rank K V ≤ 1
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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
⊢ (∃ v₀, ∀ (v : V), ∃ r, r • v₀ = v) → Module.rank K V ≤ 1
rintro ⟨v₀, hv₀⟩
case mpr.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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
v₀ : V
hv₀ : ∀ (v : V), ∃ r, r • v₀ = v
h : span K {v₀} = ⊤
⊢ Module.rank K V ≤ 1
case mpr.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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
v₀ : V
hv₀ : ∀ (v : V), ∃ r, r • v₀ = v
⊢ Module.rank K V ≤ 1
have h : (K ∙ v₀) = ⊤ := by
  ext
  simp [mem_span_singleton, hv₀]
case mpr.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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
v₀ : V
hv₀ : ∀ (v : V), ∃ r, r • v₀ = v
h : span K {v₀} = ⊤
⊢ Module.rank K { x // x ∈ span K {v₀} } ≤ 1
case mpr.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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
v₀ : V
hv₀ : ∀ (v : V), ∃ r, r • v₀ = v
h : span K {v₀} = ⊤
⊢ Module.rank K V ≤ 1
rw [← rank_top, ← h]
case mpr.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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
v₀ : V
hv₀ : ∀ (v : V), ∃ r, r • v₀ = v
h : span K {v₀} = ⊤
⊢ (#↑{v₀}) = 1
case mpr.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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
v₀ : V
hv₀ : ∀ (v : V), ∃ r, r • v₀ = v
h : span K {v₀} = ⊤
⊢ Module.rank K { x // x ∈ span K {v₀} } ≤ 1
refine' (rank_span_le _).trans_eq _
no goals
case mpr.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.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
v₀ : V
hv₀ : ∀ (v : V), ∃ r, r • v₀ = v
h : span K {v₀} = ⊤
⊢ (#↑{v₀}) = 1
simp
case h
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
v₀ : V
hv₀ : ∀ (v : V), ∃ r, r • v₀ = v
x✝ : V
⊢ x✝ ∈ span K {v₀} ↔ x✝ ∈ ⊤
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
v₀ : V
hv₀ : ∀ (v : V), ∃ r, r • v₀ = v
⊢ span K {v₀} = ⊤
ext
no goals
case h
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1044072
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
b : Basis (↑(ofVectorSpaceIndex K V)) K V := ofVectorSpace K V
v₀ : V
hv₀ : ∀ (v : V), ∃ r, r • v₀ = v
x✝ : V
⊢ x✝ ∈ span K {v₀} ↔ x✝ ∈ ⊤
simp [mem_span_singleton, hv₀]