awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : (i : ℕ) → Matrix (Fin (m + n)) (Fin (m + n)) R :=
  fun (i : ℕ) ↦
    (Matrix.of : (a : Fin (m + n) → Fin (m + n) → R) → Matrix (Fin (m + n)) (Fin (m + n)) R) fun (j₁ j₂ : Fin (m + n)) ↦
      if (↑j₂ : ℕ) < i then M₁ j₁ j₂ else M₂ j₁ j₂
j₁ : Fin (m + n)
i : Fin n
IH : ∀ (hi : (↑(Fin.natAdd m i) : ℕ) ≤ m), (M (↑(Fin.natAdd m i) : ℕ)).det = M₂.det
hi : m + (↑i : ℕ) + 1 ≤ m
this : (⟨m + (↑i : ℕ) + (k + m), ⋯⟩ : Fin (m + n)) = Fin.natAdd m ⟨(↑i : ℕ) + (k + m), ⋯⟩
⊢ HSub.hSub (α := R)
      (Fin.addCases (motive := fun (x : Fin (m + n)) ↦ R)
          (fun (j₁_1 : Fin m) ↦
            if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + n then
              g.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) +
                (HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])).coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ))
            else 0)
          (fun (j₁_1 : Fin n) ↦
            if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + m then f.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
          (Fin.natAdd m i) :
        R)
      (HMul.hMul (β := R) r
        (Fin.addCases (motive := fun (x : Fin (m + n)) ↦ R)
            (fun (j₁_1 : Fin m) ↦
              if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + n then g.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
            (fun (j₁_1 : Fin n) ↦
              if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + m then f.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
            (⟨(↑(Fin.natAdd m i) : ℕ) + (k + m), ⋯⟩ : Fin (m + n)) :
          R)) =
    Fin.addCases (motive := fun (x : Fin (m + n)) ↦ R)
      (fun (j₁_1 : Fin m) ↦
        if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + n then g.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
      (fun (j₁_1 : Fin n) ↦
        if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + m then f.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
      (Fin.natAdd m i)
have succ : (r *
    if (↑i : ℕ) + (k + m) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑i : ℕ) + (k + m) + m then
      f.coeff ((↑j₁ : ℕ) - ((↑i : ℕ) + (k + m)))
    else 0) =
  0
Tactic: simp only [Fin.addCases_right, Fin.val_natAdd, sub_eq_self, this]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : (i : ℕ) → Matrix (Fin (m + n)) (Fin (m + n)) R :=
  fun (i : ℕ) ↦
    (Matrix.of : (a : Fin (m + n) → Fin (m + n) → R) → Matrix (Fin (m + n)) (Fin (m + n)) R) fun (j₁ j₂ : Fin (m + n)) ↦
      if (↑j₂ : ℕ) < i then M₁ j₁ j₂ else M₂ j₁ j₂
j₁ : Fin (m + n)
i : Fin n
IH : ∀ (hi : (↑(Fin.natAdd m i) : ℕ) ≤ m), (M (↑(Fin.natAdd m i) : ℕ)).det = M₂.det
hi : m + (↑i : ℕ) + 1 ≤ m
this : (⟨m + (↑i : ℕ) + (k + m), ⋯⟩ : Fin (m + n)) = Fin.natAdd m ⟨(↑i : ℕ) + (k + m), ⋯⟩
⊢ (r *
      if (↑i : ℕ) + (k + m) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑i : ℕ) + (k + m) + m then
        f.coeff ((↑j₁ : ℕ) - ((↑i : ℕ) + (k + m)))
      else 0) =
    0
have succ : ¬((↑i : ℕ) + (k + m) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑i : ℕ) + (k + m) + m)
Tactic: rw [if_neg, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : (i : ℕ) → Matrix (Fin (m + n)) (Fin (m + n)) R :=
  fun (i : ℕ) ↦
    (Matrix.of : (a : Fin (m + n) → Fin (m + n) → R) → Matrix (Fin (m + n)) (Fin (m + n)) R) fun (j₁ j₂ : Fin (m + n)) ↦
      if (↑j₂ : ℕ) < i then M₁ j₁ j₂ else M₂ j₁ j₂
i : ℕ
hi : i ≤ m
⊢ (M i).det = M₂.det
have zero : ∀ (hi : 0 ≤ m), (M 0).det = M₂.det
Tactic: induction i with
    | zero => simp [M]; rfl
    | succ i IH =>
      rw [← IH (by lia), ← Matrix.det_updateCol_add_smul_self (i := ⟨i, by lia⟩)
        (j := ⟨i + k + m, by lia⟩) (c := -r) (M (i + 1)) (by simp; lia)]
      congr 1
      ext j₁ j₂
      simp only [Matrix.of_apply, lt_add_iff_pos_right, zero_lt_one, ↓reduceIte, add_assoc,
        add_lt_add_iff_left, Nat.lt_one_iff, Nat.add_eq_zero_iff, hm, and_false, smul_eq_mul,
        Matrix.updateCol_apply, Fin.ext_iff, M, M₂, neg_mul, ← sub_eq_add_neg]
      obtain rfl | h := eq_or_ne ↑j₂ i
      · simp only [↓reduceIte, sylvester, Set.mem_Icc, coeff_add, Fin.eta, Matrix.of_apply,
          lt_self_iff_false, M₁]
        induction j₂ using Fin.addCases with
        | left j₂ =>
          dsimp at hi
          have : Fin.mk (n := m + n) (↑j₂ + (k + m)) (by lia) = .natAdd m ⟨j₂ + k, by lia⟩ :=
            Fin.ext (by simp; lia)
          simp only [Fin.addCases_left, Fin.val_castAdd, this, Fin.addCases_right, mul_ite,
            mul_zero, ← C_mul_X_pow_eq_monomial, ← mul_assoc, coeff_mul_X_pow', ite_add_zero,
            coeff_mul_C, add_assoc, add_eq_left, ← ite_and, ← mul_comm r, tsub_add_eq_tsub_tsub,
            add_sub_assoc, sub_eq_zero]
          split_ifs with h₁ h₂ h₂ <;> try rfl
          · rw [coeff_eq_zero_of_natDegree_lt, mul_zero]
            exact hf.trans_lt (by lia)
          · lia
        | right i =>
          simp only [Fin.val_natAdd] at hi
          have : Fin.mk (n := m + n) (m + ↑i + (k + m)) (by lia) =
              Fin.natAdd m ⟨↑i + (k + m), by lia⟩ := Fin.ext (by simp; lia)
          simp only [Fin.addCases_right, Fin.val_natAdd, sub_eq_self, this]
          rw [if_neg, mul_zero]
          lia
      lia
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : (i : ℕ) → Matrix (Fin (m + n)) (Fin (m + n)) R :=
  fun (i : ℕ) ↦
    (Matrix.of : (a : Fin (m + n) → Fin (m + n) → R) → Matrix (Fin (m + n)) (Fin (m + n)) R) fun (j₁ j₂ : Fin (m + n)) ↦
      if (↑j₂ : ℕ) < i then M₁ j₁ j₂ else M₂ j₁ j₂
i : ℕ
hi : i ≤ m
zero : ∀ (hi : 0 ≤ m), (M 0).det = M₂.det
⊢ (M i).det = M₂.det
have succ : ∀ (i : ℕ) (IH : ∀ (hi : i ≤ m), (M i).det = M₂.det) (hi : i + 1 ≤ m), (M (i + 1)).det = M₂.det
Tactic: induction i with
    | zero => simp [M]; rfl
    | succ i IH =>
      rw [← IH (by lia), ← Matrix.det_updateCol_add_smul_self (i := ⟨i, by lia⟩)
        (j := ⟨i + k + m, by lia⟩) (c := -r) (M (i + 1)) (by simp; lia)]
      congr 1
      ext j₁ j₂
      simp only [Matrix.of_apply, lt_add_iff_pos_right, zero_lt_one, ↓reduceIte, add_assoc,
        add_lt_add_iff_left, Nat.lt_one_iff, Nat.add_eq_zero_iff, hm, and_false, smul_eq_mul,
        Matrix.updateCol_apply, Fin.ext_iff, M, M₂, neg_mul, ← sub_eq_add_neg]
      obtain rfl | h := eq_or_ne ↑j₂ i
      · simp only [↓reduceIte, sylvester, Set.mem_Icc, coeff_add, Fin.eta, Matrix.of_apply,
          lt_self_iff_false, M₁]
        induction j₂ using Fin.addCases with
        | left j₂ =>
          dsimp at hi
          have : Fin.mk (n := m + n) (↑j₂ + (k + m)) (by lia) = .natAdd m ⟨j₂ + k, by lia⟩ :=
            Fin.ext (by simp; lia)
          simp only [Fin.addCases_left, Fin.val_castAdd, this, Fin.addCases_right, mul_ite,
            mul_zero, ← C_mul_X_pow_eq_monomial, ← mul_assoc, coeff_mul_X_pow', ite_add_zero,
            coeff_mul_C, add_assoc, add_eq_left, ← ite_and, ← mul_comm r, tsub_add_eq_tsub_tsub,
            add_sub_assoc, sub_eq_zero]
          split_ifs with h₁ h₂ h₂ <;> try rfl
          · rw [coeff_eq_zero_of_natDegree_lt, mul_zero]
            exact hf.trans_lt (by lia)
          · lia
        | right i =>
          simp only [Fin.val_natAdd] at hi
          have : Fin.mk (n := m + n) (m + ↑i + (k + m)) (by lia) =
              Fin.natAdd m ⟨↑i + (k + m), by lia⟩ := Fin.ext (by simp; lia)
          simp only [Fin.addCases_right, Fin.val_natAdd, sub_eq_self, this]
          rw [if_neg, mul_zero]
          lia
      lia
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : (i : ℕ) → Matrix (Fin (m + n)) (Fin (m + n)) R :=
  fun (i : ℕ) ↦
    (Matrix.of : (a : Fin (m + n) → Fin (m + n) → R) → Matrix (Fin (m + n)) (Fin (m + n)) R) fun (j₁ j₂ : Fin (m + n)) ↦
      if (↑j₂ : ℕ) < i then M₁ j₁ j₂ else M₂ j₁ j₂
⊢ f.resultant (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n = f.resultant g m n
have this : ∀ (i : ℕ) (hi : i ≤ m), (M i).det = M₂.det
Tactic: have (i : ℕ) (hi : i ≤ m) : (M i).det = M₂.det := by
    induction i with
    | zero => simp [M]; rfl
    | succ i IH =>
      rw [← IH (by lia), ← Matrix.det_updateCol_add_smul_self (i := ⟨i, by lia⟩)
        (j := ⟨i + k + m, by lia⟩) (c := -r) (M (i + 1)) (by simp; lia)]
      congr 1
      ext j₁ j₂
      simp only [Matrix.of_apply, lt_add_iff_pos_right, zero_lt_one, ↓reduceIte, add_assoc,
        add_lt_add_iff_left, Nat.lt_one_iff, Nat.add_eq_zero_iff, hm, and_false, smul_eq_mul,
        Matrix.updateCol_apply, Fin.ext_iff, M, M₂, neg_mul, ← sub_eq_add_neg]
      obtain rfl | h := eq_or_ne ↑j₂ i
      · simp only [↓reduceIte, sylvester, Set.mem_Icc, coeff_add, Fin.eta, Matrix.of_apply,
          lt_self_iff_false, M₁]
        induction j₂ using Fin.addCases with
        | left j₂ =>
          dsimp at hi
          have : Fin.mk (n := m + n) (↑j₂ + (k + m)) (by lia) = .natAdd m ⟨j₂ + k, by lia⟩ :=
            Fin.ext (by simp; lia)
          simp only [Fin.addCases_left, Fin.val_castAdd, this, Fin.addCases_right, mul_ite,
            mul_zero, ← C_mul_X_pow_eq_monomial, ← mul_assoc, coeff_mul_X_pow', ite_add_zero,
            coeff_mul_C, add_assoc, add_eq_left, ← ite_and, ← mul_comm r, tsub_add_eq_tsub_tsub,
            add_sub_assoc, sub_eq_zero]
          split_ifs with h₁ h₂ h₂ <;> try rfl
          · rw [coeff_eq_zero_of_natDegree_lt, mul_zero]
            exact hf.trans_lt (by lia)
          · lia
        | right i =>
          simp only [Fin.val_natAdd] at hi
          have : Fin.mk (n := m + n) (m + ↑i + (k + m)) (by lia) =
              Fin.natAdd m ⟨↑i + (k + m), by lia⟩ := Fin.ext (by simp; lia)
          simp only [Fin.addCases_right, Fin.val_natAdd, sub_eq_self, this]
          rw [if_neg, mul_zero]
          lia
      lia
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : (i : ℕ) → Matrix (Fin (m + n)) (Fin (m + n)) R :=
  fun (i : ℕ) ↦
    (Matrix.of : (a : Fin (m + n) → Fin (m + n) → R) → Matrix (Fin (m + n)) (Fin (m + n)) R) fun (j₁ j₂ : Fin (m + n)) ↦
      if (↑j₂ : ℕ) < i then M₁ j₁ j₂ else M₂ j₁ j₂
this : ∀ (i : ℕ) (hi : i ≤ m), (M i).det = M₂.det
⊢ f.resultant (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n = f.resultant g m n
have inr : (f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n).det = (M m).det
Tactic: rw [resultant, resultant, ← this m le_rfl]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : (i : ℕ) → Matrix (Fin (m + n)) (Fin (m + n)) R :=
  fun (i : ℕ) ↦
    (Matrix.of : (a : Fin (m + n) → Fin (m + n) → R) → Matrix (Fin (m + n)) (Fin (m + n)) R) fun (j₁ j₂ : Fin (m + n)) ↦
      if (↑j₂ : ℕ) < i then M₁ j₁ j₂ else M₂ j₁ j₂
this : ∀ (i : ℕ) (hi : i ≤ m), (M i).det = M₂.det
⊢ (f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n).det = (M m).det
have inr : f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n = M m
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : (i : ℕ) → Matrix (Fin (m + n)) (Fin (m + n)) R :=
  fun (i : ℕ) ↦
    (Matrix.of : (a : Fin (m + n) → Fin (m + n) → R) → Matrix (Fin (m + n)) (Fin (m + n)) R) fun (j₁ j₂ : Fin (m + n)) ↦
      if (↑j₂ : ℕ) < i then M₁ j₁ j₂ else M₂ j₁ j₂
this : ∀ (i : ℕ) (hi : i ≤ m), (M i).det = M₂.det
⊢ f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n = M m
have inr : ∀ (i j : Fin (m + n)),
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n i j = M m i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : (i : ℕ) → Matrix (Fin (m + n)) (Fin (m + n)) R :=
  fun (i : ℕ) ↦
    (Matrix.of : (a : Fin (m + n) → Fin (m + n) → R) → Matrix (Fin (m + n)) (Fin (m + n)) R) fun (j₁ j₂ : Fin (m + n)) ↦
      if (↑j₂ : ℕ) < i then M₁ j₁ j₂ else M₂ j₁ j₂
this : ∀ (i : ℕ) (hi : i ≤ m), (M i).det = M₂.det
i j : Fin (m + n)
⊢ f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n i j = M m i j
have inr : ∀ (i_1 : Fin m),
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n i (Fin.castAdd n i_1) =
    M m i (Fin.castAdd n i_1)
Tactic: induction j using Fin.addCases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : (i : ℕ) → Matrix (Fin (m + n)) (Fin (m + n)) R :=
  fun (i : ℕ) ↦
    (Matrix.of : (a : Fin (m + n) → Fin (m + n) → R) → Matrix (Fin (m + n)) (Fin (m + n)) R) fun (j₁ j₂ : Fin (m + n)) ↦
      if (↑j₂ : ℕ) < i then M₁ j₁ j₂ else M₂ j₁ j₂
this : ∀ (i : ℕ) (hi : i ≤ m), (M i).det = M₂.det
i j : Fin (m + n)
inr :
  ∀ (i_1 : Fin m),
    f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n i (Fin.castAdd n i_1) =
      M m i (Fin.castAdd n i_1)
⊢ f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n i j = M m i j
have inr₁ : ∀ (i_1 : Fin n),
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n i (Fin.natAdd m i_1) =
    M m i (Fin.natAdd m i_1)
Tactic: induction j using Fin.addCases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
⊢ p.support ⊆ Finset.range (n - m + 1)
have simp : ∀ ⦃x : ℕ⦄, x ∈ p.support → x < n - m + 1
Tactic: simp only [Finset.subset_iff, Finset.mem_range]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
f g p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
⊢ f.resultant (g + f * p) m n = f.resultant g m n
have H : p.support ⊆ Finset.range (n - m + 1)
Tactic: have H : p.support ⊆ Finset.range (n - m + 1) := by
    simp only [Finset.subset_iff, Finset.mem_range]
    exact fun x hx ↦ (le_natDegree_of_mem_supp _ hx).trans_lt (by lia)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
H : p.support ⊆ Finset.range (n - m + 1)
⊢ f.resultant (g + f * p) m n = f.resultant g m n
have rw : f.resultant (g + f * ∑ n ∈ Finset.range (n - m + 1), (monomial n : (a : R) → R[X]) (p.coeff n)) m n = f.resultant g m n
Tactic: rw [← p.sum_monomial_eq, Polynomial.sum_eq_of_subset _ (by simp) H]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
H : p.support ⊆ Finset.range (n - m + 1)
⊢ f.resultant (g + f * ∑ n ∈ Finset.range (n - m + 1), (monomial n : (a : R) → R[X]) (p.coeff n)) m n =
    f.resultant g m n
have set : let k := n - m + 1;
∀ (H : p.support ⊆ Finset.range k),
  f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n : (a : R) → R[X]) (p.coeff n)) m n = f.resultant g m n
Tactic: set k := n - m + 1
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
f g p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
k : ℕ := n - m + 1
H : p.support ⊆ Finset.range k
⊢ f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n : (a : R) → R[X]) (p.coeff n)) m n = f.resultant g m n
have H₁ : k ≤ n - m + 1
Tactic: replace H := show k ≤ n - m + 1 from le_rfl
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
k : ℕ := n - m + 1
H : k ≤ n - m + 1
⊢ f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n : (a : R) → R[X]) (p.coeff n)) m n = f.resultant g m n
have clear_value : ∀ (k : ℕ) (H : k ≤ n - m + 1),
  f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n : (a : R) → R[X]) (p.coeff n)) m n = f.resultant g m n
Tactic: clear_value k
Cleared hypotheses: k, H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
g : R[X]
H : 0 ≤ n - m + 1
⊢ f.resultant (g + f * 0) m n = f.resultant g m n
have zero : f.resultant (g + 0) m n = f.resultant g m n
Tactic: rw [mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
g : R[X]
H : 0 ≤ n - m + 1
zero : f.resultant (g + 0) m n = f.resultant g m n
⊢ f.resultant (g + f * 0) m n = f.resultant g m n
have zero₁ : f.resultant g m n = f.resultant g m n
Tactic: rw [mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
k : ℕ
IH :
  ∀ (g : R[X]) (H : k ≤ n - m + 1),
    f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n : (a : R) → R[X]) (p.coeff n)) m n = f.resultant g m n
g : R[X]
H : k + 1 ≤ n - m + 1
⊢ f.resultant (g + f * ∑ n ∈ Finset.range (k + 1), (monomial n : (a : R) → R[X]) (p.coeff n)) m n = f.resultant g m n
have succ : k ≤ n - m + 1
Tactic: rw [Finset.sum_range_succ, mul_add, ← add_assoc, resultant_add_mul_monomial_right, IH]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
k : ℕ
IH :
  ∀ (g : R[X]) (H : k ≤ n - m + 1),
    f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n : (a : R) → R[X]) (p.coeff n)) m n = f.resultant g m n
