mathlib-initiative/mathlib-tactics huggingface dataset:
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
p : Ideal S
inst✝ : p.IsPrime
H✝ : ZariskisMainProperty R p
S' : Subalgebra R S
hS' : (Subalgebra.toSubmodule S').FG
r : ↥S'
hrp : ↑r ∉ p
H : Function.Bijective ⇑(Localization.awayMap S'.val.toRingHom r)
this✝¹ : Module.Finite R ↥S'
this✝ : QuasiFinite R (Localization.Away r)
this : QuasiFinite R (Localization.Away ↑r)
f : Localization.Away ↑r →ₐ[S] Localization.AtPrime p := IsLocalization.Away.liftAlgHom ↑r ⋯
x s : S
hs : s ∈ p.primeCompl
⊢ (AlgHom.restrictScalars R f).toRingHom ((algebraMap S (Localization.Away ↑r)) x) =
    IsLocalization.mk' (Localization.AtPrime p) x ⟨s, hs⟩ *
      (AlgHom.restrictScalars R f) ((algebraMap S (Localization.Away ↑r)) s)

Tactic:
simp

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₁ : X ⟶ T
f₂ : T ⟶ Y
inst✝ : IsIntegralHom f₂
H : f = f₁ ≫ f₂
⊢ IsIntegralHom (normalizationDesc f f₁ f₂ H)

Tactic:
have : IsIntegralHom (f.normalizationDesc f₁ f₂ H ≫ f₂) := by
    rw [f.normalizationDesc_comp]; infer_instance

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst✝ : IsIntegralHom f₂
H : f = f₁ ≫ f₂
this : IsIntegralHom (normalizationDesc f f₁ f₂ H ≫ f₂)
⊢ IsIntegralHom (normalizationDesc f f₁ f₂ H)
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case refine_1
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₂
⊢ (Spec.map ((normalizationDiagramMap f).app (Opposite.op ↑U)) ≫ IsAffineOpen.fromSpec ⋯) ⁻¹ᵁ ↑U = ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case refine_2
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₂
⊢ (Spec.map ((normalizationDiagramMap f).app (Opposite.op ↑U)) ≫ IsAffineOpen.fromSpec ⋯) ⁻¹ᵁ ↑U = ⊤

Tactic:
simp

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

Goal state before:
pp: case hC
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
x✝ : R
⊢ (((universalFactorizationMap S n m k hn).comp (map (algebraMap R S))).comp C) x✝ =
    (((Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId R S)))
                ((AlgHom.restrictScalars R Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId R S)))
                ⋯).comp
            (universalFactorizationMap R n m k hn).toRingHom).comp
        C)
      x✝

Tactic:
simp

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

Goal state before:
pp: case hX.e_a.e_a
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
i✝ : Fin n
n✝ : ℕ
⊢ (Polynomial.map ((↑Algebra.TensorProduct.includeLeft).comp (map (algebraMap R S))) (freeMonic R m)).coeff n✝ =
    (Polynomial.map
          ((↑(Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId R S)))
                  ((AlgHom.restrictScalars R Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId R S)))
                  ⋯)).comp
            ↑Algebra.TensorProduct.includeLeft)
          (freeMonic R m)).coeff
      n✝

Tactic:
simp

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

Goal state before:
pp: case hX.e_a.e_a
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
i✝ : Fin n
n✝ : ℕ
⊢ (Polynomial.map ((↑Algebra.TensorProduct.includeRight).comp (map (algebraMap R S))) (freeMonic R k)).coeff n✝ =
    (Polynomial.map
          ((↑(Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId R S)))
                  ((AlgHom.restrictScalars R Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId R S)))
                  ⋯)).comp
            ↑Algebra.TensorProduct.includeRight)
          (freeMonic R k)).coeff
      n✝

