awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
hgm : g.Monic
inst : Field R := hR.toField
L : Type u_1 := g.SplittingField (K := R)
this :
  (map (algebraMap R L) f).resultant (map (algebraMap R L) g) f.natDegree g.natDegree =
    Multiset.prod
      (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots))
a :
  Eq (α := g.SplittingField (K := R))
    (Multiset.prod
      (Multiset.map
        (fun (x : R) ↦
          ((aeval ((algebraMap R (g.SplittingField (K := R)) : (a : R) → g.SplittingField) x) :
                R[X] →ₐ[R] g.SplittingField (K := R)) :
              (a : R[X]) → g.SplittingField)
            g)
        f.roots))
    (Multiset.prod
      (Multiset.map
        (fun (x : R) ↦
          ((algebraMap R (g.SplittingField (K := R)) : R →+* g.SplittingField (K := R)) : (a : R) → g.SplittingField)
            (eval x g))
        f.roots))
⊢ Eq (α := L)
    (Multiset.prod
      (Multiset.map
        ((fun (x : g.SplittingField (K := R)) ↦ eval x (map (algebraMap R (g.SplittingField (K := R))) g)) ∘
          (⇑(algebraMap R L) : (a : R) → L))
        f.roots))
    (Multiset.prod
      (Multiset.map (α := R) (⇑(algebraMap R L : R →+* L) : (a : R) → L)
        (Multiset.map (fun (x : R) ↦ eval x g) f.roots)))

Tactic:
simp only [eval_map_algebraMap, Function.comp_apply, Multiset.map_map, L]

Premises used: Multiset.map_map, Polynomial.eval_map_algebraMap, Function.comp_apply
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
hgm : g.Monic
inst : Field R := hR.toField
L : Type u_1 := g.SplittingField (K := R)
this :
  (map (algebraMap R L) f).resultant (map (algebraMap R L) g) f.natDegree g.natDegree =
    Multiset.prod
      (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots))
a :
  Eq.{u_1 + 1} (α := R → g.SplittingField (K := R))
    (fun (x : R) ↦
      ((aeval ((algebraMap R (g.SplittingField (K := R)) : (a : R) → g.SplittingField) x) :
            R[X] →ₐ[R] g.SplittingField (K := R)) :
          (a : R[X]) → g.SplittingField)
        g)
    fun (x : R) ↦
    ((algebraMap R (g.SplittingField (K := R)) : R →+* g.SplittingField (K := R)) : (a : R) → g.SplittingField)
      (eval x g)
⊢ Eq (α := g.SplittingField (K := R))
    (Multiset.prod
      (Multiset.map
        (fun (x : R) ↦
          ((aeval ((algebraMap R (g.SplittingField (K := R)) : (a : R) → g.SplittingField) x) :
                R[X] →ₐ[R] g.SplittingField (K := R)) :
              (a : R[X]) → g.SplittingField)
            g)
        f.roots))
    (Multiset.prod
      (Multiset.map
        (fun (x : R) ↦
          ((algebraMap R (g.SplittingField (K := R)) : R →+* g.SplittingField (K := R)) : (a : R) → g.SplittingField)
            (eval x g))
        f.roots))

Tactic:
congr
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
hgm : g.Monic
inst : Field R := hR.toField
L : Type u_1 := g.SplittingField (K := R)
this :
  (map (algebraMap R L) f).resultant (map (algebraMap R L) g) f.natDegree g.natDegree =
    Multiset.prod
      (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots))
a :
  ∀ (x : R),
    Eq (α := g.SplittingField (K := R))
      (((aeval ((algebraMap R (g.SplittingField (K := R)) : (a : R) → g.SplittingField) x) :
            R[X] →ₐ[R] g.SplittingField (K := R)) :
          (a : R[X]) → g.SplittingField)
        g)
      (((algebraMap R (g.SplittingField (K := R)) : R →+* g.SplittingField (K := R)) : (a : R) → g.SplittingField)
        (eval x g))
⊢ Eq.{u_1 + 1} (α := R → g.SplittingField (K := R))
    (fun (x : R) ↦
      ((aeval ((algebraMap R (g.SplittingField (K := R)) : (a : R) → g.SplittingField) x) :
            R[X] →ₐ[R] g.SplittingField (K := R)) :
          (a : R[X]) → g.SplittingField)
        g)
    fun (x : R) ↦
    ((algebraMap R (g.SplittingField (K := R)) : R →+* g.SplittingField (K := R)) : (a : R) → g.SplittingField)
      (eval x g)

