mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case e_6
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
this : Nontrivial (MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))
⊢ ((localizationAway S D.gbar).ofComp D.presLeft.toGenerators).toAlgHom (D.pres.relation (Sum.inl ())) =
    C D.gbar * X () - 1

Tactic:
rw [pres, presLeft, presRight, Presentation.relation_comp_localizationAway_inl]

Goal state after:
case e_6
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
this : Nontrivial (MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))
⊢ ((localizationAway S D.gbar).ofComp
          (Presentation.naive (fun x ↦ if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x)
              ⋯).toGenerators).toAlgHom
      ((rename Sum.inr)
            ((Presentation.naive (fun x ↦ if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x) ⋯).σ
              D.gbar) *
          X (Sum.inl ()) -
        1) =
    C D.gbar * X () - 1

case e_6.h1
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
this : Nontrivial (MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))
⊢ (Presentation.naive (fun x ↦ if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x) ⋯).σ (-1) = -1

case e_6.h0
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
this : Nontrivial (MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))
⊢ (Presentation.naive (fun x ↦ if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x) ⋯).σ 0 = 0
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case e_6.h1
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
this : Nontrivial (MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))
⊢ (Presentation.naive (fun x ↦ if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x) ⋯).σ (-1) = -1

Tactic:
rw [Presentation.naive, Generators.naive_σ]

Goal state after:
case e_6.h1
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
this : Nontrivial (MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))
⊢ (if -1 = 0 then 0 else if -1 = -1 then -1 else Function.surjInv ⋯ (-1)) = -1
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case e_6.h0
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
this : Nontrivial (MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))
⊢ (Presentation.naive (fun x ↦ if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x) ⋯).σ 0 = 0

Tactic:
rw [Presentation.naive, Generators.naive_σ]

Goal state after:
case e_6.h0
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
this : Nontrivial (MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))
⊢ (if 0 = 0 then 0 else if 0 = -1 then -1 else Function.surjInv ⋯ 0) = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.Etale

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ Etale f ↔ Flat f ∧ FormallyUnramified f ∧ LocallyOfFinitePresentation f

Tactic:
rw [etale_iff, flat_iff, formallyUnramified_iff, locallyOfFinitePresentation_iff]
  grind [RingHom.Etale.iff_flat_and_formallyUnramified]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X Y Z' Z : Scheme
i : Z' ⟶ Z
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
n : ℕ
hn : Scheme.Hom.ker i ^ n = 0
⊢ IsDominant i

Tactic:
isDominant_iff,

Goal state after:
X Y Z' Z : Scheme
i : Z' ⟶ Z
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
n : ℕ
hn : Scheme.Hom.ker i ^ n = 0
⊢ DenseRange ⇑i
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: case refine_1
R S : CommRingCat
φ : R ⟶ S
h : (@Surjective ⊓ @Flat) (Spec.map φ)
T : CommRingCat
this : IsAffine (Spec T)
ψ : R ⟶ T
hfst : IsIso (pullback.fst (Spec.map φ) (Spec.map ψ))
R✝ S✝ : CommRingCat
f : R✝ ⟶ S✝
hf : (@Surjective ⊓ @Flat) (Spec.map f)
⊢ (CommRingCat.Hom.hom f).FaithfullyFlat

Tactic:
rwa [← flat_and_surjective_SpecMap_iff, and_comm]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝¹ : P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
inst✝ : IsZariskiLocalAtTarget P
R : CommRingCat
X Y : Scheme
f : X ⟶ Spec R
g : Y ⟶ Spec R
h₃ : LocallyOfFinitePresentation f
h₁ : Surjective f
h₂ : Flat f
H : P (pullback.fst f g)
V : X.Opens
hV : IsCompact V.carrier
e : ⇑f '' ↑V = Set.univ
⊢ P (pullback.fst V.ι (pullback.fst f g))

Tactic:
· exact IsZariskiLocalAtTarget.of_isPullback (.flip <| .of_hasPullback _ _) H

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : FaithfulSMul R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsIntegrallyClosed R
this : IsDomain R
⊢ ∀ {p : Ideal R} [p.IsPrime] (Q : Ideal S) [Q.IsPrime], p < Ideal.under R Q → ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
intro p

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : FaithfulSMul R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
⊢ ∀ [p.IsPrime] (Q : Ideal S) [Q.IsPrime], p < Ideal.under R Q → ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral

Goal state before:
pp: case h.inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
H : IsIntegral R s
h : ∃ t ∈ R⁰, t • s ∈ (algebraMap R S).range
b : R
hb' : b ∈ R⁰
hb : ∀ i < (minpoly R s).natDegree, b • s ^ i ∈ (algebraMap R S).range
n : ℕ
IH : ∀ m < n, b • s ^ m ∈ (algebraMap R S).range
hn : (minpoly R s).natDegree ≤ n
this :
  (minpoly R s).leadingCoeff • s ^ (minpoly R s).natDegree =
    -∑ x ∈ Finset.range (minpoly R s).natDegree, (minpoly R s).coeff x • s ^ x
⊢ b • s ^ n ∈ (algebraMap R S).range

Tactic:
minpoly.monic H,

Goal state after:
case h.inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
H : IsIntegral R s
h : ∃ t ∈ R⁰, t • s ∈ (algebraMap R S).range
b : R
hb' : b ∈ R⁰
hb : ∀ i < (minpoly R s).natDegree, b • s ^ i ∈ (algebraMap R S).range
n : ℕ
IH : ∀ m < n, b • s ^ m ∈ (algebraMap R S).range
hn : (minpoly R s).natDegree ≤ n
this : 1 • s ^ (minpoly R s).natDegree = -∑ x ∈ Finset.range (minpoly R s).natDegree, (minpoly R s).coeff x • s ^ x
⊢ b • s ^ n ∈ (algebraMap R S).range
Module: Mathlib.FieldTheory.RatFunc.Defs

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p : K[X]
⊢ RatFunc.mk p 1 = { toFractionRing := (algebraMap K[X] (FractionRing K[X])) p }

Tactic:
← IsLocalization.mk'_one (M := K[X]⁰) (FractionRing K[X]) p,

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p : K[X]
⊢ RatFunc.mk p 1 = { toFractionRing := IsLocalization.mk' (FractionRing K[X]) p 1 }
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case neg
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0
⊢ Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
      (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)

Tactic:
rw [div_mul_div_comm, eq_div_iff (mul_ne_zero hx hy), div_eq_mul_inv, mul_right_comm, ←
    div_eq_mul_inv, div_eq_iff hxy]

Goal state after:
case neg
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0
⊢ Polynomial.eval₂ f a (x * y).num * (Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom) =
    Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.num * Polynomial.eval₂ f a (x * y).denom
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x : ↥X
hx : x ∈ U.toOpens
f : ↑Γ(X, ↑U)
hfs : f ∈ s
hxf : x ∈ X.basicOpen f
⊢ x ∈ (U.basicOpen (f * 1)).toOpens

Tactic:
simpa using hxf

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
algInst✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
H : (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯)).QuasiFinite
algInst✝ : Algebra ↑(X.presheaf.obj (Opposite.op V)) ↑(X.presheaf.stalk x) :=
  (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).toAlgebra
this : IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hxV⟩)) (hV.primeIdealOf ⟨x, hxV⟩).asIdeal
⊢ (CommRingCat.Hom.hom (appLE f U V hVU)).QuasiFiniteAt (hV.primeIdealOf ⟨x, hxV⟩).asIdeal

Tactic:
let e := IsLocalization.algEquiv (hV.primeIdealOf ⟨x, hxV⟩).asIdeal.primeCompl
    (X.presheaf.stalk (⟨x, hxV⟩ : V.1)) (Localization.AtPrime (hV.primeIdealOf ⟨x, hxV⟩).asIdeal)

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
algInst✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
H : (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯)).QuasiFinite
algInst✝ : Algebra ↑(X.presheaf.obj (Opposite.op V)) ↑(X.presheaf.stalk x) :=
  (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).toAlgebra
this : IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hxV⟩)) (hV.primeIdealOf ⟨x, hxV⟩).asIdeal
e : ↑(X.presheaf.stalk ↑⟨x, hxV⟩) ≃ₐ[↑Γ(X, V)] Localization.AtPrime (hV.primeIdealOf ⟨x, hxV⟩).asIdeal :=
  IsLocalization.algEquiv (hV.primeIdealOf ⟨x, hxV⟩).asIdeal.primeCompl (↑(X.presheaf.stalk ↑⟨x, hxV⟩))
    (Localization.AtPrime (hV.primeIdealOf ⟨x, hxV⟩).asIdeal)
