awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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))
⊢ 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))))
have 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))))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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))))
⊢ 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))))
have 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)))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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
⊢ Membership.mem (γ := AffineSubspace k P)
    (affineSpan k (Set.range (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s)))) q
have 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)
Tactic: rw [mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd k V _ (⟨p, hp⟩ : s) q] at hq ⊢
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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
⊢ 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
have 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)
Tactic: rw [mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd k V _ (⟨p, hp⟩ : s) q] at hq ⊢
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨t, μ, rfl⟩ := hq
Cleared hypotheses: q, hq
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨t, μ, rfl⟩ := hq
Cleared hypotheses: q, hq
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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
⊢ ∃ (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)
have 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)
Tactic: use t
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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
⊢ ∃ (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)
have 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)
Tactic: use t
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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
⊢ ∃ (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)
have 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)
Tactic: use fun x => μ x * ↑(w x)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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
⊢ ∃ (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)
have 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)
Tactic: use fun x => μ x * ↑(w x)⁻¹
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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))
⊢ 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))))
have 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)
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)⁻¹]