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

Goal state before:
pp: case inr.e_a.e_3.e_f.hC
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
h✝ : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
x✝ : R
⊢ (((↑(aeval (universalFactorizationMapPresentation R n m k hn).val)).comp
            ↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inl))).comp
        C)
      x✝ =
    (Algebra.TensorProduct.includeLeftRingHom.comp C) x✝

pp: case inr.e_a.e_3.e_f.hX
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
h✝ : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
i✝ : Fin m
⊢ ((↑(aeval (universalFactorizationMapPresentation R n m k hn).val)).comp
        ↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inl)))
      (X i✝) =
    Algebra.TensorProduct.includeLeftRingHom (X i✝)

Tactic:
<;>

Goal state after:
case inr.e_a.e_3.e_f.hC
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
h✝ : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
x✝ : R
⊢ (((↑(aeval (universalFactorizationMapPresentation R n m k hn).val)).comp
            ↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inl))).comp
        C)
      x✝ =
    (Algebra.TensorProduct.includeLeftRingHom.comp C) x✝

case inr.e_a.e_3.e_f.hX
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
h✝ : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
i✝ : Fin m
⊢ ((↑(aeval (universalFactorizationMapPresentation R n m k hn).val)).comp
        ↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inl)))
      (X i✝) =
    Algebra.TensorProduct.includeLeftRingHom (X i✝)
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.e_a.e_4.e_f.hC
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
h✝ : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
x✝ : R
⊢ (((↑(aeval (universalFactorizationMapPresentation R n m k hn).val)).comp
            ↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inr))).comp
        C)
      x✝ =
    ((↑Algebra.TensorProduct.includeRight).comp C) x✝

pp: case inr.e_a.e_4.e_f.hX
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
h✝ : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
i✝ : Fin k
⊢ ((↑(aeval (universalFactorizationMapPresentation R n m k hn).val)).comp
        ↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inr)))
      (X i✝) =
    ↑Algebra.TensorProduct.includeRight (X i✝)

Tactic:
<;>

Goal state after:
case inr.e_a.e_4.e_f.hC
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
h✝ : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
x✝ : R
⊢ (((↑(aeval (universalFactorizationMapPresentation R n m k hn).val)).comp
            ↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inr))).comp
        C)
      x✝ =
    ((↑Algebra.TensorProduct.includeRight).comp C) x✝

case inr.e_a.e_4.e_f.hX
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
h✝ : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
i✝ : Fin k
⊢ ((↑(aeval (universalFactorizationMapPresentation R n m k hn).val)).comp
        ↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inr)))
      (X i✝) =
    ↑Algebra.TensorProduct.includeRight (X i✝)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr.inr.inr.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a : R[X]
ha : a ≠ 0
e : a * f + 0 * g = 1
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n

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

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

Goal state before:
pp: case e'_2.e'_3
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
hf : f.leadingCoeff ^ m ≠ 0
hn : g.natDegree ≤ n
⊢ f ^ m = ∏ i ∈ Finset.range m, f

pp: case e'_3
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
hf : f.leadingCoeff ^ m ≠ 0
hn : g.natDegree ≤ n
⊢ f.resultant g f.natDegree n ^ m = ∏ i ∈ Finset.range m, f.resultant g f.natDegree n

Tactic:
<;>

Goal state after:
case e'_2.e'_3
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
hf : f.leadingCoeff ^ m ≠ 0
hn : g.natDegree ≤ n
⊢ f ^ m = ∏ i ∈ Finset.range m, f

case e'_3
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
hf : f.leadingCoeff ^ m ≠ 0
hn : g.natDegree ≤ n
⊢ f.resultant g f.natDegree n ^ m = ∏ i ∈ Finset.range m, f.resultant g f.natDegree n
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case e'_2.e'_4
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
hm : f.natDegree ≤ m
hg : g.leadingCoeff ^ n ≠ 0
⊢ g ^ n = ∏ i ∈ Finset.range n, g

pp: case e'_3
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
hm : f.natDegree ≤ m
hg : g.leadingCoeff ^ n ≠ 0
⊢ f.resultant g m ^ n = ∏ i ∈ Finset.range n, f.resultant g m

Tactic:
<;>

Goal state after:
case e'_2.e'_4
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
hm : f.natDegree ≤ m
hg : g.leadingCoeff ^ n ≠ 0
⊢ g ^ n = ∏ i ∈ Finset.range n, g

case e'_3
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
hm : f.natDegree ≤ m
hg : g.leadingCoeff ^ n ≠ 0
⊢ f.resultant g m ^ n = ∏ i ∈ Finset.range n, f.resultant g m
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case e'_2.e'_5
R : Type u_1
inst✝ : CommRing R
r : R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
a✝ : Nontrivial R
⊢ m = ((X - C r) ^ m).natDegree

