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
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)
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)
⊢ 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) (i : ι) (hi : i ∈ s),
  w i = (↑({x ∈ s | x ∈ s'}) : Set ι).indicator w i
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
p1 : P
p : ι → P
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1 ↔
    ∃ (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 mp : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1 →
  ∃ (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: constructor
-- 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
p1 : P
p : ι → P
mp :
  Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1 →
    ∃ (s : Finset ι) (w : ι → k),
      Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1 ↔
    ∃ (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 mpr : (∃ (s : Finset ι) (w : ι → k),
    Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w) →
  Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1
Tactic: constructor
-- 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
p : ι → P
j : ι
q : P
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) q ↔
    ∃ (s : Finset ι) (w : ι → k),
      q = HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) ((s.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w : V) (p j)
have mp : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) q →
  ∃ (s : Finset ι) (w : ι → k),
    q = HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) ((s.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w : V) (p j)
Tactic: constructor
-- 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
p : ι → P
j : ι
q : P
mp :
  Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) q →
    ∃ (s : Finset ι) (w : ι → k),
      q = HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) ((s.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w : V) (p j)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) q ↔
    ∃ (s : Finset ι) (w : ι → k),
      q = HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) ((s.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w : V) (p j)
have mpr : (∃ (s : Finset ι) (w : ι → k),
    q = HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) ((s.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w : V) (p j)) →
  Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) q
Tactic: constructor
-- 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
p : ι → P
j : ι
q : P
hq : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) q
⊢ ∃ (s : Finset ι) (w : ι → k),
    q = HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) ((s.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w : V) (p j)
have mp : ∀ (s : Finset ι) (w : ι → k) (hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1)
  (hq :
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)),
  ∃ (s_1 : Finset ι) (w_1 : ι → k),
    (Finset.affineCombination k s p : (a : ι → k) → P) w =
      HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) ((s_1.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w_1 : V) (p j)
Tactic: obtain ⟨s, w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan hq
Cleared hypotheses: q, hq
-- 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
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w)
⊢ (insert j s).sum w' = 1
have pos : ∀ (hj : j ∈ s), (insert j s).sum w' = 1
Tactic: by_cases hj : j ∈ s
-- 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
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w)
pos : ∀ (hj : j ∈ s), (insert j s).sum w' = 1
⊢ (insert j s).sum w' = 1
have neg : ∀ (hj : j ∉ s), (insert j s).sum w' = 1
Tactic: by_cases hj : j ∈ s
-- 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
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w)
hj : j ∉ s
neg : Eq.{u_2 + 1} (α := k) (∑ x ∈ insert j s, Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w) x) 1
⊢ (insert j s).sum w' = 1
have neg₁ : Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w) j +
    ∑ x ∈ s, Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w) x =
  1
Tactic: simp_rw [w', Finset.sum_insert hj, Finset.sum_update_of_notMem hj, Function.update_self,
            ← Finset.erase_eq, Finset.erase_eq_of_notMem hj, sub_add_cancel]
-- 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
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w)
hj : j ∉ s
neg : Eq.{u_2 + 1} (α := k) (∑ x ∈ insert j s, Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w) x) 1
neg₁ :
  Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w) j +
      ∑ x ∈ s, Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w) x =
    1
⊢ (insert j s).sum w' = 1
have neg₂ : Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w) j + ∑ x ∈ s, w x = 1
Tactic: simp_rw [w', Finset.sum_insert hj, Finset.sum_update_of_notMem hj, Function.update_self,
            ← Finset.erase_eq, Finset.erase_eq_of_notMem hj, sub_add_cancel]
-- 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
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w)
hj : j ∉ s
neg : Eq.{u_2 + 1} (α := k) (∑ x ∈ insert j s, Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w) x) 1
neg₁ :
  Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w) j +
      ∑ x ∈ s, Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w) x =
    1
neg₂ : Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w) j + ∑ x ∈ s, w x = 1
⊢ (insert j s).sum w' = 1
have neg₃ : 1 - (s \ {j}).sum w + ∑ x ∈ s, w x = 1
Tactic: simp_rw [w', Finset.sum_insert hj, Finset.sum_update_of_notMem hj, Function.update_self,
            ← Finset.erase_eq, Finset.erase_eq_of_notMem hj, sub_add_cancel]
-- 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
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w)
hj : j ∉ s
neg : Eq.{u_2 + 1} (α := k) (∑ x ∈ insert j s, Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w) x) 1
neg₁ :
  Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w) j +
      ∑ x ∈ s, Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w) x =
    1
neg₂ : Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w) j + ∑ x ∈ s, w x = 1
neg₃ : 1 - (s \ {j}).sum w + ∑ x ∈ s, w x = 1
⊢ (insert j s).sum w' = 1
have neg₄ : HSub.hSub (α := k) 1 (∑ x ∈ s.erase j, w x) + ∑ x ∈ s, w x = 1
Tactic: simp_rw [w', Finset.sum_insert hj, Finset.sum_update_of_notMem hj, Function.update_self,
            ← Finset.erase_eq, Finset.erase_eq_of_notMem hj, sub_add_cancel]
-- 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
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w)
hj : j ∉ s
neg : Eq.{u_2 + 1} (α := k) (∑ x ∈ insert j s, Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w) x) 1
neg₁ :
  Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w) j +
      ∑ x ∈ s, Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w) x =
    1
neg₂ : Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w) j + ∑ x ∈ s, w x = 1
neg₃ : 1 - (s \ {j}).sum w + ∑ x ∈ s, w x = 1
neg₄ : HSub.hSub (α := k) 1 (∑ x ∈ s.erase j, w x) + ∑ x ∈ s, w x = 1
⊢ (insert j s).sum w' = 1
have neg₅ : HSub.hSub (α := k) 1 (∑ x ∈ s, w x) + ∑ x ∈ s, w x = 1
Tactic: simp_rw [w', Finset.sum_insert hj, Finset.sum_update_of_notMem hj, Function.update_self,
            ← Finset.erase_eq, Finset.erase_eq_of_notMem hj, sub_add_cancel]
