mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Smooth A B
P : Presentation A B (Fin (Presentation.ofFinitePresentationVars A B))
  (Fin (Presentation.ofFinitePresentationRels A B)) :=
  Presentation.ofFinitePresentation A B
f : P.Ring →ₐ[A] B := IsScalarTower.toAlgHom A P.Ring B
hkerf : RingHom.ker f = Ideal.span (Set.range P.relation)
σ : B →ₐ[A] MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A ⧸ RingHom.ker f ^ 2
hsig✝ : f.kerSquareLift.comp σ = AlgHom.id A B
h : Fin (Presentation.ofFinitePresentationVars A B) → MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A
hh :
  ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), (Ideal.Quotient.mk (RingHom.ker f ^ 2)) (h i) = σ (P.val i)
hdiag : (Ideal.Quotient.mkₐ A (RingHom.ker f ^ 2)).comp (aeval h) = σ.comp (aeval P.val)
p :
  Fin (Presentation.ofFinitePresentationRels A B) →
    MvPolynomial (Fin (Presentation.ofFinitePresentationRels A B))
      (MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A)
homog : ∀ (j : Fin (Presentation.ofFinitePresentationRels A B)), (p j).IsHomogeneous 2
hp : ∀ (j : Fin (Presentation.ofFinitePresentationRels A B)), (eval P.relation) (p j) = (aeval h) (P.relation j)
hsig : ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), f (h i) = P.val i
q :
  Fin (Presentation.ofFinitePresentationVars A B) →
    MvPolynomial (Fin (Presentation.ofFinitePresentationRels A B)) P.Ring
hqhom : ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), (q i).IsHomogeneous 1
hq : ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), (eval P.relation) (q i) = h i - X i
D : DescentAux A B :=
  { vars := Fin (Presentation.ofFinitePresentationVars A B), rels := Fin (Presentation.ofFinitePresentationRels A B),
    P := P, σ := σ, h := h, p := p, hphom := homog, hp := hp, q := q, hqhom := hqhom, hq := hq }
this : P.HasCoeffs ↥(DescentAux.subalgebra R D)
σ₀ :
  Presentation.ModelOfHasCoeffs ↥(DescentAux.subalgebra R D) →ₐ[↥(DescentAux.subalgebra R D)]
    MvPolynomial D.vars ↥(DescentAux.subalgebra R D) ⧸
      RingHom.ker
          (Ideal.Quotient.mkₐ (↥(DescentAux.subalgebra R D))
            (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(DescentAux.subalgebra R D))))) ^
        2
hσ₀ :
  (Ideal.Quotient.mkₐ (↥(DescentAux.subalgebra R D))
            (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(DescentAux.subalgebra R D))))).kerSquareLift.comp
      σ₀ =
    AlgHom.id (↥(DescentAux.subalgebra R D)) (Presentation.ModelOfHasCoeffs ↥(DescentAux.subalgebra R D))
⊢ ∃ A₀ B₀ x x_1, A₀.FG ∧ Smooth (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)

Tactic:
exact ⟨D.subalgebra R, P.ModelOfHasCoeffs (D.subalgebra R), inferInstance, inferInstance,
    D.fg_subalgebra R, ⟨.of_split _ σ₀ hσ₀, inferInstance⟩,
    ⟨(P.tensorModelOfHasCoeffsEquiv (D.subalgebra R)).symm⟩⟩

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
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
⊢ ∃ i ∈ Finset.univ, (fun x ↦ coeff (↑x) F) i ≠ 0

Tactic:
by simpa [MvPolynomial.eq_zero_iff] using! hF0

Goal state after:
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 : Fin 3 → A
⊢ (W'⁄B).dblY (⇑f ∘ P) = f ((W'⁄A).dblY P)

Tactic:
by
  rw [← RingHom.coe_coe, ← map_dblY, map_baseChange]

Goal state after:
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).addXYZ (⇑↑f ∘ P) (⇑↑f ∘ Q) = ⇑↑f ∘ (W'⁄A).addXYZ P Q

Tactic:
← map_addXYZ,

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).addXYZ (⇑↑f ∘ P) (⇑↑f ∘ Q) = ((W'⁄A).map ↑f).addXYZ (⇑↑f ∘ P) (⇑↑f ∘ Q)
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat) (φ : R ⟶ S),
    Function.Surjective ⇑(ConcreteCategory.hom φ) →
      RingHom.ker (CommRingCat.Hom.hom φ) ^ 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified

Tactic:
refine Algebra.FormallyUnramified.iff_comp_injective.mpr fun R _ _ I hI g₁ g₂ hg₁g₂ ↦ ?_

Goal state after:
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat) (φ : R ⟶ S),
    Function.Surjective ⇑(ConcreteCategory.hom φ) →
      RingHom.ker (CommRingCat.Hom.hom φ) ^ 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
