awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h : j = f.natDegree - 2
h_1 : j < f.natDegree - 1
h_2 : ¬(j ≤ 2 * f.natDegree - 2 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2)
neg : f.coeff 1 = 0
⊢ f.coeff f.natDegree = 0

Tactic:
on_goal 2 => rw [show f.natDegree = 1 by lia]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h : j = f.natDegree - 2
h_1 : ¬j < f.natDegree - 1
h_2 : j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2
⊢ f.natDegree = 1

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h : j = f.natDegree - 2
h_1 : ¬j < f.natDegree - 1
h_2 : j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2
pos :
  f.coeff 1 =
    f.coeff (HMul.hMul (α := ℕ) 2 1 - 2 - (j - HSub.hSub (α := ℕ) 1 1) + 1) *
      (↑(HMul.hMul (α := ℕ) 2 1 - 2 - (j - HSub.hSub (α := ℕ) 1 1) + 1) : R)
⊢ f.coeff f.natDegree =
    f.coeff (2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) *
      HAdd.hAdd (α := R) (↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1))) : R) 1

Tactic:
rw [← Nat.cast_one (R := R), ← Nat.cast_add, show f.natDegree = 1 by lia]

Premises used: Nat.cast_add, Nat.cast_one
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h : j = f.natDegree - 2
h_1 : ¬j < f.natDegree - 1
h_2 : j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2
⊢ f.coeff 1 =
    f.coeff (HMul.hMul (α := ℕ) 2 1 - 2 - (j - HSub.hSub (α := ℕ) 1 1) + 1) *
      (↑(HMul.hMul (α := ℕ) 2 1 - 2 - (j - HSub.hSub (α := ℕ) 1 1) + 1) : R)

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h : j = f.natDegree - 2
h_1 : ¬j < f.natDegree - 1
h_2 : j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2
⊢ f.coeff f.natDegree =
    f.coeff (2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) *
      HAdd.hAdd (α := R) (↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1))) : R) 1

Tactic:
on_goal 3 =>
      rw [← Nat.cast_one (R := R), ← Nat.cast_add, show f.natDegree = 1 by lia]
      norm_num

Premises used: Nat.cast_add, Nat.cast_one
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h : ¬j = f.natDegree - 2
h_1 : j = 2 * f.natDegree - 2
h_2 : ¬j < f.natDegree - 1
h_3 : j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2
pos :
  f.coeff f.natDegree * (↑f.natDegree : R) =
    f.coeff (2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) *
      (↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) : R)
⊢ f.coeff f.natDegree * (↑f.natDegree : R) =
    f.coeff (2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) *
      HAdd.hAdd (α := R) (↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1))) : R) 1

Tactic:
rw [← Nat.cast_one (R := R), ← Nat.cast_add]

Premises used: Nat.cast_add, Nat.cast_one
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h : ¬j = f.natDegree - 2
h_1 : j = 2 * f.natDegree - 2
h_2 : ¬j < f.natDegree - 1
h_3 : j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2
⊢ 2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1 = f.natDegree

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h : ¬j = f.natDegree - 2
h_1 : j = 2 * f.natDegree - 2
h_2 : ¬j < f.natDegree - 1
h_3 : j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2
⊢ 2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1 = f.natDegree

Tactic:
have : 2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1 = f.natDegree := by grind
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h : ¬j = f.natDegree - 2
h_1 : j = 2 * f.natDegree - 2
h_2 : ¬j < f.natDegree - 1
h_3 : j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2
this : 2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1 = f.natDegree
⊢ f.coeff f.natDegree * (↑f.natDegree : R) =
    f.coeff (2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) *
      (↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) : R)

Tactic:
simp [this]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h : ¬j = f.natDegree - 2
h_1 : j = 2 * f.natDegree - 2
h_2 : ¬j < f.natDegree - 1
h_3 : j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2
⊢ f.coeff f.natDegree * (↑f.natDegree : R) =
    f.coeff (2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) *
      HAdd.hAdd (α := R) (↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1))) : R) 1

Tactic:
on_goal 6 =>
      rw [← Nat.cast_one (R := R), ← Nat.cast_add]
      #adaptation_note
      /--
      Prior to nightly-2025-09-09,
      these two steps were not needed (i.e. `grind` just finished from here)
      -/
      have : 2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1 = f.natDegree := by grind
      simp [this]

Premises used: Nat.cast_add, Nat.cast_one
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h : j = f.natDegree - 2
h_1 : j < f.natDegree - 1
h_2 : j ≤ 2 * f.natDegree - 2 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2
⊢ f.coeff f.natDegree = f.coeff (2 * f.natDegree - 2 - j)

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h : j = f.natDegree - 2
h_1 : j < f.natDegree - 1
h_2 : ¬(j ≤ 2 * f.natDegree - 2 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2)
⊢ f.coeff 1 = 0

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h : j = f.natDegree - 2
h_1 : ¬j < f.natDegree - 1
h_2 : ¬(j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2)
⊢ f.coeff f.natDegree = 0

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h : ¬j = f.natDegree - 2
h_1 : j = 2 * f.natDegree - 2
h_2 : j < f.natDegree - 1
h_3 : j ≤ 2 * f.natDegree - 2 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2
⊢ f.coeff f.natDegree * (↑f.natDegree : R) = f.coeff (2 * f.natDegree - 2 - j)

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h : ¬j = f.natDegree - 2
h_1 : j = 2 * f.natDegree - 2
h_2 : j < f.natDegree - 1
h_3 : ¬(j ≤ 2 * f.natDegree - 2 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2)
⊢ f.coeff f.natDegree * (↑f.natDegree : R) = 0

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h : ¬j = f.natDegree - 2
h_1 : j = 2 * f.natDegree - 2
h_2 : ¬j < f.natDegree - 1
h_3 : ¬(j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2)
⊢ f.coeff f.natDegree * (↑f.natDegree : R) = 0

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h : ¬j = f.natDegree - 2
h_1 : ¬j = 2 * f.natDegree - 2
h_2 : j < f.natDegree - 1
h_3 : j ≤ 2 * f.natDegree - 2 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2
⊢ 0 = f.coeff (2 * f.natDegree - 2 - j)

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h : ¬j = f.natDegree - 2
h_1 : ¬j = 2 * f.natDegree - 2
h_2 : j < f.natDegree - 1
h_3 : ¬(j ≤ 2 * f.natDegree - 2 ∧ 2 * f.natDegree ≤ j + f.natDegree + 2)
⊢ Eq.{u_1 + 1} (α := R) 0 0

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h : ¬j = f.natDegree - 2
h_1 : ¬j = 2 * f.natDegree - 2
h_2 : ¬j < f.natDegree - 1
h_3 : j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2
⊢ 0 =
    f.coeff (2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) *
      HAdd.hAdd (α := R) (↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1))) : R) 1

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h : ¬j = f.natDegree - 2
h_1 : ¬j = 2 * f.natDegree - 2
h_2 : ¬j < f.natDegree - 1
h_3 : ¬(j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2)
⊢ Eq.{u_1 + 1} (α := R) 0 0

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f g : R[X]
m n : ℕ
φ : R →+* S
⊢ (map φ f).resultant (map φ g) m n = (φ : (a : R) → S) (f.resultant g m n)

Tactic:
simp [resultant, Polynomial.sylvester_map_map, RingHom.map_det]

Premises used: Polynomial.resultant, Polynomial.sylvester_map_map, RingHom.map_det, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m : ℕ
⊢ f.resultant g 0 m = f.coeff 0 ^ m

Tactic:
simp [resultant]

Premises used: Polynomial.resultant, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
r : R
m : ℕ
⊢ resultant ((C : (a : R) → R[X]) r) g 0 m = r ^ m

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n : ℕ
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 ⋯)) :
                              (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 ⋯)) :
                              (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
⊢ f.resultant g m n = HPow.hPow (α := R) (-1) (m * n) * g.resultant f n m

Tactic:
rw [resultant, resultant, sylvester_comm, Matrix.det_reindex, Equiv.Perm.sign_eq_prod_prod_Ioi]

Premises used: Polynomial.sylvester_comm, Polynomial.resultant, Equiv.Perm.sign_eq_prod_prod_Ioi, Matrix.det_reindex, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n : ℕ
e_a :
  (↑(↑(∏ 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 ⋯)) :
                            (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 ⋯)) :
                            (a : Fin (n + m)) → Fin (n + m))
                          j :
                        Fin (n + m)) then
                  1
                else -1) :
          ℤ) :
      R) =
    HPow.hPow (α := R) (-1) (m * n)
⊢ (↑(↑(∏ 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 ⋯)) :
                              (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 ⋯)) :
                              (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:
congr 1
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n : ℕ
e_a :
  (↑(↑(∏ 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)
⊢ (↑(↑(∏ 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 ⋯)) :
                            (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 ⋯)) :
                            (a : Fin (n + m)) → Fin (n + m))
                          j :
                        Fin (n + m)) then
                  1
                else -1) :
          ℤ) :
      R) =
    HPow.hPow (α := R) (-1) (m * n)

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n : ℕ
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)
⊢ (↑(↑(∏ 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)

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]

Premises used: Int.cast_neg, Int.reduceNeg, Units.coe_prod, apply_ite, Units.val_neg, Units.val_one, Fin.cast_lt_cast, Int.cast_prod, Int.cast_one
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n : ℕ
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)
⊢ (∏ 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_rw [← finSumFinEquiv.prod_comp, ← Finset.prod_map_equiv finSumFinEquiv.symm]

Premises used: Equiv.prod_comp, finSumFinEquiv, Equiv.symm, Finset.prod_map_equiv
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n : ℕ
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)
⊢ ∏ 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 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]

Premises used: Fin.val_fin_lt, finSumFinEquiv_apply_left, Sum.swap_inr, Equiv.symm_apply_apply, Finset.map, finSumFinEquiv_apply_right, Equiv.symm_symm, Finset.mem_Ioi, Finset.mem_map_equiv, Fin.val_castAdd, and_not_self, LT.lt, ite_not, Finset.prod_ite_mem_eq, Function.comp_apply, ite_and, OfNat.ofNat, Fintype.prod_sum_type, Fin.val_natAdd, add_lt_add_iff_left, Sum.swap_inl