awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : (↑s : Type u_4) → Finset ι
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fs i, w i j) 1
p' : P
hp' :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι)) (singleton (α := P) ((Finset.affineCombination k (fs i) p : (a : ι → k) → P) (w i) : P))))
      p'
fsx : (↑s : Type u_4) → Finset ι := fun (i : (↑s : Type u_4)) ↦ insert (↑i : ι) (fs i)
hfsx : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fsx i
wx : (↑s : Type u_4) → ι → k := fun (i : (↑s : Type u_4)) ↦ (↑(fs i) : Set ι).indicator (w i)
hwx : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fsx i, wx i j) 1
hp'x :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι))
          (singleton (α := P) ((Finset.affineCombination k (fsx i) p : (a : ι → k) → P) (wx i) : P))))
      p'
w' : ι → k
fs' : Finset ι
h :
  Eq.{u_1 + 1} (α := k) (∑ j ∈ fs', w' j) 1 ∧
    (Finset.affineCombination k fs' p : (a : ι → k) → P) w' = p' ∧
      ∀ (i : (↑s : Type u_4)),
        ∃ (r : k),
          ∀ (j : ι),
            r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
i : (↑s : Type u_4)
obtain :
  ∀ (r : k)
    (hr :
      ∀ (j : ι),
        r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j),
    ∃ (r : k),
      ∀ (j : ι), r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
⊢ ∃ (r : k),
    ∀ (j : ι), r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j

Tactic:
obtain ⟨r, hr⟩ := h.2.2 i

Premises used: And.right
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : (↑s : Type u_4) → Finset ι
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fs i, w i j) 1
p' : P
hp' :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι)) (singleton (α := P) ((Finset.affineCombination k (fs i) p : (a : ι → k) → P) (w i) : P))))
      p'
fsx : (↑s : Type u_4) → Finset ι := fun (i : (↑s : Type u_4)) ↦ insert (↑i : ι) (fs i)
hfsx : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fsx i
wx : (↑s : Type u_4) → ι → k := fun (i : (↑s : Type u_4)) ↦ (↑(fs i) : Set ι).indicator (w i)
hwx : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fsx i, wx i j) 1
hp'x :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι))
          (singleton (α := P) ((Finset.affineCombination k (fsx i) p : (a : ι → k) → P) (wx i) : P))))
      p'
w' : ι → k
fs' : Finset ι
h :
  Eq.{u_1 + 1} (α := k) (∑ j ∈ fs', w' j) 1 ∧
    (Finset.affineCombination k fs' p : (a : ι → k) → P) w' = p' ∧
      ∀ (i : (↑s : Type u_4)),
        ∃ (r : k),
          ∀ (j : ι),
            r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
i : (↑s : Type u_4)
r : k
hr : ∀ (j : ι), r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
⊢ ∃ (r : k),
    ∀ (j : ι), r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j

Tactic:
⟨r, fun j ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : (↑s : Type u_4) → Finset ι
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fs i, w i j) 1
p' : P
hp' :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι)) (singleton (α := P) ((Finset.affineCombination k (fs i) p : (a : ι → k) → P) (w i) : P))))
      p'
fsx : (↑s : Type u_4) → Finset ι := fun (i : (↑s : Type u_4)) ↦ insert (↑i : ι) (fs i)
hfsx : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fsx i
wx : (↑s : Type u_4) → ι → k := fun (i : (↑s : Type u_4)) ↦ (↑(fs i) : Set ι).indicator (w i)
hwx : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fsx i, wx i j) 1
hp'x :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι))
          (singleton (α := P) ((Finset.affineCombination k (fsx i) p : (a : ι → k) → P) (wx i) : P))))
      p'
