awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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))
⊢ 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 x (id y)) (basisDivisor (id y) 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]
-- 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)
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)
⊢ 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 x y) (basisDivisor y 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]
-- 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: 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]
-- 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: 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]
-- 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: 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]
-- 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: 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]
-- 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: 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]
-- 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)
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))
⊢ 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 x (id y)) (basisDivisor (id y) x)
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]
-- 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)
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)
⊢ 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 x y) (basisDivisor y x)
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]
-- 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
⊢ leadingCoeff (Lagrange.basis s v i) = (∏ j ∈ s.erase i, (v i - v j))⁻¹
have 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
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
-- 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
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
⊢ leadingCoeff (Lagrange.basis s v i) = (∏ j ∈ s.erase i, (v i - v j))⁻¹
have 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))⁻¹
Tactic: simp_rw [leadingCoeff, natDegree_basis hvs hi, Lagrange.basis]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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
⊢ ∑ 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))
have 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)))
Tactic: simp_rw [← Finset.sum_add_distrib]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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)
have 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)
Tactic: simp_rw [← add_mul, ← C_add, Pi.add_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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)
⊢ 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)
have 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)
Tactic: simp_rw [← add_mul, ← C_add, Pi.add_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (hypothesis)
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.{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)))
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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)
⊢ 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)))
have 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))
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_1 t : Finset ι
i j : ι
v_1 r r' : ι → F
s : Finset ι
v : ι → F
c : F
f : ι → F
⊢ ∑ 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))
have 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)))
Tactic: simp_rw [Finset.smul_sum, C_mul', smul_smul, Pi.smul_apply, RingHom.id_apply, smul_eq_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_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)))
⊢ ∑ 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))
have 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)))
Tactic: simp_rw [Finset.smul_sum, C_mul', smul_smul, Pi.smul_apply, RingHom.id_apply, smul_eq_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_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)))
⊢ ∑ 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))
have 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))
Tactic: simp_rw [Finset.smul_sum, C_mul', smul_smul, Pi.smul_apply, RingHom.id_apply, smul_eq_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_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))
⊢ ∑ 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))
have 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))
Tactic: simp_rw [Finset.smul_sum, C_mul', smul_smul, Pi.smul_apply, RingHom.id_apply, smul_eq_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_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))
⊢ ∑ 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))
have 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))
Tactic: simp_rw [Finset.smul_sum, C_mul', smul_smul, Pi.smul_apply, RingHom.id_apply, smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
v r : ι → F
⊢ Eq.{u_1 + 1} (α := F[X]) ((interpolate ∅ v : (a : ι → F) → F[X]) r : F[X]) (0 : F[X])
have rw : Eq.{u_1 + 1} (α := F[X])
  (∑ i ∈ ∅, HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r i) : F[X]) (Lagrange.basis ∅ v i)) 0
Tactic: rw [interpolate_apply, sum_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 r : ι → F
rw :
  Eq.{u_1 + 1} (α := F[X])
    (∑ i ∈ ∅, HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r i) : F[X]) (Lagrange.basis ∅ v i)) 0
⊢ Eq.{u_1 + 1} (α := F[X]) ((interpolate ∅ v : (a : ι → F) → F[X]) r : F[X]) (0 : F[X])
have rw₁ : Eq.{u_1 + 1} (α := F[X]) 0 0
Tactic: rw [interpolate_apply, sum_empty]
-- 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
⊢ 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])
  (∑ 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])
Tactic: rw [interpolate_apply, sum_singleton, basis_singleton, mul_one]