awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
inst_4 : Fintype ι
p : ι → P
h :
  ∀ (w : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i : ι, w i) 0 →
      Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) w : V) (0 : V) → ∀ (i : ι), w 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
⊢ w i = 0
have mpr : ∀ (hs : Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) ((↑s : Set ι).indicator w) : V) (0 : V)) (i : ι)
  (hi : i ∈ s), w i = 0
Tactic: rw [Finset.weightedVSub_indicator_subset _ _ (Finset.subset_univ s)] at hs
Cleared hypotheses: hs, i, hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
inst_4 : Fintype ι
p : ι → P
h :
  ∀ (w : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i : ι, w i) 0 →
      Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) w : V) (0 : V) → ∀ (i : ι), w i = 0
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) ((↑s : Set ι).indicator w) : V) (0 : V)
i : ι
hi : i ∈ s
⊢ w i = 0
have mpr : ∀ (hw : Eq.{u_1 + 1} (α := k) (∑ i : ι, (↑s : Set ι).indicator w i) 0)
  (hs : Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) ((↑s : Set ι).indicator w) : V) (0 : V)) (i : ι)
  (hi : i ∈ s), w i = 0
Tactic: rw [← Finset.sum_indicator_subset _ (Finset.subset_univ s)] at hw
Cleared hypotheses: hw, hs, i, hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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
inst_4 : Fintype ι
p : ι → P
h :
  ∀ (w : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i : ι, w i) 0 →
      Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) w : V) (0 : V) → ∀ (i : ι), w i = 0
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : ι, (↑s : Set ι).indicator w i) 0
hs : Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) ((↑s : Set ι).indicator w) : V) (0 : V)
i : ι
hi : i ∈ s
⊢ w i = 0
have h₁ : (↑s : Set ι).indicator w i = 0
Tactic: replace h := h ((↑s : Set ι).indicator w) hw hs i
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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 : ι
⊢ AffineIndependent k p ↔
    LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ i1 }) ↦ p (↑i : ι) -ᵥ p i1
have mp : AffineIndependent k p → LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ i1 }) ↦ p (↑i : ι) -ᵥ p i1
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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 : ι
mp :
  AffineIndependent k p →
    LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ i1 }) ↦ p (↑i : ι) -ᵥ p i1
⊢ AffineIndependent k p ↔
    LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ i1 }) ↦ p (↑i : ι) -ᵥ p i1
have mpr : (LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ i1 }) ↦ p (↑i : ι) -ᵥ p i1) →
  AffineIndependent k p
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
⊢ LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ i1 }) ↦ p (↑i : ι) -ᵥ p i1
have mp : ∀ (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']
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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
⊢ g i = 0
have hfdef : let f : ι → k := fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx);
f = fun (x : ι) ↦ if hx : x = i1 then -∑ y ∈ s, g y else g (Subtype.mk (p := fun (x : ι) ↦ x ≠ i1) x hx)
Tactic: set f : ι → k := fun x => if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩ with hfdef
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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)
⊢ g i = 0
have hfg : ∀ (x : { x : ι // x ≠ i1 }), g x = f (↑x : ι)
Tactic: have hfg : ∀ x : { x // x ≠ i1 }, g x = f x := by grind
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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 : ι)
⊢ g i = 0
have mp : f (↑i : ι) = 0
Tactic: rw [hfg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
have rw : f i1 + ∑ x ∈ s, g x = 0
Tactic: 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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) (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
have rw : HAdd.hAdd (α := k) (-∑ y ∈ s, g y) (∑ x ∈ s, g x) = 0
Tactic: rw [dif_pos rfl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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 : ι)
⊢ f (↑i : ι) = 0
have hf : 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 _
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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)
have hf2def : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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)
have rw : f (↑x : ι) • (p (↑x : ι) -ᵥ p i1) = f (↑x : ι) • (p (↑x : ι) -ᵥ p i1)
Tactic: rw [hfg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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
⊢ Eq.{u_2 + 1} (α := V) ((s2.weightedVSub p : (a : ι → k) → V) f : V) (0 : V)
have hf2g2 : ∀ (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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
⊢ f (↑i : ι) = 0
have hs2 : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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
⊢ AffineIndependent k p
have 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
Tactic: rw [linearIndependent_iff'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
⊢ w i = 0
have 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
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
Cleared hypotheses: hs, i, hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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 : ι)) 0
have 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))
Tactic: rw [← hs]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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)
⊢ w i = 0
have hs2 : Eq.{u_2 + 1} (α := V) (∑ i ∈ Finset.subtype (fun (i : ι) ↦ i ≠ i1) (s.erase i1), f (↑i : ι)) 0
Tactic: have hs2 : (∑ i ∈ (s.erase i1).subtype fun i => i ≠ i1, f i) = 0 := by
        rw [← hs]
        convert! Finset.sum_subtype_of_mem f fun x => Finset.ne_of_mem_erase
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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)
hs2 : Eq.{u_2 + 1} (α := V) (∑ i ∈ Finset.subtype (fun (i : ι) ↦ i ≠ i1) (s.erase i1), f (↑i : ι)) 0
⊢ w i = 0
have h2 : ∀ (i : { x : ι // x ≠ i1 }),
  Membership.mem (γ := Finset { x : ι // x ≠ i1 }) (Finset.subtype (fun (i : ι) ↦ i ≠ i1) (s.erase i1)) i →
    Eq.{u_1 + 1} (α := k) ((fun (x : { x : ι // x ≠ i1 }) ↦ w (↑x : ι)) i) 0
Tactic: have h2 := h ((s.erase i1).subtype fun i => i ≠ i1) (fun x => w x) hs2
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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)
hs2 : Eq.{u_2 + 1} (α := V) (∑ i ∈ Finset.subtype (fun (i : ι) ↦ i ≠ i1) (s.erase i1), f (↑i : ι)) 0
h2 :
  ∀ (i : { x : ι // x ≠ i1 }),
    Membership.mem (γ := Finset { x : ι // x ≠ i1 }) (Finset.subtype (fun (i : ι) ↦ i ≠ i1) (s.erase i1)) i →
      Eq.{u_1 + 1} (α := k) ((fun (x : { x : ι // x ≠ i1 }) ↦ w (↑x : ι)) i) 0
⊢ w i = 0
have h2₁ : ∀ (i : { x : ι // x ≠ i1 }), (↑i : ι) ∈ s.erase i1 → w (↑i : ι) = 0
Tactic: simp_rw [Finset.mem_subtype] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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)
hs2 : Eq.{u_2 + 1} (α := V) (∑ 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
have h2b : ∀ i ∈ s, i ≠ i1 → 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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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 : ι
⊢ AffineIndependent k p ↔
    LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ i1 }) ↦ p (↑i : ι) -ᵥ p i1
have mp : AffineIndependent k p → LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ i1 }) ↦ p (↑i : ι) -ᵥ p i1
Tactic: classical
    constructor
    · intro h
      rw [linearIndependent_iff']
      intro s g hg i hi
      set f : ι → k := fun x => if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩ with hfdef
      let s2 : Finset ι := insert i1 (s.map (Embedding.subtype _))
      have hfg : ∀ x : { x // x ≠ i1 }, g x = f x := by grind
      rw [hfg]
      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 _
      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
      exact h s2 f hf hs2 i (Finset.mem_insert_of_mem (Finset.mem_map.2 ⟨i, hi, rfl⟩))
    · intro h
      rw [linearIndependent_iff'] at h
      intro s w hw hs i hi
      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
      let f : ι → V := fun i => w i • (p i -ᵥ p i1)
      have hs2 : (∑ i ∈ (s.erase i1).subtype fun i => i ≠ i1, f i) = 0 := by
        rw [← hs]
        convert! Finset.sum_subtype_of_mem f fun x => Finset.ne_of_mem_erase
      have h2 := h ((s.erase i1).subtype fun i => i ≠ i1) (fun x => w x) hs2
      simp_rw [Finset.mem_subtype] at h2
      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)
      exact Finset.eq_zero_of_sum_eq_zero hw h2b i hi