w' : ι → k
fs' : Finset ι
h :
  Eq.{u_1 + 1} (α := k) (∑ j ∈ fs', w' j) 1 ∧
    (Finset.affineCombination k fs' p : (a : ι → k) → P) w' = p' ∧
      ∀ (i : (↑s : Type u_4)),
        ∃ (r : k),
          ∀ (j : ι),
            r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
i : (↑s : Type u_4)
r : k
hr : ∀ (j : ι), r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
refine :
  ∀ (j : ι), r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
⊢ ∃ (r : k),
    ∀ (j : ι), r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j

Tactic:
refine ⟨r, fun j ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : (↑s : Type u_4) → Finset ι
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fs i, w i j) 1
p' : P
hp' :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι)) (singleton (α := P) ((Finset.affineCombination k (fs i) p : (a : ι → k) → P) (w i) : P))))
      p'
fsx : (↑s : Type u_4) → Finset ι := fun (i : (↑s : Type u_4)) ↦ insert (↑i : ι) (fs i)
hfsx : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fsx i
wx : (↑s : Type u_4) → ι → k := fun (i : (↑s : Type u_4)) ↦ (↑(fs i) : Set ι).indicator (w i)
hwx : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fsx i, wx i j) 1
hp'x :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι))
          (singleton (α := P) ((Finset.affineCombination k (fsx i) p : (a : ι → k) → P) (wx i) : P))))
      p'
w' : ι → k
fs' : Finset ι
h :
  Eq.{u_1 + 1} (α := k) (∑ j ∈ fs', w' j) 1 ∧
    (Finset.affineCombination k fs' p : (a : ι → k) → P) w' = p' ∧
      ∀ (i : (↑s : Type u_4)),
        ∃ (r : k),
          ∀ (j : ι),
            r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
i : (↑s : Type u_4)
r : k
hr : ∀ (j : ι), r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
j : ι
⊢ r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j

Tactic:
hr j
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : (↑s : Type u_4) → Finset ι
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fs i, w i j) 1
p' : P
hp' :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι)) (singleton (α := P) ((Finset.affineCombination k (fs i) p : (a : ι → k) → P) (w i) : P))))
      p'
fsx : (↑s : Type u_4) → Finset ι := fun (i : (↑s : Type u_4)) ↦ insert (↑i : ι) (fs i)
hfsx : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fsx i
wx : (↑s : Type u_4) → ι → k := fun (i : (↑s : Type u_4)) ↦ (↑(fs i) : Set ι).indicator (w i)
hwx : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fsx i, wx i j) 1
hp'x :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι))
          (singleton (α := P) ((Finset.affineCombination k (fsx i) p : (a : ι → k) → P) (wx i) : P))))
      p'
w' : ι → k
fs' : Finset ι
h :
  Eq.{u_1 + 1} (α := k) (∑ j ∈ fs', w' j) 1 ∧
    (Finset.affineCombination k fs' p : (a : ι → k) → P) w' = p' ∧
      ∀ (i : (↑s : Type u_4)),
        ∃ (r : k),
          ∀ (j : ι),
            r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
i : (↑s : Type u_4)
r : k
hr : ∀ (j : ι), r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
j : ι
h₁ : ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j
⊢ r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j

Tactic:
convert! hr j using 2
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : (↑s : Type u_4) → Finset ι
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fs i, w i j) 1
p' : P
hp' :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι)) (singleton (α := P) ((Finset.affineCombination k (fs i) p : (a : ι → k) → P) (w i) : P))))
      p'
fsx : (↑s : Type u_4) → Finset ι := fun (i : (↑s : Type u_4)) ↦ insert (↑i : ι) (fs i)
hfsx : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fsx i
wx : (↑s : Type u_4) → ι → k := fun (i : (↑s : Type u_4)) ↦ (↑(fs i) : Set ι).indicator (w i)
hwx : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fsx i, wx i j) 1
hp'x :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι))
          (singleton (α := P) ((Finset.affineCombination k (fsx i) p : (a : ι → k) → P) (wx i) : P))))
      p'
