awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.adjSylvester g ∘ₗ f.sylvesterMap g hf hg =
    HSMul.hSMul (β := ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_m × ↥R[X]_n) (f.resultant g m n) LinearMap.id
have this : Eq (α := ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_m × ↥R[X]_n)
  ((Matrix.toLin b₁ b₁ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_m × ↥R[X]_n)
      (HMul.hMul (α := Matrix (Fin (m + n)) (Fin (m + n)) R) (β := 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)))
        ((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)) :
    ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_m × ↥R[X]_n)
  ((Matrix.toLin b₁ b₁ : (a : Matrix (Fin (m + n)) (Fin (m + n)) R) → ↥R[X]_m × ↥R[X]_n →ₗ[R] ↥R[X]_m × ↥R[X]_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 × ↥R[X]_n →ₗ[R] ↥R[X]_m × ↥R[X]_n)
Tactic: have := congr(Matrix.toLin b₁ b₁ $(((sylvesterMap f g hf hg).toMatrix b₁ b₂).adjugate_mul))
-- 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
H : m ≠ 0 ∨ n ≠ 0
⊢ ∃ (p : R[X]) (q : R[X]),
    p.degree < (↑n : WithBot ℕ) ∧ q.degree < (↑m : WithBot ℕ) ∧ f * p + g * q = (C : (a : R) → R[X]) (f.resultant g m n)
have a : Nontrivial R
Tactic: nontriviality R
-- 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
H : m ≠ 0 ∨ n ≠ 0
h : Nontrivial R
X : ↥R[X]_m × ↥R[X]_n :=
  (f.adjSylvester g : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n)
    (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x) 1 ⋯)
⊢ ∃ (p : R[X]) (q : R[X]),
    p.degree < (↑n : WithBot ℕ) ∧ q.degree < (↑m : WithBot ℕ) ∧ f * p + g * q = (C : (a : R) → R[X]) (f.resultant g m n)
have this : Eq.{u_1 + 1} (α := R[X]) (↑((f.sylvesterMap g hf hg : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) X) : R[X])
  (↑((HSMul.hSMul (β := ↥R[X]_(m + n) →ₗ[R] ↥R[X]_(m + n)) (f.resultant g m n) LinearMap.id :
          (a : ↥R[X]_(m + n)) → ↥R[X]_(m + n))
        (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x) 1 sorry)) :
    R[X])
Tactic: have : ((sylvesterMap f g hf hg X)).1 = _ :=
    congr(($(sylveserMap_comp_adjSylvester f g hf hg) _).1)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
⊢ IsUnit (f.resultant g) ↔ IsCoprime f g
have pos : ∀ (hf0 : f.natDegree = 0), IsUnit (f.resultant g) ↔ IsCoprime f g
Tactic: by_cases hf0 : f.natDegree = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
pos : ∀ (hf0 : f.natDegree = 0), IsUnit (f.resultant g) ↔ IsCoprime f g
⊢ IsUnit (f.resultant g) ↔ IsCoprime f g
have neg : ∀ (hf0 : ¬f.natDegree = 0), IsUnit (f.resultant g) ↔ IsCoprime f g
Tactic: by_cases hf0 : f.natDegree = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : f.natDegree = 0
⊢ IsUnit (f.resultant g) ↔ IsCoprime f g
have pos : ∀ (hf : Monic.{u_1} (R := R) 1) (hf0 : natDegree.{u_1} (R := R) 1 = 0), IsUnit (resultant 1 g) ↔ IsCoprime 1 g
Tactic: obtain rfl := eq_one_of_monic_natDegree_zero hf hf0
Cleared hypotheses: f, hf, hf0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
⊢ IsUnit (f.resultant g) ↔ IsCoprime f g
have neg : ∀ (H : IsUnit (f.resultant g)), IsCoprime f g
Tactic: refine ⟨fun H ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
neg : ∀ (H : IsUnit (f.resultant g)), IsCoprime f g
⊢ IsUnit (f.resultant g) ↔ IsCoprime f g
have neg₁ : IsCoprime f g → IsUnit (f.resultant g)
Tactic: refine ⟨fun H ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
H : IsUnit (f.resultant g)
⊢ IsCoprime f g
have neg : ∀ (p q : R[X]) (hp : p.degree < (↑g.natDegree : WithBot ℕ)) (hq : q.degree < (↑f.natDegree : WithBot ℕ))
  (e : f * p + g * q = (C : (a : R) → R[X]) (f.resultant g)), IsCoprime f g
Tactic: obtain ⟨p, q, hp, hq, e⟩ := exists_mul_add_mul_eq_C_resultant f g le_rfl le_rfl (by simp [hf0])
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
⊢ IsUnit (f.resultant g)
have neg : 1 = f.resultant b * f.resultant g
Tactic: suffices 1 = f.resultant b * f.resultant g from isUnit_iff_exists_inv'.mpr ⟨_, this.symm⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
⊢ 1 = f.resultant b * f.resultant g
have this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
Tactic: have := resultant_mul_right f b g _ 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]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
⊢ 1 = f.resultant b * f.resultant g
have neg : ∀ (e : 0 * f + b * g = 1), 1 = f.resultant b * f.resultant g
Tactic: obtain rfl | hb0 := eq_or_ne a 0
Cleared hypotheses: a, e
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
neg : ∀ (e : 0 * f + b * g = 1), 1 = f.resultant b * f.resultant g
⊢ 1 = f.resultant b * f.resultant g
have neg₁ : ∀ (hb0 : a ≠ 0), 1 = f.resultant b * f.resultant g
Tactic: obtain rfl | hb0 := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
b : R[X]
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
e : 0 * f + b * g = 1
⊢ 1 = f.resultant b * f.resultant g
have this₁ : f.coeff f.natDegree ^ (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
Tactic: rw [show b * g = 1 by simpa using e, resultant_one_right] at this
Cleared hypotheses: this, e
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
⊢ 1 = f.resultant b * f.resultant g
have neg : ∀ (this : f.resultant ((C : (a : R) → R[X]) 1) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g)
  (hb0 : a ≠ 0), 1 = f.resultant b * f.resultant g
Tactic: rw [← resultant_add_mul_right _ _ a _ _ _ le_rfl, add_comm, mul_comm, e, ← C.map_one] at this
Cleared hypotheses: this, hb0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
neg :
  ∀
    (this :
      f.resultant ((C : (a : R) → R[X]) 1) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g)
    (hb0 : a ≠ 0), 1 = f.resultant b * f.resultant g
⊢ 1 = f.resultant b * f.resultant g
have rw : a.natDegree + f.natDegree ≤ b.natDegree + g.natDegree
Tactic: rw [← resultant_add_mul_right _ _ a _ _ _ le_rfl, add_comm, mul_comm, e, ← C.map_one] at this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
⊢ a.natDegree + f.natDegree ≤ b.natDegree + g.natDegree
have by_contra! : ∀ (H : b.natDegree + g.natDegree < a.natDegree + f.natDegree), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
H : b.natDegree + g.natDegree < a.natDegree + f.natDegree
⊢ False
have H₁ : (b * g).natDegree < a.natDegree + f.natDegree
Tactic: replace H := natDegree_mul_le.trans_lt H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
H : (b * g).natDegree < a.natDegree + f.natDegree
⊢ False
have H₁ : (b * g).natDegree < (a * f).natDegree
Tactic: rw [add_comm, ← hf.natDegree_mul' hb0, mul_comm f] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
H : (b * g).natDegree < (a * f).natDegree
⊢ False
have this₁ : (a * f + b * g).natDegree = (a * f).natDegree
Tactic: have := natDegree_add_eq_left_of_natDegree_lt H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this_1 : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
H : (b * g).natDegree < (a * f).natDegree
this : (a * f + b * g).natDegree = (a * f).natDegree
⊢ False
have this₁ : 0 = (a * f).natDegree
Tactic: simp only [e, natDegree_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
K : Type u_2
inst : Field K
f g : K[X]
⊢ f.resultant g = 0 ↔ (f ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime f g
have inl : resultant 0 g = 0 ↔ (Ne.{u_2 + 1} (α := K[X]) 0 0 ∨ g ≠ 0) ∧ ¬IsCoprime 0 g
Tactic: obtain rfl | hf := eq_or_ne f 0
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
K : Type u_2
inst : Field K
f g : K[X]
inl : resultant 0 g = 0 ↔ (Ne.{u_2 + 1} (α := K[X]) 0 0 ∨ g ≠ 0) ∧ ¬IsCoprime 0 g
⊢ f.resultant g = 0 ↔ (f ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime f g
have inr : ∀ (hf : f ≠ 0), f.resultant g = 0 ↔ (f ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime f g
Tactic: obtain rfl | hf := eq_or_ne f 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
K : Type u_2
inst : Field K
g : K[X]
⊢ resultant 0 g = 0 ↔ (Ne.{u_2 + 1} (α := K[X]) 0 0 ∨ g ≠ 0) ∧ ¬IsCoprime 0 g
have inl : Eq.{u_2 + 1} (α := K) (resultant 0 0) 0 ↔
  (Ne.{u_2 + 1} (α := K[X]) 0 0 ∨ Ne.{u_2 + 1} (α := K[X]) 0 0) ∧ ¬IsCoprime.{u_2} (R := K[X]) 0 0
Tactic: obtain rfl | hg := eq_or_ne g 0
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
K : Type u_2
inst : Field K
g : K[X]
inl :
  Eq.{u_2 + 1} (α := K) (resultant 0 0) 0 ↔
    (Ne.{u_2 + 1} (α := K[X]) 0 0 ∨ Ne.{u_2 + 1} (α := K[X]) 0 0) ∧ ¬IsCoprime.{u_2} (R := K[X]) 0 0
⊢ resultant 0 g = 0 ↔ (Ne.{u_2 + 1} (α := K[X]) 0 0 ∨ g ≠ 0) ∧ ¬IsCoprime 0 g
have inl₁ : ∀ (hg : g ≠ 0), resultant 0 g = 0 ↔ (Ne.{u_2 + 1} (α := K[X]) 0 0 ∨ g ≠ 0) ∧ ¬IsCoprime 0 g
Tactic: obtain rfl | hg := eq_or_ne g 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
K : Type u_2
inst : Field K
f g : K[X]
hf : f ≠ 0
⊢ (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) f).Monic
have rw : f.leadingCoeff⁻¹ * f.coeff f.natDegree = 1
Tactic: rw [Monic, ← coeff_natDegree, natDegree_C_mul (by simpa), coeff_C_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
K : Type u_2
inst : Field K
f g : K[X]
hf : f ≠ 0
⊢ f.resultant g = 0 ↔ (f ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime f g
have H : (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) f).Monic
Tactic: have H : (C f.leadingCoeff⁻¹ * f).Monic := by
    rw [Monic, ← coeff_natDegree, natDegree_C_mul (by simpa), coeff_C_mul]; simp [hf]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
K : Type u_2
inst : Field K
f g : K[X]
hf : f ≠ 0
H : (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) f).Monic
⊢ f.resultant g = 0 ↔ (f ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime f g
have this : IsUnit ((HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) f).resultant g) ↔
  IsCoprime (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) f) g
Tactic: have := isUnit_resultant_iff_isCoprime (f := C f.leadingCoeff⁻¹ * f) (g := g) H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
K : Type u_2
inst : Field K
f g : K[X]
hf : f ≠ 0
H : (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) f).Monic
this :
  IsUnit ((HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) f).resultant g) ↔
    IsCoprime (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) f) g
⊢ f.resultant g = 0 ↔ (f ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime f g
have this₁ : IsUnit (f.leadingCoeff⁻¹ ^ g.natDegree) ∧ IsUnit (f.resultant g) ↔ IsCoprime f g
Tactic: rw [resultant_C_mul_left, IsUnit.mul_iff, natDegree_C_mul (by simp [hf]),
    isCoprime_mul_unit_left_left (isUnit_C.mpr (by simp [hf]))] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.degree = 1
⊢ f.discr = 1
have hf₁ : f.natDegree = 1
Tactic: rw [← Nat.cast_one, degree_eq_iff_natDegree_eq_of_pos one_pos] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 1
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr ⋯
⊢ Eq (α := Matrix (Fin 1) (Fin 1) R)
    ((Matrix.reindex e e :
          (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
            Matrix (Fin 1) (Fin 1) R)
        f.sylvesterDeriv :
      Matrix (Fin 1) (Fin 1) R)
    (!![1] : Matrix (Fin 1) (Fin 1) R)
have this : NeZero (f.natDegree - 1 + f.natDegree)
Tactic: have : NeZero (f.natDegree - 1 + f.natDegree) := ⟨by lia⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 1
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr ⋯
this : NeZero (f.natDegree - 1 + f.natDegree)
⊢ Eq (α := Matrix (Fin 1) (Fin 1) R)
    ((Matrix.reindex e e :
          (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
            Matrix (Fin 1) (Fin 1) R)
        f.sylvesterDeriv :
      Matrix (Fin 1) (Fin 1) R)
    (!![1] : Matrix (Fin 1) (Fin 1) R)
have a : ∀ (i : ℕ) (hi : i < 1) (j : ℕ) (hj : j < 1),
  Eq (α := R)
    ((Matrix.reindex e e :
          (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
            Matrix (Fin 1) (Fin 1) R)
        f.sylvesterDeriv ⟨i, hi⟩ ⟨j, hj⟩ :
      R)
    (!![1] ⟨i, hi⟩ ⟨j, hj⟩ : R)
Tactic: ext ⟨i, hi⟩ ⟨j, hj⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 1
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr ⋯
this : NeZero (f.natDegree - 1 + f.natDegree)
i : ℕ
hi : i < 1
j : ℕ
hj : j < 1
⊢ Eq (α := R)
    ((Matrix.reindex e e :
          (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
            Matrix (Fin 1) (Fin 1) R)
        f.sylvesterDeriv ⟨i, hi⟩ ⟨j, hj⟩ :
      R)
    (!![1] ⟨i, hi⟩ ⟨j, hj⟩ : R)
have a : ∀ (hi : LT.lt (α := ℕ) 0 1),
  Eq (α := R)
    ((Matrix.reindex e e :
          (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
            Matrix (Fin 1) (Fin 1) R)
        f.sylvesterDeriv ⟨0, hi⟩ ⟨j, hj⟩ :
      R)
    (!![1] ⟨0, hi⟩ ⟨j, hj⟩ : R)
Tactic: obtain ⟨rfl⟩ : i = 0 := by 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 : R[X]
hf : f.natDegree = 1
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr ⋯
this : NeZero (f.natDegree - 1 + f.natDegree)
j : ℕ
hj : j < 1
hi : LT.lt (α := ℕ) 0 1
⊢ Eq (α := R)
    ((Matrix.reindex e e :
          (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
            Matrix (Fin 1) (Fin 1) R)
        f.sylvesterDeriv ⟨0, hi⟩ ⟨j, hj⟩ :
      R)
    (!![1] ⟨0, hi⟩ ⟨j, hj⟩ : R)
have a : ∀ (hj : LT.lt (α := ℕ) 0 1),
  Eq (α := R)
    ((Matrix.reindex e e :
          (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
            Matrix (Fin 1) (Fin 1) R)
        f.sylvesterDeriv ⟨0, hi⟩ ⟨0, hj⟩ :
      R)
    (!![1] ⟨0, hi⟩ ⟨0, hj⟩ : R)
Tactic: obtain ⟨rfl⟩ : j = 0 := by lia
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 1
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr ⋯
⊢ f.discr = 1
have this : Eq (α := Matrix (Fin 1) (Fin 1) R)
  ((Matrix.reindex e e :
        (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
          Matrix (Fin 1) (Fin 1) R)
      f.sylvesterDeriv :
    Matrix (Fin 1) (Fin 1) R)
  (!![1] : Matrix (Fin 1) (Fin 1) R)
Tactic: have : f.sylvesterDeriv.reindex e e = !![1] := by
    have : NeZero (f.natDegree - 1 + f.natDegree) := ⟨by lia⟩
    ext ⟨i, hi⟩ ⟨j, hj⟩
    obtain ⟨rfl⟩ : i = 0 := by lia
    obtain ⟨rfl⟩ : j = 0 := by lia
    simp [e, sylvesterDeriv, mul_comm, hf]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.degree = 2
⊢ f.discr = HPow.hPow (β := ℕ) (f.coeff 1) 2 - 4 * f.coeff 0 * f.coeff 2
have hf₁ : f.natDegree = 2
Tactic: rw [← Nat.cast_two, degree_eq_iff_natDegree_eq_of_pos two_pos] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
⊢ f.discr = HPow.hPow (β := ℕ) (f.coeff 1) 2 - 4 * f.coeff 0 * f.coeff 2
have rw : Matrix.det (n := Fin 3)
      ((Matrix.reindex e e :
          (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
            Matrix (Fin 3) (Fin 3) R)
        f.sylvesterDeriv) *
    HPow.hPow (α := R) (-1) (f.natDegree * (f.natDegree - 1) / 2) =
  HPow.hPow (β := ℕ) (f.coeff 1) 2 - 4 * f.coeff 0 * f.coeff 2
Tactic: rw [discr, ← Matrix.det_reindex_self e]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
⊢ Eq (α := Matrix (Fin 3) (Fin 3) R)
    ((Matrix.reindex e e :
          (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
            Matrix (Fin 3) (Fin 3) R)
        f.sylvesterDeriv :
      Matrix (Fin 3) (Fin 3) R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] : Matrix (Fin 3) (Fin 3) R)
have a : ∀ (i j : Fin 3),
  Eq (α := R)
    ((Matrix.reindex e e :
          (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
            Matrix (Fin 3) (Fin 3) R)
        f.sylvesterDeriv i j :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] i j : R)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
i j : Fin 3
⊢ Eq (α := R)
    ((Matrix.reindex e e :
          (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
            Matrix (Fin 3) (Fin 3) R)
        f.sylvesterDeriv i j :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] i j : R)
have a : Eq (α := R)
  ((Matrix.reindex e e :
        (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
          Matrix (Fin 3) (Fin 3) R)
      f.sylvesterDeriv ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩) j :
    R)
  (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩) j : R)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
i j : Fin 3
a :
  Eq (α := R)
    ((Matrix.reindex e e :
          (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
            Matrix (Fin 3) (Fin 3) R)
        f.sylvesterDeriv ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j : R)
⊢ Eq (α := R)
    ((Matrix.reindex e e :
          (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
            Matrix (Fin 3) (Fin 3) R)
        f.sylvesterDeriv i j :
      R)
    (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] i j : R)
have a₁ : Eq (α := R)
  ((Matrix.reindex e e :
        (a : Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R) →
          Matrix (Fin 3) (Fin 3) R)
      f.sylvesterDeriv ((fun (i : Fin 3) ↦ i) ⟨1, sorry⟩) j :
    R)
  (!![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun (i : Fin 3) ↦ i) ⟨1, sorry⟩) j : R)
Tactic: fin_cases i
Cleared hypotheses: i