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

Goal state before:
pp: n : ℕ
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsStandardSmoothOfRelativeDimension n R S
this✝¹ : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w✝¹ : _root_.Finite σ
w✝ : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e✝ : P.dimension = n
e₀ : σ ⊕ Fin n ≃ ι :=
  ((Equiv.ofInjective P.map ⋯).sumCongr (Finite.equivFinOfCardEq ⋯).symm).trans (Equiv.Set.sumCompl (Set.range P.map))
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
  (MvPolynomial.sumAlgEquiv R σ (Fin n)).symm.trans (MvPolynomial.renameEquiv R e₀)
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
  (↑e).comp (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)))
algInst✝¹ : Algebra (MvPolynomial (Fin n) R) P.Ring := φ.toAlgebra
algInst✝ : Algebra (MvPolynomial (Fin n) R) S := ((algebraMap P.Ring S).comp φ.toRingHom).toAlgebra
scalarTowerInst✝ : IsScalarTower (MvPolynomial (Fin n) R) P.Ring S :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap (MvPolynomial (Fin n) R) S))
this✝ : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
H :
  (MvPolynomial.aeval fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))).toRingHom =
    (algebraMap P.Ring S).comp e.toRingEquiv.toRingHom
⊢ ⇑(MvPolynomial.aeval fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))) = ⇑(algebraMap P.Ring S) ∘ ⇑e

Tactic:
exact congr($H)

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case inr
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
r : σ
⊢ D.basis (Sum.inr r) = Extension.Cotangent.mk ⟨D.pres.relation (Sum.inr r), ⋯⟩

Tactic:
basis_inr,

Goal state after:
case inr
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
r : σ
⊢ D.cotangentEquivProd.symm (0, D.basisLeft r) = Extension.Cotangent.mk ⟨D.pres.relation (Sum.inr r), ⋯⟩
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ W.negAddY P Q / W.addZ P Q =
    W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))

Tactic:
rw [negAddY_eq hP hQ hPz hQz, addZ_eq hP hQ hPz hQz, toAffine_slope_of_ne hPz hQz hx,
    toAffine_negAddY_of_ne hPz hQz <| sub_ne_zero.mpr hx]

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

Goal state before:
pp: W P Q : MorphismProperty Scheme
X Y : Scheme
inst✝⁴ : W.IsStableUnderBaseChange
inst✝³ : Scheme.IsJointlySurjectivePreserving W
inst✝² : W.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.IsStableUnderComposition
⊢ (sourceLocalClosure W P).IsStableUnderComposition

