awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (hypothesis)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ s
⊢ degree.{u_1} (R := F) ((interpolate (insert i (t \ s)) v : (a : ι → F) → F[X]) r) + degree (Lagrange.basis s v i) <
    (↑(#t) : WithBot ℕ)
have hs₁ : 1 ≤ #s
Tactic: have hs : 1 ≤ #s := Nonempty.card_pos ⟨_, hi⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (hypothesis)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs_1 : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ s
hs : 1 ≤ #s
⊢ degree.{u_1} (R := F) ((interpolate (insert i (t \ s)) v : (a : ι → F) → F[X]) r) + degree (Lagrange.basis s v i) <
    (↑(#t) : WithBot ℕ)
have hst' : #s ≤ #t
Tactic: have hst' : #s ≤ #t := card_le_card hst
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs_1 : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ s
hs : 1 ≤ #s
hst' : #s ≤ #t
⊢ #t = 1 + (#t - #s) + (#s - 1)
have rw : #t = 1 + (#t - #s + (#s - 1))
Tactic: rw [add_assoc, tsub_add_tsub_cancel hst' hs, ← add_tsub_assoc_of_le (hs.trans hst'),
        Nat.succ_add_sub_one, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs_1 : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ s
hs : 1 ≤ #s
hst' : #s ≤ #t
rw : #t = 1 + (#t - #s + (#s - 1))
⊢ #t = 1 + (#t - #s) + (#s - 1)
have rw₁ : #t = 1 + (#t - 1)
Tactic: rw [add_assoc, tsub_add_tsub_cancel hst' hs, ← add_tsub_assoc_of_le (hs.trans hst'),
        Nat.succ_add_sub_one, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs_1 : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ s
hs : 1 ≤ #s
hst' : #s ≤ #t
rw : #t = 1 + (#t - #s + (#s - 1))
rw₁ : #t = 1 + (#t - 1)
⊢ #t = 1 + (#t - #s) + (#s - 1)
have rw₂ : #t = 1 + #t - 1
Tactic: rw [add_assoc, tsub_add_tsub_cancel hst' hs, ← add_tsub_assoc_of_le (hs.trans hst'),
        Nat.succ_add_sub_one, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs_1 : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ s
hs : 1 ≤ #s
hst' : #s ≤ #t
rw : #t = 1 + (#t - #s + (#s - 1))
rw₁ : #t = 1 + (#t - 1)
rw₂ : #t = 1 + #t - 1
⊢ #t = 1 + (#t - #s) + (#s - 1)
have rw₃ : #t = 0 + #t
Tactic: rw [add_assoc, tsub_add_tsub_cancel hst' hs, ← add_tsub_assoc_of_le (hs.trans hst'),
        Nat.succ_add_sub_one, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs_1 : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ s
hs : 1 ≤ #s
hst' : #s ≤ #t
rw : #t = 1 + (#t - #s + (#s - 1))
rw₁ : #t = 1 + (#t - 1)
rw₂ : #t = 1 + #t - 1
rw₃ : #t = 0 + #t
⊢ #t = 1 + (#t - #s) + (#s - 1)
have rw₄ : #t = #t
Tactic: rw [add_assoc, tsub_add_tsub_cancel hst' hs, ← add_tsub_assoc_of_le (hs.trans hst'),
        Nat.succ_add_sub_one, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (hypothesis)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs_1 : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ s
hs : 1 ≤ #s
hst' : #s ≤ #t
⊢ degree.{u_1} (R := F) ((interpolate (insert i (t \ s)) v : (a : ι → F) → F[X]) r) + degree (Lagrange.basis s v i) <
    (↑(#t) : WithBot ℕ)
have H : #t = 1 + (#t - #s) + (#s - 1)
Tactic: have H : #t = 1 + (#t - #s) + (#s - 1) := by
      rw [add_assoc, tsub_add_tsub_cancel hst' hs, ← add_tsub_assoc_of_le (hs.trans hst'),
        Nat.succ_add_sub_one, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs_1 : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ s
hs : 1 ≤ #s
hst' : #s ≤ #t
H : #t = 1 + (#t - #s) + (#s - 1)
⊢ degree.{u_1} (R := F) ((interpolate (insert i (t \ s)) v : (a : ι → F) → F[X]) r) + degree (Lagrange.basis s v i) <
    (↑(#t) : WithBot ℕ)
have refine_1 : degree.{u_1} (R := F) ((interpolate (insert i (t \ s)) v : (a : ι → F) → F[X]) r) < (↑(1 + (#t - #s)) : WithBot ℕ)
Tactic: rw [degree_basis (Set.InjOn.mono hst hvt) hi, H, WithBot.coe_add, Nat.cast_withBot,
      WithBot.add_lt_add_iff_right (@WithBot.coe_ne_bot _ (#s - 1))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs_1 : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ s
hs : 1 ≤ #s
hst' : #s ≤ #t
H : #t = 1 + (#t - #s) + (#s - 1)
⊢ degree.{u_1} (R := F) ((interpolate (insert i (t \ s)) v : (a : ι → F) → F[X]) r) < (↑(1 + (#t - #s)) : WithBot ℕ)
have h : 1 + (#t - #s) = #(insert i (t \ s))
Tactic: convert!
      degree_interpolate_lt _
        (hvt.mono (coe_subset.mpr (insert_subset_iff.mpr ⟨hst hi, sdiff_subset⟩)))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs_1 : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ s
hs : 1 ≤ #s
hst' : #s ≤ #t
H : #t = 1 + (#t - #s) + (#s - 1)
⊢ 1 + (#t - #s) = #(insert i (t \ s))
have h : 1 + (#t - #s) = #(t \ s) + 1
Tactic: rw [card_insert_of_notMem (notMem_sdiff_of_mem_right hi), card_sdiff_of_subset hst, add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs_1 : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ s
hs : 1 ≤ #s
hst' : #s ≤ #t
H : #t = 1 + (#t - #s) + (#s - 1)
h : 1 + (#t - #s) = #(t \ s) + 1
⊢ 1 + (#t - #s) = #(insert i (t \ s))
have h₁ : 1 + (#t - #s) = #t - #s + 1
Tactic: rw [card_insert_of_notMem (notMem_sdiff_of_mem_right hi), card_sdiff_of_subset hst, add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs_1 : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ s
hs : 1 ≤ #s
hst' : #s ≤ #t
H : #t = 1 + (#t - #s) + (#s - 1)
h : 1 + (#t - #s) = #(t \ s) + 1
h₁ : 1 + (#t - #s) = #t - #s + 1
⊢ 1 + (#t - #s) = #(insert i (t \ s))
have h₂ : #t - #s + 1 = #t - #s + 1
Tactic: rw [card_insert_of_notMem (notMem_sdiff_of_mem_right hi), card_sdiff_of_subset hst, add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
⊢ eval (v i)
      (∑ i ∈ s,
        HMul.hMul (α := F[X]) (β := F[X]) ((interpolate (insert i (t \ s)) v : (a : ι → F) → F[X]) r : F[X])
          (Lagrange.basis s v i)) =
    r i
have refine_2 : ∑ x ∈ s, eval (v i) ((interpolate (insert x (t \ s)) v : (a : ι → F) → F[X]) r) * eval (v i) (Lagrange.basis s v x) =
  r i
Tactic: simp_rw [eval_finsetSum, eval_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
⊢ ∑ x ∈ s, eval (v i) ((interpolate (insert x (t \ s)) v : (a : ι → F) → F[X]) r) * eval (v i) (Lagrange.basis s v x) =
    r i
have pos : ∀ (hi' : i ∈ s),
  ∑ x ∈ s, eval (v i) ((interpolate (insert x (t \ s)) v : (a : ι → F) → F[X]) r) * eval (v i) (Lagrange.basis s v x) =
    r i
Tactic: by_cases hi' : i ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
pos :
  ∀ (hi' : i ∈ s),
    ∑ x ∈ s,
        eval (v i) ((interpolate (insert x (t \ s)) v : (a : ι → F) → F[X]) r) * eval (v i) (Lagrange.basis s v x) =
      r i
⊢ ∑ x ∈ s, eval (v i) ((interpolate (insert x (t \ s)) v : (a : ι → F) → F[X]) r) * eval (v i) (Lagrange.basis s v x) =
    r i
have neg : ∀ (hi' : i ∉ s),
  ∑ x ∈ s, eval (v i) ((interpolate (insert x (t \ s)) v : (a : ι → F) → F[X]) r) * eval (v i) (Lagrange.basis s v x) =
    r i
Tactic: by_cases hi' : i ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∈ s
⊢ ∑ x ∈ s, eval (v i) ((interpolate (insert x (t \ s)) v : (a : ι → F) → F[X]) r) * eval (v i) (Lagrange.basis s v x) =
    r i
have pos : Eq.{u_1 + 1} (α := F)
  (∑ x ∈ s.erase i,
    eval (v i) ((interpolate (insert x (t \ s)) v : (a : ι → F) → F[X]) r) * eval (v i) (Lagrange.basis s v x))
  0
Tactic: rw [← add_sum_erase _ _ hi', eval_basis_self (hvt.mono hst) hi',
        eval_interpolate_at_node _
          (hvt.mono (coe_subset.mpr (insert_subset_iff.mpr ⟨hi, sdiff_subset⟩)))
          (mem_insert_self _ _),
        mul_one, add_eq_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∈ s
⊢ Eq.{u_1 + 1} (α := F)
    (∑ x ∈ s.erase i,
      eval (v i) ((interpolate (insert x (t \ s)) v : (a : ι → F) → F[X]) r) * eval (v i) (Lagrange.basis s v x))
    0
have pos : ∀ (j : ι) (hj : j ∈ s.erase i),
  eval (v i) ((interpolate (insert j (t \ s)) v : (a : ι → F) → F[X]) r) * eval (v i) (Lagrange.basis s v j) = 0
Tactic: refine sum_eq_zero fun j hj => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (hypothesis)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∈ s
j : ι
hj : j ∈ s.erase i
⊢ eval (v i) ((interpolate (insert j (t \ s)) v : (a : ι → F) → F[X]) r) * eval (v i) (Lagrange.basis s v j) = 0
have hij : j ≠ i
Tactic: rcases mem_erase.mp hj with ⟨hij, _⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (hypothesis)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∈ s
j : ι
hj : j ∈ s.erase i
hij : j ≠ i
⊢ eval (v i) ((interpolate (insert j (t \ s)) v : (a : ι → F) → F[X]) r) * eval (v i) (Lagrange.basis s v j) = 0
have right : j ∈ s
Tactic: rcases mem_erase.mp hj with ⟨hij, _⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∈ s
j : ι
hj : j ∈ s.erase i
hij : j ≠ i
right : j ∈ s
⊢ eval (v i) ((interpolate (insert j (t \ s)) v : (a : ι → F) → F[X]) r) * eval (v i) (Lagrange.basis s v j) = 0
have pos : eval (v i) ((interpolate (insert j (t \ s)) v : (a : ι → F) → F[X]) r) * 0 = 0
Tactic: rw [eval_basis_of_ne hij hi', mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∈ s
j : ι
hj : j ∈ s.erase i
hij : j ≠ i
right : j ∈ s
pos : eval (v i) ((interpolate (insert j (t \ s)) v : (a : ι → F) → F[X]) r) * 0 = 0
⊢ eval (v i) ((interpolate (insert j (t \ s)) v : (a : ι → F) → F[X]) r) * eval (v i) (Lagrange.basis s v j) = 0
have pos₁ : Eq.{u_1 + 1} (α := F) 0 0
Tactic: rw [eval_basis_of_ne hij hi', mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∉ s
⊢ Eq.{u_1 + 1} (α := F) (∑ j ∈ s, eval (v i) (Lagrange.basis s v j)) 1
have rw : eval (v i) (∑ i ∈ s, Lagrange.basis s v i) = 1
Tactic: rw [← eval_finsetSum, sum_basis (hvt.mono hst) hs, eval_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∉ s
rw : eval (v i) (∑ i ∈ s, Lagrange.basis s v i) = 1
⊢ Eq.{u_1 + 1} (α := F) (∑ j ∈ s, eval (v i) (Lagrange.basis s v j)) 1
have rw₁ : eval (v i) 1 = 1
Tactic: rw [← eval_finsetSum, sum_basis (hvt.mono hst) hs, eval_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∉ s
rw : eval (v i) (∑ i ∈ s, Lagrange.basis s v i) = 1
rw₁ : eval (v i) 1 = 1
⊢ Eq.{u_1 + 1} (α := F) (∑ j ∈ s, eval (v i) (Lagrange.basis s v j)) 1
have rw₂ : Eq.{u_1 + 1} (α := F) 1 1
Tactic: rw [← eval_finsetSum, sum_basis (hvt.mono hst) hs, eval_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (hypothesis)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∉ s
⊢ ∑ x ∈ s, eval (v i) ((interpolate (insert x (t \ s)) v : (a : ι → F) → F[X]) r) * eval (v i) (Lagrange.basis s v x) =
    r i
have H : Eq.{u_1 + 1} (α := F) (∑ j ∈ s, eval (v i) (Lagrange.basis s v j)) 1
Tactic: have H : (∑ j ∈ s, eval (v i) (Lagrange.basis s v j)) = 1 := by
        rw [← eval_finsetSum, sum_basis (hvt.mono hst) hs, eval_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∉ s
H : Eq.{u_1 + 1} (α := F) (∑ j ∈ s, eval (v i) (Lagrange.basis s v j)) 1
⊢ ∑ x ∈ s, eval (v i) ((interpolate (insert x (t \ s)) v : (a : ι → F) → F[X]) r) * eval (v i) (Lagrange.basis s v x) =
    r i
have neg : Eq.{u_1 + 1} (α := F)
  (∑ x ∈ s, eval (v i) ((interpolate (insert x (t \ s)) v : (a : ι → F) → F[X]) r) * eval (v i) (Lagrange.basis s v x))
  (∑ i_1 ∈ s, r i * eval (v i) (Lagrange.basis s v i_1))
Tactic: rw [← mul_one (r i), ← H, mul_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∉ s
H : Eq.{u_1 + 1} (α := F) (∑ j ∈ s, eval (v i) (Lagrange.basis s v j)) 1
⊢ Eq.{u_1 + 1} (α := F)
    (∑ x ∈ s,
      eval (v i) ((interpolate (insert x (t \ s)) v : (a : ι → F) → F[X]) r) * eval (v i) (Lagrange.basis s v x))
    (∑ i_1 ∈ s, r i * eval (v i) (Lagrange.basis s v i_1))
have neg : ∀ (j : ι) (hj : j ∈ s),
  eval (v i) ((interpolate (insert j (t \ s)) v : (a : ι → F) → F[X]) r) * eval (v i) (Lagrange.basis s v j) =
    r i * eval (v i) (Lagrange.basis s v j)
Tactic: refine sum_congr rfl fun j hj => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∉ s
H : Eq.{u_1 + 1} (α := F) (∑ j ∈ s, eval (v i) (Lagrange.basis s v j)) 1
j : ι
hj : j ∈ s
⊢ eval (v i) ((interpolate (insert j (t \ s)) v : (a : ι → F) → F[X]) r) * eval (v i) (Lagrange.basis s v j) =
    r i * eval (v i) (Lagrange.basis s v j)
have neg : eval (v i) ((interpolate (insert j (t \ s)) v : (a : ι → F) → F[X]) r) = r i
Tactic: congr
-- 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 ι
i j : ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
hj : j ∈ s
hij : i ≠ j
⊢ (interpolate s v : (a : ι → F) → F[X]) r =
    HMul.hMul (α := F[X]) (β := F[X]) ((interpolate (s.erase j) v : (a : ι → F) → F[X]) r : F[X])
        (basisDivisor (v i) (v j)) +
      HMul.hMul (α := F[X]) (β := F[X]) ((interpolate (s.erase i) v : (a : ι → F) → F[X]) r : F[X])
        (basisDivisor (v j) (v i))
have rw : {i, j} ⊆ s
Tactic: rw [interpolate_eq_sum_interpolate_insert_sdiff _ hvs ⟨i, mem_insert_self i {j}⟩ _,
    sum_insert (notMem_singleton.mpr hij), sum_singleton, basis_pair_left hij,
    basis_pair_right hij, sdiff_insert_insert_of_mem_of_notMem hi (notMem_singleton.mpr hij),
    sdiff_singleton_eq_erase, pair_comm,
    sdiff_insert_insert_of_mem_of_notMem hj (notMem_singleton.mpr hij.symm),
    sdiff_singleton_eq_erase]
-- 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 : 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: 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]
-- 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
⊢ 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]))))
have 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]))
Tactic: congr! 2 with i hi
-- 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 r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
k : ℕ
hk : k < #s
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]))
have hvs' : Set.InjOn v (↑(s.erase i) : Set ι)
Tactic: have hvs' := hvs.mono (coe_subset.mpr (erase_subset i s))
-- 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 (α := 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])))
have 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])))
Tactic: rw [Finset.prod_image hvs']
-- 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 ι)
⊢ 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]))
have 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]))
Tactic: rw [powersetCard_eq_filter, powerset_image, eq_comm]
-- 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 ι)
⊢ 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]))
have 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]))
Tactic: congrm k.factorial * ?_