-- 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
intro intro₁ intro₂ intro₃ intro₄ intro₅ :
  ∀ (fs : Finset ι2) (w : ι2 → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0)
    (hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V))
    (i0 : ι2) (hi0 : i0 ∈ fs), w i0 = 0
intro₆ intro₇ :
  ∀ (fs : Finset ι2) (w : ι2 → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0)
    (hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V))
    (i0 : ι2) (hi0 : i0 ∈ fs), w i0 = 0
intro₈ :
  ∀ (fs : Finset ι2) (w : ι2 → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0)
    (hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V))
    (i0 : ι2) (hi0 : i0 ∈ fs),
    let w' : (i : ι) → k := fun (i : ι) ↦
      if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
      else 0;
    ∀ (hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2), w i0 = 0
intro₉ :
  ∀ (fs : Finset ι2) (w : ι2 → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0)
    (hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V))
    (i0 : ι2) (hi0 : i0 ∈ fs),
    let fs' := map f fs;
    let w' : (i : ι) → k := fun (i : ι) ↦
      if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
      else 0;
    ∀ (hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2) (hw's : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs', w' i) 0),
      w i0 = 0
⊢ AffineIndependent.{u_1, u_2, u_3, u_5} k (ι := ι2) (p ∘ (⇑f : (a : ι2) → ι))
have intro₁₀ : ∀ (fs : Finset ι2) (w : ι2 → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0)
  (hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)) (i0 : ι2)
  (hi0 : i0 ∈ fs),
  let fs' := map f fs;
  let w' : (i : ι) → k := fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0;
  ∀ (hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2) (hw's : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs', w' i) 0)
    (hs' : Eq.{u_2 + 1} (α := V) ((fs'.weightedVSub p : (a : ι → k) → V) w' : V) (0 : V)), w i0 = 0
Tactic: classical
    intro fs w hw hs i0 hi0
    let fs' := fs.map f
    let w' i := if h : ∃ i2, f i2 = i then w h.choose else 0
    have hw' : ∀ i2 : ι2, w' (f i2) = w i2 := by
      intro i2
      have h : ∃ i : ι2, f i = f i2 := ⟨i2, rfl⟩
      have hs : h.choose = i2 := f.injective h.choose_spec
      simp_rw [w', dif_pos h, hs]
    have hw's : ∑ i ∈ fs', w' i = 0 := by
      rw [← hw, Finset.sum_map]
      simp [hw']
    have hs' : fs'.weightedVSub p w' = (0 : V) := by
      rw [← hs, Finset.weightedVSub_map]
      congr with i
      simp_all only [comp_apply]
    rw [← ha fs' w' hw's hs' (f i0) ((Finset.mem_map' _).2 hi0), hw']