mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
⊢ CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U)).val =
    CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U)).val ≫ 𝟙 Γ(X, f ⁻¹ᵁ U)

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
q : PrimeSpectrum S
H : QuasiFiniteAt R q.asIdeal
p : PrimeSpectrum R := PrimeSpectrum.comap (algebraMap R S) q
e : ↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p}) ≃ₜ PrimeSpectrum (p.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S p
⊢ IsOpen (⇑e '' {⟨q, ⋯⟩})

Tactic:
Set.image_singleton

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
q : PrimeSpectrum S
H : QuasiFiniteAt R q.asIdeal
p : PrimeSpectrum R := PrimeSpectrum.comap (algebraMap R S) q
e : ↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p}) ≃ₜ PrimeSpectrum (p.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S p
⊢ IsOpen {e ⟨q, ⋯⟩}
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr✝ : ¬g ∣ f
r : K[X] := ⋯
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := ⋯
this :
  (algebraMap K L) (g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    (algebraMap K L) ((f %ₘ g).leadingCoeff ^ g.natDegree) *
      (Multiset.map (fun ij ↦ ij.1 - ij.2) ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)).prod
⊢ (algebraMap K L)
      ((-1) ^ (g.natDegree * (f.natDegree - r.natDegree)) * g.coeff g.natDegree ^ (f.natDegree - r.natDegree) *
        ((-1) ^ (r.natDegree * g.natDegree) * g.resultant (f %ₘ g) g.natDegree r.natDegree)) =
    (algebraMap K L) (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod

Tactic:
rw [map_mul, map_mul, map_mul, this, map_sub_roots_sprod_eq_prod_map_eval _ _ hf hf',
      map_sub_sprod_roots_eq_prod_map_eval _ _ (hr.map _) (SplittingField.splits _), map_mul,
      hg'.roots_map]

Goal state after:
case neg
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr✝ : ¬g ∣ f
r : K[X] := C (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
this :
  (algebraMap K L) (g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    (algebraMap K L) ((f %ₘ g).leadingCoeff ^ g.natDegree) *
      (Multiset.map (fun ij ↦ ij.1 - ij.2) ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)).prod
⊢ (algebraMap K L) ((-1) ^ (g.natDegree * (f.natDegree - r.natDegree))) *
        (algebraMap K L) (g.coeff g.natDegree ^ (f.natDegree - r.natDegree)) *
      ((algebraMap K L) ((-1) ^ (r.natDegree * g.natDegree)) *
        ((algebraMap K L) ((f %ₘ g).leadingCoeff ^ g.natDegree) *
          (Multiset.map (fun x ↦ eval x (map (algebraMap K r.SplittingField) r))
              (Multiset.map (⇑(algebraMap K L)) g.roots)).prod)) =
    (algebraMap K L) ((-1) ^ (g.roots.card * f.roots.card)) *
      (algebraMap K L) (Multiset.map (fun x ↦ eval x f) g.roots).prod
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
this✝¹ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝ : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
⊢ f ⁻¹ᵁ ↑U ≤ f ⁻¹ᵁ ↑U

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
⊢ ↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m) Algebra.TensorProduct.includeLeft) *
      ↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k) Algebra.TensorProduct.includeRight) =
    Polynomial.map (algebraMap (MvPolynomial (Fin m) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))
        (freeMonic R m) *
      Polynomial.map (↑Algebra.TensorProduct.includeRight) (freeMonic R k)

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
this✝² : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝¹ : IsAffineHom f₁
this✝ : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ ↑U ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₁' : f ⁻¹ᵁ ↑U = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₂ : fromNormalization f ⁻¹ᵁ ↑U = f₁ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₂' : fromNormalization f ⁻¹ᵁ ↑U = f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₃ : f ⁻¹ᵁ ↑U = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U
this :
  appLE (toNormalization f) (f₁ ⁻¹ᵁ g ⁻¹ᵁ ↑U) (f ⁻¹ᵁ ↑U) h₁ =
    (normalization f).presheaf.map (eqToHom h₂).op ≫
      app (toNormalization f) (fromNormalization f ⁻¹ᵁ ↑U) ≫ X.presheaf.map (eqToHom h₃).op
