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

Goal state before:
pp: case inr.e_a.e_3.e_f
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
⊢ (↑(aeval (universalFactorizationMapPresentation R n m k hn).val)).comp
      ↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inl)) =
    Algebra.TensorProduct.includeLeftRingHom

pp: case inr.e_a.e_4.e_f
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
⊢ (↑(aeval (universalFactorizationMapPresentation R n m k hn).val)).comp
      ↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inr)) =
    ↑Algebra.TensorProduct.includeRight

pp: case inr.e_a.e_5
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
⊢ m = (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m)).natDegree

pp: case inr.e_a.e_6
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
⊢ k = (Polynomial.map (↑Algebra.TensorProduct.includeRight) (freeMonic R k)).natDegree

Tactic:
·

Goal state after:
case inr.e_a.e_3.e_f
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
⊢ (↑(aeval (universalFactorizationMapPresentation R n m k hn).val)).comp
      ↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inl)) =
    Algebra.TensorProduct.includeLeftRingHom
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.e_a.e_4.e_f
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
⊢ (↑(aeval (universalFactorizationMapPresentation R n m k hn).val)).comp
      ↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inr)) =
    ↑Algebra.TensorProduct.includeRight

pp: case inr.e_a.e_5
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
⊢ m = (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m)).natDegree

pp: case inr.e_a.e_6
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
⊢ k = (Polynomial.map (↑Algebra.TensorProduct.includeRight) (freeMonic R k)).natDegree

Tactic:
·

Goal state after:
case inr.e_a.e_4.e_f
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
⊢ (↑(aeval (universalFactorizationMapPresentation R n m k hn).val)).comp
      ↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inr)) =
    ↑Algebra.TensorProduct.includeRight
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.e_a.e_5
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
⊢ m = (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m)).natDegree

pp: case inr.e_a.e_6
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
⊢ k = (Polynomial.map (↑Algebra.TensorProduct.includeRight) (freeMonic R k)).natDegree

Tactic:
·

Goal state after:
case inr.e_a.e_5
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
⊢ m = (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (freeMonic R m)).natDegree
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.e_a.e_6
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
⊢ k = (Polynomial.map (↑Algebra.TensorProduct.includeRight) (freeMonic R k)).natDegree

Tactic:
·

Goal state after:
case inr.e_a.e_6
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
⊢ k = (Polynomial.map (↑Algebra.TensorProduct.includeRight) (freeMonic R k)).natDegree
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case pos
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf : f.Splits
h : f.natDegree = 0
⊢ f.resultant f = 0 ^ f.natDegree

pp: case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf : f.Splits
h : ¬f.natDegree = 0
⊢ f.resultant f = 0 ^ f.natDegree

Tactic:
·

Goal state after:
case pos
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf : f.Splits
h : f.natDegree = 0
⊢ f.resultant f = 0 ^ f.natDegree
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
this✝ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
this : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
⊢ (universalFactorizationMap R n m k hn).IsIntegral

Tactic:
let := (universalFactorizationMap ℤ n m k hn).toAlgebra

Goal state after:
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
this✝¹ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
this✝ : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (universalFactorizationMap ℤ n m k hn).toAlgebra
⊢ (universalFactorizationMap R n m k hn).IsIntegral
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
inst✝⁴ : QuasiCompact f✝
inst✝³ : QuasiSeparated f✝
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : Smooth g
x : ↥(pullback (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : (pullback.snd (fromNormalization f) g ≫ g) x ∈ ↑U
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : (pullback.snd (fromNormalization f) g) x ∈ ↑V
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (fromNormalization f) g).Opens := pullback.snd (fromNormalization f) g ⁻¹ᵁ V
this : IsIso (pushoutSection ⋯ hVU ⋯ ⋯)
⊢ IsIso ((pushout.congrHom ⋯ ⋯).hom ≫ pushoutSection ⋯ hVU ⋯ ⋯ ≫ app (normalizationPullback f g) W)

Tactic:
have : (g.appLE U V hVU).hom.Smooth := g.smooth_appLE hU hV hVU

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
inst✝⁴ : QuasiCompact f✝
inst✝³ : QuasiSeparated f✝
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : Smooth g
x : ↥(pullback (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : (pullback.snd (fromNormalization f) g ≫ g) x ∈ ↑U
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : (pullback.snd (fromNormalization f) g) x ∈ ↑V
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (fromNormalization f) g).Opens := pullback.snd (fromNormalization f) g ⁻¹ᵁ V
this✝ : IsIso (pushoutSection ⋯ hVU ⋯ ⋯)
this : (CommRingCat.Hom.hom (appLE g U V hVU)).Smooth
⊢ IsIso ((pushout.congrHom ⋯ ⋯).hom ≫ pushoutSection ⋯ hVU ⋯ ⋯ ≫ app (normalizationPullback f g) W)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
g : R[X]
H : IsCoprime 0 g
⊢ ∃ n, resultant 0 g ∣ leadingCoeff 0 ^ n

pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
g : R[X]
H : IsCoprime 0 g
⊢ ∃ n, resultant 0 g ∣ leadingCoeff 0 ^ n
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hf : f ≠ 0
H : IsCoprime f 0
⊢ ∃ n, f.resultant 0 ∣ f.leadingCoeff ^ n

pp: case inr.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n

Tactic:
·

Goal state after:
case inr.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hf : f ≠ 0
H : IsCoprime f 0
⊢ ∃ n, f.resultant 0 ∣ f.leadingCoeff ^ n
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case 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
b : R[X]
e : 0 * f + b * g = 1
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n

pp: case inr.inr.inr
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 b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n

Tactic:
·

Goal state after:
case 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
b : R[X]
e : 0 * f + b * g = 1
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n
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

pp: case inr.inr.inr.inr
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 b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n

Tactic:
·

Goal state after:
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
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr.inr.inr.inr
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 b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.coeff f.natDegree ^ (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n

pp: 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 b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
⊢ a.natDegree + f.natDegree ≤ b.natDegree + g.natDegree

Tactic:
·

Goal state after:
case inr.inr.inr.inr
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 b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.coeff f.natDegree ^ (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: 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 b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
⊢ a.natDegree + f.natDegree ≤ b.natDegree + g.natDegree

Tactic:
·

Goal state after:
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 b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
⊢ a.natDegree + f.natDegree ≤ b.natDegree + g.natDegree
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
g : R[X]
H : IsCoprime 0 g
⊢ resultant 0 g ≠ 0

pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
⊢ f.resultant g ≠ 0

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
g : R[X]
H : IsCoprime 0 g
⊢ resultant 0 g ≠ 0
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
g : R[X]
r : R
⊢ (scaleRoots 0 r).resultant (g.scaleRoots r) (natDegree 0) g.natDegree =
    r ^ (natDegree 0 * g.natDegree) * resultant 0 g

pp: case inr
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
hf : f ≠ 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
g : R[X]
r : R
⊢ (scaleRoots 0 r).resultant (g.scaleRoots r) (natDegree 0) g.natDegree =
    r ^ (natDegree 0 * g.natDegree) * resultant 0 g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝ : CommRing R
f : R[X]
r : R
hf : f ≠ 0
⊢ (f.scaleRoots r).resultant (scaleRoots 0 r) f.natDegree (natDegree 0) =
    r ^ (f.natDegree * natDegree 0) * f.resultant 0

pp: case inr.inr
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
·

Goal state after:
case inr.inl
R : Type u_1
inst✝ : CommRing R
f : R[X]
r : R
hf : f ≠ 0
⊢ (f.scaleRoots r).resultant (scaleRoots 0 r) f.natDegree (natDegree 0) =
    r ^ (f.natDegree * natDegree 0) * f.resultant 0
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

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

pp: case neg
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
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
·

Goal state after:
case pos
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
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

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

pp: case neg
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
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
·

Goal state after:
case pos
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
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg.inl
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf' : f.Splits
g : R[X]
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
⊢ (f.scaleRoots 0).resultant (g.scaleRoots 0) f.natDegree g.natDegree = 0 ^ (f.natDegree * g.natDegree) * f.resultant g

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).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
·

Goal state after:
case neg.inl
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf' : f.Splits
g : R[X]
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
⊢ (f.scaleRoots 0).resultant (g.scaleRoots 0) f.natDegree g.natDegree = 0 ^ (f.natDegree * g.natDegree) * f.resultant g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr.inr.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),
    map φ f ≠ 0 →
      g ≠ 0 →
        ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
          r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
this :
  (map φ (f.scaleRoots r)).resultant (map φ (g.scaleRoots r)) (map φ f).natDegree (map φ g).natDegree =
    φ r ^ ((map φ f).natDegree * (map φ g).natDegree) * (map φ f).resultant (map φ g)
⊢ φ ((f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree) =
    φ (r ^ (f.natDegree * g.natDegree) * f.resultant g)

pp: case inr.inr.injective.h
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),
    map φ f ≠ 0 →
      g ≠ 0 →
        ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
          r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
this :
  (map φ (f.scaleRoots r)).resultant ((map φ g).scaleRoots (φ r)) (map φ f).natDegree (map φ g).natDegree =
    φ r ^ ((map φ f).natDegree * (map φ g).natDegree) * (map φ f).resultant (map φ g)
⊢ φ g.leadingCoeff ≠ 0

pp: case inr.inr.injective.h
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),
    map φ f ≠ 0 →
      g ≠ 0 →
        ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
          r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
this :
  ((map φ f).scaleRoots (φ r)).resultant ((map φ g).scaleRoots (φ r)) (map φ f).natDegree (map φ g).natDegree =
    φ r ^ ((map φ f).natDegree * (map φ g).natDegree) * (map φ f).resultant (map φ g)
⊢ φ f.leadingCoeff ≠ 0

Tactic:
·

Goal state after:
case inr.inr.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),
    map φ f ≠ 0 →
      g ≠ 0 →
        ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
          r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
this :
  (map φ (f.scaleRoots r)).resultant (map φ (g.scaleRoots r)) (map φ f).natDegree (map φ g).natDegree =
    φ r ^ ((map φ f).natDegree * (map φ g).natDegree) * (map φ f).resultant (map φ g)
⊢ φ ((f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree) =
    φ (r ^ (f.natDegree * g.natDegree) * f.resultant g)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr.inr.injective.h
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),
    map φ f ≠ 0 →
      g ≠ 0 →
        ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
          r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
this :
  (map φ (f.scaleRoots r)).resultant ((map φ g).scaleRoots (φ r)) (map φ f).natDegree (map φ g).natDegree =
    φ r ^ ((map φ f).natDegree * (map φ g).natDegree) * (map φ f).resultant (map φ g)
⊢ φ g.leadingCoeff ≠ 0

Tactic:
simpa [map_eq_zero_iff _ hφ]

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

Goal state before:
pp: case inr.inr.injective.h
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),
    map φ f ≠ 0 →
      g ≠ 0 →
        ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
          r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
this :
  ((map φ f).scaleRoots (φ r)).resultant ((map φ g).scaleRoots (φ r)) (map φ f).natDegree (map φ g).natDegree =
    φ r ^ ((map φ f).natDegree * (map φ g).natDegree) * (map φ f).resultant (map φ g)
⊢ φ f.leadingCoeff ≠ 0

Tactic:
simpa [map_eq_zero_iff _ hφ]

Goal state after: