awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
G : Subgroup Rˣ
inst_2 : Fintype ↥G
⊢ degree.{u_1} (R := R) 1 < (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G)).degree

Tactic:
have h : degree (1 : R[X]) < degree ((X : R[X]) ^ Fintype.card G) := by simp [Fintype.card_pos]
-- Module: Mathlib.LinearAlgebra.Lagrange
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
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)
⊢ nodal (↑G : Set Rˣ).toFinset Units.val = 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

Premises used: Set.toFinset, SetLike.coe, Polynomial.eq_of_degree_le_of_eval_index_eq
-- Module: Mathlib.LinearAlgebra.Lagrange
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
⊢ Set.InjOn Units.val (↑(↑G : Set Rˣ).toFinset : Set Rˣ)

Tactic:
Units.val_injective.injOn

Premises used: Function.Injective.injOn, Units.val_injective
-- Module: Mathlib.LinearAlgebra.Lagrange
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
⊢ Set.InjOn Units.val (↑(↑G : Set Rˣ).toFinset : Set Rˣ)

Tactic:
exact Units.val_injective.injOn

Premises used: Function.Injective.injOn, Units.val_injective
-- Module: Mathlib.LinearAlgebra.Lagrange
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) ≤ (↑(#(↑G : Set Rˣ).toFinset) : WithBot ℕ)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Lagrange
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
h_deg_eq : Fintype.card.{u_1} (↑(↑G : Set Rˣ) : Type u_1) = Fintype.card.{u_1} ↥G
⊢ degree (nodal (↑G : Set Rˣ).toFinset Units.val) = (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1).degree

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]

Premises used: Polynomial.degree_pow, Lagrange.degree_nodal, Nat.cast_inj, Set.toFinset_card, Polynomial.degree_X, Polynomial.degree_sub_eq_left_of_degree_lt, nsmul_eq_mul, mul_one
-- Module: Mathlib.LinearAlgebra.Lagrange
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
⊢ Fintype.card.{u_1} (↑(↑G : Set Rˣ) : Type u_1) = Fintype.card.{u_1} ↥G

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Lagrange
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
⊢ Fintype.card.{u_1} (↑(↑G : Set Rˣ) : Type u_1) = Fintype.card.{u_1} ↥G

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Lagrange
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
hlc₂ hlc₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ leadingCoeff (nodal (↑G : Set Rˣ).toFinset Units.val) =
    (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]

Premises used: Polynomial.monic_X_pow, Polynomial.leadingCoeff_sub_of_degree_lt, Lagrange.nodal_monic
-- Module: Mathlib.LinearAlgebra.Lagrange
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
h_eval : 0 = eval (↑i : R) (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1)
⊢ 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:
rw [eval_nodal_at_node hi]

Premises used: Lagrange.eval_nodal_at_node
-- Module: Mathlib.LinearAlgebra.Lagrange
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
⊢ i ∈ G

Tactic:
simpa using hi
-- Module: Mathlib.LinearAlgebra.Lagrange
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
⊢ i ∈ G

Tactic:
replace hi : i ∈ G := by simpa using hi
-- Module: Mathlib.LinearAlgebra.Lagrange
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
⊢ ∃ (g : ↥G), (↑g : Rˣ) = i

Tactic:
⟨⟨i, hi⟩, rfl⟩

Premises used: Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.LinearAlgebra.Lagrange
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
h_eval :
  ∀ (g : ↥G) (hi : (↑g : Rˣ) ∈ G), 0 = eval (↑(↑g : Rˣ) : R) (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1)
⊢ 0 = eval (↑i : R) (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1)

Tactic:
obtain ⟨g, rfl⟩ : ∃ g : G, g.val = i := ⟨⟨i, hi⟩, rfl⟩

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Lagrange
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
g : ↥G
hi : (↑g : Rˣ) ∈ G
⊢ 0 = eval (↑(↑g : Rˣ) : R) (HPow.hPow (α := R[X]) X (Fintype.card.{u_1} ↥G) - 1)

Tactic:
simp [← Units.val_pow_eq_pow_val, ← Subgroup.coe_pow G]

Premises used: Subgroup.coe_pow, Units.val_pow_eq_pow_val
-- Module: Mathlib.LinearAlgebra.Lagrange
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))⁻¹
rw₂ rw₃ : Eq.{u_1 + 1} (α := F) (∏ x ∈ s.erase i, (v i - v x))⁻¹ (∏ i_1 ∈ s.erase i, (v i - v i_1))⁻¹
⊢ nodalWeight s v i = (eval (v i) (nodal (s.erase i) v))⁻¹

