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]
m n : ℕ
⊢ (↑(↑(∏ i : Fin (n + m),
              ∏ j ∈ Finset.Ioi i,
                if
                    Fin.cast ⋯
                        ((finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n))
                          (Sum.swap ((Equiv.symm finSumFinEquiv : (a : Fin (n + m)) → Fin n ⊕ Fin m) i))) <
                      Fin.cast ⋯
                        ((finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n))
                          (Sum.swap ((Equiv.symm finSumFinEquiv : (a : Fin (n + m)) → Fin n ⊕ Fin m) j))) then
                  1
                else -1) :
          ℤ) :
      R) =
    HPow.hPow (α := R) (-1) (m * n)
have e_a : (∏ x : Fin (n + m),
    ∏ x_1 ∈ Finset.Ioi x,
      if
          LT.lt (α := Fin (m + n))
            ((finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n))
                (Sum.swap ((Equiv.symm finSumFinEquiv : (a : Fin (n + m)) → Fin n ⊕ Fin m) x)) :
              Fin (m + n))
            ((finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n))
                (Sum.swap ((Equiv.symm finSumFinEquiv : (a : Fin (n + m)) → Fin n ⊕ Fin m) x_1)) :
              Fin (m + n)) then
        1
      else -1) =
  HPow.hPow (α := R) (-1) (m * n)
Tactic: simp only [Fin.cast_lt_cast, Units.coe_prod, apply_ite, Units.val_one, Units.val_neg,
    Int.reduceNeg, Int.cast_prod, Int.cast_one, Int.cast_neg]
-- 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 : ℕ
⊢ (∏ x : Fin (n + m),
      ∏ x_1 ∈ Finset.Ioi x,
        if
            LT.lt (α := Fin (m + n))
              ((finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n))
                  (Sum.swap ((Equiv.symm finSumFinEquiv : (a : Fin (n + m)) → Fin n ⊕ Fin m) x)) :
                Fin (m + n))
              ((finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n))
                  (Sum.swap ((Equiv.symm finSumFinEquiv : (a : Fin (n + m)) → Fin n ⊕ Fin m) x_1)) :
                Fin (m + n)) then
          1
        else -1) =
    HPow.hPow (α := R) (-1) (m * n)
have e_a : ∏ x : Fin n ⊕ Fin m,
    Finset.prod (ι := Fin n ⊕ Fin m)
      (Finset.map (Equiv.toEmbedding (Equiv.symm finSumFinEquiv))
        (Finset.Ioi ((finSumFinEquiv : (a : Fin n ⊕ Fin m) → Fin (n + m)) x)))
      ((fun (x_1 : Fin (n + m)) ↦
          if
              LT.lt (α := Fin (m + n))
                ((finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n))
                    (Sum.swap
                      ((Equiv.symm finSumFinEquiv : (a : Fin (n + m)) → Fin n ⊕ Fin m)
                        ((finSumFinEquiv : (a : Fin n ⊕ Fin m) → Fin (n + m)) x : Fin (n + m)))) :
                  Fin (m + n))
                ((finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n))
                    (Sum.swap ((Equiv.symm finSumFinEquiv : (a : Fin (n + m)) → Fin n ⊕ Fin m) x_1)) :
                  Fin (m + n)) then
            1
          else -1) ∘
        (⇑(Equiv.symm (Equiv.symm finSumFinEquiv)) : (a : Fin n ⊕ Fin m) → Fin (n + m))) =
  HPow.hPow (α := R) (-1) (m * n)
Tactic: simp_rw [← finSumFinEquiv.prod_comp, ← Finset.prod_map_equiv finSumFinEquiv.symm]
-- 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 : ℕ
⊢ ∏ x : Fin n ⊕ Fin m,
      Finset.prod (ι := Fin n ⊕ Fin m)
        (Finset.map (Equiv.toEmbedding (Equiv.symm finSumFinEquiv))
          (Finset.Ioi ((finSumFinEquiv : (a : Fin n ⊕ Fin m) → Fin (n + m)) x)))
        ((fun (x_1 : Fin (n + m)) ↦
            if
                LT.lt (α := Fin (m + n))
                  ((finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n))
                      (Sum.swap
                        ((Equiv.symm finSumFinEquiv : (a : Fin (n + m)) → Fin n ⊕ Fin m)
                          ((finSumFinEquiv : (a : Fin n ⊕ Fin m) → Fin (n + m)) x : Fin (n + m)))) :
                    Fin (m + n))
                  ((finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n))
                      (Sum.swap ((Equiv.symm finSumFinEquiv : (a : Fin (n + m)) → Fin n ⊕ Fin m) x_1)) :
                    Fin (m + n)) then
              1
            else -1) ∘
          (⇑(Equiv.symm (Equiv.symm finSumFinEquiv)) : (a : Fin n ⊕ Fin m) → Fin (n + m))) =
    HPow.hPow (α := R) (-1) (m * n)
