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

Goal state before:
pp: case h₂
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField := ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
⊢ ((↑((RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField) X)) ⋯).comp { toRingHom := f, commutes' := ⋯ })).comp
        (algebraMap R[X] J.ResidueField))
      X =
    ((↑(AlgHom.id I.ResidueField J.ResidueField)).comp (algebraMap R[X] J.ResidueField)) X

Tactic:
· simp [f, RatFunc.liftAlgHom]

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case _pq
K : Type u
inst✝³ : CommRing K
inst✝² : IsDomain K
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R K[X]
c : R
p q : K[X]
hq : q ≠ 0
⊢ c • RatFunc.mk p q = RatFunc.mk ((algebraMap R K[X]) c) 1 * RatFunc.mk p q

Tactic:
mk_one',

Goal state after:
case _pq
K : Type u
inst✝³ : CommRing K
inst✝² : IsDomain K
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R K[X]
c : R
p q : K[X]
hq : q ≠ 0
⊢ c • RatFunc.mk p q =
    { toFractionRing := (algebraMap K[X] (FractionRing K[X])) ((algebraMap R K[X]) c) } * RatFunc.mk p q
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝⁸ : CommRing K
inst✝⁷ : IsDomain K
L : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : Field L
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommSemiring S
inst✝² : Algebra S K[X]
inst✝¹ : Algebra S L
inst✝ : Algebra S R[X]
φ : K[X] →ₐ[S] L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
r : S
⊢ (liftRingHom ↑φ ⋯) ((algebraMap K[X] K⟮X⟯) ((algebraMap S K[X]) r) / (algebraMap K[X] K⟮X⟯) 1) = (algebraMap S L) r

Tactic:
liftRingHom_apply_div,

Goal state after:
K : Type u
inst✝⁸ : CommRing K
inst✝⁷ : IsDomain K
L : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : Field L
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommSemiring S
inst✝² : Algebra S K[X]
inst✝¹ : Algebra S L
inst✝ : Algebra S R[X]
φ : K[X] →ₐ[S] L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
r : S
⊢ ↑φ ((algebraMap S K[X]) r) / ↑φ 1 = (algebraMap S L) r
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
⊢ C (a * q / (a * (C a.leadingCoeff⁻¹ * gcd p q))).leadingCoeff⁻¹ * (a * p / (a * (C a.leadingCoeff⁻¹ * gcd p q))) =
      C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q) ∧
    C (a * q / (a * (C a.leadingCoeff⁻¹ * gcd p q))).leadingCoeff⁻¹ * (a * q / (a * (C a.leadingCoeff⁻¹ * gcd p q))) =
      C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q)

Tactic:
have hdeg : (gcd p q).degree ≤ q.degree := degree_gcd_le_right _ hq

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
⊢ C (a * q / (a * (C a.leadingCoeff⁻¹ * gcd p q))).leadingCoeff⁻¹ * (a * p / (a * (C a.leadingCoeff⁻¹ * gcd p q))) =
      C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q) ∧
    C (a * q / (a * (C a.leadingCoeff⁻¹ * gcd p q))).leadingCoeff⁻¹ * (a * q / (a * (C a.leadingCoeff⁻¹ * gcd p q))) =
      C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ x⁻¹ = (algebraMap K[X] K⟮X⟯) x.denom / (algebraMap K[X] K⟮X⟯) x.num

Tactic:
← x.num_div_denom

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ ((algebraMap K[X] K⟮X⟯) x.num / (algebraMap K[X] K⟮X⟯) x.denom)⁻¹ =
    (algebraMap K[X] K⟮X⟯) x.denom / (algebraMap K[X] K⟮X⟯) x.num
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
y : B
hy : IsIntegral R y
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
⊢ ∃ g, φ (derivative f) * y = φ g ∧ ∀ (i : ℕ), IsIntegral R (g.coeff i)

Tactic:
algebraize [φ.toRingHom.comp C]

