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 ι
v r : ι → F
rw :
  Eq.{u_1 + 1} (α := F[X])
    (∑ i ∈ ∅, HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r i) : F[X]) (Lagrange.basis ∅ v i)) 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := F[X]) 0 0
⊢ Eq.{u_1 + 1} (α := F[X]) ((interpolate ∅ v : (a : ι → F) → F[X]) r : F[X]) (0 : F[X])

Tactic:
rw [interpolate_apply, sum_empty]

Premises used: Lagrange.interpolate_apply, Finset.sum_empty
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
i : ι
v r : ι → F
rw :
  Eq (α := F[X])
    (∑ i_1 ∈ {i}, HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r i_1) : F[X]) (Lagrange.basis {i} v i_1) :
      F[X])
    ((C : (a : F) → F[X]) (r i) : F[X])
rw₁ :
  HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r i) : F[X]) (Lagrange.basis {i} v i) =
    (C : (a : F) → F[X]) (r i)
rw₂ : HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r i) : F[X]) (1 : F[X]) = (C : (a : F) → F[X]) (r i)
rw₃ rw₄ : Eq (α := F[X]) ((C : (a : F) → F[X]) (r i) : F[X]) ((C : (a : F) → F[X]) (r i) : F[X])
⊢ Eq.{u_1 + 1} (α := F[X]) ((interpolate {i} v : (a : ι → F) → F[X]) r : F[X]) ((C : (a : F) → F[X]) (r i) : F[X])

Tactic:
rw [interpolate_apply, sum_singleton, basis_singleton, mul_one]

Premises used: Lagrange.basis_singleton, Finset.sum_singleton, Lagrange.interpolate_apply, mul_one
-- 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 ι)
hs : s.Nonempty
simp_rw : Eq.{u_1 + 1} (α := F[X]) (∑ x ∈ s, Lagrange.basis s v x) 1
⊢ Eq.{u_1 + 1} (α := F[X]) ((interpolate s v : (a : ι → F) → F[X]) 1) 1

Tactic:
simp_rw [interpolate_apply, Pi.one_apply, map_one, one_mul]

Premises used: Pi.one_apply, map_one, Lagrange.interpolate_apply, one_mul
-- 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 ι)
hs : s.Nonempty
⊢ Eq.{u_1 + 1} (α := F[X]) (∑ x ∈ s, Lagrange.basis s v x) 1

Tactic:
sum_basis hvs hs

Premises used: Lagrange.sum_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 ι)
hs : s.Nonempty
⊢ Eq.{u_1 + 1} (α := F[X]) (∑ x ∈ s, Lagrange.basis s v x) 1

Tactic:
exact sum_basis hvs hs

Premises used: Lagrange.sum_basis
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
rw :
  eval (v i) (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r i) : F[X]) (Lagrange.basis s v i)) +
      ∑ x ∈ s.erase i,
        eval (v i) (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r x) : F[X]) (Lagrange.basis s v x)) =
    r i
⊢ eval (v i) ((interpolate s v : (a : ι → F) → F[X]) r) = r i

Tactic:
rw [interpolate_apply, eval_finsetSum, ← add_sum_erase _ _ hi]

Premises used: Polynomial.eval_finsetSum, Finset.add_sum_erase, Lagrange.interpolate_apply
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
simp_rw : Eq.{u_1 + 1} (α := F) (∑ x ∈ s.erase i, r x * eval (v i) (Lagrange.basis s v x)) 0
⊢ eval (v i) (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r i) : F[X]) (Lagrange.basis s v i)) +
      ∑ x ∈ s.erase i,
        eval (v i) (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r x) : F[X]) (Lagrange.basis s v x)) =
    r i

Tactic:
simp_rw [eval_mul, eval_C, eval_basis_self hvs hi, mul_one, add_eq_left]

