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 ι
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])
⊢ 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])
have 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)
Tactic: rw [interpolate_apply, sum_singleton, basis_singleton, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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)
⊢ 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])
have 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)
Tactic: rw [interpolate_apply, sum_singleton, basis_singleton, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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)
⊢ 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])
have rw₃ : Eq (α := F[X]) ((C : (a : F) → F[X]) (r i) : F[X]) ((C : (a : F) → F[X]) (r i) : F[X])
Tactic: rw [interpolate_apply, sum_singleton, basis_singleton, mul_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 : Finset ι
v : ι → F
hvs : Set.InjOn v (↑s : Set ι)
hs : s.Nonempty
⊢ Eq.{u_1 + 1} (α := F[X]) ((interpolate s v : (a : ι → F) → F[X]) 1) 1
have simp_rw : Eq.{u_1 + 1} (α := F[X]) (∑ x ∈ s, Lagrange.basis s v x) 1
Tactic: simp_rw [interpolate_apply, Pi.one_apply, map_one, one_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 : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
⊢ eval (v i) ((interpolate s v : (a : ι → F) → F[X]) r) = r i
have 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
Tactic: rw [interpolate_apply, eval_finsetSum, ← add_sum_erase _ _ 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 ι
i : ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
⊢ 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
have simp_rw : Eq.{u_1 + 1} (α := F) (∑ x ∈ s.erase i, r x * eval (v i) (Lagrange.basis s v x)) 0
Tactic: simp_rw [eval_mul, eval_C, eval_basis_self hvs hi, 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 : 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
have refine : ∀ (j : ι) (H : j ∈ s.erase i), r j * eval (v i) (Lagrange.basis s v j) = 0
Tactic: refine sum_eq_zero fun j 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 ι
i : ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
j : ι
H : j ∈ s.erase i
⊢ r j * eval (v i) (Lagrange.basis s v j) = 0
have rw : r j * 0 = 0
Tactic: rw [eval_basis_of_ne (mem_erase.mp H).1 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 : 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
⊢ r j * eval (v i) (Lagrange.basis s v j) = 0
have rw₁ : Eq.{u_1 + 1} (α := F) 0 0
Tactic: rw [eval_basis_of_ne (mem_erase.mp H).1 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 : 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 ℕ)
have 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 ℕ)
Tactic: refine (degree_sum_le _ _).trans ?_
-- 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 ι)
⊢ 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 ℕ)
have 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 ℕ)
Tactic: rw [Finset.sup_le_iff]
-- 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 ι)
i : ι
hi : i ∈ s
⊢ (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r i) : F[X]) (Lagrange.basis s v i)).degree ≤
    (↑(#s - 1) : WithBot ℕ)
have rw : degree.{u_1} (R := F) ((C : (a : F) → F[X]) (r i)) + (↑(#s - 1) : WithBot ℕ) ≤ (↑(#s - 1) : WithBot ℕ)
Tactic: rw [degree_mul, degree_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 r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
i : ι
hi : i ∈ s
⊢ degree.{u_1} (R := F) ((C : (a : F) → F[X]) (r i)) + (↑(#s - 1) : WithBot ℕ) ≤ (↑(#s - 1) : WithBot ℕ)
have pos : ∀ (hr : r i = 0), 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
-- 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 ι)
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 ℕ)
⊢ degree.{u_1} (R := F) ((C : (a : F) → F[X]) (r i)) + (↑(#s - 1) : WithBot ℕ) ≤ (↑(#s - 1) : WithBot ℕ)
have neg : ∀ (hr : ¬r i = 0),
  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
-- 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 ι)
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 ℕ)
have neg : HAdd.hAdd (α := WithBot ℕ) 0 (↑(#s - 1) : WithBot ℕ) ≤ (↑(#s - 1) : WithBot ℕ)
Tactic: rw [degree_C hr, 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 : 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 ℕ)
⊢ degree.{u_1} (R := F) ((C : (a : F) → F[X]) (r i)) + (↑(#s - 1) : WithBot ℕ) ≤ (↑(#s - 1) : WithBot ℕ)
have neg₁ : LE.le (α := WithBot ℕ) (↑(#s - 1) : WithBot ℕ) (↑(#s - 1) : WithBot ℕ)
Tactic: rw [degree_C hr, 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 : Finset ι
v r : ι → F
hvs : Set.InjOn v (↑s : Set ι)
⊢ degree.{u_1} (R := F) ((interpolate s v : (a : ι → F) → F[X]) r) < (↑(#s) : WithBot ℕ)
have inl : ∀ (hvs : Set.InjOn v (↑∅ : Set ι)),
  degree.{u_1} (R := F) ((interpolate ∅ v : (a : ι → F) → F[X]) r) < (↑(card.{u_2} (α := ι) ∅) : WithBot ℕ)
Tactic: rcases eq_empty_or_nonempty s with (rfl | h)
Cleared hypotheses: s, 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 ι)
inl :
  ∀ (hvs : Set.InjOn v (↑∅ : Set ι)),
    degree.{u_1} (R := F) ((interpolate ∅ v : (a : ι → F) → F[X]) r) < (↑(card.{u_2} (α := ι) ∅) : WithBot ℕ)
⊢ degree.{u_1} (R := F) ((interpolate s v : (a : ι → F) → F[X]) r) < (↑(#s) : WithBot ℕ)
have inr : ∀ (h : s.Nonempty), 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)
-- 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 ι)
h : s.Nonempty
⊢ degree.{u_1} (R := F) ((interpolate s v : (a : ι → F) → F[X]) r) < (↑(#s) : WithBot ℕ)
have inr : (↑(#s - 1) : WithBot ℕ) < (↑(#s) : WithBot ℕ)
Tactic: refine lt_of_le_of_lt (degree_interpolate_le _ 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 ι)
h : s.Nonempty
⊢ (↑(#s - 1) : WithBot ℕ) < (↑(#s) : WithBot ℕ)
have inr : #s - 1 < #s
Tactic: rw [Nat.cast_withBot, WithBot.coe_lt_coe]
-- 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 : ι
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 - 1) : WithBot ℕ)
have rw : degree.{u_1} (R := F) ((interpolate (s.erase i) v : (a : ι → F) → F[X]) r) < (↑(#(s.erase i)) : WithBot ℕ)
Tactic: rw [← Finset.card_erase_of_mem 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 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
⊢ r x = r' x
have rw : eval (v x) ((interpolate s v : (a : ι → F) → F[X]) r) = r' x
Tactic: rw [← eval_interpolate_at_node r hvs hi, hrr', eval_interpolate_at_node r' 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 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
⊢ r x = r' x
have rw₁ : eval (v x) ((interpolate s v : (a : ι → F) → F[X]) r') = r' x
Tactic: rw [← eval_interpolate_at_node r hvs hi, hrr', eval_interpolate_at_node r' 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 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
⊢ r x = r' x
have rw₂ : r' x = r' x
Tactic: rw [← eval_interpolate_at_node r hvs hi, hrr', eval_interpolate_at_node r' 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 r r' : ι → F
hrr' : ∀ i ∈ s, r i = r' i
i : ι
hi : i ∈ s
⊢ 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)
have 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)
Tactic: rw [hrr' _ 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 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
⊢ f = (interpolate s v : (a : ι → F) → F[X]) r
have 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])
Tactic: rw [eq_interpolate hvs degree_f_lt]
-- 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
f : F[X]
hvs : Set.InjOn v (↑s : Set ι)
⊢ (f.degree < (↑(#s) : WithBot ℕ) ∧ ∀ i ∈ s, eval (v i) f = r i) ↔ f = (interpolate s v : (a : ι → F) → F[X]) r
have mp : (f.degree < (↑(#s) : WithBot ℕ) ∧ ∀ i ∈ s, eval (v i) f = r i) → f = (interpolate s v : (a : ι → F) → F[X]) r
Tactic: constructor
-- 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
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
⊢ (f.degree < (↑(#s) : WithBot ℕ) ∧ ∀ i ∈ s, eval (v i) f = r i) ↔ f = (interpolate s v : (a : ι → F) → F[X]) r
have mpr : f = (interpolate s v : (a : ι → F) → F[X]) r → f.degree < (↑(#s) : WithBot ℕ) ∧ ∀ i ∈ s, eval (v i) f = r i
Tactic: constructor
-- 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
f : F[X]
hvs : Set.InjOn v (↑s : Set ι)
h : f = (interpolate s v : (a : ι → F) → F[X]) r
⊢ f.degree < (↑(#s) : WithBot ℕ) ∧ ∀ i ∈ s, eval (v i) f = r i
have 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
Tactic: rw [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 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
⊢ (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
have simp : ((interpolate s v : (a : ι → F) → F[X]) fun (x : ι) ↦ if x ∈ s then eval (v x) f else 0) = f
Tactic: simp only [Subtype.mk_eq_mk, dite_eq_ite]
-- 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 ι
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
⊢ ((interpolate s v : (a : ι → F) → F[X]) fun (x : ι) ↦ if x ∈ s then eval (v x) f else 0) = f
have hf₁ : f.degree < (↑(#s) : WithBot ℕ)
Tactic: rw [mem_degreeLT] at hf
Cleared hypotheses: hf
-- 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 ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v (↑s : Set ι)
f : F[X]
hf : f.degree < (↑(#s) : WithBot ℕ)
| ((interpolate s v : (a : ι → F) → F[X]) fun (x : ι) ↦ if x ∈ s then eval (v x) f else 0) = f
have rhs : f
Tactic: rhs
-- 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 ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v (↑s : Set ι)
f : F[X]
hf : f.degree < (↑(#s) : WithBot ℕ)
| f
have rw : (interpolate s v : (a : ι → F) → F[X]) fun (i : ι) ↦ eval (v i) f
Tactic: rw [eq_interpolate hvs hf]
-- 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 ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v (↑s : Set ι)
f : F[X]
hf : f.degree < (↑(#s) : WithBot ℕ)
| ((interpolate s v : (a : ι → F) → F[X]) fun (x : ι) ↦ if x ∈ s then eval (v x) f else 0) = f
have rw : (interpolate s v : (a : ι → F) → F[X]) fun (i : ι) ↦ eval (v i) f
Tactic: rhs; rw [eq_interpolate hvs hf]
-- 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 ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v (↑s : Set ι)
f : F[X]
hf : f.degree < (↑(#s) : WithBot ℕ)
⊢ ((interpolate s v : (a : ι → F) → F[X]) fun (x : ι) ↦ if x ∈ s then eval (v x) f else 0) = f
have 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)
Tactic: conv => rhs; rw [eq_interpolate hvs hf]
-- 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 ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v (↑s : Set ι)
f : ↥s → F
⊢ (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
have 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)
              sorry :
            ↥(degreeLT F #s)))
        f)
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) =
    f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi)
Tactic: ext ⟨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 t : Finset ι
i_1 j : ι
v r r' : ι → F
hvs : Set.InjOn v (↑s : Set ι)
f : ↥s → F
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)
have 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)
Tactic: simp only [eval_interpolate_at_node _ 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 t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs : s.Nonempty
hst : s ⊆ t
⊢ 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])
have 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])
Tactic: symm
-- 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
⊢ 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])
have 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 ℕ)
Tactic: refine eq_interpolate_of_eval_eq _ hvt (lt_of_le_of_lt (degree_sum_le _ _) ?_) fun 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 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 ℕ)
⊢ 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])
have 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
Tactic: refine eq_interpolate_of_eval_eq _ hvt (lt_of_le_of_lt (degree_sum_le _ _) ?_) fun 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 t : Finset ι
v r : ι → F
hvt : Set.InjOn v (↑t : Set ι)
hs : s.Nonempty
hst : s ⊆ t
⊢ 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 ℕ)
have 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 ℕ)
Tactic: simp_rw [Nat.cast_withBot, Finset.sup_lt_iff (WithBot.bot_lt_coe #t), degree_mul]