⊢ Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val) ≫ (normalizationOpenCover f).f U ≫ f₁ =
    Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val ≫ 𝟙 Γ(X, f ⁻¹ᵁ ↑U)) ≫
      𝟙
          (Spec
            (CommRingCat.of
              ↥(integralClosure ↑Γ(Y, (toOpensFunctor Y).obj ⟨↑U, ⋯⟩) ↑Γ(X, f ⁻¹ᵁ (toOpensFunctor Y).obj ⟨↑U, ⋯⟩)))) ≫
        (normalizationOpenCover f).f ⟨↑U, ⋯⟩ ≫ f₁

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
this✝² : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝¹ : IsAffineHom f₁
this✝ : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ ↑U ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₁' : f ⁻¹ᵁ ↑U = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₂ : fromNormalization f ⁻¹ᵁ ↑U = f₁ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₂' : fromNormalization f ⁻¹ᵁ ↑U = f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₃ : f ⁻¹ᵁ ↑U = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U
this :
  appLE (toNormalization f) (f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U) (f ⁻¹ᵁ ↑U) ⋯ =
    (normalization f).presheaf.map (eqToHom h₂').op ≫
      app (toNormalization f) (fromNormalization f ⁻¹ᵁ ↑U) ≫ X.presheaf.map (eqToHom h₃).op
⊢ Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val ≫ 𝟙 Γ(X, f ⁻¹ᵁ ↑U)) ≫
      𝟙
          (Spec
            (CommRingCat.of
              ↥(integralClosure ↑Γ(Y, (toOpensFunctor Y).obj ⟨↑U, ⋯⟩) ↑Γ(X, f ⁻¹ᵁ (toOpensFunctor Y).obj ⟨↑U, ⋯⟩)))) ≫
        (normalizationOpenCover f).f ⟨↑U, ⋯⟩ ≫ f₂ =
    Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val) ≫ (normalizationOpenCover f).f U ≫ f₂

Tactic:
rfl

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