Premises used: Polynomial.eval_C, Polynomial.eval_mul, add_eq_left, mul_one, Lagrange.eval_basis_self
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
⊢ Eq.{u_1 + 1} (α := F) (∑ x ∈ s.erase i, r x * eval (v i) (Lagrange.basis s v x)) 0

Tactic:
sum_eq_zero fun j H => ?_

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 : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
refine : ∀ (j : ι) (H : j ∈ s.erase i), r j * eval (v i) (Lagrange.basis s v j) = 0
⊢ Eq.{u_1 + 1} (α := F) (∑ x ∈ s.erase i, r x * eval (v i) (Lagrange.basis s v x)) 0

Tactic:
refine sum_eq_zero fun j H => ?_

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 : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
j : ι
H : j ∈ s.erase i
rw : r j * 0 = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := F) 0 0
⊢ r j * eval (v i) (Lagrange.basis s v j) = 0

Tactic:
rw [eval_basis_of_ne (mem_erase.mp H).1 hi, mul_zero]

Premises used: MulZeroClass.mul_zero, Finset.mem_erase, Lagrange.eval_basis_of_ne, And.left, Iff.mp
-- 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 ι)
⊢ degree.{u_1} (R := F) ((interpolate s v : (a : ι → F) → F[X]) r) ≤ (↑(#s - 1) : WithBot ℕ)

Tactic:
(degree_sum_le _ _).trans ?_

Premises used: Multiset.sum, Multiset.foldr, Polynomial.degree_sum_le, LE.le.trans, Finset.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 ι)
refine :
  LE.le (α := WithBot ℕ)
    (s.sup fun (b : ι) ↦
      (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r b) : F[X]) (Lagrange.basis s v b)).degree)
    (↑(#s - 1) : WithBot ℕ)
⊢ degree.{u_1} (R := F) ((interpolate s v : (a : ι → F) → F[X]) r) ≤ (↑(#s - 1) : WithBot ℕ)

Tactic:
refine (degree_sum_le _ _).trans ?_

Premises used: Polynomial.degree_sum_le, LE.le.trans
-- 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 ι)
rw :
  ∀ b ∈ s,
    (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r b) : F[X]) (Lagrange.basis s v b)).degree ≤
      (↑(#s - 1) : WithBot ℕ)
⊢ LE.le (α := WithBot ℕ)
    (s.sup fun (b : ι) ↦
      (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r b) : F[X]) (Lagrange.basis s v b)).degree)
    (↑(#s - 1) : WithBot ℕ)

Tactic:
rw [Finset.sup_le_iff]

Premises used: Finset.sup_le_iff
-- 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 ι)
i : ι
hi : i ∈ s
rw : degree.{u_1} (R := F) ((C : (a : F) → F[X]) (r i)) + (↑(#s - 1) : WithBot ℕ) ≤ (↑(#s - 1) : WithBot ℕ)
⊢ (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r i) : F[X]) (Lagrange.basis s v i)).degree ≤
    (↑(#s - 1) : WithBot ℕ)

Tactic:
rw [degree_mul, degree_basis hvs hi]

Premises used: Lagrange.degree_basis, Polynomial.degree_mul
-- 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 ι)
i : ι
hi : i ∈ s
pos :
  ∀ (hr : r i = 0),
    degree.{u_1} (R := F) ((C : (a : F) → F[X]) (r i)) + (↑(#s - 1) : WithBot ℕ) ≤ (↑(#s - 1) : WithBot ℕ)
neg :
  ∀ (hr : ¬r i = 0),
    degree.{u_1} (R := F) ((C : (a : F) → F[X]) (r i)) + (↑(#s - 1) : WithBot ℕ) ≤ (↑(#s - 1) : WithBot ℕ)
⊢ degree.{u_1} (R := F) ((C : (a : F) → F[X]) (r i)) + (↑(#s - 1) : WithBot ℕ) ≤ (↑(#s - 1) : WithBot ℕ)

Tactic:
by_cases hr : r i = 0
-- 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 ι)
i : ι
hi : i ∈ s
hr : r i = 0
⊢ degree.{u_1} (R := F) ((C : (a : F) → F[X]) (r i)) + (↑(#s - 1) : WithBot ℕ) ≤ (↑(#s - 1) : WithBot ℕ)

Tactic:
simpa only [hr, map_zero, degree_zero, WithBot.bot_add] using bot_le

Premises used: WithBot.bot_add, map_zero, Polynomial.degree_zero, bot_le
-- 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 ι)
i : ι
hi : i ∈ s
hr : ¬r i = 0
neg : HAdd.hAdd (α := WithBot ℕ) 0 (↑(#s - 1) : WithBot ℕ) ≤ (↑(#s - 1) : WithBot ℕ)
neg₁ neg₂ : LE.le (α := WithBot ℕ) (↑(#s - 1) : WithBot ℕ) (↑(#s - 1) : WithBot ℕ)
⊢ degree.{u_1} (R := F) ((C : (a : F) → F[X]) (r i)) + (↑(#s - 1) : WithBot ℕ) ≤ (↑(#s - 1) : WithBot ℕ)

Tactic:
rw [degree_C hr, zero_add]

Premises used: Polynomial.degree_C, zero_add
-- 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 ι)
inl :
  ∀ (hvs : Set.InjOn v (↑∅ : Set ι)),
    degree.{u_1} (R := F) ((interpolate ∅ v : (a : ι → F) → F[X]) r) < (↑(card.{u_2} (α := ι) ∅) : WithBot ℕ)
inr : ∀ (h : s.Nonempty), degree.{u_1} (R := F) ((interpolate s v : (a : ι → F) → F[X]) r) < (↑(#s) : WithBot ℕ)
⊢ degree.{u_1} (R := F) ((interpolate s v : (a : ι → F) → F[X]) r) < (↑(#s) : WithBot ℕ)

Tactic:
rcases eq_empty_or_nonempty s with (rfl | h)

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
v r : ι → F
hvs : Set.InjOn v (↑∅ : Set ι)
⊢ LT.lt (α := WithBot ℕ) ⊥ (↑0 : WithBot ℕ)

Tactic:
WithBot.bot_lt_coe _

Premises used: WithBot.bot_lt_coe
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
v r : ι → F
hvs : Set.InjOn v (↑∅ : Set ι)
⊢ LT.lt (α := WithBot ℕ) ⊥ (↑0 : WithBot ℕ)

Tactic:
exact WithBot.bot_lt_coe _

Premises used: WithBot.bot_lt_coe
-- 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 ι)
h : s.Nonempty
⊢ degree.{u_1} (R := F) ((interpolate s v : (a : ι → F) → F[X]) r) < (↑(#s) : WithBot ℕ)

Tactic:
lt_of_le_of_lt (degree_interpolate_le _ hvs) ?_

Premises used: lt_of_le_of_lt, Lagrange.degree_interpolate_le
-- 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 ι)
h : s.Nonempty
inr : (↑(#s - 1) : WithBot ℕ) < (↑(#s) : WithBot ℕ)
⊢ degree.{u_1} (R := F) ((interpolate s v : (a : ι → F) → F[X]) r) < (↑(#s) : WithBot ℕ)

Tactic:
refine lt_of_le_of_lt (degree_interpolate_le _ hvs) ?_

Premises used: lt_of_le_of_lt, Lagrange.degree_interpolate_le
-- 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 ι)
h : s.Nonempty
inr : #s - 1 < #s
⊢ (↑(#s - 1) : WithBot ℕ) < (↑(#s) : WithBot ℕ)

Tactic:
rw [Nat.cast_withBot, WithBot.coe_lt_coe]

Premises used: WithBot.coe_lt_coe, Nat.cast_withBot
-- 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 ι)
h : s.Nonempty
⊢ #s - 1 < #s

Tactic:
Nat.sub_lt (Nonempty.card_pos h) zero_lt_one

Premises used: Finset.Nonempty.card_pos, Nat.sub_lt, zero_lt_one
-- 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 ι)
h : s.Nonempty
⊢ #s - 1 < #s

Tactic:
exact Nat.sub_lt (Nonempty.card_pos h) zero_lt_one

Premises used: Finset.Nonempty.card_pos, Nat.sub_lt, zero_lt_one
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
rw : degree.{u_1} (R := F) ((interpolate (s.erase i) v : (a : ι → F) → F[X]) r) < (↑(#(s.erase i)) : WithBot ℕ)
⊢ degree.{u_1} (R := F) ((interpolate (s.erase i) v : (a : ι → F) → F[X]) r) < (↑(#s - 1) : WithBot ℕ)

Tactic:
rw [← Finset.card_erase_of_mem hi]

Premises used: Finset.card_erase_of_mem
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
⊢ degree.{u_1} (R := F) ((interpolate (s.erase i) v : (a : ι → F) → F[X]) r) < (↑(#(s.erase i)) : WithBot ℕ)

Tactic:
degree_interpolate_lt _ (Set.InjOn.mono (coe_subset.mpr (erase_subset _ _)) hvs)

Premises used: Iff.mpr, Lagrange.degree_interpolate_lt, Set.InjOn.mono, Finset.erase_subset, Finset.coe_subset
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
⊢ degree.{u_1} (R := F) ((interpolate (s.erase i) v : (a : ι → F) → F[X]) r) < (↑(#(s.erase i)) : WithBot ℕ)

Tactic:
exact degree_interpolate_lt _ (Set.InjOn.mono (coe_subset.mpr (erase_subset _ _)) hvs)

Premises used: Iff.mpr, Lagrange.degree_interpolate_lt, Set.InjOn.mono, Finset.erase_subset, Finset.coe_subset
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r r' : ι → F
hvs : Set.InjOn v (↑s : Set ι)
hrr' :
  Eq.{u_1 + 1} (α := F[X]) ((interpolate s v : (a : ι → F) → F[X]) r : F[X])
    ((interpolate s v : (a : ι → F) → F[X]) r' : F[X])
x : ι
hi : x ∈ s
rw : eval (v x) ((interpolate s v : (a : ι → F) → F[X]) r) = r' x
rw₁ : eval (v x) ((interpolate s v : (a : ι → F) → F[X]) r') = r' x
rw₂ rw₃ : r' x = r' x
⊢ r x = r' x

Tactic:
rw [← eval_interpolate_at_node r hvs hi, hrr', eval_interpolate_at_node r' 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 : Finset ι
v r r' : ι → F
hrr' : ∀ i ∈ s, r i = r' i
i : ι
hi : i ∈ s
rw rw₁ :
  HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r' i) : F[X]) (Lagrange.basis s v i) =
    HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r' i) : F[X]) (Lagrange.basis s v i)
⊢ HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r i) : F[X]) (Lagrange.basis s v i) =
    HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r' i) : F[X]) (Lagrange.basis s v i)

Tactic:
rw [hrr' _ hi]
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r r' : ι → F
hvs : Set.InjOn v (↑s : Set ι)
⊢ Eq.{u_1 + 1} (α := F[X]) ((interpolate s v : (a : ι → F) → F[X]) r : F[X])
      ((interpolate s v : (a : ι → F) → F[X]) r' : F[X]) ↔
    ∀ i ∈ s, r i = r' i

Tactic:
⟨values_eq_on_of_interpolate_eq _ _ hvs, interpolate_eq_of_values_eq_on _ _⟩

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

Tactic:
eq_of_degrees_lt_of_eval_index_eq _ hvs degree_f_lt (degree_interpolate_lt _ hvs) fun _ hi =>
    (eval_interpolate_at_node (fun x ↦ eval (v x) f) hvs hi).symm

Premises used: Polynomial.eval, Lagrange.degree_interpolate_lt, Polynomial.eq_of_degrees_lt_of_eval_index_eq, Lagrange.eval_interpolate_at_node, Eq.symm
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v (↑s : Set ι)
degree_f_lt : f.degree < (↑(#s) : WithBot ℕ)
eval_f : ∀ i ∈ s, eval (v i) f = r i
rw :
  Eq.{u_1 + 1} (α := F[X]) ((interpolate s v : (a : ι → F) → F[X]) fun (i : ι) ↦ eval (v i) f : F[X])
    ((interpolate s v : (a : ι → F) → F[X]) r : F[X])
⊢ f = (interpolate s v : (a : ι → F) → F[X]) r

Tactic:
rw [eq_interpolate hvs degree_f_lt]

Premises used: Lagrange.eq_interpolate
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v (↑s : Set ι)
degree_f_lt : f.degree < (↑(#s) : WithBot ℕ)
eval_f : ∀ i ∈ s, eval (v i) f = r i
⊢ Eq.{u_1 + 1} (α := F[X]) ((interpolate s v : (a : ι → F) → F[X]) fun (i : ι) ↦ eval (v i) f : F[X])
    ((interpolate s v : (a : ι → F) → F[X]) r : F[X])

Tactic:
interpolate_eq_of_values_eq_on _ _ eval_f

Premises used: Lagrange.interpolate_eq_of_values_eq_on
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v (↑s : Set ι)
degree_f_lt : f.degree < (↑(#s) : WithBot ℕ)
eval_f : ∀ i ∈ s, eval (v i) f = r i
⊢ Eq.{u_1 + 1} (α := F[X]) ((interpolate s v : (a : ι → F) → F[X]) fun (i : ι) ↦ eval (v i) f : F[X])
    ((interpolate s v : (a : ι → F) → F[X]) r : F[X])

Tactic:
exact interpolate_eq_of_values_eq_on _ _ eval_f

Premises used: Lagrange.interpolate_eq_of_values_eq_on
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v (↑s : Set ι)
mp : (f.degree < (↑(#s) : WithBot ℕ) ∧ ∀ i ∈ s, eval (v i) f = r i) → f = (interpolate s v : (a : ι → F) → F[X]) r
mpr : f = (interpolate s v : (a : ι → F) → F[X]) r → f.degree < (↑(#s) : WithBot ℕ) ∧ ∀ i ∈ s, eval (v i) f = r i
⊢ (f.degree < (↑(#s) : WithBot ℕ) ∧ ∀ i ∈ s, eval (v i) f = r i) ↔ f = (interpolate s v : (a : ι → F) → F[X]) r

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v (↑s : Set ι)
h : f.degree < (↑(#s) : WithBot ℕ) ∧ ∀ i ∈ s, eval (v i) f = r i
⊢ f = (interpolate s v : (a : ι → F) → F[X]) r

Tactic:
eq_interpolate_of_eval_eq _ hvs h.1 h.2

Premises used: And.right, And.left, 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 : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v (↑s : Set ι)
h : f.degree < (↑(#s) : WithBot ℕ) ∧ ∀ i ∈ s, eval (v i) f = r i
⊢ f = (interpolate s v : (a : ι → F) → F[X]) r

Tactic:
exact eq_interpolate_of_eval_eq _ hvs h.1 h.2

Premises used: And.right, And.left, 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 : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v (↑s : Set ι)
h : f = (interpolate s v : (a : ι → F) → F[X]) r
mpr :
  degree.{u_1} (R := F) ((interpolate s v : (a : ι → F) → F[X]) r) < (↑(#s) : WithBot ℕ) ∧
    ∀ i ∈ s, eval (v i) ((interpolate s v : (a : ι → F) → F[X]) r) = r i
⊢ f.degree < (↑(#s) : WithBot ℕ) ∧ ∀ i ∈ s, eval (v i) f = r i

Tactic:
rw [h]
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v (↑s : Set ι)
h : f = (interpolate s v : (a : ι → F) → F[X]) r
⊢ degree.{u_1} (R := F) ((interpolate s v : (a : ι → F) → F[X]) r) < (↑(#s) : WithBot ℕ) ∧
    ∀ i ∈ s, eval (v i) ((interpolate s v : (a : ι → F) → F[X]) r) = r i

Tactic:
⟨degree_interpolate_lt _ hvs, fun _ hi => eval_interpolate_at_node _ hvs hi⟩

Premises used: Lagrange.degree_interpolate_lt, And.intro, Lagrange.eval_interpolate_at_node
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v (↑s : Set ι)
h : f = (interpolate s v : (a : ι → F) → F[X]) r
⊢ degree.{u_1} (R := F) ((interpolate s v : (a : ι → F) → F[X]) r) < (↑(#s) : WithBot ℕ) ∧
    ∀ i ∈ s, eval (v i) ((interpolate s v : (a : ι → F) → F[X]) r) = r i

Tactic:
exact ⟨degree_interpolate_lt _ hvs, fun _ hi => eval_interpolate_at_node _ hvs hi⟩
-- 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 ι)
c : F
f : ↥(degreeLT F #s)
⊢ ∀ (x : ↥s),
    eval (v (↑x : ι)) (↑(c • f) : F[X]) =
      HSMul.hSMul (α := F) (β := ↥s → F) ((RingHom.id F : (a : F) → F) c : F)
        (fun (i : ↥s) ↦ eval (v (↑i : ι)) (↑f : F[X])) x

Tactic:
simp
-- 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 : Membership.mem (γ := Submodule F F[X]) (degreeLT F #s) f
simp : ((interpolate s v : (a : ι → F) → F[X]) fun (x : ι) ↦ if x ∈ s then eval (v x) f else 0) = f
⊢ (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)))
      ((fun (f : ↥(degreeLT F #s)) (i : ↥s) ↦ eval (v (↑i : ι)) (↑f : F[X]))
        (Subtype.mk (p := fun (x : F[X]) ↦ Membership.mem (γ := Submodule F F[X]) (degreeLT F #s) x) f hf)) =
    Subtype.mk (p := fun (x : F[X]) ↦ Membership.mem (γ := Submodule F F[X]) (degreeLT F #s) x) f hf

Tactic:
simp only [Subtype.mk_eq_mk, dite_eq_ite]

Premises used: Subtype.mk_eq_mk, dite_eq_ite
-- 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 : Membership.mem (γ := Submodule F F[X]) (degreeLT F #s) f
⊢ f.degree < (↑(#s) : WithBot ℕ)

Tactic:
rw [mem_degreeLT] at hf

Premises used: Polynomial.mem_degreeLT
-- 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 ℕ)
rhs : f
| ((interpolate s v : (a : ι → F) → F[X]) fun (x : ι) ↦ if x ∈ s then eval (v x) f else 0) = f

Tactic:
rhs
-- 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 ℕ)
rw : (interpolate s v : (a : ι → F) → F[X]) fun (i : ι) ↦ eval (v i) f
| f

Tactic:
rw [eq_interpolate hvs hf]

Premises used: Lagrange.eq_interpolate
-- 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 ℕ)
rw : (interpolate s v : (a : ι → F) → F[X]) fun (i : ι) ↦ eval (v i) f
| ((interpolate s v : (a : ι → F) → F[X]) fun (x : ι) ↦ if x ∈ s then eval (v x) f else 0) = f

Tactic:
rhs; rw [eq_interpolate hvs hf]

Premises used: Lagrange.eq_interpolate
-- 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 ℕ)
conv :
  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)
⊢ ((interpolate s v : (a : ι → F) → F[X]) fun (x : ι) ↦ if x ∈ s then eval (v x) f else 0) = f

Tactic:
conv => rhs; rw [eq_interpolate hvs hf]

Premises used: Lagrange.eq_interpolate
-- 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:
interpolate_eq_of_values_eq_on _ _ fun _ hi => if_pos hi

Premises used: Lagrange.interpolate_eq_of_values_eq_on, if_pos