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
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
ι : Type u_4
G : Type u_6
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G k V
s : Finset ι
w : ι → k
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
p : ι → V
a : G
rw :
  (s.weightedVSubOfPoint (a • p) (Classical.choice ⋯) : (a : ι → k) → V) w =
    HSMul.hSMul (β := V) a ((s.weightedVSub p : (a : ι → k) → V) w : V)
rw₁ :
  HSMul.hSMul (β := V) a
      ((s.weightedVSubOfPoint p (HSMul.hSMul (β := V) a⁻¹ (Classical.choice ⋯)) : (a : ι → k) → V) w : V) =
    HSMul.hSMul (β := V) a ((s.weightedVSub p : (a : ι → k) → V) w : V)
rw₂ :
  HSMul.hSMul (β := V) a
      ((s.weightedVSubOfPoint p (HSMul.hSMul (β := V) a⁻¹ (Classical.choice ⋯)) : (a : ι → k) → V) w : V) =
    HSMul.hSMul (β := V) a
      ((s.weightedVSubOfPoint p (HSMul.hSMul (β := V) a⁻¹ (Classical.choice ⋯)) : (a : ι → k) → V) w : V)
⊢ (s.weightedVSub (a • p) : (a : ι → k) → V) w = HSMul.hSMul (β := V) a ((s.weightedVSub p : (a : ι → k) → V) w : V)
have rw₃ : V
Tactic: rw [weightedVSub, weightedVSubOfPoint_smul,
    weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ _ _ 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
p₂ : P
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
⊢ Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w i • (p₁ i -ᵥ p₂) : V) ((s.weightedVSub p₁ : (a : ι → k) → V) w : V)
have rw : HSub.hSub (α := V) (β := V) ((s.weightedVSub p₁ : (a : ι → k) → V) w : V)
    ((weightedVSub.{u_1, u_2, u_3, u_4} (P := P) s fun (i : ι) ↦ p₂ : (a : ι → k) → V) w : V) =
  (s.weightedVSub p₁ : (a : ι → k) → V) w
Tactic: rw [sum_smul_vsub_eq_weightedVSub_sub, s.weightedVSub_apply_const _ _ h, sub_zero]
-- 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
p₂ : P
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
rw :
  HSub.hSub (α := V) (β := V) ((s.weightedVSub p₁ : (a : ι → k) → V) w : V)
      ((weightedVSub.{u_1, u_2, u_3, u_4} (P := P) s fun (i : ι) ↦ p₂ : (a : ι → k) → V) w : V) =
    (s.weightedVSub p₁ : (a : ι → k) → V) w
⊢ Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w i • (p₁ i -ᵥ p₂) : V) ((s.weightedVSub p₁ : (a : ι → k) → V) w : V)
have rw₁ : HSub.hSub (α := V) (β := V) ((s.weightedVSub p₁ : (a : ι → k) → V) w : V) (0 : V) =
  (s.weightedVSub p₁ : (a : ι → k) → V) w
Tactic: rw [sum_smul_vsub_eq_weightedVSub_sub, s.weightedVSub_apply_const _ _ h, sub_zero]
-- 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
p₂ : P
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
rw :
  HSub.hSub (α := V) (β := V) ((s.weightedVSub p₁ : (a : ι → k) → V) w : V)
      ((weightedVSub.{u_1, u_2, u_3, u_4} (P := P) s fun (i : ι) ↦ p₂ : (a : ι → k) → V) w : V) =
    (s.weightedVSub p₁ : (a : ι → k) → V) w
rw₁ :
  HSub.hSub (α := V) (β := V) ((s.weightedVSub p₁ : (a : ι → k) → V) w : V) (0 : V) =
    (s.weightedVSub p₁ : (a : ι → k) → V) w
⊢ Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w i • (p₁ i -ᵥ p₂) : V) ((s.weightedVSub p₁ : (a : ι → k) → V) w : V)
have rw₂ : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p₁ : (a : ι → k) → V) w : V) ((s.weightedVSub p₁ : (a : ι → k) → V) w : V)
Tactic: rw [sum_smul_vsub_eq_weightedVSub_sub, s.weightedVSub_apply_const _ _ h, sub_zero]
-- 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
p₁ : P
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
⊢ Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) : V) (-(s.weightedVSub p₂ : (a : ι → k) → V) w : V)
have rw : HSub.hSub (α := V) (β := V) ((weightedVSub.{u_1, u_2, u_3, u_4} (P := P) s fun (i : ι) ↦ p₁ : (a : ι → k) → V) w : V)
    ((s.weightedVSub p₂ : (a : ι → k) → V) w : V) =
  -(s.weightedVSub p₂ : (a : ι → k) → V) w
Tactic: rw [sum_smul_vsub_eq_weightedVSub_sub, s.weightedVSub_apply_const _ _ h, zero_sub]
-- 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
p₁ : P
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
rw :
  HSub.hSub (α := V) (β := V) ((weightedVSub.{u_1, u_2, u_3, u_4} (P := P) s fun (i : ι) ↦ p₁ : (a : ι → k) → V) w : V)
      ((s.weightedVSub p₂ : (a : ι → k) → V) w : V) =
    -(s.weightedVSub p₂ : (a : ι → k) → V) w
⊢ Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) : V) (-(s.weightedVSub p₂ : (a : ι → k) → V) w : V)
have rw₁ : HSub.hSub (α := V) (β := V) (0 : V) ((s.weightedVSub p₂ : (a : ι → k) → V) w : V) =
  -(s.weightedVSub p₂ : (a : ι → k) → V) w
Tactic: rw [sum_smul_vsub_eq_weightedVSub_sub, s.weightedVSub_apply_const _ _ h, zero_sub]
-- 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
p₁ : P
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
rw :
  HSub.hSub (α := V) (β := V) ((weightedVSub.{u_1, u_2, u_3, u_4} (P := P) s fun (i : ι) ↦ p₁ : (a : ι → k) → V) w : V)
      ((s.weightedVSub p₂ : (a : ι → k) → V) w : V) =
    -(s.weightedVSub p₂ : (a : ι → k) → V) w
rw₁ :
  HSub.hSub (α := V) (β := V) (0 : V) ((s.weightedVSub p₂ : (a : ι → k) → V) w : V) =
    -(s.weightedVSub p₂ : (a : ι → k) → V) w
⊢ Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) : V) (-(s.weightedVSub p₂ : (a : ι → k) → V) w : V)
have rw₂ : Eq.{u_2 + 1} (α := V) (-(s.weightedVSub p₂ : (a : ι → k) → V) w : V) (-(s.weightedVSub p₂ : (a : ι → k) → V) w : V)
Tactic: rw [sum_smul_vsub_eq_weightedVSub_sub, s.weightedVSub_apply_const _ _ h, zero_sub]
-- 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 ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
w₁ w₂ : ι → k
⊢ HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) (w₂ +ᵥ w₁) : V) (Classical.choice ⋯) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w₂ : V)
      (HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
        ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w₁ : V) (Classical.choice ⋯))
have simp_rw : HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
    ((s.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) (w₂ +ᵥ w₁) : V) (Classical.choice sorry) =
  HVAdd.hVAdd (β := P)
    (HAdd.hAdd (α := V) (β := V) ((s.weightedVSub p : (a : ι → k) → V) w₂ : V)
      ((s.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w₁ : V))
    (Classical.choice sorry)
Tactic: simp_rw [vadd_vadd, weightedVSub, vadd_eq_add, map_add]
-- 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 ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
w₁ w₂ : ι → k
simp_rw :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) (w₂ +ᵥ w₁) : V) (Classical.choice ⋯) =
    HVAdd.hVAdd (β := P)
      (HAdd.hAdd (α := V) (β := V) ((s.weightedVSub p : (a : ι → k) → V) w₂ : V)
        ((s.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₂ +ᵥ w₁) : V) (Classical.choice ⋯) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w₂ : V)
      (HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
        ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w₁ : V) (Classical.choice ⋯))
have simp_rw₁ : HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
    ((s.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) (w₂ +ᵥ w₁) : V) (Classical.choice sorry) =
  HVAdd.hVAdd (β := P)
    (HAdd.hAdd (α := V) (β := V) ((s.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w₂ : V)
      ((s.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w₁ : V))
    (Classical.choice sorry)
Tactic: simp_rw [vadd_vadd, weightedVSub, vadd_eq_add, map_add]
-- 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 ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
w₁ w₂ : ι → k
simp_rw :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) (w₂ +ᵥ w₁) : V) (Classical.choice ⋯) =
    HVAdd.hVAdd (β := P)
      (HAdd.hAdd (α := V) (β := V) ((s.weightedVSub p : (a : ι → k) → V) w₂ : V)
        ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w₁ : V))
      (Classical.choice ⋯)
simp_rw₁ :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) (w₂ +ᵥ w₁) : V) (Classical.choice ⋯) =
    HVAdd.hVAdd (β := P)
      (HAdd.hAdd (α := V) (β := V) ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w₂ : V)
        ((s.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₂ +ᵥ w₁) : V) (Classical.choice ⋯) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w₂ : V)
      (HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
        ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w₁ : V) (Classical.choice ⋯))
have simp_rw₂ : HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
    ((s.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) (w₂ + w₁) : V) (Classical.choice sorry) =
  HVAdd.hVAdd (β := P)
    (HAdd.hAdd (α := V) (β := V) ((s.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w₂ : V)
      ((s.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w₁ : V))
    (Classical.choice sorry)
Tactic: simp_rw [vadd_vadd, weightedVSub, vadd_eq_add, map_add]
-- 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
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
⊢ (affineCombination k s fun (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) s (fun (x : ι) ↦ p) (Classical.choice sorry) : (a : ι → k) → V) w :
      V)
    (Classical.choice sorry) =
  p
Tactic: rw [affineCombination_apply, s.weightedVSubOfPoint_apply_const, h, one_smul, vsub_vadd]
-- 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
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
rw :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((weightedVSubOfPoint.{u_1, u_2, u_3, u_4} (P := P) s (fun (x : ι) ↦ p) (Classical.choice ⋯) : (a : ι → k) → V)
          w :
        V)
      (Classical.choice ⋯) =
    p
⊢ (affineCombination k s fun (x : ι) ↦ p : (a : ι → k) → P) w = p
have rw₁ : HVAdd.hVAdd (β := P) (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p -ᵥ Classical.choice sorry))
    (Classical.choice sorry) =
  p
Tactic: rw [affineCombination_apply, s.weightedVSubOfPoint_apply_const, h, one_smul, vsub_vadd]
-- 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
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
rw :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((weightedVSubOfPoint.{u_1, u_2, u_3, u_4} (P := P) s (fun (x : ι) ↦ p) (Classical.choice ⋯) : (a : ι → k) → V)
          w :
        V)
      (Classical.choice ⋯) =
    p
rw₁ :
  HVAdd.hVAdd (β := P) (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p -ᵥ Classical.choice ⋯))
      (Classical.choice ⋯) =
    p
⊢ (affineCombination k s fun (x : ι) ↦ p : (a : ι → k) → P) w = p
have rw₂ : HVAdd.hVAdd (β := P) (HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (p -ᵥ Classical.choice sorry)) (Classical.choice sorry) = p
Tactic: rw [affineCombination_apply, s.weightedVSubOfPoint_apply_const, h, one_smul, vsub_vadd]
-- 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
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
rw :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((weightedVSubOfPoint.{u_1, u_2, u_3, u_4} (P := P) s (fun (x : ι) ↦ p) (Classical.choice ⋯) : (a : ι → k) → V)
          w :
        V)
      (Classical.choice ⋯) =
    p
rw₁ :
  HVAdd.hVAdd (β := P) (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p -ᵥ Classical.choice ⋯))
      (Classical.choice ⋯) =
    p
