awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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]
this :
  (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₂)
⊢ (map φ f).resultant (map φ (g₁ * g₂)) (map φ f).natDegree ((map φ g₁).natDegree + (map φ g₂).natDegree) =
    (map φ f).resultant (map φ g₁) * (map φ f).resultant (map φ g₂)

Tactic:
rw [← Polynomial.map_mul] at this

Premises used: Polynomial.map_mul
-- 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]
this :
  (map φ f).resultant (map φ (g₁ * g₂)) (map φ f).natDegree ((map φ g₁).natDegree + (map φ g₂).natDegree) =
    (map φ f).resultant (map φ g₁) * (map φ f).resultant (map φ g₂)
⊢ 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)

Tactic:
simpa only [resultant_map_map, ← map_mul, natDegree_map_eq_of_injective hφ] using this

Premises used: map_mul, Polynomial.resultant_map_map, Polynomial.natDegree_map_eq_of_injective
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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₁ g₂ : R[X]), q.resultant (g₁ * g₂) q.natDegree (g₁.natDegree + g₂.natDegree) = q.resultant g₁ * q.resultant g₂
g₁ g₂ : S[X]
surjective :
  ∀ (f' : R[X]) (hf' : map φ f' = f) (e : f'.degree = f.degree),
    f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
⊢ f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂

Tactic:
obtain ⟨f', hf', e⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)

Premises used: Polynomial.map_surjective, Polynomial.exists_degree_eq_of_mem_lifts
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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₁ g₂ : R[X]), q.resultant (g₁ * g₂) q.natDegree (g₁.natDegree + g₂.natDegree) = q.resultant g₁ * q.resultant g₂
g₁ g₂ : S[X]
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
surjective :
  ∀ (g₁' : R[X]) (hg₁ : map φ g₁' = g₁) (e₁ : g₁'.degree = g₁.degree),
    f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
⊢ f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂

Tactic:
obtain ⟨g₁', hg₁, e₁⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ g₁)

Premises used: Polynomial.map_surjective, Polynomial.exists_degree_eq_of_mem_lifts
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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₁ g₂ : R[X]), q.resultant (g₁ * g₂) q.natDegree (g₁.natDegree + g₂.natDegree) = q.resultant g₁ * q.resultant g₂
g₁ g₂ : S[X]
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
g₁' : R[X]
hg₁ : map φ g₁' = g₁
e₁ : g₁'.degree = g₁.degree
surjective :
  ∀ (g₂' : R[X]) (hg₂ : map φ g₂' = g₂) (e₂ : g₂'.degree = g₂.degree),
    f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
⊢ f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂

Tactic:
obtain ⟨g₂', hg₂, e₂⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ g₂)

Premises used: Polynomial.map_surjective, Polynomial.exists_degree_eq_of_mem_lifts
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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₁ g₂ : R[X]), q.resultant (g₁ * g₂) q.natDegree (g₁.natDegree + g₂.natDegree) = q.resultant g₁ * q.resultant g₂
g₁ g₂ : S[X]
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
g₁' : R[X]
hg₁ : map φ g₁' = g₁
e₁ : g₁'.degree = g₁.degree
g₂' : R[X]
hg₂ : map φ g₂' = g₂
e₂ : g₂'.degree = g₂.degree
surjective :
  (map φ f').resultant (map φ (g₁' * g₂')) (map φ f').natDegree ((map φ g₁').natDegree + (map φ g₂').natDegree) =
    (map φ f').resultant (map φ g₁') * (map φ f').resultant (map φ g₂')
⊢ f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂

Tactic:
rw [← hg₁, ← hg₂, ← hf', ← Polynomial.map_mul]

Premises used: Polynomial.map_mul
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g₁ g₂ : R[X]
Splits :
  ∀ (R : Type u_1) [inst : Field R] (f : R[X]) (hff : f.Splits) (g₁ g₂ : R[X]),
    f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
injective :
  ∀ (R SatisfiesM : Type u_1) [inst : CommRing R] [inst_1 : 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]), f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
surjective :
  ∀ (R S : Type u_1) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)) (f : S[X])
    (IH :
      ∀ (q g₁ g₂ : R[X]),
        q.resultant (g₁ * g₂) q.natDegree (g₁.natDegree + g₂.natDegree) = q.resultant g₁ * q.resultant g₂)
    (g₁ g₂ : S[X]), f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