-- 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
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    (HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) ((s.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w : V) (p j))
have h₁ : (insert j s).sum w' = 1
Tactic: have h₁ : (insert j s).sum w' = 1 := by
        by_cases hj : j ∈ s
        · simp [w', Finset.sum_update_of_mem hj, Finset.insert_eq_of_mem hj]
        · simp_rw [w', Finset.sum_insert hj, Finset.sum_update_of_notMem hj, Function.update_self,
            ← Finset.erase_eq, Finset.erase_eq_of_notMem hj, sub_add_cancel]
-- 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
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w)
h₁ : (insert j s).sum w' = 1
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    (HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) ((s.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w : V) (p j))
have hww : ∀ (i : ι), i ≠ j → w i = w' i
Tactic: have hww : ∀ i, i ≠ j → w i = w' i := by
        intro i hij
        simp [w', hij]
-- 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
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w)
h₁ : (insert j s).sum w' = 1
hww : ∀ (i : ι), i ≠ j → w i = w' i
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    (HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) ((s.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w : V) (p j))
have mpr : Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
  ((Finset.affineCombination k (insert j s) p : (a : ι → k) → P) w' : P)
Tactic: rw [s.weightedVSubOfPoint_eq_of_weights_eq p j w w' hww, ←
        s.weightedVSubOfPoint_insert w' p j, ←
        (insert j s).affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w' p h₁ (p j)]
-- 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
p : ι → P
j : ι
s : Finset ι
w : ι → k
mpr mpr₁ mpr₂ :
  Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    (HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) ((s.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w : V) (p j))
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    (HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) ((s.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w : V) (p j))
have mpr₃ : let w' := Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w);
∀ (h₁ : (insert j s).sum w' = 1),
  Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    (HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) ((s.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w : V) (p j))
Tactic: classical
      let w' : ι → k := Function.update w j (1 - (s \ {j}).sum w)
      have h₁ : (insert j s).sum w' = 1 := by
        by_cases hj : j ∈ s
        · simp [w', Finset.sum_update_of_mem hj, Finset.insert_eq_of_mem hj]
        · simp_rw [w', Finset.sum_insert hj, Finset.sum_update_of_notMem hj, Function.update_self,
            ← Finset.erase_eq, Finset.erase_eq_of_notMem hj, sub_add_cancel]
      have hww : ∀ i, i ≠ j → w i = w' i := by
        intro i hij
        simp [w', hij]
      rw [s.weightedVSubOfPoint_eq_of_weights_eq p j w w' hww, ←
        s.weightedVSubOfPoint_insert w' p j, ←
        (insert j s).affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w' p h₁ (p j)]
      exact affineCombination_mem_affineSpan h₁ p
-- 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
p : ι → P
j : ι
s : Finset ι
w : ι → k
mpr mpr₁ mpr₂ :
  Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    (HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) ((s.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w : V) (p j))
mpr₃ :
  let w' := Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w);
  ∀ (h₁ : (insert j s).sum w' = 1),
    Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      (HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) ((s.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w : V) (p j))
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    (HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) ((s.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w : V) (p j))
have mpr₄ : let w' := Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w);
∀ (h₁ : (insert j s).sum w' = 1) (hww : ∀ (i : ι), i ≠ j → w i = w' i),
  Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    (HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) ((s.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w : V) (p j))
Tactic: classical
      let w' : ι → k := Function.update w j (1 - (s \ {j}).sum w)
      have h₁ : (insert j s).sum w' = 1 := by
        by_cases hj : j ∈ s
        · simp [w', Finset.sum_update_of_mem hj, Finset.insert_eq_of_mem hj]
        · simp_rw [w', Finset.sum_insert hj, Finset.sum_update_of_notMem hj, Function.update_self,
            ← Finset.erase_eq, Finset.erase_eq_of_notMem hj, sub_add_cancel]
      have hww : ∀ i, i ≠ j → w i = w' i := by
        intro i hij
        simp [w', hij]
      rw [s.weightedVSubOfPoint_eq_of_weights_eq p j w w' hww, ←
        s.weightedVSubOfPoint_insert w' p j, ←
        (insert j s).affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w' p h₁ (p j)]
      exact affineCombination_mem_affineSpan h₁ p
-- 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
p : ι → P
j : ι
s : Finset ι
w : ι → k
mpr mpr₁ mpr₂ :
  Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    (HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) ((s.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w : V) (p j))
mpr₃ :
  let w' := Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w);
  ∀ (h₁ : (insert j s).sum w' = 1),
    Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      (HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) ((s.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w : V) (p j))
mpr₄ :
  let w' := Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w);
  ∀ (h₁ : (insert j s).sum w' = 1) (hww : ∀ (i : ι), i ≠ j → w i = w' i),
    Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      (HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) ((s.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w : V) (p j))
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    (HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) ((s.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w : V) (p j))
have mpr₅ : let w' := Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w);
∀ (h₁ : (insert j s).sum w' = 1) (hww : ∀ (i : ι), i ≠ j → w i = w' i),
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k (insert j s) p : (a : ι → k) → P) w' : P)
Tactic: classical
      let w' : ι → k := Function.update w j (1 - (s \ {j}).sum w)
      have h₁ : (insert j s).sum w' = 1 := by
        by_cases hj : j ∈ s
        · simp [w', Finset.sum_update_of_mem hj, Finset.insert_eq_of_mem hj]
        · simp_rw [w', Finset.sum_insert hj, Finset.sum_update_of_notMem hj, Function.update_self,
            ← Finset.erase_eq, Finset.erase_eq_of_notMem hj, sub_add_cancel]
      have hww : ∀ i, i ≠ j → w i = w' i := by
        intro i hij
        simp [w', hij]
      rw [s.weightedVSubOfPoint_eq_of_weights_eq p j w w' hww, ←
        s.weightedVSubOfPoint_insert w' p j, ←
        (insert j s).affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w' p h₁ (p j)]
      exact affineCombination_mem_affineSpan h₁ p
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (hypothesis)
Goal:
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 : Set P
p : P
hp : p ∈ s
w : (↑s : Type u_4) → kˣ
⊢ Eq (α := AffineSubspace k P)
    (affineSpan k (Set.range fun (q : (↑s : Type u_4)) ↦ (AffineMap.lineMap p (↑q : P) : (a : k) → P) (↑(w q) : k)))
    (affineSpan k s)
have this : s = Set.range (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s))
Tactic: have : s = Set.range ((↑) : s → P) := by simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
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 : Set P
p : P
hp : p ∈ s
w : (↑s : Type u_4) → kˣ
this : s = Set.range (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s))
| affineSpan k s
have rw : affineSpan k (Set.range (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s)))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
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 : Set P
p : P
hp : p ∈ s
w : (↑s : Type u_4) → kˣ
this : s = Set.range (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s))
⊢ Eq (α := AffineSubspace k P)
    (affineSpan k (Set.range fun (q : (↑s : Type u_4)) ↦ (AffineMap.lineMap p (↑q : P) : (a : k) → P) (↑(w q) : k)))
    (affineSpan k s)
have conv_rhs : Eq.{u_4 + 1} (α := AffineSubspace k P)
  (affineSpan k (Set.range fun (q : (↑s : Type u_4)) ↦ (AffineMap.lineMap p (↑q : P) : (a : k) → P) (↑(w q) : k)))
  (affineSpan k (Set.range (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s))))
Tactic: conv_rhs =>
    rw [this]