mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
this✝ : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst✝ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst✝ : Algebra.FinitePresentation ↑Γ(Y, U) ↑Γ(X, V)
this : Algebra.IsSmoothAt (↑Γ(Y, U)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
r : ↑Γ(X, V)
hrx : ((IsAffineOpen.isoSpec hV).hom ≫ IsAffineOpen.fromSpec hV) ⟨x, hxV⟩ ∈ X.basicOpen r
hr : Algebra.Smooth (↑Γ(Y, U)) (Localization.Away r)
⊢ x ∈ X.basicOpen r

Tactic:
IsAffineOpen.isoSpec_hom,

Goal state after:
case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
this✝ : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst✝ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst✝ : Algebra.FinitePresentation ↑Γ(Y, U) ↑Γ(X, V)
this : Algebra.IsSmoothAt (↑Γ(Y, U)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
r : ↑Γ(X, V)
hrx : (Scheme.Opens.toSpecΓ V ≫ IsAffineOpen.fromSpec hV) ⟨x, hxV⟩ ∈ X.basicOpen r
hr : Algebra.Smooth (↑Γ(Y, U)) (Localization.Away r)
⊢ x ∈ X.basicOpen r
Module: Mathlib.AlgebraicGeometry.Morphisms.Etale

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

Tactic:
by
  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 : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : IsOpenImmersion (pullback.diagonal (Spec.map φ))
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
F : TensorProduct ↑R ↑S ↑S →+* ↑S := (Algebra.TensorProduct.lmul' ↑R).toRingHom
hF : Function.Surjective ⇑F
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom F))
e : ↑(CommRingCat.of (TensorProduct ↑R ↑S ↑S))
he : IsIdempotentElem e
he' : RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom F)) = Ideal.span {e}
x : ↑(CommRingCat.of (TensorProduct ↑R ↑S ↑S))
hx : e * x ∈ KaehlerDifferential.ideal ↑R ↑S
⊢ ↑⟨e * x, hx⟩ ∈ KaehlerDifferential.ideal ↑R ↑S ^ 2

Tactic:
pow_two,

Goal state after:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : IsOpenImmersion (pullback.diagonal (Spec.map φ))
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
F : TensorProduct ↑R ↑S ↑S →+* ↑S := (Algebra.TensorProduct.lmul' ↑R).toRingHom
hF : Function.Surjective ⇑F
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom F))
e : ↑(CommRingCat.of (TensorProduct ↑R ↑S ↑S))
he : IsIdempotentElem e
he' : RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom F)) = Ideal.span {e}
x : ↑(CommRingCat.of (TensorProduct ↑R ↑S ↑S))
hx : e * x ∈ KaehlerDifferential.ideal ↑R ↑S
⊢ ↑⟨e * x, hx⟩ ∈ KaehlerDifferential.ideal ↑R ↑S * KaehlerDifferential.ideal ↑R ↑S
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: case H.inr
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : (@Surjective ⊓ @Flat) (Spec.map φ)
hfst : IsIso (pullback.fst (Spec.map φ) g)
this✝ : IsAffine Y
this :
  ∀ {Y : Scheme} (g : Y ⟶ Spec R),
    IsIso (pullback.fst (Spec.map φ) g) → IsAffine Y → (∃ T, Y = Spec T) → isomorphisms Scheme g
hY : ¬∃ T, Y = Spec T
heq :
  pullback.fst (Spec.map φ) (Y.isoSpec.inv ≫ g) =
    pullback.map (Spec.map φ) (Y.isoSpec.inv ≫ g) (Spec.map φ) g (𝟙 (Spec S)) Y.isoSpec.inv (𝟙 (Spec R)) ⋯ ⋯ ≫
      pullback.fst (Spec.map φ) g
⊢ isomorphisms Scheme (pullback.fst (Spec.map φ) (Y.isoSpec.inv ≫ g))

