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
p : ι → P
hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i1 1
hw1 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w1 i) 1
hw1s : (Finset.affineCombination k s p : (a : ι → k) → P) w1 = p i1
⊢ Membership.mem (α := V) (γ := Submodule k V) (vectorSpan k (Set.range p))
    ((s.weightedVSub p : (a : ι → k) → V) (w - w1) : V)
have h₁ : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, (w - w1) i) 0
Tactic: apply weightedVSub_mem_vectorSpan
-- 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
p : ι → P
hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i1 1
hw1 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w1 i) 1
hw1s : (Finset.affineCombination k s p : (a : ι → k) → P) w1 = p i1
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have hv : Membership.mem (γ := Submodule k V) (AffineSubspace.direction (affineSpan k (Set.range p)))
  ((Finset.affineCombination k s p : (a : ι → k) → P) w -ᵥ p i1)
Tactic: have hv : s.affineCombination k p w -ᵥ p i1 ∈ (affineSpan k (Set.range p)).direction := by
      rw [direction_affineSpan, ← hw1s, Finset.affineCombination_vsub]
      apply weightedVSub_mem_vectorSpan
      simp [Pi.sub_apply, h, hw1]
-- 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
p : ι → P
hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i1 1
hw1 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w1 i) 1
hw1s : (Finset.affineCombination k s p : (a : ι → k) → P) w1 = p i1
hv :
  Membership.mem (γ := Submodule k V) (AffineSubspace.direction (affineSpan k (Set.range p)))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w -ᵥ p i1)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have rw : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p))
  (((Finset.affineCombination k s p : (a : ι → k) → P) w -ᵥ p i1) +ᵥ p i1)
Tactic: rw [← vsub_vadd (s.affineCombination k p w) (p i1)]
-- 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
p : ι → P
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have have : ∀ (hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0),
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
Tactic: classical
    have hnz : ∑ i ∈ s, w i ≠ 0 := h.symm ▸ one_ne_zero
    have hn : s.Nonempty := Finset.nonempty_of_sum_ne_zero hnz
    obtain ⟨i1, hi1⟩ := hn
    let w1 : ι → k := Function.update (Function.const ι 0) i1 1
    have hw1 : ∑ i ∈ s, w1 i = 1 := by
      simp only [w1, Function.const_zero, Finset.sum_update_of_mem hi1, Pi.zero_apply,
          Finset.sum_const_zero, add_zero]
    have hw1s : s.affineCombination k p w1 = p i1 :=
      s.affineCombination_of_eq_one_of_eq_zero w1 p hi1 (Function.update_self ..) fun _ _ hne =>
        Function.update_of_ne hne ..
    have hv : s.affineCombination k p w -ᵥ p i1 ∈ (affineSpan k (Set.range p)).direction := by
      rw [direction_affineSpan, ← hw1s, Finset.affineCombination_vsub]
      apply weightedVSub_mem_vectorSpan
      simp [Pi.sub_apply, h, hw1]
    rw [← vsub_vadd (s.affineCombination k p w) (p i1)]
    exact AffineSubspace.vadd_mem_of_mem_direction hv (mem_affineSpan k (Set.mem_range_self _))
-- 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
p : ι → P
have have₁ have₂ :
  ∀ (hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0),
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have have₃ : ∀ (hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0) (hn : s.Nonempty),
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
Tactic: classical
    have hnz : ∑ i ∈ s, w i ≠ 0 := h.symm ▸ one_ne_zero
    have hn : s.Nonempty := Finset.nonempty_of_sum_ne_zero hnz
    obtain ⟨i1, hi1⟩ := hn
    let w1 : ι → k := Function.update (Function.const ι 0) i1 1
    have hw1 : ∑ i ∈ s, w1 i = 1 := by
      simp only [w1, Function.const_zero, Finset.sum_update_of_mem hi1, Pi.zero_apply,
          Finset.sum_const_zero, add_zero]
    have hw1s : s.affineCombination k p w1 = p i1 :=
      s.affineCombination_of_eq_one_of_eq_zero w1 p hi1 (Function.update_self ..) fun _ _ hne =>
        Function.update_of_ne hne ..
    have hv : s.affineCombination k p w -ᵥ p i1 ∈ (affineSpan k (Set.range p)).direction := by
      rw [direction_affineSpan, ← hw1s, Finset.affineCombination_vsub]
      apply weightedVSub_mem_vectorSpan
      simp [Pi.sub_apply, h, hw1]
    rw [← vsub_vadd (s.affineCombination k p w) (p i1)]
    exact AffineSubspace.vadd_mem_of_mem_direction hv (mem_affineSpan k (Set.mem_range_self _))
