case left
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
⊢ span K {v} ≠ ⊥

case right
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
⊢ ∀ (b : Submodule K V), b < span K {v} → b = ⊥
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
⊢ IsAtom (span K {v})
constructor
case left
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
⊢ ∃ x, x ∈ span K {v} ∧ x ≠ 0
case left
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
⊢ span K {v} ≠ ⊥
rw [Submodule.ne_bot_iff]
no goals
case left
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
⊢ ∃ x, x ∈ span K {v} ∧ x ≠ 0
exact ⟨v, ⟨mem_span_singleton_self v, hv⟩⟩
case right
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
⊢ T = ⊥
case right
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
⊢ ∀ (b : Submodule K V), b < span K {v} → b = ⊥
intro T hT
case right
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
h : ¬T = ⊥
⊢ False
case right
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
⊢ T = ⊥
by_contra h
case right
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
h : ¬T = ⊥
⊢ ↑(span K {v}) ⊆ ↑T
case right
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
h : ¬T = ⊥
⊢ False
apply hT.2
case right
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
h : ¬T = ⊥
⊢ span K {v} ≤ T
case right
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
h : ¬T = ⊥
⊢ ↑(span K {v}) ⊆ ↑T
change span K {v} ≤ T
case right
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
h : ∃ x, x ∈ T ∧ x ≠ 0
⊢ v ∈ T
case right
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
h : ¬T = ⊥
⊢ span K {v} ≤ T
simp_rw [span_singleton_le_iff_mem, ← Ne.def, Submodule.ne_bot_iff] at *
case right.intro.intro
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s✝ t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
s : V
hs : s ∈ T
hz : s ≠ 0
⊢ v ∈ T
case right
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
h : ∃ x, x ∈ T ∧ x ≠ 0
⊢ v ∈ T
rcases h with ⟨s, ⟨hs, hz⟩⟩
case right.intro.intro.intro
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
a : K
hs : a • v ∈ T
hz : a • v ≠ 0
⊢ v ∈ T
case right.intro.intro
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s✝ t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
s : V
hs : s ∈ T
hz : s ≠ 0
⊢ v ∈ T
rcases mem_span_singleton.1 (hT.1 hs) with ⟨a, rfl⟩
case right.intro.intro.intro.inl
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
hs : 0 • v ∈ T
hz : 0 • v ≠ 0
⊢ v ∈ T

case right.intro.intro.intro.inr
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
a : K
hs : a • v ∈ T
hz : a • v ≠ 0
h : a ≠ 0
⊢ v ∈ T
case right.intro.intro.intro
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
a : K
hs : a • v ∈ T
hz : a • v ≠ 0
⊢ v ∈ T
rcases eq_or_ne a 0 with rfl | h
no goals
case right.intro.intro.intro.inl
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
hs : 0 • v ∈ T
hz : 0 • v ≠ 0
⊢ v ∈ T
simp only [zero_smul, ne_eq, not_true] at hz
no goals
case right.intro.intro.intro.inr
ι : Type ?u.1166402
ι' : Type ?u.1166405
R : Type ?u.1166408
R₂ : Type ?u.1166411
K : Type u_1
M : Type ?u.1166417
M' : Type ?u.1166420
M'' : Type ?u.1166423
V : Type u
V' : Type ?u.1166428
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
a : K
hs : a • v ∈ T
hz : a • v ≠ 0
h : a ≠ 0
⊢ v ∈ T
rwa [T.smul_mem_iff h] at hs