-- 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, s ≤ K ∙ v₀

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
⊢ (∃ v₀ ∈ s, ∀ v ∈ s, ∃ r, r • v₀ = v) → ∃ v₀, ∀ (v : ↥s), ∃ r, r • v₀ = v

Tactic:
rintro ⟨v₀, hv₀, h⟩

Result:
case mpr.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
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ v ∈ s, ∃ r, r • v₀ = v
⊢ ∃ v₀, ∀ (v : ↥s), ∃ r, r • v₀ = 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
⊢ (∃ v₀, ∀ (v : ↥s), ∃ r, r • v₀ = v) → ∃ v₀ ∈ s, ∀ v ∈ s, ∃ r, r • v₀ = v

Tactic:
rintro ⟨⟨v₀, hv₀⟩, h⟩

Result:
case mp.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
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v
⊢ ∃ v₀ ∈ s, ∀ v ∈ s, ∃ r, r • v₀ = 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
⊢ (∃ v₀, ∀ (v : ↥s), ∃ r, r • v₀ = v) ↔ ∃ v₀ ∈ s, ∀ v ∈ s, ∃ r, r • v₀ = 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
⊢ (∃ v₀, ∀ (v : ↥s), ∃ r, r • v₀ = v) → ∃ v₀ ∈ s, ∀ v ∈ s, ∃ r, r • v₀ = 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
⊢ (∃ v₀ ∈ s, ∀ v ∈ s, ∃ r, r • v₀ = v) → ∃ v₀, ∀ (v : ↥s), ∃ r, r • v₀ = v

Proof state:
case h.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
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ v ∈ s, ∃ r, r • v₀ = v
v : V
hv : v ∈ s
⊢ ∃ r, r • ⟨v₀, hv₀⟩ = ⟨v, hv⟩

Tactic:
obtain ⟨r, hr⟩ := h v hv

Result:
case h.mk.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
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ v ∈ s, ∃ r, r • v₀ = v
v : V
hv : v ∈ s
r : K
hr : r • v₀ = v
⊢ ∃ r, r • ⟨v₀, hv₀⟩ = ⟨v, hv⟩

Proof state:
case h
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
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v
v : V
hv : v ∈ s
r : K
hr : r • ⟨v₀, hv₀⟩ = ⟨v, hv⟩
⊢ r • v₀ = v

Tactic:
rwa [Subtype.ext_iff, coe_smul] at hr

Result:
no goals

Proof state:
case right.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
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v
v : V
hv : v ∈ s
r : K
hr : r • ⟨v₀, hv₀⟩ = ⟨v, hv⟩
⊢ ∃ r, r • v₀ = v

Tactic:
use r

Result:
case h
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
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v
v : V
hv : v ∈ s
r : K
hr : r • ⟨v₀, hv₀⟩ = ⟨v, hv⟩
⊢ r • v₀ = v

Proof state:
case h.mk.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
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ v ∈ s, ∃ r, r • v₀ = v
v : V
hv : v ∈ s
r : K
hr : r • v₀ = v
⊢ ∃ r, r • ⟨v₀, hv₀⟩ = ⟨v, hv⟩

Tactic:
use r

Result:
case h
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
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ v ∈ s, ∃ r, r • v₀ = v
v : V
hv : v ∈ s
r : K
hr : r • v₀ = v
⊢ r • ⟨v₀, hv₀⟩ = ⟨v, hv⟩

Proof state:
case h
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
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ v ∈ s, ∃ r, r • v₀ = v
v : V
hv : v ∈ s
r : K
hr : r • v₀ = v
⊢ r • ⟨v₀, hv₀⟩ = ⟨v, hv⟩

Tactic:
rwa [Subtype.ext_iff, coe_smul]

Result:
no goals

Proof state:
case right
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
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v
v : V
hv : v ∈ s
⊢ ∃ r, r • v₀ = v

Tactic:
obtain ⟨r, hr⟩ := h ⟨v, hv⟩

Result:
case right.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
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v
v : V
hv : v ∈ s
r : K
hr : r • ⟨v₀, hv₀⟩ = ⟨v, hv⟩
⊢ ∃ r, r • v₀ = v

Proof state:
case mpr.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
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ v ∈ s, ∃ r, r • v₀ = v
⊢ ∃ v₀, ∀ (v : ↥s), ∃ r, r • v₀ = v

Tactic:
use ⟨v₀, hv₀⟩

Result:
case h
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
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ v ∈ s, ∃ r, r • v₀ = v
⊢ ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v

Proof state:
case mp.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
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v
⊢ ∃ v₀ ∈ s, ∀ v ∈ s, ∃ r, r • v₀ = v

Tactic:
use v₀, hv₀

Result:
case right
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
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v
⊢ ∀ v ∈ s, ∃ r, r • v₀ = v

Proof state:
case right
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
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v
⊢ ∀ v ∈ s, ∃ r, r • v₀ = v

Tactic:
intro v hv

Result:
case right
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
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v
v : V
hv : v ∈ s
⊢ ∃ r, r • v₀ = 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, s ≤ span K {v₀}

Tactic:
simp_rw [rank_le_one_iff, le_span_singleton_iff]

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
⊢ (∃ v₀, ∀ (v : ↥s), ∃ r, r • v₀ = v) ↔ ∃ v₀ ∈ s, ∀ v ∈ s, ∃ r, r • v₀ = v

Proof state:
case h
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
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ v ∈ s, ∃ r, r • v₀ = v
⊢ ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v

Tactic:
rintro ⟨v, hv⟩

Result:
case h.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
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ v ∈ s, ∃ r, r • v₀ = v
v : V
hv : v ∈ s
⊢ ∃ r, r • ⟨v₀, hv₀⟩ = ⟨v, hv⟩