mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg.inr
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf' : f.Splits
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
hr : r ≠ 0
⊢ (f.scaleRoots r).leadingCoeff ^ (g.scaleRoots r).natDegree *
      (Multiset.map (fun x ↦ eval x (g.scaleRoots r)) (Multiset.map (fun x ↦ r * x) f.roots)).prod =
    r ^ (f.natDegree * g.natDegree) * (f.leadingCoeff ^ g.natDegree * (Multiset.map (fun x ↦ eval x g) f.roots).prod)

Tactic:
]

Goal state after:
case neg.inr
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf' : f.Splits
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
hr : r ≠ 0
⊢ (f.scaleRoots r).leadingCoeff ^ (g.scaleRoots r).natDegree *
      (Multiset.map (fun x ↦ eval x (g.scaleRoots r)) (Multiset.map (fun x ↦ r * x) f.roots)).prod =
    r ^ (f.natDegree * g.natDegree) * (f.leadingCoeff ^ g.natDegree * (Multiset.map (fun x ↦ eval x g) f.roots).prod)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr.inr.surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH :
  ∀ (q g : R[X]) (r : R),
    q ≠ 0 →
      g ≠ 0 →
        (q.scaleRoots r).resultant (g.scaleRoots r) q.natDegree g.natDegree =
          r ^ (q.natDegree * g.natDegree) * q.resultant g
g : S[X]
hf : f ≠ 0
hg : g ≠ 0
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 = φ f'.leadingCoeff
hgl : g.leadingCoeff = φ g'.leadingCoeff
⊢ φ (r ^ (f'.natDegree * g'.natDegree) * f'.resultant g') =
    φ r ^ (f'.natDegree * g'.natDegree) * f.resultant g f'.natDegree g'.natDegree

Tactic:
]

Goal state after:
case inr.inr.surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH :
  ∀ (q g : R[X]) (r : R),
    q ≠ 0 →
      g ≠ 0 →
        (q.scaleRoots r).resultant (g.scaleRoots r) q.natDegree g.natDegree =
          r ^ (q.natDegree * g.natDegree) * q.resultant g
g : S[X]
hf : f ≠ 0
hg : g ≠ 0
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 = φ f'.leadingCoeff
hgl : g.leadingCoeff = φ g'.leadingCoeff
⊢ φ (r ^ (f'.natDegree * g'.natDegree) * f'.resultant g') =
    φ r ^ (f'.natDegree * g'.natDegree) * f.resultant g f'.natDegree g'.natDegree
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr.inr.surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH :
  ∀ (q g : R[X]) (r : R),
    q ≠ 0 →
      g ≠ 0 →
        (q.scaleRoots r).resultant (g.scaleRoots r) q.natDegree g.natDegree =
          r ^ (q.natDegree * g.natDegree) * q.resultant g
g : S[X]
hf : f ≠ 0
hg : g ≠ 0
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 = φ f'.leadingCoeff
hgl : g.leadingCoeff = φ g'.leadingCoeff
⊢ φ (r ^ (f'.natDegree * g'.natDegree) * f'.resultant g') = φ r ^ (f'.natDegree * g'.natDegree) * φ (f'.resultant g')

Tactic:
]

Goal state after:
case inr.inr.surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH :
  ∀ (q g : R[X]) (r : R),
    q ≠ 0 →
      g ≠ 0 →
        (q.scaleRoots r).resultant (g.scaleRoots r) q.natDegree g.natDegree =
          r ^ (q.natDegree * g.natDegree) * q.resultant g
g : S[X]
hf : f ≠ 0
hg : g ≠ 0
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 = φ f'.leadingCoeff
hgl : g.leadingCoeff = φ g'.leadingCoeff
⊢ φ (r ^ (f'.natDegree * g'.natDegree) * f'.resultant g') = φ r ^ (f'.natDegree * g'.natDegree) * φ (f'.resultant g')
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

Tactic:
natDegree_integralNormalization

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
⊢ (MvPolynomial.mapEquivMonic R 𝓡 n) ((Algebra.ofId R 𝓡).comp ((MvPolynomial.mapEquivMonic R R n).symm p)) =
    monicDegreeEq m k hn p

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
⊢ (MvPolynomial.mapEquivMonic R 𝓡 n) ((Algebra.ofId R 𝓡).comp ((MvPolynomial.mapEquivMonic R R n).symm p)) =
    monicDegreeEq m k hn p
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]),
    g.natDegree ≠ 0 →
      IsDomain R →
        (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
          g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type (max 0 u_1) := MvPolynomial R ℤ
φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap ℤ R) id
hφ : Function.Surjective ⇑φ
f' : S[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : S[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
hfl : f.leadingCoeff = φ f'.leadingCoeff
hgl : g.leadingCoeff = φ g'.leadingCoeff
⊢ φ (g'.leadingCoeff ^ (f'.natDegree * (g'.natDegree - 1)) * f'.resultant g') =
    φ g'.leadingCoeff ^ (f'.natDegree * (g'.natDegree - 1)) * (map φ f').resultant (map φ g') f'.natDegree g'.natDegree

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]),
    g.natDegree ≠ 0 →
      IsDomain R →
        (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
          g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type (max 0 u_1) := MvPolynomial R ℤ
φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap ℤ R) id
hφ : Function.Surjective ⇑φ
f' : S[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : S[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
hfl : f.leadingCoeff = φ f'.leadingCoeff
hgl : g.leadingCoeff = φ g'.leadingCoeff
⊢ φ (g'.leadingCoeff ^ (f'.natDegree * (g'.natDegree - 1)) * f'.resultant g') =
    φ g'.leadingCoeff ^ (f'.natDegree * (g'.natDegree - 1)) * (map φ f').resultant (map φ g') f'.natDegree g'.natDegree
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.inr.inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝² : Nontrivial 𝓡
h✝¹ : Nontrivial (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
h✝ : Nontrivial R
this✝ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
⊢ (fromTensor m k hn p)
      ((-1) ^ n *
        (map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m)).resultant
          (map Algebra.TensorProduct.includeRight.toRingHom (freeMonic R k))) =
    (-1) ^ n * (↑(factor₁ m k hn p)).resultant ↑(factor₂ m k hn p)

Tactic:
]

Goal state after:
case inr.inr.inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝² : Nontrivial 𝓡
h✝¹ : Nontrivial (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
h✝ : Nontrivial R
this✝ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
⊢ (fromTensor m k hn p)
      ((-1) ^ n *
        (map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m)).resultant
          (map Algebra.TensorProduct.includeRight.toRingHom (freeMonic R k))) =
    (-1) ^ n * (↑(factor₁ m k hn p)).resultant ↑(factor₂ m k hn p)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
this :
  g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
⊢ g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)

Tactic:
]

Goal state after:
case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
this :
  g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
⊢ g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.inr.inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝² : Nontrivial 𝓡
h✝¹ : Nontrivial (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
h✝ : Nontrivial R
this✝ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
⊢ (-1) ^ n *
      (map ((↑(fromTensor m k hn p)).comp Algebra.TensorProduct.includeLeftRingHom) (freeMonic R m)).resultant
        (map ((↑(fromTensor m k hn p)).comp Algebra.TensorProduct.includeRight.toRingHom) (freeMonic R k)) m k =
    (-1) ^ n * (↑(factor₁ m k hn p)).resultant (↑(factor₂ m k hn p)) m k

Tactic:
]

Goal state after:
case inr.inr.inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝² : Nontrivial 𝓡
h✝¹ : Nontrivial (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
h✝ : Nontrivial R
this✝ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
⊢ (-1) ^ n *
      (map ((↑(fromTensor m k hn p)).comp Algebra.TensorProduct.includeLeftRingHom) (freeMonic R m)).resultant
        (map ((↑(fromTensor m k hn p)).comp Algebra.TensorProduct.includeRight.toRingHom) (freeMonic R k)) m k =
    (-1) ^ n * (↑(factor₁ m k hn p)).resultant (↑(factor₂ m k hn p)) m k
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝ : Subsingleton 𝓡'
⊢ IsCoprime 1 ↑(factor₂ m k hn p)

Tactic:
]

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝ : Subsingleton 𝓡'
⊢ IsCoprime 1 ↑(factor₂ m k hn p)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
this :
  g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
⊢ g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝ : Nontrivial 𝓡'
⊢ IsUnit
    ((algebraMap 𝓡 𝓡')
      ((↑(UniversalFactorizationRing.factor₁ m k hn p)).resultant ↑(UniversalFactorizationRing.factor₂ m k hn p)))

Tactic:
]

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝ : Nontrivial 𝓡'
⊢ IsUnit
    ((algebraMap 𝓡 𝓡')
      ((↑(UniversalFactorizationRing.factor₁ m k hn p)).resultant ↑(UniversalFactorizationRing.factor₂ m k hn p)))
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case Splits.mem.inl
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
g : R[X]
r s : R
⊢ (C s).resultant ((taylor r) g) = (C s).resultant g

Tactic:
]

Goal state after:
case Splits.mem.inl
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
g : R[X]
r s : R
⊢ (C s).resultant ((taylor r) g) = (C s).resultant g
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝ : Nontrivial 𝓡'
⊢ IsUnit ((algebraMap 𝓡 𝓡') (UniversalFactorizationRing.presentation m k hn p).jacobian)

Tactic:
]

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝ : Nontrivial 𝓡'
⊢ IsUnit ((algebraMap 𝓡 𝓡') (UniversalFactorizationRing.presentation m k hn p).jacobian)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case Splits.mem.inr
R✝ : Type u_1
inst✝² : CommRing R✝
R : Type u_1
inst✝¹ : Field R
f : R[X]
g : R[X]
r s : R
inst✝ : Nontrivial R
⊢ (X + C (r + s)).resultant ((taylor r) g) = (X + C s).resultant g

Tactic:
]

Goal state after:
case Splits.mem.inr
R✝ : Type u_1
inst✝² : CommRing R✝
R : Type u_1
inst✝¹ : Field R
f : R[X]
g : R[X]
r s : R
inst✝ : Nontrivial R
⊢ (X + C (r + s)).resultant ((taylor r) g) = (X + C s).resultant g
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p ∧ IsCoprime ↑q.1 ↑q.2 }
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) :=
  (UniversalFactorizationRing.homEquiv S m k hn p).symm ⟨↑q, ⋯⟩
a✝ : Nontrivial S
⊢ IsUnit (↑f ((-1) ^ n)) ∧
    IsUnit
      ((map ↑f ↑(UniversalFactorizationRing.factor₁ m k hn p)).resultant
        (map ↑f ↑(UniversalFactorizationRing.factor₂ m k hn p))
        (↑(UniversalFactorizationRing.factor₁ m k hn p)).natDegree
        (↑(UniversalFactorizationRing.factor₂ m k hn p)).natDegree)

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p ∧ IsCoprime ↑q.1 ↑q.2 }
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) :=
  (UniversalFactorizationRing.homEquiv S m k hn p).symm ⟨↑q, ⋯⟩
a✝ : Nontrivial S
⊢ IsUnit (↑f ((-1) ^ n)) ∧
    IsUnit
      ((map ↑f ↑(UniversalFactorizationRing.factor₁ m k hn p)).resultant
        (map ↑f ↑(UniversalFactorizationRing.factor₂ m k hn p))
        (↑(UniversalFactorizationRing.factor₁ m k hn p)).natDegree
        (↑(UniversalFactorizationRing.factor₂ m k hn p)).natDegree)
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p ∧ IsCoprime ↑q.1 ↑q.2 }
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) :=
  (UniversalFactorizationRing.homEquiv S m k hn p).symm ⟨↑q, ⋯⟩
a✝ : Nontrivial S
⊢ IsCoprime (map ↑f ↑(UniversalFactorizationRing.factor₁ m k hn p))
    (map ↑f ↑(UniversalFactorizationRing.factor₂ m k hn p))

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p ∧ IsCoprime ↑q.1 ↑q.2 }
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) :=
  (UniversalFactorizationRing.homEquiv S m k hn p).symm ⟨↑q, ⋯⟩
a✝ : Nontrivial S
⊢ IsCoprime (map ↑f ↑(UniversalFactorizationRing.factor₁ m k hn p))
    (map ↑f ↑(UniversalFactorizationRing.factor₂ m k hn p))
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
g : R[X]
r : R
x y : R[X]
hx : x ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hy : y ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hx' : ((taylor r) x).resultant ((taylor r) g) = x.resultant g
hy' : ((taylor r) y).resultant ((taylor r) g) = y.resultant g
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ ((taylor r) x).resultant ((taylor r) g) * ((taylor r) y).resultant ((taylor r) g) = (x * y).resultant g

Tactic:
]