-- 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
p : ι → P
have have₁ have₂ :
  ∀ (hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0),
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have₃ :
  ∀ (hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0) (hn : s.Nonempty),
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have have₄ : ∀ (hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0) (i1 : ι) (hi1 : i1 ∈ s),
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
Tactic: classical
    have hnz : ∑ i ∈ s, w i ≠ 0 := h.symm ▸ one_ne_zero
    have hn : s.Nonempty := Finset.nonempty_of_sum_ne_zero hnz
    obtain ⟨i1, hi1⟩ := hn
    let w1 : ι → k := Function.update (Function.const ι 0) i1 1
    have hw1 : ∑ i ∈ s, w1 i = 1 := by
      simp only [w1, Function.const_zero, Finset.sum_update_of_mem hi1, Pi.zero_apply,
          Finset.sum_const_zero, add_zero]
    have hw1s : s.affineCombination k p w1 = p i1 :=
      s.affineCombination_of_eq_one_of_eq_zero w1 p hi1 (Function.update_self ..) fun _ _ hne =>
        Function.update_of_ne hne ..
    have hv : s.affineCombination k p w -ᵥ p i1 ∈ (affineSpan k (Set.range p)).direction := by
      rw [direction_affineSpan, ← hw1s, Finset.affineCombination_vsub]
      apply weightedVSub_mem_vectorSpan
      simp [Pi.sub_apply, h, hw1]
    rw [← vsub_vadd (s.affineCombination k p w) (p i1)]
    exact AffineSubspace.vadd_mem_of_mem_direction hv (mem_affineSpan k (Set.mem_range_self _))
-- 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
p : ι → P
have have₁ have₂ :
  ∀ (hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0),
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have₃ :
  ∀ (hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0) (hn : s.Nonempty),
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have₄ have₅ :
  ∀ (hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0) (i1 : ι) (hi1 : i1 ∈ s),
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have have₆ : ∀ (hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0) (i1 : ι) (hi1 : i1 ∈ s),
  let w1 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i1 1;
  ∀ (hw1 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w1 i) 1),
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
Tactic: classical
    have hnz : ∑ i ∈ s, w i ≠ 0 := h.symm ▸ one_ne_zero
    have hn : s.Nonempty := Finset.nonempty_of_sum_ne_zero hnz
    obtain ⟨i1, hi1⟩ := hn
    let w1 : ι → k := Function.update (Function.const ι 0) i1 1
    have hw1 : ∑ i ∈ s, w1 i = 1 := by
      simp only [w1, Function.const_zero, Finset.sum_update_of_mem hi1, Pi.zero_apply,
          Finset.sum_const_zero, add_zero]
    have hw1s : s.affineCombination k p w1 = p i1 :=
      s.affineCombination_of_eq_one_of_eq_zero w1 p hi1 (Function.update_self ..) fun _ _ hne =>
        Function.update_of_ne hne ..
    have hv : s.affineCombination k p w -ᵥ p i1 ∈ (affineSpan k (Set.range p)).direction := by
      rw [direction_affineSpan, ← hw1s, Finset.affineCombination_vsub]
      apply weightedVSub_mem_vectorSpan
      simp [Pi.sub_apply, h, hw1]
    rw [← vsub_vadd (s.affineCombination k p w) (p i1)]
    exact AffineSubspace.vadd_mem_of_mem_direction hv (mem_affineSpan k (Set.mem_range_self _))