⊢ (CommRingCat.Hom.hom (appLE f U V hVU)).QuasiFiniteAt (hV.primeIdealOf ⟨x, hxV⟩).asIdeal
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
⊢ ∀ {p q a : K[X]},
    q ≠ 0 →
      a ≠ 0 →
        (if a * q = 0 then (0, 1)
          else
            let r := gcd (a * p) (a * q);
            (C (a * q / r).leadingCoeff⁻¹ * (a * p / r), C (a * q / r).leadingCoeff⁻¹ * (a * q / r))) =
          if q = 0 then (0, 1)
          else
            let r := gcd p q;
            (C (q / r).leadingCoeff⁻¹ * (p / r), C (q / r).leadingCoeff⁻¹ * (q / r))

Tactic:
intro p

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
p : K[X]
⊢ ∀ {q a : K[X]},
    q ≠ 0 →
      a ≠ 0 →
        (if a * q = 0 then (0, 1)
          else
            let r := gcd (a * p) (a * q);
            (C (a * q / r).leadingCoeff⁻¹ * (a * p / r), C (a * q / r).leadingCoeff⁻¹ * (a * q / r))) =
          if q = 0 then (0, 1)
          else
            let r := gcd p q;
            (C (q / r).leadingCoeff⁻¹ * (p / r), C (q / r).leadingCoeff⁻¹ * (q / r))
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case f0
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ ∀ (p : K[X]),
    (if 0 = 0 then (0, 1)
      else
        have r := gcd p 0;
        (C (0 / r).leadingCoeff⁻¹ * (p / r), C (0 / r).leadingCoeff⁻¹ * (0 / r))) =
      if 1 = 0 then (0, 1)
      else
        have r := gcd 0 1;
        (C (1 / r).leadingCoeff⁻¹ * (0 / r), C (1 / r).leadingCoeff⁻¹ * (1 / r))

Tactic:
intro p

Goal state after:
case f0
K : Type u
inst✝ : Field K
p✝ q : K[X]
hq : q ≠ 0
p : K[X]
⊢ (if 0 = 0 then (0, 1)
    else
      have r := gcd p 0;
      (C (0 / r).leadingCoeff⁻¹ * (p / r), C (0 / r).leadingCoeff⁻¹ * (0 / r))) =
    if 1 = 0 then (0, 1)
    else
      have r := gcd 0 1;
      (C (1 / r).leadingCoeff⁻¹ * (0 / r), C (1 / r).leadingCoeff⁻¹ * (1 / r))
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: case add
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✝
B : Type u_4
inst✝¹ : CommRing B
inst✝ : Algebra R B
x y : S ⊗[R] ↥(integralClosure R B)
a✝¹ : (Algebra.TensorProduct.map (AlgHom.id S S) (integralClosure R B).val) x ∈ integralClosure S (S ⊗[R] B)
a✝ : (Algebra.TensorProduct.map (AlgHom.id S S) (integralClosure R B).val) y ∈ integralClosure S (S ⊗[R] B)
⊢ (Algebra.TensorProduct.map (AlgHom.id S S) (integralClosure R B).val) (x + y) ∈ integralClosure S (S ⊗[R] B)

Tactic:
map_add

Goal state after:
case add
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✝
B : Type u_4
inst✝¹ : CommRing B
inst✝ : Algebra R B
x y : S ⊗[R] ↥(integralClosure R B)
a✝¹ : (Algebra.TensorProduct.map (AlgHom.id S S) (integralClosure R B).val) x ∈ integralClosure S (S ⊗[R] B)
a✝ : (Algebra.TensorProduct.map (AlgHom.id S S) (integralClosure R B).val) y ∈ integralClosure S (S ⊗[R] B)
⊢ (Algebra.TensorProduct.map (AlgHom.id S S) (integralClosure R B).val) x +
      (Algebra.TensorProduct.map (AlgHom.id S S) (integralClosure R B).val) y ∈
    integralClosure S (S ⊗[R] B)
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
M : Submonoid R
inst✝ : IsLocalization M S
x✝ : ↥(integralClosure R B)
x : B
hx : x ∈ integralClosure R B
⊢ ((algebraMap S (S ⊗[R] B)).comp (algebraMap R S)).IsIntegralElem
    ((Algebra.TensorProduct.includeRight.comp (integralClosure R B).val) ⟨x, hx⟩)

