awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  ∃ (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)
a :
  ∀ (t : Finset { x : P // x ∈ s }) (μ : { x : P // x ∈ s } → k),
    ∃ (s_1 : Finset { x : P // x ∈ s }) (w_1 : { x : P // x ∈ s } → k),
      HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) (β := P)
          ((t.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)
              μ :
            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) =
        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_1 :
            V)
          (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : 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)

Tactic:
obtain ⟨t, μ, rfl⟩ := hq

Premises used: rfl
-- 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 :
  ∃ (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)
a :
  ∀ (t : Finset { x : P // x ∈ s }) (μ : { x : P // x ∈ s } → k),
    ∃ (s_1 : Finset { x : P // x ∈ s }) (w_1 : { x : P // x ∈ s } → k),
      HVAdd.hVAdd.{u_3, u_4, u_4} (α := V)
          ((t.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)
              μ :
            V)
          (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) =
        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_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)

Tactic:
obtain ⟨t, μ, rfl⟩ := hq

Premises used: rfl
-- 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))
t : Finset { x : P // x ∈ s }
μ : { x : P // x ∈ s } → k
h :
  ∃ (w_1 : { x : P // x ∈ s } → k),
    HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) (β := P)
        ((t.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)
            μ :
          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) =
      HVAdd.hVAdd.{u_3, u_4, u_4} (α := V)
        ((t.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_1 :
          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),
    HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) (β := P)
        ((t.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)
            μ :
          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) =
      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_1 :
          V)
        (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P)

Tactic:
use t
-- 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))
t : Finset { x : P // x ∈ s }
μ : { x : P // x ∈ s } → k
h :
  ∃ (w_1 : { x : P // x ∈ s } → k),
    HVAdd.hVAdd.{u_3, u_4, u_4} (α := V)
        ((t.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)
            μ :
          V)
        (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) =
      HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) (β := P)
        ((t.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_1 : { x : P // x ∈ s } → k),
    HVAdd.hVAdd.{u_3, u_4, u_4} (α := V)
        ((t.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)
            μ :
          V)
        (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) =
      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)

Tactic:
use t
-- 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))
t : Finset { x : P // x ∈ s }
μ : { x : P // x ∈ s } → k
h :
  HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) (β := P)
      ((t.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)
          μ :
        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) =
    HVAdd.hVAdd.{u_3, u_4, u_4} (α := V)
      ((t.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)
          fun (x : { x : P // x ∈ s }) ↦ μ x * (↑(w x) : k) :
        V)
      (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P)
⊢ ∃ (w_1 : { x : P // x ∈ s } → k),
    HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) (β := P)
        ((t.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)
            μ :
          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) =
      HVAdd.hVAdd.{u_3, u_4, u_4} (α := V)
        ((t.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_1 :
          V)
        (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P)

Tactic:
use fun x => μ x * ↑(w x)

Premises used: HMul.hMul
-- 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))
t : Finset { x : P // x ∈ s }
μ : { x : P // x ∈ s } → k
h :
  HVAdd.hVAdd.{u_3, u_4, u_4} (α := V)
      ((t.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)
          μ :
        V)
      (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) =
    HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) (β := P)
      ((t.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)
          fun (x : { x : P // x ∈ s }) ↦ μ x * (↑(w x)⁻¹ : k) :
        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)
⊢ ∃ (w_1 : { x : P // x ∈ s } → k),
    HVAdd.hVAdd.{u_3, u_4, u_4} (α := V)
        ((t.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)
            μ :
          V)
        (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) =
      HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) (β := P)
        ((t.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)

Tactic:
use fun x => μ x * ↑(w x)⁻¹

Premises used: HMul.hMul
-- 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))
h :
  ∀ (t : Finset { x : P // x ∈ s }) (μ : { x : P // x ∈ s } → k),
    HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) (β := P)
        ((t.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)
            μ :
          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) =
      HVAdd.hVAdd.{u_3, u_4, u_4} (α := V)
        ((t.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)
            fun (x : { x : P // x ∈ s }) ↦ μ x * (↑(w x) : k) :
          V)
        (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P)
h₁ :
  ∀ (t : Finset { x : P // x ∈ s }) (μ : { x : P // x ∈ s } → k),
    HVAdd.hVAdd.{u_3, u_4, u_4} (α := V)
        ((t.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)
            μ :
          V)
        (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) =
      HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) (β := P)
        ((t.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)
            fun (x : { x : P // x ∈ s }) ↦ μ x * (↑(w x)⁻¹ : k) :
          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)
⊢ 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
    <;> intro q hq
    <;> rw [mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd k V _ (⟨p, hp⟩ : s) q] at hq ⊢
    <;> obtain ⟨t, μ, rfl⟩ := hq
    <;> use t
    <;> [use fun x => μ x * ↑(w x); use fun x => μ x * ↑(w x)⁻¹]

Premises used: le_antisymm, rfl
-- 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))
t : Finset { x : P // x ∈ s }
μ : { x : P // x ∈ s } → k
⊢ HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) (β := P)
      ((t.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)
          μ :
        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) =
    HVAdd.hVAdd.{u_3, u_4, u_4} (α := V)
      ((t.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)
          fun (x : { x : P // x ∈ s }) ↦ μ x * (↑(w x) : k) :
        V)
      (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P)

Tactic:
simp [smul_smul]

Premises used: smul_smul
-- 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))
t : Finset { x : P // x ∈ s }
μ : { x : P // x ∈ s } → k
⊢ HVAdd.hVAdd.{u_3, u_4, u_4} (α := V)
      ((t.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)
          μ :
        V)
      (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) =
    HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) (β := P)
      ((t.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)
          fun (x : { x : P // x ∈ s }) ↦ μ x * (↑(w x)⁻¹ : k) :
        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)

Tactic:
simp [smul_smul]

Premises used: smul_smul
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : CommRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
v : (i : ι) → V
b' : V
⊢ (s.weightedVSubOfPoint ((v, b') +ᵥ (p, b)).1 ((v, b') +ᵥ (p, b)).2 : (a : ι → k) → V) w =
    HVAdd.hVAdd (α := V) (β := V)
      ((∑ i ∈ s,
              w i •
                HSub.hSub (α := ((i : ι) → V) × V →ₗ[k] V) (β := ((i : ι) → V) × V →ₗ[k] V)
                  (LinearMap.proj (φ := fun (i : ι) ↦ V) i ∘ₗ LinearMap.fst k ((i : ι) → V) V)
                  (LinearMap.snd k ((i : ι) → V) V) :
            (a : ((i : ι) → V) × V) → V)
          (v, b') :
        V)
      ((s.weightedVSubOfPoint (p, b).1 (p, b).2 : (a : ι → k) → V) w : V)

Tactic:
simp [LinearMap.sum_apply, Finset.weightedVSubOfPoint, vsub_vadd_eq_vsub_sub,
     vadd_vsub_assoc, ← sub_add_eq_add_sub, smul_add, Finset.sum_add_distrib]

Premises used: vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, Finset.sum_add_distrib, Finset.weightedVSubOfPoint, LinearMap.sum_apply, sub_add_eq_add_sub, smul_add
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : s.Finite
⊢ FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)

Tactic:
.span_of_finite k <| h.vsub h

Premises used: vectorSpan, FiniteDimensional.span_of_finite, Set.Mem, Set.Finite.vsub, setOf
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p : P
⊢ FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (P := P) {p})

Tactic:
finiteDimensional_vectorSpan_of_finite _ (Set.finite_singleton p)

Premises used: finiteDimensional_vectorSpan_of_finite, Set.finite_singleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Finite ι
p : ι → P
⊢ FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (Set.range p))

Tactic:
finiteDimensional_vectorSpan_of_finite k (Set.finite_range _)

Premises used: finiteDimensional_vectorSpan_of_finite, Set.finite_range
-- Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Finite ι
p : ι → P
s : Set ι
⊢ FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (p '' s))

Tactic:
finiteDimensional_vectorSpan_of_finite k (Set.toFinite _)

Premises used: finiteDimensional_vectorSpan_of_finite, Set.toFinite