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
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
j : ι
H : j ∈ s.erase i
hij : j ≠ i
hj : j ∈ s
⊢ v i ≠ v j

Tactic:
exact mt (hvs hi hj) hij.symm

Premises used: mt, Ne.symm
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hij : i ≠ j
hj : j ∈ s
simp_rw : ∃ a ∈ s.erase i, eval (v j) (basisDivisor (v i) (v a)) = 0
⊢ eval (v j) (Lagrange.basis s v i) = 0

Tactic:
simp_rw [Lagrange.basis, eval_prod, prod_eq_zero_iff]

Premises used: Polynomial.eval_prod, Finset.prod_eq_zero_iff, Lagrange.basis
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hij : i ≠ j
hj : j ∈ s
⊢ ∃ a ∈ s.erase i, eval (v j) (basisDivisor (v i) (v a)) = 0

Tactic:
⟨j, ⟨mem_erase.mpr ⟨hij.symm, hj⟩, eval_basisDivisor_right⟩⟩

Premises used: Iff.mpr, Lagrange.eval_basisDivisor_right, Ne.symm, Finset.mem_erase, And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hij : i ≠ j
hj : j ∈ s
⊢ ∃ a ∈ s.erase i, eval (v j) (basisDivisor (v i) (v a)) = 0

Tactic:
exact ⟨j, ⟨mem_erase.mpr ⟨hij.symm, hj⟩, eval_basisDivisor_right⟩⟩
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
simp_rw : ∀ (j : ι), j ≠ i ∧ j ∈ s → ¬v i = v j
⊢ ∀ j ∈ s.erase i, Ne (α := F[X]) (basisDivisor (v i) (v j)) 0

Tactic:
simp_rw [Ne, mem_erase, basisDivisor_eq_zero_iff]

Premises used: Ne, Lagrange.basisDivisor_eq_zero_iff, Finset.mem_erase
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
⊢ ∀ (j : ι), j ≠ i ∧ j ∈ s → ¬v i = v j

Tactic:
fun j ⟨hij₁, hj⟩ hij₂ => hij₁ (hvs hj hi hij₂.symm)

Premises used: False, _private.0.Lagrange.natDegree_basis.match_1, Eq.symm, Not
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
⊢ ∀ (j : ι), j ≠ i ∧ j ∈ s → ¬v i = v j

Tactic:
exact fun j ⟨hij₁, hj⟩ hij₂ => hij₁ (hvs hj hi hij₂.symm)
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
⊢ ∀ j ∈ s.erase i, Ne (α := F[X]) (basisDivisor (v i) (v j)) 0

Tactic:
have H : ∀ j, j ∈ s.erase i → basisDivisor (v i) (v j) ≠ 0 := by
    simp_rw [Ne, mem_erase, basisDivisor_eq_zero_iff]
    exact fun j ⟨hij₁, hj⟩ hij₂ => hij₁ (hvs hj hi hij₂.symm)
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
H : ∀ j ∈ s.erase i, Ne (α := F[X]) (basisDivisor (v i) (v j)) 0
rw : natDegree (Lagrange.basis s v i) = ∑ x ∈ s.erase i, 1
⊢ natDegree (Lagrange.basis s v i) = #s - 1

Tactic:
rw [← card_erase_of_mem hi, card_eq_sum_ones]

Premises used: Finset.card_eq_sum_ones, 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 ι
v : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
H : ∀ j ∈ s.erase i, Ne (α := F[X]) (basisDivisor (v i) (v j)) 0
⊢ natDegree.{u_1} (R := F) (∏ i_1 ∈ s.erase i, basisDivisor (v i) (v i_1)) =
    ∑ i_1 ∈ s.erase i, natDegree (basisDivisor (v i) (v i_1))

Tactic:
natDegree_prod _ _ H

Premises used: Polynomial.natDegree_prod
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
H : ∀ j ∈ s.erase i, Ne (α := F[X]) (basisDivisor (v i) (v j)) 0
h : Eq (α := ℕ) (∑ x ∈ s.erase i, 1) (∑ i_1 ∈ s.erase i, natDegree (basisDivisor (v i) (v i_1)))
⊢ natDegree (Lagrange.basis s v i) = ∑ x ∈ s.erase i, 1

Tactic:
convert! natDegree_prod _ _ H using 1