R : Type u
x✝¹ : CommRing R
x✝ : Algebra (↑Γ(Y, U)) R
I : Ideal R
hI : I ^ 2 = ⊥
g₁ g₂ : ↑Γ(X, V) →ₐ[↑Γ(Y, U)] R
hg₁g₂ : (Ideal.Quotient.mkₐ (↑Γ(Y, U)) I).comp g₁ = (Ideal.Quotient.mkₐ (↑Γ(Y, U)) I).comp g₂
⊢ g₁ = g₂
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: ⊢ DescendsAlong (@UniversallyInjective) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Tactic:
by
  rw [universallyInjective_eq_diagonal]
  infer_instance

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

Goal state before:
pp: P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
inst✝ : MorphismProperty.DescendsAlong (@IsAffineHom) P'
hQ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
φ : R ⟶ S
h : P' (Spec.map φ)
Y : CommRingCat
g : Spec Y ⟶ Spec R
hf : P (pullback.fst (Spec.map φ) g)
this : IsAffine (Spec Y)
⊢ ∀ {R S : CommRingCat} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)

Tactic:
simp [SpecMap_iff_of_affineAnd _ hQ]

Goal state after:
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

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
x : T
h : IsStronglyTranscendental R x
H : Function.Surjective ⇑(algebraMap R S)
⊢ IsStronglyTranscendental S x

Tactic:
by
  intro t p hp
  obtain ⟨p, rfl⟩ := map_surjective _ H p
  simpa [map_map, ← IsScalarTower.algebraMap_eq] using h t p (by simpa using hp)

Goal state after:
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
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
⊢ IsAlmostIntegral R s

Tactic:
obtain ⟨s, t, rfl⟩ := IsLocalization.exists_mk'_eq M s

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
s : R
t : ↥M
H : IsIntegral R (IsLocalization.mk' S s t)
⊢ IsAlmostIntegral R (IsLocalization.mk' S s t)
Module: Mathlib.RingTheory.Valuation.IsTrivialOn

Goal state before:
pp: case inr
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommRing A
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : y ≠ 0
hy : v y ≠ 1
this : ∀ (y : K), y ≠ 0 → v y ≠ 1 → 1 < v y → Transcendental A y
hlt : v y ≤ 1
⊢ Transcendental A y

pp: Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommRing A
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : y ≠ 0
hy : v y ≠ 1
hlt : 1 < v y
⊢ Transcendental A y

Tactic:
· rw [Transcendental, ← IsAlgebraic.inv_iff]
    apply this _ (by simpa) (by simpa)
    rw [← val_lt_one_iff _ h0]
    exact lt_of_le_of_ne hlt hy

Goal state after:
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommRing A
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : y ≠ 0
hy : v y ≠ 1
hlt : 1 < v y
⊢ Transcendental A y
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case e_p
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
⊢ (x * y).num * (x.denom * y.denom) = x.num * y.num * (x * y).denom

Tactic:
apply num_denom_mul

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 : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (X ^ m) q).Monic
hm₂ : p.natDegree < m
h₀ : (algebraMap R[X] S[X]) X = X
⊢ (Polynomial.map (algebraMap R[X] S[X]) ((taylor (X ^ m)) q)).IsRoot (p - X ^ m)

Tactic:
simpa [-algebraMap_def, q, h₀] using
      ((q.map (algebraMap _ _)).taylor_eval (X ^ m) (p - X ^ m) :)

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 ≤
    Ideal.comap ((↑(IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq)).comp (algebraMap R (Localization.AtPrime p)))
      (Ideal.map (algebraMap R Sq) p)

Tactic:
simpa [← IsScalarTower.algebraMap_eq] using Ideal.le_comap_map

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

Goal state before:
pp: X : Scheme
⊢ ∀ (a b c : X.AffineZariskiSite),
    (∃ f, X.basicOpen f = a.toOpens) → (∃ f, X.basicOpen f = b.toOpens) → ∃ f, X.basicOpen f = a.toOpens

Tactic:
by
    rintro ⟨U, hU⟩ ⟨V, hV⟩ ⟨W, hW⟩ ⟨f, rfl⟩ ⟨g, rfl⟩
    exact hW.basicOpen_basicOpen_is_basicOpen g f

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

Goal state before:
pp: X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
U : X.AffineZariskiSite
f : ↑Γ(X, ↑U)
αU : Γ(X, U.toOpens) ⟶ F.obj (Opposite.op U) := α.app (Opposite.op U)
⊢ IsPushout (X.presheaf.map (homOfLE ⋯).op) αU (α.app (Opposite.op (U.basicOpen f))) (F.map (homOfLE ⋯).op) ↔
    IsLocalization.Away ((ConcreteCategory.hom αU) f) ↑(F.obj (Opposite.op (U.basicOpen f)))

Tactic:
set αUf : Γ(X, X.basicOpen f) ⟶ F.obj (.op (U.basicOpen f)) := α.app (.op (U.basicOpen f))

Goal state after:
X : Scheme
F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat
α : (toOpensFunctor X).op ⋙ X.presheaf ⟶ F
U : X.AffineZariskiSite
f : ↑Γ(X, ↑U)
αU : Γ(X, U.toOpens) ⟶ F.obj (Opposite.op U) := α.app (Opposite.op U)
αUf : Γ(X, X.basicOpen f) ⟶ F.obj (Opposite.op (U.basicOpen f)) := α.app (Opposite.op (U.basicOpen f))
⊢ IsPushout (X.presheaf.map (homOfLE ⋯).op) αU αUf (F.map (homOfLE ⋯).op) ↔
    IsLocalization.Away ((ConcreteCategory.hom αU) f) ↑(F.obj (Opposite.op (U.basicOpen f)))
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case inl.hq
K : Type u
inst✝⁵ : CommRing K
inst✝⁴ : IsDomain K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p : K[X]
this : 0 = (algebraMap K[X] K⟮X⟯) 0 / (algebraMap K[X] K⟮X⟯) 1
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

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

Goal state before:
pp: case inr
X : Scheme
x : ↥X
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X : Scheme} {x : ↥X} (R : CommRingCat) {f : X ⟶ Spec R} [LocallyOfFiniteType f],
    (∃ S, X = Spec S) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hX : ¬∃ S, X = Spec S
