awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i : ι
inst_3 : DecidablePred fun (x : ι) ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
rw : (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i = 0
rw₁ : (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i = (s.weightedVSub p : (a : ι → k) → V) w
rw₂ :
  (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i =
    VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k (s \ {i}) p : (a : ι → k) → P) w : P)
      ((affineCombination k {i} p : (a : ι → k) → P) (-w) : P)
rw₃ :
  (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i =
    VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k (s.erase i) p : (a : ι → k) → P) w : P)
      ((affineCombination k {i} p : (a : ι → k) → P) (-w) : P)
⊢ (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w = p i
have rw₄ : (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i =
  VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k ({a ∈ s | a ≠ i}) p : (a : ι → k) → P) w : P)
    ((affineCombination k {i} p : (a : ι → k) → P) (-w) : P)
Tactic: classical
    rw [← @vsub_eq_zero_iff_eq V, ← hw,
      ← s.affineCombination_sdiff_sub (singleton_subset_iff.2 his), sdiff_singleton_eq_erase,
      ← filter_ne']
    congr
    refine (affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_singleton_self _) ?_ ?_).symm
    · simp [hwi]
    · simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i : ι
inst_3 : DecidablePred fun (x : ι) ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
rw : (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i = 0
rw₁ : (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i = (s.weightedVSub p : (a : ι → k) → V) w
rw₂ :
  (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i =
    VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k (s \ {i}) p : (a : ι → k) → P) w : P)
      ((affineCombination k {i} p : (a : ι → k) → P) (-w) : P)
rw₃ :
  (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i =
    VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k (s.erase i) p : (a : ι → k) → P) w : P)
      ((affineCombination k {i} p : (a : ι → k) → P) (-w) : P)
rw₄ rw₅ rw₆ :
  (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i =
    VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k ({a ∈ s | a ≠ i}) p : (a : ι → k) → P) w : P)
      ((affineCombination k {i} p : (a : ι → k) → P) (-w) : P)
⊢ (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w = p i
have e_a : p i = (affineCombination k {i} p : (a : ι → k) → P) (-w)
Tactic: classical
    rw [← @vsub_eq_zero_iff_eq V, ← hw,
      ← s.affineCombination_sdiff_sub (singleton_subset_iff.2 his), sdiff_singleton_eq_erase,
      ← filter_ne']
    congr
    refine (affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_singleton_self _) ?_ ?_).symm
    · simp [hwi]
    · simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i : ι
inst_3 : DecidablePred fun (x : ι) ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
rw : (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i = 0
rw₁ : (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i = (s.weightedVSub p : (a : ι → k) → V) w
rw₂ :
  (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i =
    VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k (s \ {i}) p : (a : ι → k) → P) w : P)
      ((affineCombination k {i} p : (a : ι → k) → P) (-w) : P)
rw₃ :
  (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i =
    VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k (s.erase i) p : (a : ι → k) → P) w : P)
      ((affineCombination k {i} p : (a : ι → k) → P) (-w) : P)
rw₄ rw₅ rw₆ :
  (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i =
    VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k ({a ∈ s | a ≠ i}) p : (a : ι → k) → P) w : P)
      ((affineCombination k {i} p : (a : ι → k) → P) (-w) : P)
e_a : p i = (affineCombination k {i} p : (a : ι → k) → P) (-w)
⊢ (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w = p i
have e_a₁ : (-w) i = 1
Tactic: classical
    rw [← @vsub_eq_zero_iff_eq V, ← hw,
      ← s.affineCombination_sdiff_sub (singleton_subset_iff.2 his), sdiff_singleton_eq_erase,
      ← filter_ne']
    congr
    refine (affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_singleton_self _) ?_ ?_).symm
    · simp [hwi]
    · simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i : ι
inst_3 : DecidablePred fun (x : ι) ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
rw : (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i = 0
rw₁ : (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i = (s.weightedVSub p : (a : ι → k) → V) w
rw₂ :
  (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i =
    VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k (s \ {i}) p : (a : ι → k) → P) w : P)
      ((affineCombination k {i} p : (a : ι → k) → P) (-w) : P)
rw₃ :
  (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i =
    VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k (s.erase i) p : (a : ι → k) → P) w : P)
      ((affineCombination k {i} p : (a : ι → k) → P) (-w) : P)
rw₄ rw₅ rw₆ :
  (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i =
    VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k ({a ∈ s | a ≠ i}) p : (a : ι → k) → P) w : P)
      ((affineCombination k {i} p : (a : ι → k) → P) (-w) : P)
