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

Goal state before:
pp: R✝ S✝ : Type u
inst✝⁹ : CommRing R✝
inst✝⁸ : CommRing S✝
inst✝⁷ : Algebra R✝ S✝
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal S
inst✝³ : p.IsPrime
inst✝² : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
H : integralClosure R S = ⊥
J : Ideal S := (conductor R (f X)).radical
hp : J ≤ p
inst✝¹ : (Ideal.map (Ideal.Quotient.mk J) p).IsPrime
inst✝ : IsReduced (S ⧸ J)
inst : WeaklyQuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk J) p)
⊢ aeval (f X) = f

Tactic:
ext

Goal state after:
R✝ S✝ : Type u
inst✝⁹ : CommRing R✝
inst✝⁸ : CommRing S✝
inst✝⁷ : Algebra R✝ S✝
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal S
inst✝³ : p.IsPrime
inst✝² : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
H : integralClosure R S = ⊥
J : Ideal S := ⋯
hp : J ≤ p
inst✝¹ : (Ideal.map (Ideal.Quotient.mk J) p).IsPrime
inst✝ : IsReduced (S ⧸ J)
inst : WeaklyQuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk J) p)
⊢ (aeval (f X)) X = f X
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R✝ S✝ : Type u
inst✝⁹ : CommRing R✝
inst✝⁸ : CommRing S✝
inst✝⁷ : Algebra R✝ S✝
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal S
inst✝³ : p.IsPrime
inst✝² : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
H : integralClosure R S = ⊥
J : Ideal S := (conductor R (f X)).radical
hp : J ≤ p
inst✝¹ : (Ideal.map (Ideal.Quotient.mk J) p).IsPrime
inst✝ : IsReduced (S ⧸ J)
inst : WeaklyQuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk J) p)
⊢ (aeval ((Ideal.Quotient.mk (conductor R (f X)).radical) (f X))).toRingHom = (Ideal.Quotient.mk J).comp f.toRingHom

Tactic:
ext

Goal state after:
case h₁
R✝ S✝ : Type u
inst✝⁹ : CommRing R✝
inst✝⁸ : CommRing S✝
inst✝⁷ : Algebra R✝ S✝
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal S
inst✝³ : p.IsPrime
inst✝² : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
H : integralClosure R S = ⊥
J : Ideal S := (conductor R (f X)).radical
hp : J ≤ p
inst✝¹ : (Ideal.map (Ideal.Quotient.mk J) p).IsPrime
inst✝ : IsReduced (S ⧸ J)
inst : WeaklyQuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk J) p)
x✝ : R
⊢ ((aeval ((Ideal.Quotient.mk (conductor R (f X)).radical) (f X))).comp C) x✝ =
    (((Ideal.Quotient.mk J).comp f.toRingHom).comp C) x✝

case h₂
R✝ S✝ : Type u
inst✝⁹ : CommRing R✝
inst✝⁸ : CommRing S✝
inst✝⁷ : Algebra R✝ S✝
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal S
inst✝³ : p.IsPrime
inst✝² : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
H : integralClosure R S = ⊥
J : Ideal S := ⋯
hp : J ≤ p
inst✝¹ : (Ideal.map (Ideal.Quotient.mk J) p).IsPrime
inst✝ : IsReduced (S ⧸ J)
inst : WeaklyQuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk J) p)
⊢ (aeval ((Ideal.Quotient.mk (conductor R (f X)).radical) (f X))).toRingHom X =
    ((Ideal.Quotient.mk J).comp f.toRingHom) X
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (m + (n + 1))
j : Fin m
⊢ (Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.castAdd (n + 1) j)) = Fin.castAdd (n + 1) j.castSucc

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (m + (n + 1))
j : Fin m
⊢ ↑((Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.castAdd (n + 1) j))) =
    ↑(Fin.castAdd (n + 1) j.castSucc)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (m + (n + 1))