Goal state after:
case inr
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
y : B
hy : IsIntegral R y
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝ : Algebra S B := (φ.comp C).toAlgebra
⊢ ∃ g, φ (derivative f) * y = φ g ∧ ∀ (i : ℕ), IsIntegral R (g.coeff i)
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : Module.Finite R S
inst✝ : IsUnramifiedAt R Q
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
by
  obtain ⟨x, hQ', hQ'Q⟩ :=
    exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective (R := R) Q
  let S' := R[x]
  let Q' := Q.under S'
  let := Localization.AtPrime.algebraOfLiesOver Q' Q
  have : Module.Finite S' S := .of_restrictScalars_finite R _ _
  have : IsUnramifiedAt S' Q := .of_restrictScalars R _
  have hφ : Function.Bijective (Localization.localRingHom Q' Q S'.val rfl) :=
    ⟨Localization.localRingHom_injective_of_primesOver_eq_singleton hQ',
      Localization.localRingHom_surjective_of_primesOver_eq_singleton hQ' hQ'Q.2⟩
  obtain ⟨r, hrQ', H⟩ := Localization.exists_awayMap_bijective_of_residueField_surjective hQ' hQ'Q.2
  have : Module.Finite R S' := finite_adjoin_simple_of_isIntegral (IsIntegral.isIntegral _)
  have : IsUnramifiedAt R Q' := .of_equiv <| .symm <| .ofBijective (IsScalarTower.toAlgHom _ _ _) hφ
  obtain ⟨f, hfQ', hf⟩ :=
    IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn_of_exists_adjoin_singleton_eq_top
    (R := R) (S := S') ⟨⟨x, self_mem_adjoin_singleton _ _⟩, Subalgebra.map_injective
      (f := S'.val) Subtype.val_injective (by simp [Subalgebra.range_val, S'])⟩ Q'
  obtain ⟨P, φ, hP⟩ := hf.of_dvd (g := f * r) (by simp)
  exact ⟨_, (inferInstance : Q'.IsPrime).mul_notMem hfQ' hrQ', .mk
    (f := IsScalarTower.toAlgHom R S' S (f * r))
    ((Localization.awayMapₐ (IsScalarTower.toAlgHom _ _ S) (f * r)).comp φ)
    (by exact (H _ (by simp)).surjective.comp hP)⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
⊢ LinearMap.det ↑(taylorLinearEquiv r n) = ↑1

Tactic:
det_taylorLinearEquiv_toLinearMap,

Goal state after:
R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
⊢ 1 = ↑1
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case h.succ
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
x : S
hx : R[x] = ⊤
H : integralClosure R S = ⊥
H₀ : Function.Surjective ⇑(aeval x)
f : R[X]
hf : (aeval x) f = 0
n : ℕ
hfn : (algebraMap R S) (f.coeff n) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]),
      (aeval x) f = 0 → ∀ (n : ℕ), (algebraMap R S) (f.coeff n) ∉ p → f.natDegree = m_1 → ZariskisMainProperty R p
hm : f.natDegree = m + 1
⊢ ZariskisMainProperty R p

Tactic:
by_cases Hfp : algebraMap _ _ f.leadingCoeff ∈ p

Goal state after:
case pos
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
x : S
hx : R[x] = ⊤
H : integralClosure R S = ⊥
H₀ : Function.Surjective ⇑(aeval x)
f : R[X]
hf : (aeval x) f = 0
n : ℕ
hfn : (algebraMap R S) (f.coeff n) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]),
      (aeval x) f = 0 → ∀ (n : ℕ), (algebraMap R S) (f.coeff n) ∉ p → f.natDegree = m_1 → ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : (algebraMap R S) f.leadingCoeff ∈ p
⊢ ZariskisMainProperty R p

case neg
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
x : S
hx : R[x] = ⊤
H : integralClosure R S = ⊥
H₀ : Function.Surjective ⇑(aeval x)
f : R[X]
hf : (aeval x) f = 0
n : ℕ
hfn : (algebraMap R S) (f.coeff n) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]),
      (aeval x) f = 0 → ∀ (n : ℕ), (algebraMap R S) (f.coeff n) ∉ p → f.natDegree = m_1 → ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : (algebraMap R S) f.leadingCoeff ∉ p
⊢ ZariskisMainProperty R p
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
H : integralClosure R S = ⊥
hf : ¬conductor R (f X) ≤ p
x : S
hx : x ∈ conductor R (f X)
hxp : x ∉ p
a : S
⊢ x * a ∈ f.range

