awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
k : ℕ
hk : k < #s
simp_rw :
  Eq.{u_1 + 1} (α := F[X])
    (∑ x ∈ s,
      HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r x / ∏ j ∈ s.erase x, (v x - v j)) : F[X])
        ((⇑derivative : (a : F[X]) → F[X])^[k]
            (∏ j ∈ s.erase x, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X])) :
          F[X]))
    (∑ x ∈ s,
      HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (r x / ∏ j ∈ s.erase x, (v x - v j)) : F[X])
        (HMul.hMul (α := F[X]) (↑k.factorial : F[X])
          (∑ t ∈ powersetCard (#s - (k + 1)) (s.erase x),
            ∏ j ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X]))))
⊢ (⇑derivative : (a : F[X]) → F[X])^[k] ((interpolate s v : (a : ι → F) → F[X]) r) =
    HMul.hMul (α := F[X]) (↑k.factorial : F[X])
      (∑ i ∈ s,
        HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r i / ∏ j ∈ s.erase i, (v i - v j)) : F[X])
          (∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i),
              ∏ a ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v a) : F[X]) :
            F[X]))

Tactic:
simp_rw [interpolate_eq_sum, iterate_derivative_sum, iterate_derivative_C_mul, mul_sum s,
    ← mul_assoc, mul_comm (k.factorial : F[X]), mul_assoc]

Premises used: Finset.mul_sum, Lagrange.interpolate_eq_sum, mul_assoc, Nat.cast, Nat.factorial, Polynomial.iterate_derivative_C_mul, mul_comm, Polynomial.iterate_derivative_sum
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
k : ℕ
hk : k < #s
a :
  ∀ (i : ι) (hi : i ∈ s),
    (⇑derivative : (a : F[X]) → F[X])^[k]
        (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X])) =
      HMul.hMul (α := F[X]) (↑k.factorial : F[X])
        (∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i),
          ∏ j ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X]))
⊢ Eq.{u_1 + 1} (α := F[X])
    (∑ x ∈ s,
      HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r x / ∏ j ∈ s.erase x, (v x - v j)) : F[X])
        ((⇑derivative : (a : F[X]) → F[X])^[k]
            (∏ j ∈ s.erase x, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X])) :
          F[X]))
    (∑ x ∈ s,
      HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (r x / ∏ j ∈ s.erase x, (v x - v j)) : F[X])
        (HMul.hMul (α := F[X]) (↑k.factorial : F[X])
          (∑ t ∈ powersetCard (#s - (k + 1)) (s.erase x),
            ∏ j ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X]))))

Tactic:
congr! 2 with i hi
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
⊢ Set.InjOn v (↑(s.erase i) : Set ι)

Tactic:
have hvs' := hvs.mono (coe_subset.mpr (erase_subset i s))
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
hvs' : Set.InjOn v (↑(s.erase i) : Set ι)
rw rw₁ :
  Eq.{u_1 + 1} (α := F[X])
    ((⇑derivative : (a : F[X]) → F[X])^[k]
      (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X])))
    ((⇑derivative : (a : F[X]) → F[X])^[k]
      (∏ x ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v x) : F[X])))
⊢ Eq (α := F[X])
    ((⇑derivative : (a : F[X]) → F[X])^[k]
      (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X])))
    ((⇑derivative : (a : F[X]) → F[X])^[k]
      (∏ vj ∈ image v (s.erase i), HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) vj : F[X])))

Tactic:
rw [Finset.prod_image hvs']

Premises used: Finset.prod_image
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
hvs' : Set.InjOn v (↑(s.erase i) : Set ι)
⊢ (⇑derivative : (a : F[X]) → F[X])^[k]
      (∏ vj ∈ image v (s.erase i), HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) vj : F[X])) =
    HMul.hMul (α := F[X]) (↑k.factorial : F[X])
      (∑ t ∈ powersetCard (#s - (k + 1)) (image v (s.erase i)),
        ∏ va ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) va : F[X]))

Tactic:
grind [iterate_derivative_prod_X_sub_C]

Premises used: Polynomial.iterate_derivative_prod_X_sub_C
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
hvs' : Set.InjOn v (↑(s.erase i) : Set ι)
rw :
  HMul.hMul (α := F[X]) (↑k.factorial : F[X])
      (∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i),
        ∏ a ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v a) : F[X])) =
    HMul.hMul (α := F[X]) (↑k.factorial : F[X])
      (∑ t ∈ image (fun (x : Finset ι) ↦ image v x) (s.erase i).powerset with #t = #s - (k + 1),
        ∏ va ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) va : F[X]))