g : R[X]
H : k + 1 ≤ n - m + 1
succ : k ≤ n - m + 1
⊢ f.resultant (g + f * ∑ n ∈ Finset.range (k + 1), (monomial n : (a : R) → R[X]) (p.coeff n)) m n = f.resultant g m n
have succ₁ : k + m ≤ n
Tactic: rw [Finset.sum_range_succ, mul_add, ← add_assoc, resultant_add_mul_monomial_right, IH]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
k : ℕ
H : k ≤ n - m + 1
⊢ f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n : (a : R) → R[X]) (p.coeff n)) m n = f.resultant g m n
have zero : ∀ (g : R[X]) (H : 0 ≤ n - m + 1),
  f.resultant (g + f * ∑ n ∈ Finset.range 0, (monomial n : (a : R) → R[X]) (p.coeff n)) m n = f.resultant g m n
Tactic: induction k generalizing g with
  | zero =>
    simp only [Finset.range_zero, Finset.sum_empty]
    rw [mul_zero, add_zero]
  | succ k IH =>
    rw [Finset.sum_range_succ, mul_add, ← add_assoc, resultant_add_mul_monomial_right, IH] <;> lia
Cleared hypotheses: g, k, H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
k : ℕ
H : k ≤ n - m + 1
zero :
  ∀ (g : R[X]) (H : 0 ≤ n - m + 1),
    f.resultant (g + f * ∑ n ∈ Finset.range 0, (monomial n : (a : R) → R[X]) (p.coeff n)) m n = f.resultant g m n
