-- Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
theorem LinearIndependent.fin_cons' {m : ℕ} (x : M) (v : Fin m → M) (hli : LinearIndependent R v)
    (x_ortho : ∀ (c : R) (y : Submodule.span R (Set.range v)), c • x + y = (0 : M) → c = 0) :
    LinearIndependent R (Fin.cons x v : Fin m.succ → M)

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
x : M
v : Fin m → M
hli : LinearIndependent R v
x_ortho : ∀ (c : R) (y : ↥(span R (range v))), c • x + ↑y = 0 → c = 0
⊢ LinearIndependent R (Fin.cons x v)

Tactic:
rw [Fintype.linearIndependent_iff] at hli ⊢

Result:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : ↥(span R (range v))), c • x + ↑y = 0 → c = 0
⊢ ∀ (g : Fin (m + 1) → R), ∑ i : Fin (m + 1), g i • Fin.cons x v i = 0 → ∀ (i : Fin (m + 1)), g i = 0

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : ↥(span R (range v))), c • x + ↑y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : g 0 • x + ∑ x : Fin m, g x.succ • v x = 0
this : g 0 = 0
⊢ g j = 0

Tactic:
rw [this, zero_smul, zero_add] at total_eq

Result:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : ↥(span R (range v))), c • x + ↑y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : ∑ x : Fin m, g x.succ • v x = 0
this : g 0 = 0
⊢ g j = 0

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : ↥(span R (range v))), c • x + ↑y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : g 0 • x + ∑ x : Fin m, g x.succ • v x = 0
⊢ g j = 0

Tactic:
have : g 0 = 0 := by
  refine x_ortho (g 0) ⟨∑ i : Fin m, g i.succ • v i, ?_⟩ total_eq
  exact sum_mem fun i _ => smul_mem _ _ (subset_span ⟨i, rfl⟩)

Result:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : ↥(span R (range v))), c • x + ↑y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : g 0 • x + ∑ x : Fin m, g x.succ • v x = 0
this : g 0 = 0
⊢ g j = 0

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : ↥(span R (range v))), c • x + ↑y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : ∑ x : Fin m, g x.succ • v x = 0
this : g 0 = 0
⊢ g j = 0

Tactic:
exact Fin.cases this (hli _ total_eq) j

Result:
no goals

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : ↥(span R (range v))), c • x + ↑y = 0 → c = 0
⊢ ∀ (g : Fin (m + 1) → R), ∑ i : Fin (m + 1), g i • Fin.cons x v i = 0 → ∀ (i : Fin (m + 1)), g i = 0

Tactic:
rintro g total_eq j

Result:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : ↥(span R (range v))), c • x + ↑y = 0 → c = 0
g : Fin (m + 1) → R
total_eq : ∑ i : Fin (m + 1), g i • Fin.cons x v i = 0
j : Fin (m + 1)
⊢ g j = 0

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : ↥(span R (range v))), c • x + ↑y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : g 0 • x + ∑ x : Fin m, g x.succ • v x = 0
⊢ ∑ i : Fin m, g i.succ • v i ∈ span R (range v)

Tactic:
exact sum_mem fun i _ => smul_mem _ _ (subset_span ⟨i, rfl⟩)

Result:
no goals

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : ↥(span R (range v))), c • x + ↑y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : g 0 • x + ∑ x : Fin m, g x.succ • v x = 0
⊢ g 0 = 0

Tactic:
refine x_ortho (g 0) ⟨∑ i : Fin m, g i.succ • v i, ?_⟩ total_eq

Result:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : ↥(span R (range v))), c • x + ↑y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : g 0 • x + ∑ x : Fin m, g x.succ • v x = 0
⊢ ∑ i : Fin m, g i.succ • v i ∈ span R (range v)

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : ↥(span R (range v))), c • x + ↑y = 0 → c = 0
g : Fin (m + 1) → R
total_eq : ∑ i : Fin (m + 1), g i • Fin.cons x v i = 0
j : Fin (m + 1)
⊢ g j = 0

Tactic:
simp_rw [Fin.sum_univ_succ, Fin.cons_zero, Fin.cons_succ] at total_eq

Result:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : ↥(span R (range v))), c • x + ↑y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : g 0 • x + ∑ x : Fin m, g x.succ • v x = 0
⊢ g j = 0