awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
h : ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
i j : ι
hij : x i = x j
q : F[X]
hq : ∀ (i : ι), eval (x i) q = y i
rw : eval (x i) q = y j
⊢ y i = y j
have rw₁ : eval (x i) q = eval (x j) q
Tactic: rw [← hq, ← hq, hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
h : ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
i j : ι
hij : x i = x j
q : F[X]
hq : ∀ (i : ι), eval (x i) q = y i
rw : eval (x i) q = y j
rw₁ : eval (x i) q = eval (x j) q
⊢ y i = y j
have rw₂ : eval (x j) q = eval (x j) q
Tactic: rw [← hq, ← hq, hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
⊢ (∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i) ↔ ∀ (i j : ι), x i = x j → y i = y j
have refine : ∀ (hwd : ∀ (i j : ι), x i = x j → y i = y j), ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
Tactic: refine ⟨fun ⟨q, hq⟩ i j hij ↦ by rw [← hq, ← hq, hij], fun hwd ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
⊢ ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
have have : ∀ (this : Fintype ι), ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
Tactic: have : Fintype ι := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (hypothesis)
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
⊢ ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
have hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)
Tactic: have hinj : Set.InjOn (fun d : F ↦ d) (Finset.univ.image x) := Function.injective_id.injOn
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (hypothesis)
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)
⊢ ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
have v_def : let v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0;
v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
Tactic: set v : F → F := fun z ↦ if h : ∃ i, x i = z then y h.choose else 0 with v_def
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)
v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
⊢ ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
have refine : ∀ (i : ι), eval (x i) ((interpolate (image x univ) fun (d : F) ↦ d : (a : F → F) → F[X]) v) = y i
Tactic: refine ⟨Lagrange.interpolate (Finset.univ.image x) (fun d : F ↦ d) v, fun i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)
v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
i : ι
⊢ eval (x i) ((interpolate (image x univ) fun (d : F) ↦ d : (a : F → F) → F[X]) v) = y i
have rw : (fun (z : F) ↦ (if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0 : F)) (x i) = y i
Tactic: rw [Lagrange.eval_interpolate_at_node _ hinj (by simp), v_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)
v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
i : ι
⊢ (if h : ∃ (i_1 : ι), x i_1 = x i then y (h.choose (p := fun (i_1 : ι) ↦ x i_1 = x i)) else 0) = y i
have pos : ∀ (h : ∃ (i_1 : ι), x i_1 = x i), y (h.choose (p := fun (i_1 : ι) ↦ x i_1 = x i)) = y i
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
this : Fintype ι
hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)
v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0
i : ι
pos : ∀ (h : ∃ (i_1 : ι), x i_1 = x i), y (h.choose (p := fun (i_1 : ι) ↦ x i_1 = x i)) = y i
⊢ (if h : ∃ (i_1 : ι), x i_1 = x i then y (h.choose (p := fun (i_1 : ι) ↦ x i_1 = x i)) else 0) = y i
have neg : ∀ (h : ¬∃ (i_1 : ι), x i_1 = x i), 0 = y i
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
⊢ ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
have have : ∀ (this : Fintype ι), ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
Tactic: classical
  have : Fintype ι := Fintype.ofFinite ι
  have hinj : Set.InjOn (fun d : F ↦ d) (Finset.univ.image x) := Function.injective_id.injOn
  set v : F → F := fun z ↦ if h : ∃ i, x i = z then y h.choose else 0 with v_def
  refine ⟨Lagrange.interpolate (Finset.univ.image x) (fun d : F ↦ d) v, fun i ↦ ?_⟩
  rw [Lagrange.eval_interpolate_at_node _ hinj (by simp), v_def]
  simp only
  split_ifs with h
  · exact hwd _ _ h.choose_spec
  · aesop
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
have have₁ have₂ : ∀ (this : Fintype ι), ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
⊢ ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
have have₃ : ∀ (this : Fintype ι) (hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)),
  ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
Tactic: classical
  have : Fintype ι := Fintype.ofFinite ι
  have hinj : Set.InjOn (fun d : F ↦ d) (Finset.univ.image x) := Function.injective_id.injOn
  set v : F → F := fun z ↦ if h : ∃ i, x i = z then y h.choose else 0 with v_def
  refine ⟨Lagrange.interpolate (Finset.univ.image x) (fun d : F ↦ d) v, fun i ↦ ?_⟩
  rw [Lagrange.eval_interpolate_at_node _ hinj (by simp), v_def]
  simp only
  split_ifs with h
  · exact hwd _ _ h.choose_spec
  · aesop
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
have have₁ have₂ : ∀ (this : Fintype ι), ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
have₃ :
  ∀ (this : Fintype ι) (hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)),
    ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
