K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∑ e in t, f e = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∑ e in t, f e = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0
have card_pos : 0 < t.card := lt_trans (Nat.succ_pos _) h
case intro
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∑ e in t, f e = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∑ e in t, f e = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0
obtain ⟨x₀, m⟩ := (Finset.card_pos.1 card_pos).bex
case intro
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∑ e in t, f e = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0
case intro
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∑ e in t, f e = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0
let shift : V ↪ V := ⟨fun x => x - x₀, sub_left_injective⟩
case intro
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∑ e in t, f e = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0
case intro
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∑ e in t, f e = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0
let t' := (t.erase x₀).map shift
case intro
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∑ e in t, f e = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0
case intro
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∑ e in t, f e = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0
have h' : finrank K V < t'.card := by
  simp only [card_map, Finset.card_erase_of_mem m]
  exact Nat.lt_pred_iff.mpr h
case intro.intro.intro.intro.intro
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∑ e in t, f e = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0
case intro
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∑ e in t, f e = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0
obtain ⟨g, gsum, x₁, x₁_mem, nz⟩ := exists_nontrivial_relation_of_rank_lt_card h'
case intro.intro.intro.intro.intro
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∑ e in t, f e = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0
case intro.intro.intro.intro.intro
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∑ e in t, f e = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0
let f : V → K := fun z => if z = x₀ then -∑ z in t.erase x₀, g (z - x₀) else g (z - x₀)
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ e in t, f e • e = 0

case intro.intro.intro.intro.intro.refine'_2
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ e in t, f e = 0

case intro.intro.intro.intro.intro.refine'_3
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∃ x, x ∈ t ∧ f x ≠ 0
case intro.intro.intro.intro.intro
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∑ e in t, f e = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0
refine' ⟨f, _, _, _⟩
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
⊢ finrank K V < card t - 1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
⊢ finrank K V < card t'
simp only [card_map, Finset.card_erase_of_mem m]
no goals
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
⊢ finrank K V < card t - 1
exact Nat.lt_pred_iff.mpr h
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ e in t, f e • e = 0
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ e in t, f e • e = 0
show (∑ e : V in t, f e • e) = 0
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ x in t, (if x = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (x - x₀)) • x = 0
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ e in t, f e • e = 0
simp only
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ (∑ x in t, if x = x₀ then (-∑ z in erase t x₀, g (z - x₀)) • x else g (x - x₀) • x) = 0
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ x in t, (if x = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (x - x₀)) • x = 0
conv_lhs =>
  apply_congr
  rfl
  rw [ite_smul]
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ x in filter (fun x => x = x₀) t, (-∑ z in erase t x₀, g (z - x₀)) • x +
      ∑ x in filter (fun x => ¬x = x₀) t, g (x - x₀) • x =
    0
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ (∑ x in t, if x = x₀ then (-∑ z in erase t x₀, g (z - x₀)) • x else g (x - x₀) • x) = 0
rw [Finset.sum_ite]
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ x in {x₀}, (-∑ z in erase t x₀, g (z - x₀)) • x + ∑ x in filter (fun x => ¬x = x₀) t, g (x - x₀) • x = 0
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ x in filter (fun x => x = x₀) t, (-∑ z in erase t x₀, g (z - x₀)) • x +
      ∑ x in filter (fun x => ¬x = x₀) t, g (x - x₀) • x =
    0
