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 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
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')
⊢ 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 (map φ ((taylor r : (a : R[X]) → R[X]) 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]
-- 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
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')
surjective₅ :
  (map φ ((taylor r : (a : R[X]) → R[X]) f')).resultant (map φ ((taylor r : (a : R[X]) → R[X]) g')) (map φ f').natDegree
      (map φ g').natDegree =
    (map φ f').resultant (map φ 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₆ : (φ : (a : R) → S)
    (resultant ((taylor r : (a : R[X]) → R[X]) f') ((taylor r : (a : R[X]) → R[X]) 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]
-- 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
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')
surjective₅ :
  (map φ ((taylor r : (a : R[X]) → R[X]) f')).resultant (map φ ((taylor r : (a : R[X]) → R[X]) g')) (map φ f').natDegree
      (map φ g').natDegree =
    (map φ f').resultant (map φ g')
surjective₆ :
  (φ : (a : R) → S)
      (resultant ((taylor r : (a : R[X]) → R[X]) f') ((taylor r : (a : R[X]) → R[X]) g') (map φ f').natDegree
        (map φ g').natDegree) =
    (map φ f').resultant (map φ 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₇ : Eq (α := S)
  ((φ : (a : R) → S)
      (resultant ((taylor r : (a : R[X]) → R[X]) f') ((taylor r : (a : R[X]) → R[X]) g') (map φ f').natDegree
        (map φ g').natDegree) :
    S)
  ((φ : (a : R) → S) (f'.resultant g' (map φ f').natDegree (map φ g').natDegree) : S)
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
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')
surjective₅ :
  (map φ ((taylor r : (a : R[X]) → R[X]) f')).resultant (map φ ((taylor r : (a : R[X]) → R[X]) g')) (map φ f').natDegree
      (map φ g').natDegree =
    (map φ f').resultant (map φ g')
surjective₆ :
  (φ : (a : R) → S)
      (resultant ((taylor r : (a : R[X]) → R[X]) f') ((taylor r : (a : R[X]) → R[X]) g') (map φ f').natDegree
        (map φ g').natDegree) =
    (map φ f').resultant (map φ g')
surjective₇ :
  Eq (α := S)
    ((φ : (a : R) → S)
        (resultant ((taylor r : (a : R[X]) → R[X]) f') ((taylor r : (a : R[X]) → R[X]) g') (map φ f').natDegree
          (map φ g').natDegree) :
      S)
    ((φ : (a : R) → S) (f'.resultant g' (map φ f').natDegree (map φ g').natDegree) : S)
⊢ 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₈ : Eq (α := S)
  ((φ : (a : R) → S)
      (resultant ((taylor r : (a : R[X]) → R[X]) f') ((taylor r : (a : R[X]) → R[X]) g') f.natDegree
        (map φ g').natDegree) :
    S)
  ((φ : (a : R) → S) (f'.resultant g' f.natDegree (map φ g').natDegree) : S)
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 : Type u_1
inst : CommRing R
f 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 Splits : ∀ (R : Type u_1) [inst : Field R] (f : R[X]) (hf' : f.Splits) (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
Tactic: induction f using induction_of_Splits_of_injective_of_surjective with
  | Splits R f hf' =>
    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']
  | injective R S φ hφ f IH =>
    apply hφ
    have := IH (g.map φ) (φ r)
    rw [← map_taylor, ← map_taylor] at this
    simpa [natDegree_map_eq_of_injective hφ] using this
  | surjective R S φ hφ f IH =>
    obtain ⟨f', hf', ef⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)
    obtain ⟨g', hg', eg⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ g)
    obtain ⟨r, rfl⟩ := hφ r
    have hfl : f.leadingCoeff = φ f'.leadingCoeff := by
      simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree ef, ← hf', coeff_map]
    have hgl : g.leadingCoeff = φ g'.leadingCoeff := by
      simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree eg, ← hg', coeff_map]
    rw [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]
Cleared hypotheses: f, g, r
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
Splits :
  ∀ (R : Type u_1) [inst : Field R] (f : R[X]) (hf' : f.Splits) (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
⊢ resultant ((taylor r : (a : R[X]) → R[X]) f) ((taylor r : (a : R[X]) → R[X]) g) = f.resultant g
have 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 :
    ∀ (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
Tactic: induction f using induction_of_Splits_of_injective_of_surjective with
  | Splits R f hf' =>
    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']
  | injective R S φ hφ f IH =>
    apply hφ
    have := IH (g.map φ) (φ r)
    rw [← map_taylor, ← map_taylor] at this
    simpa [natDegree_map_eq_of_injective hφ] using this
  | surjective R S φ hφ f IH =>
    obtain ⟨f', hf', ef⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)
    obtain ⟨g', hg', eg⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ g)
    obtain ⟨r, rfl⟩ := hφ r
    have hfl : f.leadingCoeff = φ f'.leadingCoeff := by
      simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree ef, ← hf', coeff_map]
    have hgl : g.leadingCoeff = φ g'.leadingCoeff := by
      simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree eg, ← hg', coeff_map]
    rw [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]
Cleared hypotheses: f, g, r
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
Splits :
  ∀ (R : Type u_1) [inst : Field R] (f : R[X]) (hf' : f.Splits) (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
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 :
      ∀ (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
⊢ resultant ((taylor r : (a : R[X]) → R[X]) f) ((taylor r : (a : R[X]) → R[X]) g) = f.resultant g
have 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 : 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
Tactic: induction f using induction_of_Splits_of_injective_of_surjective with
  | Splits R f hf' =>
    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']
  | injective R S φ hφ f IH =>
    apply hφ
    have := IH (g.map φ) (φ r)
    rw [← map_taylor, ← map_taylor] at this
    simpa [natDegree_map_eq_of_injective hφ] using this
  | surjective R S φ hφ f IH =>
    obtain ⟨f', hf', ef⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)
    obtain ⟨g', hg', eg⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ g)
    obtain ⟨r, rfl⟩ := hφ r
    have hfl : f.leadingCoeff = φ f'.leadingCoeff := by
      simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree ef, ← hf', coeff_map]
    have hgl : g.leadingCoeff = φ g'.leadingCoeff := by
      simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree eg, ← hg', coeff_map]
    rw [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]
Cleared hypotheses: f, g, r
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
pq : ↥R[X]_m × ↥R[X]_n
⊢ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) (f * (↑pq.2 : R[X]) + g * (↑pq.1 : R[X]))
have obtain : ∀ (p : R[X]) (hp : Membership.mem (γ := Submodule R R[X]) (R[X]_m) p) (q : R[X])
  (hq : Membership.mem (γ := Submodule R R[X]) (R[X]_n) q),
  Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n))
    (f *
        (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_m) x) p hp,
                Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x) q hq).2 :
          R[X]) +
      g *
        (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_m) x) p hp,
                Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x) q hq).1 :
          R[X]))
Tactic: obtain ⟨⟨p, hp⟩, ⟨q, hq⟩⟩ := pq
Cleared hypotheses: pq
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (R[X]_m) p
q : R[X]
hq : Membership.mem (γ := Submodule R R[X]) (R[X]_n) q
⊢ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n))
    (f *
        (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_m) x) p hp,
                Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x) q hq).2 :
          R[X]) +
      g *
        (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_m) x) p hp,
                Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x) q hq).1 :
          R[X]))
have rw : (f *
        (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_m) x) p hp,
                Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x) q hq).2 :
          R[X]) +
      g *
        (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_m) x) p hp,
                Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x) q hq).1 :
          R[X])).degree <
  (↑(m + n) : WithBot ℕ)
