-- 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 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)
hs2 : ∑ i ∈ Finset.subtype (fun i => i ≠ i1) (s.erase i1), f ↑i = 0
h2 : ∀ (i : { x // x ≠ i1 }), ↑i ∈ s.erase i1 → w ↑i = 0
⊢ w i = 0

Tactic:
have h2b : ∀ i ∈ s, i ≠ i1 → w i = 0 := fun i his hi =>
  h2 ⟨i, hi⟩ (Finset.mem_erase_of_ne_of_mem hi his)

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)
hs2 : ∑ i ∈ Finset.subtype (fun i => i ≠ i1) (s.erase i1), f ↑i = 0
h2 : ∀ (i : { x // x ≠ i1 }), ↑i ∈ s.erase i1 → w ↑i = 0
h2b : ∀ i ∈ s, i ≠ i1 → w i = 0
⊢ 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
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 = (fun x => if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩) ↑x

Tactic:
dsimp only

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
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⟩

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
f : ι → V := fun i => w i • (p i -ᵥ p i1)
hs2 : ∑ i ∈ Finset.subtype (fun i => i ≠ i1) (s.erase i1), f ↑i = 0
⊢ w i = 0

Tactic:
have h2 := h ((s.erase i1).subtype fun i => i ≠ i1) (fun x => w x) hs2

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)
hs2 : ∑ i ∈ Finset.subtype (fun i => i ≠ i1) (s.erase i1), f ↑i = 0
h2 : ∀ i ∈ Finset.subtype (fun i => i ≠ i1) (s.erase i1), (fun x => w ↑x) i = 0
⊢ w 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⟩
⊢ g i = 0

Tactic:
let s2 : Finset ι := insert i1 (s.map (Embedding.subtype _))

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)
⊢ 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
⊢ g i = 0

Tactic:
set f : ι → k := fun x => if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩ with hfdef

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⟩
⊢ g i = 0

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 : ι
⊢ (LinearIndependent k fun i => p ↑i -ᵥ p i1) → AffineIndependent k p

Tactic:
intro h

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 : LinearIndependent k fun i => p ↑i -ᵥ p i1
⊢ AffineIndependent k p

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
f : ι → V := fun i => w i • (p i -ᵥ p i1)
hs2 : ∑ i ∈ Finset.subtype (fun i => i ≠ i1) (s.erase i1), f ↑i = 0
h2 : ∀ i ∈ Finset.subtype (fun i => i ≠ i1) (s.erase i1), (fun x => w ↑x) i = 0
⊢ w i = 0

Tactic:
simp_rw [Finset.mem_subtype] at h2

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)
hs2 : ∑ i ∈ Finset.subtype (fun i => i ≠ i1) (s.erase i1), f ↑i = 0
h2 : ∀ (i : { x // x ≠ i1 }), ↑i ∈ s.erase i1 → w ↑i = 0
⊢ w i = 0