Tactic:
ext
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst_1 : CommRing R
inst_2 : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
hgm : g.Monic
inst : Field R := hR.toField
L : Type u_1 := g.SplittingField (K := R)
this :
  (map (algebraMap R L) f).resultant (map (algebraMap R L) g) f.natDegree g.natDegree =
    Multiset.prod
      (Multiset.map (fun (ij : L × L) ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots))
x : R
⊢ Eq (α := g.SplittingField (K := R))
    (((aeval ((algebraMap R (g.SplittingField (K := R)) : (a : R) → g.SplittingField) x) :
          R[X] →ₐ[R] g.SplittingField (K := R)) :
        (a : R[X]) → g.SplittingField)
      g)
    (((algebraMap R (g.SplittingField (K := R)) : R →+* g.SplittingField (K := R)) : (a : R) → g.SplittingField)
      (eval x g))

Tactic:
simp [aeval_algebraMap_apply]

Premises used: Polynomial.aeval_algebraMap_apply
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u
inst : CommRing R
p : R[X]
P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]) (hp : p.Splits), P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : R[X]) (IH : P (map φ p)), P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : S[X]) (IH : ∀ (q : R[X]), P q), P p
inr : ∀ (this : ∀ {R : Type u} [inst : CommRing R] (p : R[X]) (hR : IsDomain R), P p) (hR : ¬IsDomain R), P p
wlog : ∀ {R : Type u} [inst : CommRing R] (p : R[X]) (hR : IsDomain R), P p
⊢ P p

Tactic:
wlog hR : IsDomain R generalizing R

Premises used: IsDomain
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u
inst : CommRing R
p : R[X]
P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]) (hp : p.Splits), P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : R[X]) (IH : P (map φ p)), P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : S[X]) (IH : ∀ (q : R[X]), P q), P p
this : ∀ {R : Type u} [inst : CommRing R] (p : R[X]) (hR : IsDomain R), P p
hR : ¬IsDomain R
x : R
⊢ (MvPolynomial.eval₂Hom (algebraMap ℤ R) id : (a : MvPolynomial R ℤ) → R) (MvPolynomial.X x) = x

Tactic:
simp [MvPolynomial.eval₂Hom]

Premises used: MvPolynomial.eval₂Hom
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u
inst : CommRing R
p : R[X]
P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]) (hp : p.Splits), P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : R[X]) (IH : P (map φ p)), P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : S[X]) (IH : ∀ (q : R[X]), P q), P p
this : ∀ {R : Type u} [inst : CommRing R] (p : R[X]) (hR : IsDomain R), P p
hR : ¬IsDomain R
⊢ P p

Tactic:
exact surjective _ _ (MvPolynomial.eval₂Hom (algebraMap ℤ R) id)
      (fun x ↦ ⟨.X x, by simp [MvPolynomial.eval₂Hom]⟩) p
      (fun _ ↦ this _ inferInstance)

Premises used: Algebra.algebraMap, MvPolynomial.X, inferInstance, id, MvPolynomial.eval₂Hom, Int, Exists.intro
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]) (hp : p.Splits), P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : R[X]) (IH : P (map φ p)), P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : S[X]) (IH : ∀ (q : R[X]), P q), P p
R : Type u
inst : CommRing R
p : R[X]
hR : IsDomain R
inr :
  ∀ (this : ∀ {R : Type u} [inst : CommRing R] (p : R[X]) (hR : IsDomain R) (hR : IsField R), P p) (hR : ¬IsField R),
    P p
wlog : ∀ {R : Type u} [inst : CommRing R] (p : R[X]) (hR : IsDomain R) (hR : IsField R), P p
⊢ P p

Tactic:
wlog hR : IsField R generalizing R

Premises used: IsField
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]) (hp : p.Splits), P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : R[X]) (IH : P (map φ p)), P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : S[X]) (IH : ∀ (q : R[X]), P q), P p
R : Type u
inst : CommRing R
p : R[X]
hR_1 : IsDomain R
this : ∀ {R : Type u} [inst : CommRing R] (p : R[X]) (hR : IsDomain R) (hR : IsField R), P p
hR : ¬IsField R
⊢ P p