Goal state after:
case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
g : R[X]
r : R
x y : R[X]
hx : x ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hy : y ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hx' : ((taylor r) x).resultant ((taylor r) g) = x.resultant g
hy' : ((taylor r) y).resultant ((taylor r) g) = y.resultant g
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ ((taylor r) x).resultant ((taylor r) g) * ((taylor r) y).resultant ((taylor r) g) = (x * y).resultant g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case injective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Injective ⇑φ
f : R[X]
IH : ∀ (g : S[X]) (r : S), ((taylor r) (map φ f)).resultant ((taylor r) g) = (map φ f).resultant g
g : R[X]
r : R
this : (map φ ((taylor r) f)).resultant (map φ ((taylor r) g)) = (map φ f).resultant (map φ g)
⊢ φ (((taylor r) f).resultant ((taylor r) g)) = φ (f.resultant g)

Tactic:
]

Goal state after:
case injective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Injective ⇑φ
f : R[X]
IH : ∀ (g : S[X]) (r : S), ((taylor r) (map φ f)).resultant ((taylor r) g) = (map φ f).resultant g
g : R[X]
r : R
this : (map φ ((taylor r) f)).resultant (map φ ((taylor r) g)) = (map φ f).resultant (map φ g)
⊢ φ (((taylor r) f).resultant ((taylor r) g)) = φ (f.resultant g)
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
P : Ideal R
inst✝ : P.IsPrime
f : MonicDegreeEq P.ResidueField m
g : MonicDegreeEq P.ResidueField k
H : map (algebraMap R P.ResidueField) ↑p = ↑f * ↑g
Hpq : IsCoprime ↑f ↑g
φ : 𝓡' →ₐ[R] P.ResidueField := (homEquiv P.ResidueField m k hn p).symm ⟨(f, g), ⋯⟩
Q : Ideal 𝓡' := RingHom.ker φ.toRingHom
this : Q.IsPrime
⊢ P = P

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH : ∀ (q g : R[X]) (r : R), ((taylor r) q).resultant ((taylor r) 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 = φ f'.leadingCoeff
hgl : g.leadingCoeff = φ g'.leadingCoeff
⊢ φ (((taylor r) f').resultant ((taylor r) g') f'.natDegree g'.natDegree) =
    φ (((taylor r) f').resultant ((taylor r) g') f'.natDegree g'.natDegree)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: 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 : p ∈ R[X]_m
q : R[X]
hq : q ∈ R[X]_n
⊢ (f * ↑(⟨p, hp⟩, ⟨q, hq⟩).2 + g * ↑(⟨p, hp⟩, ⟨q, hq⟩).1).degree < ↑(m + n)

Tactic:
]

Goal state after:
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 : p ∈ R[X]_m
q : R[X]
hq : q ∈ R[X]_n
⊢ (f * ↑(⟨p, hp⟩, ⟨q, hq⟩).2 + g * ↑(⟨p, hp⟩, ⟨q, hq⟩).1).degree < ↑(m + n)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
x✝¹ x✝ : ↥R[X]_m × ↥R[X]_n
⊢ ⟨f * ↑(x✝¹ + x✝).2 + g * ↑(x✝¹ + x✝).1, ⋯⟩ = ⟨f * ↑x✝¹.2 + g * ↑x✝¹.1, ⋯⟩ + ⟨f * ↑x✝.2 + g * ↑x✝.1, ⋯⟩

Tactic:
ext1; dsimp; ring

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
x✝¹ : R
x✝ : ↥R[X]_m × ↥R[X]_n
⊢ ⟨f * ↑(x✝¹ • x✝).2 + g * ↑(x✝¹ • x✝).1, ⋯⟩ = (RingHom.id R) x✝¹ • ⟨f * ↑x✝.2 + g * ↑x✝.1, ⋯⟩

Tactic:
by ext1; simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inl
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
⊢ (if ↑j ≤ ↑i then g.coeff (↑i - ↑j) else 0) = if ↑j ≤ ↑i then if ↑i ≤ ↑j + n then g.coeff (↑i - ↑j) else 0 else 0

Tactic:
]

Goal state after:
case inl
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
⊢ (if ↑j ≤ ↑i then g.coeff (↑i - ↑j) else 0) = if ↑j ≤ ↑i then if ↑i ≤ ↑j + n then g.coeff (↑i - ↑j) else 0 else 0