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]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]) (hg : g.natDegree ≠ 0) (hR : IsDomain R),
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type u_1 := MvPolynomial R ℤ
φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap ℤ R) id
hφ : Function.Surjective (α := S) (β := R) (⇑φ : (a : S) → R)
f' : S[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : S[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
hfl : f.leadingCoeff = (φ : (a : S) → R) f'.leadingCoeff
hgl : g.leadingCoeff = (φ : (a : S) → R) g'.leadingCoeff
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
have neg : (φ : (a : S) → R) (g'.leadingCoeff ^ (f'.natDegree * (g'.natDegree - 1)) * f'.resultant g') =
  HPow.hPow (α := R) ((φ : (a : S) → R) g'.leadingCoeff : R) (f'.natDegree * (g'.natDegree - 1)) *
    (map φ f').resultant (map φ g') f'.natDegree g'.natDegree
Tactic: rw [← natDegree_eq_natDegree ef, ← natDegree_eq_natDegree eg,
      ← hf', hgl, ← map_scaleRoots _ _ _ (by simpa [← hfl]), ← hg', integralNormalization_map _ _
      (by simpa [← hgl]), resultant_map_map,
      this f' g' (by simpa [natDegree_eq_natDegree eg]) inferInstance]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
have pos : ∀ (hg0 : g = 0),
  (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
Tactic: by_cases hg0 : g = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
pos :
  ∀ (hg0 : g = 0),
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
have neg : ∀ (hg0 : ¬g = 0),
  (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
Tactic: by_cases hg0 : g = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
have neg : Eq.{u_1 + 1} (α := R)
  ((fun (x : R) ↦ g.leadingCoeff ^ f.natDegree * x)
    ((f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree))
  ((fun (x : R) ↦ g.leadingCoeff ^ f.natDegree * x)
    (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g))
Tactic: apply mul_right_injective₀ (a := g.leadingCoeff ^ f.natDegree) (by simp [hg0])
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
⊢ g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)
have this : (f.scaleRoots g.leadingCoeff).resultant (g.scaleRoots g.leadingCoeff) =
  g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
Tactic: have := resultant_scaleRoots f g g.leadingCoeff
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
this :
  (f.scaleRoots g.leadingCoeff).resultant (g.scaleRoots g.leadingCoeff) =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
⊢ g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)
have this₁ : g.leadingCoeff ^ f.natDegree * (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
  g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
Tactic: rw [natDegree_scaleRoots, natDegree_scaleRoots,
    ← integralNormalization_mul_C_leadingCoeff, mul_comm, resultant_C_mul_right] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
this :
  g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
⊢ g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)
have neg : g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
  g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)
Tactic: rw [this, ← mul_assoc, ← pow_add, add_comm, ← Nat.mul_add_one, Nat.sub_add_cancel (by lia)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
this :
  g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
neg :
  g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)
⊢ g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)
have neg₁ : g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
  g.leadingCoeff ^ f.natDegree * g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
Tactic: rw [this, ← mul_assoc, ← pow_add, add_comm, ← Nat.mul_add_one, Nat.sub_add_cancel (by lia)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
this :
  g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
neg :
  g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)
neg₁ :
  g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ f.natDegree * g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
⊢ g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)
have neg₂ : g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
  g.leadingCoeff ^ (f.natDegree + f.natDegree * (g.natDegree - 1)) * f.resultant g
Tactic: rw [this, ← mul_assoc, ← pow_add, add_comm, ← Nat.mul_add_one, Nat.sub_add_cancel (by lia)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
this :
  g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
neg :
  g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)
neg₁ :
  g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ f.natDegree * g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
neg₂ :
  g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ (f.natDegree + f.natDegree * (g.natDegree - 1)) * f.resultant g
⊢ g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)
have neg₃ : g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
  g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1) + f.natDegree) * f.resultant g
Tactic: rw [this, ← mul_assoc, ← pow_add, add_comm, ← Nat.mul_add_one, Nat.sub_add_cancel (by lia)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
this :
  g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
neg :
  g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)
neg₁ :
  g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ f.natDegree * g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
neg₂ :
  g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ (f.natDegree + f.natDegree * (g.natDegree - 1)) * f.resultant g
neg₃ :
  g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1) + f.natDegree) * f.resultant g
⊢ g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)
have neg₄ : g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
  g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1 + 1)) * f.resultant g
Tactic: rw [this, ← mul_assoc, ← pow_add, add_comm, ← Nat.mul_add_one, Nat.sub_add_cancel (by lia)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
this :
  g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
neg :
  g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)
neg₁ :
  g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ f.natDegree * g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
neg₂ :
  g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ (f.natDegree + f.natDegree * (g.natDegree - 1)) * f.resultant g
neg₃ :
  g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1) + f.natDegree) * f.resultant g
neg₄ :
  g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1 + 1)) * f.resultant g
⊢ g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)
have neg₅ : g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
  g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
Tactic: rw [this, ← mul_assoc, ← pow_add, add_comm, ← Nat.mul_add_one, Nat.sub_add_cancel (by lia)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : Field R
f : R[X]
g : R[X]
r : R
x : R[X]
h :
  Membership.mem (γ := Set R[X])
    ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
      {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
    x
⊢ resultant ((taylor r : (a : R[X]) → R[X]) x) ((taylor r : (a : R[X]) → R[X]) g) = x.resultant g
have Splits : ∀ (s : R),
  resultant ((taylor r : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) s)) ((taylor r : (a : R[X]) → R[X]) g) =
    resultant ((C : (a : R) → R[X]) s) g
Tactic: obtain (⟨s, rfl⟩ | ⟨s, rfl⟩) := h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : Field R
f : R[X]
g : R[X]
r : R
x : R[X]
h :
  Membership.mem (γ := Set R[X])
    ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
      {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
    x
Splits :
  ∀ (s : R),
    resultant ((taylor r : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) s)) ((taylor r : (a : R[X]) → R[X]) g) =
      resultant ((C : (a : R) → R[X]) s) g
⊢ resultant ((taylor r : (a : R[X]) → R[X]) x) ((taylor r : (a : R[X]) → R[X]) g) = x.resultant g
have Splits₁ : ∀ (s : R),
  resultant ((taylor r : (a : R[X]) → R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) s : R[X])))
      ((taylor r : (a : R[X]) → R[X]) g) =
    (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) s : R[X])).resultant g
Tactic: obtain (⟨s, rfl⟩ | ⟨s, rfl⟩) := h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : Field R
f : R[X]
g : R[X]
r s : R
⊢ resultant ((taylor r : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) s)) ((taylor r : (a : R[X]) → R[X]) g) =
    resultant ((C : (a : R) → R[X]) s) g
have Splits : resultant ((C : (a : R) → R[X]) s) ((taylor r : (a : R[X]) → R[X]) g) = resultant ((C : (a : R) → R[X]) s) g
Tactic: rw [taylor_C]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : Field R
f : R[X]
g : R[X]
r s : R
⊢ resultant ((taylor r : (a : R[X]) → R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) s : R[X])))
      ((taylor r : (a : R[X]) → R[X]) g) =
    (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) s : R[X])).resultant g
have inst : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : Field R
f : R[X]
g : R[X]
r s : R
inst_2 : Nontrivial R
⊢ resultant ((taylor r : (a : R[X]) → R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) s : R[X])))
      ((taylor r : (a : R[X]) → R[X]) g) =
    (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) s : R[X])).resultant g
have Splits : (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r + s) : R[X])).resultant
    ((taylor r : (a : R[X]) → R[X]) g) =
  (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) s : R[X])).resultant g
Tactic: rw [map_add, taylor_X, taylor_C, add_assoc, ← map_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : Field R
f : R[X]
g : R[X]
r : R
x y : R[X]
hx :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    x
hy :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    y
hx' : resultant ((taylor r : (a : R[X]) → R[X]) x) ((taylor r : (a : R[X]) → R[X]) g) = x.resultant g
hy' : resultant ((taylor r : (a : R[X]) → R[X]) y) ((taylor r : (a : R[X]) → R[X]) g) = y.resultant g
⊢ resultant ((taylor r : (a : R[X]) → R[X]) (x * y)) ((taylor r : (a : R[X]) → R[X]) g) = (x * y).resultant g
have pos : ∀ (hx0 : x = 0),
  resultant ((taylor r : (a : R[X]) → R[X]) (x * y)) ((taylor r : (a : R[X]) → R[X]) g) = (x * y).resultant g
Tactic: by_cases hx0 : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : Field R
f : R[X]
g : R[X]
r : R
x y : R[X]
hx :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    x
hy :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    y
hx' : resultant ((taylor r : (a : R[X]) → R[X]) x) ((taylor r : (a : R[X]) → R[X]) g) = x.resultant g
hy' : resultant ((taylor r : (a : R[X]) → R[X]) y) ((taylor r : (a : R[X]) → R[X]) g) = y.resultant g
pos :
  ∀ (hx0 : x = 0),
    resultant ((taylor r : (a : R[X]) → R[X]) (x * y)) ((taylor r : (a : R[X]) → R[X]) g) = (x * y).resultant g
⊢ resultant ((taylor r : (a : R[X]) → R[X]) (x * y)) ((taylor r : (a : R[X]) → R[X]) g) = (x * y).resultant g
have neg : ∀ (hx0 : ¬x = 0),
  resultant ((taylor r : (a : R[X]) → R[X]) (x * y)) ((taylor r : (a : R[X]) → R[X]) g) = (x * y).resultant g
Tactic: by_cases hx0 : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : Field R
f : R[X]
g : R[X]
r : R
x y : R[X]
hx :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    x
hy :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    y
hx' : resultant ((taylor r : (a : R[X]) → R[X]) x) ((taylor r : (a : R[X]) → R[X]) g) = x.resultant g
hy' : resultant ((taylor r : (a : R[X]) → R[X]) y) ((taylor r : (a : R[X]) → R[X]) g) = y.resultant g
hx0 : ¬x = 0
⊢ resultant ((taylor r : (a : R[X]) → R[X]) (x * y)) ((taylor r : (a : R[X]) → R[X]) g) = (x * y).resultant g
have pos : ∀ (hy0 : y = 0),
  resultant ((taylor r : (a : R[X]) → R[X]) (x * y)) ((taylor r : (a : R[X]) → R[X]) g) = (x * y).resultant g
Tactic: by_cases hy0 : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : Field R
f : R[X]
g : R[X]
r : R
x y : R[X]
hx :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    x
hy :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    y
hx' : resultant ((taylor r : (a : R[X]) → R[X]) x) ((taylor r : (a : R[X]) → R[X]) g) = x.resultant g
hy' : resultant ((taylor r : (a : R[X]) → R[X]) y) ((taylor r : (a : R[X]) → R[X]) g) = y.resultant g
hx0 : ¬x = 0
pos :
  ∀ (hy0 : y = 0),
    resultant ((taylor r : (a : R[X]) → R[X]) (x * y)) ((taylor r : (a : R[X]) → R[X]) g) = (x * y).resultant g
⊢ resultant ((taylor r : (a : R[X]) → R[X]) (x * y)) ((taylor r : (a : R[X]) → R[X]) g) = (x * y).resultant g
have neg : ∀ (hy0 : ¬y = 0),
  resultant ((taylor r : (a : R[X]) → R[X]) (x * y)) ((taylor r : (a : R[X]) → R[X]) g) = (x * y).resultant g
Tactic: by_cases hy0 : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : Field R
f : R[X]
g : R[X]
r : R
x y : R[X]
hx :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    x
hy :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
    y
hx' : resultant ((taylor r : (a : R[X]) → R[X]) x) ((taylor r : (a : R[X]) → R[X]) g) = x.resultant g
hy' : resultant ((taylor r : (a : R[X]) → R[X]) y) ((taylor r : (a : R[X]) → R[X]) g) = y.resultant g
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ resultant ((taylor r : (a : R[X]) → R[X]) (x * y)) ((taylor r : (a : R[X]) → R[X]) g) = (x * y).resultant g
have neg : HMul.hMul (α := R) (resultant ((taylor r : (a : R[X]) → R[X]) x) ((taylor r : (a : R[X]) → R[X]) g))
    (resultant ((taylor r : (a : R[X]) → R[X]) y) ((taylor r : (a : R[X]) → R[X]) g)) =
  (x * y).resultant g
Tactic: rw [taylor_mul, natDegree_mul' (by simp [*]), resultant_mul_left _ _ _ _ le_rfl]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : Field R
f : R[X]
hf' : f.Splits
g : R[X]
r : R
⊢ resultant ((taylor r : (a : R[X]) → R[X]) f) ((taylor r : (a : R[X]) → R[X]) g) = f.resultant g
have Splits : ∀ (x : R[X])
  (h :
    Membership.mem (γ := Set R[X])
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
      x),
  resultant ((taylor r : (a : R[X]) → R[X]) x) ((taylor r : (a : R[X]) → R[X]) g) = x.resultant g
Tactic: induction hf' using Submonoid.closure_induction with
    | mem x h =>
      obtain (⟨s, rfl⟩ | ⟨s, rfl⟩) := h
      · rw [taylor_C]; simp
      · nontriviality R
        rw [map_add, taylor_X, taylor_C, add_assoc, ← map_add]
        simp [-map_add, taylor_eval]
    | one => simp
    | mul x y hx hy hx' hy' =>
      by_cases hx0 : x = 0; · simp [hx0]
      by_cases hy0 : y = 0; · simp [hy0]
      rw [taylor_mul, natDegree_mul' (by simp [*]), resultant_mul_left _ _ _ _ le_rfl]
      simp [natDegree_mul', hx0, hy0, resultant_mul_left, ← hx', ← hy']
Cleared hypotheses: hf'