Tactic:
rwa [heq, (isomorphisms Scheme).cancel_left_of_respectsIso]

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (pullback.fst f g)
this✝ : UniversallyOpen g
U : Z.Opens := { carrier := Set.range ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ ↑U := pullback.snd f U.ι
g' : Y ⟶ ↑U := IsOpenImmersion.lift U.ι g ⋯
this : Surjective g'
⊢ IsIso (pullback.fst f' g')

Tactic:
isIso_iff_isOpenImmersion_and_surjective

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (pullback.fst f g)
this✝ : UniversallyOpen g
U : Z.Opens := { carrier := Set.range ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ ↑U := pullback.snd f U.ι
g' : Y ⟶ ↑U := IsOpenImmersion.lift U.ι g ⋯
this : Surjective g'
⊢ IsOpenImmersion (pullback.fst f' g') ∧ Surjective (pullback.fst f' g')
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
x : S
f : S →ₐ[R] T
hf : Function.Injective ⇑f
h : IsStronglyTranscendental R (f x)
u : S
⊢ ∀ (p : R[X]), (aeval x) p * u = 0 → map (algebraMap R S) p * C u = 0

Tactic:
p

Goal state after:
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
x : S
f : S →ₐ[R] T
hf : Function.Injective ⇑f
h : IsStronglyTranscendental R (f x)
u : S
p : R[X]
⊢ (aeval x) p * u = 0 → map (algebraMap R S) p * C u = 0
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
M : Submonoid S
inst✝¹ : IsLocalization M T
inst✝ : IsScalarTower R S T
x : S
h : IsStronglyTranscendental R x
u : T
⊢ ∀ (p : R[X]), (aeval ((algebraMap S T) x)) p * u = 0 → map (algebraMap R T) p * C u = 0

Tactic:
p

Goal state after:
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
M : Submonoid S
inst✝¹ : IsLocalization M T
inst✝ : IsScalarTower R S T
x : S
h : IsStronglyTranscendental R x
u : T
p : R[X]
⊢ (aeval ((algebraMap S T) x)) p * u = 0 → map (algebraMap R T) p * C u = 0
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
M : Submonoid R
inst✝¹ : IsLocalization M S
inst✝ : IsScalarTower R S T
x : T
h : IsStronglyTranscendental R x
t : T
⊢ ∀ (p : S[X]), (aeval x) p * t = 0 → map (algebraMap S T) p * C t = 0

Tactic:
p

Goal state after:
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
M : Submonoid R
inst✝¹ : IsLocalization M S
inst✝ : IsScalarTower R S T
x : T
h : IsStronglyTranscendental R x
t : T
p : S[X]
⊢ (aeval x) p * t = 0 → map (algebraMap S T) p * C t = 0
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 S x
t : T
⊢ ∀ (p : R[X]), (aeval x) p * t = 0 → map (algebraMap R T) p * C t = 0

Tactic:
p

Goal state after:
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 S x
t : T
p : R[X]
⊢ (aeval x) p * t = 0 → map (algebraMap R T) p * C t = 0
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)
t : T
⊢ ∀ (p : S[X]), (aeval x) p * t = 0 → map (algebraMap S T) p * C t = 0

Tactic:
p

Goal state after:
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)
t : T
p : S[X]
⊢ (aeval x) p * t = 0 → map (algebraMap S T) p * C t = 0
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

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:
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
n : ℕ
a : K
⊢ (algebraMap K[X] K⟮X⟯) ((Polynomial.monomial n) a) = C a * X ^ n

Tactic:
simp [← Polynomial.C_mul_X_pow_eq_monomial]

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L
h : Transcendental K f
u : K⟮X⟯
⊢ ↑((algEquivOfTranscendental f h) ((algebraMap K[X] K⟮X⟯) u.num / (algebraMap K[X] K⟮X⟯) u.denom)) =
    (aeval f) u.num / (aeval f) u.denom

Tactic:
simp [-num_div_denom]

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u_1
inst✝ : Field K
⊢ Function.Surjective ⇑Valued.v

Tactic:
intro n

Goal state after:
K : Type u_1
inst✝ : Field K
n : WithZero (Multiplicative ℤ)
⊢ ∃ a, Valued.v a = n
Module: Mathlib.RingTheory.Polynomial.IsIntegral

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 w
f : MvPolynomial σ S
H : (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S},
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f →
      ∀ (n : σ →₀ ℕ), Finite σ → IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial (↥f.vars) S
hg : (rename Subtype.val) g = f
n : ↥f.vars →₀ ℕ
⊢ f = ((rename Subtype.val).comp (killCompl ⋯)).toRingHom f

Tactic:
← hg

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 w
f : MvPolynomial σ S
H : (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S},
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f →
      ∀ (n : σ →₀ ℕ), Finite σ → IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial (↥f.vars) S
