awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
g : R[X]
s : Finset R
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 : ∀ x ∈ s, eval x 0 = eval x g
inl : ∀ (h_deg_eq : ⊥ = g.degree) (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ x ∈ s, eval x 0 = eval x g), 0 = g
inl₁ :
  ∀ (h_deg_eq : g.degree = ⊥) (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ x ∈ s, eval x 0 = eval x g), 0 = g
inl₂ : ∀ (h_deg_eq : g = 0) (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ x ∈ s, eval x 0 = eval x g), 0 = g
inl₃ inl₄ inl₅ inl₆ :
  ∀ (h_deg_eq : 0 = g) (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ x ∈ s, eval x 0 = eval x g), 0 = g
⊢ 0 = g

Tactic:
rwa [degree_zero, eq_comm, degree_eq_bot, eq_comm] at h_deg_eq

Premises used: eq_comm, Polynomial.degree_zero, Polynomial.degree_eq_bot
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
s : Finset R
h_deg_le : f.degree ≤ (↑(#s) : WithBot ℕ)
h_deg_eq : f.degree = g.degree
hlc : f.leadingCoeff = g.leadingCoeff
h_eval : ∀ x ∈ s, eval x f = eval x g
hf : f ≠ 0
⊢ f = g

Tactic:
eq_of_degree_sub_lt_of_eval_finset_eq s
      (lt_of_lt_of_le (degree_sub_lt h_deg_eq hf hlc) h_deg_le) h_eval

Premises used: Polynomial.eq_of_degree_sub_lt_of_eval_finset_eq, Polynomial.degree_sub_lt, lt_of_lt_of_le
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
s : Finset R
h_deg_le : f.degree ≤ (↑(#s) : WithBot ℕ)
h_deg_eq : f.degree = g.degree
hlc : f.leadingCoeff = g.leadingCoeff
h_eval : ∀ x ∈ s, eval x f = eval x g
hf : f ≠ 0
⊢ f = g

Tactic:
exact eq_of_degree_sub_lt_of_eval_finset_eq s
      (lt_of_lt_of_le (degree_sub_lt h_deg_eq hf hlc) h_deg_le) h_eval

Premises used: Polynomial.eq_of_degree_sub_lt_of_eval_finset_eq, Polynomial.degree_sub_lt, lt_of_lt_of_le
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v (↑s : Set ι)
degree_f_lt : f.degree < (↑(#s) : WithBot ℕ)
eval_f : ∀ i ∈ s, eval (v i) f = 0
⊢ f.degree < (↑(#(image v s)) : WithBot ℕ)

Tactic:
rw [← card_image_of_injOn hvs] at degree_f_lt

Premises used: Finset.card_image_of_injOn
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v (↑s : Set ι)
degree_f_lt : f.degree < (↑(#s) : WithBot ℕ)
eval_f : ∀ i ∈ s, eval (v i) f = 0
degree_f_lt₁ : f.degree < (↑(#(image v s)) : WithBot ℕ)
⊢ ∀ i ∈ s, eval (v i) f = 0

Tactic:
rw [← card_image_of_injOn hvs] at degree_f_lt

Premises used: Finset.card_image_of_injOn
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v (↑s : Set ι)
degree_f_lt : f.degree < (↑(#(image v s)) : WithBot ℕ)
eval_f : ∀ i ∈ s, eval (v i) f = 0
⊢ f = 0

Tactic:
eq_zero_of_degree_lt_of_eval_finset_eq_zero _ degree_f_lt ?_

Premises used: Polynomial.eq_zero_of_degree_lt_of_eval_finset_eq_zero
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v (↑s : Set ι)
degree_f_lt : f.degree < (↑(#(image v s)) : WithBot ℕ)
eval_f : ∀ i ∈ s, eval (v i) f = 0
refine : ∀ x ∈ image v s, eval x f = 0
⊢ f = 0

Tactic:
refine eq_zero_of_degree_lt_of_eval_finset_eq_zero _ degree_f_lt ?_

Premises used: Polynomial.eq_zero_of_degree_lt_of_eval_finset_eq_zero
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v (↑s : Set ι)
degree_f_lt : f.degree < (↑(#(image v s)) : WithBot ℕ)
eval_f : ∀ i ∈ s, eval (v i) f = 0
x : R
hx : x ∈ image v s
rcases : ∀ (w : ι) (hj : w ∈ s) (hx : v w ∈ image v s), eval (v w) f = 0
⊢ eval x f = 0

Tactic:
rcases mem_image.mp hx with ⟨_, hj, rfl⟩

Premises used: Finset.mem_image, Iff.mp, rfl
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v (↑s : Set ι)
degree_f_lt : f.degree < (↑(#(image v s)) : WithBot ℕ)
eval_f : ∀ i ∈ s, eval (v i) f = 0
w : ι
hj : w ∈ s
hx : v w ∈ image v s
⊢ eval (v w) f = 0

Tactic:
eval_f _ hj
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v (↑s : Set ι)
degree_f_lt : f.degree < (↑(#(image v s)) : WithBot ℕ)
eval_f : ∀ i ∈ s, eval (v i) f = 0
w : ι
hj : w ∈ s
hx : v w ∈ image v s
⊢ eval (v w) f = 0

Tactic:
exact eval_f _ hj
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v (↑s : Set ι)
degree_f_lt : f.degree < (↑(#s) : WithBot ℕ)
eval_f : ∀ i ∈ s, eval (v i) f = 0
rw rw₁ rw₂ : ∀ (degree_f_lt : f.degree < (↑(#(image v s)) : WithBot ℕ)) (eval_f : ∀ i ∈ s, eval (v i) f = 0), f = 0
rw₃ rw₄ :
  ∀ (degree_f_lt : f.degree < (↑(#(image v s)) : WithBot ℕ)) (eval_f : ∀ i ∈ s, eval (v i) f = 0) (x : R)
    (hx : x ∈ image v s), eval x f = 0
rw₅ :
  ∀ (degree_f_lt : f.degree < (↑(#(image v s)) : WithBot ℕ)) (eval_f : ∀ i ∈ s, eval (v i) f = 0) (w : ι) (hj : w ∈ s)
    (hx : v w ∈ image v s), eval (v w) f = 0
⊢ f = 0

Tactic:
classical
    rw [← card_image_of_injOn hvs] at degree_f_lt
    refine eq_zero_of_degree_lt_of_eval_finset_eq_zero _ degree_f_lt ?_
    intro x hx
    rcases mem_image.mp hx with ⟨_, hj, rfl⟩
    exact eval_f _ hj

Premises used: Polynomial.eq_zero_of_degree_lt_of_eval_finset_eq_zero, rfl
-- Module: Mathlib.LinearAlgebra.Lagrange
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 ι)
degree_fg_lt : (f - g).degree < (↑(#s) : WithBot ℕ)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
rw : f - g = 0
⊢ f = g

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.LinearAlgebra.Lagrange
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 ι)
degree_fg_lt : (f - g).degree < (↑(#s) : WithBot ℕ)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ f - g = 0

Tactic:
eq_zero_of_degree_lt_of_eval_index_eq_zero _ hvs degree_fg_lt ?_

Premises used: Polynomial.eq_zero_of_degree_lt_of_eval_index_eq_zero
-- Module: Mathlib.LinearAlgebra.Lagrange
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 ι)
degree_fg_lt : (f - g).degree < (↑(#s) : WithBot ℕ)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
refine : ∀ i ∈ s, eval (v i) (f - g) = 0
⊢ f - g = 0

Tactic:
refine eq_zero_of_degree_lt_of_eval_index_eq_zero _ hvs degree_fg_lt ?_

Premises used: Polynomial.eq_zero_of_degree_lt_of_eval_index_eq_zero
-- Module: Mathlib.LinearAlgebra.Lagrange
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 ι)
degree_fg_lt : (f - g).degree < (↑(#s) : WithBot ℕ)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
simp_rw : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ ∀ i ∈ s, eval (v i) (f - g) = 0

Tactic:
simp_rw [eval_sub, sub_eq_zero]

Premises used: sub_eq_zero, Polynomial.eval_sub
-- Module: Mathlib.LinearAlgebra.Lagrange
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 ι)
degree_fg_lt : (f - g).degree < (↑(#s) : WithBot ℕ)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ ∀ i ∈ s, eval (v i) f = eval (v i) g

Tactic:
eval_fg
-- Module: Mathlib.LinearAlgebra.Lagrange
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 ι)
degree_fg_lt : (f - g).degree < (↑(#s) : WithBot ℕ)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ ∀ i ∈ s, eval (v i) f = eval (v i) g

Tactic:
exact eval_fg
-- Module: Mathlib.LinearAlgebra.Lagrange
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 ι)
degree_f_lt : f.degree < (↑(#s) : WithBot ℕ)
degree_g_lt : g.degree < (↑(#s) : WithBot ℕ)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ f = g

Tactic:
eq_of_degree_sub_lt_of_eval_index_eq _ hvs ?_ eval_fg

Premises used: Polynomial.eq_of_degree_sub_lt_of_eval_index_eq
-- Module: Mathlib.LinearAlgebra.Lagrange
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 ι)
degree_f_lt : f.degree < (↑(#s) : WithBot ℕ)
degree_g_lt : g.degree < (↑(#s) : WithBot ℕ)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
refine : (f - g).degree < (↑(#s) : WithBot ℕ)
⊢ f = g

Tactic:
refine eq_of_degree_sub_lt_of_eval_index_eq _ hvs ?_ eval_fg

Premises used: Polynomial.eq_of_degree_sub_lt_of_eval_index_eq
-- Module: Mathlib.LinearAlgebra.Lagrange
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 ι)
degree_f_lt : f.degree < (↑(#s) : WithBot ℕ)
degree_g_lt : g.degree < (↑(#s) : WithBot ℕ)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
rw :
  ∀ (degree_f_lt : Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) f)
    (degree_g_lt : Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) g)
    (eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g), Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) (f - g)
⊢ (f - g).degree < (↑(#s) : WithBot ℕ)

Tactic:
rw [← mem_degreeLT] at degree_f_lt degree_g_lt ⊢

Premises used: Polynomial.mem_degreeLT
-- Module: Mathlib.LinearAlgebra.Lagrange
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 ι)
degree_f_lt : Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) f
degree_g_lt : Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) g
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) (f - g)

Tactic:
Submodule.sub_mem _ degree_f_lt degree_g_lt

Premises used: Set.Mem, Submodule.sub_mem
-- Module: Mathlib.LinearAlgebra.Lagrange
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 ι)
degree_f_lt : Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) f
degree_g_lt : Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) g
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) (f - g)

Tactic:
exact Submodule.sub_mem _ degree_f_lt degree_g_lt

Premises used: Submodule.sub_mem
-- Module: Mathlib.LinearAlgebra.Lagrange
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
inr : ∀ (hf : f ≠ 0), f = g
⊢ f = g

Tactic:
rcases eq_or_ne f 0 with rfl | hf

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.LinearAlgebra.Lagrange
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
inl₃ inl₄ inl₅ 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
⊢ 0 = g

Tactic:
rwa [degree_zero, eq_comm, degree_eq_bot, eq_comm] at h_deg_eq

Premises used: eq_comm, Polynomial.degree_zero, Polynomial.degree_eq_bot
-- Module: Mathlib.LinearAlgebra.Lagrange
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
hf : f ≠ 0
⊢ f = g

Tactic:
eq_of_degree_sub_lt_of_eval_index_eq s hvs
      (lt_of_lt_of_le (degree_sub_lt h_deg_eq hf hlc) h_deg_le)
      h_eval

Premises used: Polynomial.eq_of_degree_sub_lt_of_eval_index_eq, Polynomial.degree_sub_lt, lt_of_lt_of_le
-- Module: Mathlib.LinearAlgebra.Lagrange
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
hf : f ≠ 0
⊢ f = g

Tactic:
exact eq_of_degree_sub_lt_of_eval_index_eq s hvs
      (lt_of_lt_of_le (degree_sub_lt h_deg_eq hf hlc) h_deg_le)
      h_eval

Premises used: Polynomial.eq_of_degree_sub_lt_of_eval_index_eq, Polynomial.degree_sub_lt, lt_of_lt_of_le
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
x : F
⊢ Eq (α := F[X]) (basisDivisor x x) 0

Tactic:
simp only [basisDivisor, sub_self, inv_zero, map_zero, zero_mul]

Premises used: sub_self, inv_zero, MulZeroClass.zero_mul, map_zero, Lagrange.basisDivisor
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
x y : F
hxy : Eq (α := F[X]) (basisDivisor x y) 0
⊢ x = y

Tactic:
simp_rw [basisDivisor, mul_eq_zero, X_sub_C_ne_zero, or_false, C_eq_zero, inv_eq_zero,
    sub_eq_zero] at hxy

Premises used: inv_eq_zero, sub_eq_zero, Polynomial.C_eq_zero, mul_eq_zero, or_false, Polynomial.X_sub_C_ne_zero, Lagrange.basisDivisor
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
x y : F
hxy : x = y
⊢ x = y

Tactic:
hxy
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
x y : F
hxy : x = y
⊢ x = y

Tactic:
exact hxy
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
x y : F
⊢ Eq (α := F[X]) (basisDivisor x y) 0 ↔ x = y

Tactic:
⟨basisDivisor_inj, fun H => H ▸ basisDivisor_self⟩

Premises used: Lagrange.basisDivisor_self, Eq.rec, Lagrange.basisDivisor_inj, Iff.intro
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
x y : F
rw : ¬Eq (α := F[X]) (basisDivisor x y) 0 ↔ x ≠ y
rw₁ rw₂ : ¬x = y ↔ x ≠ y
⊢ Ne (α := F[X]) (basisDivisor x y) 0 ↔ x ≠ y

Tactic:
rw [Ne, basisDivisor_eq_zero_iff]

Premises used: Ne, Lagrange.basisDivisor_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
x y : F
hxy : x ≠ y
rw : (x - y)⁻¹ ≠ 0
⊢ degree (basisDivisor x y) = 1

Tactic:
rw [basisDivisor, degree_mul, degree_X_sub_C, degree_C, zero_add]

Premises used: Polynomial.degree_X_sub_C, Polynomial.degree_C, zero_add, Lagrange.basisDivisor, Polynomial.degree_mul
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
x y : F
hxy : x ≠ y
⊢ (x - y)⁻¹ ≠ 0

Tactic:
inv_ne_zero (sub_ne_zero_of_ne hxy)

Premises used: sub_ne_zero_of_ne, inv_ne_zero
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
x y : F
hxy : x ≠ y
⊢ (x - y)⁻¹ ≠ 0

Tactic:
exact inv_ne_zero (sub_ne_zero_of_ne hxy)

Premises used: sub_ne_zero_of_ne, inv_ne_zero
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
x : F
rw : degree.{u_1} (R := F) 0 = ⊥
rw₁ rw₂ : Eq (α := WithBot ℕ) ⊥ ⊥
⊢ degree (basisDivisor x x) = ⊥

Tactic:
rw [basisDivisor_self, degree_zero]

Premises used: Lagrange.basisDivisor_self, Polynomial.degree_zero
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
x : F
rw : natDegree.{u_1} (R := F) 0 = 0
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ natDegree (basisDivisor x x) = 0

Tactic:
rw [basisDivisor_self, natDegree_zero]

Premises used: Lagrange.basisDivisor_self, Polynomial.natDegree_zero
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
x y : F
hxy : x ≠ y
⊢ natDegree (basisDivisor x y) = 1

Tactic:
natDegree_eq_of_degree_eq_some (degree_basisDivisor_of_ne hxy)

Premises used: Lagrange.degree_basisDivisor_of_ne, Polynomial.natDegree_eq_of_degree_eq_some
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
x y : F
⊢ eval y (basisDivisor x y) = 0

Tactic:
simp only [basisDivisor, eval_mul, eval_C, eval_sub, eval_X, sub_self, mul_zero]

Premises used: Polynomial.eval_C, sub_self, Polynomial.eval_X, Polynomial.eval_mul, MulZeroClass.mul_zero, Polynomial.eval_sub, Lagrange.basisDivisor
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
x y : F
hxy : x ≠ y
simp : (x - y)⁻¹ * (x - y) = 1
⊢ eval x (basisDivisor x y) = 1

Tactic:
simp only [basisDivisor, eval_mul, eval_C, eval_sub, eval_X]

Premises used: Polynomial.eval_C, Polynomial.eval_X, Polynomial.eval_mul, Polynomial.eval_sub, Lagrange.basisDivisor
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
x y : F
hxy : x ≠ y
⊢ (x - y)⁻¹ * (x - y) = 1

Tactic:
inv_mul_cancel₀ (sub_ne_zero_of_ne hxy)

Premises used: sub_ne_zero_of_ne, inv_mul_cancel₀
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
x y : F
hxy : x ≠ y
⊢ (x - y)⁻¹ * (x - y) = 1

Tactic:
exact inv_mul_cancel₀ (sub_ne_zero_of_ne hxy)

Premises used: sub_ne_zero_of_ne, inv_mul_cancel₀
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
v : ι → F
i : ι
⊢ Eq (α := F[X]) (Lagrange.basis ∅ v i) 1

Tactic:
rfl

Premises used: Multiset.foldr, Multiset.prod, Finset.prod, Lagrange.basis, List.foldr, rfl
-- Module: Mathlib.LinearAlgebra.Lagrange
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
rw₂ rw₃ : Eq.{u_1 + 1} (α := F[X]) 1 1
⊢ Eq (α := F[X]) (Lagrange.basis {i} v i) 1

Tactic:
rw [Lagrange.basis, erase_singleton, prod_empty]

Premises used: Finset.prod_empty, Lagrange.basis, Finset.erase_singleton
-- Module: Mathlib.LinearAlgebra.Lagrange
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 i) (basisDivisor (v i) (v j))

Tactic:
simp only [Lagrange.basis, hij, erase_insert_eq_erase, erase_eq_of_notMem, mem_singleton,
    not_false_iff, prod_singleton]

Premises used: Finset.mem_singleton, Finset.prod_singleton, Finset.erase_insert_eq_erase, Lagrange.basis, Finset.erase_eq_of_notMem, not_false_iff
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
v : ι → F
i j : ι
hij : i ≠ j
rw : Eq (α := F[X]) (Lagrange.basis {j, i} v j) (basisDivisor (v j) (v i))
⊢ Eq (α := F[X]) (Lagrange.basis {i, j} v j) (basisDivisor (v j) (v i))

Tactic:
rw [pair_comm]

Premises used: Finset.pair_comm
-- Module: Mathlib.LinearAlgebra.Lagrange
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 {j, i} v j) (basisDivisor (v j) (v i))

Tactic:
basis_pair_left hij.symm

Premises used: Ne.symm, Lagrange.basis_pair_left
-- Module: Mathlib.LinearAlgebra.Lagrange
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 {j, i} v j) (basisDivisor (v j) (v i))

Tactic:
exact basis_pair_left hij.symm

Premises used: Ne.symm, Lagrange.basis_pair_left
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
simp_rw : ∀ (a : ι), a ≠ i ∧ a ∈ s → ¬Eq (α := F[X]) (basisDivisor (v i) (v a)) 0
⊢ Ne (α := F[X]) (Lagrange.basis s v i) 0

Tactic:
simp_rw [Lagrange.basis, prod_ne_zero_iff, Ne, mem_erase]

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

Tactic:
rw [basisDivisor_eq_zero_iff, hvs.eq_iff hi hj]

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

Tactic:
hij.symm

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

Tactic:
exact hij.symm

Premises used: Ne.symm
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
rw : Eq.{u_1 + 1} (α := F) (∏ j ∈ s.erase i, eval (v i) (basisDivisor (v i) (v j))) 1
⊢ eval (v i) (Lagrange.basis s v i) = 1

Tactic:
rw [Lagrange.basis, eval_prod]

Premises used: Polynomial.eval_prod, Lagrange.basis
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
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

Tactic:
prod_eq_one fun j H => ?_

Premises used: Finset.prod_eq_one
-- 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
refine : ∀ (j : ι) (H : j ∈ s.erase i), eval (v i) (basisDivisor (v i) (v j)) = 1
⊢ Eq.{u_1 + 1} (α := F) (∏ j ∈ s.erase i, eval (v i) (basisDivisor (v i) (v j))) 1

Tactic:
refine prod_eq_one fun j H => ?_

Premises used: Finset.prod_eq_one
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
j : ι
H : j ∈ s.erase i
rw : v i ≠ v j
⊢ eval (v i) (basisDivisor (v i) (v j)) = 1

Tactic:
rw [eval_basisDivisor_left_of_ne]

Premises used: Lagrange.eval_basisDivisor_left_of_ne
-- Module: Mathlib.LinearAlgebra.Lagrange
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v (↑s : Set ι)
hi : i ∈ s
j : ι
H : j ∈ s.erase i
⊢ j ≠ i

Tactic:
rcases mem_erase.mp H 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 : ι
H : j ∈ s.erase i
hij : j ≠ i
⊢ j ∈ s

Tactic:
rcases mem_erase.mp H 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 : ι
H : j ∈ s.erase i
hij : j ≠ i
hj : j ∈ s
⊢ v i ≠ v j

Tactic:
mt (hvs hi hj) hij.symm

Premises used: mt, Ne.symm