j : Fin (n + 1)
⊢ (Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.natAdd m j)) = Fin.natAdd (m + 1) j

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (m + (n + 1))
j : Fin (n + 1)
⊢ ↑((Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.natAdd m j))) = ↑(Fin.natAdd (m + 1) j)
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₂
U : (X.openCoverOfIsOpenCover (fun k ↦ (TopologicalSpace.Opens.comap (TopCat.Hom.hom f.base)) ↑k) ⋯).I₀
this : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
⊢ (f ⁻¹ᵁ ↑U).toSpecΓ ≫
      Spec.map (CommRingCat.ofHom (integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val.toRingHom) ≫
        (normalizationOpenCover f).f U ≫ normalizationDesc f f₁ f₂ H =
    (X.openCoverOfIsOpenCover (fun k ↦ (TopologicalSpace.Opens.comap (TopCat.Hom.hom f.base)) ↑k) ⋯).f U ≫ f₁

Tactic:
dsimp [normalizationOpenCover, normalizationDesc]

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₂
U : (X.openCoverOfIsOpenCover (fun k ↦ (TopologicalSpace.Opens.comap (TopCat.Hom.hom f.base)) ↑k) ⋯).I₀
this : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
⊢ (f ⁻¹ᵁ ↑U).toSpecΓ ≫
      Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val) ≫
        colimit.ι (normalizationGlueData f).functor U ≫
          colimit.desc (normalizationGlueData f).functor
            { pt := T,
              ι :=
                {
                  app := fun U ↦
                    Spec.map
                        (CommRingCat.ofHom
                          ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ ↑U) (f ⁻¹ᵁ U.toOpens) ⋯)).codRestrict
                            (integralClosure ↑Γ(Y, U.toOpens) ↑Γ(X, f ⁻¹ᵁ U.toOpens)) ⋯)) ≫
                      ⋯.fromSpec,
                  naturality := ⋯ } } =
    Opens.ι ((TopologicalSpace.Opens.comap (TopCat.Hom.hom f.base)) ↑U) ≫ f₁
Module: Mathlib.RingTheory.Ideal.Quotient.Over

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
f : S →ₐ[R] T
Hf : Function.Surjective ⇑f
P : Ideal R
P' : Ideal S
inst✝¹ : P'.IsPrime
inst✝ : P'.LiesOver P
hkP' : ¬RingHom.ker f.toRingHom ≤ P'
H : (P.primesOver S).Finite
⊢ (P.primesOver T).ncard < (P.primesOver S).ncard

Tactic:
rw [← Set.ncard_image_of_injective _ (Ideal.comap_injective_of_surjective _ Hf)]
  refine Set.ncard_lt_ncard (Set.ssubset_iff_exists.mpr ⟨?_, P', ⟨‹_›, ‹_›⟩, ?_⟩) H
  · rintro _ ⟨q, ⟨_, _⟩, rfl⟩
    exact ⟨inferInstance, inferInstanceAs ((q.comap f).LiesOver _)⟩
  · rintro ⟨q, ⟨_, _⟩, rfl⟩; exact hkP' (Ideal.ker_le_comap _)

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
⊢ (universalFactorizationMap S n m k hn).comp (map (algebraMap R S)) =
    (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

Tactic:
ext

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

case hX
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
⊢ ((universalFactorizationMap S n m k hn).comp (map (algebraMap R S))) (X i✝) =
    ((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)
      (X i✝)
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
⊢ Polynomial.map ((↑Algebra.TensorProduct.includeLeft).comp (map (algebraMap R S))) (freeMonic R m) =
    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)

Tactic:
ext

Goal state after:
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✝
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
⊢ Polynomial.map ((↑Algebra.TensorProduct.includeRight).comp (map (algebraMap R S))) (freeMonic R k) =
    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)

Tactic:
ext

Goal state after:
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✝
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
f : { f // f.comp (universalFactorizationMap R n m k hn) = (mapEquivMonic R S n).symm p }
⊢ (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) =
    f

Tactic:
ext

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

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✝)
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 }
⊢ (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) =
    q

Tactic:
ext

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

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✝
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case a
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
⊢ AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) =
    (aeval (Sum.elim (fun x ↦ X x ⊗ₜ[R] 1) fun x ↦ 1 ⊗ₜ[R] X x)).comp ↑(tensorEquivSum R (Fin m) (Fin k) R)

Tactic:
ext

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

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✝)
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
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
⊢ ((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) =
    AlgHom.id R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)

Tactic:
ext

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

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✝)
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.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))) ⋯ =
    𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))

Tactic:
ext

Goal state after:
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 ≫
      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.inl ≫ 𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))

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 ≫
      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.inr ≫ 𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case e_f
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
⊢ (fun x ↦ (aeval ((algebraMap R g.SplittingField) x)) g) = fun x ↦ (algebraMap R g.SplittingField) (eval x g)

Tactic:
ext

Goal state after:
case e_f
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
x✝ : R
⊢ (aeval ((algebraMap R g.SplittingField) x✝)) g = (algebraMap R g.SplittingField) (eval x✝ g)