pp: case e'_3
R : Type u_1
inst✝ : CommRing R
r : R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
a✝ : Nontrivial R
⊢ eval r g = (X - C r).resultant g (X - C r).natDegree n

pp: case convert_7
R : Type u_1
inst✝ : CommRing R
r : R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
a✝ : Nontrivial R
⊢ (X - C r).leadingCoeff ^ m ≠ 0

pp: case convert_8
R : Type u_1
inst✝ : CommRing R
r : R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
a✝ : Nontrivial R
⊢ g.natDegree ≤ n

Tactic:
<;>

Goal state after:
case e'_2.e'_5
R : Type u_1
inst✝ : CommRing R
r : R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
a✝ : Nontrivial R
⊢ m = ((X - C r) ^ m).natDegree

case e'_3
R : Type u_1
inst✝ : CommRing R
r : R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
a✝ : Nontrivial R
⊢ eval r g = (X - C r).resultant g (X - C r).natDegree n

case convert_7
R : Type u_1
inst✝ : CommRing R
r : R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
a✝ : Nontrivial R
⊢ (X - C r).leadingCoeff ^ m ≠ 0

case convert_8
R : Type u_1
inst✝ : CommRing R
r : R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
a✝ : Nontrivial R
⊢ g.natDegree ≤ n
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case e'_2.e'_5
R : Type u_1
inst✝ : CommRing R
r : R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
a✝ : Nontrivial R
⊢ m = ((X - C r) ^ m).natDegree

Tactic:
simp [natDegree_pow', hn]

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

Goal state before:
pp: case e'_3
R : Type u_1
inst✝ : CommRing R
r : R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
a✝ : Nontrivial R
⊢ eval r g = (X - C r).resultant g (X - C r).natDegree n

Tactic:
simp [natDegree_pow', hn]

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

Goal state before:
pp: case convert_7
R : Type u_1
inst✝ : CommRing R
r : R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
a✝ : Nontrivial R
⊢ (X - C r).leadingCoeff ^ m ≠ 0

Tactic:
simp [natDegree_pow', hn]

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

Goal state before:
pp: case convert_8
R : Type u_1
inst✝ : CommRing R
r : R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
a✝ : Nontrivial R
⊢ g.natDegree ≤ n

Tactic:
simp [natDegree_pow', hn]

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

Goal state before:
pp: case e'_2.e'_3
R : Type u_1
inst✝ : CommRing R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
⊢ X = X - C 0

pp: case e'_3
R : Type u_1
inst✝ : CommRing R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
⊢ g.coeff 0 = eval 0 g

Tactic:
<;>

Goal state after:
case e'_2.e'_3
R : Type u_1
inst✝ : CommRing R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
⊢ X = X - C 0

case e'_3
R : Type u_1
inst✝ : CommRing R
g : R[X]
m n : ℕ
hn : g.natDegree ≤ n
⊢ g.coeff 0 = eval 0 g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case e'_2.e'_4
R : Type u_1
inst✝ : CommRing R
f : R[X]
m n : ℕ
hm : f.natDegree ≤ m
⊢ X = X - C 0

pp: case e'_3
R : Type u_1
inst✝ : CommRing R
f : R[X]
m n : ℕ
hm : f.natDegree ≤ m
⊢ f.coeff 0 = eval 0 f

Tactic:
<;>

Goal state after:
case e'_2.e'_4
R : Type u_1
inst✝ : CommRing R
f : R[X]
m n : ℕ
hm : f.natDegree ≤ m
⊢ X = X - C 0

case e'_3
R : Type u_1
inst✝ : CommRing R
f : R[X]
m n : ℕ
hm : f.natDegree ≤ m
⊢ f.coeff 0 = eval 0 f
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr
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
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

Tactic:
by_cases hf0 : f = 0

Goal state after:
case pos
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
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

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
⊢ (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: case e'_3
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
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p } :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ↑(↑q).1 = (mapRingHom f.toRingHom) ↑(factor₁ m k hn p)

pp: case e'_4
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
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p } :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ↑(↑q).2 = (mapRingHom f.toRingHom) ↑(factor₂ m k hn p)

Tactic:
<;>

Goal state after:
case e'_3
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
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p } :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ↑(↑q).1 = (mapRingHom f.toRingHom) ↑(factor₁ m k hn p)

case e'_4
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
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p } :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ↑(↑q).2 = (mapRingHom f.toRingHom) ↑(factor₂ m k hn p)
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case e'_3
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
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p } :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

pp: case e'_4
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
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p } :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
<;>

Goal state after:
case e'_3
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
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p } :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

case e'_4
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
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p } :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case zero
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
m k : ℕ
a✝ : Nontrivial S
hn : 0 = m + k
p : MonicDegreeEq R 0
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, ⋯⟩
⊢ IsUnit (↑f ((-1) ^ 0))

pp: case succ
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
m k : ℕ
a✝ : Nontrivial S
n✝ : ℕ
hn : n✝ + 1 = m + k
p : MonicDegreeEq R (n✝ + 1)
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, ⋯⟩
⊢ IsUnit (↑f ((-1) ^ (n✝ + 1)))

Tactic:
<;>

Goal state after:
case zero
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
m k : ℕ
a✝ : Nontrivial S
hn : 0 = m + k
p : MonicDegreeEq R 0
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, ⋯⟩
⊢ IsUnit (↑f ((-1) ^ 0))

case succ
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
m k : ℕ
a✝ : Nontrivial S
n✝ : ℕ
hn : n✝ + 1 = m + k
p : MonicDegreeEq R (n✝ + 1)
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, ⋯⟩
⊢ IsUnit (↑f ((-1) ^ (n✝ + 1)))
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 = Ideal.under R Q

Tactic:
rw [Ideal.under, RingHom.comap_ker, AlgHom.toRingHom_eq_coe,
      φ.comp_algebraMap, Ideal.ker_algebraMap_residueField]

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

Goal state before:
pp: case pos
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
h₁ : ↑j ≤ ↑i
h₂ : ↑i ≤ ↑j + n
⊢ g.coeff (↑i - ↑j) = g.coeff (↑i - ↑j)

pp: case neg
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
h₁ : ↑j ≤ ↑i
h₂ : ¬↑i ≤ ↑j + n
⊢ g.coeff (↑i - ↑j) = 0

pp: case neg
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
h₁ : ¬↑j ≤ ↑i
⊢ 0 = 0

Tactic:
<;>

Goal state after:
case pos
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
h₁ : ↑j ≤ ↑i
h₂ : ↑i ≤ ↑j + n
⊢ g.coeff (↑i - ↑j) = g.coeff (↑i - ↑j)

case neg
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
h₁ : ↑j ≤ ↑i
h₂ : ¬↑i ≤ ↑j + n
⊢ g.coeff (↑i - ↑j) = 0

case neg
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
h₁ : ¬↑j ≤ ↑i
⊢ 0 = 0
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case pos
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 n
h₁ : ↑j ≤ ↑i
h₂ : ↑i ≤ ↑j + m
⊢ f.coeff (↑i - ↑j) = f.coeff (↑i - ↑j)

pp: case neg
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 n
h₁ : ↑j ≤ ↑i
h₂ : ¬↑i ≤ ↑j + m
⊢ f.coeff (↑i - ↑j) = 0

pp: case neg
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 n
h₁ : ¬↑j ≤ ↑i
⊢ 0 = 0

Tactic:
<;>

Goal state after:
case pos
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 n
h₁ : ↑j ≤ ↑i
h₂ : ↑i ≤ ↑j + m
⊢ f.coeff (↑i - ↑j) = f.coeff (↑i - ↑j)

case neg
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 n
h₁ : ↑j ≤ ↑i
h₂ : ¬↑i ≤ ↑j + m
⊢ f.coeff (↑i - ↑j) = 0

case neg
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 n
h₁ : ¬↑j ≤ ↑i
⊢ 0 = 0
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
j : Fin 3
⊢ (Matrix.reindex e e) f.sylvesterDeriv ((fun i ↦ i) ⟨0, ⋯⟩) j =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun i ↦ i) ⟨0, ⋯⟩) j

pp: case «1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
j : Fin 3
⊢ (Matrix.reindex e e) f.sylvesterDeriv ((fun i ↦ i) ⟨1, ⋯⟩) j =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun i ↦ i) ⟨1, ⋯⟩) j

pp: case «2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
j : Fin 3
⊢ (Matrix.reindex e e) f.sylvesterDeriv ((fun i ↦ i) ⟨2, ⋯⟩) j =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun i ↦ i) ⟨2, ⋯⟩) j

Tactic:
<;>

Goal state after:
case «0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
j : Fin 3
⊢ (Matrix.reindex e e) f.sylvesterDeriv ((fun i ↦ i) ⟨0, ⋯⟩) j =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
j : Fin 3
⊢ (Matrix.reindex e e) f.sylvesterDeriv ((fun i ↦ i) ⟨1, ⋯⟩) j =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun i ↦ i) ⟨1, ⋯⟩) j

case «2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 2
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr ⋯
j : Fin 3
⊢ (Matrix.reindex e e) f.sylvesterDeriv ((fun i ↦ i) ⟨2, ⋯⟩) j =
    !![f.coeff 0, f.coeff 1, 0; f.coeff 1, 2 * f.coeff 2, f.coeff 1; 1, 0, 2] ((fun i ↦ i) ⟨2, ⋯⟩) j