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

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
P : StandardEtalePair R
f : R →+* S
⊢ ∃ p₁ p₂ n, derivative (map f P.f) * p₁ + map f P.f * p₂ = map f P.g ^ n

Tactic:
obtain ⟨p₁, p₂, n, e⟩ := P.cond

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
P : StandardEtalePair R
f : R →+* S
p₁ p₂ : R[X]
n : ℕ
e : derivative P.f * p₁ + P.f * p₂ = P.g ^ n
⊢ ∃ p₁ p₂ n, derivative (map f P.f) * p₁ + map f P.f * p₂ = map f P.g ^ n
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsStandardEtale R S
Sₛ : Type u_4
inst✝⁴ : CommRing Sₛ
inst✝³ : Algebra S Sₛ
inst✝² : Algebra R Sₛ
inst✝¹ : IsScalarTower R S Sₛ
s : S
inst✝ : IsLocalization.Away s Sₛ
⊢ IsStandardEtale R Sₛ

Tactic:
by
  have P : StandardEtalePresentation R S := IsStandardEtale.nonempty_standardEtalePresentation.some
  obtain ⟨p, n, hp⟩ := P.exists_mul_aeval_x_g_pow_eq_aeval_x s
  let P' : StandardEtalePair R := ⟨P.f, P.monic_f, p * P.g, have ⟨p₁, p₂, m, e⟩ := P.cond;
    ⟨p₁ * p ^ m, p₂ * p ^ m, m, by linear_combination e * p ^ m⟩⟩
  let S' := Localization.Away (AdjoinRoot.mk P.f P.g)
  let e : S ≃ₐ[R] S' := P.equivRing.trans P.P.equivAwayAdjoinRoot
  have := IsLocalization.Away.mul S' (Localization.Away (algebraMap _ S' (AdjoinRoot.mk P.f p)))
    (AdjoinRoot.mk P.f P.g) (.mk _ p)
  rw [← map_mul] at this
  have H : Submonoid.map e.symm.toRingEquiv.toMonoidHom (.powers
      (algebraMap _ S' (AdjoinRoot.mk P.f p))) = .powers (aeval P.x p) := by
    have : ((e.symm.toAlgHom.comp (IsScalarTower.toAlgHom R _ S')).comp (AdjoinRoot.mkₐ P.f)) =
      aeval P.x := by ext; simp [e, StandardEtalePair.equivAwayAdjoinRoot]
    rw [Submonoid.map_powers]
    exact congr(Submonoid.powers ($this p))
  have : IsLocalization.Away (aeval P.x p) Sₛ :=
    IsLocalization.Away.of_associated (r := s) ⟨(P.hasMap.2.pow n).unit, hp⟩
  let e₁ : P'.Ring ≃ₐ[R]
      Localization.Away (algebraMap _ S' (AdjoinRoot.mk P.f p)) :=
    P'.equivAwayAdjoinRoot.trans ((IsLocalization.algEquiv (.powers (AdjoinRoot.mk P.f (p * P.g)))
      (Localization.Away (AdjoinRoot.mk P.f (p * P.g))) _).restrictScalars R)
  let e₂ : Localization.Away (algebraMap _ S' (AdjoinRoot.mk P.f p)) ≃ₐ[R] Sₛ :=
    { __ := IsLocalization.ringEquivOfRingEquiv _ _ _ H,
      commutes' r := by
        simp [IsScalarTower.algebraMap_apply R S' (Localization.Away _),
          - AlgEquiv.symm_toRingEquiv, IsScalarTower.algebraMap_eq R S Sₛ] }
  exact .of_equiv (e₁.trans e₂)

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

Goal state before:
pp: case refine_3
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}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
a : S'
ham : a ∈ m
⊢ ∀ (i : ℕ), IsIntegral R ((Polynomial.map (algebraMap S S') f).coeff i)

Tactic:
· simp only [coeff_map]
      exact fun _ ↦ (hf' _).algebraMap

Goal state after:
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: case refine_2
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
this✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q'
ht : (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤
p : Ideal R := Ideal.under R Q
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this : Algebra (Localization.AtPrime (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
⊢ Function.Surjective ⇑(IsScalarTower.toAlgHom p.ResidueField (Ideal.under (↥R[t]) Q).ResidueField Q.ResidueField)

Tactic:
rw [← AlgHom.range_eq_top, ← top_le_iff, ← ht]

Goal state after:
case refine_2
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
this✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q'
ht : (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤
p : Ideal R := Ideal.under R Q
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this : Algebra (Localization.AtPrime (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
⊢ (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] ≤
    (IsScalarTower.toAlgHom p.ResidueField (Ideal.under (↥R[t]) Q).ResidueField Q.ResidueField).range
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f g : R[X]
m : ℕ
i j✝ : Fin (0 + m)
j : Fin m
⊢ Fin.addCases (fun j₁ ↦ if ↑i ∈ Icc (↑j₁) (↑j₁ + m) then g.coeff (↑i - ↑j₁) else 0)
      (fun j₁ ↦ if ↑i ∈ Icc (↑j₁) (↑j₁ + 0) then f.coeff (↑i - ↑j₁) else 0) (Fin.natAdd 0 j) =
    Matrix.diagonal (fun x ↦ f.coeff 0) i (Fin.natAdd 0 j)

Tactic:
Fin.addCases_right,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f g : R[X]
m : ℕ
i j✝ : Fin (0 + m)
j : Fin m
⊢ (if ↑i ∈ Icc (↑j) (↑j + 0) then f.coeff (↑i - ↑j) else 0) = Matrix.diagonal (fun x ↦ f.coeff 0) i (Fin.natAdd 0 j)
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)
⊢ WeaklyQuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk J) p)

Tactic:
refine .of_surjectiveOnStalks p _ (Ideal.Quotient.mkₐ R _)
        (RingHom.surjectiveOnStalks_of_surjective Ideal.Quotient.mk_surjective)
        ((Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective p).trans ?_).symm

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 := (conductor R (f X)).radical
hp : J ≤ p
inst✝ : (Ideal.map (Ideal.Quotient.mk J) p).IsPrime
inst : IsReduced (S ⧸ J)
⊢ p ⊔ Ideal.comap (Ideal.Quotient.mk J) ⊥ = p
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.AffineZariskiSite
r : ↑Γ(Y, ↑U)
this✝⁸ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝⁷ : Algebra ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (app f ↑(U.basicOpen r))).toAlgebra
this✝⁶ : Algebra ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U))
  ↥(integralClosure ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this✝⁵ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this✝⁴ : IsLocalization.Away ((algebraMap ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)) r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)
this✝³ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (appLE f (↑U) (f ⁻¹ᵁ Y.basicOpen r) ⋯)).toAlgebra
this✝² : IsScalarTower ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)
this✝¹ : IsScalarTower ↑Γ(Y, ↑U) ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)
this✝ :
  IsScalarTower ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U))
    ↥(integralClosure ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)
this :
  IsScalarTower ↑Γ(Y, ↑U) ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U))
    ↥(integralClosure ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r))
