awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  ∀ (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 ((φ : (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)
-- 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 :
  ∀ (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)
⊢ (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

Premises used: Polynomial.map_taylor
-- 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 :
  ∀ (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 :
  (map φ ((taylor r : (a : R[X]) → R[X]) f)).resultant (map φ ((taylor r : (a : R[X]) → R[X]) 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)

Tactic:
simpa [natDegree_map_eq_of_injective hφ] using this

Premises used: 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 : 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
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
⊢ 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)

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 : 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
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
⊢ 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)

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 : 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
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
⊢ resultant ((taylor r : (a : S[X]) → S[X]) f) ((taylor r : (a : S[X]) → S[X]) g) = f.resultant g

Tactic:
obtain ⟨r, rfl⟩ := hφ r

Premises used: rfl
-- 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 : 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)
simp_rw₂ : (map φ f').coeff f'.natDegree = (φ : (a : R) → S) (f'.coeff f'.natDegree)
⊢ f.leadingCoeff = (φ : (a : R) → S) f'.leadingCoeff

Tactic:
simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree ef, ← hf', coeff_map]

Premises used: Polynomial.coeff_map, Polynomial.coeff_natDegree, Polynomial.natDegree_eq_natDegree
-- 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 : 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

Tactic:
have hfl : f.leadingCoeff = φ f'.leadingCoeff := by
      simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree ef, ← hf', coeff_map]
-- 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 : 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)
simp_rw₂ : (map φ g').coeff g'.natDegree = (φ : (a : R) → S) (g'.coeff g'.natDegree)
⊢ g.leadingCoeff = (φ : (a : R) → S) g'.leadingCoeff

Tactic:
simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree eg, ← hg', coeff_map]

Premises used: Polynomial.coeff_map, Polynomial.coeff_natDegree, Polynomial.natDegree_eq_natDegree
-- 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 : 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

Tactic:
have hgl : g.leadingCoeff = φ g'.leadingCoeff := by
      simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree eg, ← hg', coeff_map]
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
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]))
⊢ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) (f * (↑pq.2 : R[X]) + g * (↑pq.1 : R[X]))

Tactic:
obtain ⟨⟨p, hp⟩, ⟨q, hq⟩⟩ := pq
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
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 ℕ)
⊢ 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:
rw [Polynomial.mem_degreeLT]

Premises used: Polynomial.mem_degreeLT
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 ℕ)

Tactic:
(degree_add_le _ _).trans_lt (max_lt ?_ ?_)

Premises used: max_lt, Polynomial.degree_add_le, LE.le.trans_lt
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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 ℕ)
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 ℕ)
⊢ (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:
refine (degree_add_le _ _).trans_lt (max_lt ?_ ?_)

Premises used: max_lt, Polynomial.degree_add_le, LE.le.trans_lt
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
pos :
  ∀ (hf' : f = 0),
    (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 ℕ)
neg :
  ∀ (hf' : ¬f = 0),
    (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])).degree <
    (↑(m + n) : WithBot ℕ)

Tactic:
by_cases hf' : f = 0
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
hf' : f = 0
⊢ (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:
simp_all
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
hf' : ¬f = 0
⊢ f.degree ≠ ⊥

Tactic:
simpa
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
hf' : ¬f = 0
⊢ q.degree < (↑n : WithBot ℕ)

Tactic:
simpa using hq
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
hf' : ¬f = 0
⊢ (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:
exact (degree_mul_le _ _).trans_lt (WithBot.add_lt_add_of_le_of_lt (by simpa)
        (degree_le_of_natDegree_le hf) (by simpa using hq))

Premises used: Polynomial.degree_mul_le, Polynomial.degree_le_of_natDegree_le, WithBot.add_lt_add_of_le_of_lt, LE.le.trans_lt
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
pos :
  ∀ (hg' : g = 0),
    (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 ℕ)
neg :
  ∀ (hg' : ¬g = 0),
    (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 ℕ)
⊢ (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:
by_cases hg' : g = 0
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
hg' : g = 0
⊢ (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:
simp_all
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
hg' : ¬g = 0
⊢ g.degree ≠ ⊥

Tactic:
simpa
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
hg' : ¬g = 0
⊢ (↑(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 : WithBot ℕ)

Tactic:
simpa using hp
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
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
hg' : ¬g = 0
⊢ (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:
exact (degree_mul_le _ _).trans_lt ((WithBot.add_lt_add_of_le_of_lt (by simpa)
        (degree_le_of_natDegree_le hg) (by simpa using hp)).trans_eq (add_comm _ _))

Premises used: Polynomial.degree_mul_le, Polynomial.degree_le_of_natDegree_le, LT.lt.trans_eq, add_comm, WithBot.add_lt_add_of_le_of_lt, LE.le.trans_lt
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
x x_1 : ↥R[X]_m × ↥R[X]_n
a :
  (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x)
          (f * (↑(x + x_1).2 : R[X]) + g * (↑(x + x_1).1 : R[X])) ⋯) :
      R[X]) =
    (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x)
            (f * (↑x.2 : R[X]) + g * (↑x.1 : R[X])) ⋯ +
          Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x)
            (f * (↑x_1.2 : R[X]) + g * (↑x_1.1 : R[X])) ⋯) :
      R[X])
⊢ Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x)
      (f * (↑(x + x_1).2 : R[X]) + g * (↑(x + x_1).1 : R[X])) ⋯ =
    Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x)
        (f * (↑x.2 : R[X]) + g * (↑x.1 : R[X])) ⋯ +
      Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x)
        (f * (↑x_1.2 : R[X]) + g * (↑x_1.1 : R[X])) ⋯

Tactic:
ext1
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
x x_1 : ↥R[X]_m × ↥R[X]_n
⊢ f * ((↑x.2 : R[X]) + (↑x_1.2 : R[X])) + g * ((↑x.1 : R[X]) + (↑x_1.1 : R[X])) =
    f * (↑x.2 : R[X]) + g * (↑x.1 : R[X]) + (f * (↑x_1.2 : R[X]) + g * (↑x_1.1 : R[X]))

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
x : R
x_1 : ↥R[X]_m × ↥R[X]_n
a :
  (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x)
          (f * (↑(x • x_1).2 : R[X]) + g * (↑(x • x_1).1 : R[X])) ⋯) :
      R[X]) =
    (↑(HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R)
          (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x)
            (f * (↑x_1.2 : R[X]) + g * (↑x_1.1 : R[X])) ⋯)) :
      R[X])
⊢ Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x)
      (f * (↑(x • x_1).2 : R[X]) + g * (↑(x • x_1).1 : R[X])) ⋯ =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R)
      (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x)
        (f * (↑x_1.2 : R[X]) + g * (↑x_1.1 : R[X])) ⋯)

Tactic:
ext1
-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
m n : ℕ
R : Type u_1
inst : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
x : R
x_1 : ↥R[X]_m × ↥R[X]_n
⊢ (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x)
          (f * (↑(x • x_1).2 : R[X]) + g * (↑(x • x_1).1 : R[X])) ⋯) :
      R[X]) =
    (↑(HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R)
          (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_(m + n)) x)
            (f * (↑x_1.2 : R[X]) + g * (↑x_1.1 : R[X])) ⋯)) :
      R[X])

Tactic:
simp