⊢ f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n : (a : R) → R[X]) (p.coeff n)) m n = f.resultant g m n
have succ : ∀ (k : ℕ)
  (IH :
    ∀ (g : R[X]) (H : k ≤ n - m + 1),
      f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n : (a : R) → R[X]) (p.coeff n)) m n = f.resultant g m n)
  (g : R[X]) (H : k + 1 ≤ n - m + 1),
  f.resultant (g + f * ∑ n ∈ Finset.range (k + 1), (monomial n : (a : R) → R[X]) (p.coeff n)) m n = f.resultant g m n
Tactic: induction k generalizing g with
  | zero =>
    simp only [Finset.range_zero, Finset.sum_empty]
    rw [mul_zero, add_zero]
  | succ k IH =>
    rw [Finset.sum_range_succ, mul_add, ← add_assoc, resultant_add_mul_monomial_right, IH] <;> lia
Cleared hypotheses: g, k, H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g p : R[X]
m n : ℕ
hk : p.natDegree + n ≤ m
hg : g.natDegree ≤ n
⊢ (f + g * p).resultant g m n = f.resultant g m n
have rw : HPow.hPow (α := R) (β := ℕ) (-1) 2 ^ (n * m) * f.resultant g m n = f.resultant g m n
Tactic: rw [resultant_comm, resultant_add_mul_right _ _ _ _ _ hk hg, resultant_comm,
    ← mul_assoc, ← pow_add, mul_comm m n, ← two_mul, pow_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n : ℕ
r : R
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) g) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : (i : ℕ) → Matrix (Fin (m + n)) (Fin (m + n)) R :=
  fun (i : ℕ) ↦
    (Matrix.of : (a : Fin (m + n) → Fin (m + n) → R) → Matrix (Fin (m + n)) (Fin (m + n)) R) fun (j₁ j₂ : Fin (m + n)) ↦
      if (↑j₂ : ℕ) < i then M₁ j₁ j₂ else M₂ j₁ j₂
hi : 0 ≤ m
⊢ (M 0).det = HPow.hPow (β := ℕ) r 0 * M₂.det
have zero : Matrix.det (n := Fin (m + n))
    ((Matrix.of : (a : Fin (m + n) → Fin (m + n) → R) → Matrix (Fin (m + n)) (Fin (m + n)) R)
      fun (j₁ j₂ : Fin (m + n)) ↦ M₂ j₁ j₂) =
  M₂.det
Tactic: simp [M]