Tactic:
simpa [← AlgHom.map_adjoin_singleton f] using hx a

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case e'_3
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
e : ↑(fromNormalization f ⁻¹ᵁ ↑U) ≅ (normalizationOpenCover f).X U := ⋯
this : (CommRingCat.Hom.hom ((normalizationDiagramMap f).app (Opposite.op ↑U))).IsIntegral
e_1✝ : (normalizationOpenCover f).X U = Spec ((normalizationDiagram f).obj (Opposite.op ↑U))
⊢ (e.inv ≫ fromNormalization f ∣_ ↑U) ≫ (IsAffineOpen.isoSpec ⋯).hom =
    Spec.map ((normalizationDiagramMap f).app (Opposite.op ↑U))

Tactic:
rw [← cancel_mono U.2.fromSpec]

Goal state after:
case e'_3
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
e : ↑(fromNormalization f ⁻¹ᵁ ↑U) ≅ (normalizationOpenCover f).X U :=
  IsOpenImmersion.isoOfRangeEq (fromNormalization f ⁻¹ᵁ ↑U).ι ((normalizationOpenCover f).f U) ⋯
this : (CommRingCat.Hom.hom ((normalizationDiagramMap f).app (Opposite.op ↑U))).IsIntegral
e_1✝ : (normalizationOpenCover f).X U = Spec ((normalizationDiagram f).obj (Opposite.op ↑U))
⊢ ((e.inv ≫ fromNormalization f ∣_ ↑U) ≫ (IsAffineOpen.isoSpec ⋯).hom) ≫ IsAffineOpen.fromSpec ⋯ =
    Spec.map ((normalizationDiagramMap f).app (Opposite.op ↑U)) ≫ IsAffineOpen.fromSpec ⋯
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
g : R[X]
n : ℕ
r : R
hg✝ : g.natDegree ≤ n
a✝ : Nontrivial R
hg : g.natDegree > 0
⊢ (X - C r).resultant (g %ₘ (X - C r)) 1 n = eval r g

pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
n : ℕ
r : R
hg✝ : g.natDegree ≤ n
a✝ : Nontrivial R
hg : g.natDegree > 0
⊢ (g /ₘ (X - C r)).natDegree + 1 ≤ n

Tactic:
modByMonic_X_sub_C_eq_C_eval

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
g : R[X]
n : ℕ
r : R
hg✝ : g.natDegree ≤ n
a✝ : Nontrivial R
hg : g.natDegree > 0
⊢ (X - C r).resultant (C (eval r g)) 1 n = eval r g

R : Type u_1
inst✝ : CommRing R
g : R[X]
n : ℕ
r : R
hg✝ : g.natDegree ≤ n
a✝ : Nontrivial R
hg : g.natDegree > 0
⊢ (g /ₘ (X - C r)).natDegree + 1 ≤ n
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) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (universalFactorizationMap ℤ n m k hn).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId ℤ R)))
    ((AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId ℤ R))) ⋯
i : Fin m
p : (MvPolynomial (Fin n) ℤ)[X]
hp : p.Monic
hp' : Polynomial.eval₂ (universalFactorizationMap ℤ n m k hn).toRingHom (X i ⊗ₜ[ℤ] 1) p = 0
⊢ (universalFactorizationMap R n m k hn).IsIntegralElem (X i ⊗ₜ[R] 1)

Tactic:
refine ⟨p.map (MvPolynomial.map (algebraMap ℤ R)), hp.map _, ?_⟩

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
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId ℤ R)))
    ((AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId ℤ R))) ⋯
i : Fin m
p : (MvPolynomial (Fin n) ℤ)[X]
hp : p.Monic
hp' : Polynomial.eval₂ (universalFactorizationMap ℤ n m k hn).toRingHom (X i ⊗ₜ[ℤ] 1) p = 0
⊢ Polynomial.eval₂ (universalFactorizationMap R n m k hn).toRingHom (X i ⊗ₜ[R] 1)
      (Polynomial.map (map (algebraMap ℤ R)) p) =
    0
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) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (universalFactorizationMap ℤ n m k hn).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId ℤ R)))
    ((AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId ℤ R))) ⋯
H₁ : ∀ (i : Fin m), (universalFactorizationMap R n m k hn).IsIntegralElem (X i ⊗ₜ[R] 1)
i : Fin k
p : (MvPolynomial (Fin n) ℤ)[X]
hp : p.Monic
hp' : Polynomial.eval₂ (universalFactorizationMap ℤ n m k hn).toRingHom (1 ⊗ₜ[ℤ] X i) p = 0
⊢ (universalFactorizationMap R n m k hn).IsIntegralElem (1 ⊗ₜ[R] X i)

Tactic:
refine ⟨p.map (MvPolynomial.map (algebraMap ℤ R)), hp.map _, ?_⟩

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
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId ℤ R)))
    ((AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId ℤ R))) ⋯
H₁ : ∀ (i : Fin m), (universalFactorizationMap R n m k hn).IsIntegralElem (X i ⊗ₜ[R] 1)
i : Fin k
p : (MvPolynomial (Fin n) ℤ)[X]
hp : p.Monic
hp' : Polynomial.eval₂ (universalFactorizationMap ℤ n m k hn).toRingHom (1 ⊗ₜ[ℤ] X i) p = 0
⊢ Polynomial.eval₂ (universalFactorizationMap R n m k hn).toRingHom (1 ⊗ₜ[R] X i)
      (Polynomial.map (map (algebraMap ℤ R)) p) =
    0
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 ∧ IsCoprime ↑q.1 ↑q.2 }
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) :=
  (UniversalFactorizationRing.homEquiv S m k hn p).symm ⟨↑q, ⋯⟩
a✝ : Nontrivial S
⊢ IsUnit
    ((map ↑f ↑(UniversalFactorizationRing.factor₁ m k hn p)).resultant
      (map ↑f ↑(UniversalFactorizationRing.factor₂ m k hn p))
      (map f.toRingHom ↑(UniversalFactorizationRing.factor₁ m k hn p)).natDegree
      (↑(UniversalFactorizationRing.factor₂ m k hn p)).natDegree)

Tactic:
← (UniversalFactorizationRing.factor₂ m k hn p).monic.natDegree_map f.toRingHom,

Goal state after:
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 ∧ IsCoprime ↑q.1 ↑q.2 }
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) :=
  (UniversalFactorizationRing.homEquiv S m k hn p).symm ⟨↑q, ⋯⟩
a✝ : Nontrivial S
⊢ IsUnit
    ((map ↑f ↑(UniversalFactorizationRing.factor₁ m k hn p)).resultant
      (map ↑f ↑(UniversalFactorizationRing.factor₂ m k hn p))
      (map f.toRingHom ↑(UniversalFactorizationRing.factor₁ m k hn p)).natDegree
      (map f.toRingHom ↑(UniversalFactorizationRing.factor₂ m k hn p)).natDegree)
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 𝓡') ⋯
x : Q.ResidueField
⊢ (φ'.comp φi) (φ' x) = (AlgHom.id R P.ResidueField) (φ' x)

Tactic:
congr; ext

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

Goal state before:
pp: R : Type u
S : Type v
T : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra.FiniteType R T
inst✝¹ : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg : Function.Surjective ⇑(awayMapₐ f g)
p : Ideal R
inst✝ : p.IsPrime
hgp : IsUnit (1 ⊗ₜ[R] g)
this✝¹ : IsClosed (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})
r : R
hpr : { asIdeal := p, isPrime := inst✝ } ∈ ↑(PrimeSpectrum.basicOpen r)
hrg : ↑(PrimeSpectrum.basicOpen r) ⊆ (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})ᶜ
this✝ : IsLocalization.Away (f.toRingHom ((algebraMap R S) r)) (Away ((algebraMap R T) r))
h₁ : (awayMap (algebraMap R S) r).IsIntegral
x : T
n m' : ℕ
s : S
hs : (algebraMap R S) r ^ m' = g * s
b : S
m : ℕ
e : f b = f g ^ m * x
this : f (s ^ m * b) = (algebraMap R T) r ^ (m' * m) * x
⊢ (algebraMap R T) r ^ (0 + n) * ((algebraMap R T) r ^ (m' * m) * x) = (algebraMap R T) r ^ (0 + (n + m' * m)) * x

Tactic:
simp [pow_add, mul_assoc]

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

Goal state before:
pp: case inl
K : Type u_2
inst✝ : Field K
g : K[X]
⊢ resultant 0 g = 0 ↔ (0 ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime 0 g

Tactic:
obtain rfl | hg := eq_or_ne g 0; · simp
    simpa [isCoprime_zero_left, isUnit_iff, hg, natDegree_eq_zero] using
      show (∀ x, C x ≠ g) ↔ ∀ x ≠ 0, C x ≠ g by aesop

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
i : ℕ
hi : i < 5
j : ℕ
hj : j < 5
hi' : i ∈ Finset.range 5
⊢ (if i = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ i ∧ i ≤ j + 3 then f.coeff (i - j) else 0
      else if j ≤ i + 2 ∧ i ≤ j - 2 + 2 then f.coeff (i - (j - 2) + 1) * (↑(i - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨i, hi⟩

Tactic:
have hj' : j ∈ Finset.range 5 := Finset.mem_range.mpr hj

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
i : ℕ
hi : i < 5
j : ℕ
hj : j < 5
hi' : i ∈ Finset.range 5
hj' : j ∈ Finset.range 5
⊢ (if i = 4 then if j = 1 then 1 else if j = 4 then 3 else 0
    else
      if j < 2 then if j ≤ i ∧ i ≤ j + 3 then f.coeff (i - j) else 0
      else if j ≤ i + 2 ∧ i ≤ j - 2 + 2 then f.coeff (i - (j - 2) + 1) * (↑(i - (j - 2)) + 1) else 0) =
    Matrix.vecCons (![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩)
      (fun i ↦
        Matrix.vecCons (![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩)
          (fun i ↦
            Matrix.vecCons (![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩)
              (fun i ↦
                Matrix.vecCons (![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩)
                  (fun i ↦ ![0, 1, 0, 0, 3] ⟨j, hj⟩) i)
              i)
          i)
      ⟨i, hi⟩
Module: Mathlib.RingTheory.Finiteness.Descent

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R S
I : Ideal R
hI : (Ideal.map (algebraMap R S) I).FG
f : S ⊗[R] ↥I →ₗ[S] S := ↑(AlgebraTensorModule.rid R S S) ∘ₗ (AlgebraTensorModule.lTensor S S) (Submodule.subtype I)
hf : Function.Injective ⇑f
⊢ Ideal.map (algebraMap R S) I ≤ f.range

Tactic:
rw [Ideal.map_le_iff_le_comap]

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R S
I : Ideal R
hI : (Ideal.map (algebraMap R S) I).FG
f : S ⊗[R] ↥I →ₗ[S] S := ↑(AlgebraTensorModule.rid R S S) ∘ₗ (AlgebraTensorModule.lTensor S S) (Submodule.subtype I)
hf : Function.Injective ⇑f
⊢ I ≤ comap (algebraMap R S) f.range
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: ⊢ @IsClosedImmersion = @IsProper ⊓ MorphismProperty.monomorphisms Scheme

Tactic:
by
  ext
  exact IsClosedImmersion.iff_isProper_and_mono ..

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

Goal state before:
pp: R S T : Type u_1
x✝⁴ : CommRing R
x✝³ : CommRing S
x✝² : CommRing T
x✝¹ : Algebra R S
x✝ : Algebra R T
h : (algebraMap R S).FaithfullyFlat
h' : (algebraMap S (S ⊗[R] T)).Smooth
⊢ (algebraMap R T).Smooth

Tactic:
smooth_algebraMap

Goal state after:
R S T : Type u_1
x✝⁴ : CommRing R
x✝³ : CommRing S
x✝² : CommRing T
x✝¹ : Algebra R S
x✝ : Algebra R T
h : (algebraMap R S).FaithfullyFlat
h' : Algebra.Smooth S (S ⊗[R] T)
⊢ Algebra.Smooth R T
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: case hg₂
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Exact ⇑0 ⇑(↑R h1Cotangentι)

Tactic:
LinearMap.exact_zero_iff_injective

Goal state after:
case hg₂
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Injective ⇑(↑R h1Cotangentι)