⊢ ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
have have₄ : ∀ (this : Fintype ι) (hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)),
  let v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0;
  ∀ (v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0),
    ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
Tactic: classical
  have : Fintype ι := Fintype.ofFinite ι
  have hinj : Set.InjOn (fun d : F ↦ d) (Finset.univ.image x) := Function.injective_id.injOn
  set v : F → F := fun z ↦ if h : ∃ i, x i = z then y h.choose else 0 with v_def
  refine ⟨Lagrange.interpolate (Finset.univ.image x) (fun d : F ↦ d) v, fun i ↦ ?_⟩
  rw [Lagrange.eval_interpolate_at_node _ hinj (by simp), v_def]
  simp only
  split_ifs with h
  · exact hwd _ _ h.choose_spec
  · aesop
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
have have₁ have₂ : ∀ (this : Fintype ι), ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
have₃ :
  ∀ (this : Fintype ι) (hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)),
    ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
have₄ :
  ∀ (this : Fintype ι) (hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)),
    let v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0;
    ∀ (v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0),
      ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
⊢ ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
have have₅ : ∀ (this : Fintype ι) (hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)),
  let v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0;
  ∀ (v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0) (i : ι),
    eval (x i) ((interpolate (image x univ) fun (d : F) ↦ d : (a : F → F) → F[X]) v) = y i
Tactic: classical
  have : Fintype ι := Fintype.ofFinite ι
  have hinj : Set.InjOn (fun d : F ↦ d) (Finset.univ.image x) := Function.injective_id.injOn
  set v : F → F := fun z ↦ if h : ∃ i, x i = z then y h.choose else 0 with v_def
  refine ⟨Lagrange.interpolate (Finset.univ.image x) (fun d : F ↦ d) v, fun i ↦ ?_⟩
  rw [Lagrange.eval_interpolate_at_node _ hinj (by simp), v_def]
  simp only
  split_ifs with h
  · exact hwd _ _ h.choose_spec
  · aesop
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
have have₁ have₂ : ∀ (this : Fintype ι), ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
have₃ :
  ∀ (this : Fintype ι) (hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)),
    ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
have₄ :
  ∀ (this : Fintype ι) (hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)),
    let v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0;
    ∀ (v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0),
      ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
have₅ :
  ∀ (this : Fintype ι) (hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)),
    let v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0;
    ∀ (v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0)
      (i : ι), eval (x i) ((interpolate (image x univ) fun (d : F) ↦ d : (a : F → F) → F[X]) v) = y i
⊢ ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
have have₆ : ∀ (this : Fintype ι) (hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)),
  let v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0;
  ∀ (v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0) (i : ι),
    (fun (z : F) ↦ (if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0 : F)) (x i) = y i
Tactic: classical
  have : Fintype ι := Fintype.ofFinite ι
  have hinj : Set.InjOn (fun d : F ↦ d) (Finset.univ.image x) := Function.injective_id.injOn
  set v : F → F := fun z ↦ if h : ∃ i, x i = z then y h.choose else 0 with v_def
  refine ⟨Lagrange.interpolate (Finset.univ.image x) (fun d : F ↦ d) v, fun i ↦ ?_⟩
  rw [Lagrange.eval_interpolate_at_node _ hinj (by simp), v_def]
  simp only
  split_ifs with h
  · exact hwd _ _ h.choose_spec
  · aesop
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_3
inst_1 : Finite ι
x y : ι → F
hwd : ∀ (i j : ι), x i = x j → y i = y j
have have₁ have₂ : ∀ (this : Fintype ι), ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
have₃ :
  ∀ (this : Fintype ι) (hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)),
    ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
have₄ :
  ∀ (this : Fintype ι) (hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)),
    let v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0;
    ∀ (v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0),
      ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
have₅ :
  ∀ (this : Fintype ι) (hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)),
    let v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0;
    ∀ (v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0)
      (i : ι), eval (x i) ((interpolate (image x univ) fun (d : F) ↦ d : (a : F → F) → F[X]) v) = y i
have₆ :
  ∀ (this : Fintype ι) (hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)),
    let v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0;
    ∀ (v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0)
      (i : ι),
      (fun (z : F) ↦ (if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0 : F)) (x i) = y i
have₇ :
  ∀ (this : Fintype ι) (hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)),
    let v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0;
    ∀ (v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0)
      (i : ι), (if h : ∃ (i_1 : ι), x i_1 = x i then y (h.choose (p := fun (i_1 : ι) ↦ x i_1 = x i)) else 0) = y i