w' : ι → k
fs' : Finset ι
h :
  Eq.{u_1 + 1} (α := k) (∑ j ∈ fs', w' j) 1 ∧
    (Finset.affineCombination k fs' p : (a : ι → k) → P) w' = p' ∧
      ∀ (i : (↑s : Type u_4)),
        ∃ (r : k),
          ∀ (j : ι),
            r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
i : (↑s : Type u_4)
r : k
hr : ∀ (j : ι), r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
j : ι
h₁ :
  (if j ∈ fs i ∧ ¬j = (↑i : ι) then w i j else 0) =
    if j ∈ fs i ∧ ¬j = (↑i : ι) then if j ∈ fs i then w i j else 0 else 0
⊢ ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j

Tactic:
simp only [Set.indicator_apply, Set.mem_diff, SetLike.mem_coe, Set.mem_singleton_iff,
    Finset.coe_insert, Set.insert_diff_of_mem, fsx, wx]

Premises used: Set.indicator_apply, Set.insert_diff_of_mem, Set.mem_singleton_iff, SetLike.mem_coe, Set.mem_diff, Finset.coe_insert
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : (↑s : Type u_4) → Finset ι
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fs i, w i j) 1
p' : P
hp' :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι)) (singleton (α := P) ((Finset.affineCombination k (fs i) p : (a : ι → k) → P) (w i) : P))))
      p'
fsx : (↑s : Type u_4) → Finset ι := fun (i : (↑s : Type u_4)) ↦ insert (↑i : ι) (fs i)
hfsx : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fsx i
wx : (↑s : Type u_4) → ι → k := fun (i : (↑s : Type u_4)) ↦ (↑(fs i) : Set ι).indicator (w i)
hwx : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fsx i, wx i j) 1
hp'x :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι))
          (singleton (α := P) ((Finset.affineCombination k (fsx i) p : (a : ι → k) → P) (wx i) : P))))
      p'
w' : ι → k
fs' : Finset ι
h :
  Eq.{u_1 + 1} (α := k) (∑ j ∈ fs', w' j) 1 ∧
    (Finset.affineCombination k fs' p : (a : ι → k) → P) w' = p' ∧
      ∀ (i : (↑s : Type u_4)),
        ∃ (r : k),
          ∀ (j : ι),
            r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
i : (↑s : Type u_4)
r : k
hr : ∀ (j : ι), r * ((↑(fsx i) : Set ι) \ {(↑i : ι)}).indicator (wx i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
j : ι
⊢ (if j ∈ fs i ∧ ¬j = (↑i : ι) then w i j else 0) =
    if j ∈ fs i ∧ ¬j = (↑i : ι) then if j ∈ fs i then w i j else 0 else 0

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j : ι, w i j) 1
p' : P
hp' :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι))
          (singleton (α := P) ((Finset.affineCombination k Finset.univ p : (a : ι → k) → P) (w i) : P))))
      p'
obtain :
  ∀ (w'' : ι → k) (fs'' : Finset ι) (hw'' : Eq.{u_1 + 1} (α := k) (∑ j ∈ fs'', w'' j) 1)
    (hw''p' : (Finset.affineCombination k fs'' p : (a : ι → k) → P) w'' = p')
    (hi :
      ∀ (i : (↑s : Type u_4)),
        ∃ (r : k),
          ∀ (j : ι),
            r * ((↑Finset.univ : Set ι) \ {(↑i : ι)}).indicator (w i) j =
              ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j),
    ∃ (w' : ι → k),
      Eq.{u_1 + 1} (α := k) (∑ j : ι, w' j) 1 ∧
        (Finset.affineCombination k Finset.univ p : (a : ι → k) → P) w' = p' ∧
          ∀ (i : (↑s : Type u_4)),
            ∃ (r : k), ∀ (j : ι), r * Set.indicator {(↑i : ι)}ᶜ (w i) j = Set.indicator {(↑i : ι)}ᶜ w' j
⊢ ∃ (w' : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ j : ι, w' j) 1 ∧
      (Finset.affineCombination k Finset.univ p : (a : ι → k) → P) w' = p' ∧
        ∀ (i : (↑s : Type u_4)),
          ∃ (r : k), ∀ (j : ι), r * Set.indicator {(↑i : ι)}ᶜ (w i) j = Set.indicator {(↑i : ι)}ᶜ w' j

Tactic:
obtain ⟨w'', fs'', hw'', hw''p', hi⟩ := hp.exists_affineCombination_eq_smul_eq hs hw hp'

Premises used: AffineIndependent.exists_affineCombination_eq_smul_eq
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j : ι, w i j) 1
p' : P
hp' :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι))
          (singleton (α := P) ((Finset.affineCombination k Finset.univ p : (a : ι → k) → P) (w i) : P))))
      p'
w'' : ι → k
fs'' : Finset ι
hw'' : Eq.{u_1 + 1} (α := k) (∑ j ∈ fs'', w'' j) 1
hw''p' : (Finset.affineCombination k fs'' p : (a : ι → k) → P) w'' = p'
hi :
  ∀ (i : (↑s : Type u_4)),
    ∃ (r : k),
      ∀ (j : ι),
        r * ((↑Finset.univ : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j
⊢ ∃ (w' : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ j : ι, w' j) 1 ∧
      (Finset.affineCombination k Finset.univ p : (a : ι → k) → P) w' = p' ∧
        ∀ (i : (↑s : Type u_4)),
          ∃ (r : k), ∀ (j : ι), r * Set.indicator {(↑i : ι)}ᶜ (w i) j = Set.indicator {(↑i : ι)}ᶜ w' j

Tactic:
⟨Set.indicator fs'' w'', ?_, ?_, ?_⟩

Premises used: Set.indicator, SetLike.coe, And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j : ι, w i j) 1
p' : P
hp' :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι))
          (singleton (α := P) ((Finset.affineCombination k Finset.univ p : (a : ι → k) → P) (w i) : P))))
      p'
w'' : ι → k
fs'' : Finset ι
hw'' : Eq.{u_1 + 1} (α := k) (∑ j ∈ fs'', w'' j) 1
hw''p' : (Finset.affineCombination k fs'' p : (a : ι → k) → P) w'' = p'
hi :
  ∀ (i : (↑s : Type u_4)),
    ∃ (r : k),
      ∀ (j : ι),
        r * ((↑Finset.univ : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j
refine_1 : Eq.{u_1 + 1} (α := k) (∑ j : ι, (↑fs'' : Set ι).indicator w'' j) 1
refine_2 : (Finset.affineCombination k Finset.univ p : (a : ι → k) → P) ((↑fs'' : Set ι).indicator w'') = p'
refine_3 :
  ∀ (i : (↑s : Type u_4)),
    ∃ (r : k),
      ∀ (j : ι), r * Set.indicator {(↑i : ι)}ᶜ (w i) j = Set.indicator {(↑i : ι)}ᶜ ((↑fs'' : Set ι).indicator w'') j
⊢ ∃ (w' : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ j : ι, w' j) 1 ∧
      (Finset.affineCombination k Finset.univ p : (a : ι → k) → P) w' = p' ∧
        ∀ (i : (↑s : Type u_4)),
          ∃ (r : k), ∀ (j : ι), r * Set.indicator {(↑i : ι)}ᶜ (w i) j = Set.indicator {(↑i : ι)}ᶜ w' j

Tactic:
refine ⟨Set.indicator fs'' w'', ?_, ?_, ?_⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j : ι, w i j) 1
p' : P
hp' :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι))
          (singleton (α := P) ((Finset.affineCombination k Finset.univ p : (a : ι → k) → P) (w i) : P))))
      p'
w'' : ι → k
fs'' : Finset ι
hw'' : Eq.{u_1 + 1} (α := k) (∑ j ∈ fs'', w'' j) 1
hw''p' : (Finset.affineCombination k fs'' p : (a : ι → k) → P) w'' = p'
hi :
  ∀ (i : (↑s : Type u_4)),
    ∃ (r : k),
      ∀ (j : ι),
        r * ((↑Finset.univ : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j
refine_1 : Eq.{u_1 + 1} (α := k) (∑ j : ι, (↑fs'' : Set ι).indicator w'' j) (∑ j ∈ fs'', w'' j)
⊢ Eq.{u_1 + 1} (α := k) (∑ j : ι, (↑fs'' : Set ι).indicator w'' j) 1

Tactic:
rw [← hw'']
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j : ι, w i j) 1
p' : P
hp' :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι))
          (singleton (α := P) ((Finset.affineCombination k Finset.univ p : (a : ι → k) → P) (w i) : P))))
      p'
w'' : ι → k
fs'' : Finset ι
hw'' : Eq.{u_1 + 1} (α := k) (∑ j ∈ fs'', w'' j) 1
hw''p' : (Finset.affineCombination k fs'' p : (a : ι → k) → P) w'' = p'
hi :
  ∀ (i : (↑s : Type u_4)),
    ∃ (r : k),
      ∀ (j : ι),
        r * ((↑Finset.univ : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j
⊢ fs'' ⊆ Finset.univ

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j : ι, w i j) 1
p' : P
hp' :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι))
          (singleton (α := P) ((Finset.affineCombination k Finset.univ p : (a : ι → k) → P) (w i) : P))))
      p'
w'' : ι → k
fs'' : Finset ι
hw'' : Eq.{u_1 + 1} (α := k) (∑ j ∈ fs'', w'' j) 1
hw''p' : (Finset.affineCombination k fs'' p : (a : ι → k) → P) w'' = p'
hi :
  ∀ (i : (↑s : Type u_4)),
    ∃ (r : k),
      ∀ (j : ι),
        r * ((↑Finset.univ : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j
⊢ Eq.{u_1 + 1} (α := k) (∑ j : ι, (↑fs'' : Set ι).indicator w'' j) (∑ j ∈ fs'', w'' j)

Tactic:
exact Finset.sum_indicator_subset _ (by simp)

Premises used: Finset.sum_indicator_subset
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j : ι, w i j) 1
p' : P
hp' :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι))
          (singleton (α := P) ((Finset.affineCombination k Finset.univ p : (a : ι → k) → P) (w i) : P))))
      p'
w'' : ι → k
fs'' : Finset ι
hw'' : Eq.{u_1 + 1} (α := k) (∑ j ∈ fs'', w'' j) 1
hw''p' : (Finset.affineCombination k fs'' p : (a : ι → k) → P) w'' = p'
hi :
  ∀ (i : (↑s : Type u_4)),
    ∃ (r : k),
      ∀ (j : ι),
        r * ((↑Finset.univ : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j
refine_2 :
  Eq.{u_3 + 1} (α := P)
    ((Finset.affineCombination k Finset.univ p : (a : ι → k) → P) ((↑fs'' : Set ι).indicator w'') : P)
    ((Finset.affineCombination k fs'' p : (a : ι → k) → P) w'' : P)
⊢ (Finset.affineCombination k Finset.univ p : (a : ι → k) → P) ((↑fs'' : Set ι).indicator w'') = p'

Tactic:
rw [← hw''p']
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Fintype ι
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j : ι, w i j) 1
p' : P
hp' :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι))
          (singleton (α := P) ((Finset.affineCombination k Finset.univ p : (a : ι → k) → P) (w i) : P))))
      p'
w'' : ι → k
fs'' : Finset ι
hw'' : Eq.{u_1 + 1} (α := k) (∑ j ∈ fs'', w'' j) 1
hw''p' : (Finset.affineCombination k fs'' p : (a : ι → k) → P) w'' = p'
hi :
  ∀ (i : (↑s : Type u_4)),
    ∃ (r : k),
      ∀ (j : ι),
        r * ((↑Finset.univ : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs'' : Set ι) \ {(↑i : ι)}).indicator w'' j
⊢ Eq.{u_3 + 1} (α := P)
    ((Finset.affineCombination k Finset.univ p : (a : ι → k) → P) ((↑fs'' : Set ι).indicator w'') : P)
    ((Finset.affineCombination k fs'' p : (a : ι → k) → P) w'' : P)

Tactic:
exact (Finset.affineCombination_indicator_subset _ _ (by simp)).symm

Premises used: Finset.affineCombination_indicator_subset, Eq.symm