Premises used: Polynomial.natDegree_prod
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
H : ∀ j ∈ s.erase i, Ne (α := F[X]) (basisDivisor (v i) (v j)) 0
⊢ Eq (α := ℕ) (∑ x ∈ s.erase i, 1) (∑ i_1 ∈ s.erase i, natDegree (basisDivisor (v i) (v i_1)))

Tactic:
sum_congr rfl fun j hj => (natDegree_basisDivisor_of_ne ?_).symm

Premises used: Lagrange.natDegree_basisDivisor_of_ne, Eq.symm, Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
H : ∀ j ∈ s.erase i, Ne (α := F[X]) (basisDivisor (v i) (v j)) 0
h : ∀ (j : ι) (hj : j ∈ s.erase i), v i ≠ v j
⊢ Eq (α := ℕ) (∑ x ∈ s.erase i, 1) (∑ i_1 ∈ s.erase i, natDegree (basisDivisor (v i) (v i_1)))

Tactic:
refine sum_congr rfl fun j hj => (natDegree_basisDivisor_of_ne ?_).symm

Premises used: Lagrange.natDegree_basisDivisor_of_ne, Eq.symm, Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
H : ∀ j ∈ s.erase i, Ne (α := F[X]) (basisDivisor (v i) (v j)) 0
j : ι
hj : j ∈ s.erase i
h : ¬Eq (α := F[X]) (basisDivisor (v i) (v j)) 0
⊢ v i ≠ v j

Tactic:
rw [Ne, ← basisDivisor_eq_zero_iff]

Premises used: Ne, Lagrange.basisDivisor_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
H : ∀ j ∈ s.erase i, Ne (α := F[X]) (basisDivisor (v i) (v j)) 0
j : ι
hj : j ∈ s.erase i
⊢ ¬Eq (α := F[X]) (basisDivisor (v i) (v j)) 0

Tactic:
H _ hj
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
H : ∀ j ∈ s.erase i, Ne (α := F[X]) (basisDivisor (v i) (v j)) 0
j : ι
hj : j ∈ s.erase i
⊢ ¬Eq (α := F[X]) (basisDivisor (v i) (v j)) 0