Tactic:
convert!
      RingHom.IsIntegralElem.map hx
        (Algebra.TensorProduct.includeRight : B →ₐ[R] S ⊗[R] B).toRingHom

Goal state after:
case e'_5
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
M : Submonoid R
inst✝ : IsLocalization M S
x✝ : ↥(integralClosure R B)
x : B
hx : x ∈ integralClosure R B
⊢ (algebraMap S (S ⊗[R] B)).comp (algebraMap R S) = Algebra.TensorProduct.includeRight.comp (algebraMap R B)
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
p : Ideal T
inst✝ : p.IsPrime
s : S
hsp : s ∉ Ideal.under S p
hs : IsIntegral R s
Hs : ∀ (x : S), ∃ m, IsIntegral R (s ^ m * x)
t : S
htp : t ∉ Ideal.under S p
Ht : ⊥.saturation (Submonoid.powers ((algebraMap S T) t)) ⋯ = ⊤
m : ℕ
hm : IsIntegral R (s ^ m * t)
x : T
n : ℕ
a : S
ha : (ofId S T).toRingHom a = (fun x ↦ (algebraMap S T) t ^ x) n * x
k : ℕ
hk : IsIntegral R (s ^ k * a)
⊢ (algebraMap S T) (s ^ (m + 1) * t) ^ (k + n) * x =
    (algebraMap S T) (s ^ ((m + 1) * n) * (s ^ m * t) ^ k * (s ^ k * a))

pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
p : Ideal T
inst✝ : p.IsPrime
s : S
hsp : s ∉ Ideal.under S p
hs : IsIntegral R s
Hs : ∀ (x : S), ∃ m, IsIntegral R (s ^ m * x)
t : S
htp : t ∉ Ideal.under S p
Ht : ⊥.saturation (Submonoid.powers ((algebraMap S T) t)) ⋯ = ⊤
m : ℕ
hm : IsIntegral R (s ^ m * t)
x : T
n : ℕ
a : S
ha : (ofId S T).toRingHom a = (fun x ↦ (algebraMap S T) t ^ x) n * x
k : ℕ
hk : IsIntegral R (s ^ k * a)
⊢ IsIntegral R ((algebraMap S T) (s ^ ((m + 1) * n) * (s ^ m * t) ^ k * (s ^ k * a)))