have e_a : HMul.hMul (α := R)
    (∏ x : Fin n,
      HMul.hMul (α := R) (∏ x : Fin n, if False then -1 else 1)
        (∏ x_1 : Fin m, if (↑x : ℕ) < n + (↑x_1 : ℕ) ∧ ¬m + (↑x : ℕ) < (↑x_1 : ℕ) then -1 else 1))
    (∏ x : Fin m,
      HMul.hMul (α := R) (∏ x_1 : Fin n, if n + (↑x : ℕ) < (↑x_1 : ℕ) ∧ ¬(↑x : ℕ) < m + (↑x_1 : ℕ) then -1 else 1)
        (∏ x : Fin m, if False then -1 else 1)) =
  HPow.hPow (α := R) (-1) (m * n)
Tactic: simp only [Equiv.symm_apply_apply, ← Fin.val_fin_lt, Equiv.symm_symm, Function.comp_apply,
    ← Finset.prod_ite_mem_eq (Finset.map _ _), Finset.mem_map_equiv, Finset.mem_Ioi,
    Fintype.prod_sum_type, finSumFinEquiv_apply_left, Fin.val_castAdd, Sum.swap_inl,
    finSumFinEquiv_apply_right, Fin.val_natAdd, Sum.swap_inr, add_lt_add_iff_left,
    ← ite_not (α := R) (p := _ < _) (y := 1), ← ite_and, and_not_self]