⊢ HMul.hMul (α := F[X]) (↑k.factorial : F[X])
      (∑ t ∈ powersetCard (#s - (k + 1)) (image v (s.erase i)),
        ∏ va ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) va : F[X])) =
    HMul.hMul (α := F[X]) (↑k.factorial : F[X])
      (∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i),
        ∏ a ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v a) : F[X]))

Tactic:
rw [powersetCard_eq_filter, powerset_image, eq_comm]

Premises used: Finset.powersetCard_eq_filter, Finset.powerset_image, eq_comm
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
hvs' : Set.InjOn v (↑(s.erase i) : Set ι)
congrm :
  Eq.{u_1 + 1} (α := F[X])
    (∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i),
      ∏ a ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v a) : F[X]))
    (∑ t ∈ image (fun (x : Finset ι) ↦ image v x) (s.erase i).powerset with #t = #s - (k + 1),
      ∏ va ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) va : F[X]))
⊢ HMul.hMul (α := F[X]) (↑k.factorial : F[X])
      (∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i),
        ∏ a ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v a) : F[X])) =
    HMul.hMul (α := F[X]) (↑k.factorial : F[X])
      (∑ t ∈ image (fun (x : Finset ι) ↦ image v x) (s.erase i).powerset with #t = #s - (k + 1),
        ∏ va ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) va : F[X]))

Tactic:
congrm k.factorial * ?_

Premises used: Nat.factorial
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
hvs' : Set.InjOn v (↑(s.erase i) : Set ι)
⊢ Eq.{u_1 + 1} (α := F[X])
    (∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i),
      ∏ a ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v a) : F[X]))
    (∑ t ∈ image (fun (x : Finset ι) ↦ image v x) (s.erase i).powerset with #t = #s - (k + 1),
      ∏ va ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) va : F[X]))

Tactic:
sum_nbij (·.image v) (fun a ha ↦ ?hi) ?i_inj (fun t ht ↦ ?i_surj) fun a ha ↦ ?h

Premises used: Finset.sum_nbij, Finset.image
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
hvs' : Set.InjOn v (↑(s.erase i) : Set ι)
refine :
  ∀ (a : Finset ι) (ha : a ∈ powersetCard (#s - (k + 1)) (s.erase i)),
    Membership.mem (γ := Finset (Finset F))
      ({x ∈ image (fun (x : Finset ι) ↦ image v x) (s.erase i).powerset | #x = #s - (k + 1)})
      ((fun (x : Finset ι) ↦ image v x) a)
refine₁ :
  Set.InjOn.{u_2, u_1} (β := Finset F) (fun (x : Finset ι) ↦ image v x)
    (↑(powersetCard (#s - (k + 1)) (s.erase i)) : Set (Finset ι))
refine₂ :
  ∀ (t : Finset F)
    (ht :
      t ∈ (↑({x ∈ image (fun (x : Finset ι) ↦ image v x) (s.erase i).powerset | #x = #s - (k + 1)}) : Set (Finset F))),
    Membership.mem (γ := Set (Finset F))
      ((fun (x : Finset ι) ↦ image v x) '' (↑(powersetCard (#s - (k + 1)) (s.erase i)) : Set (Finset ι))) t
refine₃ :
  ∀ (a : Finset ι) (ha : a ∈ powersetCard (#s - (k + 1)) (s.erase i)),
    Eq.{u_1 + 1} (α := F[X]) (∏ a ∈ a, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v a) : F[X]))
      (∏ va ∈ (fun (x : Finset ι) ↦ image v x) a, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) va : F[X]))
⊢ Eq.{u_1 + 1} (α := F[X])
    (∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i),
      ∏ a ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v a) : F[X]))
    (∑ t ∈ image (fun (x : Finset ι) ↦ image v x) (s.erase i).powerset with #t = #s - (k + 1),
      ∏ va ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) va : F[X]))

Tactic:
refine sum_nbij (·.image v) (fun a ha ↦ ?hi) ?i_inj (fun t ht ↦ ?i_surj) fun a ha ↦ ?h

Premises used: Finset.sum_nbij
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
hvs' : Set.InjOn v (↑(s.erase i) : Set ι)
a : Finset ι
ha : a ∈ powersetCard (#s - (k + 1)) (s.erase i)
⊢ Membership.mem (γ := Finset (Finset F))
    ({x ∈ image (fun (x : Finset ι) ↦ image v x) (s.erase i).powerset | #x = #s - (k + 1)})
    ((fun (x : Finset ι) ↦ image v x) a)

Tactic:
grind [card_image_of_injOn, hvs'.mono]

Premises used: Set.InjOn.mono, Finset.card_image_of_injOn
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
hvs' : Set.InjOn v (↑(s.erase i) : Set ι)
a : Finset ι
ha : a ∈ powersetCard (#s - (k + 1)) (s.erase i)
⊢ Membership.mem (γ := Finset (Finset F))
    ({x ∈ image (fun (x : Finset ι) ↦ image v x) (s.erase i).powerset | #x = #s - (k + 1)})
    ((fun (x : Finset ι) ↦ image v x) a)

Tactic:
case hi => grind [card_image_of_injOn, hvs'.mono]

Premises used: Set.InjOn.mono, Finset.card_image_of_injOn
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
hvs' : Set.InjOn v (↑(s.erase i) : Set ι)
⊢ (↑(powersetCard (#s - (k + 1)) (s.erase i)) : Set (Finset ι)) ⊆ (↑(s.erase i).powerset : Set (Finset ι))

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
hvs' : Set.InjOn v (↑(s.erase i) : Set ι)
⊢ Set.InjOn.{u_2, u_1} (β := Finset F) (fun (x : Finset ι) ↦ image v x)
    (↑(powersetCard (#s - (k + 1)) (s.erase i)) : Set (Finset ι))

Tactic:
exact (image_injOn_powerset_of_injOn hvs').mono (by grind)

Premises used: Finset.image_injOn_powerset_of_injOn, Set.InjOn.mono
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
hvs' : Set.InjOn v (↑(s.erase i) : Set ι)
⊢ Set.InjOn.{u_2, u_1} (β := Finset F) (fun (x : Finset ι) ↦ image v x)
    (↑(powersetCard (#s - (k + 1)) (s.erase i)) : Set (Finset ι))

Tactic:
case i_inj => exact (image_injOn_powerset_of_injOn hvs').mono (by grind)

Premises used: Finset.image_injOn_powerset_of_injOn, Set.InjOn.mono
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
hvs' : Set.InjOn v (↑(s.erase i) : Set ι)
t : Finset F
ht : t ∈ (↑({x ∈ image (fun (x : Finset ι) ↦ image v x) (s.erase i).powerset | #x = #s - (k + 1)}) : Set (Finset F))
⊢ Membership.mem (γ := Set (Finset F))
    ((fun (x : Finset ι) ↦ image v x) '' (↑(powersetCard (#s - (k + 1)) (s.erase i)) : Set (Finset ι))) t

Tactic:
grind [card_image_of_injOn, hvs'.mono]

Premises used: Set.InjOn.mono, Finset.card_image_of_injOn
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
hvs' : Set.InjOn v (↑(s.erase i) : Set ι)
t : Finset F
ht : t ∈ (↑({x ∈ image (fun (x : Finset ι) ↦ image v x) (s.erase i).powerset | #x = #s - (k + 1)}) : Set (Finset F))
⊢ Membership.mem (γ := Set (Finset F))
    ((fun (x : Finset ι) ↦ image v x) '' (↑(powersetCard (#s - (k + 1)) (s.erase i)) : Set (Finset ι))) t

Tactic:
case i_surj => grind [card_image_of_injOn, hvs'.mono]

Premises used: Set.InjOn.mono, Finset.card_image_of_injOn
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
hvs' : Set.InjOn v (↑(s.erase i) : Set ι)
a : Finset ι
ha : a ∈ powersetCard (#s - (k + 1)) (s.erase i)
⊢ Set.InjOn v (↑a : Set ι)

Tactic:
grind [hvs'.mono]

Premises used: Set.InjOn.mono
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
hvs' : Set.InjOn v (↑(s.erase i) : Set ι)
a : Finset ι
ha : a ∈ powersetCard (#s - (k + 1)) (s.erase i)
⊢ Eq.{u_1 + 1} (α := F[X]) (∏ a ∈ a, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v a) : F[X]))
    (∏ va ∈ (fun (x : Finset ι) ↦ image v x) a, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) va : F[X]))

Tactic:
exact eq_comm.mp <| prod_image <| by grind [hvs'.mono]

Premises used: eq_comm, Iff.mp, Finset.prod_image
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
hvs' : Set.InjOn v (↑(s.erase i) : Set ι)
a : Finset ι
ha : a ∈ powersetCard (#s - (k + 1)) (s.erase i)
⊢ Eq.{u_1 + 1} (α := F[X]) (∏ a ∈ a, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v a) : F[X]))
    (∏ va ∈ (fun (x : Finset ι) ↦ image v x) a, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) va : F[X]))

Tactic:
case h => exact eq_comm.mp <| prod_image <| by grind [hvs'.mono]

Premises used: eq_comm, Iff.mp, Finset.prod_image
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
hvs' : Set.InjOn v (↑(s.erase i) : Set ι)
j :
  Eq (α := F[X])
    ((⇑derivative : (a : F[X]) → F[X])^[k]
      (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X])))
    ((⇑derivative : (a : F[X]) → F[X])^[k]
      (∏ vj ∈ image v (s.erase i), HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) vj : F[X])))
j₁ :
  (⇑derivative : (a : F[X]) → F[X])^[k]
      (∏ vj ∈ image v (s.erase i), HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) vj : F[X])) =
    HMul.hMul (α := F[X]) (↑k.factorial : F[X])
      (∑ t ∈ powersetCard (#s - (k + 1)) (image v (s.erase i)),
        ∏ va ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) va : F[X]))
j₂ :
  HMul.hMul (α := F[X]) (↑k.factorial : F[X])
      (∑ t ∈ powersetCard (#s - (k + 1)) (image v (s.erase i)),
        ∏ va ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) va : F[X])) =
    HMul.hMul (α := F[X]) (↑k.factorial : F[X])
      (∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i),
        ∏ a ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v a) : F[X]))
⊢ (⇑derivative : (a : F[X]) → F[X])^[k]
      (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X])) =
    HMul.hMul (α := F[X]) (↑k.factorial : F[X])
      (∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i),
        ∏ j ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X]))

Tactic:
calc
    derivative^[k] (∏ j ∈ s.erase i, (X - C (v j))) =
    derivative^[k] (∏ vj ∈ (s.erase i).image v, (X - C vj)) := by rw [Finset.prod_image hvs']
    _ = k.factorial * ∑ t ∈ ((s.erase i).image v).powersetCard (#s - (k + 1)),
          ∏ va ∈ t, (X - C va) := by
        grind [iterate_derivative_prod_X_sub_C]
    _ = k.factorial * ∑ t ∈ (s.erase i).powersetCard (#s - (k + 1)), ∏ a ∈ t, (X - C (v a)) := by
        rw [powersetCard_eq_filter, powerset_image, eq_comm]
        congrm k.factorial * ?_
        refine sum_nbij (·.image v) (fun a ha ↦ ?hi) ?i_inj (fun t ht ↦ ?i_surj) fun a ha ↦ ?h
        case hi => grind [card_image_of_injOn, hvs'.mono]
        case i_inj => exact (image_injOn_powerset_of_injOn hvs').mono (by grind)
        case i_surj => grind [card_image_of_injOn, hvs'.mono]
        case h => exact eq_comm.mp <| prod_image <| by grind [hvs'.mono]

Premises used: Polynomial.derivative, Polynomial.C, HSub.hSub, Nat.iterate, Finset.prod, HAdd.hAdd, Nat.factorial, Finset.powersetCard, Finset.card, OfNat.ofNat, Finset.erase, Polynomial.X, DFunLike.coe, Finset.image
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v (↑s : Set ι)
P : F[X]
hP : P.degree < (↑(#s) : WithBot ℕ)
k : ℕ
hk : k < #s
x : F
nth_rewrite :
  eval x
      (HMul.hMul (α := F[X]) (↑k.factorial : F[X])
        (∑ i ∈ s,
          HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)) : F[X])
            (∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i),
                ∏ a ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v a) : F[X]) :
              F[X]))) =
    HMul.hMul (α := F) (↑k.factorial : F)
      (∑ i ∈ s,
        (eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)) *
          ∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i), ∏ a ∈ t, (x - v a))
⊢ eval x ((⇑derivative : (a : F[X]) → F[X])^[k] P) =
    HMul.hMul (α := F) (↑k.factorial : F)
      (∑ i ∈ s,
        (eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)) *
          ∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i), ∏ a ∈ t, (x - v a))

Tactic:
nth_rewrite 1 [eq_interpolate hvs hP, iterate_derivative_interpolate _ hvs hk]

Premises used: Lagrange.eq_interpolate, Lagrange.iterate_derivative_interpolate
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v (↑s : Set ι)
P : F[X]
hP : P.degree < (↑(#s) : WithBot ℕ)
k : ℕ
hk : k < #s
x : F
⊢ eval x
      (HMul.hMul (α := F[X]) (↑k.factorial : F[X])
        (∑ i ∈ s,
          HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)) : F[X])
            (∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i),
                ∏ a ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v a) : F[X]) :
              F[X]))) =
    HMul.hMul (α := F) (↑k.factorial : F)
      (∑ i ∈ s,
        (eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)) *
          ∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i), ∏ a ∈ t, (x - v a))

Tactic:
simp [eval_finsetSum, eval_prod]

Premises used: Polynomial.eval_prod, Polynomial.eval_finsetSum
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v (↑s : Set ι)
P : F[X]
hP : P.degree < (↑(#s) : WithBot ℕ)
⊢ ((interpolate s v : (a : ι → F) → F[X]) fun (i : ι) ↦ eval (v i) P) = P

Tactic:
(eq_interpolate hvs hP).symm

Premises used: Lagrange.eq_interpolate, Eq.symm
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v (↑s : Set ι)
P : F[X]
hP : P.degree < (↑(#s) : WithBot ℕ)
nth_rewrite :
  Eq.{u_1 + 1} (α := F)
    (∑ b ∈ s,
      (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (eval (v b) P) : F[X]) (Lagrange.basis s v b)).coeff
        (#s - 1))
    (∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j))
⊢ P.coeff (#s - 1) = ∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)

Tactic:
nth_rewrite 1 [eq_interpolate hvs hP, interpolate_apply, finsetSum_coeff]

Premises used: Polynomial.finsetSum_coeff, Lagrange.eq_interpolate, Lagrange.interpolate_apply
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v (↑s : Set ι)
P : F[X]
hP : P.degree < (↑(#s) : WithBot ℕ)
a :
  ∀ (i : ι) (hi : i ∈ s),
    (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (eval (v i) P) : F[X]) (Lagrange.basis s v i)).coeff
        (#s - 1) =
      eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)
⊢ Eq.{u_1 + 1} (α := F)
    (∑ b ∈ s,
      (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (eval (v b) P) : F[X]) (Lagrange.basis s v b)).coeff
        (#s - 1))
    (∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j))

Tactic:
congr! with i hi
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v (↑s : Set ι)
P : F[X]
hP : P.degree < (↑(#s) : WithBot ℕ)
i : ι
hi : i ∈ s
a : eval (v i) P * (∏ j ∈ s.erase i, (v i - v j))⁻¹ = eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)
⊢ (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (eval (v i) P) : F[X]) (Lagrange.basis s v i)).coeff
      (#s - 1) =
    eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)

Tactic:
rw [coeff_C_mul, ← natDegree_basis hvs hi, ← leadingCoeff, leadingCoeff_basis hvs hi]

Premises used: Lagrange.leadingCoeff_basis, Polynomial.coeff_C_mul, Polynomial.leadingCoeff, Lagrange.natDegree_basis
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v (↑s : Set ι)
P : F[X]
hP : P.degree < (↑(#s) : WithBot ℕ)
i : ι
hi : i ∈ s
⊢ eval (v i) P * (∏ j ∈ s.erase i, (v i - v j))⁻¹ = eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)

Tactic:
field_simp
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v (↑s : Set ι)
P : F[X]
hP : (↑(#s) : WithBot ℕ) = P.degree + 1
contrapose! : ∀ (hP : P.degree = ⊥), (↑(#s) : WithBot ℕ) ≠ P.degree + 1
⊢ P.degree ≠ ⊥

Tactic:
contrapose! hP
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v (↑s : Set ι)
P : F[X]
hP : P.degree = ⊥
⊢ (↑(#s) : WithBot ℕ) ≠ P.degree + 1

Tactic:
simp [hP]
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v (↑s : Set ι)
P : F[X]
hP : (↑(#s) : WithBot ℕ) = P.degree + 1
lift :
  ∀ (deg : ℕ) (hdeg : (↑deg : WithBot ℕ) = P.degree) (hP : (↑(#s) : WithBot ℕ) = (↑deg : WithBot ℕ) + 1),
    P.leadingCoeff = ∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)
⊢ P.leadingCoeff = ∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)

Tactic:
lift P.degree to ℕ using (by contrapose! hP; simp [hP]) with deg hdeg

Premises used: Polynomial.degree
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v (↑s : Set ι)
P : F[X]
deg : ℕ
hdeg : (↑deg : WithBot ℕ) = P.degree
hP : (↑(#s) : WithBot ℕ) = (↑deg : WithBot ℕ) + 1
⊢ (↑(#s) : WithBot ℕ) = (↑(deg + 1) : WithBot ℕ)

Tactic:
rw [← WithBot.coe_one, ← WithBot.coe_add] at hP

Premises used: WithBot.coe_one, WithBot.coe_add