-- Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
theorem Submodule.rank_le_one_iff_isPrincipal (W : Submodule K V) [Module.Free K W] :
    Module.rank K W ≤ 1 ↔ W.IsPrincipal

Proof state:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Submodule K V
inst✝ : Free K ↥W
⊢ Module.rank K ↥W ≤ 1 ↔ W.IsPrincipal

Tactic:
simp only [rank_le_one_iff, Submodule.isPrincipal_iff, le_antisymm_iff, le_span_singleton_iff,
  span_singleton_le_iff_mem]

Result:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Submodule K V
inst✝ : Free K ↥W
⊢ (∃ v₀, ∀ (v : ↥W), ∃ r, r • v₀ = v) ↔ ∃ a, (∀ v ∈ W, ∃ r, r • a = v) ∧ a ∈ W

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
W : Submodule K V
inst✝ : Free K ↥W
m : V
hm : m ∈ W
hm' : ∀ (v : ↥W), ∃ r, r • ⟨m, hm⟩ = v
⊢ ∃ a, (∀ v ∈ W, ∃ r, r • a = v) ∧ a ∈ W

Tactic:
choose f hf using hm'

Result:
case mp.intro.mk
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Submodule K V
inst✝ : Free K ↥W
m : V
hm : m ∈ W
f : ↥W → K
hf : ∀ (v : ↥W), f v • ⟨m, hm⟩ = v
⊢ ∃ a, (∀ v ∈ W, ∃ r, r • a = v) ∧ a ∈ W

Proof state:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Submodule K V
inst✝ : Free K ↥W
⊢ (∃ v₀, ∀ (v : ↥W), ∃ r, r • v₀ = v) ↔ ∃ a, (∀ v ∈ W, ∃ r, r • a = v) ∧ a ∈ W

Tactic:
constructor

Result:
case mp
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Submodule K V
inst✝ : Free K ↥W
⊢ (∃ v₀, ∀ (v : ↥W), ∃ r, r • v₀ = v) → ∃ a, (∀ v ∈ W, ∃ r, r • a = v) ∧ a ∈ W

case mpr
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Submodule K V
inst✝ : Free K ↥W
⊢ (∃ a, (∀ v ∈ W, ∃ r, r • a = v) ∧ a ∈ W) → ∃ v₀, ∀ (v : ↥W), ∃ r, r • v₀ = v

Proof state:
case mpr
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Submodule K V
inst✝ : Free K ↥W
⊢ (∃ a, (∀ v ∈ W, ∃ r, r • a = v) ∧ a ∈ W) → ∃ v₀, ∀ (v : ↥W), ∃ r, r • v₀ = v

Tactic:
rintro ⟨a, ⟨h, ha⟩⟩

Result:
case mpr.intro.intro
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Submodule K V
inst✝ : Free K ↥W
a : V
h : ∀ v ∈ W, ∃ r, r • a = v
ha : a ∈ W
⊢ ∃ v₀, ∀ (v : ↥W), ∃ 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
W : Submodule K V
inst✝ : Free K ↥W
a : V
ha : a ∈ W
f : (v : V) → v ∈ W → K
hf : ∀ (v : V) (a_1 : v ∈ W), f v a_1 • a = v
⊢ ∃ v₀, ∀ (v : ↥W), ∃ r, r • v₀ = v

Tactic:
exact ⟨⟨a, ha⟩, fun v => ⟨f v.1 v.2, Subtype.ext (hf v.1 v.2)⟩⟩

Result:
no goals

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
W : Submodule K V
inst✝ : Free K ↥W
m : V
hm : m ∈ W
f : ↥W → K
hf : ∀ (v : ↥W), f v • ⟨m, hm⟩ = v
⊢ ∃ a, (∀ v ∈ W, ∃ r, r • a = v) ∧ a ∈ W

Tactic:
exact ⟨m, ⟨fun v hv => ⟨f ⟨v, hv⟩, congr_arg ((↑) : W → V) (hf ⟨v, hv⟩)⟩, hm⟩⟩

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
W : Submodule K V
inst✝ : Free K ↥W
⊢ (∃ v₀, ∀ (v : ↥W), ∃ r, r • v₀ = v) → ∃ a, (∀ v ∈ W, ∃ r, r • a = v) ∧ a ∈ W

Tactic:
rintro ⟨⟨m, hm⟩, hm'⟩

Result:
case mp.intro.mk
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Submodule K V
inst✝ : Free K ↥W
m : V
hm : m ∈ W
hm' : ∀ (v : ↥W), ∃ r, r • ⟨m, hm⟩ = v
⊢ ∃ a, (∀ v ∈ W, ∃ r, r • a = v) ∧ a ∈ W

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
W : Submodule K V
inst✝ : Free K ↥W
a : V
h : ∀ v ∈ W, ∃ r, r • a = v
ha : a ∈ W
⊢ ∃ v₀, ∀ (v : ↥W), ∃ r, r • v₀ = v

Tactic:
choose f hf using 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
W : Submodule K V
inst✝ : Free K ↥W
a : V
ha : a ∈ W
f : (v : V) → v ∈ W → K
hf : ∀ (v : V) (a_1 : v ∈ W), f v a_1 • a = v
⊢ ∃ v₀, ∀ (v : ↥W), ∃ r, r • v₀ = v