Tactic:
exact H _ hj
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
rw : Eq (α := WithBot ℕ) (↑(natDegree (Lagrange.basis s v i)) : WithBot ℕ) (↑(#s - 1) : WithBot ℕ)
rw₁ rw₂ : Eq (α := WithBot ℕ) (↑(#s - 1) : WithBot ℕ) (↑(#s - 1) : WithBot ℕ)
⊢ degree (Lagrange.basis s v i) = (↑(#s - 1) : WithBot ℕ)

Tactic:
rw [degree_eq_natDegree (basis_ne_zero hvs hi), natDegree_basis hvs hi]

Premises used: Polynomial.degree_eq_natDegree, Lagrange.basis_ne_zero, Lagrange.natDegree_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]) (∑ j ∈ s, Lagrange.basis s v j) 1

Tactic:
eq_of_degrees_lt_of_eval_index_eq s hvs (lt_of_le_of_lt (degree_sum_le _ _) ?_) ?_ ?_

Premises used: lt_of_le_of_lt, Polynomial.eq_of_degrees_lt_of_eval_index_eq, Polynomial.degree_sum_le
-- 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
refine_1 : LT.lt (α := WithBot ℕ) (s.sup fun (b : ι) ↦ degree (Lagrange.basis s v b)) (↑(#s) : WithBot ℕ)
refine_2 : degree.{u_1} (R := F) 1 < (↑(#s) : WithBot ℕ)
refine_3 : ∀ i ∈ s, eval (v i) (∑ j ∈ s, Lagrange.basis s v j) = eval (v i) 1
⊢ Eq.{u_1 + 1} (α := F[X]) (∑ j ∈ s, Lagrange.basis s v j) 1

Tactic:
refine eq_of_degrees_lt_of_eval_index_eq s hvs (lt_of_le_of_lt (degree_sum_le _ _) ?_) ?_ ?_

Premises used: lt_of_le_of_lt, Polynomial.eq_of_degrees_lt_of_eval_index_eq, Polynomial.degree_sum_le
-- 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
refine_1 : ∀ b ∈ s, degree (Lagrange.basis s v b) < (↑(#s) : WithBot ℕ)
⊢ LT.lt (α := WithBot ℕ) (s.sup fun (b : ι) ↦ degree (Lagrange.basis s v b)) (↑(#s) : WithBot ℕ)

Tactic:
rw [Nat.cast_withBot, Finset.sup_lt_iff (WithBot.bot_lt_coe #s)]

Premises used: Finset.sup_lt_iff, Nat.cast_withBot, WithBot.bot_lt_coe, Finset.card
-- 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
i : ι
hi : i ∈ s
refine_1 : #s - 1 < #s
⊢ degree (Lagrange.basis s v i) < (↑(#s) : WithBot ℕ)

Tactic:
rw [degree_basis hvs hi, Nat.cast_withBot, WithBot.coe_lt_coe]

Premises used: Lagrange.degree_basis, 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 : ι → F
hvs : Set.InjOn v (↑s : Set ι)
hs : s.Nonempty
i : ι
hi : i ∈ s
⊢ #s - 1 < #s

Tactic:
Nat.pred_lt (card_ne_zero_of_mem hi)

Premises used: Finset.card_ne_zero_of_mem, Nat.pred_lt, Finset.card, Multiset.card, Nat.pred
-- 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
i : ι
hi : i ∈ s
⊢ #s - 1 < #s

Tactic:
exact Nat.pred_lt (card_ne_zero_of_mem hi)

Premises used: Finset.card_ne_zero_of_mem, Nat.pred_lt
-- 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
refine_2 : 0 < #s
⊢ degree.{u_1} (R := F) 1 < (↑(#s) : WithBot ℕ)

Tactic:
rw [degree_one, ← WithBot.coe_zero, Nat.cast_withBot, WithBot.coe_lt_coe]

Premises used: Polynomial.degree_one, WithBot.coe_lt_coe, Nat.cast_withBot, WithBot.coe_zero
-- 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
⊢ 0 < #s

Tactic:
Nonempty.card_pos hs

Premises used: Finset.Nonempty.card_pos
-- 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
⊢ 0 < #s

Tactic:
exact Nonempty.card_pos hs

Premises used: Finset.Nonempty.card_pos
-- 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
i : ι
hi : i ∈ s
refine_3 : Eq.{u_1 + 1} (α := F) (∑ x ∈ s.erase i, eval (v i) (Lagrange.basis s v x)) 0
⊢ eval (v i) (∑ j ∈ s, Lagrange.basis s v j) = eval (v i) 1

Tactic:
rw [eval_finsetSum, eval_one, ← add_sum_erase _ _ hi, eval_basis_self hvs hi,
      add_eq_left]

Premises used: Polynomial.eval_finsetSum, Finset.add_sum_erase, add_eq_left, Polynomial.eval_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 ι
v : ι → F
hvs : Set.InjOn v (↑s : Set ι)
hs : s.Nonempty
i : ι
hi : i ∈ s
⊢ Eq.{u_1 + 1} (α := F) (∑ x ∈ s.erase i, 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 : Finset ι
v : ι → F
hvs : Set.InjOn v (↑s : Set ι)
hs : s.Nonempty
i : ι
hi : i ∈ s
refine_3 : ∀ (j : ι) (hj : j ∈ s.erase i), eval (v i) (Lagrange.basis s v j) = 0
⊢ Eq.{u_1 + 1} (α := F) (∑ x ∈ s.erase i, 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 : Finset ι
v : ι → F
hvs : Set.InjOn v (↑s : Set ι)
hs : s.Nonempty
i : ι
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 : Finset ι
v : ι → F
hvs : Set.InjOn v (↑s : Set ι)
hs : s.Nonempty
i : ι
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 : Finset ι
v : ι → F
hvs : Set.InjOn v (↑s : Set ι)
hs : s.Nonempty
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s.erase i
hij : j ≠ i
right : j ∈ s
refine_3 refine_3₁ : Eq.{u_1 + 1} (α := F) 0 0
⊢ eval (v i) (Lagrange.basis s v j) = 0

Tactic:
rw [eval_basis_of_ne hij hi]

Premises used: Lagrange.eval_basis_of_ne
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
x y : F
hxy : x ≠ y
rw : HAdd.hAdd (α := F[X]) (basisDivisor x y) (basisDivisor y x) = ∑ j ∈ {x, y}, Lagrange.basis {x, y} id j
rw₁ :
  HAdd.hAdd (α := F[X]) (basisDivisor x y) (basisDivisor y x) =
    HAdd.hAdd (α := F[X]) (Lagrange.basis {x, y} id x) (∑ x_1 ∈ {y}, Lagrange.basis {x, y} id x_1)
rw₂ :
  HAdd.hAdd (α := F[X]) (basisDivisor x y) (basisDivisor y x) =
    HAdd.hAdd (α := F[X]) (Lagrange.basis {x, y} id x) (Lagrange.basis {x, y} id y)
rw₃ :
  HAdd.hAdd (α := F[X]) (basisDivisor x y) (basisDivisor y x) =
    HAdd.hAdd (α := F[X]) (basisDivisor (id x) (id y)) (Lagrange.basis {x, y} id y)
rw₄ :
  HAdd.hAdd (α := F[X]) (basisDivisor x y) (basisDivisor y x) =
    HAdd.hAdd (α := F[X]) (basisDivisor (id x) (id y)) (basisDivisor (id y) (id x))
rw₅ :
  HAdd.hAdd (α := F[X]) (basisDivisor x y) (basisDivisor y x) =
    HAdd.hAdd (α := F[X]) (basisDivisor x (id y)) (basisDivisor (id y) x)
rw₆ rw₇ :
  HAdd.hAdd (α := F[X]) (basisDivisor x y) (basisDivisor y x) =
    HAdd.hAdd (α := F[X]) (basisDivisor x y) (basisDivisor y x)
⊢ HAdd.hAdd (α := F[X]) (basisDivisor x y) (basisDivisor y x) = 1

Tactic:
rw [← sum_basis Function.injective_id.injOn ⟨x, mem_insert_self _ {y}⟩,
    sum_insert (notMem_singleton.mpr hxy), sum_singleton, basis_pair_left hxy,
    basis_pair_right hxy, id, id]

Premises used: Finset.notMem_singleton, Iff.mpr, Lagrange.basis_pair_right, Finset.mem_insert_self, Function.Injective.injOn, id, Function.injective_id, Finset.sum_singleton, Exists.intro, Lagrange.sum_basis, Finset.sum_insert, Singleton.singleton, Lagrange.basis_pair_left
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
x y : F
hxy : x ≠ y
rw : HAdd.hAdd (α := F[X]) (basisDivisor x y) (basisDivisor y x) = ∑ j ∈ {x, y}, Lagrange.basis {x, y} id j
rw₁ :
  HAdd.hAdd (α := F[X]) (basisDivisor x y) (basisDivisor y x) =
    HAdd.hAdd (α := F[X]) (Lagrange.basis {x, y} id x) (∑ x_1 ∈ {y}, Lagrange.basis {x, y} id x_1)
rw₂ :
  HAdd.hAdd (α := F[X]) (basisDivisor x y) (basisDivisor y x) =
    HAdd.hAdd (α := F[X]) (Lagrange.basis {x, y} id x) (Lagrange.basis {x, y} id y)
rw₃ :
  HAdd.hAdd (α := F[X]) (basisDivisor x y) (basisDivisor y x) =
    HAdd.hAdd (α := F[X]) (basisDivisor (id x) (id y)) (Lagrange.basis {x, y} id y)
rw₄ :
  HAdd.hAdd (α := F[X]) (basisDivisor x y) (basisDivisor y x) =
    HAdd.hAdd (α := F[X]) (basisDivisor (id x) (id y)) (basisDivisor (id y) (id x))
rw₅ :
  HAdd.hAdd (α := F[X]) (basisDivisor x y) (basisDivisor y x) =
    HAdd.hAdd (α := F[X]) (basisDivisor x (id y)) (basisDivisor (id y) x)
rw₆ rw₇ :
  HAdd.hAdd (α := F[X]) (basisDivisor x y) (basisDivisor y x) =
    HAdd.hAdd (α := F[X]) (basisDivisor x y) (basisDivisor y x)
⊢ HAdd.hAdd (α := F[X]) (basisDivisor x y) (basisDivisor y x) = 1

Tactic:
classical
  rw [← sum_basis Function.injective_id.injOn ⟨x, mem_insert_self _ {y}⟩,
    sum_insert (notMem_singleton.mpr hxy), sum_singleton, basis_pair_left hxy,
    basis_pair_right hxy, id, id]

Premises used: id, Finset.sum_singleton
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
⊢ Eq.{u_1 + 1} (α := F)
    (coeff (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X])) (#s - 1)) 1

Tactic:
simpa [hi] using (monic_prod_X_sub_C v (s.erase i)).coeff_natDegree

Premises used: Polynomial.Monic.coeff_natDegree, Finset.erase, Polynomial.monic_prod_X_sub_C
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
⊢ Eq.{u_1 + 1} (α := F)
    (coeff (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X])) (#s - 1)) 1

Tactic:
have : (∏ j ∈ s.erase i, (X - C (v j))).coeff (#s - 1) = 1 := by
    simpa [hi] using (monic_prod_X_sub_C v (s.erase i)).coeff_natDegree
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
this :
  Eq.{u_1 + 1} (α := F)
    (coeff (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X])) (#s - 1)) 1
simp_rw :
  Eq.{u_1 + 1} (α := F) (coeff (∏ j ∈ s.erase i, basisDivisor (v i) (v j)) (#s - 1)) (∏ j ∈ s.erase i, (v i - v j))⁻¹
⊢ leadingCoeff (Lagrange.basis s v i) = (∏ j ∈ s.erase i, (v i - v j))⁻¹

Tactic:
simp_rw [leadingCoeff, natDegree_basis hvs hi, Lagrange.basis]

Premises used: Polynomial.leadingCoeff, Lagrange.basis, Lagrange.natDegree_basis
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
this :
  Eq.{u_1 + 1} (α := F)
    (coeff (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X])) (#s - 1)) 1
⊢ Eq.{u_1 + 1} (α := F) (coeff (∏ j ∈ s.erase i, basisDivisor (v i) (v j)) (#s - 1)) (∏ j ∈ s.erase i, (v i - v j))⁻¹

Tactic:
simp [basisDivisor, Finset.prod_mul_distrib, ← map_prod, this]

Premises used: Finset.prod_mul_distrib, map_prod, Lagrange.basisDivisor
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s_1 t : Finset ι
i j : ι
v_1 r r' : ι → F
s : Finset ι
v f g : ι → F
simp_rw :
  Eq.{u_1 + 1} (α := F[X]) (∑ i ∈ s, HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) ((f + g) i)) (Lagrange.basis s v i))
    (∑ x ∈ s,
      (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (f x) : F[X]) (Lagrange.basis s v x) +
        HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (g x) : F[X]) (Lagrange.basis s v x)))
⊢ ∑ i ∈ s, HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) ((f + g) i)) (Lagrange.basis s v i) =
    HAdd.hAdd (α := F[X])
      (∑ i ∈ s, HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (f i) : F[X]) (Lagrange.basis s v i))
      (∑ i ∈ s, HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (g i) : F[X]) (Lagrange.basis s v i))

Tactic:
simp_rw [← Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s_1 t : Finset ι
i j : ι
v_1 r r' : ι → F
s : Finset ι
v f g : ι → F
simp_rw :
  Eq (α := (x : ι) → F[X])
    (fun (x : ι) ↦
      HAdd.hAdd (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (f x) : F[X]) ((C : (a : F) → F[X]) (g x) : F[X]) *
        Lagrange.basis s v x)
    fun (x : ι) ↦ HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) ((f + g) x)) (Lagrange.basis s v x)
simp_rw₁ :
  Eq (α := (x : ι) → F[X])
    (fun (x : ι) ↦ HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (f x + g x) : F[X]) (Lagrange.basis s v x))
    fun (x : ι) ↦ HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) ((f + g) x)) (Lagrange.basis s v x)
⊢ Eq (α := (x : ι) → F[X])
    (fun (x : ι) ↦
      HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (f x) : F[X]) (Lagrange.basis s v x) +
        HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (g x) : F[X]) (Lagrange.basis s v x))
    fun (x : ι) ↦ HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) ((f + g) x)) (Lagrange.basis s v x)

Tactic:
simp_rw [← add_mul, ← C_add, Pi.add_apply]

Premises used: add_mul, Pi.add_apply, Polynomial.C_add
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s_1 t : Finset ι
i j : ι
v_1 r r' : ι → F
s : Finset ι
v f g : ι → F
⊢ Eq (α := (x : ι) → F[X])
    (fun (x : ι) ↦
      HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (f x) : F[X]) (Lagrange.basis s v x) +
        HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (g x) : F[X]) (Lagrange.basis s v x))
    fun (x : ι) ↦ HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) ((f + g) x)) (Lagrange.basis s v x)

Tactic:
have h : (fun x => C (f x) * Lagrange.basis s v x + C (g x) * Lagrange.basis s v x) =
    (fun x => C ((f + g) x) * Lagrange.basis s v x) := by
      simp_rw [← add_mul, ← C_add, Pi.add_apply]
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s_1 t : Finset ι
i j : ι
v_1 r r' : ι → F
s : Finset ι
v f g : ι → F
h :
  Eq (α := (x : ι) → F[X])
    (fun (x : ι) ↦
      HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (f x) : F[X]) (Lagrange.basis s v x) +
        HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (g x) : F[X]) (Lagrange.basis s v x))
    fun (x : ι) ↦ HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) ((f + g) x)) (Lagrange.basis s v x)
rw rw₁ :
  Eq.{u_1 + 1} (α := F[X]) (∑ i ∈ s, HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) ((f + g) i)) (Lagrange.basis s v i))
    (∑ x ∈ s, HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) ((f + g) x)) (Lagrange.basis s v x))