Tactic:
· simp only [AlgHom.toRingHom_eq_coe, Algebra.toRingHom_ofId] at ha
    simp only [map_pow, map_mul, ha, pow_add, mul_pow]
    ring

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
p : Ideal T
inst✝ : p.IsPrime
s : S
hsp : s ∉ Ideal.under S p
hs : IsIntegral R s
Hs : ∀ (x : S), ∃ m, IsIntegral R (s ^ m * x)
t : S
htp : t ∉ Ideal.under S p
Ht : ⊥.saturation (Submonoid.powers ((algebraMap S T) t)) ⋯ = ⊤
m : ℕ
hm : IsIntegral R (s ^ m * t)
x : T
n : ℕ
a : S
ha : (ofId S T).toRingHom a = (fun x ↦ (algebraMap S T) t ^ x) n * x
k : ℕ
hk : IsIntegral R (s ^ k * a)
⊢ IsIntegral R ((algebraMap S T) (s ^ ((m + 1) * n) * (s ^ m * t) ^ k * (s ^ k * a)))
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]
ht : φ.IsIntegralElem t
hp : φ p * t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away ((algebraMap R S) a)
this✝ : Algebra R' S' := (Localization.awayMap (algebraMap R S) a).toAlgebra
this : IsScalarTower R R' S'
ha : IsUnit ((algebraMap R R') a)
H : (aeval ((algebraMap S S') (φ X))).comp (mapRingHom (algebraMap R R')) = (algebraMap S S').comp ↑φ
⊢ (C ↑ha.unit⁻¹ * map (algebraMap R R') p).Monic

Tactic:
nontriviality R'

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]
ht : φ.IsIntegralElem t
hp : φ p * t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away ((algebraMap R S) a)
this✝ : Algebra R' S' := (Localization.awayMap (algebraMap R S) a).toAlgebra
this : IsScalarTower R R' S'
ha : IsUnit ((algebraMap R R') a)
H : (aeval ((algebraMap S S') (φ X))).comp (mapRingHom (algebraMap R R')) = (algebraMap S S').comp ↑φ
a✝ : Nontrivial R'
⊢ (C ↑ha.unit⁻¹ * map (algebraMap R R') p).Monic
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✝⁴ : FaithfulSMul R S
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this : IsDomain R
hf' : Function.Injective ⇑(aeval x)
⊢ False

Tactic:
generalize hf : aeval (R := R) x = f at *

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FaithfulSMul R S
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
x : S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this : IsDomain R
f : R[X] →ₐ[R] S
hf : aeval x = f
hx' : f.Finite
hf' : Function.Injective ⇑f
⊢ False
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✝⁴ : FaithfulSMul R S
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
this✝² : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective ⇑f
hx : IsStronglyTranscendental R (f X)
hf : aeval (f X) = f
this✝¹ : Algebra R[X] S := f.toAlgebra
this✝ : IsScalarTower R R[X] S
this : Module.Finite R[X] S
⊢ ∀ (a : R[X]), (algebraMap R[X] S) a = 0 → a = 0

Tactic:
intro p

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FaithfulSMul R S
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
this✝² : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective ⇑f
hx : IsStronglyTranscendental R (f X)
hf : aeval (f X) = f
this✝¹ : Algebra R[X] S := f.toAlgebra
this✝ : IsScalarTower R R[X] S
this : Module.Finite R[X] S
p : R[X]
⊢ (algebraMap R[X] S) p = 0 → p = 0
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
⊢ Submodule.map (↑↑(taylorEquiv r)) (Submodule.comap (↑↑(taylorEquiv r)) R[X]_n) = R[X]_n

Tactic:
Submodule.map_comap_eq_of_surjective

Goal state after:
R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
⊢ R[X]_n = R[X]_n

case hf
R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
⊢ Function.Surjective ⇑↑↑(taylorEquiv r)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case succ.inl.left
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
j₁ : Fin (m + n)
j₂ : Fin m
IH : ↑(Fin.castAdd n j₂) ≤ m → (M ↑(Fin.castAdd n j₂)).det = M₂.det
hi : ↑(Fin.castAdd n j₂) + 1 ≤ m
⊢ Fin.addCases
        (fun j₁_1 ↦
          if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then g.coeff (↑j₁ - ↑j₁_1) + (f * (monomial k) r).coeff (↑j₁ - ↑j₁_1) else 0)
        (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0) (Fin.castAdd n j₂) -
      r *
        Fin.addCases (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then g.coeff (↑j₁ - ↑j₁_1) else 0)
          (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0)
          ⟨↑(Fin.castAdd n j₂) + (k + m), ⋯⟩ =
    Fin.addCases (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then g.coeff (↑j₁ - ↑j₁_1) else 0)
      (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0) (Fin.castAdd n j₂)

Tactic:
dsimp at hi

Goal state after:
case succ.inl.left
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
j₁ : Fin (m + n)
j₂ : Fin m
IH : ↑(Fin.castAdd n j₂) ≤ m → (M ↑(Fin.castAdd n j₂)).det = M₂.det
hi : ↑j₂ + 1 ≤ m
⊢ Fin.addCases
        (fun j₁_1 ↦
          if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then g.coeff (↑j₁ - ↑j₁_1) + (f * (monomial k) r).coeff (↑j₁ - ↑j₁_1) else 0)
        (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0) (Fin.castAdd n j₂) -
      r *
        Fin.addCases (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then g.coeff (↑j₁ - ↑j₁_1) else 0)
          (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0)
          ⟨↑(Fin.castAdd n j₂) + (k + m), ⋯⟩ =
    Fin.addCases (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + n then g.coeff (↑j₁ - ↑j₁_1) else 0)
      (fun j₁_1 ↦ if ↑j₁_1 ≤ ↑j₁ ∧ ↑j₁ ≤ ↑j₁_1 + m then f.coeff (↑j₁ - ↑j₁_1) else 0) (Fin.castAdd n j₂)