Goal state before:
pp: case inl.left
R : Type u_1
inst✝ : CommRing R
m k : ℕ
this : Algebra (MvPolynomial (Fin (m + k)) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
i i✝ : Fin m
⊢ (if i✝ < i then 0 else if h : ↑i✝ - ↑i < k then X (Sum.inr ⟨↑i✝ - ↑i, ⋯⟩) else if ↑i✝ - ↑i = k then 1 else 0) =
    if i ≤ i✝ ∧ ↑i✝ ≤ ↑i + k then if h : ↑i✝ - ↑i < k then X (Sum.inr ⟨↑i✝ - ↑i, h⟩) else if ↑i✝ - ↑i = k then 1 else 0
    else 0

Tactic:
grind

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

Goal state before:
pp: case inl.right
R : Type u_1
inst✝ : CommRing R
m k : ℕ
this : Algebra (MvPolynomial (Fin (m + k)) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
i : Fin m
i✝ : Fin k
⊢ (if m + ↑i✝ < ↑i then 0
    else if h : m + ↑i✝ - ↑i < k then X (Sum.inr ⟨m + ↑i✝ - ↑i, ⋯⟩) else if m + ↑i✝ - ↑i = k then 1 else 0) =
    if ↑i ≤ m + ↑i✝ ∧ m + ↑i✝ ≤ ↑i + k then
      if h : m + ↑i✝ - ↑i < k then X (Sum.inr ⟨m + ↑i✝ - ↑i, h⟩) else if m + ↑i✝ - ↑i = k then 1 else 0
    else 0

Tactic:
grind

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

Goal state before:
pp: case inr.left
R : Type u_1
inst✝ : CommRing R
m k : ℕ
this : Algebra (MvPolynomial (Fin (m + k)) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
i : Fin k
i✝ : Fin m
⊢ (if ↑i✝ < ↑i then 0 else if h : ↑i✝ - ↑i < m then X (Sum.inl ⟨↑i✝ - ↑i, ⋯⟩) else if ↑i✝ - ↑i = m then 1 else 0) =
    if ↑i ≤ ↑i✝ ∧ ↑i✝ ≤ ↑i + m then
      if h : ↑i✝ - ↑i < m then X (Sum.inl ⟨↑i✝ - ↑i, h⟩) else if ↑i✝ - ↑i = m then 1 else 0
    else 0

Tactic:
grind

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

Goal state before:
pp: case inr.right
R : Type u_1
inst✝ : CommRing R
m k : ℕ
this : Algebra (MvPolynomial (Fin (m + k)) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R (m + k) m k ⋯).toAlgebra
i i✝ : Fin k
⊢ (if m + ↑i✝ < ↑i then 0
    else if h : m + ↑i✝ - ↑i < m then X (Sum.inl ⟨m + ↑i✝ - ↑i, ⋯⟩) else if m + ↑i✝ - ↑i = m then 1 else 0) =
    if ↑i ≤ m + ↑i✝ ∧ m + ↑i✝ ≤ ↑i + m then
      if h : m + ↑i✝ - ↑i < m then X (Sum.inl ⟨m + ↑i✝ - ↑i, h⟩) else if m + ↑i✝ - ↑i = m then 1 else 0
    else 0

Tactic:
grind

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

Goal state before:
pp: 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 ^ n) m = f.resultant g m ^ n

Tactic:
by
  convert! resultant_prod_right (Finset.range n) f (fun _ ↦ g) m hm (by simpa) <;> simp

Goal state after:
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 }
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
this✝ : Algebra (MvPolynomial (Fin n) R) S := Algebra.compHom S ((MvPolynomial.mapEquivMonic R R n).symm p).toRingHom
this : IsScalarTower (MvPolynomial (Fin n) R) R S
f : { f //
  f.comp (MvPolynomial.universalFactorizationMap R n m k hn) =
    (MvPolynomial.mapEquivMonic R S n).symm (p.map (algebraMap R S)) } :=
  (MvPolynomial.universalFactorizationMapLiftEquiv R S n m k hn (p.map (algebraMap R S))).symm q
r : MvPolynomial (Fin n) R
⊢ (algebraMap R S) (((MvPolynomial.mapEquivMonic R R n).symm p) r) = (algebraMap (MvPolynomial (Fin n) R) S) r

Tactic:
rfl

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

Goal state before:
pp: case refine_1
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)
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
this✝¹ : Algebra (MvPolynomial (Fin n) R) S := Algebra.compHom S ((MvPolynomial.mapEquivMonic R R n).symm p).toRingHom
this✝ : IsScalarTower (MvPolynomial (Fin n) R) R S
this : IsScalarTower R (MvPolynomial (Fin n) R) S
i✝ : Fin m
⊢ f ((fromTensor m k hn p) (MvPolynomial.X i✝ ⊗ₜ[R] 1)) = f (1 ⊗ₜ[MvPolynomial (Fin n) R] (MvPolynomial.X i✝ ⊗ₜ[R] 1))

Tactic:
rfl

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

Goal state before:
pp: case refine_2
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)
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
this✝¹ : Algebra (MvPolynomial (Fin n) R) S := Algebra.compHom S ((MvPolynomial.mapEquivMonic R R n).symm p).toRingHom
this✝ : IsScalarTower (MvPolynomial (Fin n) R) R S
this : IsScalarTower R (MvPolynomial (Fin n) R) S
i✝ : Fin k
⊢ f ((fromTensor m k hn p) (1 ⊗ₜ[R] MvPolynomial.X i✝)) = f (1 ⊗ₜ[MvPolynomial (Fin n) R] (1 ⊗ₜ[R] MvPolynomial.X i✝))

Tactic:
rfl

Goal state after:
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:
rfl

Goal state after:
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)

Tactic:
rfl

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

