-- Mathlib/LinearAlgebra/Basis/VectorSpace.lean
theorem atom_iff_nonzero_span (W : Submodule K V) :
    IsAtom W ↔ ∃ v ≠ 0, W = span K {v}

Proof state:
case refine_1.intro.intro.intro
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ b < W, b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
⊢ W = span K {v}

Tactic:
by_contra heq

Result:
case refine_1.intro.intro.intro
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ b < W, b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = span K {v}
⊢ False

Proof state:
case refine_1.intro.intro.intro
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K 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

Tactic:
exact hv (h ⟨(span_singleton_le_iff_mem v W).2 hW, Ne.symm heq⟩)

Result:
no goals

Proof state:
case refine_2.intro.intro
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ IsAtom (span K {v})

Tactic:
exact nonzero_span_atom v hv

Result:
no goals

Proof state:
case refine_2
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
h : ∃ v, v ≠ 0 ∧ W = span K {v}
⊢ IsAtom W

Tactic:
rcases h with ⟨v, ⟨hv, rfl⟩⟩

Result:
case refine_2.intro.intro
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ IsAtom (span K {v})

Proof state:
case refine_1
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
h : IsAtom W
⊢ ∃ v, v ≠ 0 ∧ W = span K {v}

Tactic:
obtain ⟨hbot, h⟩ := h

Result:
case refine_1.intro
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ b < W, b = ⊥
⊢ ∃ v, v ≠ 0 ∧ W = span K {v}

Proof state:
case refine_1.intro.intro.intro
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K 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

Tactic:
rw [span_singleton_eq_bot, lt_iff_le_and_ne] at h

Result:
case refine_1.intro.intro.intro
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K 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

Proof state:
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
⊢ IsAtom W ↔ ∃ v, v ≠ 0 ∧ W = span K {v}

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Result:
case refine_1
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
h : IsAtom W
⊢ ∃ v, v ≠ 0 ∧ W = span K {v}

case refine_2
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
h : ∃ v, v ≠ 0 ∧ W = span K {v}
⊢ IsAtom W

Proof state:
case refine_1.intro.intro.intro
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ b < W, b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = span K {v}
⊢ False

Tactic:
specialize h (span K {v})

Result:
case refine_1.intro.intro.intro
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K 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

Proof state:
case refine_1.intro.intro.intro
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ b < W, b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
⊢ ∃ v, v ≠ 0 ∧ W = span K {v}

Tactic:
refine ⟨v, ⟨hv, ?_⟩⟩

Result:
case refine_1.intro.intro.intro
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ b < W, b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
⊢ W = span K {v}

Proof state:
case refine_1.intro
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ b < W, b = ⊥
⊢ ∃ v, v ≠ 0 ∧ W = span K {v}

Tactic:
rcases (Submodule.ne_bot_iff W).1 hbot with ⟨v, ⟨hW, hv⟩⟩

Result:
case refine_1.intro.intro.intro
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ b < W, b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
⊢ ∃ v, v ≠ 0 ∧ W = span K {v}