⊢ IsLocalization.Away ((algebraMap ↑Γ(Y, ↑U) ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U))) r)
    ↥(integralClosure ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r))

Tactic:
exact IsLocalization.Away.integralClosure r

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

Goal state before:
pp: case succ.e_a.right
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.addCases (fun j₁ ↦ if ↑j₁ ≤ ↑i ∧ ↑i ≤ ↑j₁ + (n + 1) then g.coeff (↑i - ↑j₁) else 0)
      (fun j₁ ↦ if ↑j₁ ≤ ↑i ∧ ↑i ≤ ↑j₁ + (m + 1) then f.coeff (↑i - ↑j₁) else 0)
      ((Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.natAdd m j))) =
    Fin.addCases (fun j₁ ↦ if ↑j₁ ≤ ↑i ∧ ↑i ≤ ↑j₁ + (n + 1) then g.coeff (↑i - ↑j₁) else 0)
      (fun j₁ ↦ if ↑j₁ ≤ ↑i ∧ ↑i ≤ ↑j₁ + m then f.coeff (↑i - ↑j₁) else 0) (Fin.natAdd m j)

Tactic:
| right j =>

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : IsAffineHom f
⊢ IsAffineHom (toNormalization f)

Tactic:
apply MorphismProperty.of_postcomp (W := @IsAffineHom) (W' := @IsSeparated) _ f.fromNormalization
  · infer_instance
  · rw [Hom.toNormalization_fromNormalization]
    infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ 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))

Tactic:
simp only [← Iso.inv_comp_eq, Category.assoc]
    apply coprod.hom_ext <;> simp

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

Goal state before:
pp: case inr.inr.surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH :
  ∀ (q g : R[X]) (r : R),
    q ≠ 0 →
      g ≠ 0 →
        (q.scaleRoots r).resultant (g.scaleRoots r) q.natDegree g.natDegree =
          r ^ (q.natDegree * g.natDegree) * q.resultant g
g : S[X]
r : S
hf : f ≠ 0
hg : g ≠ 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
obtain ⟨f', hf', ef⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)

Goal state after:
case inr.inr.surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH :
  ∀ (q g : R[X]) (r : R),
    q ≠ 0 →
      g ≠ 0 →
        (q.scaleRoots r).resultant (g.scaleRoots r) q.natDegree g.natDegree =
          r ^ (q.natDegree * g.natDegree) * q.resultant g
g : S[X]
r : S
hf : f ≠ 0
hg : g ≠ 0
f' : R[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]),
    g.natDegree ≠ 0 →
      IsDomain R →
        (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
          g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type (max 0 u_1) := MvPolynomial R ℤ
φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap ℤ R) id
hφ : Function.Surjective ⇑φ
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

Tactic:
obtain ⟨f', hf', ef⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]),
    g.natDegree ≠ 0 →
      IsDomain R →
        (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
          g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type (max 0 u_1) := MvPolynomial R ℤ
φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap ℤ R) id
hφ : Function.Surjective ⇑φ
f' : S[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case injective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Injective ⇑φ
f : R[X]
IH : ∀ (g : S[X]) (r : S), ((taylor r) (map φ f)).resultant ((taylor r) g) = (map φ f).resultant g
g : R[X]
r : R
⊢ ((taylor r) f).resultant ((taylor r) g) = f.resultant g

Tactic:
apply hφ
    have := IH (g.map φ) (φ r)
    rw [← map_taylor, ← map_taylor] at this
    simpa [natDegree_map_eq_of_injective hφ] using this

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

Goal state before:
pp: case surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH : ∀ (q g : R[X]) (r : R), ((taylor r) q).resultant ((taylor r) g) = q.resultant g
g : S[X]
r : S
⊢ ((taylor r) f).resultant ((taylor r) g) = f.resultant g

Tactic:
obtain ⟨f', hf', ef⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)

Goal state after:
case surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH : ∀ (q g : R[X]) (r : R), ((taylor r) q).resultant ((taylor r) g) = q.resultant g
g : S[X]
r : S
f' : R[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
⊢ ((taylor r) f).resultant ((taylor r) g) = f.resultant g
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 : ℕ
this : ∃ n, g ∣ (algebraMap R S) r ^ n
⊢ ∃ a k l, (algebraMap R T) r ^ (l + n) * f a = (algebraMap R T) r ^ (l + k) * x

Tactic:
obtain ⟨m', s, hs⟩ := this

Goal state after:
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
⊢ ∃ a k l, (algebraMap R T) r ^ (l + n) * f a = (algebraMap R T) r ^ (l + k) * x
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsSeparated f
x : ↥X
s : ↥S
h : f x = s
hx : Scheme.Hom.QuasiFiniteAt f x
⊢ ∃ U g,
    Etale g ∧ s ∈ Set.range ⇑g ∧ ∃ V W v, IsCompl V W ∧ IsFinite (V.ι ≫ pullback.snd f g) ∧ (pullback.fst f g) ↑v = x

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := S.isBasis_affineOpens.exists_subset_of_mem_open
    (Set.mem_univ (f x)) isOpen_univ

Goal state after:
X S : Scheme
f : X ⟶ S
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsSeparated f
x : ↥X
s : ↥S
h : f x = s
hx : Scheme.Hom.QuasiFiniteAt f x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : f x ∈ ↑U
⊢ ∃ U g,
    Etale g ∧ s ∈ Set.range ⇑g ∧ ∃ V W v, IsCompl V W ∧ IsFinite (V.ι ≫ pullback.snd f g) ∧ (pullback.fst f g) ↑v = x
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
inst✝⁴ : QuasiCompact f✝
inst✝³ : QuasiSeparated f✝
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : Smooth g
x✝ : ↥(pullback (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : (pullback.snd (fromNormalization f) g ≫ g) x✝ ∈ ↑U
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : (pullback.snd (fromNormalization f) g) x✝ ∈ ↑V
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (fromNormalization f) g).Opens := ⋯
this✝² : IsIso (pushoutSection ⋯ hVU ⋯ ⋯)
this✝¹ : (CommRingCat.Hom.hom (appLE g U V hVU)).Smooth
algInst✝² : Algebra ↑Γ(S, U) ↑Γ(X, f ⁻¹ᵁ U) := ⋯
algInst✝¹ : Algebra ↑Γ(S, U) ↑Γ(Y, V) := ⋯
algInst✝ : Algebra ↑Γ(Y, V) ↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) := ⋯
algebraizeInst✝ : Algebra.Smooth ↑Γ(S, U) ↑Γ(Y, V)
this✝ : IsIso (pushoutSection ⋯ hVU ⋯ ⋯)
e₀ : CommRingCat.of
    (↑(Y.presheaf.1 (Opposite.op V)) ⊗[↑(S.presheaf.1 (Opposite.op U))] ↑(X.presheaf.1 (Opposite.op (f ⁻¹ᵁ U)))) ≅
  Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) := ⋯
