awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : g.natDegree = 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
have pos : ∀ (a : R) (hg : Ne (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (0 : R[X]))
  (hg0 : natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a) = 0),
  (f.scaleRoots r).resultant (scaleRoots ((C : (a : R) → R[X]) a) r) f.natDegree
      (natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a)) =
    r ^ (f.natDegree * natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a)) * f.resultant ((C : (a : R) → R[X]) a)
Tactic: obtain ⟨a, rfl⟩ := natDegree_eq_zero.mp hg0
Cleared hypotheses: g, hg, hg0
-- 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
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
have neg : (f.scaleRoots 0).resultant (g.scaleRoots 0) f.natDegree g.natDegree =
  HPow.hPow (α := R) 0 (f.natDegree * g.natDegree) * f.resultant g
Tactic: obtain rfl | hr := eq_or_ne r 0
Cleared hypotheses: 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]
hf' : f.Splits
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
neg :
  (f.scaleRoots 0).resultant (g.scaleRoots 0) f.natDegree g.natDegree =
    HPow.hPow (α := R) 0 (f.natDegree * g.natDegree) * f.resultant g
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
have neg₁ : ∀ (hr : r ≠ 0),
  (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
Tactic: obtain rfl | hr := eq_or_ne r 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]
hf' : f.Splits
g : R[X]
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
⊢ (f.scaleRoots 0).resultant (g.scaleRoots 0) f.natDegree g.natDegree =
    HPow.hPow (α := R) 0 (f.natDegree * g.natDegree) * f.resultant g
have neg : (HMul.hMul (α := R[X]) ((algebraMap R R[X] : (a : R) → R[X]) f.leadingCoeff : R[X])
        (HPow.hPow (α := R[X]) X f.natDegree)).resultant
    (HMul.hMul (α := R[X]) ((algebraMap R R[X] : (a : R) → R[X]) g.leadingCoeff : R[X])
      (HPow.hPow (α := R[X]) X g.natDegree))
    f.natDegree g.natDegree =
  HPow.hPow (α := R) 0 (f.natDegree * g.natDegree) * f.resultant g
Tactic: rw [scaleRoots_zero, scaleRoots_zero, Algebra.smul_def, Algebra.smul_def]
-- 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
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
hr : r ≠ 0
| (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree
have rw : (f.scaleRoots r).resultant (g.scaleRoots r) (f.scaleRoots r).natDegree
Tactic: rw [← natDegree_scaleRoots f r, ← natDegree_scaleRoots g 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]
hf' : f.Splits
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
hr : r ≠ 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
have neg : (f.scaleRoots r).resultant (g.scaleRoots r) (f.scaleRoots r).natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
Tactic: conv_lhs => rw [← natDegree_scaleRoots f r, ← natDegree_scaleRoots g 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]
hf' : f.Splits
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
hr : r ≠ 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) (f.scaleRoots r).natDegree =
    r ^ (f.natDegree * g.natDegree) * f.resultant g
have neg : (f.scaleRoots r).leadingCoeff ^ (g.scaleRoots r).natDegree *
    Multiset.prod (Multiset.map (fun (x : R) ↦ eval x (g.scaleRoots r)) (Multiset.map (fun (x : R) ↦ r * x) f.roots)) =
  r ^ (f.natDegree * g.natDegree) *
    (f.leadingCoeff ^ g.natDegree * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots))
Tactic: rw [resultant_eq_prod_eval _ _ _ le_rfl hf',
      resultant_eq_prod_eval _ _ _ le_rfl (hf'.scaleRoots _),
      roots_scaleRoots _ (isUnit_iff_ne_zero.mpr hr)]
-- 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
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
hr : r ≠ 0
⊢ (f.scaleRoots r).leadingCoeff ^ (g.scaleRoots r).natDegree *
      Multiset.prod
        (Multiset.map (fun (x : R) ↦ eval x (g.scaleRoots r)) (Multiset.map (fun (x : R) ↦ r * x) f.roots)) =
    r ^ (f.natDegree * g.natDegree) *
      (f.leadingCoeff ^ g.natDegree * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots))
have neg : (f.scaleRoots r).leadingCoeff ^ (g.scaleRoots r).natDegree *
    Multiset.prod (Multiset.map (fun (x : R) ↦ r ^ g.natDegree * eval x g) f.roots) =
  r ^ (f.natDegree * g.natDegree) *
    (f.leadingCoeff ^ g.natDegree * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots))
Tactic: simp only [Multiset.map_map, Function.comp_def, scaleRoots_eval_mul]
-- 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
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
hr : r ≠ 0
⊢ (f.scaleRoots r).leadingCoeff ^ (g.scaleRoots r).natDegree *
      Multiset.prod (Multiset.map (fun (x : R) ↦ r ^ g.natDegree * eval x g) f.roots) =
    r ^ (f.natDegree * g.natDegree) *
      (f.leadingCoeff ^ g.natDegree * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots))
have neg : f.leadingCoeff ^ g.natDegree *
    ((r ^ g.natDegree) ^ f.natDegree * Multiset.prod (Multiset.map (fun (i : R) ↦ eval i g) f.roots)) =
  r ^ (f.natDegree * g.natDegree) *
    (f.leadingCoeff ^ g.natDegree * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) f.roots))
Tactic: simp only [leadingCoeff_scaleRoots, natDegree_scaleRoots, Multiset.prod_map_mul,
      Multiset.map_const', Multiset.prod_replicate, ← hf'.natDegree_eq_card_roots]
-- 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.Injective (α := R) (β := S) (⇑φ : (a : R) → S)
f : R[X]
IH :
  ∀ (g : S[X]) (r : S) (hf : map φ f ≠ 0) (hg : g ≠ 0),
    ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
      r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g
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 this : ((map φ f).scaleRoots ((φ : (a : R) → S) r)).resultant ((map φ g).scaleRoots ((φ : (a : R) → S) r)) (map φ f).natDegree
    (map φ g).natDegree =
  HPow.hPow (α := S) ((φ : (a : R) → S) r : S) ((map φ f).natDegree * (map φ g).natDegree) *
    (map φ f).resultant (map φ g)
Tactic: have := IH (g.map φ) (φ r) (by simpa using (map_injective _ hφ).ne hf)
      (by simpa using (map_injective _ hφ).ne hg)
-- 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.Injective (α := R) (β := S) (⇑φ : (a : R) → S)
f : R[X]
IH :
  ∀ (g : S[X]) (r : S) (hf : map φ f ≠ 0) (hg : g ≠ 0),
    ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
      r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
this :
  ((map φ f).scaleRoots ((φ : (a : R) → S) r)).resultant ((map φ g).scaleRoots ((φ : (a : R) → S) r))
      (map φ f).natDegree (map φ g).natDegree =
    HPow.hPow (α := S) ((φ : (a : R) → S) r : S) ((map φ f).natDegree * (map φ g).natDegree) *
      (map φ f).resultant (map φ g)
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
have inr : Eq (α := S) ((φ : (a : R) → S) ((f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree) : S)
  ((φ : (a : R) → S) (r ^ (f.natDegree * g.natDegree) * f.resultant g) : S)
Tactic: apply hφ
-- 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.Injective (α := R) (β := S) (⇑φ : (a : R) → S)
f : R[X]
IH :
  ∀ (g : S[X]) (r : S) (hf : map φ f ≠ 0) (hg : g ≠ 0),
    ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
      r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
this :
  ((map φ f).scaleRoots ((φ : (a : R) → S) r)).resultant ((map φ g).scaleRoots ((φ : (a : R) → S) r))
      (map φ f).natDegree (map φ g).natDegree =
    HPow.hPow (α := S) ((φ : (a : R) → S) r : S) ((map φ f).natDegree * (map φ g).natDegree) *
      (map φ f).resultant (map φ g)
⊢ Eq (α := S) ((φ : (a : R) → S) ((f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree) : S)
    ((φ : (a : R) → S) (r ^ (f.natDegree * g.natDegree) * f.resultant g) : S)
have inr : ∀
  (this :
    (map φ (f.scaleRoots r)).resultant (map φ (g.scaleRoots r)) (map φ f).natDegree (map φ g).natDegree =
      HPow.hPow (α := S) ((φ : (a : R) → S) r : S) ((map φ f).natDegree * (map φ g).natDegree) *
        (map φ f).resultant (map φ g)),
  Eq (α := S) ((φ : (a : R) → S) ((f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree) : S)
    ((φ : (a : R) → S) (r ^ (f.natDegree * g.natDegree) * f.resultant g) : S)
Tactic: rw [← map_scaleRoots, ← map_scaleRoots] 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 S : Type u_1
inst_1 : CommRing R
inst_2 : CommRing S
φ : R →+* S
hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)
f : R[X]
IH :
  ∀ (g : S[X]) (r : S) (hf : map φ f ≠ 0) (hg : g ≠ 0),
    ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
      r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
this :
  ((map φ f).scaleRoots ((φ : (a : R) → S) r)).resultant ((map φ g).scaleRoots ((φ : (a : R) → S) r))
      (map φ f).natDegree (map φ g).natDegree =
    HPow.hPow (α := S) ((φ : (a : R) → S) r : S) ((map φ f).natDegree * (map φ g).natDegree) *
      (map φ f).resultant (map φ g)
inr :
  ∀
    (this :
      (map φ (f.scaleRoots r)).resultant (map φ (g.scaleRoots r)) (map φ f).natDegree (map φ g).natDegree =
        HPow.hPow (α := S) ((φ : (a : R) → S) r : S) ((map φ f).natDegree * (map φ g).natDegree) *
          (map φ f).resultant (map φ g)),
    Eq (α := S) ((φ : (a : R) → S) ((f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree) : S)
      ((φ : (a : R) → S) (r ^ (f.natDegree * g.natDegree) * f.resultant g) : S)
⊢ Eq (α := S) ((φ : (a : R) → S) ((f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree) : S)
    ((φ : (a : R) → S) (r ^ (f.natDegree * g.natDegree) * f.resultant g) : S)
have inr₁ : ∀
  (this :
    (map φ (f.scaleRoots r)).resultant ((map φ g).scaleRoots ((φ : (a : R) → S) r)) (map φ f).natDegree
        (map φ g).natDegree =
      HPow.hPow (α := S) ((φ : (a : R) → S) r : S) ((map φ f).natDegree * (map φ g).natDegree) *
        (map φ f).resultant (map φ g)),
  Ne (α := S) ((φ : (a : R) → S) g.leadingCoeff : S) (0 : S)
Tactic: rw [← map_scaleRoots, ← map_scaleRoots] 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 S : Type u_1
inst_1 : CommRing R
inst_2 : CommRing S
φ : R →+* S
hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)
f : R[X]
IH :
  ∀ (g : S[X]) (r : S) (hf : map φ f ≠ 0) (hg : g ≠ 0),
    ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
      r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
this :
  ((map φ f).scaleRoots ((φ : (a : R) → S) r)).resultant ((map φ g).scaleRoots ((φ : (a : R) → S) r))
      (map φ f).natDegree (map φ g).natDegree =
    HPow.hPow (α := S) ((φ : (a : R) → S) r : S) ((map φ f).natDegree * (map φ g).natDegree) *
      (map φ f).resultant (map φ g)
inr :
  ∀
    (this :
      (map φ (f.scaleRoots r)).resultant (map φ (g.scaleRoots r)) (map φ f).natDegree (map φ g).natDegree =
        HPow.hPow (α := S) ((φ : (a : R) → S) r : S) ((map φ f).natDegree * (map φ g).natDegree) *
          (map φ f).resultant (map φ g)),
    Eq (α := S) ((φ : (a : R) → S) ((f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree) : S)
      ((φ : (a : R) → S) (r ^ (f.natDegree * g.natDegree) * f.resultant g) : S)
inr₁ :
  ∀
    (this :
      (map φ (f.scaleRoots r)).resultant ((map φ g).scaleRoots ((φ : (a : R) → S) r)) (map φ f).natDegree
          (map φ g).natDegree =
        HPow.hPow (α := S) ((φ : (a : R) → S) r : S) ((map φ f).natDegree * (map φ g).natDegree) *
          (map φ f).resultant (map φ g)),
    Ne (α := S) ((φ : (a : R) → S) g.leadingCoeff : S) (0 : S)
⊢ Eq (α := S) ((φ : (a : R) → S) ((f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree) : S)
    ((φ : (a : R) → S) (r ^ (f.natDegree * g.natDegree) * f.resultant g) : S)
have inr₂ : Ne (α := S) ((φ : (a : R) → S) f.leadingCoeff : S) (0 : S)
Tactic: rw [← map_scaleRoots, ← map_scaleRoots] at this
-- 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]
r : S
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 : ∀ (f' : R[X]) (hf' : map φ f' = f) (ef : f'.degree = f.degree),
  (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * 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_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]
r : S
hf : f ≠ 0
hg : g ≠ 0
f' : R[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
have inr : ∀ (g' : R[X]) (hg' : map φ g' = g) (eg : g'.degree = g.degree),
  (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * 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_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]
r : S
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
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
have inr : ∀ (r : R),
  (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
Tactic: obtain ⟨r, rfl⟩ := hφ r
Cleared hypotheses: r
-- 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
⊢ f.leadingCoeff = (φ : (a : R) → S) f'.leadingCoeff
have simp_rw : f.coeff f.natDegree = (φ : (a : R) → S) (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_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
simp_rw : f.coeff f.natDegree = (φ : (a : R) → S) (f'.coeff f'.natDegree)
⊢ f.leadingCoeff = (φ : (a : R) → S) f'.leadingCoeff
have simp_rw₁ : f.coeff f'.natDegree = (φ : (a : R) → S) (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_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
simp_rw : f.coeff f.natDegree = (φ : (a : R) → S) (f'.coeff f'.natDegree)
simp_rw₁ : f.coeff f'.natDegree = (φ : (a : R) → S) (f'.coeff f'.natDegree)
⊢ f.leadingCoeff = (φ : (a : R) → S) f'.leadingCoeff
have simp_rw₂ : (map φ f').coeff f'.natDegree = (φ : (a : R) → S) (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_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
⊢ (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 hfl : f.leadingCoeff = (φ : (a : R) → S) 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_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
⊢ g.leadingCoeff = (φ : (a : R) → S) g'.leadingCoeff
have simp_rw : g.coeff g.natDegree = (φ : (a : R) → S) (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_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
simp_rw : g.coeff g.natDegree = (φ : (a : R) → S) (g'.coeff g'.natDegree)
⊢ g.leadingCoeff = (φ : (a : R) → S) g'.leadingCoeff
have simp_rw₁ : g.coeff g'.natDegree = (φ : (a : R) → S) (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_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
simp_rw : g.coeff g.natDegree = (φ : (a : R) → S) (g'.coeff g'.natDegree)
simp_rw₁ : g.coeff g'.natDegree = (φ : (a : R) → S) (g'.coeff g'.natDegree)
⊢ g.leadingCoeff = (φ : (a : R) → S) g'.leadingCoeff
have simp_rw₂ : (map φ g').coeff g'.natDegree = (φ : (a : R) → S) (g'.coeff g'.natDegree)
Tactic: simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree eg, ← hg', coeff_map]