-- 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 : ℕ
⊢ f.resultant g m n = HPow.hPow (α := R) (-1) (m * n) * g.resultant f n m
have rw : (f.sylvester g m n).det = HPow.hPow (α := R) (-1) (m * n) * g.resultant f n m
Tactic: classical
  rw [resultant, resultant, sylvester_comm, Matrix.det_reindex, Equiv.Perm.sign_eq_prod_prod_Ioi]
  congr 1
  dsimp
  simp only [Fin.cast_lt_cast, Units.coe_prod, apply_ite, Units.val_one, Units.val_neg,
    Int.reduceNeg, Int.cast_prod, Int.cast_one, Int.cast_neg]
  simp_rw [← finSumFinEquiv.prod_comp, ← Finset.prod_map_equiv finSumFinEquiv.symm]
  simp only [Equiv.symm_apply_apply, ← Fin.val_fin_lt, Equiv.symm_symm, Function.comp_apply,
    ← Finset.prod_ite_mem_eq (Finset.map _ _), Finset.mem_map_equiv, Finset.mem_Ioi,
    Fintype.prod_sum_type, finSumFinEquiv_apply_left, Fin.val_castAdd, Sum.swap_inl,
    finSumFinEquiv_apply_right, Fin.val_natAdd, Sum.swap_inr, add_lt_add_iff_left,
    ← ite_not (α := R) (p := _ < _) (y := 1), ← ite_and, and_not_self]
  simp [(Fin.isLt _).trans_le, (Fin.isLt _).le.trans, 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 : ℕ
rw : (f.sylvester g m n).det = HPow.hPow (α := R) (-1) (m * n) * g.resultant f n m
⊢ f.resultant g m n = HPow.hPow (α := R) (-1) (m * n) * g.resultant f n m
have rw₁ : (f.sylvester g m n).det = HPow.hPow (α := R) (-1) (m * n) * (g.sylvester f n m).det
Tactic: classical
  rw [resultant, resultant, sylvester_comm, Matrix.det_reindex, Equiv.Perm.sign_eq_prod_prod_Ioi]
  congr 1
  dsimp
  simp only [Fin.cast_lt_cast, Units.coe_prod, apply_ite, Units.val_one, Units.val_neg,
    Int.reduceNeg, Int.cast_prod, Int.cast_one, Int.cast_neg]
  simp_rw [← finSumFinEquiv.prod_comp, ← Finset.prod_map_equiv finSumFinEquiv.symm]
  simp only [Equiv.symm_apply_apply, ← Fin.val_fin_lt, Equiv.symm_symm, Function.comp_apply,
    ← Finset.prod_ite_mem_eq (Finset.map _ _), Finset.mem_map_equiv, Finset.mem_Ioi,
    Fintype.prod_sum_type, finSumFinEquiv_apply_left, Fin.val_castAdd, Sum.swap_inl,
    finSumFinEquiv_apply_right, Fin.val_natAdd, Sum.swap_inr, add_lt_add_iff_left,
    ← ite_not (α := R) (p := _ < _) (y := 1), ← ite_and, and_not_self]
  simp [(Fin.isLt _).trans_le, (Fin.isLt _).le.trans, 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 : ℕ
rw : (f.sylvester g m n).det = HPow.hPow (α := R) (-1) (m * n) * g.resultant f n m
rw₁ : (f.sylvester g m n).det = HPow.hPow (α := R) (-1) (m * n) * (g.sylvester f n m).det
⊢ f.resultant g m n = HPow.hPow (α := R) (-1) (m * n) * g.resultant f n m
have rw₂ : Matrix.det (n := Fin (m + n))
    ((Matrix.reindex (finCongr sorry)
          (Equiv.trans (Equiv.symm finSumFinEquiv) (Equiv.trans (Equiv.sumComm (Fin n) (Fin m)) finSumFinEquiv)) :
        (a : Matrix (Fin (n + m)) (Fin (n + m)) R) → Matrix (Fin (m + n)) (Fin (m + n)) R)
      (g.sylvester f n m)) =
  HPow.hPow (α := R) (-1) (m * n) * (g.sylvester f n m).det
Tactic: classical
  rw [resultant, resultant, sylvester_comm, Matrix.det_reindex, Equiv.Perm.sign_eq_prod_prod_Ioi]
  congr 1
  dsimp
  simp only [Fin.cast_lt_cast, Units.coe_prod, apply_ite, Units.val_one, Units.val_neg,
    Int.reduceNeg, Int.cast_prod, Int.cast_one, Int.cast_neg]
  simp_rw [← finSumFinEquiv.prod_comp, ← Finset.prod_map_equiv finSumFinEquiv.symm]
  simp only [Equiv.symm_apply_apply, ← Fin.val_fin_lt, Equiv.symm_symm, Function.comp_apply,
    ← Finset.prod_ite_mem_eq (Finset.map _ _), Finset.mem_map_equiv, Finset.mem_Ioi,
    Fintype.prod_sum_type, finSumFinEquiv_apply_left, Fin.val_castAdd, Sum.swap_inl,
    finSumFinEquiv_apply_right, Fin.val_natAdd, Sum.swap_inr, add_lt_add_iff_left,
    ← ite_not (α := R) (p := _ < _) (y := 1), ← ite_and, and_not_self]
  simp [(Fin.isLt _).trans_le, (Fin.isLt _).le.trans, 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 : ℕ
rw : (f.sylvester g m n).det = HPow.hPow (α := R) (-1) (m * n) * g.resultant f n m
rw₁ : (f.sylvester g m n).det = HPow.hPow (α := R) (-1) (m * n) * (g.sylvester f n m).det
rw₂ :
  Matrix.det (n := Fin (m + n))
      ((Matrix.reindex (finCongr ⋯)
            (Equiv.trans (Equiv.symm finSumFinEquiv) (Equiv.trans (Equiv.sumComm (Fin n) (Fin m)) finSumFinEquiv)) :
          (a : Matrix (Fin (n + m)) (Fin (n + m)) R) → Matrix (Fin (m + n)) (Fin (m + n)) R)
        (g.sylvester f n m)) =
    HPow.hPow (α := R) (-1) (m * n) * (g.sylvester f n m).det
⊢ f.resultant g m n = HPow.hPow (α := R) (-1) (m * n) * g.resultant f n m
have rw₃ : (↑(↑((Equiv.Perm.sign : (a : Equiv.Perm (Fin (n + m))) → ℤˣ)
              (Equiv.trans
                (Equiv.trans (Equiv.symm finSumFinEquiv) (Equiv.trans (Equiv.sumComm (Fin n) (Fin m)) finSumFinEquiv))
                (Equiv.symm (finCongr sorry)))) :
          ℤ) :
      R) *
    (g.sylvester f n m).det =
  HPow.hPow (α := R) (-1) (m * n) * (g.sylvester f n m).det
Tactic: classical
  rw [resultant, resultant, sylvester_comm, Matrix.det_reindex, Equiv.Perm.sign_eq_prod_prod_Ioi]
  congr 1
  dsimp
  simp only [Fin.cast_lt_cast, Units.coe_prod, apply_ite, Units.val_one, Units.val_neg,
    Int.reduceNeg, Int.cast_prod, Int.cast_one, Int.cast_neg]
  simp_rw [← finSumFinEquiv.prod_comp, ← Finset.prod_map_equiv finSumFinEquiv.symm]
  simp only [Equiv.symm_apply_apply, ← Fin.val_fin_lt, Equiv.symm_symm, Function.comp_apply,
    ← Finset.prod_ite_mem_eq (Finset.map _ _), Finset.mem_map_equiv, Finset.mem_Ioi,
    Fintype.prod_sum_type, finSumFinEquiv_apply_left, Fin.val_castAdd, Sum.swap_inl,
    finSumFinEquiv_apply_right, Fin.val_natAdd, Sum.swap_inr, add_lt_add_iff_left,
    ← ite_not (α := R) (p := _ < _) (y := 1), ← ite_and, and_not_self]
  simp [(Fin.isLt _).trans_le, (Fin.isLt _).le.trans, 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 : ℕ
rw : (f.sylvester g m n).det = HPow.hPow (α := R) (-1) (m * n) * g.resultant f n m
rw₁ : (f.sylvester g m n).det = HPow.hPow (α := R) (-1) (m * n) * (g.sylvester f n m).det
rw₂ :
  Matrix.det (n := Fin (m + n))
      ((Matrix.reindex (finCongr ⋯)
            (Equiv.trans (Equiv.symm finSumFinEquiv) (Equiv.trans (Equiv.sumComm (Fin n) (Fin m)) finSumFinEquiv)) :
          (a : Matrix (Fin (n + m)) (Fin (n + m)) R) → Matrix (Fin (m + n)) (Fin (m + n)) R)
        (g.sylvester f n m)) =
    HPow.hPow (α := R) (-1) (m * n) * (g.sylvester f n m).det
rw₃ :
  (↑(↑((Equiv.Perm.sign : (a : Equiv.Perm (Fin (n + m))) → ℤˣ)
                (Equiv.trans
                  (Equiv.trans (Equiv.symm finSumFinEquiv) (Equiv.trans (Equiv.sumComm (Fin n) (Fin m)) finSumFinEquiv))
                  (Equiv.symm (finCongr ⋯)))) :
            ℤ) :
        R) *
      (g.sylvester f n m).det =
    HPow.hPow (α := R) (-1) (m * n) * (g.sylvester f n m).det
⊢ f.resultant g m n = HPow.hPow (α := R) (-1) (m * n) * g.resultant f n m
have rw₄ : (↑(↑(∏ i : Fin (n + m),
              ∏ j ∈ Finset.Ioi i,
                if
                    LT.lt (α := Fin (n + m))
                      ((Equiv.trans
                              (Equiv.trans (Equiv.symm finSumFinEquiv)
                                (Equiv.trans (Equiv.sumComm (Fin n) (Fin m)) finSumFinEquiv))
                              (Equiv.symm (finCongr sorry)) :
                            (a : Fin (n + m)) → Fin (n + m))
                          i :
                        Fin (n + m))
                      ((Equiv.trans
                              (Equiv.trans (Equiv.symm finSumFinEquiv)
                                (Equiv.trans (Equiv.sumComm (Fin n) (Fin m)) finSumFinEquiv))
                              (Equiv.symm (finCongr sorry)) :
                            (a : Fin (n + m)) → Fin (n + m))
                          j :
                        Fin (n + m)) then
                  1
                else -1) :
          ℤ) :
      R) *
    (g.sylvester f n m).det =
  HPow.hPow (α := R) (-1) (m * n) * (g.sylvester f n m).det
Tactic: classical
  rw [resultant, resultant, sylvester_comm, Matrix.det_reindex, Equiv.Perm.sign_eq_prod_prod_Ioi]
  congr 1
  dsimp
  simp only [Fin.cast_lt_cast, Units.coe_prod, apply_ite, Units.val_one, Units.val_neg,
    Int.reduceNeg, Int.cast_prod, Int.cast_one, Int.cast_neg]
  simp_rw [← finSumFinEquiv.prod_comp, ← Finset.prod_map_equiv finSumFinEquiv.symm]
  simp only [Equiv.symm_apply_apply, ← Fin.val_fin_lt, Equiv.symm_symm, Function.comp_apply,
    ← Finset.prod_ite_mem_eq (Finset.map _ _), Finset.mem_map_equiv, Finset.mem_Ioi,
    Fintype.prod_sum_type, finSumFinEquiv_apply_left, Fin.val_castAdd, Sum.swap_inl,
    finSumFinEquiv_apply_right, Fin.val_natAdd, Sum.swap_inr, add_lt_add_iff_left,
    ← ite_not (α := R) (p := _ < _) (y := 1), ← ite_and, and_not_self]
  simp [(Fin.isLt _).trans_le, (Fin.isLt _).le.trans, 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 : ℕ
⊢ f.resultant g m 0 = g.coeff 0 ^ m
have rw : HPow.hPow (α := R) (-1) (m * 0) * g.resultant f 0 m = g.coeff 0 ^ m
Tactic: rw [resultant_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
m n : ℕ
⊢ f.resultant 0 m n = HPow.hPow (α := R) 0 m * f.coeff 0 ^ n
have zero : f.resultant 0 0 n = HPow.hPow (α := R) (β := ℕ) 0 0 * f.coeff 0 ^ n
Tactic: obtain _ | m := m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
m n : ℕ
zero : f.resultant 0 0 n = HPow.hPow (α := R) (β := ℕ) 0 0 * f.coeff 0 ^ n
⊢ f.resultant 0 m n = HPow.hPow (α := R) 0 m * f.coeff 0 ^ n
have succ : ∀ (m : ℕ), f.resultant 0 (m + 1) n = HPow.hPow (α := R) 0 (m + 1) * f.coeff 0 ^ n
Tactic: obtain _ | m := m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
n m : ℕ
⊢ f.resultant 0 (m + 1) n = HPow.hPow (α := R) 0 (m + 1) * f.coeff 0 ^ n
have this : ∀ (i : Fin (m + 1 + n)), f.sylvester 0 (m + 1) n i (⟨0, sorry⟩ : Fin (m + 1 + n)) = 0
Tactic: have (i : Fin (m + 1 + n)) : sylvester f 0 (m + 1) n i ⟨0, by lia⟩ = 0 := by
    simp [sylvester, show (0 : Fin (m + 1 + n)) = Fin.castAdd _ 0 from rfl, Fin.addCases_left]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
m n : ℕ
⊢ resultant 0 g m n = HPow.hPow (α := R) 0 n * g.coeff 0 ^ m
have rw : HPow.hPow (α := R) (-1) (m * n) * (HPow.hPow (α := R) 0 n * g.coeff 0 ^ m) = HPow.hPow (α := R) 0 n * g.coeff 0 ^ m
Tactic: rw [resultant_comm, resultant_zero_right]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
m n : ℕ
⊢ HPow.hPow (α := R) (-1) (m * n) * (HPow.hPow (α := R) 0 n * g.coeff 0 ^ m) = HPow.hPow (α := R) 0 n * g.coeff 0 ^ m
have zero : HPow.hPow (α := R) (-1) (m * 0) * (HPow.hPow (α := R) (β := ℕ) 0 0 * g.coeff 0 ^ m) =
  HPow.hPow (α := R) (β := ℕ) 0 0 * g.coeff 0 ^ m
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
m n : ℕ
zero :
  HPow.hPow (α := R) (-1) (m * 0) * (HPow.hPow (α := R) (β := ℕ) 0 0 * g.coeff 0 ^ m) =
    HPow.hPow (α := R) (β := ℕ) 0 0 * g.coeff 0 ^ m
⊢ HPow.hPow (α := R) (-1) (m * n) * (HPow.hPow (α := R) 0 n * g.coeff 0 ^ m) = HPow.hPow (α := R) 0 n * g.coeff 0 ^ m
have succ : ∀ (n : ℕ),
  HPow.hPow (α := R) (-1) (m * (n + 1)) * (HPow.hPow (α := R) 0 (n + 1) * g.coeff 0 ^ m) =
    HPow.hPow (α := R) 0 (n + 1) * g.coeff 0 ^ m
Tactic: cases n
Cleared hypotheses: n
-- 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
⊢ 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 inl : ∀ (hk : k + 0 ≤ n) (hf : f.natDegree ≤ 0),
  f.resultant (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) 0 n = f.resultant g 0 n
Tactic: obtain rfl | hm := eq_or_ne m 0
Cleared hypotheses: m, hk, hf
-- 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
inl :
  ∀ (hk : k + 0 ≤ n) (hf : f.natDegree ≤ 0),
    f.resultant (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) 0 n = f.resultant g 0 n
⊢ 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 : ∀ (hm : m ≠ 0),
  f.resultant (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) m n = f.resultant g m n
Tactic: obtain rfl | hm := eq_or_ne m 0
-- 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
n k : ℕ
hk : k + 0 ≤ n
hf : f.natDegree ≤ 0
⊢ f.resultant (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) 0 n = f.resultant g 0 n
have inl : ∀ (q : R) (hf : natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) q) ≤ 0),
  resultant ((C : (a : R) → R[X]) q)
      (g + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) q : R[X]) ((monomial k : (a : R) → R[X]) r : R[X])) 0
      n =
    resultant ((C : (a : R) → R[X]) q) g 0 n
Tactic: obtain ⟨q, rfl⟩ := natDegree_eq_zero.mp (le_zero_iff.mp hf)
Cleared hypotheses: f, hf
-- 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₂
hi : 0 ≤ m
⊢ (M 0).det = 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]
-- 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 : ℕ
IH : ∀ (hi : i ≤ m), (M i).det = M₂.det
hi : i + 1 ≤ m
⊢ (⟨i, ⋯⟩ : Fin (m + n)) ≠ ⟨i + k + m, ⋯⟩
have simp : ¬i = i + k + m
Tactic: simp
-- 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 : ℕ
IH : ∀ (hi : i ≤ m), (M i).det = M₂.det
hi : i + 1 ≤ m
⊢ (M (i + 1)).det = M₂.det
have succ : ((M (i + 1)).updateCol (⟨i, sorry⟩ : Fin (m + n)) fun (k_1 : Fin (m + n)) ↦
      M (i + 1) k_1 (⟨i, sorry⟩ : Fin (m + n)) + -r • M (i + 1) k_1 (⟨i + k + m, sorry⟩ : Fin (m + n))).det =
  (M i).det
Tactic: 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)]
-- 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 : ℕ
IH : ∀ (hi : i ≤ m), (M i).det = M₂.det
hi : i + 1 ≤ m
⊢ ((M (i + 1)).updateCol (⟨i, ⋯⟩ : Fin (m + n)) fun (k_1 : Fin (m + n)) ↦
        M (i + 1) k_1 (⟨i, ⋯⟩ : Fin (m + n)) + -r • M (i + 1) k_1 (⟨i + k + m, ⋯⟩ : Fin (m + n))).det =
    (M i).det
have succ : ((M (i + 1)).updateCol (⟨i, sorry⟩ : Fin (m + n)) fun (k_1 : Fin (m + n)) ↦
    M (i + 1) k_1 (⟨i, sorry⟩ : Fin (m + n)) + -r • M (i + 1) k_1 (⟨i + k + m, sorry⟩ : Fin (m + n))) =
  M i
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₂
i : ℕ
IH : ∀ (hi : i ≤ m), (M i).det = M₂.det
hi : i + 1 ≤ m
⊢ ((M (i + 1)).updateCol (⟨i, ⋯⟩ : Fin (m + n)) fun (k_1 : Fin (m + n)) ↦
      M (i + 1) k_1 (⟨i, ⋯⟩ : Fin (m + n)) + -r • M (i + 1) k_1 (⟨i + k + m, ⋯⟩ : Fin (m + n))) =
    M i
have succ : ∀ (j₁ j₂ : Fin (m + n)),
  (M (i + 1)).updateCol (⟨i, sorry⟩ : Fin (m + n))
      (fun (k_1 : Fin (m + n)) ↦
        M (i + 1) k_1 (⟨i, sorry⟩ : Fin (m + n)) + -r • M (i + 1) k_1 (⟨i + k + m, sorry⟩ : Fin (m + n)))
      j₁ j₂ =
    M i j₁ j₂
Tactic: ext j₁ j₂