Tactic:
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 S n
q : { q // ↑q.1 * ↑q.2 = ↑p }
⊢ (Algebra.TensorProduct.lift ((mapEquivMonic R S m).symm (↑q).1) ((mapEquivMonic R S k).symm (↑q).2) ⋯).comp
      (universalFactorizationMap R n m k hn) =
    (mapEquivMonic R S n).symm p

Tactic:
refine (mapEquivMonic R S n).eq_symm_apply.mpr <| Subtype.ext ?_
    simp only [universalFactorizationMap, coe_mapEquivMonic_comp, Equiv.apply_symm_apply,
      Polynomial.map_mul]
    simp [← coe_mapEquivMonic_comp, ← q.2]

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

Goal state before:
pp: case ha
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 S n
f : { f // f.comp (universalFactorizationMap R n m k hn) = (mapEquivMonic R S n).symm p }
i✝ : Fin m
⊢ ((↑((fun q ↦
                ⟨Algebra.TensorProduct.lift ((mapEquivMonic R S m).symm (↑q).1) ((mapEquivMonic R S k).symm (↑q).2) ⋯,
                  ⋯⟩)
              ((fun f ↦
                  ⟨((mapEquivMonic R S m) ((↑f).comp Algebra.TensorProduct.includeLeft),
                      (mapEquivMonic R S k) ((↑f).comp Algebra.TensorProduct.includeRight)),
                    ⋯⟩)
                f))).comp
        Algebra.TensorProduct.includeLeft)
      (X i✝) =
    ((↑f).comp Algebra.TensorProduct.includeLeft) (X i✝)

Tactic:
simp

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

Goal state before:
pp: case hb
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 S n
f : { f // f.comp (universalFactorizationMap R n m k hn) = (mapEquivMonic R S n).symm p }
i✝ : Fin k
⊢ ((AlgHom.restrictScalars R
            ↑((fun q ↦
                  ⟨Algebra.TensorProduct.lift ((mapEquivMonic R S m).symm (↑q).1) ((mapEquivMonic R S k).symm (↑q).2) ⋯,
                    ⋯⟩)
                ((fun f ↦
                    ⟨((mapEquivMonic R S m) ((↑f).comp Algebra.TensorProduct.includeLeft),
                        (mapEquivMonic R S k) ((↑f).comp Algebra.TensorProduct.includeRight)),
                      ⋯⟩)
                  f))).comp
        Algebra.TensorProduct.includeRight)
      (X i✝) =
    ((AlgHom.restrictScalars R ↑f).comp Algebra.TensorProduct.includeRight) (X i✝)

Tactic:
simp

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

Goal state before:
pp: case fst
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 S n
q : { q // ↑q.1 * ↑q.2 = ↑p }
n✝ : ℕ
⊢ (↑(↑((fun f ↦
                  ⟨((mapEquivMonic R S m) ((↑f).comp Algebra.TensorProduct.includeLeft),
                      (mapEquivMonic R S k) ((↑f).comp Algebra.TensorProduct.includeRight)),
                    ⋯⟩)
                ((fun q ↦
                    ⟨Algebra.TensorProduct.lift ((mapEquivMonic R S m).symm (↑q).1) ((mapEquivMonic R S k).symm (↑q).2)
                        ⋯,
                      ⋯⟩)
                  q))).1).coeff
      n✝ =
    (↑(↑q).1).coeff n✝

Tactic:
simp

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

Goal state before:
pp: case snd
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 S n
q : { q // ↑q.1 * ↑q.2 = ↑p }
n✝ : ℕ
⊢ (↑(↑((fun f ↦
                  ⟨((mapEquivMonic R S m) ((↑f).comp Algebra.TensorProduct.includeLeft),
                      (mapEquivMonic R S k) ((↑f).comp Algebra.TensorProduct.includeRight)),
                    ⋯⟩)
                ((fun q ↦
                    ⟨Algebra.TensorProduct.lift ((mapEquivMonic R S m).symm (↑q).1) ((mapEquivMonic R S k).symm (↑q).2)
                        ⋯,
                      ⋯⟩)
                  q))).2).coeff
      n✝ =
    (↑(↑q).2).coeff n✝

Tactic:
simp

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

Goal state before:
pp: case neg.hg
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
⊢ g.natDegree ≤ g.natDegree

Tactic:
simp

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

Goal state before:
pp: case a.ha
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  eval₂Hom (↑(universalFactorizationMap R n m k hn)) (Sum.elim (fun x ↦ X x ⊗ₜ[R] 1) fun x ↦ 1 ⊗ₜ[R] X x)
H : ∀ (i : Fin m ⊕ Fin k), (tensorEquivSum R (Fin m) (Fin k) R) (f (X i)) = X i
i : Fin n
p : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R
i✝ : Fin m
⊢ ((AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)).comp Algebra.TensorProduct.includeLeft) (X i✝) =
    (((aeval (Sum.elim (fun x ↦ X x ⊗ₜ[R] 1) fun x ↦ 1 ⊗ₜ[R] X x)).comp ↑(tensorEquivSum R (Fin m) (Fin k) R)).comp
        Algebra.TensorProduct.includeLeft)
      (X i✝)

Tactic:
simp

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

Goal state before:
pp: case a.hb
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  eval₂Hom (↑(universalFactorizationMap R n m k hn)) (Sum.elim (fun x ↦ X x ⊗ₜ[R] 1) fun x ↦ 1 ⊗ₜ[R] X x)
H : ∀ (i : Fin m ⊕ Fin k), (tensorEquivSum R (Fin m) (Fin k) R) (f (X i)) = X i
i : Fin n
p : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R
i✝ : Fin k
⊢ ((AlgHom.restrictScalars R (AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))).comp
        Algebra.TensorProduct.includeRight)
      (X i✝) =
    ((AlgHom.restrictScalars R
            ((aeval (Sum.elim (fun x ↦ X x ⊗ₜ[R] 1) fun x ↦ 1 ⊗ₜ[R] X x)).comp
              ↑(tensorEquivSum R (Fin m) (Fin k) R))).comp
        Algebra.TensorProduct.includeRight)
      (X i✝)

Tactic:
simp

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
hR : IsField R
hg : natDegree 0 ≤ n
hf : Splits 1
hfm : Monic 1
hf' : natDegree 1 = 0
⊢ resultant 1 0 (natDegree 1) n = (Multiset.map (fun x ↦ eval x 0) (roots 1)).prod

Tactic:
simp

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

Goal state before:
pp: case ha
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
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
s : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R
i✝ : Fin m
⊢ ((((AlgHom.restrictScalars R (aeval (Sum.elim (fun x ↦ X x ⊗ₜ[R] 1) fun x ↦ 1 ⊗ₜ[R] X x))).comp
                (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R)))).comp
            ↑(tensorEquivSum R (Fin m) (Fin k) R)).comp
        Algebra.TensorProduct.includeLeft)
      (X i✝) =
    ((AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)).comp Algebra.TensorProduct.includeLeft) (X i✝)

Tactic:
simp

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

Goal state before:
pp: case hb
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
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
s : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R
i✝ : Fin k
⊢ ((AlgHom.restrictScalars R
            (((AlgHom.restrictScalars R (aeval (Sum.elim (fun x ↦ X x ⊗ₜ[R] 1) fun x ↦ 1 ⊗ₜ[R] X x))).comp
                  (mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R)))).comp
              ↑(tensorEquivSum R (Fin m) (Fin k) R))).comp
        Algebra.TensorProduct.includeRight)
      (X i✝) =
    ((AlgHom.restrictScalars R (AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R))).comp
        Algebra.TensorProduct.includeRight)
      (X i✝)

Tactic:
simp

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
i : Fin m
j : Fin n
h : ↑i ≤ ↑j
⊢ (if h : (↑i, ↑j - ↑i).2 < k then
      if (↑i, ↑j - ↑i).1 < m ∧ (↑i, ↑j - ↑i).1 = ↑i then X (Sum.inr ⟨(↑i, ↑j - ↑i).2, h⟩) else 0
    else if (↑i, ↑j - ↑i).2 = k ∧ (↑i, ↑j - ↑i).1 < m ∧ (↑i, ↑j - ↑i).1 = ↑i then 1 else 0) =
    if h : ↑j - ↑i < k then X (Sum.inr ⟨↑j - ↑i, h⟩) else if ↑j - ↑i = k then 1 else 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