⊢ ∃ (q : F[X]), ∀ (i : ι), eval (x i) q = y i
have pos : ∀ (this : Fintype ι) (hinj : Set.InjOn (β := F) (fun (d : F) ↦ d) (↑(image x univ) : Set F)),
  let v : F → F := fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0;
  ∀ (v_def : v = fun (z : F) ↦ if h : ∃ (i : ι), x i = z then y (h.choose (p := fun (i : ι) ↦ x i = z)) else 0) (i : ι)
    (h : ∃ (i_1 : ι), x i_1 = x i), y (h.choose (p := fun (i_1 : ι) ↦ x i_1 = x i)) = y i
Tactic: classical
  have : Fintype ι := Fintype.ofFinite ι
  have hinj : Set.InjOn (fun d : F ↦ d) (Finset.univ.image x) := Function.injective_id.injOn
  set v : F → F := fun z ↦ if h : ∃ i, x i = z then y h.choose else 0 with v_def
  refine ⟨Lagrange.interpolate (Finset.univ.image x) (fun d : F ↦ d) v, fun i ↦ ?_⟩
  rw [Lagrange.eval_interpolate_at_node _ hinj (by simp), v_def]
  simp only
  split_ifs with h
  · exact hwd _ _ h.choose_spec
  · aesop
-- 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 : Nontrivial R
⊢ natDegree (nodal s v) = #s
have simp_rw : natDegree.{u_1} (R := R) (∏ i ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X])) = #s
Tactic: simp_rw [nodal, natDegree_prod_of_monic (h := fun i _ => monic_X_sub_C (v i)),
    natDegree_X_sub_C, sum_const, smul_eq_mul, mul_one]
-- 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 : Nontrivial R
simp_rw :
  natDegree.{u_1} (R := R) (∏ i ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X])) = #s
⊢ natDegree (nodal s v) = #s
have simp_rw₁ : ∑ i ∈ s, (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X])).natDegree = #s
Tactic: simp_rw [nodal, natDegree_prod_of_monic (h := fun i _ => monic_X_sub_C (v i)),
    natDegree_X_sub_C, sum_const, smul_eq_mul, mul_one]
-- 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 : Nontrivial R
simp_rw :
  natDegree.{u_1} (R := R) (∏ i ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X])) = #s
simp_rw₁ : ∑ i ∈ s, (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X])).natDegree = #s
⊢ natDegree (nodal s v) = #s
have simp_rw₂ : ∑ x ∈ s, 1 = #s
Tactic: simp_rw [nodal, natDegree_prod_of_monic (h := fun i _ => monic_X_sub_C (v i)),
    natDegree_X_sub_C, sum_const, smul_eq_mul, mul_one]
-- 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 : Nontrivial R
simp_rw :
  natDegree.{u_1} (R := R) (∏ i ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X])) = #s
simp_rw₁ : ∑ i ∈ s, (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X])).natDegree = #s
simp_rw₂ : ∑ x ∈ s, 1 = #s
⊢ natDegree (nodal s v) = #s
have simp_rw₃ : HSMul.hSMul (β := ℕ) (#s) 1 = #s
Tactic: simp_rw [nodal, natDegree_prod_of_monic (h := fun i _ => monic_X_sub_C (v i)),
    natDegree_X_sub_C, sum_const, smul_eq_mul, mul_one]
-- 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 : Nontrivial R
simp_rw :
  natDegree.{u_1} (R := R) (∏ i ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X])) = #s
