awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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]))
have 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)
Tactic: refine sum_nbij (·.image v) (fun a ha ↦ ?hi) ?i_inj (fun t ht ↦ ?i_surj) fun a ha ↦ ?h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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)
⊢ 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]))
have refine₁ : Set.InjOn.{u_2, u_1} (β := Finset F) (fun (x : Finset ι) ↦ image v x)
  (↑(powersetCard (#s - (k + 1)) (s.erase i)) : Set (Finset ι))
Tactic: refine sum_nbij (·.image v) (fun a ha ↦ ?hi) ?i_inj (fun t ht ↦ ?i_surj) fun a ha ↦ ?h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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 ι))
⊢ 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]))
have 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
Tactic: refine sum_nbij (·.image v) (fun a ha ↦ ?hi) ?i_inj (fun t ht ↦ ?i_surj) fun a ha ↦ ?h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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
⊢ 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]))
have 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]))
Tactic: refine sum_nbij (·.image v) (fun a ha ↦ ?hi) ?i_inj (fun t ht ↦ ?i_surj) fun a ha ↦ ?h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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]
      (∏ 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]))
have 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])))
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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])))
⊢ (⇑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]))
have 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]))
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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]))
⊢ (⇑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]))
have 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]))
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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
⊢ (⇑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]))
have simp_rw : (⇑derivative : (a : F[X]) → F[X])^[k]
    (∑ 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])
        (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X]) : F[X])) =
  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),
            ∏ j ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X]) :
          F[X]))
Tactic: classical
  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]
  congr! 2 with i hi
  have hvs' := hvs.mono (coe_subset.mpr (erase_subset i s))
  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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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 :
  (⇑derivative : (a : F[X]) → F[X])^[k]
      (∑ 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])
          (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X]) : F[X])) =
    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),
              ∏ j ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X]) :
            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]))
have simp_rw₁ : ∑ b ∈ s,
    (⇑derivative : (a : F[X]) → F[X])^[k]
      (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r b / ∏ j ∈ s.erase b, (v b - v j)) : F[X])
        (∏ j ∈ s.erase b, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X]) : F[X])) =
  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),
            ∏ j ∈ t, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X]) :
          F[X]))
Tactic: classical
  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]
  congr! 2 with i hi
  have hvs' := hvs.mono (coe_subset.mpr (erase_subset i s))
  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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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 ((⇑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))
have 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))
Tactic: nth_rewrite 1 [eq_interpolate hvs hP, iterate_derivative_interpolate _ hvs hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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.coeff (#s - 1) = ∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)
have 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))
Tactic: nth_rewrite 1 [eq_interpolate hvs hP, interpolate_apply, finsetSum_coeff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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 ℕ)
⊢ 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))
have 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)
Tactic: congr! with i hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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
⊢ (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)
have 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)
Tactic: rw [coeff_C_mul, ← natDegree_basis hvs hi, ← leadingCoeff, leadingCoeff_basis hvs hi]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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
⊢ P.degree ≠ ⊥
have contrapose! : ∀ (hP : P.degree = ⊥), (↑(#s) : WithBot ℕ) ≠ P.degree + 1
Tactic: contrapose! hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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
⊢ P.leadingCoeff = ∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)
have 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)
Tactic: lift P.degree to ℕ using (by contrapose! hP; simp [hP]) with deg hdeg
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (hypothesis)
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
⊢ P.leadingCoeff = ∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)
have hP₁ : (↑(#s) : WithBot ℕ) = (↑(deg + 1) : WithBot ℕ)
Tactic: rw [← WithBot.coe_one, ← WithBot.coe_add] at hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (hypothesis)
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 + 1) : WithBot ℕ)
⊢ P.leadingCoeff = ∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)
have hP₁ : #s = deg + 1
Tactic: replace hP : #s = deg + 1 := WithBot.coe_eq_coe.mp hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (hypothesis)
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 = deg + 1
⊢ P.leadingCoeff = ∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)
have hdegree : P.degree = (↑(#s - 1) : WithBot ℕ)
Tactic: have hdegree : P.degree = ↑(#s - 1) := hdeg.symm.trans (WithBot.coe_eq_coe.mpr (by grind))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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 = deg + 1
hdegree : P.degree = (↑(#s - 1) : WithBot ℕ)
⊢ P.leadingCoeff = ∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)
have rw : P.coeff (#s - 1) = ∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)
Tactic: rw [leadingCoeff, natDegree_eq_of_degree_eq_some hdegree]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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 = deg + 1
hdegree : P.degree = (↑(#s - 1) : WithBot ℕ)
⊢ P.degree < (↑(#s) : WithBot ℕ)
have rw : LT.lt (α := WithBot ℕ) (↑(#s - 1) : WithBot ℕ) (↑(#s) : WithBot ℕ)
Tactic: rw [hdegree]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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 = deg + 1
hdegree : P.degree = (↑(#s - 1) : WithBot ℕ)
⊢ LT.lt (α := WithBot ℕ) (↑(#s - 1) : WithBot ℕ) (↑(#s) : WithBot ℕ)
have norm_cast : #s - 1 < #s
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
h : ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
i j : ι
hij : x i = x j
q : F[X]
hq : ∀ (i : ι), eval (x i) q = y i
⊢ y i = y j
have rw : eval (x i) q = y j
Tactic: rw [← hq, ← hq, hij]