⊢ f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂

Tactic:
induction f using induction_of_Splits_of_injective_of_surjective with
  | Splits R f hff =>
    simp [resultant_eq_prod_eval, natDegree_mul_le, hff]
    ring_nf
  | injective R SatisfiesM φ hφ f IH =>
    apply hφ
    have := IH (g₁.map φ) (g₂.map φ)
    rw [← Polynomial.map_mul] at this
    simpa only [resultant_map_map, ← map_mul, natDegree_map_eq_of_injective hφ] using this
  | surjective R S φ hφ f IH =>
    obtain ⟨f', hf', e⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)
    obtain ⟨g₁', hg₁, e₁⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ g₁)
    obtain ⟨g₂', hg₂, e₂⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ g₂)
    rw [← hg₁, ← hg₂, ← hf', ← Polynomial.map_mul]
    simp_rw [resultant_map_map, hg₁, hg₂, hf', ← natDegree_eq_natDegree e₁,
      ← natDegree_eq_natDegree e₂, ← natDegree_eq_natDegree e, IH, map_mul]

Premises used: Polynomial.map_mul, Polynomial.resultant_eq_prod_eval, map_mul, Polynomial.resultant_map_map, Polynomial.natDegree_mul_le, Polynomial.induction_of_Splits_of_injective_of_surjective, Polynomial.Splits
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f₁ f₂ g : R[X]
n : ℕ
hn : g.natDegree ≤ n
rw :
  HPow.hPow (α := R) (-1) ((f₁.natDegree + f₂.natDegree) * n) *
      (HPow.hPow (α := R) (-1) (n * f₁.natDegree) * f₁.resultant g f₁.natDegree n * g.resultant f₂ n) =
    f₁.resultant g f₁.natDegree n * (HPow.hPow (α := R) (-1) (f₂.natDegree * n) * g.resultant f₂ n)
⊢ (f₁ * f₂).resultant g (f₁.natDegree + f₂.natDegree) n = f₁.resultant g f₁.natDegree n * f₂.resultant g f₂.natDegree n

Tactic:
rw [resultant_comm, resultant_mul_right _ _ _ n hn, resultant_comm, resultant_comm f₂]

Premises used: Polynomial.resultant_comm, Polynomial.resultant_mul_right
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f₁ f₂ g : R[X]
n : ℕ
hn : g.natDegree ≤ n
ring_nf :
  f₁.resultant g f₁.natDegree n * g.resultant f₂ n * HPow.hPow (α := R) (-1) (f₁.natDegree * n * 2) *
      HPow.hPow (α := R) (-1) (f₂.natDegree * n) =
    f₁.resultant g f₁.natDegree n * g.resultant f₂ n * HPow.hPow (α := R) (-1) (f₂.natDegree * n)
⊢ HPow.hPow (α := R) (-1) ((f₁.natDegree + f₂.natDegree) * n) *
      (HPow.hPow (α := R) (-1) (n * f₁.natDegree) * f₁.resultant g f₁.natDegree n * g.resultant f₂ n) =
    f₁.resultant g f₁.natDegree n * (HPow.hPow (α := R) (-1) (f₂.natDegree * n) * g.resultant f₂ n)

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f₁ f₂ g : R[X]
n : ℕ
hn : g.natDegree ≤ n
⊢ f₁.resultant g f₁.natDegree n * g.resultant f₂ n * HPow.hPow (α := R) (-1) (f₁.natDegree * n * 2) *
      HPow.hPow (α := R) (-1) (f₂.natDegree * n) =
    f₁.resultant g f₁.natDegree n * g.resultant f₂ n * HPow.hPow (α := R) (-1) (f₂.natDegree * n)

Tactic:
simp
-- 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]
hf : f.Splits
pos : ∀ (h : f.natDegree = 0), f.resultant f = HPow.hPow (α := R) 0 f.natDegree
neg : ∀ (h : ¬f.natDegree = 0), f.resultant f = HPow.hPow (α := R) 0 f.natDegree
⊢ f.resultant f = HPow.hPow (α := R) 0 f.natDegree