simp_rw₁ : ∑ i ∈ s, (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X])).natDegree = #s
simp_rw₂ : ∑ x ∈ s, 1 = #s
simp_rw₃ : HSMul.hSMul (β := ℕ) (#s) 1 = #s
⊢ natDegree (nodal s v) = #s
have simp_rw₄ : #s * 1 = #s
Tactic: simp_rw [nodal, natDegree_prod_of_monic (h := fun i _ => monic_X_sub_C (v i)),
    natDegree_X_sub_C, sum_const, smul_eq_mul, mul_one]
-- 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 : Nontrivial R
⊢ Ne (α := R[X]) (nodal s v) 0
have inl : Ne (α := R[X]) (nodal ∅ v) 0
Tactic: rcases s.eq_empty_or_nonempty with (rfl | h)
Cleared hypotheses: s
-- 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 : Nontrivial R
inl : Ne (α := R[X]) (nodal ∅ v) 0
⊢ Ne (α := R[X]) (nodal s v) 0
have inr : ∀ (h : s.Nonempty), Ne (α := R[X]) (nodal s v) 0
Tactic: rcases s.eq_empty_or_nonempty with (rfl | h)
-- 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 : Nontrivial R
h : s.Nonempty
⊢ Ne (α := R[X]) (nodal s v) 0
have inr : 0 < natDegree (nodal s v)
Tactic: apply ne_zero_of_natDegree_gt (n := 0)
-- 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 : Nontrivial R
⊢ degree (nodal s v) = (↑(#s) : WithBot ℕ)
have simp_rw : Eq (α := WithBot ℕ) (↑(natDegree (nodal s v)) : WithBot ℕ) (↑(#s) : WithBot ℕ)
Tactic: simp_rw [degree_eq_natDegree nodal_ne_zero, natDegree_nodal]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
x : R
⊢ eval x (nodal s v) = ∏ i ∈ s, (x - v i)
have simp_rw : eval x (∏ i ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X])) = ∏ i ∈ s, (x - v i)
Tactic: simp_rw [nodal, eval_prod, eval_sub, eval_X, eval_C]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
x : R
simp_rw : eval x (∏ i ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X])) = ∏ i ∈ s, (x - v i)
⊢ eval x (nodal s v) = ∏ i ∈ s, (x - v i)
have simp_rw₁ : Eq.{u_1 + 1} (α := R) (∏ j ∈ s, eval x (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v j) : R[X])))
  (∏ i ∈ s, (x - v i))
Tactic: simp_rw [nodal, eval_prod, eval_sub, eval_X, eval_C]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
x : R
simp_rw : eval x (∏ i ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X])) = ∏ i ∈ s, (x - v i)
simp_rw₁ :
  Eq.{u_1 + 1} (α := R) (∏ j ∈ s, eval x (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v j) : R[X])))
    (∏ i ∈ s, (x - v i))
⊢ eval x (nodal s v) = ∏ i ∈ s, (x - v i)
have simp_rw₂ : Eq.{u_1 + 1} (α := R) (∏ x_1 ∈ s, (eval x X - eval x ((C : (a : R) → R[X]) (v x_1)))) (∏ i ∈ s, (x - v i))
Tactic: simp_rw [nodal, eval_prod, eval_sub, eval_X, eval_C]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
x : R
simp_rw : eval x (∏ i ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v i) : R[X])) = ∏ i ∈ s, (x - v i)
simp_rw₁ :
  Eq.{u_1 + 1} (α := R) (∏ j ∈ s, eval x (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (v j) : R[X])))
    (∏ i ∈ s, (x - v i))
simp_rw₂ : Eq.{u_1 + 1} (α := R) (∏ x_1 ∈ s, (eval x X - eval x ((C : (a : R) → R[X]) (v x_1)))) (∏ i ∈ s, (x - v i))
⊢ eval x (nodal s v) = ∏ i ∈ s, (x - v i)
have simp_rw₃ : Eq.{u_1 + 1} (α := R) (∏ x_1 ∈ s, (x - eval x ((C : (a : R) → R[X]) (v x_1)))) (∏ i ∈ s, (x - v i))
Tactic: simp_rw [nodal, eval_prod, eval_sub, eval_X, eval_C]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
i : ι
hi : i ∈ s
⊢ eval (v i) (nodal s v) = 0
have rw : Eq.{u_1 + 1} (α := R) (∏ i_1 ∈ s, (v i - v i_1)) 0
Tactic: rw [eval_nodal]
-- 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 ι
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (nodal s v) : R[X]) (∑ i ∈ s, nodal (s.erase i) v : R[X])
have refine_1 : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (nodal ∅ v) : R[X]) (∑ i ∈ ∅, nodal (Finset.erase ∅ i) v : R[X])
Tactic: refine s.induction_on ?_ fun i t hit IH => ?_
-- 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 (α := R[X]) ((derivative : (a : R[X]) → R[X]) (nodal ∅ v) : R[X]) (∑ i ∈ ∅, nodal (Finset.erase ∅ i) v : R[X])
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (nodal s v) : R[X]) (∑ i ∈ s, nodal (s.erase i) v : R[X])
have refine_2 : ∀ (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])
Tactic: refine s.induction_on ?_ fun i t hit IH => ?_
-- 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 ι
⊢ 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]) ((derivative : (a : R[X]) → R[X]) 1) (∑ i ∈ ∅, nodal (Finset.erase ∅ i) v)
Tactic: rw [nodal_empty, derivative_one, sum_empty]