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
p1 : P
p : ι → P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1
have have₁ have₂ :
  ∀ (hn : (↑(affineSpan k (Set.range p)) : Set P).Nonempty),
    ∃ (s : Finset ι) (w : ι → k),
      Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
have₃ :
  ∀ (hn : Nonempty ι),
    ∃ (s : Finset ι) (w : ι → k),
      Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
have₄ :
  ∀ (i0 : ι),
    ∃ (s : Finset ι) (w : ι → k),
      Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
⊢ ∃ (s : Finset ι) (w : ι → k),
    Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
have have₅ : ∀ (i0 : ι) (h0 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) (p i0)),
  ∃ (s : Finset ι) (w : ι → k),
    Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
Tactic: classical
    have hn : (affineSpan k (Set.range p) : Set P).Nonempty := ⟨p1, h⟩
    rw [affineSpan_nonempty, Set.range_nonempty_iff_nonempty] at hn
    obtain ⟨i0⟩ := hn
    have h0 : p i0 ∈ affineSpan k (Set.range p) := mem_affineSpan k (Set.mem_range_self i0)
    have hd : p1 -ᵥ p i0 ∈ (affineSpan k (Set.range p)).direction :=
      AffineSubspace.vsub_mem_direction h h0
    rw [direction_affineSpan, mem_vectorSpan_iff_eq_weightedVSub] at hd
    rcases hd with ⟨s, w, h, hs⟩
    let s' := insert i0 s
    let w' := Set.indicator (↑s) w
    have h' : ∑ i ∈ s', w' i = 0 := by
      rw [← h, Finset.sum_indicator_subset _ (Finset.subset_insert i0 s)]
    have hs' : s'.weightedVSub p w' = p1 -ᵥ p i0 := by
      rw [hs]
      exact (Finset.weightedVSub_indicator_subset _ _ (Finset.subset_insert i0 s)).symm
    let w0 : ι → k := Function.update (Function.const ι 0) i0 1
    have hw0 : ∑ i ∈ s', w0 i = 1 := by
      rw [Finset.sum_update_of_mem (Finset.mem_insert_self _ _)]
      simp only [Function.const_apply, Finset.sum_const_zero,
        add_zero]
    have hw0s : s'.affineCombination k p w0 = p i0 :=
      s'.affineCombination_of_eq_one_of_eq_zero w0 p (Finset.mem_insert_self _ _)
        (Function.update_self ..) fun _ _ hne => Function.update_of_ne hne _ _
    refine ⟨s', w0 + w', ?_, ?_⟩
    · simp [Pi.add_apply, Finset.sum_add_distrib, hw0, h']
    · rw [add_comm, ← Finset.weightedVSub_vadd_affineCombination, hw0s, hs', vsub_vadd]
-- 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
p1 : P
p : ι → P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1
have have₁ have₂ :
  ∀ (hn : (↑(affineSpan k (Set.range p)) : Set P).Nonempty),
    ∃ (s : Finset ι) (w : ι → k),
      Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
have₃ :
  ∀ (hn : Nonempty ι),
    ∃ (s : Finset ι) (w : ι → k),
      Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
have₄ :
  ∀ (i0 : ι),
    ∃ (s : Finset ι) (w : ι → k),
      Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
have₅ :
  ∀ (i0 : ι) (h0 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) (p i0)),
    ∃ (s : Finset ι) (w : ι → k),
      Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
⊢ ∃ (s : Finset ι) (w : ι → k),
    Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
have have₆ : ∀ (i0 : ι) (h0 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) (p i0))
  (hd : Membership.mem (γ := Submodule k V) (AffineSubspace.direction (affineSpan k (Set.range p))) (p1 -ᵥ p i0)),
  ∃ (s : Finset ι) (w : ι → k),
    Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