Tactic:
by_cases h : f.natDegree = 0

Premises used: Polynomial.natDegree
-- 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]
hf : f.Splits
h : f.natDegree = 0
pos :
  ∀ (r : R) (hf : Splits.{u_1} (R := R) ((C : (a : R) → R[X]) r))
    (h : natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) r) = 0),
    resultant ((C : (a : R) → R[X]) r) ((C : (a : R) → R[X]) r) =
      HPow.hPow (α := R) 0 (natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) r))
⊢ f.resultant f = HPow.hPow (α := R) 0 f.natDegree

Tactic:
obtain ⟨r, rfl⟩ := natDegree_eq_zero.mp h

Premises used: Iff.mp, Polynomial.natDegree_eq_zero, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_1
inst_1 : Field R
r : R
hf : Splits.{u_1} (R := R) ((C : (a : R) → R[X]) r)
h : natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) r) = 0
⊢ resultant ((C : (a : R) → R[X]) r) ((C : (a : R) → R[X]) r) =
    HPow.hPow (α := R) 0 (natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) r))

Tactic:
simp
-- 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]
hf : f.Splits
h : ¬f.natDegree = 0
neg :
  f.leadingCoeff ^ f.natDegree * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x f) f.roots) =
    HPow.hPow (α := R) 0 f.natDegree
⊢ f.resultant f = HPow.hPow (α := R) 0 f.natDegree

Tactic:
rw [resultant_eq_prod_eval _ _ _ le_rfl hf]

Premises used: le_rfl, Polynomial.resultant_eq_prod_eval
-- 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]
hf : f.Splits
h : ¬f.natDegree = 0
⊢ f.leadingCoeff ^ f.natDegree * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x f) f.roots) =
    HPow.hPow (α := R) 0 f.natDegree

Tactic:
simp [zero_pow h, h, hf.exists_eval_eq_zero (degree_ne_of_natDegree_ne h), eq_or_ne f]

Premises used: Polynomial.degree_ne_of_natDegree_ne, eq_or_ne, Polynomial.Splits.exists_eval_eq_zero, zero_pow
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 : (map φ f).resultant (map φ f) = HPow.hPow (α := S) 0 (map φ f).natDegree
injective :
  Eq (α := S) ((φ : (a : R) → S) (f.resultant f) : S) ((φ : (a : R) → S) (HPow.hPow (α := R) 0 f.natDegree) : S)
⊢ f.resultant f = HPow.hPow (α := R) 0 f.natDegree

Tactic:
apply hφ
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 : (map φ f).resultant (map φ f) = HPow.hPow (α := S) 0 (map φ f).natDegree
⊢ Eq (α := S) ((φ : (a : R) → S) (f.resultant f) : S) ((φ : (a : R) → S) (HPow.hPow (α := R) 0 f.natDegree) : S)

Tactic:
simpa only [resultant_map_map, natDegree_map_eq_of_injective hφ, map_zero, map_pow] using IH

Premises used: map_zero, map_pow, Polynomial.resultant_map_map, Polynomial.natDegree_map_eq_of_injective
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 : R[X]), q.resultant q = HPow.hPow (α := R) 0 q.natDegree
surjective :
  ∀ (f' : R[X]) (hf' : map φ f' = f) (e : f'.degree = f.degree), f.resultant f = HPow.hPow (α := S) 0 f.natDegree
⊢ f.resultant f = HPow.hPow (α := S) 0 f.natDegree

Tactic:
obtain ⟨f', hf', e⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)