hgm : g.Monic
inst : Field R := hR.toField
L : Type u_1 := g.SplittingField
this :
  (map (algebraMap R L) f).resultant (map (algebraMap R L) g) f.natDegree g.natDegree =
    (Multiset.map (fun ij ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots)).prod
⊢ (map (algebraMap R L) g).natDegree ≤ g.natDegree

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ iU ≫ f = (iU ≫ toNormalization f) ≫ fromNormalization f

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ iV ≫ f = (iV ≫ toNormalization f) ≫ fromNormalization f

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case h₁
X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ coprod.inl ≫ (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv ≫ f =
    coprod.inl ≫
      coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)) ≫
        coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case h₂
X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ coprod.inr ≫ (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv ≫ f =
    coprod.inr ≫
      coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)) ≫
        coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ (coprod.inl ≫
        coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
            (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) ⋯) ≫
          normalizationDesc f
            ((e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).hom ≫
              coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
            (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))) ⋯) ≫
      coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f)) =
    fromNormalization (iU ≫ f)

Tactic:
simp

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
i : Fin k
j : Fin n
h : ↑i ≤ ↑j
⊢ (if (↑j - ↑i, ↑i).2 < k then
      if h : (↑j - ↑i, ↑i).1 < m then if (↑j - ↑i, ↑i).2 = ↑i then X (Sum.inl ⟨(↑j - ↑i, ↑i).1, h⟩) else 0
      else if (↑j - ↑i, ↑i).1 = m ∧ (↑j - ↑i, ↑i).2 = ↑i then 1 else 0
    else 0) =
    if h : ↑j - ↑i < m then X (Sum.inl ⟨↑j - ↑i, h⟩) else if ↑j - ↑i = m then 1 else 0

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ (coprod.inl ≫ 𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))) ≫
      coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f)) =
    fromNormalization (iU ≫ f)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ (coprod.inr ≫
        coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
            (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) ⋯) ≫
          normalizationDesc f
            ((e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).hom ≫
              coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
            (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))) ⋯) ≫
      coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f)) =
    fromNormalization (iV ≫ f)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ (coprod.inr ≫ 𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))) ≫
      coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f)) =
    fromNormalization (iV ≫ f)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ (normalizationDesc f
          ((e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).hom ≫
            coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
          (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))) ⋯ ≫
        coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
          (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) ⋯)) ≫
      fromNormalization f =
    fromNormalization f

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ 𝟙 (normalization f) ≫ fromNormalization f = fromNormalization f

Tactic:
simp

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
f g₁ g₂ : R[X]
m : ℕ
hm : f.natDegree ≤ m
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g₁ g₂ : R[X]) (m : ℕ),
    f.natDegree ≤ m →
      m = f.natDegree → f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m
hgn : ¬m = f.natDegree
⊢ f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m

Tactic:
obtain ⟨c, rfl⟩ := le_iff_exists_add.mp hm
    simp [resultant_add_left_deg, this f g₁ g₂, coeff_mul_degree_add_degree]
    ring_nf

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case h₁
X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ coprod.inl ≫
      (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv ≫
        toNormalization f ≫
          normalizationDesc f
              ((e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).hom ≫
                coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
              (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))) ⋯ ≫
            coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
              (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) ⋯) =
    coprod.inl ≫
      (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv ≫ toNormalization f ≫ 𝟙 (normalization f)

Tactic:
simp

Goal state after: