-- Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
theorem rank_submodule_le_one_iff' (s : Submodule K V) [Module.Free K s] :
    Module.rank K s ≤ 1 ↔ ∃ v₀, s ≤ K ∙ v₀

Proof state:
case mp
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
this : Nontrivial K
⊢ (∃ v₀ ∈ s, s ≤ span K {v₀}) → ∃ v₀, s ≤ span K {v₀}

Tactic:
rintro ⟨v₀, _, h⟩

Result:
case mp.intro.intro
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
this : Nontrivial K
v₀ : V
left✝ : v₀ ∈ s
h : s ≤ span K {v₀}
⊢ ∃ v₀, s ≤ span K {v₀}

Proof state:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
⊢ Module.rank K ↥s ≤ 1 ↔ ∃ v₀, s ≤ span K {v₀}

Tactic:
haveI := nontrivial_of_invariantBasisNumber K

Result:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
this : Nontrivial K
⊢ Module.rank K ↥s ≤ 1 ↔ ∃ v₀, s ≤ span K {v₀}

Proof state:
case mpr.intro
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
this : Nontrivial K
v₀ : V
h : s ≤ span K {v₀}
⊢ Module.rank K ↥s ≤ 1

Tactic:
obtain ⟨κ, b⟩ := Module.Free.exists_basis (R := K) (M := s)

Result:
case mpr.intro.intro.mk
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
this : Nontrivial K
v₀ : V
h : s ≤ span K {v₀}
κ : Type v
b : Basis κ K ↥s
⊢ Module.rank K ↥s ≤ 1

Proof state:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
this : Nontrivial K
⊢ Module.rank K ↥s ≤ 1 ↔ ∃ v₀, s ≤ span K {v₀}

Tactic:
constructor

Result:
case mp
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
this : Nontrivial K
⊢ Module.rank K ↥s ≤ 1 → ∃ v₀, s ≤ span K {v₀}

case mpr
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
this : Nontrivial K
⊢ (∃ v₀, s ≤ span K {v₀}) → Module.rank K ↥s ≤ 1

Proof state:
case mp.intro.intro
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
this : Nontrivial K
v₀ : V
left✝ : v₀ ∈ s
h : s ≤ span K {v₀}
⊢ ∃ v₀, s ≤ span K {v₀}

Tactic:
exact ⟨v₀, h⟩

Result:
no goals

Proof state:
case mpr
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
this : Nontrivial K
⊢ (∃ v₀, s ≤ span K {v₀}) → Module.rank K ↥s ≤ 1

Tactic:
rintro ⟨v₀, h⟩

Result:
case mpr.intro
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
this : Nontrivial K
v₀ : V
h : s ≤ span K {v₀}
⊢ Module.rank K ↥s ≤ 1

Proof state:
case mpr.intro.intro.mk
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
this : Nontrivial K
v₀ : V
h : s ≤ span K {v₀}
κ : Type v
b : Basis κ K ↥s
⊢ Module.rank K ↥s ≤ 1

Tactic:
simpa [b.mk_eq_rank''] using b.linearIndependent.map' _ (ker_inclusion _ _ h)
  |>.cardinal_le_rank.trans (rank_span_le {v₀})

Result:
no goals

Proof state:
case mp
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
this : Nontrivial K
⊢ Module.rank K ↥s ≤ 1 → ∃ v₀, s ≤ span K {v₀}

Tactic:
rw [rank_submodule_le_one_iff]

Result:
case mp
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
this : Nontrivial K
⊢ (∃ v₀ ∈ s, s ≤ span K {v₀}) → ∃ v₀, s ≤ span K {v₀}