Premises used: Polynomial.map_surjective, Polynomial.exists_degree_eq_of_mem_lifts
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 : R[X]), q.resultant q = HPow.hPow (α := R) 0 q.natDegree
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
surjective : (map φ f').resultant (map φ f') = HPow.hPow (α := S) 0 (map φ f').natDegree
surjective₁ :
  (φ : (a : R) → S) (f'.resultant f' (map φ f').natDegree (map φ f').natDegree) =
    HPow.hPow (α := S) 0 (map φ f').natDegree
surjective₂ : (φ : (a : R) → S) (f'.resultant f' f.natDegree f.natDegree) = HPow.hPow (α := S) 0 f.natDegree
surjective₃ : (φ : (a : R) → S) (f'.resultant f') = HPow.hPow (α := S) 0 f'.natDegree
surjective₄ : (φ : (a : R) → S) (HPow.hPow (α := R) 0 f'.natDegree) = HPow.hPow (α := S) 0 f'.natDegree
surjective₅ : HPow.hPow (α := S) ((φ : (a : R) → S) 0 : S) f'.natDegree = HPow.hPow (α := S) 0 f'.natDegree
surjective₆ surjective₇ : HPow.hPow (α := S) 0 f'.natDegree = HPow.hPow (α := S) 0 f'.natDegree
⊢ f.resultant f = HPow.hPow (α := S) 0 f.natDegree

Tactic:
rw [← hf', resultant_map_map, hf', ← natDegree_eq_natDegree e, IH f', map_pow, map_zero]

Premises used: map_zero, map_pow, Polynomial.natDegree_eq_natDegree, Polynomial.resultant_map_map
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
Splits : ∀ (R : Type u_1) [inst : Field R] (f : R[X]) (hf : f.Splits), f.resultant f = HPow.hPow (α := R) 0 f.natDegree
injective :
  ∀ (R S : Type u_1) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)) (f : R[X])
    (IH : (map φ f).resultant (map φ f) = HPow.hPow (α := S) 0 (map φ f).natDegree),
    f.resultant f = HPow.hPow (α := R) 0 f.natDegree
surjective :
  ∀ (R S : Type u_1) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)) (f : S[X])
    (IH : ∀ (q : R[X]), q.resultant q = HPow.hPow (α := R) 0 q.natDegree),
    f.resultant f = HPow.hPow (α := S) 0 f.natDegree
⊢ f.resultant f = HPow.hPow (α := R) 0 f.natDegree

Tactic:
induction f using induction_of_Splits_of_injective_of_surjective with
  | Splits R f hf =>
    by_cases h : f.natDegree = 0
    · obtain ⟨r, rfl⟩ := natDegree_eq_zero.mp h; simp
    rw [resultant_eq_prod_eval _ _ _ le_rfl hf]
    simp [zero_pow h, h, hf.exists_eval_eq_zero (degree_ne_of_natDegree_ne h), eq_or_ne f]
  | injective R S φ hφ f IH =>
    apply hφ
    simpa only [resultant_map_map, natDegree_map_eq_of_injective hφ, map_zero, map_pow] using IH
  | surjective R S φ hφ f IH =>
    obtain ⟨f', hf', e⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)
    rw [← hf', resultant_map_map, hf', ← natDegree_eq_natDegree e, IH f', map_pow, map_zero]

Premises used: map_zero, map_pow, Polynomial.resultant_map_map, eq_or_ne, Polynomial.induction_of_Splits_of_injective_of_surjective, Polynomial.Splits, Polynomial.natDegree, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
h : f.natDegree ≠ 0
⊢ f.resultant f = 0

Tactic:
simp [resultant_self, h]

Premises used: Polynomial.resultant_self
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
inl : ∀ (H : IsCoprime 0 g), ∃ (n : ℕ), resultant 0 g ∣ HPow.hPow (α := R) (leadingCoeff 0) n
inr : ∀ (hf : f ≠ 0), ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
⊢ ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n

Tactic:
obtain rfl | hf := eq_or_ne f 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
g : R[X]
H : IsCoprime 0 g
⊢ ∃ (r : R), IsUnit r ∧ (C : (a : R) → R[X]) r = g

Tactic:
simp only [isCoprime_zero_left, isUnit_iff] at H

Premises used: Polynomial.isUnit_iff, isCoprime_zero_left
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
g : R[X]
H : ∃ (r : R), IsUnit r ∧ (C : (a : R) → R[X]) r = g
⊢ ∃ (n : ℕ), resultant 0 g ∣ HPow.hPow (α := R) (leadingCoeff 0) n

Tactic:
aesop
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
inr : ∀ (H : IsCoprime f 0), ∃ (n : ℕ), f.resultant 0 ∣ f.leadingCoeff ^ n
inr₁ : ∀ (hg : g ≠ 0), ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
⊢ ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n

Tactic:
obtain rfl | hg := eq_or_ne g 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
hf : f ≠ 0
H : IsCoprime f 0
⊢ ∃ (r : R), IsUnit r ∧ (C : (a : R) → R[X]) r = f

Tactic:
simp only [isCoprime_zero_right, isUnit_iff] at H

Premises used: Polynomial.isUnit_iff, isCoprime_zero_right
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
hf : f ≠ 0
H : ∃ (r : R), IsUnit r ∧ (C : (a : R) → R[X]) r = f
⊢ ∃ (n : ℕ), f.resultant 0 ∣ f.leadingCoeff ^ n

Tactic:
aesop
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
inr : ∀ (a b : R[X]) (e : a * f + b * g = 1), ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
⊢ ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n

Tactic:
have ⟨a, b, e⟩ := H
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
inr : ∀ (e : 0 * f + b * g = 1), ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
inr₁ : ∀ (ha : a ≠ 0), ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
⊢ ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
b : R[X]
e : 0 * f + b * g = 1
⊢ b * g = 1

Tactic:
simpa using e
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
b : R[X]
e : 0 * f + b * g = 1
inr :
  ∀ (r : R) (hr : IsUnit r) (H : IsCoprime f ((C : (a : R) → R[X]) r))
    (hg : Ne (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X]))
    (e : 0 * f + HMul.hMul (β := R[X]) b ((C : (a : R) → R[X]) r : R[X]) = 1),
    ∃ (n : ℕ), f.resultant ((C : (a : R) → R[X]) r) ∣ f.leadingCoeff ^ n