Tactic: classical
    have hn : (affineSpan k (Set.range p) : Set P).Nonempty := ⟨p1, h⟩
    rw [affineSpan_nonempty, Set.range_nonempty_iff_nonempty] at hn
    obtain ⟨i0⟩ := hn
    have h0 : p i0 ∈ affineSpan k (Set.range p) := mem_affineSpan k (Set.mem_range_self i0)
    have hd : p1 -ᵥ p i0 ∈ (affineSpan k (Set.range p)).direction :=
      AffineSubspace.vsub_mem_direction h h0
    rw [direction_affineSpan, mem_vectorSpan_iff_eq_weightedVSub] at hd
    rcases hd with ⟨s, w, h, hs⟩
    let s' := insert i0 s
    let w' := Set.indicator (↑s) w
    have h' : ∑ i ∈ s', w' i = 0 := by
      rw [← h, Finset.sum_indicator_subset _ (Finset.subset_insert i0 s)]
    have hs' : s'.weightedVSub p w' = p1 -ᵥ p i0 := by
      rw [hs]
      exact (Finset.weightedVSub_indicator_subset _ _ (Finset.subset_insert i0 s)).symm
    let w0 : ι → k := Function.update (Function.const ι 0) i0 1
    have hw0 : ∑ i ∈ s', w0 i = 1 := by
      rw [Finset.sum_update_of_mem (Finset.mem_insert_self _ _)]
      simp only [Function.const_apply, Finset.sum_const_zero,
        add_zero]
    have hw0s : s'.affineCombination k p w0 = p i0 :=
      s'.affineCombination_of_eq_one_of_eq_zero w0 p (Finset.mem_insert_self _ _)
        (Function.update_self ..) fun _ _ hne => Function.update_of_ne hne _ _
    refine ⟨s', w0 + w', ?_, ?_⟩
    · simp [Pi.add_apply, Finset.sum_add_distrib, hw0, h']
    · rw [add_comm, ← Finset.weightedVSub_vadd_affineCombination, hw0s, hs', vsub_vadd]
-- 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 : Fintype ι
p1 : P
p : ι → P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1
⊢ ∃ (w : ι → k),
    Eq.{u_2 + 1} (α := k) (∑ i : ι, w i) 1 ∧ p1 = (Finset.affineCombination k Finset.univ p : (a : ι → k) → P) w
have obtain : ∀ (s : Finset ι) (w : ι → k) (hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1)
  (h :
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)),
  ∃ (w_1 : ι → k),
    Eq.{u_2 + 1} (α := k) (∑ i : ι, w_1 i) 1 ∧
      Eq.{u_4 + 1} (α := P) ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
        ((Finset.affineCombination k Finset.univ p : (a : ι → k) → P) w_1 : P)
Tactic: obtain ⟨s, w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan h
Cleared hypotheses: p1, 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 : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
h :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
⊢ ∃ (w_1 : ι → k),
    Eq.{u_2 + 1} (α := k) (∑ i : ι, w_1 i) 1 ∧
      Eq.{u_4 + 1} (α := P) ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
        ((Finset.affineCombination k Finset.univ p : (a : ι → k) → P) w_1 : P)
have Set : Eq.{u_2 + 1} (α := k) (∑ i : ι, (↑s : Set ι).indicator w i) 1
Tactic: refine
      ⟨(s : Set ι).indicator w, ?_, Finset.affineCombination_indicator_subset w p s.subset_univ⟩
-- 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 : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
h :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
⊢ Eq.{u_2 + 1} (α := k) (∑ i : ι, (↑s : Set ι).indicator w i) 1
have simp : Eq.{u_2 + 1} (α := k) (∑ x : ι, if x ∈ s then w x else 0) (∑ i ∈ s, w i)
Tactic: simp only [Finset.mem_coe, Set.indicator_apply, ← hw]
-- 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 : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
h :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
⊢ Eq.{u_2 + 1} (α := k) (∑ x : ι, if x ∈ s then w x else 0) (∑ i ∈ s, w i)
have rw : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) (∑ i ∈ s, w i)
Tactic: rw [Fintype.sum_extend_by_zero s w]
-- 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 : Fintype ι
p1 : P
p : ι → P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1
⊢ ∃ (w : ι → k),
    Eq.{u_2 + 1} (α := k) (∑ i : ι, w i) 1 ∧ p1 = (Finset.affineCombination k Finset.univ p : (a : ι → k) → P) w
have obtain : ∀ (s : Finset ι) (w : ι → k) (hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1)
  (h :
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)),
  ∃ (w_1 : ι → k),
    Eq.{u_2 + 1} (α := k) (∑ i : ι, w_1 i) 1 ∧
      Eq.{u_4 + 1} (α := P) ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
        ((Finset.affineCombination k Finset.univ p : (a : ι → k) → P) w_1 : P)