⊢ Eq.{u_1 + 1} (α := F[X]) (∑ i ∈ s, HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) ((f + g) i)) (Lagrange.basis s v i))
    (∑ x ∈ s,
      (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (f x) : F[X]) (Lagrange.basis s v x) +
        HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (g x) : F[X]) (Lagrange.basis s v x)))

Tactic:
rw [h]
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s_1 t : Finset ι
i j : ι
v_1 r r' : ι → F
s : Finset ι
v : ι → F
c : F
f : ι → F
simp_rw :
  Eq.{u_1 + 1} (α := F[X]) (∑ i ∈ s, HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) ((c • f) i)) (Lagrange.basis s v i))
    (∑ x ∈ s,
      HSMul.hSMul (α := F) ((RingHom.id F : (a : F) → F) c : F)
        (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (f x) : F[X]) (Lagrange.basis s v x)))
simp_rw₁ :
  Eq.{u_1 + 1} (α := F[X]) (∑ x ∈ s, HSMul.hSMul (β := F[X]) ((c • f) x) (Lagrange.basis s v x))
    (∑ x ∈ s,
      HSMul.hSMul (α := F) ((RingHom.id F : (a : F) → F) c : F) (HSMul.hSMul (β := F[X]) (f x) (Lagrange.basis s v x)))
simp_rw₂ :
  Eq.{u_1 + 1} (α := F[X]) (∑ x ∈ s, HSMul.hSMul (β := F[X]) ((c • f) x) (Lagrange.basis s v x))
    (∑ x ∈ s,
      HSMul.hSMul (β := F[X]) (HMul.hMul (α := F) ((RingHom.id F : (a : F) → F) c : F) (f x)) (Lagrange.basis s v x))
simp_rw₃ :
  Eq.{u_1 + 1} (α := F[X]) (∑ x ∈ s, HSMul.hSMul (β := F[X]) (c • f x) (Lagrange.basis s v x))
    (∑ x ∈ s,
      HSMul.hSMul (β := F[X]) (HMul.hMul (α := F) ((RingHom.id F : (a : F) → F) c : F) (f x)) (Lagrange.basis s v x))
simp_rw₄ :
  Eq.{u_1 + 1} (α := F[X]) (∑ x ∈ s, HSMul.hSMul (β := F[X]) (c • f x) (Lagrange.basis s v x))
    (∑ x ∈ s, HSMul.hSMul (β := F[X]) (c * f x) (Lagrange.basis s v x))
⊢ ∑ i ∈ s, HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) ((c • f) i)) (Lagrange.basis s v i) =
    HSMul.hSMul (α := F) (β := F[X]) ((RingHom.id F : (a : F) → F) c : F)
      (∑ i ∈ s, HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (f i) : F[X]) (Lagrange.basis s v i))

Tactic:
simp_rw [Finset.smul_sum, C_mul', smul_smul, Pi.smul_apply, RingHom.id_apply, smul_eq_mul]

Premises used: RingHom.id_apply, Polynomial.C_mul', smul_smul, Finset.smul_sum, smul_eq_mul, Pi.smul_apply