Goal state before:
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:
rfl

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
T : Type u_4
inst✝¹ : CommRing T
inst✝ : Algebra R T
f : 𝓡' →ₐ[R] S
g : S →ₐ[R] T
⊢ map ↑((g.comp f).comp (IsScalarTower.toAlgHom R 𝓡 𝓡')) ↑(UniversalFactorizationRing.factor₁ m k hn p) =
    map ((↑g).comp ↑(f.comp (IsScalarTower.toAlgHom R 𝓡 𝓡'))) ↑(UniversalFactorizationRing.factor₁ m k hn p)

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
T : Type u_4
inst✝¹ : CommRing T
inst✝ : Algebra R T
f : 𝓡' →ₐ[R] S
g : S →ₐ[R] T
⊢ map ↑((g.comp f).comp (IsScalarTower.toAlgHom R 𝓡 𝓡')) ↑(UniversalFactorizationRing.factor₂ m k hn p) =
    map ((↑g).comp ↑(f.comp (IsScalarTower.toAlgHom R 𝓡 𝓡'))) ↑(UniversalFactorizationRing.factor₂ m k hn p)

Tactic:
rfl

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)

Tactic:
rfl

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

Goal state before:
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

Tactic:
rfl

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

Goal state before:
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:
rfl

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

Goal state before:
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

Tactic:
exact coeff_eq_zero_of_natDegree_lt (by lia)

Goal state after:
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
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField := Ideal.ResidueField.mapₐ P Q (Algebra.ofId R 𝓡') ⋯
e : P.ResidueField ≃ₐ[R] Q.ResidueField := AlgEquiv.ofAlgHom φi φ' ⋯ ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ map ↑((IsScalarTower.toAlgHom R 𝓡' Q.ResidueField).comp (IsScalarTower.toAlgHom R 𝓡 𝓡'))
      ↑(UniversalFactorizationRing.factor₁ m k hn p) =
    map ((algebraMap 𝓡' Q.ResidueField).comp (algebraMap 𝓡 𝓡')) ↑(UniversalFactorizationRing.factor₁ m k hn p)

Tactic:
rfl

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

Tactic:
rfl

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

Goal state before:
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

Tactic:
rfl

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

Goal state before:
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:
rfl

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

Goal state before:
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

Tactic:
exact coeff_eq_zero_of_natDegree_lt (by lia)

Goal state after:
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
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField := Ideal.ResidueField.mapₐ P Q (Algebra.ofId R 𝓡') ⋯
e : P.ResidueField ≃ₐ[R] Q.ResidueField := AlgEquiv.ofAlgHom φi φ' ⋯ ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ map ↑((IsScalarTower.toAlgHom R 𝓡' Q.ResidueField).comp (IsScalarTower.toAlgHom R 𝓡 𝓡'))
      ↑(UniversalFactorizationRing.factor₂ m k hn p) =
    map ((algebraMap 𝓡' Q.ResidueField).comp (algebraMap 𝓡 𝓡')) ↑(UniversalFactorizationRing.factor₂ m k hn p)

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : FiniteType R S
inst✝ : QuasiFiniteAt R q
s₁ : S
hs₁q : s₁ ∉ q
hs₁ : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s₁ ∈ q'
s₂ : ↥(integralClosure R S)
hs₂q : ↑s₂ ∉ q
hs₂ : Function.Bijective ⇑(Localization.awayMap (integralClosure R S).val.toRingHom s₂)
s₃ : ↥(integralClosure R S)
n : ℕ
hs₃ :
  (Localization.awayMap (integralClosure R S).val.toRingHom s₂)
      (IsLocalization.mk' (Localization.Away s₂) s₃ ⟨(fun x ↦ s₂ ^ x) n, ⋯⟩) =
    (algebraMap S (Localization.Away ((integralClosure R S).val.toRingHom s₂))) s₁
m : ℕ
hm : ↑s₂ ^ m * ↑s₃ = ↑s₂ ^ m * (s₁ * ↑s₂ ^ n)
this :
  ∀ (m : ℕ),
    ↑s₂ ^ m * ↑s₃ = ↑s₂ ^ m * (s₁ * ↑s₂ ^ n) →
      0 < m →
        ∃ s ∉ q,
          ∃ (hs : IsIntegral R s),
            (∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q') ∧
              ∀ (q' : Ideal ↥(integralClosure R S)),
                q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q → q'.LiesOver p → ⟨s, hs⟩ ∈ q'
hm0 : ¬0 < m
⊢ ↑s₂ ^ (m + 1) * ↑s₃ = ↑s₂ ^ (m + 1) * (s₁ * ↑s₂ ^ n)

Tactic:
grind

Goal state after: