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 : Finset ι
v : ι → F
hvs : Set.InjOn v (↑s : Set ι)
P : F[X]
deg : ℕ
hdeg : (↑deg : WithBot ℕ) = P.degree
hP : (↑(#s) : WithBot ℕ) = (↑(deg + 1) : WithBot ℕ)
⊢ #s = deg + 1

Tactic:
replace hP : #s = deg + 1 := WithBot.coe_eq_coe.mp hP
-- 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 ι)
P : F[X]
deg : ℕ
hdeg : (↑deg : WithBot ℕ) = P.degree
hP : #s = deg + 1
⊢ deg = (↑(#s - 1) : ℕ)

Tactic:
grind
-- 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 ι)
P : F[X]
deg : ℕ
hdeg : (↑deg : WithBot ℕ) = P.degree
hP : #s = deg + 1
⊢ P.degree = (↑(#s - 1) : WithBot ℕ)

Tactic:
have hdegree : P.degree = ↑(#s - 1) := hdeg.symm.trans (WithBot.coe_eq_coe.mpr (by grind))
-- 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 ι)
P : F[X]
deg : ℕ
hdeg : (↑deg : WithBot ℕ) = P.degree
hP : #s = deg + 1
hdegree : P.degree = (↑(#s - 1) : WithBot ℕ)
rw : P.coeff (#s - 1) = ∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)
⊢ P.leadingCoeff = ∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)

Tactic:
rw [leadingCoeff, natDegree_eq_of_degree_eq_some hdegree]

Premises used: Polynomial.leadingCoeff, Polynomial.natDegree_eq_of_degree_eq_some
-- 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 ι)
P : F[X]
deg : ℕ
hdeg : (↑deg : WithBot ℕ) = P.degree
hP : #s = deg + 1
hdegree : P.degree = (↑(#s - 1) : WithBot ℕ)
rw : LT.lt (α := WithBot ℕ) (↑(#s - 1) : WithBot ℕ) (↑(#s) : WithBot ℕ)
⊢ P.degree < (↑(#s) : WithBot ℕ)

Tactic:
rw [hdegree]
-- 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 ι)
P : F[X]
deg : ℕ
hdeg : (↑deg : WithBot ℕ) = P.degree
hP : #s = deg + 1
hdegree : P.degree = (↑(#s - 1) : WithBot ℕ)
norm_cast : #s - 1 < #s
⊢ LT.lt (α := WithBot ℕ) (↑(#s - 1) : WithBot ℕ) (↑(#s) : WithBot ℕ)

Tactic:
norm_cast
-- 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 ι)
P : F[X]
deg : ℕ
hdeg : (↑deg : WithBot ℕ) = P.degree
hP : #s = deg + 1
hdegree : P.degree = (↑(#s - 1) : WithBot ℕ)
⊢ #s - 1 < #s

Tactic:
lia
-- 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 ι)
P : F[X]
deg : ℕ
hdeg : (↑deg : WithBot ℕ) = P.degree
hP : #s = deg + 1
hdegree : P.degree = (↑(#s - 1) : WithBot ℕ)
⊢ P.coeff (#s - 1) = ∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)

Tactic:
exact coeff_eq_sum hvs (by rw [hdegree]; norm_cast; lia)

Premises used: Lagrange.coeff_eq_sum
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
h : ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
i j : ι
hij : x i = x j
q : F[X]
hq : ∀ (i : ι), eval (x i) q = y i
rw : eval (x i) q = y j
rw₁ : eval (x i) q = eval (x j) q
rw₂ rw₃ : eval (x j) q = eval (x j) q
⊢ y i = y j

Tactic:
rw [← hq, ← hq, hij]
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
refine : ∀ (hwd : ∀ (i j : ι), x i = x j → y i = y j), ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
⊢ (∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i) ↔ ∀ (i j : ι), x i = x j → y i = y j

Tactic:
refine ⟨fun ⟨q, hq⟩ i j hij ↦ by rw [← hq, ← hq, hij], fun hwd ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
have : ∀ (this : Fintype ι), ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
⊢ ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i

Tactic:
have : Fintype ι := Fintype.ofFinite ι
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
⊢ Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)

Tactic:
have hinj : Set.InjOn (fun d : F ↦ d) (Finset.univ.image x) := Function.injective_id.injOn
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)
⊢ let v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0;
  v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0

Tactic:
set v : F → F := fun z ↦ if h : ∃ i, x i = z then y h.choose else 0 with v_def

Premises used: Exists, dite, Exists.choose, OfNat.ofNat, Eq
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)
v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
⊢ ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i

Tactic:
⟨Lagrange.interpolate (Finset.univ.image x) (fun d : F ↦ d) v, fun i ↦ ?_⟩

Premises used: Finset.univ, Lagrange.interpolate, Exists.intro, DFunLike.coe, Finset.image
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)
v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
refine : ∀ (i : ι), eval (x i) ((interpolate (image x univ) fun (d : F) ↦ d : (a : F → F) → F[X]) v) = y i
⊢ ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i

Tactic:
refine ⟨Lagrange.interpolate (Finset.univ.image x) (fun d : F ↦ d) v, fun i ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)
v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
i : ι
⊢ x i ∈ image x univ

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)
v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
i : ι
rw : (fun (z : F) ↦ (if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0 : F)) (x i) = y i
⊢ eval (x i) ((interpolate (image x univ) fun (d : F) ↦ d : (a : F → F) → F[X]) v) = y i

Tactic:
rw [Lagrange.eval_interpolate_at_node _ hinj (by simp), v_def]

Premises used: Lagrange.eval_interpolate_at_node
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)
v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
i : ι
pos : ∀ (h : ∃ (i_1 : ι), x i_1 = x i), y (h.choose (p := fun (i_1 : ι) ↦ x i_1 = x i)) = y i
neg : ∀ (h : ¬∃ (i_1 : ι), x i_1 = x i), 0 = y i
⊢ (if h : ∃ (i_1 : ι), x i_1 = x i then y (h.choose (p := fun (i_1 : ι) ↦ x i_1 = x i)) else 0) = y i

Tactic:
split_ifs with h
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)
v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
i : ι
h : ∃ (i_1 : ι), x i_1 = x i
⊢ y (h.choose (p := fun (i_1 : ι) ↦ x i_1 = x i)) = y i

Tactic:
hwd _ _ h.choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)
v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
i : ι
h : ∃ (i_1 : ι), x i_1 = x i
⊢ y (h.choose (p := fun (i_1 : ι) ↦ x i_1 = x i)) = y i

Tactic:
exact hwd _ _ h.choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)
v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
i : ι
h : ¬∃ (i_1 : ι), x i_1 = x i
⊢ 0 = y i

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
⊢ Eq (α := R[X]) (nodal s v) (∏ i ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X]))

Tactic:
rfl

Premises used: Lagrange.nodal, rfl
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
v : ι → R
⊢ Eq (α := R[X]) (nodal ∅ v) 1

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst_1 : Nontrivial R
simp_rw :
  natDegree.{u_1} (R := R) (∏ i ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X])) = #s
simp_rw₁ : ∑ i ∈ s, (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X])).natDegree = #s
simp_rw₂ : ∑ x ∈ s, 1 = #s
simp_rw₃ : HSMul.hSMul (β := ℕ) (#s) 1 = #s
simp_rw₄ : #s * 1 = #s
⊢ natDegree (nodal s v) = #s

Tactic:
simp_rw [nodal, natDegree_prod_of_monic (h := fun i _ => monic_X_sub_C (v i)),
    natDegree_X_sub_C, sum_const, smul_eq_mul, mul_one]

Premises used: Polynomial.monic_X_sub_C, Polynomial.natDegree_X_sub_C, Lagrange.nodal, smul_eq_mul, Polynomial.natDegree_prod_of_monic, mul_one, Finset.sum_const
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst_1 : Nontrivial R
inl : Ne (α := R[X]) (nodal ∅ v) 0
inr : ∀ (h : s.Nonempty), Ne (α := R[X]) (nodal s v) 0
⊢ Ne (α := R[X]) (nodal s v) 0

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | h)

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
v : ι → R
inst_1 : Nontrivial R
⊢ Ne (α := R[X]) (nodal ∅ v) 0

Tactic:
one_ne_zero

Premises used: Multiset.foldr, Multiset.prod, Lagrange.nodal, Finset.prod, one_ne_zero, List.foldr
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
v : ι → R
inst_1 : Nontrivial R
⊢ Ne (α := R[X]) (nodal ∅ v) 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst_1 : Nontrivial R
h : s.Nonempty
inr : 0 < natDegree (nodal s v)
⊢ Ne (α := R[X]) (nodal s v) 0

Tactic:
apply ne_zero_of_natDegree_gt (n := 0)

Premises used: Polynomial.ne_zero_of_natDegree_gt
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst_1 : Nontrivial R
h : s.Nonempty
⊢ 0 < natDegree (nodal s v)

Tactic:
simp only [natDegree_nodal, h.card_pos]

Premises used: Lagrange.natDegree_nodal, Finset.Nonempty.card_pos
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst_1 : Nontrivial R
simp_rw : Eq (α := WithBot ℕ) (↑(natDegree (nodal s v)) : WithBot ℕ) (↑(#s) : WithBot ℕ)
⊢ degree (nodal s v) = (↑(#s) : WithBot ℕ)

Tactic:
simp_rw [degree_eq_natDegree nodal_ne_zero, natDegree_nodal]

Premises used: Polynomial.degree_eq_natDegree, Lagrange.natDegree_nodal, Lagrange.nodal_ne_zero
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
⊢ Monic (nodal s v)

Tactic:
monic_prod_of_monic s (fun i ↦ X - C (v i)) fun i _ ↦ monic_X_sub_C (v i)

Premises used: Polynomial.monic_X_sub_C, Polynomial.C, HSub.hSub, Lagrange.nodal, Polynomial.monic_prod_of_monic, Polynomial.X, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
x : R
simp_rw : eval x (∏ i ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X])) = ∏ i ∈ s, (x - v i)
simp_rw₁ :
  Eq.{u_1 + 1} (α := R) (∏ j ∈ s, eval x (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v j) : R[X])))
    (∏ i ∈ s, (x - v i))
simp_rw₂ : Eq.{u_1 + 1} (α := R) (∏ x_1 ∈ s, (eval x X - eval x ((C : (a : R) → R[X]) (v x_1)))) (∏ i ∈ s, (x - v i))
simp_rw₃ : Eq.{u_1 + 1} (α := R) (∏ x_1 ∈ s, (x - eval x ((C : (a : R) → R[X]) (v x_1)))) (∏ i ∈ s, (x - v i))
⊢ eval x (nodal s v) = ∏ i ∈ s, (x - v i)

Tactic:
simp_rw [nodal, eval_prod, eval_sub, eval_X, eval_C]

Premises used: Polynomial.eval_prod, Polynomial.eval_C, Polynomial.eval_X, Lagrange.nodal, Polynomial.eval_sub
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
i : ι
hi : i ∈ s
rw : Eq.{u_1 + 1} (α := R) (∏ i_1 ∈ s, (v i - v i_1)) 0
⊢ eval (v i) (nodal s v) = 0

Tactic:
rw [eval_nodal]

Premises used: Lagrange.eval_nodal
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
i : ι
hi : i ∈ s
⊢ Eq.{u_1 + 1} (α := R) (∏ i_1 ∈ s, (v i - v i_1)) 0

Tactic:
s.prod_eq_zero hi (sub_self (v i))

Premises used: sub_self, Finset.prod_eq_zero
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
i : ι
hi : i ∈ s
⊢ Eq.{u_1 + 1} (α := R) (∏ i_1 ∈ s, (v i - v i_1)) 0

Tactic:
exact s.prod_eq_zero hi (sub_self (v i))

Premises used: Finset.prod_eq_zero
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
x : R
hx simp_rw : ∀ a ∈ s, x ≠ v a
⊢ eval x (nodal s v) ≠ 0

Tactic:
simp_rw [nodal, eval_prod, prod_ne_zero_iff, eval_sub, eval_X, eval_C, sub_ne_zero]

Premises used: Polynomial.eval_prod, Polynomial.eval_C, Polynomial.eval_X, sub_ne_zero, Finset.prod_ne_zero_iff, Lagrange.nodal, Polynomial.eval_sub
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
x : R
hx : ∀ i ∈ s, x ≠ v i
⊢ ∀ a ∈ s, x ≠ v a

Tactic:
hx
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
x : R
hx : ∀ i ∈ s, x ≠ v i
⊢ ∀ a ∈ s, x ≠ v a

Tactic:
exact hx
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
i : ι
hi : i ∈ s
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X]) ∣ nodal s v