conv =>
  congr
  congr
  apply_congr
  erw [filter_eq']
  simp [m]
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ x in {x₀}, (-∑ z in erase t x₀, g (z - x₀)) • x + ∑ x in erase t x₀, g (x - x₀) • x = 0
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ x in {x₀}, (-∑ z in erase t x₀, g (z - x₀)) • x + ∑ x in filter (fun x => ¬x = x₀) t, g (x - x₀) • x = 0
conv =>
  congr
  congr
  rfl
  apply_congr
  simp [filter_ne']
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ x in erase t x₀, (g (x - x₀) • x - g (x - x₀) • x₀) = 0
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ x in {x₀}, (-∑ z in erase t x₀, g (z - x₀)) • x + ∑ x in erase t x₀, g (x - x₀) • x = 0
rw [sum_singleton, neg_smul, add_comm, ← sub_eq_add_neg, sum_smul, ← sum_sub_distrib]
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ x in erase t x₀, g (x - x₀) • (x - x₀) = 0
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ x in erase t x₀, (g (x - x₀) • x - g (x - x₀) • x₀) = 0
simp only [← smul_sub]
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ x in erase t x₀, (fun e => g e • e) (↑shift x) = 0
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ x in erase t x₀, g (x - x₀) • (x - x₀) = 0
change (∑ x : V in t.erase x₀, (fun e => g e • e) (shift x)) = 0
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ x in Finset.map shift (erase t x₀), g x • x = 0
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ x in erase t x₀, (fun e => g e • e) (↑shift x) = 0
rw [← sum_map _ shift (fun e => g e • e)]
no goals
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ x in Finset.map shift (erase t x₀), g x • x = 0
exact gsum
case intro.intro.intro.intro.intro.refine'_2
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ e in t, f e = 0
case intro.intro.intro.intro.intro.refine'_2
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ e in t, f e = 0
show (∑ e : V in t, f e) = 0
case intro.intro.intro.intro.intro.refine'_2
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ f x₀ + ∑ x in erase t x₀, f x = 0
case intro.intro.intro.intro.intro.refine'_2
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ e in t, f e = 0
rw [← insert_erase m, sum_insert (not_mem_erase x₀ t)]
case intro.intro.intro.intro.intro.refine'_2
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ((if x₀ = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (x₀ - x₀)) +
      ∑ x in erase t x₀, if x = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (x - x₀)) =
    0
case intro.intro.intro.intro.intro.refine'_2
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ f x₀ + ∑ x in erase t x₀, f x = 0
dsimp
case intro.intro.intro.intro.intro.refine'_2
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ (-∑ z in erase t x₀, g (z - x₀) + ∑ x in erase t x₀, if x = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (x - x₀)) =
    0
case intro.intro.intro.intro.intro.refine'_2
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ((if x₀ = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (x₀ - x₀)) +
      ∑ x in erase t x₀, if x = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (x - x₀)) =
    0
rw [if_pos rfl]
case intro.intro.intro.intro.intro.refine'_2
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ -∑ z in erase t x₀, g (z - x₀) + ∑ x in erase t x₀, g (x - x₀) = 0
case intro.intro.intro.intro.intro.refine'_2
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ (-∑ z in erase t x₀, g (z - x₀) + ∑ x in erase t x₀, if x = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (x - x₀)) =
    0
conv_lhs =>
  congr
  rfl
  apply_congr
  rfl
  rw [if_neg (show _ ≠ x₀ from (mem_erase.mp ‹_›).1)]
no goals
case intro.intro.intro.intro.intro.refine'_2
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ -∑ z in erase t x₀, g (z - x₀) + ∑ x in erase t x₀, g (x - x₀) = 0
exact neg_add_self _
case intro.intro.intro.intro.intro.refine'_3
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∃ x, x ∈ t ∧ f x ≠ 0
case intro.intro.intro.intro.intro.refine'_3
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∃ x, x ∈ t ∧ f x ≠ 0
show ∃ (x : V), x ∈ t ∧ f x ≠ 0
case intro.intro.intro.intro.intro.refine'_3.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ x₁ + x₀ ∈ t

case intro.intro.intro.intro.intro.refine'_3.refine'_2
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ f (x₁ + x₀) ≠ 0
case intro.intro.intro.intro.intro.refine'_3
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ∃ x, x ∈ t ∧ f x ≠ 0
refine' ⟨x₁ + x₀, _, _⟩
case intro.intro.intro.intro.intro.refine'_3.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : ∃ a, a ∈ erase t x₀ ∧ ↑shift a = x₁
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ x₁ + x₀ ∈ t
case intro.intro.intro.intro.intro.refine'_3.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ x₁ + x₀ ∈ t
rw [Finset.mem_map] at x₁_mem
case intro.intro.intro.intro.intro.refine'_3.refine'_1.intro.intro
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
x₁ : V
x₁_mem : x₁ ∈ erase t x₀
nz : g (↑shift x₁) ≠ 0
⊢ ↑shift x₁ + x₀ ∈ t
case intro.intro.intro.intro.intro.refine'_3.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : ∃ a, a ∈ erase t x₀ ∧ ↑shift a = x₁
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ x₁ + x₀ ∈ t
rcases x₁_mem with ⟨x₁, x₁_mem, rfl⟩
case intro.intro.intro.intro.intro.refine'_3.refine'_1.intro.intro
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
x₁ : V
x₁_mem : x₁ ≠ x₀ ∧ x₁ ∈ t
nz : g (↑shift x₁) ≠ 0
⊢ ↑shift x₁ + x₀ ∈ t
case intro.intro.intro.intro.intro.refine'_3.refine'_1.intro.intro
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
x₁ : V
x₁_mem : x₁ ∈ erase t x₀
nz : g (↑shift x₁) ≠ 0
⊢ ↑shift x₁ + x₀ ∈ t
rw [mem_erase] at x₁_mem
no goals
case intro.intro.intro.intro.intro.refine'_3.refine'_1.intro.intro
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
x₁ : V
x₁_mem : x₁ ≠ x₀ ∧ x₁ ∈ t
nz : g (↑shift x₁) ≠ 0
⊢ ↑shift x₁ + x₀ ∈ t
simp only [x₁_mem, sub_add_cancel, Function.Embedding.coeFn_mk]
case intro.intro.intro.intro.intro.refine'_3.refine'_2
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ (if x₁ + x₀ = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (x₁ + x₀ - x₀)) ≠ 0
case intro.intro.intro.intro.intro.refine'_3.refine'_2
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ f (x₁ + x₀) ≠ 0
dsimp only
case intro.intro.intro.intro.intro.refine'_3.refine'_2.hnc
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ¬x₁ + x₀ = x₀
case intro.intro.intro.intro.intro.refine'_3.refine'_2
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ (if x₁ + x₀ = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (x₁ + x₀ - x₀)) ≠ 0
rwa [if_neg, add_sub_cancel]
case intro.intro.intro.intro.intro.refine'_3.refine'_2.hnc
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ¬x₁ = 0
case intro.intro.intro.intro.intro.refine'_3.refine'_2.hnc
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ¬x₁ + x₀ = x₀
rw [add_left_eq_self]
case intro.intro.intro.intro.intro.refine'_3.refine'_2.hnc
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
x₁_mem : 0 ∈ t'
nz : g 0 ≠ 0
⊢ False
case intro.intro.intro.intro.intro.refine'_3.refine'_2.hnc
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
x₁ : V
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
⊢ ¬x₁ = 0
rintro rfl
no goals
case intro.intro.intro.intro.intro.refine'_3.refine'_2.hnc
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V + 1 < card t
card_pos : 0 < card t
x₀ : V
m : x₀ ∈ t
shift : V ↪ V := { toFun := fun x => x - x₀, inj' := (_ : Injective fun a => a - x₀) }
t' : Finset V := Finset.map shift (erase t x₀)
h' : finrank K V < card t'
g : V → K
gsum : ∑ e in t', g e • e = 0
f : V → K := fun z => if z = x₀ then -∑ z in erase t x₀, g (z - x₀) else g (z - x₀)
x₁_mem : 0 ∈ t'
nz : g 0 ≠ 0
⊢ False
simp only [sub_eq_zero, exists_prop, Finset.mem_map, Embedding.coeFn_mk, eq_self_iff_true,
  mem_erase, not_true, exists_eq_right, Ne.def, false_and_iff] at x₁_mem