e : ↑Γ(Y, V) ⊗[↑Γ(S, U)] ↑Γ(X, f ⁻¹ᵁ U) ≃ₐ[↑Γ(Y, V)] ↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) := ⋯
ψ : ↑Γ(Y, V) ⊗[↑Γ(S, U)] ↥(integralClosure ↑Γ(S, U) ↑Γ(X, f ⁻¹ᵁ U)) →ₐ[↑Γ(Y, V)]
  ↥(integralClosure ↑Γ(Y, V) ↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)) := ⋯
hψ : Function.Bijective ⇑ψ
φ : pushout (app (fromNormalization f) U) (appLE g U V hVU) ⟶
  Γ(normalization (pullback.snd f g), normalizationPullback f g ⁻¹ᵁ W) := ⋯
this : Mono (CommRingCat.ofHom (integralClosure ↑Γ(Y, V) ↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)).val.toRingHom)
H : pullback.snd f g ⁻¹ᵁ V ≤ pullback.fst f g ⁻¹ᵁ f ⁻¹ᵁ U
x : ↑(CommRingCat.of ↥(integralClosure ↑Γ(S, U) ↑Γ(X, f ⁻¹ᵁ U)))
⊢ (ConcreteCategory.hom (CommRingCat.ofHom Algebra.TensorProduct.includeRight.toRingHom ≫ e₀.hom)) ↑x =
    (CommRingCat.Hom.hom
        (CommRingCat.ofHom
          ((integralClosure ↑Γ(Y, V) ↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)).val.comp
            ((↑(RingEquiv.ofBijective (↑ψ) hψ)).comp ↑Algebra.TensorProduct.includeRight))))
      x

Tactic:
· simp [ψ, toIntegralClosure, e]; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this✝ : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
W : TopologicalSpace.Opens ↥X
hW : W ∈ X.affineOpens
hxW : x ∈ ↑W
hWV : W ≤ toNormalization f ⁻¹ᵁ V y
this : IsAffine ↑W
V' : (normalization f).Opens := opensRange (X.homOfLE hWV ≫ toNormalization f ∣_ V y ≫ (V y).ι)
hV' : IsAffineOpen V'
⊢ V' ≤ V y

Tactic:
V',

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this✝ : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
W : TopologicalSpace.Opens ↥X
hW : W ∈ X.affineOpens
hxW : x ∈ ↑W
hWV : W ≤ toNormalization f ⁻¹ᵁ V y
this : IsAffine ↑W
V' : (normalization f).Opens := opensRange (X.homOfLE hWV ≫ toNormalization f ∣_ V y ≫ (V y).ι)
hV' : IsAffineOpen V'
⊢ opensRange (X.homOfLE hWV ≫ toNormalization f ∣_ V y ≫ (V y).ι) ≤ V y
Module: Mathlib.RingTheory.Ideal.CotangentBaseChange

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
I : Ideal S
⊢ Function.Surjective ⇑(tensorCotangentHom R T I)

Tactic:
let a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
I : Ideal S
a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
⊢ Function.Surjective ⇑(tensorCotangentHom R T I)
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y S : Scheme
f : X ⟶ Y
g : Y ⟶ S
s : ↥S
H : (⇑f '' ⇑(f ≫ g) ⁻¹' {s}).Finite
inst✝² : IsProper (f ≫ g)
inst✝¹ : IsSeparated g
inst✝ : LocallyOfFiniteType g
⊢ ∃ U, s ∈ U ∧ IsFinite ((Scheme.Hom.imageι f ≫ g) ∣_ U)

Tactic:
have : IsProper f := .of_comp f g

Goal state after:
X Y S : Scheme
f : X ⟶ Y
g : Y ⟶ S
s : ↥S
H : (⇑f '' ⇑(f ≫ g) ⁻¹' {s}).Finite
inst✝² : IsProper (f ≫ g)
inst✝¹ : IsSeparated g
inst✝ : LocallyOfFiniteType g
this : IsProper f
⊢ ∃ U, s ∈ U ∧ IsFinite ((Scheme.Hom.imageι f ≫ g) ∣_ U)
Module: Mathlib.RingTheory.Ideal.CotangentBaseChange

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
I : Ideal S
inst✝ : Module.Flat R T
⊢ Function.Injective ⇑(tensorCotangentHom R T I)

Tactic:
let a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
I : Ideal S
inst✝ : Module.Flat R T
a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
⊢ Function.Injective ⇑(tensorCotangentHom R T I)