Tactic:
rw [eval_nodal, nodalWeight, prod_inv_distrib]

Premises used: Lagrange.eval_nodal, Finset.prod_inv_distrib, Lagrange.nodalWeight
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hi : i ∈ s
ha : HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]) ≠ 0
⊢ nodal (s.erase i) v = nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X])

Tactic:
rw [nodal_eq_mul_nodal_erase hi, mul_div_cancel_left₀]

Premises used: mul_div_cancel_left₀, Lagrange.nodal_eq_mul_nodal_erase
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hi : i ∈ s
⊢ HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]) ≠ 0

Tactic:
X_sub_C_ne_zero _

Premises used: Polynomial.X_sub_C_ne_zero
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hi : i ∈ s
⊢ HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]) ≠ 0

Tactic:
exact X_sub_C_ne_zero _

Premises used: Polynomial.X_sub_C_ne_zero
-- Module: Mathlib.LinearAlgebra.Lagrange
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))⁻¹
rw₁ rw₂ : (eval (v i) (nodal (s.erase i) v))⁻¹ = (eval (v i) (nodal (s.erase i) v))⁻¹
⊢ nodalWeight s v i = (eval (v i) ((derivative : (a : F[X]) → F[X]) (nodal s v)))⁻¹

Tactic:
rw [eval_nodal_derivative_eval_node_eq hi, nodalWeight_eq_eval_nodal_erase_inv]

Premises used: Lagrange.nodalWeight_eq_eval_nodal_erase_inv, Lagrange.eval_nodal_derivative_eval_node_eq
-- 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 : ∀ a ∈ s.erase i, (v i - v a)⁻¹ ≠ 0
⊢ nodalWeight s v i ≠ 0

Tactic:
rw [nodalWeight, prod_ne_zero_iff]

Premises used: Finset.prod_ne_zero_iff, Lagrange.nodalWeight
-- 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 : ι
hj : j ∈ s.erase i
⊢ j ≠ i

Tactic:
rcases mem_erase.mp hj with ⟨hij, hj⟩

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

Tactic:
rcases mem_erase.mp hj with ⟨hij, hj⟩

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

Tactic:
inv_ne_zero (sub_ne_zero_of_ne (mt (hvs.eq_iff hi hj).mp hij.symm))

Premises used: Set.InjOn.eq_iff, mt, Ne.symm, sub_ne_zero_of_ne, Iff.mp, inv_ne_zero
-- 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 : ι
hj_1 : j ∈ s.erase i
hij : j ≠ i
hj : j ∈ s
⊢ (v i - v j)⁻¹ ≠ 0

Tactic:
exact inv_ne_zero (sub_ne_zero_of_ne (mt (hvs.eq_iff hi hj).mp hij.symm))

Premises used: Set.InjOn.eq_iff, mt, Ne.symm, sub_ne_zero_of_ne, Iff.mp, inv_ne_zero
-- Module: Mathlib.LinearAlgebra.Lagrange
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]))
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]))
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])) =
    HMul.hMul (α := F[X]) (∏ x ∈ s.erase i, (C : (a : F) → F[X]) (v i - v x)⁻¹) (nodal (s.erase i) v)
⊢ 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]))

Tactic:
simp_rw [Lagrange.basis, basisDivisor, nodalWeight, prod_mul_distrib, map_prod, ←
    nodal_erase_eq_nodal_div hi, nodal]

Premises used: Finset.prod_mul_distrib, Lagrange.nodalWeight, map_prod, Lagrange.nodal, Lagrange.basis, Lagrange.basisDivisor, Lagrange.nodal_erase_eq_nodal_div
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
x : F
hi : i ∈ s
hxi : x ≠ v i
rw : eval x (Lagrange.basis s v i) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₁ :
  eval 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]))) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₂ :
  eval x ((C : (a : F) → F[X]) (nodalWeight s v i)) *
      eval x (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X])) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₃ :
  nodalWeight s v i * eval x (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X])) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₄ : nodalWeight s v i * eval x (nodal (s.erase i) v) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₅ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₆ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * (x - v i)⁻¹ * ∏ i ∈ s, (x - v i)
rw₇ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * ((x - v i)⁻¹ * ∏ i ∈ s, (x - v i))
rw₈ :
  nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) =
    nodalWeight s v i * ((x - v i)⁻¹ * ((x - v i) * ∏ x_1 ∈ s.erase i, (x - v x_1)))
rw₉ :
  nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) =
    nodalWeight s v i * ((x - v i)⁻¹ * (x - v i) * ∏ x_1 ∈ s.erase i, (x - v x_1))
rw₁₀ :
  nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) =
    nodalWeight s v i * HMul.hMul (α := F) 1 (∏ x_1 ∈ s.erase i, (x - v x_1))
rw₁₁ rw₁₂ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * ∏ x_1 ∈ s.erase i, (x - v x_1)
⊢ eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹)

Tactic:
rw [mul_comm, basis_eq_prod_sub_inv_mul_nodal_div hi, eval_mul, eval_C, ←
    nodal_erase_eq_nodal_div hi, eval_nodal, eval_nodal, mul_assoc, ← mul_prod_erase _ _ hi, ←
    mul_assoc (x - v i)⁻¹, inv_mul_cancel₀ (sub_ne_zero_of_ne hxi), one_mul]

Premises used: Polynomial.eval_C, mul_assoc, HSub.hSub, Lagrange.basis_eq_prod_sub_inv_mul_nodal_div, Lagrange.eval_nodal, Polynomial.eval_mul, Finset.mul_prod_erase, Inv.inv, sub_ne_zero_of_ne, mul_comm, inv_mul_cancel₀, Lagrange.nodal_erase_eq_nodal_div, one_mul
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
j : ι
hj : j ∈ s
rw :
  HMul.hMul (α := F[X]) (β := F[X]) (Lagrange.basis s v j) ((C : (a : F) → F[X]) (r j) : F[X]) =
    HMul.hMul (β := F[X])
      (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v j) : F[X])
        (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X])))
      ((C : (a : F) → F[X]) (r j) : F[X])
rw₁ rw₂ :
  HMul.hMul (β := F[X])
      (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v j) : F[X])
        (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X])))
      ((C : (a : F) → F[X]) (r j) : F[X]) =
    HMul.hMul (β := F[X])
      (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v j) : F[X])
        (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X])))
      ((C : (a : F) → F[X]) (r j) : F[X])
⊢ HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r j) : F[X]) (Lagrange.basis s v j) =
    HMul.hMul (β := F[X])
      (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v j) : F[X])
        (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X])))
      ((C : (a : F) → F[X]) (r j) : F[X])

Tactic:
rw [mul_comm, basis_eq_prod_sub_inv_mul_nodal_div hj]

Premises used: Lagrange.basis_eq_prod_sub_inv_mul_nodal_div, mul_comm
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
x : F
hx : ∀ i ∈ s, x ≠ v i
simp_rw :
  Eq.{u_1 + 1} (α := F) (∑ x_1 ∈ s, r x_1 * eval x (Lagrange.basis s v x_1))
    (∑ i ∈ s, eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹ * r i))
⊢ eval x ((interpolate s v : (a : ι → F) → F[X]) r) =
    eval x (nodal s v) * ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i

Tactic:
simp_rw [interpolate_apply, mul_sum, eval_finsetSum, eval_mul, eval_C]

Premises used: Finset.mul_sum, Polynomial.eval_C, Polynomial.eval_mul, Polynomial.eval_finsetSum, Lagrange.interpolate_apply
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
x : F
hx : ∀ i ∈ s, x ≠ v i
⊢ Eq.{u_1 + 1} (α := F) (∑ x_1 ∈ s, r x_1 * eval x (Lagrange.basis s v x_1))
    (∑ i ∈ s, eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹ * r i))

Tactic:
sum_congr rfl fun i hi => ?_

Premises used: 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 r : ι → F
x : F
hx : ∀ i ∈ s, x ≠ v i
refine :
  ∀ (i : ι) (hi : i ∈ s),
    r i * eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹ * r i)
⊢ Eq.{u_1 + 1} (α := F) (∑ x_1 ∈ s, r x_1 * eval x (Lagrange.basis s v x_1))
    (∑ i ∈ s, eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹ * r i))

Tactic:
refine sum_congr rfl fun i hi => ?_

Premises used: 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 r : ι → F
x : F
hx : ∀ i ∈ s, x ≠ v i
i : ι
hi : i ∈ s
rw : r i * eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹) * r i
rw₁ : eval x (Lagrange.basis s v i) * r i = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹) * r i
rw₂ rw₃ :
  eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹) * r i =
    eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹) * r i
⊢ r i * eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹ * r i)

