-- Mathlib/LinearAlgebra/Dimension/RankNullity.lean
theorem exists_linearIndepOn_of_lt_rank [StrongRankCondition R]
    {s : Set M} (hs : LinearIndepOn R id s) :
    ∃ t, s ⊆ t ∧ #t = Module.rank R M ∧ LinearIndepOn R id t

Proof state:
case intro.intro
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
⊢ ∃ t, s ⊆ t ∧ #↑t = Module.rank R M ∧ LinearIndepOn R _root_.id t

Tactic:
choose sec hsec using Submodule.Quotient.mk_surjective (Submodule.span R s)

Result:
case intro.intro
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), Submodule.Quotient.mk (sec b) = b
⊢ ∃ t, s ⊆ t ∧ #↑t = Module.rank R M ∧ LinearIndepOn R _root_.id t

Proof state:
case intro.intro
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), Submodule.Quotient.mk (sec b) = b
hsec' : Submodule.Quotient.mk ∘ sec = _root_.id
⊢ ∃ t, s ⊆ t ∧ #↑t = Module.rank R M ∧ LinearIndepOn R _root_.id t

Tactic:
have hst : Disjoint s (sec '' t) := by
  rw [Set.disjoint_iff]
  rintro _ ⟨hxs, ⟨x, hxt, rfl⟩⟩
  apply ht'.ne_zero ⟨x, hxt⟩
  rw [Subtype.coe_mk, ← hsec x, Submodule.Quotient.mk_eq_zero]
  exact Submodule.subset_span hxs

Result:
case intro.intro
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), Submodule.Quotient.mk (sec b) = b
hsec' : Submodule.Quotient.mk ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ ∃ t, s ⊆ t ∧ #↑t = Module.rank R M ∧ LinearIndepOn R _root_.id t

Proof state:
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), Submodule.Quotient.mk (sec b) = b
hsec' : Submodule.Quotient.mk ∘ sec = _root_.id
⊢ s ∩ sec '' t ⊆ ∅

Tactic:
rintro _ ⟨hxs, ⟨x, hxt, rfl⟩⟩

Result:
case intro.intro.intro
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), Submodule.Quotient.mk (sec b) = b
hsec' : Submodule.Quotient.mk ∘ sec = _root_.id
x : M ⧸ span R s
hxt : x ∈ t
hxs : sec x ∈ s
⊢ sec x ∈ ∅

Proof state:
case intro.intro
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), Submodule.Quotient.mk (sec b) = b
hsec' : Submodule.Quotient.mk ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ ∃ t, s ⊆ t ∧ #↑t = Module.rank R M ∧ LinearIndepOn R _root_.id t

Tactic:
refine ⟨s ∪ sec '' t, subset_union_left, ?_, ?_⟩

Result:
case intro.intro.refine_1
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), Submodule.Quotient.mk (sec b) = b
hsec' : Submodule.Quotient.mk ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ #↑(s ∪ sec '' t) = Module.rank R M

case intro.intro.refine_2
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), Submodule.Quotient.mk (sec b) = b
hsec' : Submodule.Quotient.mk ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ LinearIndepOn R _root_.id (s ∪ sec '' t)

Proof state:
case intro.intro.refine_1
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), Submodule.Quotient.mk (sec b) = b
hsec' : Submodule.Quotient.mk ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ Injective sec

Tactic:
exact HasLeftInverse.injective ⟨Submodule.Quotient.mk, hsec⟩

Result:
no goals

Proof state:
case intro.intro.refine_2
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), Submodule.Quotient.mk (sec b) = b
hsec' : Submodule.Quotient.mk ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ LinearIndepOn R _root_.id (s ∪ sec '' t)

Tactic:
apply LinearIndepOn.union_of_quotient Submodule.subset_span hs

Result:
case intro.intro.refine_2
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), Submodule.Quotient.mk (sec b) = b
hsec' : Submodule.Quotient.mk ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ LinearIndepOn R Submodule.Quotient.mk (sec '' t)