awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R S : Type u_1
inst_1 : CommRing R
inst_2 : CommRing S
φ : R →+* S
hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)
f : S[X]
IH :
  ∀ (q g : R[X]) (r : R) (hf : q ≠ 0) (hg : g ≠ 0),
    (q.scaleRoots r).resultant (g.scaleRoots r) q.natDegree g.natDegree =
      r ^ (q.natDegree * g.natDegree) * q.resultant g
g : S[X]
hf : f ≠ 0
hg : g ≠ 0
f' : R[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : R[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
r : R
hfl : f.leadingCoeff = (φ : (a : R) → S) f'.leadingCoeff
⊢ (f.scaleRoots ((φ : (a : R) → S) r)).resultant (g.scaleRoots ((φ : (a : R) → S) r)) f.natDegree g.natDegree =
    HPow.hPow (α := S) ((φ : (a : R) → S) r : S) (f.natDegree * g.natDegree) * f.resultant g
have hgl : g.leadingCoeff = (φ : (a : R) → S) g'.leadingCoeff
Tactic: have hgl : g.leadingCoeff = φ g'.leadingCoeff := by
      simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree eg, ← hg', coeff_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R S : Type u_1
inst_1 : CommRing R
inst_2 : CommRing S
φ : R →+* S
hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)
f : S[X]
IH :
  ∀ (q g : R[X]) (r : R) (hf : q ≠ 0) (hg : g ≠ 0),
    (q.scaleRoots r).resultant (g.scaleRoots r) q.natDegree g.natDegree =
      r ^ (q.natDegree * g.natDegree) * q.resultant g
g : S[X]
hf : f ≠ 0
hg : g ≠ 0
f' : R[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : R[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
r : R
hfl : f.leadingCoeff = (φ : (a : R) → S) f'.leadingCoeff
hgl : g.leadingCoeff = (φ : (a : R) → S) g'.leadingCoeff
⊢ (f.scaleRoots ((φ : (a : R) → S) r)).resultant (g.scaleRoots ((φ : (a : R) → S) r)) f.natDegree g.natDegree =
    HPow.hPow (α := S) ((φ : (a : R) → S) r : S) (f.natDegree * g.natDegree) * f.resultant g
have inr : (φ : (a : R) → S) (r ^ (f'.natDegree * g'.natDegree) * f'.resultant g') =
  HPow.hPow (α := S) ((φ : (a : R) → S) r : S) (f'.natDegree * g'.natDegree) * f.resultant g f'.natDegree g'.natDegree
Tactic: rw [← hf', ← map_scaleRoots _ _ _ (by simpa [← hfl]), ← hg',
      ← map_scaleRoots _ _ _ (by simpa [← hgl]), hf', hg',
      ← natDegree_eq_natDegree ef, ← natDegree_eq_natDegree eg,
      resultant_map_map, IH f' g' r (by aesop) (by aesop)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
R S : Type u_1
inst_1 : CommRing R
inst_2 : CommRing S
φ : R →+* S
hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)
f : S[X]
IH :
  ∀ (q g : R[X]) (r : R) (hf : q ≠ 0) (hg : g ≠ 0),
    (q.scaleRoots r).resultant (g.scaleRoots r) q.natDegree g.natDegree =
      r ^ (q.natDegree * g.natDegree) * q.resultant g
g : S[X]
hf : f ≠ 0
hg : g ≠ 0
f' : R[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : R[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
r : R
hfl : f.leadingCoeff = (φ : (a : R) → S) f'.leadingCoeff
hgl : g.leadingCoeff = (φ : (a : R) → S) g'.leadingCoeff
⊢ (φ : (a : R) → S) (r ^ (f'.natDegree * g'.natDegree) * f'.resultant g') =
    HPow.hPow (α := S) ((φ : (a : R) → S) r : S) (f'.natDegree * g'.natDegree) * f.resultant g f'.natDegree g'.natDegree
have inr : (φ : (a : R) → S) (r ^ (f'.natDegree * g'.natDegree) * f'.resultant g') =
  HMul.hMul (β := S) (HPow.hPow (α := S) ((φ : (a : R) → S) r : S) (f'.natDegree * g'.natDegree))
    ((φ : (a : R) → S) (f'.resultant g') : S)
Tactic: rw [← hf', ← hg', resultant_map_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
have inr : ∀ (R : Type u_1) [inst : Field R] (f : R[X]) (hf' : f.Splits) (g : R[X]) (r : R) (hf : f ≠ 0) (hg : g ≠ 0),
  (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
Tactic: induction f using induction_of_Splits_of_injective_of_surjective with
  | Splits R f hf' =>
    by_cases hf0 : f.natDegree = 0
    · obtain ⟨a, rfl⟩ := natDegree_eq_zero.mp hf0; simp
    by_cases hg0 : g.natDegree = 0
    · obtain ⟨a, rfl⟩ := natDegree_eq_zero.mp hg0; simp
    obtain rfl | hr := eq_or_ne r 0
    · rw [scaleRoots_zero, scaleRoots_zero, Algebra.smul_def, Algebra.smul_def]
      simp [resultant_C_mul_right, resultant_X_pow_right, *, (Ne.symm hf0)]
    conv_lhs => rw [← natDegree_scaleRoots f r, ← natDegree_scaleRoots g r]
    rw [resultant_eq_prod_eval _ _ _ le_rfl hf',
      resultant_eq_prod_eval _ _ _ le_rfl (hf'.scaleRoots _),
      roots_scaleRoots _ (isUnit_iff_ne_zero.mpr hr)]
    simp only [Multiset.map_map, Function.comp_def, scaleRoots_eval_mul]
    simp only [leadingCoeff_scaleRoots, natDegree_scaleRoots, Multiset.prod_map_mul,
      Multiset.map_const', Multiset.prod_replicate, ← hf'.natDegree_eq_card_roots]
    ring
  | injective R S φ hφ f IH =>
    have := IH (g.map φ) (φ r) (by simpa using (map_injective _ hφ).ne hf)
      (by simpa using (map_injective _ hφ).ne hg)
    apply hφ
    rw [← map_scaleRoots, ← map_scaleRoots] at this
    · simpa [natDegree_map_eq_of_injective hφ] using this
    all_goals simpa [map_eq_zero_iff _ hφ]
  | surjective R S φ hφ f IH =>
    obtain ⟨f', hf', ef⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)
    obtain ⟨g', hg', eg⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ g)
    obtain ⟨r, rfl⟩ := hφ r
    have hfl : f.leadingCoeff = φ f'.leadingCoeff := by
      simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree ef, ← hf', coeff_map]
    have hgl : g.leadingCoeff = φ g'.leadingCoeff := by
      simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree eg, ← hg', coeff_map]
    rw [← hf', ← map_scaleRoots _ _ _ (by simpa [← hfl]), ← hg',
      ← map_scaleRoots _ _ _ (by simpa [← hgl]), hf', hg',
      ← natDegree_eq_natDegree ef, ← natDegree_eq_natDegree eg,
      resultant_map_map, IH f' g' r (by aesop) (by aesop)]
    rw [← hf', ← hg', resultant_map_map]
    simp
Cleared hypotheses: f, g, r, hf, hg
-- 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
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
have rw : (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
  g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
Tactic: rw [natDegree_scaleRoots, natDegree_integralNormalization]
-- 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
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
have inr : ∀
  (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),
  (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
Tactic: wlog hR : IsDomain R
-- 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
inr :
  ∀
    (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),
    (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 wlog : ∀ {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
Tactic: wlog hR : IsDomain R
Cleared hypotheses: f, g, hg
-- 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
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
have pos : ∀ (hf0 : f = 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 hf0 : f = 0
-- 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
pos :
  ∀ (hf0 : f = 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 : ∀ (hf0 : ¬f = 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 hf0 : f = 0
-- 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
⊢ (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 : 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
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 (hypothesis)
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
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
have hφ : Function.Surjective (α := S) (β := R) (⇑φ : (a : S) → R)
Tactic: have hφ : Function.Surjective φ := fun x ↦ ⟨.X x, by simp [φ, MvPolynomial.eval₂Hom]⟩
-- 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.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
have neg : ∀ (f' : S[X]) (hf' : map φ f' = f) (ef : f'.degree = f.degree),
  (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
Tactic: obtain ⟨f', hf', ef⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)
-- 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
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
have neg : ∀ (g' : S[X]) (hg' : map φ g' = g) (eg : g'.degree = g.degree),
  (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
Tactic: obtain ⟨g', hg', eg⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ g)
-- 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
⊢ f.leadingCoeff = (φ : (a : S) → R) f'.leadingCoeff
have simp_rw : f.coeff f.natDegree = (φ : (a : S) → R) (f'.coeff f'.natDegree)
Tactic: simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree ef, ← hf', coeff_map]
-- 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
simp_rw : f.coeff f.natDegree = (φ : (a : S) → R) (f'.coeff f'.natDegree)
⊢ f.leadingCoeff = (φ : (a : S) → R) f'.leadingCoeff
have simp_rw₁ : f.coeff f'.natDegree = (φ : (a : S) → R) (f'.coeff f'.natDegree)
Tactic: simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree ef, ← hf', coeff_map]
-- 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
simp_rw : f.coeff f.natDegree = (φ : (a : S) → R) (f'.coeff f'.natDegree)
simp_rw₁ : f.coeff f'.natDegree = (φ : (a : S) → R) (f'.coeff f'.natDegree)
⊢ f.leadingCoeff = (φ : (a : S) → R) f'.leadingCoeff
have simp_rw₂ : (map φ f').coeff f'.natDegree = (φ : (a : S) → R) (f'.coeff f'.natDegree)
Tactic: simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree ef, ← hf', coeff_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
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
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
have hfl : f.leadingCoeff = (φ : (a : S) → R) f'.leadingCoeff
Tactic: have hfl : f.leadingCoeff = φ f'.leadingCoeff := by
      simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree ef, ← hf', coeff_map]
-- 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
⊢ g.leadingCoeff = (φ : (a : S) → R) g'.leadingCoeff
have simp_rw : g.coeff g.natDegree = (φ : (a : S) → R) (g'.coeff g'.natDegree)
Tactic: simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree eg, ← hg', coeff_map]
-- 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
simp_rw : g.coeff g.natDegree = (φ : (a : S) → R) (g'.coeff g'.natDegree)
⊢ g.leadingCoeff = (φ : (a : S) → R) g'.leadingCoeff
have simp_rw₁ : g.coeff g'.natDegree = (φ : (a : S) → R) (g'.coeff g'.natDegree)
Tactic: simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree eg, ← hg', coeff_map]
-- 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
simp_rw : g.coeff g.natDegree = (φ : (a : S) → R) (g'.coeff g'.natDegree)
simp_rw₁ : g.coeff g'.natDegree = (φ : (a : S) → R) (g'.coeff g'.natDegree)
⊢ g.leadingCoeff = (φ : (a : S) → R) g'.leadingCoeff
have simp_rw₂ : (map φ g').coeff g'.natDegree = (φ : (a : S) → R) (g'.coeff g'.natDegree)
Tactic: simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree eg, ← hg', coeff_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (hypothesis)
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
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
have hgl : g.leadingCoeff = (φ : (a : S) → R) g'.leadingCoeff
Tactic: have hgl : g.leadingCoeff = φ g'.leadingCoeff := by
      simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree eg, ← hg', coeff_map]