-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem affineIndependent_iff_linearIndependent_vsub (p : ι → P) (i1 : ι) :
    AffineIndependent k p ↔ LinearIndependent k fun i : { x // x ≠ i1 } => (p i -ᵥ p i1 : V)

Proof state:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
⊢ LinearIndependent k fun i => p ↑i -ᵥ p i1

Tactic:
rw [linearIndependent_iff']

Result:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
⊢ ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k), ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ i ∈ s, g i = 0

Proof state:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
hfdef : f = fun x => if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
s2 : Finset ι := insert i1 (map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι ∈ s2, f ι = 0
hs2 : (s2.weightedVSub p) f = 0
⊢ f ↑i = 0

Tactic:
exact h s2 f hf hs2 i (Finset.mem_insert_of_mem (Finset.mem_map.2 ⟨i, hi, rfl⟩))

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
hfdef : f = fun x => if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
s2 : Finset ι := insert i1 (map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι ∈ s2, f ι = 0
f2 : ι → V := fun x => f x • (p x -ᵥ p i1)
hf2def : f2 = fun x => f x • (p x -ᵥ p i1)
g2 : { x // x ≠ i1 } → V := fun x => g x • (p ↑x -ᵥ p i1)
hg : s.sum g2 = 0
hf2g2 : ∀ (x : { x // x ≠ i1 }), f2 ↑x = g2 x
⊢ (s2.weightedVSub p) f = 0

Tactic:
rw [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero s2 f p hf (p i1),
  Finset.weightedVSubOfPoint_insert, Finset.weightedVSubOfPoint_apply,
  Finset.sum_subtype_map_embedding fun x _ => hf2g2 x]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
hfdef : f = fun x => if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
s2 : Finset ι := insert i1 (map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι ∈ s2, f ι = 0
f2 : ι → V := fun x => f x • (p x -ᵥ p i1)
hf2def : f2 = fun x => f x • (p x -ᵥ p i1)
g2 : { x // x ≠ i1 } → V := fun x => g x • (p ↑x -ᵥ p i1)
hg : s.sum g2 = 0
hf2g2 : ∀ (x : { x // x ≠ i1 }), f2 ↑x = g2 x
⊢ ∑ x ∈ s, g2 x = 0

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
hfdef : f = fun x => if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
s2 : Finset ι := insert i1 (map (Embedding.subtype fun x => x ≠ i1) s)
x : { x // x ≠ i1 }
⊢ g x = if hx : ↑x = i1 then -∑ y ∈ s, g y else g ⟨↑x, hx⟩

Tactic:
rw [dif_neg x.property, Subtype.coe_eta]

Result:
no goals

Proof state:
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k), ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : ∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
⊢ w i = 0

Tactic:
let f : ι → V := fun i => w i • (p i -ᵥ p i1)

Result:
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k), ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : ∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
f : ι → V := fun i => w i • (p i -ᵥ p i1)
⊢ w i = 0

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
hfdef : f = fun x => if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
s2 : Finset ι := insert i1 (map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι ∈ s2, f ι = 0
f2 : ι → V := fun x => f x • (p x -ᵥ p i1)
hf2def : f2 = fun x => f x • (p x -ᵥ p i1)
g2 : { x // x ≠ i1 } → V := fun x => g x • (p ↑x -ᵥ p i1)
hg : s.sum g2 = 0
⊢ ∀ (x : { x // x ≠ i1 }), f ↑x • (p ↑x -ᵥ p i1) = g x • (p ↑x -ᵥ p i1)

Tactic:
refine fun x => ?_

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
hfdef : f = fun x => if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
s2 : Finset ι := insert i1 (map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι ∈ s2, f ι = 0
f2 : ι → V := fun x => f x • (p x -ᵥ p i1)
hf2def : f2 = fun x => f x • (p x -ᵥ p i1)
g2 : { x // x ≠ i1 } → V := fun x => g x • (p ↑x -ᵥ p i1)
hg : s.sum g2 = 0
x : { x // x ≠ i1 }
⊢ f ↑x • (p ↑x -ᵥ p i1) = g x • (p ↑x -ᵥ p i1)

Proof state:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
hfdef : f = fun x => if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
s2 : Finset ι := insert i1 (map (Embedding.subtype fun x => x ≠ i1) s)
⊢ g i = 0

Tactic:
have hfg : ∀ x : { x // x ≠ i1 }, g x = f x := by
  intro x
  rw [hfdef]
  dsimp only
  rw [dif_neg x.property, Subtype.coe_eta]

Result:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
hfdef : f = fun x => if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
s2 : Finset ι := insert i1 (map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
⊢ g i = 0