e_a : p i = (affineCombination k {i} p : (a : ι → k) → P) (-w)
e_a₁ : (-w) i = 1
⊢ (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w = p i
have e_a₂ : ∀ (i2 : ι), Membership.mem (γ := Finset ι) {i} i2 → i2 ≠ i → (-w) i2 = 0
Tactic: classical
    rw [← @vsub_eq_zero_iff_eq V, ← hw,
      ← s.affineCombination_sdiff_sub (singleton_subset_iff.2 his), sdiff_singleton_eq_erase,
      ← filter_ne']
    congr
    refine (affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_singleton_self _) ?_ ?_).symm
    · simp [hwi]
    · simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
pred : ι → Prop
inst_3 : DecidablePred pred
⊢ Eq.{u_3 + 1} (α := P)
    ((affineCombination k (Finset.subtype pred s) fun (i : Subtype pred) ↦ p (↑i : ι) : (a : Subtype pred → k) → P)
        fun (i : Subtype pred) ↦ w (↑i : ι) :
      P)
    ((affineCombination k ({x ∈ s | pred x}) p : (a : ι → k) → P) w : P)
have rw : HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
    ((weightedVSubOfPoint.{u_1, u_2, u_3, u_4} (P := P) (Finset.subtype pred s) (fun (i : Subtype pred) ↦ p (↑i : ι))
            (Classical.choice sorry) :
          (a : Subtype pred → k) → V)
        fun (i : Subtype pred) ↦ w (↑i : ι) :
      V)
    (Classical.choice sorry) =
  (affineCombination k ({x ∈ s | pred x}) p : (a : ι → k) → P) w
Tactic: rw [affineCombination_apply, affineCombination_apply, weightedVSubOfPoint_subtype_eq_filter]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
pred : ι → Prop
inst_3 : DecidablePred pred
rw :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((weightedVSubOfPoint.{u_1, u_2, u_3, u_4} (P := P) (Finset.subtype pred s) (fun (i : Subtype pred) ↦ p (↑i : ι))
              (Classical.choice ⋯) :
            (a : Subtype pred → k) → V)
          fun (i : Subtype pred) ↦ w (↑i : ι) :
        V)
      (Classical.choice ⋯) =
    (affineCombination k ({x ∈ s | pred x}) p : (a : ι → k) → P) w
⊢ Eq.{u_3 + 1} (α := P)
    ((affineCombination k (Finset.subtype pred s) fun (i : Subtype pred) ↦ p (↑i : ι) : (a : Subtype pred → k) → P)
        fun (i : Subtype pred) ↦ w (↑i : ι) :
      P)
    ((affineCombination k ({x ∈ s | pred x}) p : (a : ι → k) → P) w : P)
have rw₁ : HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
    ((weightedVSubOfPoint.{u_1, u_2, u_3, u_4} (P := P) (Finset.subtype pred s) (fun (i : Subtype pred) ↦ p (↑i : ι))
            (Classical.choice sorry) :
          (a : Subtype pred → k) → V)
        fun (i : Subtype pred) ↦ w (↑i : ι) :
      V)
    (Classical.choice sorry) =
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
    (({x ∈ s | pred x}.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w : V) (Classical.choice sorry)
Tactic: rw [affineCombination_apply, affineCombination_apply, weightedVSubOfPoint_subtype_eq_filter]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
pred : ι → Prop
inst_3 : DecidablePred pred
rw :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((weightedVSubOfPoint.{u_1, u_2, u_3, u_4} (P := P) (Finset.subtype pred s) (fun (i : Subtype pred) ↦ p (↑i : ι))
              (Classical.choice ⋯) :
            (a : Subtype pred → k) → V)
          fun (i : Subtype pred) ↦ w (↑i : ι) :
        V)
      (Classical.choice ⋯) =
    (affineCombination k ({x ∈ s | pred x}) p : (a : ι → k) → P) w
rw₁ :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((weightedVSubOfPoint.{u_1, u_2, u_3, u_4} (P := P) (Finset.subtype pred s) (fun (i : Subtype pred) ↦ p (↑i : ι))
              (Classical.choice ⋯) :
            (a : Subtype pred → k) → V)
          fun (i : Subtype pred) ↦ w (↑i : ι) :
        V)
      (Classical.choice ⋯) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      (({x ∈ s | pred x}.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w : V) (Classical.choice ⋯)
⊢ Eq.{u_3 + 1} (α := P)
    ((affineCombination k (Finset.subtype pred s) fun (i : Subtype pred) ↦ p (↑i : ι) : (a : Subtype pred → k) → P)
        fun (i : Subtype pred) ↦ w (↑i : ι) :
      P)
    ((affineCombination k ({x ∈ s | pred x}) p : (a : ι → k) → P) w : P)
have rw₂ : HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
    (({x ∈ s | pred x}.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w : V) (Classical.choice sorry) =
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
    (({x ∈ s | pred x}.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w : V) (Classical.choice sorry)
Tactic: rw [affineCombination_apply, affineCombination_apply, weightedVSubOfPoint_subtype_eq_filter]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
pred : ι → Prop
inst_3 : DecidablePred pred
h : ∀ i ∈ s, w i ≠ 0 → pred i
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k ({x ∈ s | pred x}) p : (a : ι → k) → P) w : P)
    ((affineCombination k s p : (a : ι → k) → P) w : P)
have rw : HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
    (({x ∈ s | pred x}.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w : V) (Classical.choice sorry) =
  (affineCombination k s p : (a : ι → k) → P) w
Tactic: rw [affineCombination_apply, affineCombination_apply,
    s.weightedVSubOfPoint_filter_of_ne _ _ _ h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
pred : ι → Prop
inst_3 : DecidablePred pred
h : ∀ i ∈ s, w i ≠ 0 → pred i
rw :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      (({x ∈ s | pred x}.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w : V) (Classical.choice ⋯) =
    (affineCombination k s p : (a : ι → k) → P) w
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k ({x ∈ s | pred x}) p : (a : ι → k) → P) w : P)
    ((affineCombination k s p : (a : ι → k) → P) w : P)
have rw₁ : HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
    (({x ∈ s | pred x}.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w : V) (Classical.choice sorry) =
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P) ((s.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w : V)
    (Classical.choice sorry)
Tactic: rw [affineCombination_apply, affineCombination_apply,
    s.weightedVSubOfPoint_filter_of_ne _ _ _ h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
pred : ι → Prop
inst_3 : DecidablePred pred
h : ∀ i ∈ s, w i ≠ 0 → pred i
rw :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      (({x ∈ s | pred x}.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w : V) (Classical.choice ⋯) =
    (affineCombination k s p : (a : ι → k) → P) w
rw₁ :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      (({x ∈ s | pred x}.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w : V) (Classical.choice ⋯) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w : V) (Classical.choice ⋯)
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k ({x ∈ s | pred x}) p : (a : ι → k) → P) w : P)
    ((affineCombination k s p : (a : ι → k) → P) w : P)
have rw₂ : HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P) ((s.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w : V)
    (Classical.choice sorry) =
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P) ((s.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w : V)
    (Classical.choice sorry)
Tactic: rw [affineCombination_apply, affineCombination_apply,
    s.weightedVSubOfPoint_filter_of_ne _ _ _ h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
v : V
x : k
s : Set ι
p : ι → P
b : P
⊢ (∃ (fs : Finset ι),
      (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = (fs.weightedVSubOfPoint p b : (a : ι → k) → V) w) ↔
    ∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k),
      ∑ i ∈ fs, w i = x ∧
        v = (fs.weightedVSubOfPoint (fun (i : (↑s : Type u_4)) ↦ p (↑i : ι)) b : (a : (↑s : Type u_4) → k) → V) w
have simp_rw : (∃ (fs : Finset ι), (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p i -ᵥ b)) ↔
  ∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b)
Tactic: simp_rw [weightedVSubOfPoint_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
v : V
x : k
s : Set ι
p : ι → P
b : P
⊢ (∃ (fs : Finset ι), (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p i -ᵥ b)) ↔
    ∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b)
have mp : (∃ (fs : Finset ι), (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p i -ᵥ b)) →
  ∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
v : V
x : k
s : Set ι
p : ι → P
b : P
mp :
  (∃ (fs : Finset ι), (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p i -ᵥ b)) →
    ∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b)
⊢ (∃ (fs : Finset ι), (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p i -ᵥ b)) ↔
    ∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b)
have mpr : (∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b)) →
  ∃ (fs : Finset ι), (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p i -ᵥ b)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Set ι
p : ι → P
b : P
fs : Finset (↑s : Type u_4)
w : (↑s : Type u_4) → k
⊢ ∃ (fs_1 : Finset ι),
    (↑fs_1 : Set ι) ⊆ s ∧
      ∃ (w_1 : ι → k),
        Eq.{u_1 + 1} (α := k) (∑ i ∈ fs_1, w_1 i) (∑ i ∈ fs, w i) ∧
          Eq.{u_2 + 1} (α := V) (∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b)) (∑ i ∈ fs_1, w_1 i • (p i -ᵥ b))
have mpr : Eq.{u_1 + 1} (α := k)
  (∑ i ∈ map (Function.Embedding.subtype fun (x : ι) ↦ x ∈ s) fs,
    (fun (i : ι) ↦ (if h : i ∈ s then w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else 0 : k)) i)
  (∑ i ∈ fs, w i)
Tactic: refine ⟨fs.map (Function.Embedding.subtype _), map_subtype_subset _, fun i =>
        if h : i ∈ s then w ⟨i, h⟩ else 0, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Set ι
p : ι → P
b : P
fs : Finset (↑s : Type u_4)
w : (↑s : Type u_4) → k
mpr :
  Eq.{u_1 + 1} (α := k)
    (∑ i ∈ map (Function.Embedding.subtype fun (x : ι) ↦ x ∈ s) fs,
      (fun (i : ι) ↦ (if h : i ∈ s then w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else 0 : k)) i)
    (∑ i ∈ fs, w i)
⊢ ∃ (fs_1 : Finset ι),
    (↑fs_1 : Set ι) ⊆ s ∧
      ∃ (w_1 : ι → k),
        Eq.{u_1 + 1} (α := k) (∑ i ∈ fs_1, w_1 i) (∑ i ∈ fs, w i) ∧
          Eq.{u_2 + 1} (α := V) (∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b)) (∑ i ∈ fs_1, w_1 i • (p i -ᵥ b))
have mpr₁ : Eq.{u_2 + 1} (α := V) (∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b))
  (∑ i ∈ map (Function.Embedding.subtype fun (x : ι) ↦ x ∈ s) fs,
    HSMul.hSMul.{u_1, u_2, u_2} (α := k)
      ((fun (i : ι) ↦ (if h : i ∈ s then w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else 0 : k)) i) (p i -ᵥ b))
Tactic: refine ⟨fs.map (Function.Embedding.subtype _), map_subtype_subset _, fun i =>
        if h : i ∈ s then w ⟨i, h⟩ else 0, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
v : V
x : k
s : Set ι
p : ι → P
b : P
⊢ (∃ (fs : Finset ι),
      (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = (fs.weightedVSubOfPoint p b : (a : ι → k) → V) w) ↔
    ∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k),
      ∑ i ∈ fs, w i = x ∧
        v = (fs.weightedVSubOfPoint (fun (i : (↑s : Type u_4)) ↦ p (↑i : ι)) b : (a : (↑s : Type u_4) → k) → V) w
have simp_rw : (∃ (fs : Finset ι), (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p i -ᵥ b)) ↔
  ∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b)
Tactic: classical
    simp_rw [weightedVSubOfPoint_apply]
    constructor
    · rintro ⟨fs, hfs, w, rfl, rfl⟩
      exact ⟨fs.subtype (· ∈ s), fun i => w i, sum_subtype_of_mem _ hfs,
        (sum_subtype_of_mem _ hfs).symm⟩
    · rintro ⟨fs, w, rfl, rfl⟩
      refine ⟨fs.map (Function.Embedding.subtype _), map_subtype_subset _, fun i =>
        if h : i ∈ s then w ⟨i, h⟩ else 0, ?_, ?_⟩ <;> simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
v : V
x : k
s : Set ι
p : ι → P
b : P
simp_rw :
  (∃ (fs : Finset ι), (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p i -ᵥ b)) ↔
    ∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b)
⊢ (∃ (fs : Finset ι),
      (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = (fs.weightedVSubOfPoint p b : (a : ι → k) → V) w) ↔
    ∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k),
      ∑ i ∈ fs, w i = x ∧
        v = (fs.weightedVSubOfPoint (fun (i : (↑s : Type u_4)) ↦ p (↑i : ι)) b : (a : (↑s : Type u_4) → k) → V) w
have mp : (∃ (fs : Finset ι), (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p i -ᵥ b)) →
  ∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b)
Tactic: classical
    simp_rw [weightedVSubOfPoint_apply]
    constructor
    · rintro ⟨fs, hfs, w, rfl, rfl⟩
      exact ⟨fs.subtype (· ∈ s), fun i => w i, sum_subtype_of_mem _ hfs,
        (sum_subtype_of_mem _ hfs).symm⟩
    · rintro ⟨fs, w, rfl, rfl⟩
      refine ⟨fs.map (Function.Embedding.subtype _), map_subtype_subset _, fun i =>
        if h : i ∈ s then w ⟨i, h⟩ else 0, ?_, ?_⟩ <;> simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
v : V
x : k
s : Set ι
p : ι → P
b : P
simp_rw :
  (∃ (fs : Finset ι), (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p i -ᵥ b)) ↔
    ∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b)
mp :
  (∃ (fs : Finset ι), (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p i -ᵥ b)) →
    ∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b)
⊢ (∃ (fs : Finset ι),
      (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = (fs.weightedVSubOfPoint p b : (a : ι → k) → V) w) ↔
    ∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k),
      ∑ i ∈ fs, w i = x ∧
        v = (fs.weightedVSubOfPoint (fun (i : (↑s : Type u_4)) ↦ p (↑i : ι)) b : (a : (↑s : Type u_4) → k) → V) w
have mpr : (∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b)) →
  ∃ (fs : Finset ι), (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p i -ᵥ b)
Tactic: classical
    simp_rw [weightedVSubOfPoint_apply]
    constructor
    · rintro ⟨fs, hfs, w, rfl, rfl⟩
      exact ⟨fs.subtype (· ∈ s), fun i => w i, sum_subtype_of_mem _ hfs,
        (sum_subtype_of_mem _ hfs).symm⟩
    · rintro ⟨fs, w, rfl, rfl⟩
      refine ⟨fs.map (Function.Embedding.subtype _), map_subtype_subset _, fun i =>
        if h : i ∈ s then w ⟨i, h⟩ else 0, ?_, ?_⟩ <;> simp