awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x : ι // x ≠ i1 }
g : { x : ι // x ≠ i1 } → k
hg : Eq.{u_2 + 1} (α := V) (∑ 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 (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
hfdef : f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
s2 : Finset ι := insert i1 (map (Embedding.subtype fun (x : ι) ↦ x ≠ i1) s)
hfg : ∀ (x : { x : ι // x ≠ i1 }), g x = f (↑x : ι)
dsimp :
  HAdd.hAdd (α := k) (if hx : i1 = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) i1 hx))
      (∑ x ∈ s, g x) =
    0
⊢ HAdd.hAdd (α := k)
      ((fun (x : ι) ↦ (if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx) : k)) i1)
      (∑ x ∈ s, g x) =
    0

Tactic:
dsimp only
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x : ι // x ≠ i1 }
g : { x : ι // x ≠ i1 } → k
hg : Eq.{u_2 + 1} (α := V) (∑ 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 (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
hfdef : f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
s2 : Finset ι := insert i1 (map (Embedding.subtype fun (x : ι) ↦ x ≠ i1) s)
hfg : ∀ (x : { x : ι // x ≠ i1 }), g x = f (↑x : ι)
rw : HAdd.hAdd (α := k) (-∑ y ∈ s, g y) (∑ x ∈ s, g x) = 0
⊢ HAdd.hAdd (α := k) (if hx : i1 = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) i1 hx))
      (∑ x ∈ s, g x) =
    0

Tactic:
rw [dif_pos rfl]

Premises used: dif_pos, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x : ι // x ≠ i1 }
g : { x : ι // x ≠ i1 } → k
hg : Eq.{u_2 + 1} (α := V) (∑ 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 (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
hfdef : f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
s2 : Finset ι := insert i1 (map (Embedding.subtype fun (x : ι) ↦ x ≠ i1) s)
hfg : ∀ (x : { x : ι // x ≠ i1 }), g x = f (↑x : ι)
⊢ HAdd.hAdd (α := k) (-∑ y ∈ s, g y) (∑ x ∈ s, g x) = 0

Tactic:
neg_add_cancel _

Premises used: neg_add_cancel
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x : ι // x ≠ i1 }
g : { x : ι // x ≠ i1 } → k
hg : Eq.{u_2 + 1} (α := V) (∑ 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 (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
hfdef : f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
s2 : Finset ι := insert i1 (map (Embedding.subtype fun (x : ι) ↦ x ≠ i1) s)
hfg : ∀ (x : { x : ι // x ≠ i1 }), g x = f (↑x : ι)
⊢ HAdd.hAdd (α := k) (-∑ y ∈ s, g y) (∑ x ∈ s, g x) = 0

Tactic:
exact neg_add_cancel _

Premises used: neg_add_cancel
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x : ι // x ≠ i1 }
g : { x : ι // x ≠ i1 } → k
hg : Eq.{u_2 + 1} (α := V) (∑ 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 (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
hfdef : f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
s2 : Finset ι := insert i1 (map (Embedding.subtype fun (x : ι) ↦ x ≠ i1) s)
hfg : ∀ (x : { x : ι // x ≠ i1 }), g x = f (↑x : ι)
⊢ Eq.{u_1 + 1} (α := k) (∑ ι ∈ s2, f ι) 0

Tactic:
have hf : ∑ ι ∈ s2, f ι = 0 := by
        rw [Finset.sum_insert
            (Finset.notMem_map_subtype_of_not_property s (Classical.not_not.2 rfl)),
          Finset.sum_subtype_map_embedding fun x _ => (hfg x).symm]
        rw [hfdef]
        dsimp only
        rw [dif_pos rfl]
        exact neg_add_cancel _
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x : ι // x ≠ i1 }
g : { x : ι // x ≠ i1 } → k
hg : Eq.{u_2 + 1} (α := V) (∑ 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 (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
hfdef : f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
s2 : Finset ι := insert i1 (map (Embedding.subtype fun (x : ι) ↦ x ≠ i1) s)
hfg : ∀ (x : { x : ι // x ≠ i1 }), g x = f (↑x : ι)
hf : Eq.{u_1 + 1} (α := k) (∑ ι ∈ s2, f ι) 0
⊢ let f2 : ι → V := fun (x : ι) ↦ f x • (p x -ᵥ p i1);
  f2 = fun (x : ι) ↦ f x • (p x -ᵥ p i1)

Tactic:
set f2 : ι → V := fun x => f x • (p x -ᵥ p i1) with hf2def

Premises used: VSub.vsub, HSMul.hSMul
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x : ι // x ≠ i1 }
g : { x : ι // x ≠ i1 } → k
hg : Eq.{u_2 + 1} (α := V) (∑ 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 (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
hfdef : f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
s2 : Finset ι := insert i1 (map (Embedding.subtype fun (x : ι) ↦ x ≠ i1) s)
hfg : ∀ (x : { x : ι // x ≠ i1 }), g x = f (↑x : ι)
hf : Eq.{u_1 + 1} (α := k) (∑ ι ∈ s2, f ι) 0
f2 : ι → V := fun (x : ι) ↦ f x • (p x -ᵥ p i1)
hf2def : f2 = fun (x : ι) ↦ f x • (p x -ᵥ p i1)
⊢ let g2 : { x : ι // x ≠ i1 } → V := fun (x : { x : ι // x ≠ i1 }) ↦ g x • (p (↑x : ι) -ᵥ p i1);
  s.sum g2 = 0

Tactic:
set g2 : { x // x ≠ i1 } → V := fun x => g x • (p x -ᵥ p i1)

Premises used: VSub.vsub, HSMul.hSMul, Subtype.val
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : 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 (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
hfdef : f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
s2 : Finset ι := insert i1 (map (Embedding.subtype fun (x : ι) ↦ x ≠ i1) s)
hfg : ∀ (x : { x : ι // x ≠ i1 }), g x = f (↑x : ι)
hf : Eq.{u_1 + 1} (α := k) (∑ ι ∈ 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 : { x : ι // x ≠ i1 }) ↦ g x • (p (↑x : ι) -ᵥ p i1)
hg : s.sum g2 = 0
simp : ∀ (x : { x : ι // x ≠ i1 }), f (↑x : ι) • (p (↑x : ι) -ᵥ p i1) = g x • (p (↑x : ι) -ᵥ p i1)
⊢ ∀ (x : { x : ι // x ≠ i1 }), f2 (↑x : ι) = g2 x

Tactic:
simp only [g2, hf2def]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : 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 (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
hfdef : f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
s2 : Finset ι := insert i1 (map (Embedding.subtype fun (x : ι) ↦ x ≠ i1) s)
hfg : ∀ (x : { x : ι // x ≠ i1 }), g x = f (↑x : ι)
hf : Eq.{u_1 + 1} (α := k) (∑ ι ∈ 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 : { x : ι // x ≠ i1 }) ↦ 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:
fun x => ?_
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : 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 (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
hfdef : f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
s2 : Finset ι := insert i1 (map (Embedding.subtype fun (x : ι) ↦ x ≠ i1) s)
hfg : ∀ (x : { x : ι // x ≠ i1 }), g x = f (↑x : ι)
hf : Eq.{u_1 + 1} (α := k) (∑ ι ∈ 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 : { x : ι // x ≠ i1 }) ↦ g x • (p (↑x : ι) -ᵥ p i1)
hg : s.sum g2 = 0
refine : ∀ (x : { x : ι // x ≠ i1 }), f (↑x : ι) • (p (↑x : ι) -ᵥ p i1) = g x • (p (↑x : ι) -ᵥ p i1)
⊢ ∀ (x : { x : ι // x ≠ i1 }), f (↑x : ι) • (p (↑x : ι) -ᵥ p i1) = g x • (p (↑x : ι) -ᵥ p i1)

Tactic:
refine fun x => ?_
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : 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 (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
hfdef : f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
s2 : Finset ι := insert i1 (map (Embedding.subtype fun (x : ι) ↦ x ≠ i1) s)
hfg : ∀ (x : { x : ι // x ≠ i1 }), g x = f (↑x : ι)
hf : Eq.{u_1 + 1} (α := k) (∑ ι ∈ 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 : { x : ι // x ≠ i1 }) ↦ g x • (p (↑x : ι) -ᵥ p i1)
hg : s.sum g2 = 0
x : { x : ι // x ≠ i1 }
rw rw₁ : f (↑x : ι) • (p (↑x : ι) -ᵥ p i1) = f (↑x : ι) • (p (↑x : ι) -ᵥ p i1)
⊢ f (↑x : ι) • (p (↑x : ι) -ᵥ p i1) = g x • (p (↑x : ι) -ᵥ p i1)

Tactic:
rw [hfg]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : 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 (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
hfdef : f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
s2 : Finset ι := insert i1 (map (Embedding.subtype fun (x : ι) ↦ x ≠ i1) s)
hfg : ∀ (x : { x : ι // x ≠ i1 }), g x = f (↑x : ι)
hf : Eq.{u_1 + 1} (α := k) (∑ ι ∈ 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 : { x : ι // x ≠ i1 }) ↦ g x • (p (↑x : ι) -ᵥ p i1)
hg : s.sum g2 = 0
⊢ ∀ (x : { x : ι // x ≠ i1 }), f2 (↑x : ι) = g2 x

Tactic:
have hf2g2 : ∀ x : { x // x ≠ i1 }, f2 x = g2 x := by
          simp only [g2, hf2def]
          refine fun x => ?_
          rw [hfg]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : 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 (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
hfdef : f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
s2 : Finset ι := insert i1 (map (Embedding.subtype fun (x : ι) ↦ x ≠ i1) s)
hfg : ∀ (x : { x : ι // x ≠ i1 }), g x = f (↑x : ι)
hf : Eq.{u_1 + 1} (α := k) (∑ ι ∈ 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 : { x : ι // x ≠ i1 }) ↦ g x • (p (↑x : ι) -ᵥ p i1)
hg : s.sum g2 = 0
hf2g2 : ∀ (x : { x : ι // x ≠ i1 }), f2 (↑x : ι) = g2 x
rw : Eq.{u_2 + 1} (α := V) (∑ x ∈ s, g2 x) 0
⊢ Eq.{u_2 + 1} (α := V) ((s2.weightedVSub p : (a : ι → k) → V) f : V) (0 : V)

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]

Premises used: Finset.weightedVSubOfPoint_apply, Finset.weightedVSubOfPoint_insert, Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero, Finset.sum_subtype_map_embedding
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : 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 (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
hfdef : f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
s2 : Finset ι := insert i1 (map (Embedding.subtype fun (x : ι) ↦ x ≠ i1) s)
hfg : ∀ (x : { x : ι // x ≠ i1 }), g x = f (↑x : ι)
hf : Eq.{u_1 + 1} (α := k) (∑ ι ∈ 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 : { x : ι // x ≠ i1 }) ↦ g x • (p (↑x : ι) -ᵥ p i1)
hg : s.sum g2 = 0
hf2g2 : ∀ (x : { x : ι // x ≠ i1 }), f2 (↑x : ι) = g2 x
⊢ Eq.{u_2 + 1} (α := V) (∑ x ∈ s, g2 x) 0

Tactic:
hg
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : 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 (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
hfdef : f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
s2 : Finset ι := insert i1 (map (Embedding.subtype fun (x : ι) ↦ x ≠ i1) s)
hfg : ∀ (x : { x : ι // x ≠ i1 }), g x = f (↑x : ι)
hf : Eq.{u_1 + 1} (α := k) (∑ ι ∈ 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 : { x : ι // x ≠ i1 }) ↦ g x • (p (↑x : ι) -ᵥ p i1)
hg : s.sum g2 = 0
hf2g2 : ∀ (x : { x : ι // x ≠ i1 }), f2 (↑x : ι) = g2 x
⊢ Eq.{u_2 + 1} (α := V) (∑ x ∈ s, g2 x) 0

Tactic:
exact hg
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x : ι // x ≠ i1 }
g : { x : ι // x ≠ i1 } → k
hg : Eq.{u_2 + 1} (α := V) (∑ 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 (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
hfdef : f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
s2 : Finset ι := insert i1 (map (Embedding.subtype fun (x : ι) ↦ x ≠ i1) s)
hfg : ∀ (x : { x : ι // x ≠ i1 }), g x = f (↑x : ι)
hf : Eq.{u_1 + 1} (α := k) (∑ ι ∈ s2, f ι) 0
⊢ Eq.{u_2 + 1} (α := V) ((s2.weightedVSub p : (a : ι → k) → V) f : V) (0 : V)

Tactic:
have hs2 : s2.weightedVSub p f = (0 : V) := by
        set f2 : ι → V := fun x => f x • (p x -ᵥ p i1) with hf2def
        set g2 : { x // x ≠ i1 } → V := fun x => g x • (p x -ᵥ p i1)
        have hf2g2 : ∀ x : { x // x ≠ i1 }, f2 x = g2 x := by
          simp only [g2, hf2def]
          refine fun x => ?_
          rw [hfg]
        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]
        exact hg
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x : ι // x ≠ i1 }
g : { x : ι // x ≠ i1 } → k
hg : Eq.{u_2 + 1} (α := V) (∑ 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 (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
hfdef : f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
s2 : Finset ι := insert i1 (map (Embedding.subtype fun (x : ι) ↦ x ≠ i1) s)
hfg : ∀ (x : { x : ι // x ≠ i1 }), g x = f (↑x : ι)
hf : Eq.{u_1 + 1} (α := k) (∑ ι ∈ s2, f ι) 0
hs2 : Eq.{u_2 + 1} (α := V) ((s2.weightedVSub p : (a : ι → k) → V) f : V) (0 : V)
⊢ f (↑i : ι) = 0

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

Premises used: Iff.mpr, Finset.mem_insert_of_mem, And.intro, Exists.intro, Finset.mem_map, Subtype.val, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x : ι // x ≠ i1 }
g : { x : ι // x ≠ i1 } → k
hg : Eq.{u_2 + 1} (α := V) (∑ 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 (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
hfdef : f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
s2 : Finset ι := insert i1 (map (Embedding.subtype fun (x : ι) ↦ x ≠ i1) s)
hfg : ∀ (x : { x : ι // x ≠ i1 }), g x = f (↑x : ι)
hf : Eq.{u_1 + 1} (α := k) (∑ ι ∈ s2, f ι) 0
hs2 : Eq.{u_2 + 1} (α := V) ((s2.weightedVSub p : (a : ι → k) → V) f : V) (0 : V)
⊢ f (↑i : ι) = 0

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

Premises used: Iff.mpr, Finset.mem_insert_of_mem, And.intro, Exists.intro, Finset.mem_map, Subtype.val, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ i1 }) ↦ p (↑i : ι) -ᵥ p i1
⊢ ∀ (s : Finset { x : ι // x ≠ i1 }) (g : { x : ι // x ≠ i1 } → k),
    Eq.{u_2 + 1} (α := V) (∑ i ∈ s, g i • (p (↑i : ι) -ᵥ p i1)) 0 → ∀ i ∈ s, g i = 0

Tactic:
rw [linearIndependent_iff'] at h

Premises used: linearIndependent_iff'
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h :
  ∀ (s : Finset { x : ι // x ≠ i1 }) (g : { x : ι // x ≠ i1 } → k),
    Eq.{u_2 + 1} (α := V) (∑ i ∈ s, g i • (p (↑i : ι) -ᵥ p i1)) 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i : ι
hi : i ∈ s
mpr : ∀ (hs : Eq.{u_2 + 1} (α := V) (∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1)) 0) (i : ι) (hi : i ∈ s), w i = 0
⊢ w i = 0

Tactic:
rw [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero s w p hw (p i1), ←
        s.weightedVSubOfPoint_erase w p i1, Finset.weightedVSubOfPoint_apply] at hs

Premises used: Finset.weightedVSubOfPoint_apply, Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero, Finset.weightedVSubOfPoint_erase
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h :
  ∀ (s : Finset { x : ι // x ≠ i1 }) (g : { x : ι // x ≠ i1 } → k),
    Eq.{u_2 + 1} (α := V) (∑ i ∈ s, g i • (p (↑i : ι) -ᵥ p i1)) 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) (∑ 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)
rw :
  Eq.{u_2 + 1} (α := V) (∑ i ∈ Finset.subtype (fun (i : ι) ↦ i ≠ i1) (s.erase i1), f (↑i : ι))
    (∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1))
⊢ Eq.{u_2 + 1} (α := V) (∑ i ∈ Finset.subtype (fun (i : ι) ↦ i ≠ i1) (s.erase i1), f (↑i : ι)) 0

Tactic:
rw [← hs]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h :
  ∀ (s : Finset { x : ι // x ≠ i1 }) (g : { x : ι // x ≠ i1 } → k),
    Eq.{u_2 + 1} (α := V) (∑ i ∈ s, g i • (p (↑i : ι) -ᵥ p i1)) 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) (∑ 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)
⊢ Eq.{u_2 + 1} (α := V) (∑ x ∈ Finset.subtype (fun (x : ι) ↦ x ≠ i1) (s.erase i1), f (↑x : ι)) (∑ x ∈ s.erase i1, f x)

Tactic:
Finset.sum_subtype_of_mem f fun x => Finset.ne_of_mem_erase

Premises used: Finset.sum_subtype_of_mem, Finset.ne_of_mem_erase
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h :
  ∀ (s : Finset { x : ι // x ≠ i1 }) (g : { x : ι // x ≠ i1 } → k),
    Eq.{u_2 + 1} (α := V) (∑ i ∈ s, g i • (p (↑i : ι) -ᵥ p i1)) 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) (∑ 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)
⊢ Eq.{u_2 + 1} (α := V) (∑ i ∈ Finset.subtype (fun (i : ι) ↦ i ≠ i1) (s.erase i1), f (↑i : ι))
    (∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1))

Tactic:
convert! Finset.sum_subtype_of_mem f fun x => Finset.ne_of_mem_erase

Premises used: Finset.sum_subtype_of_mem, Finset.ne_of_mem_erase