Tactic:
⟨nodal (s.erase i) v, nodal_eq_mul_nodal_erase hi⟩

Premises used: Lagrange.nodal, Lagrange.nodal_eq_mul_nodal_erase, Exists.intro, Finset.erase
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
i : ι
hi : i ∈ s
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X]) ∣ nodal s v

Tactic:
exact ⟨nodal (s.erase i) v, nodal_eq_mul_nodal_erase hi⟩
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
i : ι
hi : i ∈ s
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X]) ∣ nodal s v

Tactic:
classical
  exact ⟨nodal (s.erase i) v, nodal_eq_mul_nodal_erase hi⟩
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst_1 : DecidableEq ι
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (nodal s v) : R[X]) (∑ i ∈ s, nodal (s.erase i) v : R[X])

Tactic:
s.induction_on ?_ fun i t hit IH => ?_

Premises used: Finset.induction_on
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst_1 : DecidableEq ι
refine_1 :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (nodal ∅ v) : R[X]) (∑ i ∈ ∅, nodal (Finset.erase ∅ i) v : R[X])
refine_2 :
  ∀ (i : ι) (t : Finset ι) (hit : i ∉ t)
    (IH : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (nodal t v) : R[X]) (∑ i ∈ t, nodal (t.erase i) v : R[X])),
    Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (nodal (insert i t) v) : R[X])
      (∑ i_1 ∈ insert i t, nodal ((insert i t).erase i_1) v : R[X])
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (nodal s v) : R[X]) (∑ i ∈ s, nodal (s.erase i) v : R[X])