Tactic: rw [Polynomial.mem_degreeLT]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (R[X]_m) p
q : R[X]
hq : Membership.mem (γ := Submodule R R[X]) (R[X]_n) q
⊢ (f *
          (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_m) x) p hp,
                  Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x) q hq).2 :
            R[X]) +
        g *
          (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_m) x) p hp,
                  Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x) q hq).1 :
            R[X])).degree <
    (↑(m + n) : WithBot ℕ)
have refine_1 : (f *
      (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_m) x) p hp,
              Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x) q hq).2 :
        R[X])).degree <
  (↑(m + n) : WithBot ℕ)
Tactic: refine (degree_add_le _ _).trans_lt (max_lt ?_ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (R[X]_m) p
q : R[X]
hq : Membership.mem (γ := Submodule R R[X]) (R[X]_n) q
refine_1 :
  (f *
        (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_m) x) p hp,
                Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x) q hq).2 :
          R[X])).degree <
    (↑(m + n) : WithBot ℕ)
⊢ (f *
          (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_m) x) p hp,
                  Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x) q hq).2 :
            R[X]) +
        g *
          (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_m) x) p hp,
                  Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x) q hq).1 :
            R[X])).degree <
    (↑(m + n) : WithBot ℕ)
have refine_2 : (g *
      (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_m) x) p hp,
              Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x) q hq).1 :
        R[X])).degree <
  (↑(m + n) : WithBot ℕ)
Tactic: refine (degree_add_le _ _).trans_lt (max_lt ?_ ?_)