ι : Type u'
ι' : Type ?u.115828
R : Type u_1
K : Type ?u.115834
M : Type u_2
M' : Type ?u.115840
M'' : Type ?u.115843
V : Type u
V' : Type ?u.115848
v✝ : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x✝ y : M
m : ℕ
x : M
v : Fin m → M
hli✝ : LinearIndependent R v
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : { x // x ∈ 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
ι : Type u'
ι' : Type ?u.115828
R : Type u_1
K : Type ?u.115834
M : Type u_2
M' : Type ?u.115840
M'' : Type ?u.115843
V : Type u
V' : Type ?u.115848
v✝ : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x✝ y : M
m : ℕ
x : M
v : Fin m → M
hli : LinearIndependent R v
x_ortho : ∀ (c : R) (y : { x // x ∈ span R (range v) }), c • x + ↑y = 0 → c = 0
⊢ LinearIndependent R (Fin.cons x v)
rw [Fintype.linearIndependent_iff] at hli⊢
ι : Type u'
ι' : Type ?u.115828
R : Type u_1
K : Type ?u.115834
M : Type u_2
M' : Type ?u.115840
M'' : Type ?u.115843
V : Type u
V' : Type ?u.115848
v✝ : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x✝ y : M
m : ℕ
x : M
v : Fin m → M
hli✝ : LinearIndependent R v
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : { x // x ∈ 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
ι : Type u'
ι' : Type ?u.115828
R : Type u_1
K : Type ?u.115834
M : Type u_2
M' : Type ?u.115840
M'' : Type ?u.115843
V : Type u
V' : Type ?u.115848
v✝ : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x✝ y : M
m : ℕ
x : M
v : Fin m → M
hli✝ : LinearIndependent R v
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : { x // x ∈ 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
rintro g total_eq j
ι : Type u'
ι' : Type ?u.115828
R : Type u_1
K : Type ?u.115834
M : Type u_2
M' : Type ?u.115840
M'' : Type ?u.115843
V : Type u
V' : Type ?u.115848
v✝ : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x✝ y : M
m : ℕ
x : M
v : Fin m → M
hli✝ : LinearIndependent R v
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : { x // x ∈ 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 (Fin.succ x) • v x = 0
⊢ g j = 0
ι : Type u'
ι' : Type ?u.115828
R : Type u_1
K : Type ?u.115834
M : Type u_2
M' : Type ?u.115840
M'' : Type ?u.115843
V : Type u
V' : Type ?u.115848
v✝ : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x✝ y : M
m : ℕ
x : M
v : Fin m → M
hli✝ : LinearIndependent R v
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : { x // x ∈ 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
simp_rw [Fin.sum_univ_succ, Fin.cons_zero, Fin.cons_succ] at total_eq
ι : Type u'
ι' : Type ?u.115828
R : Type u_1
K : Type ?u.115834
M : Type u_2
M' : Type ?u.115840
M'' : Type ?u.115843
V : Type u
V' : Type ?u.115848
v✝ : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x✝ y : M
m : ℕ
x : M
v : Fin m → M
hli✝ : LinearIndependent R v
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : { x // x ∈ 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 (Fin.succ x) • v x = 0
this : g 0 = 0
⊢ g j = 0
ι : Type u'
ι' : Type ?u.115828
R : Type u_1
K : Type ?u.115834
M : Type u_2
M' : Type ?u.115840
M'' : Type ?u.115843
V : Type u
V' : Type ?u.115848
v✝ : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x✝ y : M
m : ℕ
x : M
v : Fin m → M
hli✝ : LinearIndependent R v
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : { x // x ∈ 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 (Fin.succ x) • v x = 0
⊢ g j = 0
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⟩)
ι : Type u'
ι' : Type ?u.115828
R : Type u_1
K : Type ?u.115834
M : Type u_2
M' : Type ?u.115840
M'' : Type ?u.115843
V : Type u
V' : Type ?u.115848
v✝ : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x✝ y : M
m : ℕ
x : M
v : Fin m → M
hli✝ : LinearIndependent R v
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : { x // x ∈ 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 (Fin.succ x) • v x = 0
this : g 0 = 0
⊢ g j = 0
ι : Type u'
ι' : Type ?u.115828
R : Type u_1
K : Type ?u.115834
M : Type u_2
M' : Type ?u.115840
M'' : Type ?u.115843
V : Type u
V' : Type ?u.115848
v✝ : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x✝ y : M
m : ℕ
x : M
v : Fin m → M
hli✝ : LinearIndependent R v
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : { x // x ∈ 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 (Fin.succ x) • v x = 0
this : g 0 = 0
⊢ g j = 0
rw [this, zero_smul, zero_add] at total_eq
no goals
ι : Type u'
ι' : Type ?u.115828
R : Type u_1
K : Type ?u.115834
M : Type u_2
M' : Type ?u.115840
M'' : Type ?u.115843
V : Type u
V' : Type ?u.115848
v✝ : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x✝ y : M
m : ℕ
x : M
v : Fin m → M
hli✝ : LinearIndependent R v
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : { x // x ∈ 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 (Fin.succ x) • v x = 0
this : g 0 = 0
⊢ g j = 0
exact Fin.cases this (hli _ total_eq) j
ι : Type u'
ι' : Type ?u.115828
R : Type u_1
K : Type ?u.115834
M : Type u_2
M' : Type ?u.115840
M'' : Type ?u.115843
V : Type u
V' : Type ?u.115848
v✝ : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x✝ y : M
m : ℕ
x : M
v : Fin m → M
hli✝ : LinearIndependent R v
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : { x // x ∈ 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 (Fin.succ x) • v x = 0
⊢ ∑ i : Fin m, g (Fin.succ i) • v i ∈ span R (range v)
ι : Type u'
ι' : Type ?u.115828
R : Type u_1
K : Type ?u.115834
M : Type u_2
M' : Type ?u.115840
M'' : Type ?u.115843
V : Type u
V' : Type ?u.115848
v✝ : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x✝ y : M
m : ℕ
x : M
v : Fin m → M
hli✝ : LinearIndependent R v
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : { x // x ∈ 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 (Fin.succ x) • v x = 0
⊢ g 0 = 0
refine' x_ortho (g 0) ⟨∑ i : Fin m, g i.succ • v i, _⟩ total_eq
no goals
ι : Type u'
ι' : Type ?u.115828
R : Type u_1
K : Type ?u.115834
M : Type u_2
M' : Type ?u.115840
M'' : Type ?u.115843
V : Type u
V' : Type ?u.115848
v✝ : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x✝ y : M
m : ℕ
x : M
v : Fin m → M
hli✝ : LinearIndependent R v
hli : ∀ (g : Fin m → R), ∑ i : Fin m, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : { x // x ∈ 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 (Fin.succ x) • v x = 0
⊢ ∑ i : Fin m, g (Fin.succ i) • v i ∈ span R (range v)
exact sum_mem fun i _ => smul_mem _ _ (subset_span ⟨i, rfl⟩)