Tactic:
refine s.induction_on ?_ fun i t hit IH => ?_
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst_1 : DecidableEq ι
refine_1 : Eq.{u_1 + 1} (α := R[X]) ((derivative : (a : R[X]) → R[X]) 1) (∑ i ∈ ∅, nodal (Finset.erase ∅ i) v)
refine_1₁ : Eq.{u_1 + 1} (α := R[X]) 0 (∑ i ∈ ∅, nodal (Finset.erase ∅ i) v)
refine_1₂ refine_1₃ : Eq.{u_1 + 1} (α := R[X]) 0 0
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (nodal ∅ v) : R[X]) (∑ i ∈ ∅, nodal (Finset.erase ∅ i) v : R[X])

Tactic:
rw [nodal_empty, derivative_one, sum_empty]

Premises used: Lagrange.nodal_empty, Finset.sum_empty, Polynomial.derivative_one
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst_1 : DecidableEq ι
i : ι
t : Finset ι
hit : i ∉ t
IH : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (nodal t v) : R[X]) (∑ i ∈ t, nodal (t.erase i) v : R[X])
refine_2 :
  Eq.{u_1 + 1} (α := R[X])
    (∑ i_1 ∈ t, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X]) * nodal (t.erase i_1) v)
    (∑ x ∈ t, nodal ((insert i t).erase x) v)
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (nodal (insert i t) v) : R[X])
    (∑ i_1 ∈ insert i t, nodal ((insert i t).erase i_1) v : R[X])

Tactic:
rw [nodal_insert_eq_nodal hit, derivative_mul, IH, derivative_sub, derivative_X, derivative_C,
      sub_zero, one_mul, sum_insert hit, mul_sum, erase_insert hit, add_right_inj]

Premises used: Finset.mul_sum, Polynomial.derivative_mul, Polynomial.derivative_X, Lagrange.nodal_insert_eq_nodal, sub_zero, Finset.erase_insert, Polynomial.derivative_sub, Polynomial.derivative_C, Finset.sum_insert, add_right_inj, one_mul
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst_1 : DecidableEq ι
i : ι
t : Finset ι
hit : i ∉ t
IH : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (nodal t v) : R[X]) (∑ i ∈ t, nodal (t.erase i) v : R[X])
⊢ Eq.{u_1 + 1} (α := R[X])
    (∑ i_1 ∈ t, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X]) * nodal (t.erase i_1) v)
    (∑ x ∈ t, nodal ((insert i t).erase x) v)

Tactic:
sum_congr rfl fun j hjt => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst_1 : DecidableEq ι
i : ι
t : Finset ι
hit : i ∉ t
IH : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (nodal t v) : R[X]) (∑ i ∈ t, nodal (t.erase i) v : R[X])
refine_2 :
  ∀ (j : ι) (hjt : j ∈ t),
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X]) * nodal (t.erase j) v =
      nodal ((insert i t).erase j) v
⊢ Eq.{u_1 + 1} (α := R[X])
    (∑ i_1 ∈ t, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X]) * nodal (t.erase i_1) v)
    (∑ x ∈ t, nodal ((insert i t).erase x) v)

Tactic:
refine sum_congr rfl fun j hjt => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst_1 : DecidableEq ι
i : ι
t : Finset ι
hit : i ∉ t
IH : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (nodal t v) : R[X]) (∑ i ∈ t, nodal (t.erase i) v : R[X])
j : ι
hjt : j ∈ t
refine_2 :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X]) * nodal (t.erase j) v =
    nodal (insert i (t.erase j)) v
refine_2₁ refine_2₂ :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X]) * nodal (t.erase j) v =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X]) * nodal (t.erase j) v
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X]) * nodal (t.erase j) v =
    nodal ((insert i t).erase j) v

Tactic:
rw [t.erase_insert_of_ne (ne_of_mem_of_not_mem hjt hit).symm,
      nodal_insert_eq_nodal (mem_of_mem_erase.mt hit)]

Premises used: Lagrange.nodal_insert_eq_nodal, Function.mt, Ne.symm, Finset.erase_insert_of_ne, ne_of_mem_of_not_mem, Finset.mem_of_mem_erase
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst_1 : DecidableEq ι
i : ι
hi : i ∈ s
rw : Eq.{u_1 + 1} (α := R) (∑ x ∈ s.erase i, eval (v i) (nodal (s.erase x) v)) 0
⊢ eval (v i) ((derivative : (a : R[X]) → R[X]) (nodal s v)) = eval (v i) (nodal (s.erase i) v)

Tactic:
rw [derivative_nodal, eval_finsetSum, ← add_sum_erase _ _ hi, add_eq_left]

Premises used: Lagrange.derivative_nodal, Polynomial.eval_finsetSum, Finset.add_sum_erase, add_eq_left
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst_1 : DecidableEq ι
i : ι
hi : i ∈ s
⊢ Eq.{u_1 + 1} (α := R) (∑ x ∈ s.erase i, eval (v i) (nodal (s.erase x) v)) 0

Tactic:
sum_eq_zero fun j hj => (eval_nodal_at_node (mem_erase.mpr ⟨(mem_erase.mp hj).1.symm, hi⟩))

Premises used: Iff.mpr, Lagrange.eval_nodal_at_node, Finset.sum_eq_zero, Ne.symm, Finset.mem_erase, And.left, And.intro, Iff.mp
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst_1 : DecidableEq ι
i : ι
hi : i ∈ s
⊢ Eq.{u_1 + 1} (α := R) (∑ x ∈ s.erase i, eval (v i) (nodal (s.erase x) v)) 0

Tactic:
exact sum_eq_zero fun j hj => (eval_nodal_at_node (mem_erase.mpr ⟨(mem_erase.mp hj).1.symm, hi⟩))

Premises used: Iff.mpr, Lagrange.eval_nodal_at_node, Finset.sum_eq_zero, Ne.symm, Finset.mem_erase, And.left, And.intro, Iff.mp
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
G : Subgroup Rˣ
inst_2 : Fintype ↥G
⊢ degree.{u_1} (R := R) 1 < (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G)).degree

Tactic:
simp [Fintype.card_pos]

Premises used: Fintype.card_pos