Tactic:
injective _ _ _ (FaithfulSMul.algebraMap_injective R (FractionRing R)) _
      (this _ inferInstance (Field.toIsField _))

Premises used: FractionRing, Field.toIsField, inferInstance, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]) (hp : p.Splits), P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : R[X]) (IH : P (map φ p)), P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : S[X]) (IH : ∀ (q : R[X]), P q), P p
R : Type u
inst : CommRing R
p : R[X]
hR_1 : IsDomain R
this : ∀ {R : Type u} [inst : CommRing R] (p : R[X]) (hR : IsDomain R) (hR : IsField R), P p
hR : ¬IsField R
⊢ P p

Tactic:
exact injective _ _ _ (FaithfulSMul.algebraMap_injective R (FractionRing R)) _
      (this _ inferInstance (Field.toIsField _))

Premises used: FractionRing, Field.toIsField, inferInstance, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]) (hp : p.Splits), P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : R[X]) (IH : P (map φ p)), P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : S[X]) (IH : ∀ (q : R[X]), P q), P p
R : Type u
inst : CommRing R
p : R[X]
hR_1 : IsDomain R
hR : IsField R
inr :
  ∀ (this : ∀ {R : Type u} [inst : CommRing R] (p : R[X]) (hR : IsDomain R) (hR : IsField R) (hp : p.Splits), P p)
    (hp : ¬p.Splits), P p
wlog : ∀ {R : Type u} [inst : CommRing R] (p : R[X]) (hR : IsDomain R) (hR : IsField R) (hp : p.Splits), P p
⊢ P p

Tactic:
wlog hp : p.Splits generalizing R

Premises used: Polynomial.Splits
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]) (hp : p.Splits), P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : R[X]) (IH : P (map φ p)), P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : S[X]) (IH : ∀ (q : R[X]), P q), P p
R : Type u
inst : CommRing R
p : R[X]
hR_1 : IsDomain R
hR : IsField R
this : ∀ {R : Type u} [inst : CommRing R] (p : R[X]) (hR : IsDomain R) (hR : IsField R) (hp : p.Splits), P p
hp : ¬p.Splits
inr : P p
⊢ P p

Tactic:
letI inst := hR.toField
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]) (hp : p.Splits), P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_2 : CommRing S] (φ : R →+* S)
    (hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : R[X]) (IH : P (map φ p)), P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_2 : CommRing S] (φ : R →+* S)
    (hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : S[X]) (IH : ∀ (q : R[X]), P q), P p
R : Type u
inst_1 : CommRing R
p : R[X]
hR_1 : IsDomain R
hR : IsField R
this : ∀ {R : Type u} [inst : CommRing R] (p : R[X]) (hR : IsDomain R) (hR : IsField R) (hp : p.Splits), P p
hp : ¬p.Splits
inst : Field R := hR.toField
⊢ P p

Tactic:
injective _ _ _ (algebraMap R p.SplittingField).injective _
      (this _ inferInstance (Field.toIsField _) (SplittingField.splits _))

Premises used: Algebra.algebraMap, Polynomial.SplittingField, Field.toIsField, inferInstance, Polynomial.SplittingField.splits, RingHom.injective
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]) (hp : p.Splits), P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_2 : CommRing S] (φ : R →+* S)
    (hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : R[X]) (IH : P (map φ p)), P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_2 : CommRing S] (φ : R →+* S)
    (hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : S[X]) (IH : ∀ (q : R[X]), P q), P p
R : Type u
inst_1 : CommRing R
p : R[X]
hR_1 : IsDomain R
hR : IsField R
this : ∀ {R : Type u} [inst : CommRing R] (p : R[X]) (hR : IsDomain R) (hR : IsField R) (hp : p.Splits), P p
hp : ¬p.Splits
inst : Field R := hR.toField
⊢ P p

Tactic:
exact injective _ _ _ (algebraMap R p.SplittingField).injective _
      (this _ inferInstance (Field.toIsField _) (SplittingField.splits _))

Premises used: Algebra.algebraMap, Polynomial.SplittingField, Field.toIsField, inferInstance, Polynomial.SplittingField.splits, RingHom.injective
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]) (hp : p.Splits), P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : R[X]) (IH : P (map φ p)), P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : S[X]) (IH : ∀ (q : R[X]), P q), P p
R : Type u
inst : CommRing R
p : R[X]
hR_1 : IsDomain R
hR : IsField R
hp : p.Splits
letI : P p
⊢ P p

Tactic:
letI inst := hR.toField
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]) (hp : p.Splits), P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_2 : CommRing S] (φ : R →+* S)
    (hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : R[X]) (IH : P (map φ p)), P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_2 : CommRing S] (φ : R →+* S)
    (hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : S[X]) (IH : ∀ (q : R[X]), P q), P p
R : Type u
inst_1 : CommRing R
p : R[X]
hR_1 : IsDomain R
hR : IsField R
hp : p.Splits
inst : Field R := hR.toField
⊢ P p

Tactic:
Splits _ _ hp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
P : {R : Type u} → [inst : CommRing R] → R[X] → Prop
Splits : ∀ (R : Type u) [inst : Field R] (p : R[X]) (hp : p.Splits), P p
injective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_2 : CommRing S] (φ : R →+* S)
    (hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : R[X]) (IH : P (map φ p)), P p
surjective :
  ∀ (R S : Type u) [inst : CommRing R] [inst_2 : CommRing S] (φ : R →+* S)
    (hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)) (p : S[X]) (IH : ∀ (q : R[X]), P q), P p
R : Type u
inst_1 : CommRing R
p : R[X]
hR_1 : IsDomain R
hR : IsField R
hp : p.Splits
inst : Field R := hR.toField
⊢ P p

Tactic:
exact Splits _ _ hp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g₁ g₂ : R[X]
m : ℕ
hm : f.natDegree ≤ m
inr :
  ∀
    (this :
      ∀ {R : Type u_1} [inst : CommRing R] (f g₁ g₂ : R[X]) (m : ℕ) (hm : f.natDegree ≤ m) (hgn : m = f.natDegree),
        f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m)
    (hgn : ¬m = f.natDegree),
    f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m
wlog :
  ∀ {R : Type u_1} [inst : CommRing R] (f g₁ g₂ : R[X]) (m : ℕ) (hm : f.natDegree ≤ m) (hgn : m = f.natDegree),
    f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m
⊢ f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m

Tactic:
wlog hgn : m = f.natDegree

Premises used: Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g₁ g₂ : R[X]
m : ℕ
hm : f.natDegree ≤ m
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g₁ g₂ : R[X]) (m : ℕ) (hm : f.natDegree ≤ m) (hgn : m = f.natDegree),
    f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m
hgn : ¬m = f.natDegree
inr :
  ∀ (c : ℕ) (hm : f.natDegree ≤ f.natDegree + c) (hgn : ¬f.natDegree + c = f.natDegree),
    f.resultant (g₁ * g₂) (f.natDegree + c) (g₁.natDegree + g₂.natDegree) =
      f.resultant g₁ (f.natDegree + c) * f.resultant g₂ (f.natDegree + c)
⊢ f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m

Tactic:
obtain ⟨c, rfl⟩ := le_iff_exists_add.mp hm

Premises used: le_iff_exists_add, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g₁ g₂ : R[X]
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g₁ g₂ : R[X]) (m : ℕ) (hm : f.natDegree ≤ m) (hgn : m = f.natDegree),
    f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m
c : ℕ
hm : f.natDegree ≤ f.natDegree + c
hgn : ¬f.natDegree + c = f.natDegree
inr :
  HPow.hPow (α := R) (-1) ((g₁.natDegree + g₂.natDegree) * c) * (g₁.leadingCoeff * g₂.leadingCoeff) ^ c *
      (f.resultant g₁ * f.resultant g₂) =
    HPow.hPow (α := R) (-1) (g₁.natDegree * c) * g₁.leadingCoeff ^ c * f.resultant g₁ *
      (HPow.hPow (α := R) (-1) (g₂.natDegree * c) * g₂.leadingCoeff ^ c * f.resultant g₂)
⊢ f.resultant (g₁ * g₂) (f.natDegree + c) (g₁.natDegree + g₂.natDegree) =
    f.resultant g₁ (f.natDegree + c) * f.resultant g₂ (f.natDegree + c)

Tactic:
simp [resultant_add_left_deg, this f g₁ g₂, coeff_mul_degree_add_degree]

Premises used: Polynomial.resultant_add_left_deg, Polynomial.coeff_mul_degree_add_degree
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g₁ g₂ : R[X]
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g₁ g₂ : R[X]) (m : ℕ) (hm : f.natDegree ≤ m) (hgn : m = f.natDegree),
    f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m
c : ℕ
hm : f.natDegree ≤ f.natDegree + c
hgn : ¬f.natDegree + c = f.natDegree
⊢ HPow.hPow (α := R) (-1) ((g₁.natDegree + g₂.natDegree) * c) * (g₁.leadingCoeff * g₂.leadingCoeff) ^ c *
      (f.resultant g₁ * f.resultant g₂) =
    HPow.hPow (α := R) (-1) (g₁.natDegree * c) * g₁.leadingCoeff ^ c * f.resultant g₁ *
      (HPow.hPow (α := R) (-1) (g₂.natDegree * c) * g₂.leadingCoeff ^ c * f.resultant g₂)

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g₁ g₂ : R[X]
m : ℕ
hm : f.natDegree ≤ m
hgn : m = f.natDegree
subst :
  ∀ (hm : f.natDegree ≤ f.natDegree),
    f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
⊢ f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m

Tactic:
subst hgn
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : Field R
f : R[X]
hff : f.Splits
g₁ g₂ : R[X]
Splits :
  f.leadingCoeff ^ (g₁.natDegree + g₂.natDegree) *
      HMul.hMul (α := R) (Multiset.prod (Multiset.map (fun (i : R) ↦ eval i g₁) f.roots))
        (Multiset.prod (Multiset.map (fun (i : R) ↦ eval i g₂) f.roots)) =
    f.leadingCoeff ^ g₁.natDegree * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g₁) f.roots) *
      (f.leadingCoeff ^ g₂.natDegree * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g₂) f.roots))
⊢ f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂

Tactic:
simp [resultant_eq_prod_eval, natDegree_mul_le, hff]

Premises used: Polynomial.resultant_eq_prod_eval, Polynomial.natDegree_mul_le
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : Field R
f : R[X]
hff : f.Splits
g₁ g₂ : R[X]
⊢ f.leadingCoeff ^ (g₁.natDegree + g₂.natDegree) *
      HMul.hMul (α := R) (Multiset.prod (Multiset.map (fun (i : R) ↦ eval i g₁) f.roots))
        (Multiset.prod (Multiset.map (fun (i : R) ↦ eval i g₂) f.roots)) =
    f.leadingCoeff ^ g₁.natDegree * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g₁) f.roots) *
      (f.leadingCoeff ^ g₂.natDegree * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g₂) f.roots))

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R_1 : Type u_1
inst : CommRing R_1
R SatisfiesM : Type u_1
inst_1 : CommRing R
inst_2 : CommRing SatisfiesM
φ : R →+* SatisfiesM
hφ : Function.Injective (α := R) (β := SatisfiesM) (⇑φ : (a : R) → SatisfiesM)
f : R[X]
IH :
  ∀ (g₁ g₂ : SatisfiesM[X]),
    (map φ f).resultant (g₁ * g₂) (map φ f).natDegree (g₁.natDegree + g₂.natDegree) =
      (map φ f).resultant g₁ * (map φ f).resultant g₂
g₁ g₂ : R[X]
injective :
  Eq (α := SatisfiesM)
    ((φ : (a : R) → SatisfiesM) (f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree)) : SatisfiesM)
    ((φ : (a : R) → SatisfiesM) (f.resultant g₁ * f.resultant g₂) : SatisfiesM)
⊢ f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂

Tactic:
apply hφ
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R_1 : Type u_1
inst : CommRing R_1
R SatisfiesM : Type u_1
inst_1 : CommRing R
inst_2 : CommRing SatisfiesM
φ : R →+* SatisfiesM
hφ : Function.Injective (α := R) (β := SatisfiesM) (⇑φ : (a : R) → SatisfiesM)
f : R[X]
IH :
  ∀ (g₁ g₂ : SatisfiesM[X]),
    (map φ f).resultant (g₁ * g₂) (map φ f).natDegree (g₁.natDegree + g₂.natDegree) =
      (map φ f).resultant g₁ * (map φ f).resultant g₂
g₁ g₂ : R[X]
⊢ (map φ f).resultant (map φ g₁ * map φ g₂) (map φ f).natDegree ((map φ g₁).natDegree + (map φ g₂).natDegree) =
    (map φ f).resultant (map φ g₁) * (map φ f).resultant (map φ g₂)

Tactic:
have := IH (g₁.map φ) (g₂.map φ)