rw₂ : HVAdd.hVAdd (β := P) (HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (p -ᵥ Classical.choice ⋯)) (Classical.choice ⋯) = p
⊢ (affineCombination k s fun (x : ι) ↦ p : (a : ι → k) → P) w = p
have rw₃ : HVAdd.hVAdd (β := P) (p -ᵥ Classical.choice sorry) (Classical.choice sorry) = p
Tactic: rw [affineCombination_apply, s.weightedVSubOfPoint_apply_const, h, one_smul, vsub_vadd]
-- 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
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
rw :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((weightedVSubOfPoint.{u_1, u_2, u_3, u_4} (P := P) s (fun (x : ι) ↦ p) (Classical.choice ⋯) : (a : ι → k) → V)
          w :
        V)
      (Classical.choice ⋯) =
    p
rw₁ :
  HVAdd.hVAdd (β := P) (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p -ᵥ Classical.choice ⋯))
      (Classical.choice ⋯) =
    p
rw₂ : HVAdd.hVAdd (β := P) (HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (p -ᵥ Classical.choice ⋯)) (Classical.choice ⋯) = p
rw₃ : HVAdd.hVAdd (β := P) (p -ᵥ Classical.choice ⋯) (Classical.choice ⋯) = p
⊢ (affineCombination k s fun (x : ι) ↦ p : (a : ι → k) → P) w = p
have rw₄ : p = p
Tactic: rw [affineCombination_apply, s.weightedVSubOfPoint_apply_const, h, one_smul, vsub_vadd]
-- 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₁ w₂ : ι → k
hw : ∀ i ∈ s, w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ i ∈ s, p₁ i = p₂ i
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k s p₁ : (a : ι → k) → P) w₁ : P)
    ((affineCombination k s p₂ : (a : ι → k) → P) w₂ : P)
have simp_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: simp_rw [affineCombination_apply, s.weightedVSubOfPoint_congr hw hp]
-- 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₁ w₂ : ι → k
p : ι → P
⊢ HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P) ((s.weightedVSub p : (a : ι → k) → V) w₁ : V)
      ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
    (affineCombination k s p : (a : ι → k) → P) (w₁ + w₂)
have rw : HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P) ((s.weightedVSub p : (a : ι → k) → V) w₁ : V)
    ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
  (affineCombination k s p : (a : ι → k) → P) (w₁ +ᵥ w₂)
Tactic: rw [← vadd_eq_add, AffineMap.map_vadd, affineCombination_linear]
-- 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₁ w₂ : ι → k
p : ι → P
rw :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P) ((s.weightedVSub p : (a : ι → k) → V) w₁ : V)
      ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
    (affineCombination k s p : (a : ι → k) → P) (w₁ +ᵥ w₂)
⊢ HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P) ((s.weightedVSub p : (a : ι → k) → V) w₁ : V)
      ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
    (affineCombination k s p : (a : ι → k) → P) (w₁ + w₂)
have rw₁ : HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P) ((s.weightedVSub p : (a : ι → k) → V) w₁ : V)
    ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P) ((AffineMap.linear (affineCombination k s p) : (a : ι → k) → V) w₁ : V)
    ((affineCombination k s p : (a : ι → k) → P) w₂ : P)
Tactic: rw [← vadd_eq_add, AffineMap.map_vadd, affineCombination_linear]
-- 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₁ w₂ : ι → k
p : ι → P
rw :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P) ((s.weightedVSub p : (a : ι → k) → V) w₁ : V)
      ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
    (affineCombination k s p : (a : ι → k) → P) (w₁ +ᵥ w₂)
rw₁ :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P) ((s.weightedVSub p : (a : ι → k) → V) w₁ : V)
      ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((AffineMap.linear (affineCombination k s p) : (a : ι → k) → V) w₁ : V)
      ((affineCombination k s p : (a : ι → k) → P) w₂ : P)
⊢ HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P) ((s.weightedVSub p : (a : ι → k) → V) w₁ : V)
      ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
    (affineCombination k s p : (a : ι → k) → P) (w₁ + w₂)
have rw₂ : HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P) ((s.weightedVSub p : (a : ι → k) → V) w₁ : V)
    ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P) ((s.weightedVSub p : (a : ι → k) → V) w₁ : V)
    ((affineCombination k s p : (a : ι → k) → P) w₂ : P)
Tactic: rw [← vadd_eq_add, AffineMap.map_vadd, affineCombination_linear]
-- 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₁ w₂ : ι → k
p : ι → P
⊢ VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
      ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
    (s.weightedVSub p : (a : ι → k) → V) (w₁ - w₂)
have rw : Eq.{u_2 + 1} (α := V) ((AffineMap.linear (affineCombination k s p) : (a : ι → k) → V) (w₁ -ᵥ w₂) : V)
  ((s.weightedVSub p : (a : ι → k) → V) (w₁ - w₂) : V)
Tactic: rw [← AffineMap.linearMap_vsub, affineCombination_linear, vsub_eq_sub]
-- 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₁ w₂ : ι → k
p : ι → P
rw :
  Eq.{u_2 + 1} (α := V) ((AffineMap.linear (affineCombination k s p) : (a : ι → k) → V) (w₁ -ᵥ w₂) : V)
    ((s.weightedVSub p : (a : ι → k) → V) (w₁ - w₂) : V)
⊢ VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
      ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
    (s.weightedVSub p : (a : ι → k) → V) (w₁ - w₂)
have rw₁ : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) (w₁ -ᵥ w₂) : V)
  ((s.weightedVSub p : (a : ι → k) → V) (w₁ - w₂) : V)
Tactic: rw [← AffineMap.linearMap_vsub, affineCombination_linear, vsub_eq_sub]
-- 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₁ w₂ : ι → k
p : ι → P
rw :
  Eq.{u_2 + 1} (α := V) ((AffineMap.linear (affineCombination k s p) : (a : ι → k) → V) (w₁ -ᵥ w₂) : V)
    ((s.weightedVSub p : (a : ι → k) → V) (w₁ - w₂) : V)
rw₁ :
  Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) (w₁ -ᵥ w₂) : V)
    ((s.weightedVSub p : (a : ι → k) → V) (w₁ - w₂) : V)
⊢ VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
      ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
    (s.weightedVSub p : (a : ι → k) → V) (w₁ - w₂)
have rw₂ : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) (w₁ - w₂) : V)
  ((s.weightedVSub p : (a : ι → k) → V) (w₁ - w₂) : V)
Tactic: rw [← AffineMap.linearMap_vsub, affineCombination_linear, vsub_eq_sub]
-- 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
s : Finset P
w : P → k
⊢ Eq.{u_3 + 1} (α := P)
    ((affineCombination k s.attach (Subtype.val (p := fun (x : P) ↦ x ∈ s)) : (a : ↥s → k) → P)
        (w ∘ Subtype.val (p := fun (x : P) ↦ x ∈ s)) :
      P)
    ((affineCombination k s id : (a : P → k) → P) w : P)
have rw : Eq.{u_3 + 1} (α := P)
  ((affineCombination k (image (α := ↥s) (Subtype.val (p := fun (x : P) ↦ x ∈ s)) univ) id : (a : P → k) → P) w : P)
  ((affineCombination k s id : (a : P → k) → P) w : P)
Tactic: rw [attach_affineCombination_of_injective s w ((↑) : s → P) Subtype.coe_injective,
      univ_eq_attach, attach_image_val]
-- 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
s : Finset P
w : P → k
rw :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k (image (α := ↥s) (Subtype.val (p := fun (x : P) ↦ x ∈ s)) univ) id : (a : P → k) → P) w : P)
    ((affineCombination k s id : (a : P → k) → P) w : P)
⊢ Eq.{u_3 + 1} (α := P)
    ((affineCombination k s.attach (Subtype.val (p := fun (x : P) ↦ x ∈ s)) : (a : ↥s → k) → P)
        (w ∘ Subtype.val (p := fun (x : P) ↦ x ∈ s)) :
      P)
    ((affineCombination k s id : (a : P → k) → P) w : P)
have rw₁ : Eq.{u_3 + 1} (α := P)
  ((affineCombination k (image (Subtype.val (p := fun (x : P) ↦ x ∈ s)) s.attach) id : (a : P → k) → P) w : P)
  ((affineCombination k s id : (a : P → k) → P) w : P)
Tactic: rw [attach_affineCombination_of_injective s w ((↑) : s → P) Subtype.coe_injective,
      univ_eq_attach, attach_image_val]