awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v (↑s : Set ι)
h_deg_le : f.degree ≤ (↑(#s) : WithBot ℕ)
h_deg_eq : f.degree = g.degree
hlc : f.leadingCoeff = g.leadingCoeff
h_eval : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ f = g
have inl : ∀ (h_deg_le : degree.{u_1} (R := R) 0 ≤ (↑(#s) : WithBot ℕ)) (h_deg_eq : degree.{u_1} (R := R) 0 = g.degree)
  (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ i ∈ s, eval (v i) 0 = eval (v i) g), 0 = g
Tactic: rcases eq_or_ne f 0 with rfl | hf
Cleared hypotheses: f, h_deg_le, h_deg_eq, hlc, h_eval
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v (↑s : Set ι)
h_deg_le : f.degree ≤ (↑(#s) : WithBot ℕ)
h_deg_eq : f.degree = g.degree
hlc : f.leadingCoeff = g.leadingCoeff
h_eval : ∀ i ∈ s, eval (v i) f = eval (v i) g
inl :
  ∀ (h_deg_le : degree.{u_1} (R := R) 0 ≤ (↑(#s) : WithBot ℕ)) (h_deg_eq : degree.{u_1} (R := R) 0 = g.degree)
    (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ i ∈ s, eval (v i) 0 = eval (v i) g), 0 = g
⊢ f = g
have inr : ∀ (hf : f ≠ 0), f = g
Tactic: rcases eq_or_ne f 0 with rfl | hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v (↑s : Set ι)
h_deg_le : degree.{u_1} (R := R) 0 ≤ (↑(#s) : WithBot ℕ)
h_deg_eq : degree.{u_1} (R := R) 0 = g.degree
hlc : leadingCoeff 0 = g.leadingCoeff
h_eval : ∀ i ∈ s, eval (v i) 0 = eval (v i) g
⊢ 0 = g
have inl : ∀ (h_deg_eq : ⊥ = g.degree) (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ i ∈ s, eval (v i) 0 = eval (v i) g),
  0 = g
Tactic: rwa [degree_zero, eq_comm, degree_eq_bot, eq_comm] at h_deg_eq
Cleared hypotheses: h_deg_eq, hlc, h_eval
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v (↑s : Set ι)
h_deg_le : degree.{u_1} (R := R) 0 ≤ (↑(#s) : WithBot ℕ)
h_deg_eq : degree.{u_1} (R := R) 0 = g.degree
hlc : leadingCoeff 0 = g.leadingCoeff
h_eval : ∀ i ∈ s, eval (v i) 0 = eval (v i) g
inl :
  ∀ (h_deg_eq : ⊥ = g.degree) (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ i ∈ s, eval (v i) 0 = eval (v i) g),
    0 = g
⊢ 0 = g
have inl₁ : ∀ (h_deg_eq : g.degree = ⊥) (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ i ∈ s, eval (v i) 0 = eval (v i) g),
  0 = g
Tactic: rwa [degree_zero, eq_comm, degree_eq_bot, eq_comm] at h_deg_eq
Cleared hypotheses: h_deg_eq, hlc, h_eval
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v (↑s : Set ι)
h_deg_le : degree.{u_1} (R := R) 0 ≤ (↑(#s) : WithBot ℕ)
h_deg_eq : degree.{u_1} (R := R) 0 = g.degree
hlc : leadingCoeff 0 = g.leadingCoeff
h_eval : ∀ i ∈ s, eval (v i) 0 = eval (v i) g
inl :
  ∀ (h_deg_eq : ⊥ = g.degree) (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ i ∈ s, eval (v i) 0 = eval (v i) g),
    0 = g
inl₁ :
  ∀ (h_deg_eq : g.degree = ⊥) (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ i ∈ s, eval (v i) 0 = eval (v i) g),
    0 = g
⊢ 0 = g
have inl₂ : ∀ (h_deg_eq : g = 0) (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ i ∈ s, eval (v i) 0 = eval (v i) g), 0 = g
Tactic: rwa [degree_zero, eq_comm, degree_eq_bot, eq_comm] at h_deg_eq
Cleared hypotheses: h_deg_eq, hlc, h_eval
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v (↑s : Set ι)
h_deg_le : degree.{u_1} (R := R) 0 ≤ (↑(#s) : WithBot ℕ)
h_deg_eq : degree.{u_1} (R := R) 0 = g.degree
hlc : leadingCoeff 0 = g.leadingCoeff
h_eval : ∀ i ∈ s, eval (v i) 0 = eval (v i) g
inl :
  ∀ (h_deg_eq : ⊥ = g.degree) (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ i ∈ s, eval (v i) 0 = eval (v i) g),
    0 = g
inl₁ :
  ∀ (h_deg_eq : g.degree = ⊥) (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ i ∈ s, eval (v i) 0 = eval (v i) g),
    0 = g
inl₂ :
  ∀ (h_deg_eq : g = 0) (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ i ∈ s, eval (v i) 0 = eval (v i) g), 0 = g
⊢ 0 = g
have inl₃ : ∀ (h_deg_eq : 0 = g) (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ i ∈ s, eval (v i) 0 = eval (v i) g), 0 = g
Tactic: rwa [degree_zero, eq_comm, degree_eq_bot, eq_comm] at h_deg_eq
Cleared hypotheses: h_deg_eq, hlc, h_eval
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
x y : F
⊢ Ne (α := F[X]) (basisDivisor x y) 0 ↔ x ≠ y
have rw : ¬Eq (α := F[X]) (basisDivisor x y) 0 ↔ x ≠ y
Tactic: rw [Ne, basisDivisor_eq_zero_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
x y : F
rw : ¬Eq (α := F[X]) (basisDivisor x y) 0 ↔ x ≠ y
⊢ Ne (α := F[X]) (basisDivisor x y) 0 ↔ x ≠ y
have rw₁ : ¬x = y ↔ x ≠ y
Tactic: rw [Ne, basisDivisor_eq_zero_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
x y : F
hxy : x ≠ y
⊢ degree (basisDivisor x y) = 1
have rw : (x - y)⁻¹ ≠ 0
Tactic: rw [basisDivisor, degree_mul, degree_X_sub_C, degree_C, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
x : F
⊢ degree (basisDivisor x x) = ⊥
have rw : degree.{u_1} (R := F) 0 = ⊥
Tactic: rw [basisDivisor_self, degree_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
x : F
rw : degree.{u_1} (R := F) 0 = ⊥
⊢ degree (basisDivisor x x) = ⊥
have rw₁ : Eq (α := WithBot ℕ) ⊥ ⊥
Tactic: rw [basisDivisor_self, degree_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
x : F
⊢ natDegree (basisDivisor x x) = 0
have rw : natDegree.{u_1} (R := F) 0 = 0
Tactic: rw [basisDivisor_self, natDegree_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
x : F
rw : natDegree.{u_1} (R := F) 0 = 0
⊢ natDegree (basisDivisor x x) = 0
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [basisDivisor_self, natDegree_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
x y : F
hxy : x ≠ y
⊢ eval x (basisDivisor x y) = 1
have simp : (x - y)⁻¹ * (x - y) = 1
Tactic: simp only [basisDivisor, eval_mul, eval_C, eval_sub, eval_X]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
v : ι → F
i : ι
⊢ Eq (α := F[X]) (Lagrange.basis {i} v i) 1
have rw : Eq.{u_1 + 1} (α := F[X]) (∏ j ∈ Finset.erase {i} i, basisDivisor (v i) (v j)) 1
Tactic: rw [Lagrange.basis, erase_singleton, prod_empty]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
v : ι → F
i : ι
rw : Eq.{u_1 + 1} (α := F[X]) (∏ j ∈ Finset.erase {i} i, basisDivisor (v i) (v j)) 1
⊢ Eq (α := F[X]) (Lagrange.basis {i} v i) 1
have rw₁ : Eq.{u_1 + 1} (α := F[X]) (∏ j ∈ ∅, basisDivisor (v i) (v j)) 1
Tactic: rw [Lagrange.basis, erase_singleton, prod_empty]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
v : ι → F
i : ι
rw : Eq.{u_1 + 1} (α := F[X]) (∏ j ∈ Finset.erase {i} i, basisDivisor (v i) (v j)) 1
rw₁ : Eq.{u_1 + 1} (α := F[X]) (∏ j ∈ ∅, basisDivisor (v i) (v j)) 1
⊢ Eq (α := F[X]) (Lagrange.basis {i} v i) 1
have rw₂ : Eq.{u_1 + 1} (α := F[X]) 1 1
Tactic: rw [Lagrange.basis, erase_singleton, prod_empty]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
v : ι → F
i j : ι
hij : i ≠ j
⊢ Eq (α := F[X]) (Lagrange.basis {i, j} v j) (basisDivisor (v j) (v i))
have rw : Eq (α := F[X]) (Lagrange.basis {j, i} v j) (basisDivisor (v j) (v i))
Tactic: rw [pair_comm]
-- 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
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
⊢ Ne (α := F[X]) (Lagrange.basis s v i) 0
have simp_rw : ∀ (a : ι), a ≠ i ∧ a ∈ s → ¬Eq (α := F[X]) (basisDivisor (v i) (v a)) 0
Tactic: simp_rw [Lagrange.basis, prod_ne_zero_iff, Ne, mem_erase]
-- 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
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
j : ι
hij : j ≠ i
hj : j ∈ s
⊢ ¬Eq (α := F[X]) (basisDivisor (v i) (v j)) 0
have rw : ¬i = j
Tactic: rw [basisDivisor_eq_zero_iff, hvs.eq_iff hi hj]
-- 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
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
⊢ eval (v i) (Lagrange.basis s v i) = 1
have rw : Eq.{u_1 + 1} (α := F) (∏ j ∈ s.erase i, eval (v i) (basisDivisor (v i) (v j))) 1
Tactic: rw [Lagrange.basis, eval_prod]
-- 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
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
⊢ Eq.{u_1 + 1} (α := F) (∏ j ∈ s.erase i, eval (v i) (basisDivisor (v i) (v j))) 1
have refine : ∀ (j : ι) (H : j ∈ s.erase i), eval (v i) (basisDivisor (v i) (v j)) = 1
Tactic: refine prod_eq_one 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 ι
v : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
j : ι
H : j ∈ s.erase i
⊢ eval (v i) (basisDivisor (v i) (v j)) = 1
have rw : v i ≠ v j
Tactic: rw [eval_basisDivisor_left_of_ne]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (hypothesis)
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
⊢ v i ≠ v j
have hij : j ≠ i
Tactic: rcases mem_erase.mp H with ⟨hij, hj⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (hypothesis)
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
⊢ v i ≠ v j
have hj : j ∈ s
Tactic: rcases mem_erase.mp H with ⟨hij, hj⟩
-- 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
i j : ι
hij : i ≠ j
hj : j ∈ s
⊢ eval (v j) (Lagrange.basis s v i) = 0
have simp_rw : ∃ a ∈ s.erase i, eval (v j) (basisDivisor (v i) (v a)) = 0
Tactic: simp_rw [Lagrange.basis, eval_prod, prod_eq_zero_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 : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
⊢ ∀ j ∈ s.erase i, Ne (α := F[X]) (basisDivisor (v i) (v j)) 0
have simp_rw : ∀ (j : ι), j ≠ i ∧ j ∈ s → ¬v i = v j
Tactic: simp_rw [Ne, mem_erase, basisDivisor_eq_zero_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (hypothesis)
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
⊢ natDegree (Lagrange.basis s v i) = #s - 1
have H : ∀ 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)
-- 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
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 (Lagrange.basis s v i) = #s - 1
have rw : natDegree (Lagrange.basis s v i) = ∑ x ∈ s.erase i, 1
Tactic: rw [← card_erase_of_mem hi, card_eq_sum_ones]
-- 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
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 (Lagrange.basis s v i) = ∑ x ∈ s.erase i, 1
have h : Eq (α := ℕ) (∑ x ∈ s.erase i, 1) (∑ i_1 ∈ s.erase i, natDegree (basisDivisor (v i) (v i_1)))
Tactic: convert! natDegree_prod _ _ H using 1
-- 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
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)))
have h : ∀ (j : ι) (hj : j ∈ s.erase i), v i ≠ v j
Tactic: refine sum_congr rfl fun j hj => (natDegree_basisDivisor_of_ne ?_).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 : 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
⊢ v i ≠ v j
have h : ¬Eq (α := F[X]) (basisDivisor (v i) (v j)) 0
Tactic: rw [Ne, ← basisDivisor_eq_zero_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 : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
⊢ degree (Lagrange.basis s v i) = (↑(#s - 1) : WithBot ℕ)
have rw : Eq (α := WithBot ℕ) (↑(natDegree (Lagrange.basis s v i)) : WithBot ℕ) (↑(#s - 1) : WithBot ℕ)
Tactic: rw [degree_eq_natDegree (basis_ne_zero hvs hi), natDegree_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 : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
rw : Eq (α := WithBot ℕ) (↑(natDegree (Lagrange.basis s v i)) : WithBot ℕ) (↑(#s - 1) : WithBot ℕ)
⊢ degree (Lagrange.basis s v i) = (↑(#s - 1) : WithBot ℕ)
have rw₁ : Eq (α := WithBot ℕ) (↑(#s - 1) : WithBot ℕ) (↑(#s - 1) : WithBot ℕ)
Tactic: rw [degree_eq_natDegree (basis_ne_zero hvs hi), natDegree_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 : ι → F
hvs : Set.InjOn v (↑s : Set ι)
hs : s.Nonempty
⊢ Eq.{u_1 + 1} (α := F[X]) (∑ j ∈ s, Lagrange.basis s v j) 1
have refine_1 : LT.lt (α := WithBot ℕ) (s.sup fun (b : ι) ↦ degree (Lagrange.basis s v b)) (↑(#s) : WithBot ℕ)
Tactic: refine eq_of_degrees_lt_of_eval_index_eq s hvs (lt_of_le_of_lt (degree_sum_le _ _) ?_) ?_ ?_
-- 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
refine_1 : LT.lt (α := WithBot ℕ) (s.sup fun (b : ι) ↦ degree (Lagrange.basis s v b)) (↑(#s) : WithBot ℕ)
⊢ Eq.{u_1 + 1} (α := F[X]) (∑ j ∈ s, Lagrange.basis s v j) 1
have refine_2 : degree.{u_1} (R := F) 1 < (↑(#s) : WithBot ℕ)
Tactic: refine eq_of_degrees_lt_of_eval_index_eq s hvs (lt_of_le_of_lt (degree_sum_le _ _) ?_) ?_ ?_
-- 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
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 ℕ)
⊢ Eq.{u_1 + 1} (α := F[X]) (∑ j ∈ s, Lagrange.basis s v j) 1
have refine_3 : ∀ i ∈ s, eval (v i) (∑ j ∈ s, Lagrange.basis s v j) = eval (v i) 1
Tactic: refine eq_of_degrees_lt_of_eval_index_eq s hvs (lt_of_le_of_lt (degree_sum_le _ _) ?_) ?_ ?_
-- 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
⊢ LT.lt (α := WithBot ℕ) (s.sup fun (b : ι) ↦ degree (Lagrange.basis s v b)) (↑(#s) : WithBot ℕ)
have refine_1 : ∀ b ∈ s, degree (Lagrange.basis s v b) < (↑(#s) : WithBot ℕ)
Tactic: rw [Nat.cast_withBot, Finset.sup_lt_iff (WithBot.bot_lt_coe #s)]
-- 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
i : ι
hi : i ∈ s
⊢ degree (Lagrange.basis s v i) < (↑(#s) : WithBot ℕ)
have refine_1 : #s - 1 < #s
Tactic: rw [degree_basis hvs hi, 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 ι
v : ι → F
hvs : Set.InjOn v (↑s : Set ι)
hs : s.Nonempty
⊢ degree.{u_1} (R := F) 1 < (↑(#s) : WithBot ℕ)
have refine_2 : 0 < #s
Tactic: rw [degree_one, ← WithBot.coe_zero, 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 ι
v : ι → F
hvs : Set.InjOn v (↑s : Set ι)
hs : s.Nonempty
i : ι
hi : i ∈ s
⊢ eval (v i) (∑ j ∈ s, Lagrange.basis s v j) = eval (v i) 1
have refine_3 : Eq.{u_1 + 1} (α := F) (∑ x ∈ s.erase i, eval (v i) (Lagrange.basis s v x)) 0
Tactic: rw [eval_finsetSum, eval_one, ← add_sum_erase _ _ hi, eval_basis_self hvs hi,
      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 ι
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
have refine_3 : ∀ (j : ι) (hj : j ∈ s.erase i), eval (v i) (Lagrange.basis s v j) = 0
Tactic: refine sum_eq_zero fun j hj => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (hypothesis)
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
⊢ eval (v i) (Lagrange.basis s v j) = 0
have hij : j ≠ i
Tactic: rcases mem_erase.mp hj with ⟨hij, _⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (hypothesis)
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
⊢ eval (v i) (Lagrange.basis s v j) = 0
have right : j ∈ s
Tactic: rcases mem_erase.mp hj with ⟨hij, _⟩
-- 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
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s.erase i
hij : j ≠ i
right : j ∈ s
⊢ eval (v i) (Lagrange.basis s v j) = 0
have refine_3 : Eq.{u_1 + 1} (α := F) 0 0
Tactic: rw [eval_basis_of_ne hij hi]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
x y : F
hxy : x ≠ y
⊢ HAdd.hAdd (α := F[X]) (basisDivisor x y) (basisDivisor y x) = 1
have rw : HAdd.hAdd (α := F[X]) (basisDivisor x y) (basisDivisor y x) = ∑ j ∈ {x, y}, Lagrange.basis {x, y} id j
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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
⊢ HAdd.hAdd (α := F[X]) (basisDivisor x y) (basisDivisor y x) = 1
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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)
⊢ HAdd.hAdd (α := F[X]) (basisDivisor x y) (basisDivisor y x) = 1
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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)
⊢ HAdd.hAdd (α := F[X]) (basisDivisor x y) (basisDivisor y x) = 1
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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)
⊢ HAdd.hAdd (α := F[X]) (basisDivisor x y) (basisDivisor y x) = 1
have 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))
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]