-- 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
p : ι → P
have have₁ have₂ :
  ∀ (hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0),
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have₃ :
  ∀ (hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0) (hn : s.Nonempty),
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have₄ have₅ :
  ∀ (hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0) (i1 : ι) (hi1 : i1 ∈ s),
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have₆ :
  ∀ (hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0) (i1 : ι) (hi1 : i1 ∈ s),
    let w1 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i1 1;
    ∀ (hw1 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w1 i) 1),
      Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
        ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have have₇ : ∀ (hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0) (i1 : ι) (hi1 : i1 ∈ s),
  let w1 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i1 1;
  ∀ (hw1 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w1 i) 1)
    (hw1s : (Finset.affineCombination k s p : (a : ι → k) → P) w1 = p i1),
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
Tactic: classical
    have hnz : ∑ i ∈ s, w i ≠ 0 := h.symm ▸ one_ne_zero
    have hn : s.Nonempty := Finset.nonempty_of_sum_ne_zero hnz
    obtain ⟨i1, hi1⟩ := hn
    let w1 : ι → k := Function.update (Function.const ι 0) i1 1
    have hw1 : ∑ i ∈ s, w1 i = 1 := by
      simp only [w1, Function.const_zero, Finset.sum_update_of_mem hi1, Pi.zero_apply,
          Finset.sum_const_zero, add_zero]
    have hw1s : s.affineCombination k p w1 = p i1 :=
      s.affineCombination_of_eq_one_of_eq_zero w1 p hi1 (Function.update_self ..) fun _ _ hne =>
        Function.update_of_ne hne ..
    have hv : s.affineCombination k p w -ᵥ p i1 ∈ (affineSpan k (Set.range p)).direction := by
      rw [direction_affineSpan, ← hw1s, Finset.affineCombination_vsub]
      apply weightedVSub_mem_vectorSpan
      simp [Pi.sub_apply, h, hw1]
    rw [← vsub_vadd (s.affineCombination k p w) (p i1)]
    exact AffineSubspace.vadd_mem_of_mem_direction hv (mem_affineSpan k (Set.mem_range_self _))
-- 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 : Nonempty ι
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
p : ι → P
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have inl : ∀ (hs : Subsingleton k),
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
Tactic: rcases subsingleton_or_nontrivial k with hs | hn
-- 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 : Nonempty ι
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
p : ι → P
inl :
  ∀ (hs : Subsingleton k),
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have inr : ∀ (hn : Nontrivial k),
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
Tactic: rcases subsingleton_or_nontrivial k with hs | hn
-- 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 : Nonempty ι
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
p : ι → P
hs : Subsingleton k
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have hnv : Subsingleton V
Tactic: have hnv := Module.subsingleton k V
-- 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 : Nonempty ι
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
p : ι → P
hs : Subsingleton k
hnv : Subsingleton V
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have hnv₁ : Subsingleton P
Tactic: rw [AddTorsor.subsingleton_iff V P] at hnv
Cleared hypotheses: hnv
-- 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 : Nonempty ι
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
p : ι → P
hs : Subsingleton k
hnv : Subsingleton P
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have inl : Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P) ⊤
  ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
Tactic: rw [(affineSpan_eq_top_iff_nonempty_of_subsingleton k).2 (Set.range_nonempty 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
v : V
p : ι → P
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (Set.range p)) v ↔
    ∃ (s : Finset ι) (w : ι → k), Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0 ∧ v = (s.weightedVSub p : (a : ι → k) → V) w
have mp : Membership.mem (γ := Submodule k V) (vectorSpan k (Set.range p)) v →
  ∃ (s : Finset ι) (w : ι → k), Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0 ∧ v = (s.weightedVSub p : (a : ι → k) → V) 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
v : V
p : ι → P
mp :
  Membership.mem (γ := Submodule k V) (vectorSpan k (Set.range p)) v →
    ∃ (s : Finset ι) (w : ι → k), Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0 ∧ v = (s.weightedVSub p : (a : ι → k) → V) w
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (Set.range p)) v ↔
    ∃ (s : Finset ι) (w : ι → k), Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0 ∧ v = (s.weightedVSub p : (a : ι → k) → V) w
have mpr : (∃ (s : Finset ι) (w : ι → k), Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0 ∧ v = (s.weightedVSub p : (a : ι → k) → V) w) →
  Membership.mem (γ := Submodule k V) (vectorSpan k (Set.range p)) v
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
v : V
p : ι → P
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (Set.range p)) v →
    ∃ (s : Finset ι) (w : ι → k), Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0 ∧ v = (s.weightedVSub p : (a : ι → k) → V) w
have mp : ∀ (hι : IsEmpty ι),
  Membership.mem (γ := Submodule k V) (vectorSpan k (Set.range p)) v →
    ∃ (s : Finset ι) (w : ι → k), Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0 ∧ v = (s.weightedVSub p : (a : ι → k) → V) w
