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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
⊢ ∀ {f : MvPolynomial PEmpty.{w + 1} S},
    (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).IsIntegralElem f →
      ∀ (n : PEmpty.{w + 1} →₀ ℕ), IsIntegral R (coeff n f)

pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
⊢ ∀ {α : Type w} [Fintype α],
    (∀ {f : MvPolynomial α S},
        (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f →
          ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)) →
      ∀ {f : MvPolynomial (Option α) S},
        (algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)).IsIntegralElem f →
          ∀ (n : Option α →₀ ℕ), IsIntegral R (coeff n f)

Tactic:
· intro f H n
    refine .of_map (g := (isEmptyAlgEquiv _ PEmpty).symm.toRingHom)
      (isEmptyAlgEquiv _ PEmpty).symm.injective
      (.of_comp (f := (isEmptyAlgEquiv _ PEmpty).toRingHom) ?_)
    convert! H
    · ext r m <;> simp [Subsingleton.elim m 0, C, X, monomial, coeff, map]
    · obtain rfl := Subsingleton.elim n 0
      have : constantCoeff = (isEmptyAlgEquiv S PEmpty).toRingHom := by aesop
      simpa [-EmbeddingLike.apply_eq_iff_eq, -isEmptyAlgEquiv_apply] using!
        congr((isEmptyAlgEquiv S PEmpty.{w + 1}).symm ($this f))

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
⊢ ∀ {α : Type w} [Fintype α],
    (∀ {f : MvPolynomial α S},
        (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f →
          ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)) →
      ∀ {f : MvPolynomial (Option α) S},
        (algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)).IsIntegralElem f →
          ∀ (n : Option α →₀ ℕ), IsIntegral R (coeff n f)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case H
R : Type u_3
S : Type u_4
F : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
hf : Function.Injective ⇑φ
y : FractionRing R[X]
y✝ : R[X] × ↥R[X]⁰
h : (map φ hφ) { toFractionRing := Localization.mk y✝.1 y✝.2 } = (map φ hφ) { toFractionRing := y }
⊢ { toFractionRing := Localization.mk y✝.1 y✝.2 } = { toFractionRing := y }

Tactic:
induction y using Localization.induction_on

Goal state after:
case H.H
R : Type u_3
S : Type u_4
F : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
hf : Function.Injective ⇑φ
y✝¹ y✝ : R[X] × ↥R[X]⁰
h :
  (map φ hφ) { toFractionRing := Localization.mk y✝¹.1 y✝¹.2 } =
    (map φ hφ) { toFractionRing := Localization.mk y✝.1 y✝.2 }
⊢ { toFractionRing := Localization.mk y✝¹.1 y✝¹.2 } = { toFractionRing := Localization.mk y✝.1 y✝.2 }
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case H
K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : RingHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
y : FractionRing R[X]
y✝ : R[X] × ↥R[X]⁰
⊢ (↑(map φ hφ)).toFun ({ toFractionRing := Localization.mk y✝.1 y✝.2 } + { toFractionRing := y }) =
    (↑(map φ hφ)).toFun { toFractionRing := Localization.mk y✝.1 y✝.2 } + (↑(map φ hφ)).toFun { toFractionRing := y }

Tactic:
induction y using Localization.induction_on

Goal state after:
case H.H
K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : RingHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
y✝¹ y✝ : R[X] × ↥R[X]⁰
⊢ (↑(map φ hφ)).toFun
      ({ toFractionRing := Localization.mk y✝¹.1 y✝¹.2 } + { toFractionRing := Localization.mk y✝.1 y✝.2 }) =
    (↑(map φ hφ)).toFun { toFractionRing := Localization.mk y✝¹.1 y✝¹.2 } +
      (↑(map φ hφ)).toFun { toFractionRing := Localization.mk y✝.1 y✝.2 }
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case pos
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : Algebra.IsAlgebraic k K
hf : Module.Finite k⟮X⟯ K⟮X⟯
hrank : Module.rank k⟮X⟯ K⟮X⟯ = Module.rank k K
⊢ Module.finrank k⟮X⟯ K⟮X⟯ = Module.finrank k K

Tactic:
rw [← Module.finrank_eq_rank] at hrank

Goal state after:
case pos
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : Algebra.IsAlgebraic k K
hf : Module.Finite k⟮X⟯ K⟮X⟯
hrank : ↑(Module.finrank k⟮X⟯ K⟮X⟯) = Module.rank k K
⊢ Module.finrank k⟮X⟯ K⟮X⟯ = Module.finrank k K
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q) ∣ p

Tactic:
by simpa using num_div_dvd p hq

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case inr.refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : φ p * t = φ r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : t' * (algebraMap S St) t = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[(algebraMap S St) (φ X)]
this✝² : Algebra ↥R₁ ↥R₂ := R₂.algebra
this✝¹ : Algebra (↥R₂) St := R₂.toAlgebra
this✝ : Algebra (↥R₁) St := R₁.toAlgebra
this : IsScalarTower (↥R₁) (↥R₂) St
h✝ : Nontrivial ↥R₁
⊢ eval₂ (algebraMap (↥R₁) St) ((algebraMap S St) (φ X))
      (map (algebraMap R ↥R₁) p - C ⟨t', ⋯⟩ * map (algebraMap R ↥R₁) r) =
    0

Tactic:
· simp [← aeval_def, aeval_algebraMap_apply, aeval_algHom_apply,
        ← hp, ← mul_assoc, ht't, mul_right_comm]

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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : integralClosure R S = ⊥
hφ : φ.Finite
hp : φ p * t ∈ conductor R (φ X)
algInst✝ : Algebra R[X] S := φ.toAlgebra
algebraizeInst✝ : Module.Finite R[X] S
this✝ : IsScalarTower R R[X] S
x : S
this : φ p * t * x ∈ φ.range
q : R[X]
n : ℕ
hn : IsIntegral R (p.leadingCoeff ^ n • (t * x) - φ q)
⊢ ∃ n, p.leadingCoeff ^ n • (t * x) ∈ φ.range

Tactic:
obtain ⟨r, hr : algebraMap _ _ r = _⟩ := hRS.le hn

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : integralClosure R S = ⊥
hφ : φ.Finite
hp : φ p * t ∈ conductor R (φ X)
algInst✝ : Algebra R[X] S := φ.toAlgebra
algebraizeInst✝ : Module.Finite R[X] S
this✝ : IsScalarTower R R[X] S
x : S
this : φ p * t * x ∈ φ.range
q : R[X]
n : ℕ
hn : IsIntegral R (p.leadingCoeff ^ n • (t * x) - φ q)
r : R
hr : (algebraMap R S) r = p.leadingCoeff ^ n • (t * x) - φ q
⊢ ∃ n, p.leadingCoeff ^ n • (t * x) ∈ φ.range
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
x : S
hQ' : (Ideal.under (↥R[x]) Q).primesOver S = {Q}
hQ'Q : Function.Bijective ⇑(algebraMap (Ideal.under (↥R[x]) Q).ResidueField Q.ResidueField)
S' : Subalgebra R S := R[x]
Q' : Ideal ↥S' := Ideal.under (↥S') Q
this✝¹ : Algebra (Localization.AtPrime Q') (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver Q' Q
this✝ : Module.Finite (↥S') S
this : IsUnramifiedAt (↥S') Q
hφ : Function.Bijective ⇑(Localization.localRingHom Q' Q ↑S'.val ⋯)
r : ↥R[x]
hrQ' : r ∉ Ideal.under (↥R[x]) Q
H : ∀ (r' : ↥R[x]), r ∣ r' → Function.Bijective ⇑(Localization.awayMap (algebraMap (↥R[x]) S) r')
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
have : Module.Finite R S' := finite_adjoin_simple_of_isIntegral (IsIntegral.isIntegral _)

Goal state after:
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
x : S
hQ' : (Ideal.under (↥R[x]) Q).primesOver S = {Q}
hQ'Q : Function.Bijective ⇑(algebraMap (Ideal.under (↥R[x]) Q).ResidueField Q.ResidueField)
S' : Subalgebra R S := R[x]
Q' : Ideal ↥S' := Ideal.under (↥S') Q
this✝² : Algebra (Localization.AtPrime Q') (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver Q' Q
this✝¹ : Module.Finite (↥S') S
this✝ : IsUnramifiedAt (↥S') Q
hφ : Function.Bijective ⇑(Localization.localRingHom Q' Q ↑S'.val ⋯)
r : ↥R[x]
hrQ' : r ∉ Ideal.under (↥R[x]) Q
H : ∀ (r' : ↥R[x]), r ∣ r' → Function.Bijective ⇑(Localization.awayMap (algebraMap (↥R[x]) S) r')
this : Module.Finite R ↥S'
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
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
x : S
hQ' : (Ideal.under (↥R[x]) Q).primesOver S = {Q}
hQ'Q : Function.Bijective ⇑(algebraMap (Ideal.under (↥R[x]) Q).ResidueField Q.ResidueField)
S' : Subalgebra R S := R[x]
Q' : Ideal ↥S' := Ideal.under (↥S') Q
this✝³ : Algebra (Localization.AtPrime Q') (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver Q' Q
this✝² : Module.Finite (↥S') S
this✝¹ : IsUnramifiedAt (↥S') Q
hφ : Function.Bijective ⇑(Localization.localRingHom Q' Q ↑S'.val ⋯)
r : ↥R[x]
hrQ' : r ∉ Ideal.under (↥R[x]) Q
H : ∀ (r' : ↥R[x]), r ∣ r' → Function.Bijective ⇑(Localization.awayMap (algebraMap (↥R[x]) S) r')
this✝ : Module.Finite R ↥S'
this : IsUnramifiedAt R Q'
f : ↥S'
hfQ' : f ∉ Q'
hf : HasStandardEtaleSurjectionOn R f
P : StandardEtalePair R
φ : P.Ring →ₐ[R] Localization.Away (f * r)
hP : Function.Surjective ⇑φ
⊢ Function.Surjective ⇑((Localization.awayMapₐ (IsScalarTower.toAlgHom R (↥S') S) (f * r)).comp φ)

Tactic:
exact (H _ (by simp)).surjective.comp hP

Goal state after:
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: 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
inst✝ : Algebra.IsStandardEtale R S
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e : B ⊗[R] S ≃ₐ[B] Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g) := 𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx✝ :
  IsIntegral S
    ((Algebra.TensorProduct.comm R B S)
      (e.symm
        (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
          ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      ((aeval 𝓟.x) 𝓟.g ^ (n + m_1) •
        (Algebra.TensorProduct.comm R B S)
          (e.symm
            (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
              ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hfg : IsIntegral R ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)
heg :
  ∀ (g : R[X]),
    e (1 ⊗ₜ[R] (aeval 𝓟.x) g) =
      (algebraMap (AdjoinRoot 𝓟'.f) (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)))
        ((AdjoinRoot.mk 𝓟'.f) (Polynomial.map (algebraMap R B) g))
k : ℕ
hk : IsIntegral R ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ k * a)
⊢ ∀ (i : ℕ), IsIntegral R (𝓟'.f.coeff i)

Tactic:
simp [𝓟', StandardEtalePresentation.baseChange, isIntegral_algebraMap]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: 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) ⋯
⊢ IsIntegralHom (fromNormalization f ∣_ ↑U)

Tactic:
← MorphismProperty.cancel_left_of_respectsIso @IsIntegralHom e.inv,

Goal state after:
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) ⋯
⊢ IsIntegralHom (e.inv ≫ fromNormalization f ∣_ ↑U)
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) n) (universalFactorizationMap R n m k hn)) =
    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:
simp [universalFactorizationMap]

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

Goal state before:
pp: case a.convert_2.mul_X
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
p : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)
i : Fin m ⊕ Fin k
a✝ :
  p - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) (f p)) ∈
    Ideal.span
      (Set.range fun i ↦
        C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))
⊢ p * X i - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) (f (p * X i))) ∈
    Ideal.span
      (Set.range fun i ↦
        C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))

Tactic:
simp only [map_mul, H, map_X, ← sub_mul]; exact Ideal.mul_mem_right _ _ ‹_›

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

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝¹ : Nontrivial 𝓡
h✝ : Subsingleton (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
⊢ (presentation m k hn p).jacobian = (-1) ^ n * (↑(factor₁ m k hn p)).resultant ↑(factor₂ m k hn p)

pp: case 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)
⊢ (presentation m k hn p).jacobian = (-1) ^ n * (↑(factor₁ m k hn p)).resultant ↑(factor₂ m k hn p)

Tactic:
· dsimp [UniversalFactorizationRing]; exact Subsingleton.elim _ _

Goal state after:
case 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)
⊢ (presentation m k hn p).jacobian = (-1) ^ n * (↑(factor₁ m k hn p)).resultant ↑(factor₂ m k hn p)
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.inr.inl
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✝ : Subsingleton R
⊢ (presentation m k hn p).jacobian = (-1) ^ n * (↑(factor₁ m k hn p)).resultant ↑(factor₂ m k hn p)

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
⊢ (presentation m k hn p).jacobian = (-1) ^ n * (↑(factor₁ m k hn p)).resultant ↑(factor₂ m k hn p)

Tactic:
· dsimp [UniversalFactorizationRing]; exact Subsingleton.elim _ _

Goal state after:
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
⊢ (presentation m k hn p).jacobian = (-1) ^ n * (↑(factor₁ m k hn p)).resultant ↑(factor₂ m k hn p)
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 := ⋯
Q : Ideal 𝓡' := ⋯
this✝ : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField := ⋯
e : P.ResidueField ≃ₐ[R] Q.ResidueField := ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ (↑((homEquiv Q.ResidueField m k hn p) (φi.comp φ))).1 = (factor₁ m k hn p).map (algebraMap 𝓡' Q.ResidueField)

Tactic:
rw [H]

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

Tactic:
rw [H]

Goal state after:
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
⊢ (↑((homEquiv Q.ResidueField m k hn p) (IsScalarTower.toAlgHom R 𝓡' Q.ResidueField))).2 =
    (factor₂ m k hn p).map (algebraMap 𝓡' Q.ResidueField)
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 ∉ 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'

Tactic:
obtain ⟨s₁, hs₁q, hs₁⟩ := Ideal.exists_not_mem_forall_mem_of_ne_of_liesOver (R := R) p q

Goal state after:
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 ∉ 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'
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case a
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left✝¹ : Etale fT
u : ↥T
hu : fT u = f x
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left✝ : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) ↑v = x
hVW' : ↑W = (↑V)ᶜ
this✝ : IsClosedImmersion V.ι
this : IsClosedImmersion W.ι
H : IsColimit (BinaryCofan.mk V.ι W.ι)
e : normalization (pullback.snd f fT) ≅ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) :=
  (normalizationCoprodIso (pullback.snd f fT) H).symm ≪≫
    coprod.mapIso (asIso (toNormalization (V.ι ≫ pullback.snd f fT))).symm
      (Iso.refl (normalization (W.ι ≫ pullback.snd f fT)))
ι : ↑V ⟶ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) := coprod.inl
b : ↥↑V
a : ↥W
hab : ι b = e.hom ((toNormalization (pullback.snd f fT)) ↑a)
h : ↑a ∉ V
⊢ False

Tactic:
replace hab : ι b = ((W.ι ≫ pullback.snd f fT).toNormalization ≫ coprod.inr) a := by
          have : W.ι ≫ (H.coconePointUniqueUpToIso (colimit.isColimit _)).hom = coprod.inr :=
            H.comp_coconePointUniqueUpToIso_hom _ ⟨.right⟩
          simp only [← W.ι_apply, ← Scheme.Hom.comp_apply, Category.assoc, e] at hab
          simpa [-Scheme.Hom.comp_base, Scheme.Hom.normalizationCoprodIso,
            reassoc_of% this] using hab

Goal state after:
case a
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left✝¹ : Etale fT
u : ↥T
hu : fT u = f x
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left✝ : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) ↑v = x
hVW' : ↑W = (↑V)ᶜ
this✝ : IsClosedImmersion V.ι
this : IsClosedImmersion W.ι
H : IsColimit (BinaryCofan.mk V.ι W.ι)
e : normalization (pullback.snd f fT) ≅ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) :=
  (normalizationCoprodIso (pullback.snd f fT) H).symm ≪≫
    coprod.mapIso (asIso (toNormalization (V.ι ≫ pullback.snd f fT))).symm
      (Iso.refl (normalization (W.ι ≫ pullback.snd f fT)))
ι : ↑V ⟶ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) := coprod.inl
b : ↥↑V
a : ↥W
h : ↑a ∉ V
hab : ι b = (toNormalization (W.ι ≫ pullback.snd f fT) ≫ coprod.inr) a
⊢ False
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X✝ Y✝ S✝ : Scheme
f✝ : X✝ ⟶ S✝
inst✝³ : LocallyOfFiniteType f✝
X Y S : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
⊢ IsOpenImmersion ((Scheme.Hom.quasiFiniteLocus f).ι ≫ Scheme.Hom.toNormalization f)

Tactic:
by
  obtain ⟨U, hU, e⟩ := Scheme.Hom.exists_isIso_morphismRestrict_toNormalization f
  convert!
    (inferInstance :
      IsOpenImmersion
        ((X.isoOfEq (U := f.quasiFiniteLocus) (SetLike.coe_injective e.symm)).hom ≫
          f.toNormalization ∣_ U ≫ U.ι)) using 1
  simp

Goal state after: