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 t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v (↑s : Set ι)
f : F[X]
hf : f.degree < (↑(#s) : WithBot ℕ)
⊢ Eq.{u_1 + 1} (α := F[X]) ((interpolate s v : (a : ι → F) → F[X]) fun (x : ι) ↦ if x ∈ s then eval (v x) f else 0)
    ((interpolate s v : (a : ι → F) → F[X]) fun (i : ι) ↦ eval (v i) f)

Tactic:
exact interpolate_eq_of_values_eq_on _ _ fun _ hi => if_pos hi

Premises used: Lagrange.interpolate_eq_of_values_eq_on, if_pos
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v (↑s : Set ι)
f : ↥s → F
h :
  ∀ (i : ι) (hi : i ∈ s),
    (fun (f : ↥(degreeLT F #s)) (i : ↥s) ↦ eval (v (↑i : ι)) (↑f : F[X]))
        ((fun (r : ↥s → F) ↦
            (Subtype.mk (p := fun (x : F[X]) ↦ Membership.mem (γ := Submodule F F[X]) (degreeLT F #s) x)
                ((interpolate s v : (a : ι → F) → F[X]) fun (x : ι) ↦
                  if hx : x ∈ s then r (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) else 0)
                ⋯ :
              ↥(degreeLT F #s)))
          f)
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) =
      f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)
⊢ (fun (f : ↥(degreeLT F #s)) (i : ↥s) ↦ eval (v (↑i : ι)) (↑f : F[X]))
      ((fun (r : ↥s → F) ↦
          (Subtype.mk (p := fun (x : F[X]) ↦ Membership.mem (γ := Submodule F F[X]) (degreeLT F #s) x)
              ((interpolate s v : (a : ι → F) → F[X]) fun (x : ι) ↦
                if hx : x ∈ s then r (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) else 0)
              ⋯ :
            ↥(degreeLT F #s)))
        f) =
    f

Tactic:
ext ⟨i, hi⟩
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
i_1 j : ι
v r r' : ι → F
hvs : Set.InjOn v (↑s : Set ι)
f : ↥s → F
i : ι
hi : i ∈ s
h :
  (if hx : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hx) else 0) =
    f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)
⊢ (fun (f : ↥(degreeLT F #s)) (i : ↥s) ↦ eval (v (↑i : ι)) (↑f : F[X]))
      ((fun (r : ↥s → F) ↦
          (Subtype.mk (p := fun (x : F[X]) ↦ Membership.mem (γ := Submodule F F[X]) (degreeLT F #s) x)
              ((interpolate s v : (a : ι → F) → F[X]) fun (x : ι) ↦
                if hx : x ∈ s then r (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) else 0)
              ⋯ :
            ↥(degreeLT F #s)))
        f)
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) =
    f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)

Tactic:
simp only [eval_interpolate_at_node _ hvs hi]

Premises used: Lagrange.eval_interpolate_at_node
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
i_1 j : ι
v r r' : ι → F
hvs : Set.InjOn v (↑s : Set ι)
f : ↥s → F
i : ι
hi : i ∈ s
⊢ (if hx : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hx) else 0) =
    f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)

Tactic:
dif_pos hi

Premises used: dif_pos
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s t : Finset ι
i_1 j : ι
v r r' : ι → F
hvs : Set.InjOn v (↑s : Set ι)
f : ↥s → F
i : ι
hi : i ∈ s
⊢ (if hx : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hx) else 0) =
    f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)

Tactic:
exact dif_pos hi

Premises used: dif_pos
-- Module: Mathlib.LinearAlgebra.Lagrange
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
symm :
  Eq.{u_1 + 1} (α := F[X])
    (∑ 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) :
      F[X])
    ((interpolate t v : (a : ι → F) → F[X]) r : F[X])
⊢ Eq.{u_1 + 1} (α := F[X]) ((interpolate t v : (a : ι → F) → F[X]) r : F[X])
    (∑ 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) :
      F[X])

Tactic:
symm
-- Module: Mathlib.LinearAlgebra.Lagrange
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
⊢ Eq.{u_1 + 1} (α := F[X])
    (∑ 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) :
      F[X])
    ((interpolate t v : (a : ι → F) → F[X]) r : F[X])

Tactic:
eq_interpolate_of_eval_eq _ hvt (lt_of_le_of_lt (degree_sum_le _ _) ?_) fun i hi => ?_

Premises used: lt_of_le_of_lt, Polynomial.degree_sum_le, Lagrange.eq_interpolate_of_eval_eq
-- Module: Mathlib.LinearAlgebra.Lagrange
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
refine_1 :
  LT.lt (α := WithBot ℕ)
    (s.sup fun (b : ι) ↦
      (HMul.hMul (α := F[X]) (β := F[X]) ((interpolate (insert b (t \ s)) v : (a : ι → F) → F[X]) r : F[X])
          (Lagrange.basis s v b)).degree)
    (↑(#t) : WithBot ℕ)
refine_2 :
  ∀ (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
⊢ Eq.{u_1 + 1} (α := F[X])
    (∑ 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) :
      F[X])
    ((interpolate t v : (a : ι → F) → F[X]) r : F[X])

Tactic:
refine eq_interpolate_of_eval_eq _ hvt (lt_of_le_of_lt (degree_sum_le _ _) ?_) fun i hi => ?_

Premises used: lt_of_le_of_lt, Polynomial.degree_sum_le, Lagrange.eq_interpolate_of_eval_eq
-- Module: Mathlib.LinearAlgebra.Lagrange
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
refine_1 :
  ∀ b ∈ s,
    degree.{u_1} (R := F) ((interpolate (insert b (t \ s)) v : (a : ι → F) → F[X]) r) + degree (Lagrange.basis s v b) <
      (↑(#t) : WithBot ℕ)
⊢ LT.lt (α := WithBot ℕ)
    (s.sup fun (b : ι) ↦
      (HMul.hMul (α := F[X]) (β := F[X]) ((interpolate (insert b (t \ s)) v : (a : ι → F) → F[X]) r : F[X])
          (Lagrange.basis s v b)).degree)
    (↑(#t) : WithBot ℕ)

Tactic:
simp_rw [Nat.cast_withBot, Finset.sup_lt_iff (WithBot.bot_lt_coe #t), degree_mul]

Premises used: Finset.sup_lt_iff, Nat.cast_withBot, WithBot.bot_lt_coe, Finset.card, Polynomial.degree_mul
-- Module: Mathlib.LinearAlgebra.Lagrange
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
⊢ 1 ≤ #s

Tactic:
have hs : 1 ≤ #s := Nonempty.card_pos ⟨_, hi⟩
-- Module: Mathlib.LinearAlgebra.Lagrange
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
⊢ #s ≤ #t

Tactic:
have hst' : #s ≤ #t := card_le_card hst
-- Module: Mathlib.LinearAlgebra.Lagrange
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
rw₄ rw₅ : #t = #t
⊢ #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]

Premises used: add_tsub_assoc_of_le, add_assoc, Nat.succ_add_sub_one, zero_add, LE.le.trans, tsub_add_tsub_cancel
-- Module: Mathlib.LinearAlgebra.Lagrange
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)

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]
-- Module: Mathlib.LinearAlgebra.Lagrange
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)
refine_1 :
  degree.{u_1} (R := F) ((interpolate (insert i (t \ s)) v : (a : ι → F) → F[X]) r) < (↑(1 + (#t - #s)) : WithBot ℕ)
⊢ degree.{u_1} (R := F) ((interpolate (insert i (t \ s)) v : (a : ι → F) → F[X]) r) + degree (Lagrange.basis s v i) <
    (↑(#t) : 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))]

Premises used: Lagrange.degree_basis, Nat.cast_withBot, Set.InjOn.mono, WithBot.coe_add, WithBot.coe_ne_bot, WithBot.add_lt_add_iff_right
-- Module: Mathlib.LinearAlgebra.Lagrange
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) <
    (↑(#(insert i (t \ s))) : WithBot ℕ)

Tactic:
degree_interpolate_lt _
        (hvt.mono (coe_subset.mpr (insert_subset_iff.mpr ⟨hst hi, sdiff_subset⟩)))

Premises used: Iff.mpr, Finset.insert_subset_iff, Lagrange.degree_interpolate_lt, And.intro, Set.InjOn.mono, Finset.sdiff_subset, Finset.coe_subset
-- Module: Mathlib.LinearAlgebra.Lagrange
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) = #(insert i (t \ s))
⊢ degree.{u_1} (R := F) ((interpolate (insert i (t \ s)) v : (a : ι → F) → F[X]) r) < (↑(1 + (#t - #s)) : WithBot ℕ)

Tactic:
convert!
      degree_interpolate_lt _
        (hvt.mono (coe_subset.mpr (insert_subset_iff.mpr ⟨hst hi, sdiff_subset⟩)))

Premises used: Iff.mpr, Finset.insert_subset_iff, Lagrange.degree_interpolate_lt, And.intro, Set.InjOn.mono, Finset.sdiff_subset, Finset.coe_subset
-- Module: Mathlib.LinearAlgebra.Lagrange
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
h₂ h₃ : #t - #s + 1 = #t - #s + 1
⊢ 1 + (#t - #s) = #(insert i (t \ s))

Tactic:
rw [card_insert_of_notMem (notMem_sdiff_of_mem_right hi), card_sdiff_of_subset hst, add_comm]

Premises used: Finset.card_sdiff_of_subset, Finset.notMem_sdiff_of_mem_right, Finset.card_insert_of_notMem, add_comm
-- Module: Mathlib.LinearAlgebra.Lagrange
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
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
⊢ 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

Tactic:
simp_rw [eval_finsetSum, eval_mul]

Premises used: Polynomial.eval_mul, Polynomial.eval_finsetSum
-- Module: Mathlib.LinearAlgebra.Lagrange
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
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
⊢ ∑ 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
-- Module: Mathlib.LinearAlgebra.Lagrange
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
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
⊢ ∑ 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:
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]

Premises used: Iff.mpr, Finset.mem_insert_self, Finset.insert_subset_iff, Finset.add_sum_erase, add_eq_left, And.intro, Set.InjOn.mono, Lagrange.eval_interpolate_at_node, mul_one, Lagrange.eval_basis_self, Finset.sdiff_subset, Finset.coe_subset
-- Module: Mathlib.LinearAlgebra.Lagrange
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

Tactic:
sum_eq_zero fun j hj => ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.LinearAlgebra.Lagrange
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
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
⊢ 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:
refine sum_eq_zero fun j hj => ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.LinearAlgebra.Lagrange
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
⊢ j ≠ i

Tactic:
rcases mem_erase.mp hj with ⟨hij, _⟩

Premises used: Finset.mem_erase, Iff.mp
-- Module: Mathlib.LinearAlgebra.Lagrange
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
⊢ j ∈ s

Tactic:
rcases mem_erase.mp hj with ⟨hij, _⟩

Premises used: Finset.mem_erase, Iff.mp
-- Module: Mathlib.LinearAlgebra.Lagrange
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
pos₁ pos₂ : Eq.{u_1 + 1} (α := F) 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

Tactic:
rw [eval_basis_of_ne hij hi', mul_zero]

Premises used: MulZeroClass.mul_zero, Lagrange.eval_basis_of_ne
-- Module: Mathlib.LinearAlgebra.Lagrange
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
rw₂ rw₃ : Eq.{u_1 + 1} (α := F) 1 1
⊢ Eq.{u_1 + 1} (α := F) (∑ j ∈ s, eval (v i) (Lagrange.basis s v j)) 1

Tactic:
rw [← eval_finsetSum, sum_basis (hvt.mono hst) hs, eval_one]

Premises used: Polynomial.eval_finsetSum, Polynomial.eval_one, Set.InjOn.mono, Lagrange.sum_basis
-- Module: Mathlib.LinearAlgebra.Lagrange
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

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]
-- Module: Mathlib.LinearAlgebra.Lagrange
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
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))
⊢ ∑ 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:
rw [← mul_one (r i), ← H, mul_sum]

Premises used: Finset.mul_sum, mul_one
-- Module: Mathlib.LinearAlgebra.Lagrange
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))

Tactic:
sum_congr rfl fun j hj => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Lagrange
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
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)
⊢ 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:
refine sum_congr rfl fun j hj => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Lagrange
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
neg : eval (v i) ((interpolate (insert j (t \ s)) v : (a : ι → F) → F[X]) r) = r i
⊢ 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:
congr
-- Module: Mathlib.LinearAlgebra.Lagrange
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) = r i

Tactic:
eval_interpolate_at_node _ (hvt.mono (insert_subset_iff.mpr ⟨hst hj, sdiff_subset⟩))
          (mem_insert.mpr (Or.inr (mem_sdiff.mpr ⟨hi, hi'⟩)))

Premises used: Iff.mpr, Finset.insert_subset_iff, Finset.mem_insert, Finset.mem_sdiff, And.intro, Set.InjOn.mono, Lagrange.eval_interpolate_at_node, Finset.sdiff_subset, Or.inr
-- Module: Mathlib.LinearAlgebra.Lagrange
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) = r i

Tactic:
exact
        eval_interpolate_at_node _ (hvt.mono (insert_subset_iff.mpr ⟨hst hj, sdiff_subset⟩))
          (mem_insert.mpr (Or.inr (mem_sdiff.mpr ⟨hi, hi'⟩)))

Premises used: Iff.mpr, Finset.insert_subset_iff, Finset.mem_insert, Finset.mem_sdiff, And.intro, Set.InjOn.mono, Lagrange.eval_interpolate_at_node, Finset.sdiff_subset, Or.inr
-- Module: Mathlib.LinearAlgebra.Lagrange
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
rw : {i, j} ⊆ s
⊢ (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))

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]

Premises used: Finset.notMem_singleton, Iff.mpr, Finset.pair_comm, Lagrange.basis_pair_right, Finset.sdiff_singleton_eq_erase, Finset.sdiff_insert_insert_of_mem_of_notMem, Lagrange.interpolate_eq_sum_interpolate_insert_sdiff, Finset.mem_insert_self, Ne.symm, Finset.sum_singleton, Exists.intro, Finset.sum_insert, Singleton.singleton, Lagrange.basis_pair_left
-- Module: Mathlib.LinearAlgebra.Lagrange
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
⊢ {i, j} ⊆ s

Tactic:
insert_subset_iff.mpr ⟨hi, singleton_subset_iff.mpr hj⟩

Premises used: Iff.mpr, Finset.insert_subset_iff, Finset.singleton_subset_iff, And.intro
-- Module: Mathlib.LinearAlgebra.Lagrange
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
⊢ {i, j} ⊆ s

Tactic:
exact insert_subset_iff.mpr ⟨hi, singleton_subset_iff.mpr hj⟩

Premises used: Iff.mpr, Finset.insert_subset_iff, Finset.singleton_subset_iff, And.intro
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
⊢ Eq.{u_1 + 1} (α := F[X]) ((interpolate s v : (a : ι → F) → F[X]) r : 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])
          (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X]) : F[X]) :
      F[X])

Tactic:
simp [Lagrange.basis, basisDivisor, div_eq_mul_inv, prod_mul_distrib, ← map_prod,
    ← prod_inv_distrib, mul_assoc]

Premises used: Finset.prod_mul_distrib, mul_assoc, Finset.prod_inv_distrib, div_eq_mul_inv, map_prod, Lagrange.basis, Lagrange.basisDivisor