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
Splits :
  ∀ (x : R[X])
    (h :
      Membership.mem (γ := Set R[X])
        ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
          {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
        x),
    resultant ((taylor r : (a : R[X]) → R[X]) x) ((taylor r : (a : R[X]) → R[X]) g) = x.resultant g
⊢ resultant ((taylor r : (a : R[X]) → R[X]) f) ((taylor r : (a : R[X]) → R[X]) g) = f.resultant g
have Splits₁ : resultant ((taylor r : (a : R[X]) → R[X]) 1) ((taylor r : (a : R[X]) → R[X]) g) = resultant 1 g
Tactic: induction hf' using Submonoid.closure_induction with
    | mem x h =>
      obtain (⟨s, rfl⟩ | ⟨s, rfl⟩) := h
      · rw [taylor_C]; simp
      · nontriviality R
        rw [map_add, taylor_X, taylor_C, add_assoc, ← map_add]
        simp [-map_add, taylor_eval]
    | one => simp
    | mul x y hx hy hx' hy' =>
      by_cases hx0 : x = 0; · simp [hx0]
      by_cases hy0 : y = 0; · simp [hy0]
      rw [taylor_mul, natDegree_mul' (by simp [*]), resultant_mul_left _ _ _ _ le_rfl]
      simp [natDegree_mul', hx0, hy0, resultant_mul_left, ← hx', ← hy']
Cleared hypotheses: hf'
-- 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
Splits :
  ∀ (x : R[X])
    (h :
      Membership.mem (γ := Set R[X])
        ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
          {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
        x),
    resultant ((taylor r : (a : R[X]) → R[X]) x) ((taylor r : (a : R[X]) → R[X]) g) = x.resultant g
Splits₁ : resultant ((taylor r : (a : R[X]) → R[X]) 1) ((taylor r : (a : R[X]) → R[X]) g) = resultant 1 g
⊢ resultant ((taylor r : (a : R[X]) → R[X]) f) ((taylor r : (a : R[X]) → R[X]) g) = f.resultant g
have Splits₂ : ∀ (x y : R[X])
  (hx :
    Membership.mem (γ := Submonoid R[X])
      (Submonoid.closure
        ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
          {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
      x)
  (hy :
    Membership.mem (γ := Submonoid R[X])
      (Submonoid.closure
        ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
          {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
      y)
  (hx' : resultant ((taylor r : (a : R[X]) → R[X]) x) ((taylor r : (a : R[X]) → R[X]) g) = x.resultant g)
  (hy' : resultant ((taylor r : (a : R[X]) → R[X]) y) ((taylor r : (a : R[X]) → R[X]) g) = y.resultant g),
  resultant ((taylor r : (a : R[X]) → R[X]) (x * y)) ((taylor r : (a : R[X]) → R[X]) g) = (x * y).resultant g
Tactic: induction hf' using Submonoid.closure_induction with
    | mem x h =>
      obtain (⟨s, rfl⟩ | ⟨s, rfl⟩) := h
      · rw [taylor_C]; simp
      · nontriviality R
        rw [map_add, taylor_X, taylor_C, add_assoc, ← map_add]
        simp [-map_add, taylor_eval]
    | one => simp
    | mul x y hx hy hx' hy' =>
      by_cases hx0 : x = 0; · simp [hx0]
      by_cases hy0 : y = 0; · simp [hy0]
      rw [taylor_mul, natDegree_mul' (by simp [*]), resultant_mul_left _ _ _ _ le_rfl]
      simp [natDegree_mul', hx0, hy0, resultant_mul_left, ← hx', ← hy']
Cleared hypotheses: hf'
-- 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),
    resultant ((taylor r : (a : S[X]) → S[X]) (map φ f)) ((taylor r : (a : S[X]) → S[X]) g) = (map φ f).resultant g
g : R[X]
r : R
⊢ resultant ((taylor r : (a : R[X]) → R[X]) f) ((taylor r : (a : R[X]) → R[X]) g) = f.resultant g
have injective : Eq (α := S) ((φ : (a : R) → S) (resultant ((taylor r : (a : R[X]) → R[X]) f) ((taylor r : (a : R[X]) → R[X]) g)) : S)
  ((φ : (a : R) → S) (f.resultant g) : S)
Tactic: apply hφ
-- 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),
    resultant ((taylor r : (a : S[X]) → S[X]) (map φ f)) ((taylor r : (a : S[X]) → S[X]) g) = (map φ f).resultant g
g : R[X]
r : R
⊢ Eq (α := S) ((φ : (a : R) → S) (resultant ((taylor r : (a : R[X]) → R[X]) f) ((taylor r : (a : R[X]) → R[X]) g)) : S)
    ((φ : (a : R) → S) (f.resultant g) : S)
have this : resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) (map φ f))
    (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) (map φ g)) =
  (map φ f).resultant (map φ g)
Tactic: have := IH (g.map φ) (φ r)
-- 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),
    resultant ((taylor r : (a : S[X]) → S[X]) (map φ f)) ((taylor r : (a : S[X]) → S[X]) g) = (map φ f).resultant g
g : R[X]
r : R
this :
  resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) (map φ f))
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) (map φ g)) =
    (map φ f).resultant (map φ g)
⊢ Eq (α := S) ((φ : (a : R) → S) (resultant ((taylor r : (a : R[X]) → R[X]) f) ((taylor r : (a : R[X]) → R[X]) g)) : S)
    ((φ : (a : R) → S) (f.resultant g) : S)
have this₁ : (map φ ((taylor r : (a : R[X]) → R[X]) f)).resultant (map φ ((taylor r : (a : R[X]) → R[X]) g)) =
  (map φ f).resultant (map φ g)
Tactic: rw [← map_taylor, ← map_taylor] 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.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)
f : S[X]
IH :
  ∀ (q g : R[X]) (r : R),
    resultant ((taylor r : (a : R[X]) → R[X]) q) ((taylor r : (a : R[X]) → R[X]) g) = q.resultant g
g : S[X]
r : S
⊢ resultant ((taylor r : (a : S[X]) → S[X]) f) ((taylor r : (a : S[X]) → S[X]) g) = f.resultant g
have surjective : ∀ (f' : R[X]) (hf' : map φ f' = f) (ef : f'.degree = f.degree),
  resultant ((taylor r : (a : S[X]) → S[X]) f) ((taylor r : (a : S[X]) → S[X]) g) = 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),
    resultant ((taylor r : (a : R[X]) → R[X]) q) ((taylor r : (a : R[X]) → R[X]) g) = q.resultant g
g : S[X]
r : S
f' : R[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
⊢ resultant ((taylor r : (a : S[X]) → S[X]) f) ((taylor r : (a : S[X]) → S[X]) g) = f.resultant g
have surjective : ∀ (g' : R[X]) (hg' : map φ g' = g) (eg : g'.degree = g.degree),
  resultant ((taylor r : (a : S[X]) → S[X]) f) ((taylor r : (a : S[X]) → S[X]) g) = 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),
    resultant ((taylor r : (a : R[X]) → R[X]) q) ((taylor r : (a : R[X]) → R[X]) g) = q.resultant g
g : S[X]
r : S
f' : R[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : R[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
⊢ resultant ((taylor r : (a : S[X]) → S[X]) f) ((taylor r : (a : S[X]) → S[X]) g) = f.resultant g
have surjective : ∀ (r : R),
  resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) f)
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) =
    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),
    resultant ((taylor r : (a : R[X]) → R[X]) q) ((taylor r : (a : R[X]) → R[X]) g) = q.resultant g
g : S[X]
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),
    resultant ((taylor r : (a : R[X]) → R[X]) q) ((taylor r : (a : R[X]) → R[X]) g) = q.resultant g
g : S[X]
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),
    resultant ((taylor r : (a : R[X]) → R[X]) q) ((taylor r : (a : R[X]) → R[X]) g) = q.resultant g
g : S[X]
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),
    resultant ((taylor r : (a : R[X]) → R[X]) q) ((taylor r : (a : R[X]) → R[X]) g) = q.resultant g
g : S[X]
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
⊢ resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) f)
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) =
    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),
    resultant ((taylor r : (a : R[X]) → R[X]) q) ((taylor r : (a : R[X]) → R[X]) g) = q.resultant g
g : S[X]
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),
    resultant ((taylor r : (a : R[X]) → R[X]) q) ((taylor r : (a : R[X]) → R[X]) g) = q.resultant g
g : S[X]
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),
    resultant ((taylor r : (a : R[X]) → R[X]) q) ((taylor r : (a : R[X]) → R[X]) g) = q.resultant g
g : S[X]
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]
-- 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),
    resultant ((taylor r : (a : R[X]) → R[X]) q) ((taylor r : (a : R[X]) → R[X]) g) = q.resultant g
g : S[X]
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
⊢ resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) f)
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) =
    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),
    resultant ((taylor r : (a : R[X]) → R[X]) q) ((taylor r : (a : R[X]) → R[X]) g) = q.resultant g
g : S[X]
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
⊢ resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) f)
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) =
    f.resultant g
have surjective : resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) f)
    (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) f.natDegree =
  f.resultant g
Tactic: rw [natDegree_taylor, natDegree_taylor, ← hf', ← map_taylor, ← hg', ← map_taylor,
      resultant_map_map, resultant_map_map, hf', hg', ← natDegree_eq_natDegree ef,
      ← natDegree_eq_natDegree eg, ← IH f' g' r, natDegree_taylor, natDegree_taylor]
-- 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),
    resultant ((taylor r : (a : R[X]) → R[X]) q) ((taylor r : (a : R[X]) → R[X]) g) = q.resultant g
g : S[X]
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
surjective :
  resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) f)
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) f.natDegree =
    f.resultant g
⊢ resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) f)
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) =
    f.resultant g
have surjective₁ : resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) f)
    (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) f.natDegree g.natDegree =
  f.resultant g
Tactic: rw [natDegree_taylor, natDegree_taylor, ← hf', ← map_taylor, ← hg', ← map_taylor,
      resultant_map_map, resultant_map_map, hf', hg', ← natDegree_eq_natDegree ef,
      ← natDegree_eq_natDegree eg, ← IH f' g' r, natDegree_taylor, natDegree_taylor]
-- 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),
    resultant ((taylor r : (a : R[X]) → R[X]) q) ((taylor r : (a : R[X]) → R[X]) g) = q.resultant g
g : S[X]
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
surjective :
  resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) f)
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) f.natDegree =
    f.resultant g
surjective₁ :
  resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) f)
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) f.natDegree g.natDegree =
    f.resultant g
⊢ resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) f)
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) =
    f.resultant g
have surjective₂ : resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) (map φ f'))
    (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) (map φ f').natDegree g.natDegree =
  (map φ f').resultant g
Tactic: rw [natDegree_taylor, natDegree_taylor, ← hf', ← map_taylor, ← hg', ← map_taylor,
      resultant_map_map, resultant_map_map, hf', hg', ← natDegree_eq_natDegree ef,
      ← natDegree_eq_natDegree eg, ← IH f' g' r, natDegree_taylor, natDegree_taylor]
-- 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),
    resultant ((taylor r : (a : R[X]) → R[X]) q) ((taylor r : (a : R[X]) → R[X]) g) = q.resultant g
g : S[X]
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
surjective :
  resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) f)
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) f.natDegree =
    f.resultant g
surjective₁ :
  resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) f)
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) f.natDegree g.natDegree =
    f.resultant g
surjective₂ :
  resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) (map φ f'))
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) (map φ f').natDegree g.natDegree =
    (map φ f').resultant g
⊢ resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) f)
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) =
    f.resultant g
have surjective₃ : (map φ ((taylor r : (a : R[X]) → R[X]) f')).resultant
    (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) (map φ f').natDegree g.natDegree =
  (map φ f').resultant g
Tactic: rw [natDegree_taylor, natDegree_taylor, ← hf', ← map_taylor, ← hg', ← map_taylor,
      resultant_map_map, resultant_map_map, hf', hg', ← natDegree_eq_natDegree ef,
      ← natDegree_eq_natDegree eg, ← IH f' g' r, natDegree_taylor, natDegree_taylor]
-- 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),
    resultant ((taylor r : (a : R[X]) → R[X]) q) ((taylor r : (a : R[X]) → R[X]) g) = q.resultant g
g : S[X]
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
surjective :
  resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) f)
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) f.natDegree =
    f.resultant g
surjective₁ :
  resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) f)
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) f.natDegree g.natDegree =
    f.resultant g
surjective₂ :
  resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) (map φ f'))
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) (map φ f').natDegree g.natDegree =
    (map φ f').resultant g
surjective₃ :
  (map φ ((taylor r : (a : R[X]) → R[X]) f')).resultant
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) (map φ f').natDegree g.natDegree =
    (map φ f').resultant g
⊢ resultant (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) f)
      (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) g) =
    f.resultant g
have surjective₄ : (map φ ((taylor r : (a : R[X]) → R[X]) f')).resultant
    (((taylor ((φ : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) (map φ g')) (map φ f').natDegree
    (map φ g').natDegree =
  (map φ f').resultant (map φ g')
Tactic: rw [natDegree_taylor, natDegree_taylor, ← hf', ← map_taylor, ← hg', ← map_taylor,
      resultant_map_map, resultant_map_map, hf', hg', ← natDegree_eq_natDegree ef,
      ← natDegree_eq_natDegree eg, ← IH f' g' r, natDegree_taylor, natDegree_taylor]