Tactic:
by
  refine ⟨fun {X Y Z} f g ⟨𝒰, hf⟩ ⟨𝒱, hg⟩ ↦ ?_⟩
  refine ⟨𝒰.bind fun i ↦ (𝒱.pullback₁ (𝒰.f i ≫ f)), fun ⟨l, r⟩ ↦ ?_⟩
  simpa [← pullbackRightPullbackFstIso_inv_snd_fst_assoc, pullback.condition_assoc] using
    P.comp_mem _ _ (P.pullback_snd _ _ (hf _)) (hg r)

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
inst✝ : ExpChar k p
s : Set ι
n : ι
ha : IsTranscendenceBasis k fun i ↦ a ↑i
hn : n ∉ s
e₁ : { j // j ≠ ⟨n, ⋯⟩ } ≃ ↑s :=
  { toFun := fun x ↦ ⟨↑↑x, ⋯⟩, invFun := fun x ↦ ⟨⟨↑x, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
⊢ ∃ i, (IsTranscendenceBasis k fun j ↦ a ↑j) ∧ IsSeparable (↥(adjoin k (a '' (insert n s \ {i})))) (a i)

Tactic:
obtain ⟨i, hi, hi'⟩ := exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow p hp H
    (a := fun i : ↥(insert n s) ↦ a i) ⟨n, by simp⟩ (ha.comp_equiv e₁)

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
inst✝ : ExpChar k p
s : Set ι
n : ι
ha : IsTranscendenceBasis k fun i ↦ a ↑i
hn : n ∉ s
e₁ : { j // j ≠ ⟨n, ⋯⟩ } ≃ ↑s :=
  { toFun := fun x ↦ ⟨↑↑x, ⋯⟩, invFun := fun x ↦ ⟨⟨↑x, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
i : ↑(insert n s)
hi : IsTranscendenceBasis k fun j ↦ a ↑↑j
hi' : IsSeparable (↥(adjoin k ((fun i ↦ a ↑i) '' {i}ᶜ))) (a ↑i)
⊢ ∃ i, (IsTranscendenceBasis k fun j ↦ a ↑j) ∧ IsSeparable (↥(adjoin k (a '' (insert n s \ {i})))) (a i)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Projective R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
⊢ (W'⁄B).addX (⇑↑f ∘ P) (⇑↑f ∘ Q) = ↑f ((W'⁄A).addX P Q)

Tactic:
← map_addX,

Goal state after:
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Projective R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
⊢ (W'⁄B).addX (⇑↑f ∘ P) (⇑↑f ∘ Q) = ((W'⁄A).map ↑f).addX (⇑↑f ∘ P) (⇑↑f ∘ Q)
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
H : IsIntegral R s
t : R
ht : t ∈ R⁰
ht' : t • s ∈ (algebraMap R S).range
i : ℕ
hi : i < (minpoly R s).natDegree
⊢ t ^ (minpoly R s).natDegree • s ^ i ∈ (algebraMap R S).range

Tactic:
rw [← Nat.sub_add_cancel hi.le, pow_add, mul_smul, ← smul_pow]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
H : IsIntegral R s
t : R
ht : t ∈ R⁰
ht' : t • s ∈ (algebraMap R S).range
i : ℕ
hi : i < (minpoly R s).natDegree
⊢ t ^ ((minpoly R s).natDegree - i) • (t • s) ^ i ∈ (algebraMap R S).range
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ Function.Injective (⇑(algebraMap K[X] K⟮X⟯) ∘ ⇑Polynomial.C)

Tactic:
exact Function.Injective.comp (algebraMap_injective K) (Polynomial.C_injective)

Goal state after:
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
p : S[X]
hp : IsIntegral R[X] p
i : ℕ
⊢ IsIntegral R (p.coeff i)

Tactic:
by
  nontriviality R
  nontriviality S
  obtain rfl | hp0 := eq_or_ne p 0; · simp [isIntegral_zero]
  let q := minpoly R[X] p
  let m := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
  have hm₁ (i) : (q.coeff i).natDegree < m := by
    by_cases hi : i ∈ q.support
    · exact (Finset.le_sup (f := fun i ↦ (q.coeff i).natDegree) hi).trans_lt (by lia)
    · simp_all [m]
  have hm₁' : (q.eval (X ^ m)).Monic := by
    rw [eval_eq_sum_range, Finset.sum_range_succ]
    refine .add_of_right (by simp [q, minpoly.monic hp, ← pow_mul]) (degree_lt_degree ?_)
    refine lt_of_lt_of_eq (b := m * q.natDegree) ?_ (by simp [q, minpoly.monic hp, ← pow_mul])
    refine (natDegree_sum_le ..).trans_lt ((Finset.fold_max_lt _).mpr
      ⟨by simpa using ⟨by lia, minpoly.natDegree_pos hp⟩, fun i hi ↦ ?_⟩)
    dsimp
    simp only [Finset.mem_range] at hi
    grw [← pow_mul, natDegree_mul_le, natDegree_X_pow, ← Nat.add_one_le_iff.mpr hi]
    have := hm₁ i
    lia
  have hm₂ : p.natDegree < m := by grind
  have h₀ : algebraMap R[X] S[X] X = X := by simp
  have : (((taylor (X ^ m)) q).map (algebraMap R[X] S[X])).IsRoot (p - X ^ m) := by
    simpa [-algebraMap_def, q, h₀] using
      ((q.map (algebraMap _ _)).taylor_eval (X ^ m) (p - X ^ m) :)
  have : X ^ m - p ∣ (eval (X ^ m) q).map (algebraMap _ _) := by
    change X ^ m - p ∣ Algebra.ofId R[X] S[X] _
    rw [← coe_aeval_eq_eval, ← aeval_algHom_apply, ← neg_dvd, neg_sub]
    simpa [Polynomial.taylor_coeff_zero, -algebraMap_def, h₀] using this.dvd_coeff_zero
  have := (isIntegral_coeff_of_dvd _ _ hm₁'
    ((monic_X_pow _).sub_of_left (by simpa [← natDegree_lt_iff_degree_lt, hp0])) this i).neg
  obtain hi | hi := le_or_gt i p.natDegree
  · simpa [show i ≠ m by lia] using this
  · simp [coeff_eq_zero_of_natDegree_lt hi, isIntegral_zero]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: case refine_2
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
x : R[X]
hx : ∀ (i : ℕ), x.coeff i ∈ I
⊢ x ∈ Ideal.map C I

Tactic:
Ideal.mem_map_C_iff

Goal state after:
case refine_2
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
x : R[X]
hx : ∀ (i : ℕ), x.coeff i ∈ I
⊢ ∀ (n : ℕ), x.coeff n ∈ I
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
inst✝ : WeaklyQuasiFiniteAt R Q
⊢ RingHom.ker (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) ≤ P

Tactic:
by simpa [← h₂] using Ideal.map_comap_le

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : p.IsPrime
inst✝² : q.LiesOver p
Q : Ideal (p.Fiber S)
inst✝¹ : Q.IsPrime
hQ : Ideal.comap TensorProduct.includeRight.toRingHom Q = q
inst✝ : QuasiFiniteAt p.ResidueField Q
Sq : Type u_2 := Localization.AtPrime q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
φ₁ : p.ResidueField →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  Ideal.quotientMapₐ (Ideal.map (algebraMap R Sq) p) (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) ⋯
φ₂ : p.Fiber S →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  TensorProduct.lift φ₁ (IsScalarTower.toAlgHom R S (Sq ⧸ Ideal.map (algebraMap R Sq) p)) ⋯
φ₃ : Localization.AtPrime Q →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p := IsLocalization.liftAlgHom ⋯
x : Sq ⧸ Ideal.map (algebraMap R Sq) p
⊢ ∃ a, φ₃ a = x

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : p.IsPrime
inst✝² : q.LiesOver p
Q : Ideal (p.Fiber S)
inst✝¹ : Q.IsPrime
hQ : Ideal.comap TensorProduct.includeRight.toRingHom Q = q
inst✝ : QuasiFiniteAt p.ResidueField Q
Sq : Type u_2 := Localization.AtPrime q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
φ₁ : p.ResidueField →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  Ideal.quotientMapₐ (Ideal.map (algebraMap R Sq) p) (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) ⋯
φ₂ : p.Fiber S →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  TensorProduct.lift φ₁ (IsScalarTower.toAlgHom R S (Sq ⧸ Ideal.map (algebraMap R Sq) p)) ⋯
φ₃ : Localization.AtPrime Q →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p := IsLocalization.liftAlgHom ⋯
x : Sq
⊢ ∃ a, φ₃ a = (Ideal.Quotient.mk (Ideal.map (algebraMap R Sq) p)) x
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case refine_2
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
x : ↥(Spec R)
hP : x.asIdeal.IsPrime
⊢ (Arrow.mk (Hom.fiberToSpecResidueField (Spec.map φ) x)).right ≅
    (Arrow.mk (Spec.map (CommRingCat.ofHom (algebraMap x.asIdeal.ResidueField (x.asIdeal.Fiber ↑S))))).right

Tactic:
exact asIso (Spec.map (Spec.residueFieldIso _ x).inv)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: case mp
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
f₂ : ↑Γ(X, U.toOpens)
hf₂s : f₂ ∈ s
hW : IsAffineOpen (X.basicOpen f₂)
f₁ : ↑Γ(X, toOpens ⟨X.basicOpen f₂, hW⟩)
hV : IsAffineOpen (X.basicOpen f₁)
f₃ : ↑Γ(X, ↑U)
hf₃ : X.basicOpen f₃ = X.basicOpen f₁
⊢ X.basicOpen (f₂ * f₃) = toOpens ⟨X.basicOpen f₁, hV⟩

Tactic:
X.basicOpen_mul,

Goal state after:
case mp
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
f₂ : ↑Γ(X, U.toOpens)
hf₂s : f₂ ∈ s
hW : IsAffineOpen (X.basicOpen f₂)
f₁ : ↑Γ(X, toOpens ⟨X.basicOpen f₂, hW⟩)
hV : IsAffineOpen (X.basicOpen f₁)
f₃ : ↑Γ(X, ↑U)
hf₃ : X.basicOpen f₃ = X.basicOpen f₁
⊢ X.basicOpen f₂ ⊓ X.basicOpen f₃ = toOpens ⟨X.basicOpen f₁, hV⟩
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f✝ : X ⟶ Y
inst✝² : LocallyQuasiFinite f✝
x : ↥X
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.QuasiFinite
J : Ideal S
x✝ : J.IsPrime
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.QuasiFinite R S
⊢ ((Localization.localRingHom (Ideal.comap f J) J f ⋯).comp
      (algebraMap R (Localization.AtPrime (Ideal.comap f J)))).QuasiFinite

Tactic:
convert!
    RingHom.quasiFinite_algebraMap.mpr
      (inferInstance : Algebra.QuasiFinite R (Localization.AtPrime J))

Goal state after:
X Y : Scheme
f✝ : X ⟶ Y
inst✝² : LocallyQuasiFinite f✝
x : ↥X
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.QuasiFinite
J : Ideal S
x✝ : J.IsPrime
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.QuasiFinite R S
⊢ (Localization.localRingHom (Ideal.comap f J) J f ⋯).comp (algebraMap R (Localization.AtPrime (Ideal.comap f J))) =
    algebraMap R (Localization.AtPrime J)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: L : Type u_2
R : Type u_3
inst✝¹ : Field L
inst✝ : CommRing R
φ : R[X] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
x : R[X]
⊢ (liftRingHom φ hφ) { toFractionRing := (algebraMap R[X] (FractionRing R[X])) x } = φ x

Tactic:
rw [← Localization.mk_one_eq_algebraMap, liftRingHom_apply_ofFractionRing_mk]

Goal state after:
L : Type u_2
R : Type u_3
inst✝¹ : Field L
inst✝ : CommRing R
φ : R[X] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
x : R[X]
⊢ φ x / φ ↑1 = φ x
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
x : S
h : P.HasMap x
f : S →ₐ[R] T
⊢ (aeval (f x)) P.f = 0

Tactic:
simp [aeval_algHom, h.1]

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

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
ε : S
hεI : ε ∈ I
b : S
hb : (aeval x) (derivative P.f) * b = 1 + ε
this✝ : (aeval x) P.f ^ 2 = 0
this : (aeval x) P.f * ε = 0
⊢ ∀ (y : S), (fun ε ↦ ε ∈ I ∧ P.HasMap (x + ε)) y → y = (aeval x) P.f * -b

Tactic:
rintro ε' ⟨hε'I, hε', hε''⟩
    rw [Polynomial.aeval_add_of_sq_eq_zero _ _ _ (hI.le (Ideal.pow_mem_pow hε'I 2))] at hε'
    have : ε * ε' = 0 := ((pow_two _).symm.trans hI).le (Ideal.mul_mem_mul hεI hε'I)
    grind

Goal state after:
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
P : StandardEtalePresentation R S
⊢ Ideal.span (Set.range ![(Bivariate.equivMvPolynomial R) (C P.f), (Bivariate.equivMvPolynomial R) (Y * C P.g - 1)]) =
    RingHom.ker
      ↑(Ideal.Quotient.mkₐ R
          (Ideal.span {(Bivariate.equivMvPolynomial R) (C P.f), (Bivariate.equivMvPolynomial R) (Y * C P.g - 1)}))

Tactic:
simp [Set.pair_comm]

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
φ : 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'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
g : S'[X]
hg :
  Polynomial.map (algebraMap S S') (derivative f * y) -
      (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum =
    Polynomial.map (algebraMap S S') f * g
⊢ ∀ a ∈ m, ((Multiset.map (fun x ↦ X - C x) (m.erase a)).prod * C ((aeval a) y)).natDegree ≤ f.natDegree - 1

Tactic:
refine fun a ha ↦ (natDegree_mul_C_le _ _).trans ((natDegree_multiset_prod_le _).trans ?_)

Goal state after:
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'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
g : S'[X]
hg :
  Polynomial.map (algebraMap S S') (derivative f * y) -
      (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum =
    Polynomial.map (algebraMap S S') f * g
a : S'
ha : a ∈ m
⊢ (Multiset.map natDegree (Multiset.map (fun x ↦ X - C x) (m.erase a))).sum ≤ f.natDegree - 1
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
⊢ ∃ q n, IsIntegral R (p.leadingCoeff ^ n • t - φ q)

Tactic:
by
  set a := p.leadingCoeff
  let R' := Localization.Away a
  let S' := Localization.Away (algebraMap R S a)
  let : Algebra R' S' := (Localization.awayMap (algebraMap R S) a).toAlgebra
  have : IsScalarTower R R' S' := .of_algebraMap_eq (by
    simp +zetaDelta [RingHom.algebraMap_toAlgebra, IsLocalization.Away.map, ← algebraMap_apply R S])
  have ha : IsUnit (algebraMap R R' a) := IsLocalization.Away.algebraMap_isUnit a
  have H : (aeval ((algebraMap S S') (φ X))).toRingHom.comp (mapRingHom (algebraMap R R')) =
    (algebraMap S S').comp φ := by ext <;>
      simp [-Polynomial.algebraMap_apply, ← Polynomial.algebraMap_eq, ← algebraMap_apply]
  obtain ⟨q, hq⟩ := exists_isIntegral_sub_of_isIntegralElem_of_mul_mem_range (R := R')
    (aeval (algebraMap S S' (φ X))) (algebraMap S S' t) (C ha.unit⁻¹.1 * p.map (algebraMap _ _)) (by
      obtain ⟨q, hqm, hq⟩ := ht
      refine ⟨q.map (mapRingHom (algebraMap _ _)), hqm.map _, ?_⟩
      rw [eval₂_map, H, ← hom_eval₂, ← AlgHom.toRingHom_eq_coe, hq, map_zero]) (by
      nontriviality R'
      simp [Monic, leadingCoeff_C_mul_of_isUnit,
        leadingCoeff_map_of_leadingCoeff_ne_zero _ ha.ne_zero, a]) (by
      obtain ⟨r, hr : φ r = _⟩ := hp
      use C ha.unit⁻¹.1 * mapRingHom (algebraMap R R') r
      simp [aeval_algebraMap_apply, aeval_algHom_apply, hr, mul_assoc])
  obtain ⟨_, ⟨n, rfl⟩, e⟩ := IsLocalization.integerNormalization_spec (.powers a) q
  generalize IsLocalization.integerNormalization (.powers a) q = q' at e
  have : IsIntegral R' ((algebraMap S S') (a ^ n • t - φ q')) := by
    have : algebraMap S S' (φ q') = (algebraMap R S' a) ^ n * aeval (algebraMap S S' (φ X)) q := by
      simpa [Algebra.smul_def, aeval_algebraMap_apply, aeval_algHom_apply, ← algebraMap_apply] using
        congr(aeval (algebraMap S S' (φ X)) $e)
    simpa [Algebra.smul_def, ← mul_sub, ← algebraMap_apply, this] using
      (isIntegral_algebraMap (A := S') (x := algebraMap R R' a ^ n)).mul hq
  obtain ⟨⟨_, m, rfl⟩, hm⟩ := this.exists_multiple_integral_of_isLocalization (.powers a) _
  simp only [Algebra.smul_def, Submonoid.smul_def, algebraMap_apply R S S', ← map_mul] at hm
  obtain ⟨_, ⟨k, rfl⟩, hk⟩ := IsLocalization.exists_isIntegral_smul_of_isIntegral_map (.powers a) hm
  refine ⟨C a ^ (k + m) * q', k + m + n, ?_⟩
  convert! hk using 1
  simp only [Algebra.smul_def, map_pow, ← Polynomial.algebraMap_eq, map_mul, AlgHom.commutes]
  ring

Goal state after: