awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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)
simp : Eq.{u_2 + 1} (α := k) (∑ x : ι, if x ∈ s then w x else 0) (∑ i ∈ s, w i)
⊢ Eq.{u_2 + 1} (α := k) (∑ i : ι, (↑s : Set ι).indicator w i) 1

Tactic:
simp only [Finset.mem_coe, Set.indicator_apply, ← hw]

Premises used: Set.indicator_apply, Finset.mem_coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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)
rw rw₁ : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) (∑ i ∈ s, w i)
⊢ Eq.{u_2 + 1} (α := k) (∑ x : ι, if x ∈ s then w x else 0) (∑ i ∈ s, w i)

Tactic:
rw [Fintype.sum_extend_by_zero s w]

Premises used: Fintype.sum_extend_by_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
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)
⊢ ∃ (w : ι → k),
    Eq.{u_2 + 1} (α := k) (∑ i : ι, w i) 1 ∧ p1 = (Finset.affineCombination k Finset.univ p : (a : ι → k) → P) w

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]

Premises used: Set.indicator_apply, eq_affineCombination_of_mem_affineSpan, Finset.mem_coe, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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₁
⊢ 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

Premises used: Set.image_eq_range
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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₁
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)
⊢ ∃ (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:
obtain ⟨fs', w', hw', rfl⟩ := eq_affineCombination_of_mem_affineSpan h

Premises used: eq_affineCombination_of_mem_affineSpan, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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)
⊢ (↑(Finset.map (Function.Embedding.subtype fun (x : ι) ↦ x ∈ s) fs') : Set ι) ⊆ s

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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_2 + 1} (α := k)
    (∑ i ∈ Finset.map (Function.Embedding.subtype fun (x : ι) ↦ x ∈ s) fs',
      (fun (i : ι) ↦ (if hi : i ∈ s then w' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) else 0 : k)) i)
    1

Tactic:
simp [hw']
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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)
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)
⊢ ∃ (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:
refine ⟨fs'.map (Function.Embedding.subtype _), fun i ↦ if hi : i ∈ s then w' ⟨i, hi⟩ else 0,
    (by simp), (by simp [hw']), ?_⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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)
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)
⊢ 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:
simp only [Finset.affineCombination_map, Function.Embedding.coe_subtype]

Premises used: Function.Embedding.coe_subtype, Finset.affineCombination_map
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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)
⊢ ∀ i ∈ fs',
    w' i =
      ((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))
        i

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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)
⊢ ∀ i ∈ fs', p (↑i : ι) = (p ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) i

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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 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:
exact fs'.affineCombination_congr (by simp) (by simp)

Premises used: Finset.affineCombination_congr
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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 :
  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)

Tactic:
rw [Set.image_eq_range]

Premises used: Set.image_eq_range
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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 : ι)
⊢ {x ∈ s | x ∈ s'} ⊆ s

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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 : ι)
rw : Eq.{u_2 + 1} (α := k) (∑ x ∈ s \ {x ∈ s | x ∈ s'}, w x) 0
⊢ Eq.{u_2 + 1} (α := k) (∑ i ∈ s with i ∈ s', w i) 1

Tactic:
rw [← h, ← Finset.sum_sdiff (s₁ := {x ∈ s | x ∈ s'}) (s₂ := s) (by simp), right_eq_add]

Premises used: right_eq_add, Finset.sum_sdiff
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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

Tactic:
Finset.sum_eq_zero ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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 : ι)
refine : ∀ x ∈ s \ {x ∈ s | x ∈ s'}, w x = 0
⊢ Eq.{u_2 + 1} (α := k) (∑ x ∈ s \ {x ∈ s | x ∈ s'}, w x) 0

Tactic:
refine Finset.sum_eq_zero ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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'}
⊢ i ∈ s ∧ (i ∈ s → i ∉ s')

Tactic:
simp only [Finset.mem_sdiff, Finset.mem_filter, not_and] at hi

Premises used: Finset.mem_sdiff, Finset.mem_filter, not_and
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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 ∧ (i ∈ s → i ∉ s')
⊢ w i = 0

Tactic:
hs' i hi.1 (hi.2 hi.1)

Premises used: And.right, And.left
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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 ∧ (i ∈ s → i ∉ s')
⊢ w i = 0

Tactic:
exact hs' i hi.1 (hi.2 hi.1)

Premises used: And.right, And.left
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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

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)
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
⊢ 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'

Premises used: Finset.sum_subtype_eq_sum_filter
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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 : Subtype (Membership.mem s')) ↦ p (↑x : ι)))
    ((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:
affineCombination_mem_affineSpan h' (fun x ↦ p x)

Premises used: affineCombination_mem_affineSpan, Subtype.val
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
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)
⊢ 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:
convert! affineCombination_mem_affineSpan h' (fun x ↦ p x)

Premises used: affineCombination_mem_affineSpan, Subtype.val
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
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)
⊢ 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:
rw [Finset.affineCombination_subtype_eq_filter, Finset.affineCombination_indicator_subset w p
    (Finset.filter_subset _ _)]

Premises used: Finset.filter_subset, Finset.affineCombination_indicator_subset, Finset.affineCombination_subtype_eq_filter
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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)

Tactic:
Finset.affineCombination_congr _ (fun i hi ↦ ?_) (fun _ _ ↦ rfl)

Premises used: Finset.affineCombination_congr, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
h₁ : ∀ (i : ι) (hi : i ∈ s), w i = (↑({x ∈ s | x ∈ s'}) : Set ι).indicator w i
⊢ 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:
refine Finset.affineCombination_congr _ (fun i hi ↦ ?_) (fun _ _ ↦ rfl)

Premises used: Finset.affineCombination_congr, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
i : ι
hi : i ∈ s
⊢ w i = (↑({x ∈ s | x ∈ s'}) : Set ι).indicator w i

Tactic:
simp_all [Set.indicator_apply]

Premises used: Set.indicator_apply