K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1076616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
W : Submodule K V
⊢ (∃ v₀, ∀ (v : { x // x ∈ W }), ∃ r, r • v₀ = v) ↔ ∃ a, (∀ (v : V), v ∈ W → ∃ r, r • a = v) ∧ a ∈ W
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1076616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
W : Submodule K V
⊢ Module.rank K { x // x ∈ W } ≤ 1 ↔ IsPrincipal W
simp only [rank_le_one_iff, Submodule.IsPrincipal_iff, le_antisymm_iff, le_span_singleton_iff,
  span_singleton_le_iff_mem]
case mp
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1076616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
W : Submodule K V
⊢ (∃ v₀, ∀ (v : { x // x ∈ W }), ∃ r, r • v₀ = v) → ∃ a, (∀ (v : V), v ∈ W → ∃ r, r • a = v) ∧ a ∈ W

case mpr
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1076616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
W : Submodule K V
⊢ (∃ a, (∀ (v : V), v ∈ W → ∃ r, r • a = v) ∧ a ∈ W) → ∃ v₀, ∀ (v : { x // x ∈ W }), ∃ r, r • v₀ = v
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1076616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
W : Submodule K V
⊢ (∃ v₀, ∀ (v : { x // x ∈ W }), ∃ r, r • v₀ = v) ↔ ∃ a, (∀ (v : V), v ∈ W → ∃ r, r • a = v) ∧ a ∈ W
constructor
case mp.intro.mk
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1076616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
W : Submodule K V
m : V
hm : m ∈ W
hm' : ∀ (v : { x // x ∈ W }), ∃ r, r • { val := m, property := hm } = v
⊢ ∃ a, (∀ (v : V), v ∈ W → ∃ r, r • a = v) ∧ a ∈ W
case mp
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1076616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
W : Submodule K V
⊢ (∃ v₀, ∀ (v : { x // x ∈ W }), ∃ r, r • v₀ = v) → ∃ a, (∀ (v : V), v ∈ W → ∃ r, r • a = v) ∧ a ∈ W
rintro ⟨⟨m, hm⟩, hm'⟩
case mp.intro.mk
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1076616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
W : Submodule K V
m : V
hm : m ∈ W
f : { x // x ∈ W } → K
hf : ∀ (v : { x // x ∈ W }), f v • { val := m, property := hm } = v
⊢ ∃ a, (∀ (v : V), v ∈ W → ∃ r, r • a = v) ∧ a ∈ W
case mp.intro.mk
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1076616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
W : Submodule K V
m : V
hm : m ∈ W
hm' : ∀ (v : { x // x ∈ W }), ∃ r, r • { val := m, property := hm } = v
⊢ ∃ a, (∀ (v : V), v ∈ W → ∃ r, r • a = v) ∧ a ∈ W
choose f hf using hm'
no goals
case mp.intro.mk
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1076616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
W : Submodule K V
m : V
hm : m ∈ W
f : { x // x ∈ W } → K
hf : ∀ (v : { x // x ∈ W }), f v • { val := m, property := hm } = v
⊢ ∃ a, (∀ (v : V), v ∈ W → ∃ r, r • a = v) ∧ a ∈ W
exact ⟨m, ⟨fun v hv => ⟨f ⟨v, hv⟩, congr_arg ((↑) : W → V) (hf ⟨v, hv⟩)⟩, hm⟩⟩
case mpr.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1076616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
W : Submodule K V
a : V
h : ∀ (v : V), v ∈ W → ∃ r, r • a = v
ha : a ∈ W
⊢ ∃ v₀, ∀ (v : { x // x ∈ W }), ∃ r, r • v₀ = v
case mpr
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1076616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
W : Submodule K V
⊢ (∃ a, (∀ (v : V), v ∈ W → ∃ r, r • a = v) ∧ a ∈ W) → ∃ v₀, ∀ (v : { x // x ∈ W }), ∃ r, r • v₀ = v
rintro ⟨a, ⟨h, ha⟩⟩
case mpr.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1076616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
W : Submodule K V
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 : { x // x ∈ W }), ∃ r, r • v₀ = v
case mpr.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1076616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
W : Submodule K V
a : V
h : ∀ (v : V), v ∈ W → ∃ r, r • a = v
ha : a ∈ W
⊢ ∃ v₀, ∀ (v : { x // x ∈ W }), ∃ r, r • v₀ = v
choose f hf using h
no goals
case mpr.intro.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.1076616
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
W : Submodule K V
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 : { x // x ∈ W }), ∃ r, r • v₀ = v
exact ⟨⟨a, ha⟩, fun v => ⟨f v.1 v.2, Subtype.ext (hf v.1 v.2)⟩⟩