Tactic:
rw [← mul_assoc, mul_comm, eval_basis_not_at_node hi (hx _ hi)]

Premises used: mul_assoc, mul_comm, Lagrange.eval_basis_not_at_node
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
x : F
hvs : Set.InjOn v (↑s : Set ι)
hx : ∀ i ∈ s, x ≠ v i
hs : s.Nonempty
⊢ eval x (nodal s v) * ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ = 1

Tactic:
simpa only [Pi.one_apply, interpolate_one hvs hs, eval_one, mul_one] using
      (eval_interpolate_not_at_node 1 hx).symm

Premises used: Lagrange.interpolate_one, Lagrange.eval_interpolate_not_at_node, Pi.one_apply, Polynomial.eval_one, mul_one, OfNat.ofNat, Eq.symm
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
x : F
hvs : Set.InjOn v (↑s : Set ι)
hs : s.Nonempty
hx : ∀ i ∈ s, x ≠ v i
rw :
  (eval x (nodal s v) * ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i) /
      (eval x (nodal s v) * ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * 1 i) =
    HDiv.hDiv (α := F) (∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i) (∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹)
⊢ eval x ((interpolate s v : (a : ι → F) → F[X]) r) =
    HDiv.hDiv (α := F) (∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i) (∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹)

Tactic:
rw [← div_one (eval x (interpolate s v r)), ← @eval_one _ _ x, ← interpolate_one hvs hs,
    eval_interpolate_not_at_node r hx, eval_interpolate_not_at_node 1 hx]

Premises used: Lagrange.interpolate_one, Polynomial.eval, Lagrange.eval_interpolate_not_at_node, Lagrange.interpolate, Polynomial.eval_one, OfNat.ofNat, div_one, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
x : F
hvs : Set.InjOn v (↑s : Set ι)
hs : s.Nonempty
hx : ∀ i ∈ s, x ≠ v i
⊢ (eval x (nodal s v) * ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i) /
      (eval x (nodal s v) * ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * 1 i) =
    HDiv.hDiv (α := F) (∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i) (∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹)

Tactic:
simp only [mul_div_mul_left _ _ (eval_nodal_not_at_node hx), Pi.one_apply, mul_one]

Premises used: Pi.one_apply, Lagrange.eval_nodal_not_at_node, mul_div_mul_left, mul_one
-- Module: Mathlib.LinearAlgebra.Matrix.AbsoluteValue
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
n : Type u_3
inst_5 : Fintype n
inst_6 : DecidableEq n
A : Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (i j : n), (abv : (a : R) → S) (A i j) ≤ x
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
rw :
  Eq.{u_2 + 1} (α := S) ((abv : (a : R) → S) (∏ i : n, A ((σ : (a : n) → n) i) i) : S)
    (∏ i : n, (abv : (a : R) → S) (A ((σ : (a : n) → n) i) i) : S)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := S) (∏ i : n, (abv : (a : R) → S) (A ((σ : (a : n) → n) i) i))
    (∏ i : n, (abv : (a : R) → S) (A ((σ : (a : n) → n) i) i))
⊢ Eq.{u_2 + 1} (α := S)
    ((abv : (a : R) → S)
        (HSMul.hSMul (α := ℤˣ) (β := R) (((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ : ℤˣ)
          (∏ i : n, A ((σ : (a : n) → n) i) i)) :
      S)
    (∏ i : n, (abv : (a : R) → S) (A ((σ : (a : n) → n) i) i) : S)

Tactic:
rw [abv.map_units_int_smul, abv.map_prod]

Premises used: AbsoluteValue.map_units_int_smul, AbsoluteValue.map_prod
-- Module: Mathlib.LinearAlgebra.Matrix.AbsoluteValue
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
n : Type u_3
inst_5 : Fintype n
inst_6 : DecidableEq n
A : Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (i j : n), (abv : (a : R) → S) (A i j) ≤ x
h :
  ∀ (i : Perm n),
    Membership.mem (γ := Finset (Perm n)) univ i →
      ∀ (i_1 : n), Membership.mem (γ := Finset n) univ i_1 → (abv : (a : R) → S) (A ((i : (a : n) → n) i_1) i_1) ≤ x
⊢ LE.le.{u_2} (α := S) (∑ σ : Perm n, ∏ i : n, (abv : (a : R) → S) (A ((σ : (a : n) → n) i) i))
    (∑ _σ : Perm n, ∏ _i : n, x)

Tactic:
gcongr