case refine'_1
ι : Type ?u.1173697
ι' : Type ?u.1173700
R : Type ?u.1173703
R₂ : Type ?u.1173706
K : Type u_1
M : Type ?u.1173712
M' : Type ?u.1173715
M'' : Type ?u.1173718
V : Type u
V' : Type ?u.1173723
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
W : Submodule K V
h : IsAtom W
⊢ ∃ v x, W = span K {v}

case refine'_2
ι : Type ?u.1173697
ι' : Type ?u.1173700
R : Type ?u.1173703
R₂ : Type ?u.1173706
K : Type u_1
M : Type ?u.1173712
M' : Type ?u.1173715
M'' : Type ?u.1173718
V : Type u
V' : Type ?u.1173723
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
W : Submodule K V
h : ∃ v x, W = span K {v}
⊢ IsAtom W
ι : Type ?u.1173697
ι' : Type ?u.1173700
R : Type ?u.1173703
R₂ : Type ?u.1173706
K : Type u_1
M : Type ?u.1173712
M' : Type ?u.1173715
M'' : Type ?u.1173718
V : Type u
V' : Type ?u.1173723
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
W : Submodule K V
⊢ IsAtom W ↔ ∃ v x, W = span K {v}
refine' ⟨fun h => _, fun h => _⟩
case refine'_1.intro
ι : Type ?u.1173697
ι' : Type ?u.1173700
R : Type ?u.1173703
R₂ : Type ?u.1173706
K : Type u_1
M : Type ?u.1173712
M' : Type ?u.1173715
M'' : Type ?u.1173718
V : Type u
V' : Type ?u.1173723
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
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ (b : Submodule K V), b < W → b = ⊥
⊢ ∃ v x, W = span K {v}
case refine'_1
ι : Type ?u.1173697
ι' : Type ?u.1173700
R : Type ?u.1173703
R₂ : Type ?u.1173706
K : Type u_1
M : Type ?u.1173712
M' : Type ?u.1173715
M'' : Type ?u.1173718
V : Type u
V' : Type ?u.1173723
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
W : Submodule K V
h : IsAtom W
⊢ ∃ v x, W = span K {v}
cases' h with hbot h
case refine'_1.intro.intro.intro
ι : Type ?u.1173697
ι' : Type ?u.1173700
R : Type ?u.1173703
R₂ : Type ?u.1173706
K : Type u_1
M : Type ?u.1173712
M' : Type ?u.1173715
M'' : Type ?u.1173718
V : Type u
V' : Type ?u.1173723
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
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ (b : Submodule K V), b < W → b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
⊢ ∃ v x, W = span K {v}
case refine'_1.intro
ι : Type ?u.1173697
ι' : Type ?u.1173700
R : Type ?u.1173703
R₂ : Type ?u.1173706
K : Type u_1
M : Type ?u.1173712
M' : Type ?u.1173715
M'' : Type ?u.1173718
V : Type u
V' : Type ?u.1173723
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
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ (b : Submodule K V), b < W → b = ⊥
⊢ ∃ v x, W = span K {v}
rcases(Submodule.ne_bot_iff W).1 hbot with ⟨v, ⟨hW, hv⟩⟩
case refine'_1.intro.intro.intro
ι : Type ?u.1173697
ι' : Type ?u.1173700
R : Type ?u.1173703
R₂ : Type ?u.1173706
K : Type u_1
M : Type ?u.1173712
M' : Type ?u.1173715
M'' : Type ?u.1173718
V : Type u
V' : Type ?u.1173723
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
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ (b : Submodule K V), b < W → b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
⊢ W = span K {v}
case refine'_1.intro.intro.intro
ι : Type ?u.1173697
ι' : Type ?u.1173700
R : Type ?u.1173703
R₂ : Type ?u.1173706
K : Type u_1
M : Type ?u.1173712
M' : Type ?u.1173715
M'' : Type ?u.1173718
V : Type u
V' : Type ?u.1173723
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
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ (b : Submodule K V), b < W → b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
⊢ ∃ v x, W = span K {v}
refine' ⟨v, ⟨hv, _⟩⟩
case refine'_1.intro.intro.intro
ι : Type ?u.1173697
ι' : Type ?u.1173700
R : Type ?u.1173703
R₂ : Type ?u.1173706
K : Type u_1
M : Type ?u.1173712
M' : Type ?u.1173715
M'' : Type ?u.1173718
V : Type u
V' : Type ?u.1173723
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
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ (b : Submodule K V), b < W → b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = span K {v}
⊢ False
case refine'_1.intro.intro.intro
ι : Type ?u.1173697
ι' : Type ?u.1173700
R : Type ?u.1173703
R₂ : Type ?u.1173706
K : Type u_1
M : Type ?u.1173712
M' : Type ?u.1173715
M'' : Type ?u.1173718
V : Type u
V' : Type ?u.1173723
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
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ (b : Submodule K V), b < W → b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
⊢ W = span K {v}
by_contra heq
case refine'_1.intro.intro.intro
ι : Type ?u.1173697
ι' : Type ?u.1173700
R : Type ?u.1173703
R₂ : Type ?u.1173706
K : Type u_1
M : Type ?u.1173712
M' : Type ?u.1173715
M'' : Type ?u.1173718
V : Type u
V' : Type ?u.1173723
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
W : Submodule K V
hbot : W ≠ ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = span K {v}
h : span K {v} < W → span K {v} = ⊥
⊢ False
case refine'_1.intro.intro.intro
ι : Type ?u.1173697
ι' : Type ?u.1173700
R : Type ?u.1173703
R₂ : Type ?u.1173706
K : Type u_1
M : Type ?u.1173712
M' : Type ?u.1173715
M'' : Type ?u.1173718
V : Type u
V' : Type ?u.1173723
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
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ (b : Submodule K V), b < W → b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = span K {v}
⊢ False
specialize h (span K {v})
case refine'_1.intro.intro.intro
ι : Type ?u.1173697
ι' : Type ?u.1173700
R : Type ?u.1173703
R₂ : Type ?u.1173706
K : Type u_1
M : Type ?u.1173712
M' : Type ?u.1173715
M'' : Type ?u.1173718
V : Type u
V' : Type ?u.1173723
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
W : Submodule K V
hbot : W ≠ ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = span K {v}
h : span K {v} ≤ W ∧ span K {v} ≠ W → v = 0
⊢ False
case refine'_1.intro.intro.intro
ι : Type ?u.1173697
ι' : Type ?u.1173700
R : Type ?u.1173703
R₂ : Type ?u.1173706
K : Type u_1
M : Type ?u.1173712
M' : Type ?u.1173715
M'' : Type ?u.1173718
V : Type u
V' : Type ?u.1173723
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
W : Submodule K V
hbot : W ≠ ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = span K {v}
h : span K {v} < W → span K {v} = ⊥
⊢ False
rw [span_singleton_eq_bot, lt_iff_le_and_ne] at h
no goals
case refine'_1.intro.intro.intro
ι : Type ?u.1173697
ι' : Type ?u.1173700
R : Type ?u.1173703
R₂ : Type ?u.1173706
K : Type u_1
M : Type ?u.1173712
M' : Type ?u.1173715
M'' : Type ?u.1173718
V : Type u
V' : Type ?u.1173723
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
W : Submodule K V
hbot : W ≠ ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = span K {v}
h : span K {v} ≤ W ∧ span K {v} ≠ W → v = 0
⊢ False
exact hv (h ⟨(span_singleton_le_iff_mem v W).2 hW, Ne.symm heq⟩)
case refine'_2.intro.intro
ι : Type ?u.1173697
ι' : Type ?u.1173700
R : Type ?u.1173703
R₂ : Type ?u.1173706
K : Type u_1
M : Type ?u.1173712
M' : Type ?u.1173715
M'' : Type ?u.1173718
V : Type u
V' : Type ?u.1173723
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})
case refine'_2
ι : Type ?u.1173697
ι' : Type ?u.1173700
R : Type ?u.1173703
R₂ : Type ?u.1173706
K : Type u_1
M : Type ?u.1173712
M' : Type ?u.1173715
M'' : Type ?u.1173718
V : Type u
V' : Type ?u.1173723
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
W : Submodule K V
h : ∃ v x, W = span K {v}
⊢ IsAtom W
rcases h with ⟨v, ⟨hv, rfl⟩⟩
no goals
case refine'_2.intro.intro
ι : Type ?u.1173697
ι' : Type ?u.1173700
R : Type ?u.1173703
R₂ : Type ?u.1173706
K : Type u_1
M : Type ?u.1173712
M' : Type ?u.1173715
M'' : Type ?u.1173718
V : Type u
V' : Type ?u.1173723
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})
exact nonzero_span_atom v hv