awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ : P
p : ι → P
s : Set ι
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s)) p₁
rw rw₁ rw₂ :
  ∀ (h : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range fun (x : (↑s : Type u_1)) ↦ p (↑x : ι))) p₁),
    ∃ (fs : Finset ι) (w : ι → k),
      (↑fs : Set ι) ⊆ s ∧
        Eq.{u_2 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p₁ = (Finset.affineCombination k fs p : (a : ι → k) → P) w
rw₃ :
  ∀ (fs' : Finset (↑s : Type u_1)) (w' : (↑s : Type u_1) → k) (hw' : Eq.{u_2 + 1} (α := k) (∑ i ∈ fs', w' i) 1)
    (h :
      Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
        (affineSpan k (Set.range fun (x : (↑s : Type u_1)) ↦ p (↑x : ι)))
        ((Finset.affineCombination k fs' fun (x : (↑s : Type u_1)) ↦ p (↑x : ι) : (a : (↑s : Type u_1) → k) → P) w' :
          P)),
    ∃ (fs : Finset ι) (w : ι → k),
      (↑fs : Set ι) ⊆ s ∧
        Eq.{u_2 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧
          Eq.{u_4 + 1} (α := P)
            ((Finset.affineCombination k fs' fun (x : (↑s : Type u_1)) ↦ p (↑x : ι) : (a : (↑s : Type u_1) → k) → P)
                w' :
              P)
            ((Finset.affineCombination k fs p : (a : ι → k) → P) w : P)
⊢ ∃ (fs : Finset ι) (w : ι → k),
    (↑fs : Set ι) ⊆ s ∧
      Eq.{u_2 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p₁ = (Finset.affineCombination k fs p : (a : ι → k) → P) w
have rw₄ : ∀ (fs' : Finset (↑s : Type u_1)) (w' : (↑s : Type u_1) → k) (hw' : Eq.{u_2 + 1} (α := k) (∑ i ∈ fs', w' i) 1)
  (h :
    Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
      (affineSpan k (Set.range fun (x : (↑s : Type u_1)) ↦ p (↑x : ι)))
      ((Finset.affineCombination k fs' fun (x : (↑s : Type u_1)) ↦ p (↑x : ι) : (a : (↑s : Type u_1) → k) → P) w' : P)),
  Eq.{u_4 + 1} (α := P)
    ((Finset.affineCombination k fs' fun (x : (↑s : Type u_1)) ↦ p (↑x : ι) : (a : (↑s : Type u_1) → k) → P) w' : P)
    ((Finset.affineCombination k (Finset.map (Function.Embedding.subtype fun (x : ι) ↦ x ∈ s) fs') p : (a : ι → k) → P)
        fun (i : ι) ↦ if hi : i ∈ s then w' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) else 0 :
      P)
Tactic: classical
  rw [Set.image_eq_range] at h
  obtain ⟨fs', w', hw', rfl⟩ := eq_affineCombination_of_mem_affineSpan h
  refine ⟨fs'.map (Function.Embedding.subtype _), fun i ↦ if hi : i ∈ s then w' ⟨i, hi⟩ else 0,
    (by simp), (by simp [hw']), ?_⟩
  simp only [Finset.affineCombination_map, Function.Embedding.coe_subtype]
  exact fs'.affineCombination_congr (by simp) (by simp)
Cleared hypotheses: p₁, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (p '' s'))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have rw : Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
  (affineSpan k (Set.range fun (x : (↑s' : Type u_1)) ↦ p (↑x : ι)))
  ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
Tactic: rw [Set.image_eq_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
w' : (↑s' : Type u_1) → k := fun (i : (↑s' : Type u_1)) ↦ w (↑i : ι)
⊢ Eq.{u_2 + 1} (α := k) (∑ i ∈ s with i ∈ s', w i) 1
have rw : Eq.{u_2 + 1} (α := k) (∑ x ∈ s \ {x ∈ s | x ∈ s'}, w x) 0
Tactic: rw [← h, ← Finset.sum_sdiff (s₁ := {x ∈ s | x ∈ s'}) (s₂ := s) (by simp), right_eq_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
w' : (↑s' : Type u_1) → k := fun (i : (↑s' : Type u_1)) ↦ w (↑i : ι)
⊢ Eq.{u_2 + 1} (α := k) (∑ x ∈ s \ {x ∈ s | x ∈ s'}, w x) 0
have refine : ∀ x ∈ s \ {x ∈ s | x ∈ s'}, w x = 0
Tactic: refine Finset.sum_eq_zero ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (hypothesis)
Goal:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
w' : (↑s' : Type u_1) → k := fun (i : (↑s' : Type u_1)) ↦ w (↑i : ι)
i : ι
hi : i ∈ s \ {x ∈ s | x ∈ s'}
⊢ w i = 0
have hi₁ : i ∈ s ∧ (i ∈ s → i ∉ s')
Tactic: simp only [Finset.mem_sdiff, Finset.mem_filter, not_and] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (hypothesis)
Goal:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
w' : (↑s' : Type u_1) → k := fun (i : (↑s' : Type u_1)) ↦ w (↑i : ι)
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
    (affineSpan k (Set.range fun (x : (↑s' : Type u_1)) ↦ p (↑x : ι)))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have h' : Eq.{u_2 + 1} (α := k) (∑ i ∈ s with i ∈ s', w i) 1
Tactic: have h' : ∑ i ∈ s with i ∈ s', w i = 1 := by
    rw [← h, ← Finset.sum_sdiff (s₁ := {x ∈ s | x ∈ s'}) (s₂ := s) (by simp), right_eq_add]
    refine Finset.sum_eq_zero ?_
    intro i hi
    simp only [Finset.mem_sdiff, Finset.mem_filter, not_and] at hi
    exact hs' i hi.1 (hi.2 hi.1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (hypothesis)
Goal:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
w' : (↑s' : Type u_1) → k := fun (i : (↑s' : Type u_1)) ↦ w (↑i : ι)
h' : Eq.{u_2 + 1} (α := k) (∑ i ∈ s with i ∈ s', w i) 1
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
    (affineSpan k (Set.range fun (x : (↑s' : Type u_1)) ↦ p (↑x : ι)))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have h'₁ : Eq.{u_2 + 1} (α := k) (∑ x ∈ Finset.subtype (Membership.mem s') s, w (↑x : ι)) 1
Tactic: rw [← Finset.sum_subtype_eq_sum_filter] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
w' : (↑s' : Type u_1) → k := fun (i : (↑s' : Type u_1)) ↦ w (↑i : ι)
h' : Eq.{u_2 + 1} (α := k) (∑ x ∈ Finset.subtype (Membership.mem s') s, w (↑x : ι)) 1
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
    (affineSpan k (Set.range fun (x : (↑s' : Type u_1)) ↦ p (↑x : ι)))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have h₁ : Eq.{u_4 + 1} (α := P) ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
  ((Finset.affineCombination k (Finset.subtype (Membership.mem s') s) fun (x : Subtype (Membership.mem s')) ↦
          p (↑x : ι) :
        (a : Subtype (Membership.mem s') → k) → P)
      fun (i : Subtype (Membership.mem s')) ↦ w (↑i : ι) :
    P)
Tactic: convert! affineCombination_mem_affineSpan h' (fun x ↦ p x)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
w' : (↑s' : Type u_1) → k := fun (i : (↑s' : Type u_1)) ↦ w (↑i : ι)
h' : Eq.{u_2 + 1} (α := k) (∑ x ∈ Finset.subtype (Membership.mem s') s, w (↑x : ι)) 1
⊢ Eq.{u_4 + 1} (α := P) ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
    ((Finset.affineCombination k (Finset.subtype (Membership.mem s') s) fun (x : Subtype (Membership.mem s')) ↦
            p (↑x : ι) :
          (a : Subtype (Membership.mem s') → k) → P)
        fun (i : Subtype (Membership.mem s')) ↦ w (↑i : ι) :
      P)
have h₁ : Eq.{u_4 + 1} (α := P) ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
  ((Finset.affineCombination k s p : (a : ι → k) → P) ((↑({x ∈ s | x ∈ s'}) : Set ι).indicator w) : P)
Tactic: rw [Finset.affineCombination_subtype_eq_filter, Finset.affineCombination_indicator_subset w p
    (Finset.filter_subset _ _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
w' : (↑s' : Type u_1) → k := fun (i : (↑s' : Type u_1)) ↦ w (↑i : ι)
h' : Eq.{u_2 + 1} (α := k) (∑ x ∈ Finset.subtype (Membership.mem s') s, w (↑x : ι)) 1
⊢ Eq.{u_4 + 1} (α := P) ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
    ((Finset.affineCombination k s p : (a : ι → k) → P) ((↑({x ∈ s | x ∈ s'}) : Set ι).indicator w) : P)
have h₁ : ∀ (i : ι) (hi : i ∈ s), w i = (↑({x ∈ s | x ∈ s'}) : Set ι).indicator w i
Tactic: refine Finset.affineCombination_congr _ (fun i hi ↦ ?_) (fun _ _ ↦ rfl)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (p '' s'))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have rw : Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
  (affineSpan k (Set.range fun (x : (↑s' : Type u_1)) ↦ p (↑x : ι)))
  ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
Tactic: classical
  rw [Set.image_eq_range]
  let w' : s' → k := fun i ↦ w i
  have h' : ∑ i ∈ s with i ∈ s', w i = 1 := by
    rw [← h, ← Finset.sum_sdiff (s₁ := {x ∈ s | x ∈ s'}) (s₂ := s) (by simp), right_eq_add]
    refine Finset.sum_eq_zero ?_
    intro i hi
    simp only [Finset.mem_sdiff, Finset.mem_filter, not_and] at hi
    exact hs' i hi.1 (hi.2 hi.1)
  rw [← Finset.sum_subtype_eq_sum_filter] at h'
  convert! affineCombination_mem_affineSpan h' (fun x ↦ p x)
  rw [Finset.affineCombination_subtype_eq_filter, Finset.affineCombination_indicator_subset w p
    (Finset.filter_subset _ _)]
  refine Finset.affineCombination_congr _ (fun i hi ↦ ?_) (fun _ _ ↦ rfl)
  simp_all [Set.indicator_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
rw rw₁ rw₂ :
  Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
    (affineSpan k (Set.range fun (x : (↑s' : Type u_1)) ↦ p (↑x : ι)))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
rw₃ :
  Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
    (affineSpan k (Set.range fun (x : (↑s' : Type u_1)) ↦ p (↑x : ι)))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (p '' s'))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have rw₄ : ∀ (h' : Eq.{u_2 + 1} (α := k) (∑ i ∈ s with i ∈ s', w i) 1),
  Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
    (affineSpan k (Set.range fun (x : (↑s' : Type u_1)) ↦ p (↑x : ι)))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
Tactic: classical
  rw [Set.image_eq_range]
  let w' : s' → k := fun i ↦ w i
  have h' : ∑ i ∈ s with i ∈ s', w i = 1 := by
    rw [← h, ← Finset.sum_sdiff (s₁ := {x ∈ s | x ∈ s'}) (s₂ := s) (by simp), right_eq_add]
    refine Finset.sum_eq_zero ?_
    intro i hi
    simp only [Finset.mem_sdiff, Finset.mem_filter, not_and] at hi
    exact hs' i hi.1 (hi.2 hi.1)
  rw [← Finset.sum_subtype_eq_sum_filter] at h'
  convert! affineCombination_mem_affineSpan h' (fun x ↦ p x)
  rw [Finset.affineCombination_subtype_eq_filter, Finset.affineCombination_indicator_subset w p
    (Finset.filter_subset _ _)]
  refine Finset.affineCombination_congr _ (fun i hi ↦ ?_) (fun _ _ ↦ rfl)
  simp_all [Set.indicator_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
rw rw₁ rw₂ :
  Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
    (affineSpan k (Set.range fun (x : (↑s' : Type u_1)) ↦ p (↑x : ι)))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
rw₃ :
  Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
    (affineSpan k (Set.range fun (x : (↑s' : Type u_1)) ↦ p (↑x : ι)))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
rw₄ :
  ∀ (h' : Eq.{u_2 + 1} (α := k) (∑ i ∈ s with i ∈ s', w i) 1),
    Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
      (affineSpan k (Set.range fun (x : (↑s' : Type u_1)) ↦ p (↑x : ι)))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (p '' s'))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have rw₅ : ∀ (h' : Eq.{u_2 + 1} (α := k) (∑ x ∈ Finset.subtype (Membership.mem s') s, w (↑x : ι)) 1),
  Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
    (affineSpan k (Set.range fun (x : (↑s' : Type u_1)) ↦ p (↑x : ι)))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
Tactic: classical
  rw [Set.image_eq_range]
  let w' : s' → k := fun i ↦ w i
  have h' : ∑ i ∈ s with i ∈ s', w i = 1 := by
    rw [← h, ← Finset.sum_sdiff (s₁ := {x ∈ s | x ∈ s'}) (s₂ := s) (by simp), right_eq_add]
    refine Finset.sum_eq_zero ?_
    intro i hi
    simp only [Finset.mem_sdiff, Finset.mem_filter, not_and] at hi
    exact hs' i hi.1 (hi.2 hi.1)
  rw [← Finset.sum_subtype_eq_sum_filter] at h'
  convert! affineCombination_mem_affineSpan h' (fun x ↦ p x)
  rw [Finset.affineCombination_subtype_eq_filter, Finset.affineCombination_indicator_subset w p
    (Finset.filter_subset _ _)]
  refine Finset.affineCombination_congr _ (fun i hi ↦ ?_) (fun _ _ ↦ rfl)
  simp_all [Set.indicator_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
rw rw₁ rw₂ :
  Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
    (affineSpan k (Set.range fun (x : (↑s' : Type u_1)) ↦ p (↑x : ι)))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
rw₃ :
  Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
    (affineSpan k (Set.range fun (x : (↑s' : Type u_1)) ↦ p (↑x : ι)))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
rw₄ :
  ∀ (h' : Eq.{u_2 + 1} (α := k) (∑ i ∈ s with i ∈ s', w i) 1),
    Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
      (affineSpan k (Set.range fun (x : (↑s' : Type u_1)) ↦ p (↑x : ι)))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
rw₅ :
  ∀ (h' : Eq.{u_2 + 1} (α := k) (∑ x ∈ Finset.subtype (Membership.mem s') s, w (↑x : ι)) 1),
    Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
      (affineSpan k (Set.range fun (x : (↑s' : Type u_1)) ↦ p (↑x : ι)))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (p '' s'))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have h₁ : ∀ (h' : Eq.{u_2 + 1} (α := k) (∑ x ∈ Finset.subtype (Membership.mem s') s, w (↑x : ι)) 1),
  Eq.{u_4 + 1} (α := P) ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
    ((Finset.affineCombination k (Finset.subtype (Membership.mem s') s) fun (x : Subtype (Membership.mem s')) ↦
            p (↑x : ι) :
          (a : Subtype (Membership.mem s') → k) → P)
        fun (i : Subtype (Membership.mem s')) ↦ w (↑i : ι) :
      P)
Tactic: classical
  rw [Set.image_eq_range]
  let w' : s' → k := fun i ↦ w i
  have h' : ∑ i ∈ s with i ∈ s', w i = 1 := by
    rw [← h, ← Finset.sum_sdiff (s₁ := {x ∈ s | x ∈ s'}) (s₂ := s) (by simp), right_eq_add]
    refine Finset.sum_eq_zero ?_
    intro i hi
    simp only [Finset.mem_sdiff, Finset.mem_filter, not_and] at hi
    exact hs' i hi.1 (hi.2 hi.1)
  rw [← Finset.sum_subtype_eq_sum_filter] at h'
  convert! affineCombination_mem_affineSpan h' (fun x ↦ p x)
  rw [Finset.affineCombination_subtype_eq_filter, Finset.affineCombination_indicator_subset w p
    (Finset.filter_subset _ _)]
  refine Finset.affineCombination_congr _ (fun i hi ↦ ?_) (fun _ _ ↦ rfl)
  simp_all [Set.indicator_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
rw rw₁ rw₂ :
  Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
    (affineSpan k (Set.range fun (x : (↑s' : Type u_1)) ↦ p (↑x : ι)))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
rw₃ :
  Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
    (affineSpan k (Set.range fun (x : (↑s' : Type u_1)) ↦ p (↑x : ι)))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
rw₄ :
  ∀ (h' : Eq.{u_2 + 1} (α := k) (∑ i ∈ s with i ∈ s', w i) 1),
    Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
      (affineSpan k (Set.range fun (x : (↑s' : Type u_1)) ↦ p (↑x : ι)))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
rw₅ :
  ∀ (h' : Eq.{u_2 + 1} (α := k) (∑ x ∈ Finset.subtype (Membership.mem s') s, w (↑x : ι)) 1),
    Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
      (affineSpan k (Set.range fun (x : (↑s' : Type u_1)) ↦ p (↑x : ι)))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
h₁ :
  ∀ (h' : Eq.{u_2 + 1} (α := k) (∑ x ∈ Finset.subtype (Membership.mem s') s, w (↑x : ι)) 1),
    Eq.{u_4 + 1} (α := P) ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
      ((Finset.affineCombination k (Finset.subtype (Membership.mem s') s) fun (x : Subtype (Membership.mem s')) ↦
              p (↑x : ι) :
            (a : Subtype (Membership.mem s') → k) → P)
          fun (i : Subtype (Membership.mem s')) ↦ w (↑i : ι) :
        P)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (p '' s'))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have h₂ : ∀ (h' : Eq.{u_2 + 1} (α := k) (∑ x ∈ Finset.subtype (Membership.mem s') s, w (↑x : ι)) 1),
  Eq.{u_4 + 1} (α := P) ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
    ((Finset.affineCombination k s p : (a : ι → k) → P) ((↑({x ∈ s | x ∈ s'}) : Set ι).indicator w) : P)
Tactic: classical
  rw [Set.image_eq_range]
  let w' : s' → k := fun i ↦ w i
  have h' : ∑ i ∈ s with i ∈ s', w i = 1 := by
    rw [← h, ← Finset.sum_sdiff (s₁ := {x ∈ s | x ∈ s'}) (s₂ := s) (by simp), right_eq_add]
    refine Finset.sum_eq_zero ?_
    intro i hi
    simp only [Finset.mem_sdiff, Finset.mem_filter, not_and] at hi
    exact hs' i hi.1 (hi.2 hi.1)
  rw [← Finset.sum_subtype_eq_sum_filter] at h'
  convert! affineCombination_mem_affineSpan h' (fun x ↦ p x)
  rw [Finset.affineCombination_subtype_eq_filter, Finset.affineCombination_indicator_subset w p
    (Finset.filter_subset _ _)]
  refine Finset.affineCombination_congr _ (fun i hi ↦ ?_) (fun _ _ ↦ rfl)
  simp_all [Set.indicator_apply]