hg : (rename Subtype.val) g = f
n : ↥f.vars →₀ ℕ
⊢ (rename Subtype.val) g = ((rename Subtype.val).comp (killCompl ⋯)).toRingHom ((rename Subtype.val) g)
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
q : Ideal S
inst✝ : q.IsPrime
q' : Ideal (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R q)) :=
  Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R q))) q
hq' : q = Ideal.comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R q))) q'
φ₁ : Localization.AtPrime q →ₐ[R] Localization.AtPrime q' :=
  Localization.localAlgHom q q' (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap R S) (Ideal.under R q))) hq'
hφ₁ : Function.Surjective ⇑φ₁
x : Localization.AtPrime q
⊢ x ∈ RingHom.ker φ₁ ↔
    x ∈ Ideal.map (↑AlgEquiv.refl) (Ideal.map (algebraMap R (Localization.AtPrime q)) (Ideal.under R q))

Tactic:
obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq q.primeCompl x

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
q : Ideal S
inst✝ : q.IsPrime
q' : Ideal (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R q)) :=
  Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R q))) q
hq' : q = Ideal.comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R q))) q'
φ₁ : Localization.AtPrime q →ₐ[R] Localization.AtPrime q' :=
  Localization.localAlgHom q q' (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap R S) (Ideal.under R q))) hq'
hφ₁ : Function.Surjective ⇑φ₁
x s : S
hs : s ∈ q.primeCompl
⊢ IsLocalization.mk' (Localization.AtPrime q) x ⟨s, hs⟩ ∈ RingHom.ker φ₁ ↔
    IsLocalization.mk' (Localization.AtPrime q) x ⟨s, hs⟩ ∈
      Ideal.map (↑AlgEquiv.refl) (Ideal.map (algebraMap R (Localization.AtPrime q)) (Ideal.under R q))
Module: Mathlib.RingTheory.QuasiFinite.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
f : R[X] →ₐ[R] S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : Algebra.WeaklyQuasiFiniteAt R P
algInst✝ : Algebra R[X] S := f.toAlgebra
e : Ideal.map C (Ideal.under R P) = Ideal.comap (↑f) P
this : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime (Ideal.under R[X] P)) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) (Ideal.under R[X] P)
⊢ False

Tactic:
let := Localization.AtPrime.algebraOfLiesOver (P.under R[X]) P

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X] →ₐ[R] S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : Algebra.WeaklyQuasiFiniteAt R P
algInst✝ : Algebra R[X] S := f.toAlgebra
e : Ideal.map C (Ideal.under R P) = Ideal.comap (↑f) P
this✝ : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime (Ideal.under R[X] P)) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) (Ideal.under R[X] P)
this : Algebra (Localization.AtPrime (Ideal.under R[X] P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R[X] P) P
⊢ False
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
⊢ ∃ a, φ₃ a = (Ideal.Quotient.mk (Ideal.map (algebraMap R Sq) p)) x

Tactic:
obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq q.primeCompl 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 s : S
hs : s ∈ q.primeCompl
⊢ ∃ a, φ₃ a = (Ideal.Quotient.mk (Ideal.map (algebraMap R Sq) p)) (IsLocalization.mk' Sq x ⟨s, hs⟩)
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
f : S
P : StandardEtalePair R
φ : P.Ring →ₐ[R] Localization.Away f
hsurj : Function.Surjective ⇑φ
g : S
a : P.Ring
ha : φ a = (algebraMap S (Localization.Away f)) g
this : IsLocalization.Away (f * g) (Localization.Away (φ a))
⊢ HasStandardEtaleSurjectionOn R (f * g)

Tactic:
have : IsStandardEtale R (Localization.Away a) := .of_isLocalizationAway a

Goal state after:
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S
P : StandardEtalePair R
φ : P.Ring →ₐ[R] Localization.Away f
hsurj : Function.Surjective ⇑φ
g : S
a : P.Ring
ha : φ a = (algebraMap S (Localization.Away f)) g
this✝ : IsLocalization.Away (f * g) (Localization.Away (φ a))
this : IsStandardEtale R (Localization.Away a)
⊢ HasStandardEtaleSurjectionOn R (f * g)
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)]) =
    (Algebra.Generators.ofAlgHom
        ((P.lift P.x ⋯).comp
          ((↑P.equivMvPolynomialQuotient.symm).comp
            (Ideal.Quotient.mkₐ R
              (Ideal.span {(Bivariate.equivMvPolynomial R) (C P.f), (Bivariate.equivMvPolynomial R) (Y * C P.g - 1)}))))
        ⋯).ker

Tactic:
by
    rw [Algebra.Generators.ker_ofAlgHom, AlgHom.toRingHom_eq_coe, AlgHom.comp_toRingHom,
      AlgHom.comp_toRingHom,
      RingHom.ker_comp_of_injective _ (by exact P.lift_bijective.injective),
      RingHom.ker_comp_of_injective _ (by exact P.equivMvPolynomialQuotient.symm.injective)]
    simp [Set.pair_comm]

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case e_f
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : φ p * t = φ r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : t' * (algebraMap S St) t = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[(algebraMap S St) (φ X)]
this✝³ : Algebra ↥R₁ ↥R₂ := R₂.algebra
this✝² : Algebra (↥R₂) St := R₂.toAlgebra
this✝¹ : Algebra (↥R₁) St := R₁.toAlgebra
this✝ : IsScalarTower (↥R₁) (↥R₂) St
this : Algebra.IsIntegral ↥R₁ ↥R₂
q : R[X][X]
hq : q.Monic
hq' : eval₂ φ.toRingHom t q = 0
⊢ (algebraMap (↥R₂) St).comp ↑(aeval ⟨(algebraMap S St) (φ X), ⋯⟩) = (algebraMap S St).comp φ.toRingHom

Tactic:
ext <;> simp [-Polynomial.algebraMap_apply, ← algebraMap_eq, ← IsScalarTower.algebraMap_apply]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
i : Fin n
⊢ (basisProd R m n) (Fin.natAdd m i) = (0, (basis R n) i)

Tactic:
basisProd_natAdd

Goal state after:
R : Type u_1
inst✝ : Semiring R
m n : ℕ
i : Fin n
⊢ (0, (basis R n) i) = (0, (basis R n) i)
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
⊢ IsLocalization.Away
    ((ConcreteCategory.hom (((toOpensFunctor Y).op.whiskerLeft (normalizationDiagramMap f)).app (Opposite.op U))) r)
    ↑(((toOpensFunctor Y).op ⋙ normalizationDiagram f).obj (Opposite.op (U.basicOpen r)))

Tactic:
let inst : Algebra Γ(X, f ⁻¹ᵁ U.1) Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
    (X.presheaf.map (homOfLE (f.preimage_mono (Y.basicOpen_le r))).op).hom.toAlgebra

Goal state after:
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
⊢ IsLocalization.Away
    ((ConcreteCategory.hom (((toOpensFunctor Y).op.whiskerLeft (normalizationDiagramMap f)).app (Opposite.op U))) r)
    ↑(((toOpensFunctor Y).op ⋙ normalizationDiagram f).obj (Opposite.op (U.basicOpen r)))
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : Algebra.IsStandardEtale R S
⊢ Function.Bijective ⇑(toIntegralClosure R S B)

Tactic:
by
  refine ⟨toIntegralClosure_injective_of_flat, ?_⟩
  intro ⟨x, hx⟩
  simp only [toIntegralClosure, Subtype.ext_iff, AlgHom.coe_codRestrict, ← AlgHom.mem_range]
  refine Algebra.adjoin_le ?_ (mem_adjoin_map_integralClosure_of_isStandardEtale x hx)
  rintro _ ⟨y, hy : IsIntegral _ _, rfl⟩
  refine ⟨1 ⊗ₜ ⟨y, hy⟩, by simp⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
this✝¹ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝ : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
⊢ ((normalizationOpenCover f).f U ≫ f₂) ⁻¹ᵁ g ⁻¹ᵁ ↑U = ⊤

Tactic:
simp only [← Scheme.Hom.comp_preimage, Category.assoc, hf₂, ι_fromNormalization]; simp

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

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
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin n) R →ₐ[R] S
⊢ (fun p ↦ aeval fun x ↦ (↑p).coeff ↑x) ((fun f ↦ (MonicDegreeEq.freeMonic R n).map f.toRingHom) f) = f

Tactic:
by ext i; simp [coeff_freeMonic]

Goal state after: