awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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)
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (nodal ∅ v) : R[X]) (∑ i ∈ ∅, nodal (Finset.erase ∅ i) v : R[X])
have refine_1₁ : Eq.{u_1 + 1} (α := R[X]) 0 (∑ i ∈ ∅, nodal (Finset.erase ∅ i) v)
Tactic: rw [nodal_empty, derivative_one, sum_empty]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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)
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (nodal ∅ v) : R[X]) (∑ i ∈ ∅, nodal (Finset.erase ∅ i) v : R[X])
have refine_1₂ : Eq.{u_1 + 1} (α := R[X]) 0 0
Tactic: rw [nodal_empty, derivative_one, sum_empty]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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 (α := 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])
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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)
have 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
Tactic: refine sum_congr rfl fun j hjt => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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
⊢ 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
have 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
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)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
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
⊢ 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
have 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
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)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst_1 : DecidableEq ι
i : ι
hi : i ∈ s
⊢ eval (v i) ((derivative : (a : R[X]) → R[X]) (nodal s v)) = eval (v i) (nodal (s.erase i) v)
have rw : Eq.{u_1 + 1} (α := R) (∑ x ∈ s.erase i, eval (v i) (nodal (s.erase x) v)) 0
Tactic: rw [derivative_nodal, eval_finsetSum, ← add_sum_erase _ _ hi, add_eq_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
G : Subgroup Rˣ
inst_2 : Fintype ↥G
⊢ nodal (↑G : Set Rˣ).toFinset Units.val = HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1
have h : degree.{u_1} (R := R) 1 < (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G)).degree
Tactic: have h : degree (1 : R[X]) < degree ((X : R[X]) ^ Fintype.card G) := by simp [Fintype.card_pos]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
G : Subgroup Rˣ
inst_2 : Fintype ↥G
h : degree.{u_1} (R := R) 1 < (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G)).degree
⊢ nodal (↑G : Set Rˣ).toFinset Units.val = HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1
have hvs : Set.InjOn Units.val (↑(↑G : Set Rˣ).toFinset : Set Rˣ)
Tactic: apply eq_of_degree_le_of_eval_index_eq (v := ((↑) : Rˣ → R)) (G : Set Rˣ).toFinset
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
G : Subgroup Rˣ
inst_2 : Fintype ↥G
h : degree.{u_1} (R := R) 1 < (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G)).degree
hvs : Set.InjOn Units.val (↑(↑G : Set Rˣ).toFinset : Set Rˣ)
⊢ nodal (↑G : Set Rˣ).toFinset Units.val = HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1
have h_deg_le : degree (nodal (↑G : Set Rˣ).toFinset Units.val) ≤ (↑(#(↑G : Set Rˣ).toFinset) : WithBot ℕ)
Tactic: apply eq_of_degree_le_of_eval_index_eq (v := ((↑) : Rˣ → R)) (G : Set Rˣ).toFinset
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
G : Subgroup Rˣ
inst_2 : Fintype ↥G
h : degree.{u_1} (R := R) 1 < (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G)).degree
hvs : Set.InjOn Units.val (↑(↑G : Set Rˣ).toFinset : Set Rˣ)
h_deg_le : degree (nodal (↑G : Set Rˣ).toFinset Units.val) ≤ (↑(#(↑G : Set Rˣ).toFinset) : WithBot ℕ)
⊢ nodal (↑G : Set Rˣ).toFinset Units.val = HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1
have h_deg_eq : degree (nodal (↑G : Set Rˣ).toFinset Units.val) = (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1).degree
Tactic: apply eq_of_degree_le_of_eval_index_eq (v := ((↑) : Rˣ → R)) (G : Set Rˣ).toFinset
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
G : Subgroup Rˣ
inst_2 : Fintype ↥G
h : degree.{u_1} (R := R) 1 < (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G)).degree
hvs : Set.InjOn Units.val (↑(↑G : Set Rˣ).toFinset : Set Rˣ)
h_deg_le : degree (nodal (↑G : Set Rˣ).toFinset Units.val) ≤ (↑(#(↑G : Set Rˣ).toFinset) : WithBot ℕ)
h_deg_eq :
  degree (nodal (↑G : Set Rˣ).toFinset Units.val) = (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1).degree
⊢ nodal (↑G : Set Rˣ).toFinset Units.val = HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1
have hlc : leadingCoeff (nodal (↑G : Set Rˣ).toFinset Units.val) =
  (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1).leadingCoeff
Tactic: apply eq_of_degree_le_of_eval_index_eq (v := ((↑) : Rˣ → R)) (G : Set Rˣ).toFinset
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
G : Subgroup Rˣ
inst_2 : Fintype ↥G
h : degree.{u_1} (R := R) 1 < (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G)).degree
hvs : Set.InjOn Units.val (↑(↑G : Set Rˣ).toFinset : Set Rˣ)
h_deg_le : degree (nodal (↑G : Set Rˣ).toFinset Units.val) ≤ (↑(#(↑G : Set Rˣ).toFinset) : WithBot ℕ)
h_deg_eq :
  degree (nodal (↑G : Set Rˣ).toFinset Units.val) = (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1).degree
hlc :
  leadingCoeff (nodal (↑G : Set Rˣ).toFinset Units.val) =
    (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1).leadingCoeff
⊢ nodal (↑G : Set Rˣ).toFinset Units.val = HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1
have h_eval : ∀ i ∈ (↑G : Set Rˣ).toFinset,
  eval (↑i : R) (nodal (↑G : Set Rˣ).toFinset Units.val) =
    eval (↑i : R) (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1)
Tactic: apply eq_of_degree_le_of_eval_index_eq (v := ((↑) : Rˣ → R)) (G : Set Rˣ).toFinset
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
G : Subgroup Rˣ
inst_2 : Fintype ↥G
h : degree.{u_1} (R := R) 1 < (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G)).degree
⊢ degree (nodal (↑G : Set Rˣ).toFinset Units.val) = (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1).degree
have h_deg_eq : Fintype.card.{u_1} (↑(↑G : Set Rˣ) : Type u_1) = Fintype.card.{u_1} ↥G
Tactic: rw [degree_sub_eq_left_of_degree_lt h, degree_nodal, Set.toFinset_card, degree_pow, degree_X,
      nsmul_eq_mul, mul_one, Nat.cast_inj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
G : Subgroup Rˣ
inst_2 : Fintype ↥G
h : degree.{u_1} (R := R) 1 < (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G)).degree
⊢ leadingCoeff (nodal (↑G : Set Rˣ).toFinset Units.val) =
    (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1).leadingCoeff
have hlc : 1 = (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1).leadingCoeff
Tactic: rw [nodal_monic, leadingCoeff_sub_of_degree_lt h, monic_X_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
G : Subgroup Rˣ
inst_2 : Fintype ↥G
h : degree.{u_1} (R := R) 1 < (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G)).degree
hlc : 1 = (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1).leadingCoeff
⊢ leadingCoeff (nodal (↑G : Set Rˣ).toFinset Units.val) =
    (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1).leadingCoeff
have hlc₁ : 1 = (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G)).leadingCoeff
Tactic: rw [nodal_monic, leadingCoeff_sub_of_degree_lt h, monic_X_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
G : Subgroup Rˣ
inst_2 : Fintype ↥G
h : degree.{u_1} (R := R) 1 < (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G)).degree
hlc : 1 = (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1).leadingCoeff
hlc₁ : 1 = (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G)).leadingCoeff
⊢ leadingCoeff (nodal (↑G : Set Rˣ).toFinset Units.val) =
    (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1).leadingCoeff
have hlc₂ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [nodal_monic, leadingCoeff_sub_of_degree_lt h, monic_X_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
G : Subgroup Rˣ
inst_2 : Fintype ↥G
h : degree.{u_1} (R := R) 1 < (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G)).degree
i : Rˣ
hi : i ∈ (↑G : Set Rˣ).toFinset
⊢ eval (↑i : R) (nodal (↑G : Set Rˣ).toFinset Units.val) =
    eval (↑i : R) (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1)
have h_eval : 0 = eval (↑i : R) (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1)
Tactic: rw [eval_nodal_at_node hi]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
G : Subgroup Rˣ
inst_2 : Fintype ↥G
h : degree.{u_1} (R := R) 1 < (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G)).degree
i : Rˣ
hi : i ∈ (↑G : Set Rˣ).toFinset
⊢ 0 = eval (↑i : R) (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1)
have hi₁ : i ∈ G
Tactic: replace hi : i ∈ G := by simpa using hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
G : Subgroup Rˣ
inst_2 : Fintype ↥G
h : degree.{u_1} (R := R) 1 < (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G)).degree
i : Rˣ
hi : i ∈ G
⊢ 0 = eval (↑i : R) (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1)
have h_eval : ∀ (g : ↥G) (hi : (↑g : Rˣ) ∈ G), 0 = eval (↑(↑g : Rˣ) : R) (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1)
Tactic: obtain ⟨g, rfl⟩ : ∃ g : G, g.val = i := ⟨⟨i, hi⟩, rfl⟩
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
⊢ nodalWeight s v i = (eval (v i) (nodal (s.erase i) v))⁻¹
have rw : nodalWeight s v i = (∏ i_1 ∈ s.erase i, (v i - v i_1))⁻¹
Tactic: rw [eval_nodal, nodalWeight, prod_inv_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 : Finset ι
v : ι → F
i : ι
rw : nodalWeight s v i = (∏ i_1 ∈ s.erase i, (v i - v i_1))⁻¹
⊢ nodalWeight s v i = (eval (v i) (nodal (s.erase i) v))⁻¹
have rw₁ : Eq.{u_1 + 1} (α := F) (∏ j ∈ s.erase i, (v i - v j)⁻¹) (∏ i_1 ∈ s.erase i, (v i - v i_1))⁻¹
Tactic: rw [eval_nodal, nodalWeight, prod_inv_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 : Finset ι
v : ι → F
i : ι
rw : nodalWeight s v i = (∏ i_1 ∈ s.erase i, (v i - v i_1))⁻¹
rw₁ : Eq.{u_1 + 1} (α := F) (∏ j ∈ s.erase i, (v i - v j)⁻¹) (∏ i_1 ∈ s.erase i, (v i - v i_1))⁻¹
⊢ nodalWeight s v i = (eval (v i) (nodal (s.erase i) v))⁻¹
have rw₂ : Eq.{u_1 + 1} (α := F) (∏ x ∈ s.erase i, (v i - v x))⁻¹ (∏ i_1 ∈ s.erase i, (v i - v i_1))⁻¹
Tactic: rw [eval_nodal, nodalWeight, prod_inv_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 : Finset ι
v : ι → F
i : ι
hi : i ∈ s
⊢ nodal (s.erase i) v = nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X])
have ha : HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]) ≠ 0
Tactic: rw [nodal_eq_mul_nodal_erase hi, mul_div_cancel_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
i : ι
hi : i ∈ s
⊢ nodalWeight s v i = (eval (v i) ((derivative : (a : F[X]) → F[X]) (nodal s v)))⁻¹
have rw : nodalWeight s v i = (eval (v i) (nodal (s.erase i) v))⁻¹
Tactic: rw [eval_nodal_derivative_eval_node_eq hi, nodalWeight_eq_eval_nodal_erase_inv]
-- 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 : ι
hi : i ∈ s
rw : nodalWeight s v i = (eval (v i) (nodal (s.erase i) v))⁻¹
⊢ nodalWeight s v i = (eval (v i) ((derivative : (a : F[X]) → F[X]) (nodal s v)))⁻¹
have rw₁ : (eval (v i) (nodal (s.erase i) v))⁻¹ = (eval (v i) (nodal (s.erase i) v))⁻¹
Tactic: rw [eval_nodal_derivative_eval_node_eq hi, nodalWeight_eq_eval_nodal_erase_inv]
-- 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
⊢ nodalWeight s v i ≠ 0
have rw : ∀ a ∈ s.erase i, (v i - v a)⁻¹ ≠ 0
Tactic: rw [nodalWeight, prod_ne_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
j : ι
hj : j ∈ s.erase i
⊢ (v i - v j)⁻¹ ≠ 0
have hij : j ≠ i
Tactic: rcases mem_erase.mp hj 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 : ι
hj : j ∈ s.erase i
hij : j ≠ i
⊢ (v i - v j)⁻¹ ≠ 0
have hj₁ : j ∈ s
Tactic: rcases mem_erase.mp hj 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 : ι
hi : i ∈ s
⊢ Lagrange.basis s v i =
    HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
have simp_rw : ∏ j ∈ s.erase i, basisDivisor (v i) (v j) =
  HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
    (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
Tactic: simp_rw [Lagrange.basis, basisDivisor, nodalWeight, prod_mul_distrib, map_prod, ←
    nodal_erase_eq_nodal_div hi, nodal]
-- 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 : ι
hi : i ∈ s
simp_rw :
  ∏ j ∈ s.erase i, basisDivisor (v i) (v j) =
    HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
⊢ Lagrange.basis s v i =
    HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
have simp_rw₁ : ∏ x ∈ s.erase i,
    HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (v i - v x)⁻¹ : F[X])
      (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v x) : F[X])) =
  HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
    (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
Tactic: simp_rw [Lagrange.basis, basisDivisor, nodalWeight, prod_mul_distrib, map_prod, ←
    nodal_erase_eq_nodal_div hi, nodal]
-- 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 : ι
hi : i ∈ s
simp_rw :
  ∏ j ∈ s.erase i, basisDivisor (v i) (v j) =
    HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
simp_rw₁ :
  ∏ x ∈ s.erase i,
      HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (v i - v x)⁻¹ : F[X])
        (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v x) : F[X])) =
    HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
⊢ Lagrange.basis s v i =
    HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
have simp_rw₂ : ∏ x ∈ s.erase i,
    HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (v i - v x)⁻¹ : F[X])
      (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v x) : F[X])) =
  (C : (a : F) → F[X]) (∏ j ∈ s.erase i, (v i - v j)⁻¹) *
    (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
Tactic: simp_rw [Lagrange.basis, basisDivisor, nodalWeight, prod_mul_distrib, map_prod, ←
    nodal_erase_eq_nodal_div hi, nodal]
-- 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 : ι
hi : i ∈ s
simp_rw :
  ∏ j ∈ s.erase i, basisDivisor (v i) (v j) =
    HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
simp_rw₁ :
  ∏ x ∈ s.erase i,
      HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (v i - v x)⁻¹ : F[X])
        (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v x) : F[X])) =
    HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
simp_rw₂ :
  ∏ x ∈ s.erase i,
      HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (v i - v x)⁻¹ : F[X])
        (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v x) : F[X])) =
    (C : (a : F) → F[X]) (∏ j ∈ s.erase i, (v i - v j)⁻¹) *
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
⊢ Lagrange.basis s v i =
    HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
have simp_rw₃ : HMul.hMul (α := F[X]) (∏ x ∈ s.erase i, (C : (a : F) → F[X]) (v i - v x)⁻¹)
    (∏ x ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v x) : F[X])) =
  (C : (a : F) → F[X]) (∏ j ∈ s.erase i, (v i - v j)⁻¹) *
    (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
Tactic: simp_rw [Lagrange.basis, basisDivisor, nodalWeight, prod_mul_distrib, map_prod, ←
    nodal_erase_eq_nodal_div hi, nodal]
-- 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 : ι
hi : i ∈ s
simp_rw :
  ∏ j ∈ s.erase i, basisDivisor (v i) (v j) =
    HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
simp_rw₁ :
  ∏ x ∈ s.erase i,
      HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (v i - v x)⁻¹ : F[X])
        (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v x) : F[X])) =
    HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
simp_rw₂ :
  ∏ x ∈ s.erase i,
      HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (v i - v x)⁻¹ : F[X])
        (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v x) : F[X])) =
    (C : (a : F) → F[X]) (∏ j ∈ s.erase i, (v i - v j)⁻¹) *
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
simp_rw₃ :
  HMul.hMul (α := F[X]) (∏ x ∈ s.erase i, (C : (a : F) → F[X]) (v i - v x)⁻¹)
      (∏ x ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v x) : F[X])) =
    (C : (a : F) → F[X]) (∏ j ∈ s.erase i, (v i - v j)⁻¹) *
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
⊢ Lagrange.basis s v i =
    HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
have simp_rw₄ : HMul.hMul (α := F[X]) (∏ x ∈ s.erase i, (C : (a : F) → F[X]) (v i - v x)⁻¹)
    (∏ x ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v x) : F[X])) =
  (∏ x ∈ s.erase i, (C : (a : F) → F[X]) (v i - v x)⁻¹) *
    (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
Tactic: simp_rw [Lagrange.basis, basisDivisor, nodalWeight, prod_mul_distrib, map_prod, ←
    nodal_erase_eq_nodal_div hi, nodal]