Tactic: rcases isEmpty_or_nonempty ι with (hι | ⟨⟨i0⟩⟩)
-- 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
v : V
p : ι → P
mp :
  ∀ (hι : IsEmpty ι),
    Membership.mem (γ := Submodule k V) (vectorSpan k (Set.range p)) v →
      ∃ (s : Finset ι) (w : ι → k), Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0 ∧ v = (s.weightedVSub p : (a : ι → k) → V) w
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (Set.range p)) v →
    ∃ (s : Finset ι) (w : ι → k), Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0 ∧ v = (s.weightedVSub p : (a : ι → k) → V) w
have mp₁ : ∀ (i0 : ι),
  Membership.mem (γ := Submodule k V) (vectorSpan k (Set.range p)) v →
    ∃ (s : Finset ι) (w : ι → k), Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0 ∧ v = (s.weightedVSub p : (a : ι → k) → V) w
Tactic: rcases isEmpty_or_nonempty ι with (hι | ⟨⟨i0⟩⟩)
-- 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
v : V
p : ι → P
i0 : ι
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (Set.range p)) v →
    ∃ (s : Finset ι) (w : ι → k), Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0 ∧ v = (s.weightedVSub p : (a : ι → k) → V) w
have mp : (∃ (l : ι →₀ k),
    Membership.mem (γ := Submodule k (ι →₀ k)) (Finsupp.supported k k Set.univ) l ∧
      (Finsupp.linearCombination k fun (i : ι) ↦ p i -ᵥ p i0 : (a : ι →₀ k) → V) l = v) →
  ∃ (s : Finset ι) (w : ι → k), Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0 ∧ v = (s.weightedVSub p : (a : ι → k) → V) w
Tactic: rw [vectorSpan_range_eq_span_range_vsub_right k p i0, ← Set.image_univ,
          Finsupp.mem_span_image_iff_linearCombination]
-- 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
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left : Membership.mem (γ := Submodule k (ι →₀ k)) (Finsupp.supported k k Set.univ) l
hv : (Finsupp.linearCombination k fun (i : ι) ↦ p i -ᵥ p i0 : (a : ι →₀ k) → V) l = v
⊢ ∃ (s : Finset ι) (w : ι → k), Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0 ∧ v = (s.weightedVSub p : (a : ι → k) → V) w
have h : ∃ (w : ι → k),
  Eq.{u_2 + 1} (α := k) (∑ i ∈ insert i0 l.support, w i) 0 ∧
    v = ((insert i0 l.support).weightedVSub p : (a : ι → k) → V) w
Tactic: use insert i0 l.support
-- 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
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left : Membership.mem (γ := Submodule k (ι →₀ k)) (Finsupp.supported k k Set.univ) l
hv : (Finsupp.linearCombination k fun (i : ι) ↦ p i -ᵥ p i0 : (a : ι →₀ k) → V) l = v
⊢ ∃ (w : ι → k),
    Eq.{u_2 + 1} (α := k) (∑ i ∈ insert i0 l.support, w i) 0 ∧
      v = ((insert i0 l.support).weightedVSub p : (a : ι → k) → V) w
have hwdef : let w :=
  HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
    (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i));
w =
  HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
    (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
Tactic: set w :=
          (l : ι → k) - Function.update (Function.const ι 0 : ι → k) i0 (∑ i ∈ l.support, l i) with
          hwdef
-- 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
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left : Membership.mem (γ := Submodule k (ι →₀ k)) (Finsupp.supported k k Set.univ) l
hv : (Finsupp.linearCombination k fun (i : ι) ↦ p i -ᵥ p i0 : (a : ι →₀ k) → V) l = v
w : (a : ι) → k :=
  HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
    (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
hwdef :
  w =
    HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
      (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
⊢ ∃ (w : ι → k),
    Eq.{u_2 + 1} (α := k) (∑ i ∈ insert i0 l.support, w i) 0 ∧
      v = ((insert i0 l.support).weightedVSub p : (a : ι → k) → V) w
have h : Eq.{u_2 + 1} (α := k) (∑ i ∈ insert i0 l.support, w i) 0 ∧
  v = ((insert i0 l.support).weightedVSub p : (a : ι → k) → V) w
Tactic: use w