-- 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 ι
hfs : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fs i
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'
have :
  ∀ (i : (↑s : Type u_4)),
    ∃ (r : k),
      (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
          ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
            (j : ι) → k) =
        p'
have₁ :
  ∀
    (hp'' :
      ∀ (i : (↑s : Type u_4)),
        ∃ (r : k),
          (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
              ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
                (j : ι) → k) =
            p'),
    ∃ (w' : ι → k) (fs' : Finset ι),
      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 * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
have₂ :
  ∀ (i : (↑s : Type u_4)),
    ∃ (r : k),
      (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
          ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
            (j : ι) → k) =
        p'
have₃ have₄ :
  ∀
    (hp'' :
      ∀ (i : (↑s : Type u_4)),
        ∃ (r : k),
          (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
              ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
                (j : ι) → k) =
            p'),
    ∃ (w' : ι → k) (fs' : Finset ι),
      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 * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
have₅ :
  ∀
    (hp'' :
      ∀ (i : (↑s : Type u_4)),
        ∃ (r : k),
          (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
              ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
                (j : ι) → k) =
            p')
    (i' : ι) (hi' : i' ∈ s),
    ∃ (w' : ι → k) (fs' : Finset ι),
      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 * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
have₆ have₇ :
  ∀
    (hp'' :
      ∀ (i : (↑s : Type u_4)),
        ∃ (r : k),
          (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
              ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
                (j : ι) → k) =
            p')
    (i' : ι) (hi' : i' ∈ s) (ri' : k)
    (hri' :
      (Finset.affineCombination k (fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) p : (a : ι → k) → P)
          ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi') : ι) 1)
                  (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
                (a : k) → (j : ι) → k)
              ri' :
            (j : ι) → k) =
        p'),
    ∃ (w' : ι → k) (fs' : Finset ι),
      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 * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j
refine_1 :
  ∀
    (hp'' :
      ∀ (i : (↑s : Type u_4)),
        ∃ (r : k),
          (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
              ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
                (j : ι) → k) =
            p')
    (i' : ι) (hi' : i' ∈ s) (ri' : k)
    (hri' :
      (Finset.affineCombination k (fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) p : (a : ι → k) → P)
          ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi') : ι) 1)
                  (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
                (a : k) → (j : ι) → k)
              ri' :
            (j : ι) → k) =
        p'),
    let w' : ι → k :=
      (AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) i' 1) (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
          (a : k) → (j : ι) → k)
        ri';
    Eq.{u_1 + 1} (α := k) (∑ j ∈ fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi'), w' j) 1
refine_2 :
  ∀
    (hp'' :
      ∀ (i : (↑s : Type u_4)),
        ∃ (r : k),
          (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
              ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
                (j : ι) → k) =
            p')
    (i' : ι) (hi' : i' ∈ s) (ri' : k)
    (hri' :
      (Finset.affineCombination k (fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) p : (a : ι → k) → P)
          ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi') : ι) 1)
                  (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
                (a : k) → (j : ι) → k)
              ri' :
            (j : ι) → k) =
        p'),
    let w' : ι → k :=
      (AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) i' 1) (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
          (a : k) → (j : ι) → k)
        ri';
    (Finset.affineCombination k (fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) p : (a : ι → k) → P) w' = p'
refine_3 :
  ∀
    (hp'' :
      ∀ (i : (↑s : Type u_4)),
        ∃ (r : k),
          (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
              ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
                (j : ι) → k) =
            p')
    (i' : ι) (hi' : i' ∈ s) (ri' : k)
    (hri' :
      (Finset.affineCombination k (fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) p : (a : ι → k) → P)
          ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi') : ι) 1)
                  (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
                (a : k) → (j : ι) → k)
              ri' :
            (j : ι) → k) =
        p'),
    let w' : ι → k :=
      (AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) i' 1) (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
          (a : k) → (j : ι) → k)
        ri';
    ∀ (i : (↑s : Type u_4)),
      ∃ (r : k),
        ∀ (j : ι),
          r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j =
            ((↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) : Set ι) \ {(↑i : ι)}).indicator w' j
refine_2₁ :
  ∀
    (hp'' :
      ∀ (i : (↑s : Type u_4)),
        ∃ (r : k),
          (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
              ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
                (j : ι) → k) =
            p')
    (i' : ι) (hi' : i' ∈ s) (ri' : k)
    (hri' :
      (Finset.affineCombination k (fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) p : (a : ι → k) → P)
          ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi') : ι) 1)
                  (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
                (a : k) → (j : ι) → k)
              ri' :
            (j : ι) → k) =
        p'),
    let w' : ι → k :=
      (AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) i' 1) (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
          (a : k) → (j : ι) → k)
        ri';
    (Finset.affineCombination k (fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) p : (a : ι → k) → P) w' = p'
refine_3₁ refine_3₂ :
  ∀
    (hp'' :
      ∀ (i : (↑s : Type u_4)),
        ∃ (r : k),
          (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
              ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
                (j : ι) → k) =
            p')
    (i' : ι) (hi' : i' ∈ s) (ri' : k)
    (hri' :
      (Finset.affineCombination k (fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) p : (a : ι → k) → P)
          ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi') : ι) 1)
                  (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
                (a : k) → (j : ι) → k)
              ri' :
            (j : ι) → k) =
        p'),
    let w' : ι → k :=
      (AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) i' 1) (w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) :
          (a : k) → (j : ι) → k)
        ri';
    ∀ (i : (↑s : Type u_4)),
      ∃ (r : k),
        ∀ (j : ι),
          r * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j =
            ((↑(fs (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i' hi')) : Set ι) \ {(↑i : ι)}).indicator w' j
⊢ ∃ (w' : ι → k) (fs' : Finset ι),
    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 * ((↑(fs i) : Set ι) \ {(↑i : ι)}).indicator (w i) j = ((↑fs' : Set ι) \ {(↑i : ι)}).indicator w' j

Tactic:
classical
  have hp'' : ∀ i : s, ∃ r : k, (fs i).affineCombination k p
      (AffineMap.lineMap (Pi.single (i : ι) 1) (w i) r) = p' := by
    intro i
    simp_rw [mem_affineSpan_pair_iff_exists_lineMap_eq] at hp'
    obtain ⟨r, rfl⟩ := hp' i
    exact ⟨r, by simp [hfs]⟩
  obtain ⟨i', hi'⟩ := hs
  obtain ⟨ri', hri'⟩ := hp'' ⟨i', hi'⟩
  let w' : ι → k := AffineMap.lineMap (Pi.single i' 1) (w ⟨i', hi'⟩) ri'
  refine ⟨w', fs ⟨i', hi'⟩, ?_, ?_, ?_⟩
  · simp [w', AffineMap.lineMap_apply_module, Finset.sum_add_distrib, ← Finset.mul_sum, hw, hfs]
  · simp [w', hri']
  · intro i
    obtain ⟨r, hr⟩ := hp'' i
    refine ⟨r, ?_⟩
    rw [← hri'] at hr
    simp only [AffineMap.lineMap_apply_module] at hr
    have hind := hp.indicator_eq_of_affineCombination_eq _ _ _ _ ?_ ?_ hr
    · intro j
      by_cases hj : j = i
      · simp [hj]
      replace hind := congr_fun hind j
      convert! hind using 1
      · simp [Set.indicator_apply, hj]
      · simp [Set.indicator_apply, hj, w', AffineMap.lineMap_apply_module]
    · simp [Finset.sum_add_distrib, ← Finset.mul_sum, hw, hfs]
    · simp [Finset.sum_add_distrib, ← Finset.mul_sum, hw, hfs]

Premises used: AffineMap.lineMap_apply_module, Finset.mul_sum, Set.indicator_apply, Finset.sum_add_distrib