awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (R[X]_m) p
q : R[X]
hq : Membership.mem (γ := Submodule R R[X]) (R[X]_n) q
⊢ (f *
        (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_m) x) p hp,
                Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x) q hq).2 :
          R[X])).degree <
    (↑(m + n) : WithBot ℕ)
have pos : ∀ (hf' : f = 0),
  (f *
        (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_m) x) p hp,
                Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x) q hq).2 :
          R[X])).degree <
    (↑(m + n) : WithBot ℕ)
Tactic: by_cases hf' : f = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (R[X]_m) p
q : R[X]
hq : Membership.mem (γ := Submodule R R[X]) (R[X]_n) q
pos :
  ∀ (hf' : f = 0),
    (f *
          (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_m) x) p hp,
                  Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x) q hq).2 :
            R[X])).degree <
      (↑(m + n) : WithBot ℕ)
⊢ (f *
        (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_m) x) p hp,
                Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x) q hq).2 :
          R[X])).degree <
    (↑(m + n) : WithBot ℕ)
have neg : ∀ (hf' : ¬f = 0),
  (f *
        (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_m) x) p hp,
                Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x) q hq).2 :
          R[X])).degree <
    (↑(m + n) : WithBot ℕ)
Tactic: by_cases hf' : f = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (R[X]_m) p
q : R[X]
hq : Membership.mem (γ := Submodule R R[X]) (R[X]_n) q
⊢ (g *
        (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_m) x) p hp,
                Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x) q hq).1 :
          R[X])).degree <
    (↑(m + n) : WithBot ℕ)
have pos : ∀ (hg' : g = 0),
  (g *
        (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_m) x) p hp,
                Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x) q hq).1 :
          R[X])).degree <
    (↑(m + n) : WithBot ℕ)
Tactic: by_cases hg' : g = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (R[X]_m) p
q : R[X]
hq : Membership.mem (γ := Submodule R R[X]) (R[X]_n) q
pos :
  ∀ (hg' : g = 0),
    (g *
          (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_m) x) p hp,
                  Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x) q hq).1 :
            R[X])).degree <
      (↑(m + n) : WithBot ℕ)
⊢ (g *
        (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_m) x) p hp,
                Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x) q hq).1 :
          R[X])).degree <
    (↑(m + n) : WithBot ℕ)
have neg : ∀ (hg' : ¬g = 0),
  (g *
        (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_m) x) p hp,
                Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x) q hq).1 :
          R[X])).degree <
    (↑(m + n) : WithBot ℕ)
Tactic: by_cases hg' : g = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
x x_1 : ↥R[X]_m × ↥R[X]_n
⊢ Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x)
      (f * (↑(x + x_1).2 : R[X]) + g * (↑(x + x_1).1 : R[X])) ⋯ =
    Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x)
        (f * (↑x.2 : R[X]) + g * (↑x.1 : R[X])) ⋯ +
      Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x)
        (f * (↑x_1.2 : R[X]) + g * (↑x_1.1 : R[X])) ⋯
have a : (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x)
        (f * (↑(x + x_1).2 : R[X]) + g * (↑(x + x_1).1 : R[X])) sorry) :
    R[X]) =
  (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x)
          (f * (↑x.2 : R[X]) + g * (↑x.1 : R[X])) sorry +
        Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x)
          (f * (↑x_1.2 : R[X]) + g * (↑x_1.1 : R[X])) sorry) :
    R[X])
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
x : R
x_1 : ↥R[X]_m × ↥R[X]_n
⊢ Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x)
      (f * (↑(x • x_1).2 : R[X]) + g * (↑(x • x_1).1 : R[X])) ⋯ =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R)
      (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x)
        (f * (↑x_1.2 : R[X]) + g * (↑x_1.1 : R[X])) ⋯)
have a : (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x)
        (f * (↑(x • x_1).2 : R[X]) + g * (↑(x • x_1).1 : R[X])) sorry) :
    R[X]) =
  (↑(HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R)
        (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x)
          (f * (↑x_1.2 : R[X]) + g * (↑x_1.1 : R[X])) sorry)) :
    R[X])
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
⊢ Eq (α := Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
    ((LinearMap.toMatrix (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) (degreeLT.basis R (m + n)) :
          (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
        (f.sylvesterMap g hf hg) :
      Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
    ((Matrix.reindex (Equiv.refl (Fin (m + n))) (Equiv.symm finSumFinEquiv) :
          (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
        (f.sylvester g m n) :
      Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
have a : ∀ (i : Fin (m + n)) (j : Fin m),
  Eq (α := R)
    ((LinearMap.toMatrix (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) (degreeLT.basis R (m + n)) :
          (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
        (f.sylvesterMap g hf hg) i (Sum.inl j) :
      R)
    ((Matrix.reindex (Equiv.refl (Fin (m + n))) (Equiv.symm finSumFinEquiv) :
          (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
        (f.sylvester g m n) i (Sum.inl j) :
      R)
Tactic: ext i (j | j)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
a :
  ∀ (i : Fin (m + n)) (j : Fin m),
    Eq (α := R)
      ((LinearMap.toMatrix (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) (degreeLT.basis R (m + n)) :
            (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
          (f.sylvesterMap g hf hg) i (Sum.inl j) :
        R)
      ((Matrix.reindex (Equiv.refl (Fin (m + n))) (Equiv.symm finSumFinEquiv) :
            (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
          (f.sylvester g m n) i (Sum.inl j) :
        R)
⊢ Eq (α := Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
    ((LinearMap.toMatrix (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) (degreeLT.basis R (m + n)) :
          (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
        (f.sylvesterMap g hf hg) :
      Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
    ((Matrix.reindex (Equiv.refl (Fin (m + n))) (Equiv.symm finSumFinEquiv) :
          (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
        (f.sylvester g m n) :
      Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
have a₁ : ∀ (i : Fin (m + n)) (j : Fin n),
  Eq (α := R)
    ((LinearMap.toMatrix (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) (degreeLT.basis R (m + n)) :
          (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
        (f.sylvesterMap g hf hg) i (Sum.inr j) :
      R)
    ((Matrix.reindex (Equiv.refl (Fin (m + n))) (Equiv.symm finSumFinEquiv) :
          (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
        (f.sylvester g m n) i (Sum.inr j) :
      R)
Tactic: ext i (j | j)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
⊢ Eq (α := R)
    ((LinearMap.toMatrix (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) (degreeLT.basis R (m + n)) :
          (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
        (f.sylvesterMap g hf hg) i (Sum.inl j) :
      R)
    ((Matrix.reindex (Equiv.refl (Fin (m + n))) (Equiv.symm finSumFinEquiv) :
          (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
        (f.sylvester g m n) i (Sum.inl j) :
      R)
have a : (if (↑j : ℕ) ≤ (↑i : ℕ) then g.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
  if (↑j : ℕ) ≤ (↑i : ℕ) ∧ (↑i : ℕ) ≤ (↑j : ℕ) + n then g.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0
Tactic: suffices (if j.1 ≤ i then g.coeff (i - j) else 0) =
      if j ≤ i.1 ∧ ↑i ≤ j + n then g.coeff (i - j) else 0 by
        simpa [LinearMap.toMatrix_apply, sylvester, coeff_mul_X_pow']
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
⊢ (if (↑j : ℕ) ≤ (↑i : ℕ) then g.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
    if (↑j : ℕ) ≤ (↑i : ℕ) ∧ (↑i : ℕ) ≤ (↑j : ℕ) + n then g.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0
have a : (if (↑j : ℕ) ≤ (↑i : ℕ) then g.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
  if (↑j : ℕ) ≤ (↑i : ℕ) then if (↑i : ℕ) ≤ (↑j : ℕ) + n then g.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0 else 0
Tactic: rw [ite_and]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
⊢ (if (↑j : ℕ) ≤ (↑i : ℕ) then g.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
    if (↑j : ℕ) ≤ (↑i : ℕ) then if (↑i : ℕ) ≤ (↑j : ℕ) + n then g.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0 else 0
have pos : ∀ (h₁ : (↑j : ℕ) ≤ (↑i : ℕ)) (h₂ : (↑i : ℕ) ≤ (↑j : ℕ) + n),
  g.coeff ((↑i : ℕ) - (↑j : ℕ)) = g.coeff ((↑i : ℕ) - (↑j : ℕ))
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
pos :
  ∀ (h₁ : (↑j : ℕ) ≤ (↑i : ℕ)) (h₂ : (↑i : ℕ) ≤ (↑j : ℕ) + n),
    g.coeff ((↑i : ℕ) - (↑j : ℕ)) = g.coeff ((↑i : ℕ) - (↑j : ℕ))
⊢ (if (↑j : ℕ) ≤ (↑i : ℕ) then g.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
    if (↑j : ℕ) ≤ (↑i : ℕ) then if (↑i : ℕ) ≤ (↑j : ℕ) + n then g.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0 else 0
have neg : ∀ (h₁ : (↑j : ℕ) ≤ (↑i : ℕ)) (h₂ : ¬(↑i : ℕ) ≤ (↑j : ℕ) + n), g.coeff ((↑i : ℕ) - (↑j : ℕ)) = 0
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
pos :
  ∀ (h₁ : (↑j : ℕ) ≤ (↑i : ℕ)) (h₂ : (↑i : ℕ) ≤ (↑j : ℕ) + n),
    g.coeff ((↑i : ℕ) - (↑j : ℕ)) = g.coeff ((↑i : ℕ) - (↑j : ℕ))
neg : ∀ (h₁ : (↑j : ℕ) ≤ (↑i : ℕ)) (h₂ : ¬(↑i : ℕ) ≤ (↑j : ℕ) + n), g.coeff ((↑i : ℕ) - (↑j : ℕ)) = 0
⊢ (if (↑j : ℕ) ≤ (↑i : ℕ) then g.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
    if (↑j : ℕ) ≤ (↑i : ℕ) then if (↑i : ℕ) ≤ (↑j : ℕ) + n then g.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0 else 0
have neg₁ : ∀ (h₁ : ¬(↑j : ℕ) ≤ (↑i : ℕ)), Eq.{u_1 + 1} (α := R) 0 0
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
⊢ Eq (α := R)
    ((LinearMap.toMatrix (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) (degreeLT.basis R (m + n)) :
          (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
        (f.sylvesterMap g hf hg) i (Sum.inr j) :
      R)
    ((Matrix.reindex (Equiv.refl (Fin (m + n))) (Equiv.symm finSumFinEquiv) :
          (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R)
        (f.sylvester g m n) i (Sum.inr j) :
      R)
have a : (if (↑j : ℕ) ≤ (↑i : ℕ) then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
  if (↑j : ℕ) ≤ (↑i : ℕ) ∧ (↑i : ℕ) ≤ (↑j : ℕ) + m then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0
Tactic: suffices (if j.1 ≤ i then f.coeff (i - j) else 0) =
      if j ≤ i.1 ∧ ↑i ≤ j + m then f.coeff (i - j) else 0 by
        simpa [LinearMap.toMatrix_apply, sylvester, coeff_mul_X_pow']
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
⊢ (if (↑j : ℕ) ≤ (↑i : ℕ) then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
    if (↑j : ℕ) ≤ (↑i : ℕ) ∧ (↑i : ℕ) ≤ (↑j : ℕ) + m then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0
have a : (if (↑j : ℕ) ≤ (↑i : ℕ) then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
  if (↑j : ℕ) ≤ (↑i : ℕ) then if (↑i : ℕ) ≤ (↑j : ℕ) + m then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0 else 0
Tactic: rw [ite_and]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
⊢ (if (↑j : ℕ) ≤ (↑i : ℕ) then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
    if (↑j : ℕ) ≤ (↑i : ℕ) then if (↑i : ℕ) ≤ (↑j : ℕ) + m then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0 else 0
have pos : ∀ (h₁ : (↑j : ℕ) ≤ (↑i : ℕ)) (h₂ : (↑i : ℕ) ≤ (↑j : ℕ) + m),
  f.coeff ((↑i : ℕ) - (↑j : ℕ)) = f.coeff ((↑i : ℕ) - (↑j : ℕ))
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
pos :
  ∀ (h₁ : (↑j : ℕ) ≤ (↑i : ℕ)) (h₂ : (↑i : ℕ) ≤ (↑j : ℕ) + m),
    f.coeff ((↑i : ℕ) - (↑j : ℕ)) = f.coeff ((↑i : ℕ) - (↑j : ℕ))
⊢ (if (↑j : ℕ) ≤ (↑i : ℕ) then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
    if (↑j : ℕ) ≤ (↑i : ℕ) then if (↑i : ℕ) ≤ (↑j : ℕ) + m then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0 else 0
have neg : ∀ (h₁ : (↑j : ℕ) ≤ (↑i : ℕ)) (h₂ : ¬(↑i : ℕ) ≤ (↑j : ℕ) + m), f.coeff ((↑i : ℕ) - (↑j : ℕ)) = 0
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
pos :
  ∀ (h₁ : (↑j : ℕ) ≤ (↑i : ℕ)) (h₂ : (↑i : ℕ) ≤ (↑j : ℕ) + m),
    f.coeff ((↑i : ℕ) - (↑j : ℕ)) = f.coeff ((↑i : ℕ) - (↑j : ℕ))
neg : ∀ (h₁ : (↑j : ℕ) ≤ (↑i : ℕ)) (h₂ : ¬(↑i : ℕ) ≤ (↑j : ℕ) + m), f.coeff ((↑i : ℕ) - (↑j : ℕ)) = 0
⊢ (if (↑j : ℕ) ≤ (↑i : ℕ) then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
    if (↑j : ℕ) ≤ (↑i : ℕ) then if (↑i : ℕ) ≤ (↑j : ℕ) + m then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0 else 0
have neg₁ : ∀ (h₁ : ¬(↑j : ℕ) ≤ (↑i : ℕ)), Eq.{u_1 + 1} (α := R) 0 0
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
⊢ (LinearMap.toMatrix
          (Module.Basis.reindex (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) finSumFinEquiv)
          (degreeLT.basis R (m + n)) :
        (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
      (f.sylvesterMap g hf hg) =
    f.sylvester g m n
have a : ∀ (i j : Fin (m + n)),
  (LinearMap.toMatrix
          (Module.Basis.reindex (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) finSumFinEquiv)
          (degreeLT.basis R (m + n)) :
        (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
      (f.sylvesterMap g hf hg) i j =
    f.sylvester g m n i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i j : Fin (m + n)
⊢ (LinearMap.toMatrix
          (Module.Basis.reindex (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) finSumFinEquiv)
          (degreeLT.basis R (m + n)) :
        (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
      (f.sylvesterMap g hf hg) i j =
    f.sylvester g m n i j
have a : ∀ (j : Fin m ⊕ Fin n),
  (LinearMap.toMatrix
          (Module.Basis.reindex (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) finSumFinEquiv)
          (degreeLT.basis R (m + n)) :
        (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
      (f.sylvesterMap g hf hg) i ((finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n)) j) =
    f.sylvester g m n i ((finSumFinEquiv : (a : Fin m ⊕ Fin n) → Fin (m + n)) j)
Tactic: obtain ⟨j, rfl⟩ := finSumFinEquiv.surjective j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
b₁ : Module.Basis (Fin (m + n)) R (↥R[X]_m × ↥R[X]_n) :=
  Module.Basis.reindex (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) finSumFinEquiv
b₂ : Module.Basis (Fin (m + n)) R ↥R[X]_(m + n) := degreeLT.basis R (m + n)
⊢ f.sylvesterMap g hf hg ∘ₗ f.adjSylvester g =
    HSMul.hSMul (β := ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n)) (f.resultant g m n) LinearMap.id
have this : Eq (α := ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n))
  ((Matrix.toLin b₂ b₂ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n))
      (HMul.hMul (α := Matrix (Fin (m + n)) (Fin (m + n)) R) (β := Matrix (Fin (m + n)) (Fin (m + n)) R)
        ((LinearMap.toMatrix b₁ b₂ : (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
            (f.sylvesterMap g hf hg) :
          Matrix (Fin (m + n)) (Fin (m + n)) R)
        (Matrix.adjugate
          ((LinearMap.toMatrix b₁ b₂ :
              (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
            (f.sylvesterMap g hf hg)))) :
    ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n))
  ((Matrix.toLin b₂ b₂ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n))
      (HSMul.hSMul (α := R) (β := Matrix (Fin (m + n)) (Fin (m + n)) R)
        (Matrix.det (n := Fin (m + n))
          ((LinearMap.toMatrix b₁ b₂ :
              (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
            (f.sylvesterMap g hf hg)))
        1) :
    ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n))
Tactic: have := congr(Matrix.toLin b₂ b₂ $(((sylvesterMap f g hf hg).toMatrix b₁ b₂).mul_adjugate))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
b₁ : Module.Basis (Fin (m + n)) R (↥R[X]_m × ↥R[X]_n) :=
  Module.Basis.reindex (Module.Basis.prod (degreeLT.basis R m) (degreeLT.basis R n)) finSumFinEquiv
b₂ : Module.Basis (Fin (m + n)) R ↥R[X]_(m + n) := degreeLT.basis R (m + n)
this :
  Eq (α := ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n))
    ((Matrix.toLin b₂ b₂ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n))
        (HMul.hMul (α := Matrix (Fin (m + n)) (Fin (m + n)) R) (β := Matrix (Fin (m + n)) (Fin (m + n)) R)
          ((LinearMap.toMatrix b₁ b₂ :
                (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
              (f.sylvesterMap g hf hg) :
            Matrix (Fin (m + n)) (Fin (m + n)) R)
          (Matrix.adjugate
            ((LinearMap.toMatrix b₁ b₂ :
                (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
              (f.sylvesterMap g hf hg)))) :
      ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n))
    ((Matrix.toLin b₂ b₂ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n))
        (HSMul.hSMul (α := R) (β := Matrix (Fin (m + n)) (Fin (m + n)) R)
          (Matrix.det (n := Fin (m + n))
            ((LinearMap.toMatrix b₁ b₂ :
                (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
              (f.sylvesterMap g hf hg)))
          1) :
      ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n))
⊢ f.sylvesterMap g hf hg ∘ₗ f.adjSylvester g =
    HSMul.hSMul (β := ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n)) (f.resultant g m n) LinearMap.id
have rwa : ∀
  (this :
    Eq (α := ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n))
      ((Matrix.toLin b₁ b₂ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n))
          ((LinearMap.toMatrix b₁ b₂ :
              (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
            (f.sylvesterMap g hf hg)) ∘ₗ
        (Matrix.toLin b₂ b₁ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_(m + n) →ₗ[R] ↥R[X]_m × ↥R[X]_n)
          (Matrix.adjugate
            ((LinearMap.toMatrix b₁ b₂ :
                (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
              (f.sylvesterMap g hf hg))))
      ((Matrix.toLin b₂ b₂ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n))
        (HSMul.hSMul (α := R) (β := Matrix (Fin (m + n)) (Fin (m + n)) R)
          (Matrix.det (n := Fin (m + n))
            ((LinearMap.toMatrix b₁ b₂ :
                (a : ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_(m + n)) → Matrix (Fin (m + n)) (Fin (m + n)) R)
              (f.sylvesterMap g hf hg)))
          1))),
  f.sylvesterMap g hf hg ∘ₗ f.adjSylvester g =
    HSMul.hSMul (β := ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n)) (f.resultant g m n) LinearMap.id
Tactic: rwa [Matrix.toLin_mul b₂ b₁ b₂, Matrix.toLin_toMatrix, map_smul,
    toMatrix_sylvesterMap', Matrix.toLin_one, ← resultant] at this
Cleared hypotheses: this