-- Mathlib/LinearAlgebra/Dimension/RankNullity.lean
theorem exists_linearIndependent_pair_of_one_lt_rank [StrongRankCondition R]
    [NoZeroSMulDivisors R M] (h : 1 < Module.rank R M) {x : M} (hx : x ≠ 0) :
    ∃ y, LinearIndependent R ![x, y]

Proof state:
case 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
inst✝ : NoZeroSMulDivisors R M
h : 1 < Module.rank R M
x : M
hx : x ≠ 0
y : M
hy : LinearIndependent R (Fin.snoc ![x] y)
⊢ ∃ y, LinearIndependent R ![x, y]

Tactic:
have : Fin.snoc ![x] y = ![x, y] := by simp [Fin.snoc, ← List.ofFn_inj]

Result:
case 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
inst✝ : NoZeroSMulDivisors R M
h : 1 < Module.rank R M
x : M
hx : x ≠ 0
y : M
hy : LinearIndependent R (Fin.snoc ![x] y)
this : Fin.snoc ![x] y = ![x, y]
⊢ ∃ y, LinearIndependent R ![x, y]

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
inst✝ : NoZeroSMulDivisors R M
h : 1 < Module.rank R M
x : M
hx : x ≠ 0
⊢ ∃ y, LinearIndependent R ![x, y]

Tactic:
obtain ⟨y, hy⟩ := exists_linearIndependent_snoc_of_lt_rank (linearIndependent_unique ![x] hx) h

Result:
case 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
inst✝ : NoZeroSMulDivisors R M
h : 1 < Module.rank R M
x : M
hx : x ≠ 0
y : M
hy : LinearIndependent R (Fin.snoc ![x] y)
⊢ ∃ y, LinearIndependent R ![x, y]

Proof state:
case 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
inst✝ : NoZeroSMulDivisors R M
h : 1 < Module.rank R M
x : M
hx : x ≠ 0
y : M
hy : LinearIndependent R ![x, y]
this : Fin.snoc ![x] y = ![x, y]
⊢ ∃ y, LinearIndependent R ![x, y]

Tactic:
exact ⟨y, hy⟩

Result:
no goals

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
inst✝ : NoZeroSMulDivisors R M
h : 1 < Module.rank R M
x : M
hx : x ≠ 0
y : M
hy : LinearIndependent R (Fin.snoc ![x] y)
⊢ Fin.snoc ![x] y = ![x, y]

Tactic:
simp [Fin.snoc, ← List.ofFn_inj]

Result:
no goals

Proof state:
case 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
inst✝ : NoZeroSMulDivisors R M
h : 1 < Module.rank R M
x : M
hx : x ≠ 0
y : M
hy : LinearIndependent R (Fin.snoc ![x] y)
this : Fin.snoc ![x] y = ![x, y]
⊢ ∃ y, LinearIndependent R ![x, y]

Tactic:
rw [this] at hy

Result:
case 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
inst✝ : NoZeroSMulDivisors R M
h : 1 < Module.rank R M
x : M
hx : x ≠ 0
y : M
hy : LinearIndependent R ![x, y]
this : Fin.snoc ![x] y = ![x, y]
⊢ ∃ y, LinearIndependent R ![x, y]