Tactic: classical
    obtain ⟨s, w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan h
    refine
      ⟨(s : Set ι).indicator w, ?_, Finset.affineCombination_indicator_subset w p s.subset_univ⟩
    simp only [Finset.mem_coe, Set.indicator_apply, ← hw]
    rw [Fintype.sum_extend_by_zero s w]
Cleared hypotheses: p1, 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 : Fintype ι
p1 : P
p : ι → P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1
obtain :
  ∀ (s : Finset ι) (w : ι → k) (hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1)
    (h :
      Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
        ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)),
    ∃ (w_1 : ι → k),
      Eq.{u_2 + 1} (α := k) (∑ i : ι, w_1 i) 1 ∧
        Eq.{u_4 + 1} (α := P) ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
          ((Finset.affineCombination k Finset.univ p : (a : ι → k) → P) w_1 : P)
⊢ ∃ (w : ι → k),
    Eq.{u_2 + 1} (α := k) (∑ i : ι, w i) 1 ∧ p1 = (Finset.affineCombination k Finset.univ p : (a : ι → k) → P) w
have obtain₁ : ∀ (s : Finset ι) (w : ι → k) (hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1)
  (h :
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)),
  Eq.{u_2 + 1} (α := k) (∑ i : ι, (↑s : Set ι).indicator w i) 1
Tactic: classical
    obtain ⟨s, w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan h
    refine
      ⟨(s : Set ι).indicator w, ?_, Finset.affineCombination_indicator_subset w p s.subset_univ⟩
    simp only [Finset.mem_coe, Set.indicator_apply, ← hw]
    rw [Fintype.sum_extend_by_zero s w]
Cleared hypotheses: p1, 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 : Fintype ι
p1 : P
p : ι → P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1
obtain :
  ∀ (s : Finset ι) (w : ι → k) (hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1)
    (h :
      Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
        ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)),
    ∃ (w_1 : ι → k),
      Eq.{u_2 + 1} (α := k) (∑ i : ι, w_1 i) 1 ∧
        Eq.{u_4 + 1} (α := P) ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
          ((Finset.affineCombination k Finset.univ p : (a : ι → k) → P) w_1 : P)
obtain₁ :
  ∀ (s : Finset ι) (w : ι → k) (hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1)
    (h :
      Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
        ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)),
    Eq.{u_2 + 1} (α := k) (∑ i : ι, (↑s : Set ι).indicator w i) 1
⊢ ∃ (w : ι → k),
    Eq.{u_2 + 1} (α := k) (∑ i : ι, w i) 1 ∧ p1 = (Finset.affineCombination k Finset.univ p : (a : ι → k) → P) w
have obtain₂ : ∀ (s : Finset ι) (w : ι → k) (hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1)
  (h :
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)),
  Eq.{u_2 + 1} (α := k) (∑ x : ι, if x ∈ s then w x else 0) (∑ i ∈ s, w i)
Tactic: classical
    obtain ⟨s, w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan h
    refine
      ⟨(s : Set ι).indicator w, ?_, Finset.affineCombination_indicator_subset w p s.subset_univ⟩
    simp only [Finset.mem_coe, Set.indicator_apply, ← hw]
    rw [Fintype.sum_extend_by_zero s w]
Cleared hypotheses: p1, h
-- 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
p₁ : P
p : ι → P
s : Set ι
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s)) 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 h₁ : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range fun (x : (↑s : Type u_1)) ↦ p (↑x : ι))) p₁
Tactic: rw [Set.image_eq_range] 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
p₁ : P
p : ι → P
s : Set ι
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
have obtain : ∀ (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)
Tactic: obtain ⟨fs', w', hw', rfl⟩ := eq_affineCombination_of_mem_affineSpan h
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
p : ι → P
s : Set ι
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)
have refine : 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: refine ⟨fs'.map (Function.Embedding.subtype _), fun i ↦ if hi : i ∈ s then w' ⟨i, hi⟩ else 0,
    (by simp), (by simp [hw']), ?_⟩
-- 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
s : Set ι
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)
have simp : 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 ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) : (a : { x : ι // x ∈ s } → k) → P)
      ((fun (i : ι) ↦ if hi : i ∈ s then w' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) else 0) ∘
        Subtype.val (p := fun (x : ι) ↦ x ∈ s)) :
    P)
Tactic: simp only [Finset.affineCombination_map, Function.Embedding.coe_subtype]
-- 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₁
⊢ ∃ (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 : ∀ (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
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: 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
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
⊢ ∃ (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)),
  ∃ (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)
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