⊢ ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n

Tactic:
obtain ⟨r, hr, rfl⟩ := isUnit_iff.mp (.of_mul_eq_one_right b (by simpa using e))

Premises used: Polynomial.isUnit_iff, IsUnit.of_mul_eq_one_right, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
hf : f ≠ 0
b : R[X]
r : R
hr : IsUnit r
H : IsCoprime f ((C : (a : R) → R[X]) r)
hg : Ne (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X])
e : 0 * f + HMul.hMul (β := R[X]) b ((C : (a : R) → R[X]) r : R[X]) = 1
⊢ ∃ (n : ℕ), f.resultant ((C : (a : R) → R[X]) r) ∣ f.leadingCoeff ^ n

Tactic:
simp [hr.pow]

Premises used: IsUnit.pow
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
inr : ∀ (e : a * f + 0 * g = 1), ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
inr₁ : ∀ (hb : b ≠ 0), ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n
⊢ ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n

Tactic:
obtain rfl | hb := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a : R[X]
ha : a ≠ 0
e : a * f + 0 * g = 1
⊢ a * f = 1

Tactic:
simpa using e
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a : R[X]
ha : a ≠ 0
e : a * f + 0 * g = 1
inr :
  ∀ (r : R) (hr : IsUnit r) (H : IsCoprime ((C : (a : R) → R[X]) r) g)
    (hf : Ne (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X]))
    (e : HMul.hMul (β := R[X]) a ((C : (a : R) → R[X]) r : R[X]) + 0 * g = 1),
    ∃ (n : ℕ), resultant ((C : (a : R) → R[X]) r) g ∣ HPow.hPow (α := R) (leadingCoeff ((C : (a : R) → R[X]) r)) n
⊢ ∃ (n : ℕ), f.resultant g ∣ f.leadingCoeff ^ n

Tactic:
obtain ⟨r, hr, rfl⟩ := isUnit_iff.mp (.of_mul_eq_one_right a (by simpa using e))

Premises used: Polynomial.isUnit_iff, IsUnit.of_mul_eq_one_right, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
g : R[X]
hg : g ≠ 0
a : R[X]
ha : a ≠ 0
r : R
hr : IsUnit r
H : IsCoprime ((C : (a : R) → R[X]) r) g
hf : Ne (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X])
e : HMul.hMul (β := R[X]) a ((C : (a : R) → R[X]) r : R[X]) + 0 * g = 1
⊢ ∃ (n : ℕ), resultant ((C : (a : R) → R[X]) r) g ∣ HPow.hPow (α := R) (leadingCoeff ((C : (a : R) → R[X]) r)) n

Tactic:
simp [hr.pow]

Premises used: IsUnit.pow
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
⊢ f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g

Tactic:
have := resultant_mul_right f b g _ le_rfl