⊢ QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩}

pp: X : Scheme
x : ↥X
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
hX : ∃ S, X = Spec S
⊢ QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩}

Tactic:
· obtain ⟨i, x, rfl⟩ := X.affineCover.exists_eq x
    let ι := X.affineCover.f i
    convert! this (x := x) _ (f := ι ≫ f) ⟨_, rfl⟩ using 1
    · exact quasiFiniteAt_comp_iff_of_isOpenImmersion.symm
    rw [((f ⁻¹' {f (ι x)}).restrictPreimage_isOpenEmbedding
      ι.isOpenEmbedding).isOpen_iff_image_isOpen, Set.image_singleton]; rfl

Goal state after:
X : Scheme
x : ↥X
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
hX : ∃ S, X = Spec S
⊢ QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩}
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
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
⊢ (aeval (x + (aeval x) P.f * -b)) P.f = 0

Tactic:
Polynomial.aeval_add_of_sq_eq_zero _ _ _ (by grind)

Goal state after:
case refine_1
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
⊢ (aeval x) P.f + (aeval x) (derivative P.f) * ((aeval x) P.f * -b) = 0
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
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this✝⁵ : p.IsPrime
this✝⁴ : Module p.ResidueField (p.Fiber S) := leftModule
this✝³ : SMul p.ResidueField (p.Fiber S) := this✝⁴.toSMul
this✝² : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := IsScalarTower.right
this✝¹ : Module.Finite p.ResidueField (p.Fiber S) := Module.Finite.base_change R p.ResidueField S
this✝ : IsArtinianRing (p.Fiber S)
α : ↑(p.primesOver S) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : p.ResidueField ⊗[R] S
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯
hx0 : φ x ≠ 0
hx : p.ResidueField[φ x] = ⊤
r : p.Fiber S
hrQ : r ∉ (α ⟨Q, ⋯⟩).asIdeal
hrid : IsIdempotentElem r
hr : ∀ (q : Ideal (p.Fiber S)), q.IsPrime → q ≠ (α ⟨Q, ⋯⟩).asIdeal → r ∈ q
s : R
hsQ : s ∉ p
t : S
e : s • (r * x) = 1 ⊗ₜ[R] t
this : Ideal.ResidueField.mapₐ p Q (ofId R S) ⋯ = AlgHom.restrictScalars R (ofId p.ResidueField Q.ResidueField)
⊢ (TensorProduct.lift (AlgHom.restrictScalars R (ofId p.ResidueField Q.ResidueField))
        (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯)
      r ≠
    0

Tactic:
convert! hrQ

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
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := ⋯
this✝⁵ : p.IsPrime
this✝⁴ : Module p.ResidueField (p.Fiber S) := ⋯
this✝³ : SMul p.ResidueField (p.Fiber S) := ⋯
this✝² : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := ⋯
this✝¹ : Module.Finite p.ResidueField (p.Fiber S) := ⋯
this✝ : IsArtinianRing (p.Fiber S)
α : ↑(p.primesOver S) ≃o PrimeSpectrum (p.Fiber S) := ⋯
x : p.ResidueField ⊗[R] S
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField := ⋯
hx0 : φ x ≠ 0
hx : p.ResidueField[φ x] = ⊤
r : p.Fiber S
hrQ : r ∉ (α ⟨Q, ⋯⟩).asIdeal
hrid : IsIdempotentElem r
hr : ∀ (q : Ideal (p.Fiber S)), q.IsPrime → q ≠ (α ⟨Q, ⋯⟩).asIdeal → r ∈ q
s : R
hsQ : s ∉ p
t : S
e : s • (r * x) = 1 ⊗ₜ[R] t
this : Ideal.ResidueField.mapₐ p Q (ofId R S) ⋯ = AlgHom.restrictScalars R (ofId p.ResidueField Q.ResidueField)
⊢ (TensorProduct.lift (AlgHom.restrictScalars R (ofId p.ResidueField Q.ResidueField))
          (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯)
        r =
      0 ↔
    r ∈ (α ⟨Q, ⋯⟩).asIdeal
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)
⊢ ∃ q n, IsIntegral R (a ^ n • t - φ q)

Tactic:
let : Algebra R' S' := (Localization.awayMap (algebraMap R S) a).toAlgebra

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
⊢ ∃ q n, IsIntegral R (a ^ n • t - φ q)
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 ↑φ
a✝ : Nontrivial R'
⊢ (C ↑ha.unit⁻¹ * map (algebraMap R R') p).Monic

Tactic:
simp [Monic, leadingCoeff_C_mul_of_isUnit,
        leadingCoeff_map_of_leadingCoeff_ne_zero _ ha.ne_zero, a]

Goal state after:
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✝
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✝¹ : FiniteType R S
inst✝ : IsUnramifiedAt R Q
H : Unramified R S
S' : Subalgebra R S
hS' : (Subalgebra.toSubmodule S').FG
r : ↥S'
hrQ : ↑r ∉ Q
hr : Function.Bijective ⇑(Localization.awayMap S'.val.toRingHom r)
this✝ : Module.Finite R ↥S'
this : FormallyUnramified R (Localization.Away r)
⊢ IsUnramifiedAt R (Ideal.under (↥S') Q)

Tactic:
rw [← basicOpen_subset_unramifiedLocus_iff] at this

Goal state after:
R✝ : Type u_1
S✝ : Type u_3
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing S✝
inst✝⁶ : Algebra R✝ S✝
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✝¹ : FiniteType R S
inst✝ : IsUnramifiedAt R Q
H : Unramified R S
S' : Subalgebra R S
hS' : (Subalgebra.toSubmodule S').FG
r : ↥S'
hrQ : ↑r ∉ Q
hr : Function.Bijective ⇑(Localization.awayMap S'.val.toRingHom r)
this✝ : Module.Finite R ↥S'
this : ↑(PrimeSpectrum.basicOpen r) ⊆ unramifiedLocus R ↥S'
⊢ IsUnramifiedAt R (Ideal.under (↥S') Q)
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: case refine_1
m n : ℕ
R : Type u_2
inst✝ : Ring R
f : ↥R[X]_(m + n)
a✝ : Nontrivial R
⊢ ↑((addLinearEquiv R m n).symm ((addLinearEquiv R m n) f)) = ↑f

Tactic:
LinearEquiv.symm_apply_apply

Goal state after:
case refine_1
m n : ℕ
R : Type u_2
inst✝ : Ring R
f : ↥R[X]_(m + n)
a✝ : Nontrivial R
⊢ ↑f = ↑f
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
a✝ : Nontrivial R
i j : Fin n
hji : id j < id i
⊢ ((taylor r) (X ^ ↑j)).degree < ↑↑i

Tactic:
simpa [-taylor_X_pow, -taylor_pow]

Goal state after: