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 : 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
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
⊢ 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
-- 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
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

Tactic:
eq_affineCombination_of_mem_affineSpan

Premises used: eq_affineCombination_of_mem_affineSpan
-- 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
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

Tactic:
exact eq_affineCombination_of_mem_affineSpan

Premises used: eq_affineCombination_of_mem_affineSpan
-- 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
p : ι → P
s : Finset ι
w : ι → k
hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)

Tactic:
affineCombination_mem_affineSpan hw p

Premises used: affineCombination_mem_affineSpan
-- 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
p : ι → P
s : Finset ι
w : ι → k
hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)

Tactic:
exact affineCombination_mem_affineSpan hw p

Premises used: affineCombination_mem_affineSpan
-- 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
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)
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
⊢ 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
-- 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
p : ι → P
j : ι
q : P
hq : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) q
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)
⊢ ∃ (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:
obtain ⟨s, w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan hq

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
inst_4 : Nontrivial k
p : ι → P
j : ι
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:
⟨s, w, s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p hw (p j)⟩

Premises used: Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one, Exists.intro
-- 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
p : ι → P
j : ι
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:
exact ⟨s, w, s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p hw (p j)⟩
-- 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
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
neg : ∀ (hj : j ∉ s), (insert j s).sum w' = 1
⊢ (insert j s).sum w' = 1

Tactic:
by_cases hj : j ∈ s
-- 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
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update (β := fun (a : ι) ↦ k) w j (1 - (s \ {j}).sum w)
hj : j ∈ s
⊢ (insert j s).sum w' = 1

Tactic:
simp [w', Finset.sum_update_of_mem hj, Finset.insert_eq_of_mem hj]

Premises used: Finset.sum_update_of_mem, Finset.insert_eq_of_mem
-- 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
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
neg₅ : HSub.hSub (α := k) 1 (∑ x ∈ s, w x) + ∑ x ∈ s, w x = 1
⊢ (insert j s).sum w' = 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]

Premises used: Finset.erase_eq, Finset.sum_update_of_notMem, Finset.erase_eq_of_notMem, Function.update_self, Finset.sum_insert, sub_add_cancel
-- 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
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

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]
-- 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
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
i : ι
hij : i ≠ j
⊢ w i = w' i

Tactic:
simp [w', hij]
-- 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
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
⊢ ∀ (i : ι), i ≠ j → w i = w' i

Tactic:
have hww : ∀ i, i ≠ j → w i = w' i := by
        intro i hij
        simp [w', hij]
-- 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
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
mpr :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k (insert j s) p : (a : ι → k) → P) w' : P)
⊢ 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:
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)]

Premises used: Finset.weightedVSubOfPoint_insert, Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one, Insert.insert, Finset.weightedVSubOfPoint_eq_of_weights_eq
-- 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
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 (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k (insert j s) p : (a : ι → k) → P) w' : P)

Tactic:
affineCombination_mem_affineSpan h₁ p

Premises used: Set.Mem, affineCombination_mem_affineSpan
-- 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
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 (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k (insert j s) p : (a : ι → k) → P) w' : P)

Tactic:
exact affineCombination_mem_affineSpan h₁ p

Premises used: affineCombination_mem_affineSpan
-- 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
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))
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)
⊢ 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
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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ˣ
⊢ s = Set.range (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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ˣ
⊢ s = Set.range (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s))

Tactic:
have : s = Set.range ((↑) : s → P) := by simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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))
rw : affineSpan k (Set.range (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s)))
| affineSpan k s

Tactic:
rw [this]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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))
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))))
⊢ 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)

Tactic:
conv_rhs =>
    rw [this]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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))
a :
  LE.le.{u_4} (α := 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))))
a₁ :
  LE.le.{u_4} (α := AffineSubspace k P)
    (affineSpan k (Set.range (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s))))
    (affineSpan k (Set.range fun (q : (↑s : Type u_4)) ↦ (AffineMap.lineMap p (↑q : P) : (a : k) → P) (↑(w q) : k)))
⊢ 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:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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))
q : P
hq :
  Membership.mem (γ := AffineSubspace k P)
    (affineSpan k (Set.range fun (q : (↑s : Type u_4)) ↦ (AffineMap.lineMap p (↑q : P) : (a : k) → P) (↑(w q) : k))) q
a :
  ∀
    (hq :
      ∃ (s_1 : Finset { x : P // x ∈ s }) (w_1 : { x : P // x ∈ s } → k),
        q =
          HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) (β := P)
            ((s_1.weightedVSubOfPoint (P := P)
                    (fun (q : (↑s : Type u_4)) ↦ ((AffineMap.lineMap p (↑q : P) : (a : k) → P) (↑(w q) : k) : P))
                    ((AffineMap.lineMap p (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) : (a : k) → P)
                        (↑(w (Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp)) : k) :
                      P) :
                  (a : { x : P // x ∈ s } → k) → V)
                w_1 :
              V)
            ((AffineMap.lineMap p (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) : (a : k) → P)
                (↑(w (Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp)) : k) :
              P)),
    ∃ (s_1 : Finset { x : P // x ∈ s }) (w : { x : P // x ∈ s } → k),
      q =
        HVAdd.hVAdd.{u_3, u_4, u_4} (α := V)
          ((s_1.weightedVSubOfPoint (Subtype.val (p := fun (x : P) ↦ x ∈ s))
                  (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) :
                (a : { x : P // x ∈ s } → k) → V)
              w :
            V)
          (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P)
⊢ Membership.mem (γ := AffineSubspace k P)
    (affineSpan k (Set.range (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s)))) q

Tactic:
rw [mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd k V _ (⟨p, hp⟩ : s) q] at hq ⊢

Premises used: Subtype.mk, mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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))
q : P
hq :
  Membership.mem (γ := AffineSubspace k P)
    (affineSpan k (Set.range (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s)))) q
a :
  ∀
    (hq :
      ∃ (s_1 : Finset { x : P // x ∈ s }) (w : { x : P // x ∈ s } → k),
        q =
          HVAdd.hVAdd.{u_3, u_4, u_4} (α := V)
            ((s_1.weightedVSubOfPoint (Subtype.val (p := fun (x : P) ↦ x ∈ s))
                    (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) :
                  (a : { x : P // x ∈ s } → k) → V)
                w :
              V)
            (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P)),
    ∃ (s_1 : Finset { x : P // x ∈ s }) (w_1 : { x : P // x ∈ s } → k),
      q =
        HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) (β := P)
          ((s_1.weightedVSubOfPoint (P := P)
                  (fun (q : (↑s : Type u_4)) ↦ ((AffineMap.lineMap p (↑q : P) : (a : k) → P) (↑(w q) : k) : P))
                  ((AffineMap.lineMap p (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) : (a : k) → P)
                      (↑(w (Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp)) : k) :
                    P) :
                (a : { x : P // x ∈ s } → k) → V)
              w_1 :
            V)
          ((AffineMap.lineMap p (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) : (a : k) → P)
              (↑(w (Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp)) : k) :
            P)
⊢ Membership.mem (γ := AffineSubspace k P)
    (affineSpan k (Set.range fun (q : (↑s : Type u_4)) ↦ (AffineMap.lineMap p (↑q : P) : (a : k) → P) (↑(w q) : k))) q

Tactic:
rw [mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd k V _ (⟨p, hp⟩ : s) q] at hq ⊢

Premises used: Subtype.mk, mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd