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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
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
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
x : ((localizationAway T g).comp P).toExtension.Cotangent
hx : (Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom) x = cMulXSubOneCotangent T g
⊢ Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom ∘ₗ cotangentCompAwaySec g P x = LinearMap.id

Tactic:
refine (basisCotangentAway T g).ext fun r ↦ ?_

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
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
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
x : ((localizationAway T g).comp P).toExtension.Cotangent
hx : (Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom) x = cMulXSubOneCotangent T g
r : Unit
⊢ (Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom ∘ₗ cotangentCompAwaySec g P x)
      ((basisCotangentAway T g) r) =
    LinearMap.id ((basisCotangentAway T g) r)
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
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
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
x : ((localizationAway T g).comp P).toExtension.Cotangent
hx : (Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom) x = cMulXSubOneCotangent T g
a : ((localizationAway T g).comp P).toExtension.Cotangent
⊢ ((cotangentCompLocalizationAwayEquiv g P hx) a).2 =
    (Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom) a

Tactic:
by
  simp [← snd_comp_cotangentCompLocalizationAwayEquiv g P hx]

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: ⊢ RespectsIso @IsStandardSmooth

Tactic:
apply isStandardSmooth_stableUnderComposition.respectsIso
  introv
  exact (IsStandardSmoothOfRelativeDimension.equiv e).isStandardSmooth

Goal state after:
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
D : DescentAux A B
i : D.vars
⊢ ↑(D.q i).coeffs ⊆ Set.range ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))

Tactic:
intro q

Goal state after:
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
D : DescentAux A B
i : D.vars
q : MvPolynomial D.vars A
⊢ q ∈ ↑(D.q i).coeffs → q ∈ Set.range ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -3 * P x ^ 2 * Q x * Q y + 3 * P x * Q x ^ 2 * P y - P y ^ 2 * Q y * 0 + P y * Q y ^ 2 * P z +
                                W'.a₁ * P x * Q y ^ 2 * P z -
                              W'.a₁ * Q x * P y ^ 2 * 0 -
                            W'.a₂ * P x ^ 2 * Q y * 0 +
                          W'.a₂ * Q x ^ 2 * P y * P z +
                        2 * W'.a₂ * P x * Q x * P y * 0 -
                      2 * W'.a₂ * P x * Q x * Q y * P z -
                    W'.a₃ * P y ^ 2 * 0 ^ 2 +
                  W'.a₃ * Q y ^ 2 * P z ^ 2 +
                W'.a₄ * P x * P y * 0 ^ 2 -
              2 * W'.a₄ * P x * Q y * P z * 0 +
            2 * W'.a₄ * Q x * P y * P z * 0 -
          W'.a₄ * Q x * Q y * P z ^ 2 +
        3 * W'.a₆ * P y * P z * 0 ^ 2 -
      3 * W'.a₆ * Q y * P z ^ 2 * 0 =
    -(Q y ^ 2 * P z) * W'.negY P

Tactic:
X_eq_zero_of_Z_eq_zero hQ hQz,

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -3 * P x ^ 2 * 0 * Q y + 3 * P x * 0 ^ 2 * P y - P y ^ 2 * Q y * 0 + P y * Q y ^ 2 * P z +
                                W'.a₁ * P x * Q y ^ 2 * P z -
                              W'.a₁ * 0 * P y ^ 2 * 0 -
                            W'.a₂ * P x ^ 2 * Q y * 0 +
                          W'.a₂ * 0 ^ 2 * P y * P z +
                        2 * W'.a₂ * P x * 0 * P y * 0 -
                      2 * W'.a₂ * P x * 0 * Q y * P z -
                    W'.a₃ * P y ^ 2 * 0 ^ 2 +
                  W'.a₃ * Q y ^ 2 * P z ^ 2 +
                W'.a₄ * P x * P y * 0 ^ 2 -
              2 * W'.a₄ * P x * Q y * P z * 0 +
            2 * W'.a₄ * 0 * P y * P z * 0 -
          W'.a₄ * 0 * Q y * P z ^ 2 +
        3 * W'.a₆ * P y * P z * 0 ^ 2 -
      3 * W'.a₆ * Q y * P z ^ 2 * 0 =
    -(Q y ^ 2 * P z) * W'.negY P
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this : CompactSpace ↥X
⊢ UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))

Tactic:
rwa [← Scheme.toSpecΓ_naturality,
      MorphismProperty.cancel_right_of_respectsIso (P := @UniversallyClosed)]

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
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hFa : (aeval a) F = 0
i : ι
hi : i ∈ F.vars
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hσi : i ∈ σ.support
⊢ IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)

Tactic:
refine ⟨toPolynomialAdjoinImageCompl F a i,
    fun h ↦ coeff_toPolynomialAdjoinImageCompl_ne_zero HF σ hσ i
      (Finsupp.mem_support_iff.mp hσi) ?_, aeval_toPolynomialAdjoinImageCompl_eq_zero hFa ..⟩

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hFa : (aeval a) F = 0
i : ι
hi : i ∈ F.vars
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hσi : i ∈ σ.support
h : F.toPolynomialAdjoinImageCompl a i = 0
⊢ (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
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
⊢ ¬LinearIndependent k fun x ↦ (aeval a) ((monomial (σ' ↑x)) 1) ^ p

Tactic:
simp_rw [← map_pow, monomial_pow, ← hσ'', one_pow, not_linearIndependent_iff]

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
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
⊢ ∃ s g, ∑ i ∈ s, g i • (aeval a) ((monomial ↑i) 1) = 0 ∧ ∃ i ∈ s, g i ≠ 0
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X✝ : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
X : Scheme
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
H : CompactSpace ↥X
this : IsNoetherian X
x : ↥X
U : X.Opens := { carrier := (⋃₀ (irreducibleComponents ↥X \ {irreducibleComponent x}))ᶜ, is_open' := ⋯ }
⊢ x ∈ closure ↑(smoothLocus f)

Tactic:
have hU : closure U = irreducibleComponent x :=
    closure_sUnion_irreducibleComponents_sdiff_singleton
      TopologicalSpace.NoetherianSpace.finite_irreducibleComponents
      _ (irreducibleComponent_mem_irreducibleComponents x)

Goal state after:
X✝ : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
X : Scheme
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
H : CompactSpace ↥X
this : IsNoetherian X
x : ↥X
U : X.Opens := { carrier := (⋃₀ (irreducibleComponents ↥X \ {irreducibleComponent x}))ᶜ, is_open' := ⋯ }
hU : closure ↑U = irreducibleComponent x
⊢ x ∈ closure ↑(smoothLocus f)
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:
refine ⟨fun {X Y Z} f g ⟨𝒰, hf⟩ ⟨𝒱, hg⟩ ↦ ?_⟩

Goal state after:
W P Q : MorphismProperty Scheme
X✝ Y✝ : Scheme
inst✝⁴ : W.IsStableUnderBaseChange
inst✝³ : Scheme.IsJointlySurjectivePreserving W
inst✝² : W.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.IsStableUnderComposition
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
x✝¹ : sourceLocalClosure W P f
x✝ : sourceLocalClosure W P g
𝒰 : Scheme.Cover (Scheme.precoverage W) X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
𝒱 : Scheme.Cover (Scheme.precoverage W) Y
hg : ∀ (i : 𝒱.I₀), P (𝒱.f i ≫ g)
⊢ sourceLocalClosure W P (f ≫ g)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: case h₂
P : MorphismProperty Scheme
inst✝¹ : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦
    RingHom.FaithfullyFlat
⊢ @IsLocalIso ≤ @Flat

Tactic:
exact IsLocalIso.le_of_isZariskiLocalAtSource @Flat

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
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 + i) • s ^ i ∈ (algebraMap R S).range

Tactic:
pow_add,

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 ^ i) • s ^ i ∈ (algebraMap R S).range
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral

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

Tactic:
pow_add,

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

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

Tactic:
← mk_coe_def,

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p : K[X]
⊢ RatFunc.mk p 1 = RatFunc.mk p ↑1
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
⊢ ¬IsAlgebraic A y⁻¹

Tactic:
apply this _ (by simpa) (by simpa)

Goal state after:
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
⊢ 1 < v y⁻¹
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: 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
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯ ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
x✝ : I.ResidueField[X]
x : I.ResidueField[X]
hx : (aeval ((algebraMap R[X] J.ResidueField) X)) x = 0
r : R[X]
hr : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x
s : R
hb0 : (Ideal.Quotient.mk I) s ∈ (R ⧸ I)⁰
hb :
  map (algebraMap (R ⧸ I) I.ResidueField) (IsLocalization.integerNormalization (R ⧸ I)⁰ x) = (Ideal.Quotient.mk I) s • x
⊢ map (algebraMap R I.ResidueField) r = s • x

Tactic:
simpa [← hr, map_map, ← Ideal.Quotient.algebraMap_eq] using! hb

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

Goal state before:
pp: K : Type u
inst✝ : CommRing K
x : K⟮X⟯
r : K
⊢ r • x = Polynomial.C r • x

Tactic:
by
  obtain ⟨x⟩ := x
  induction x using Localization.induction_on
  rw [← ofFractionRing_smul, ← ofFractionRing_smul, Localization.smul_mk,
    Localization.smul_mk, smul_eq_mul, Polynomial.smul_eq_C_mul]

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

Goal state before:
pp: case neg
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass R (FractionRing K[X]) := inferInstance
hq : ¬q = 0
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q

Tactic:
rw [mk_eq_localization_mk _ hq, mk_eq_localization_mk _ hq, ← Localization.smul_mk, ←
      ofFractionRing_smul]

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

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

Tactic:
e.toAlgHom.comp_algebraMap.symm

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : StandardEtalePair R
this : aeval P.X = (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1})).comp CAlgHom
⊢ (aeval P.X) P.g * (Ideal.Quotient.mk (Ideal.span {C P.f, Y * C P.g - 1})) Y = 1

Tactic:
rw [this]

Goal state after:
R : Type u_1
inst✝ : CommRing R
P : StandardEtalePair R
this : aeval P.X = (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1})).comp CAlgHom
⊢ ((Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1})).comp CAlgHom) P.g *
      (Ideal.Quotient.mk (Ideal.span {C P.f, Y * C P.g - 1})) Y =
    1
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 : Set S
hs : Ideal.span s = ⊤
Sᵣ : ↑s → Type u_4
inst✝⁴ : (r : ↑s) → CommRing (Sᵣ r)
inst✝³ : (r : ↑s) → Algebra S (Sᵣ r)
inst✝² : (r : ↑s) → Algebra R (Sᵣ r)
inst✝¹ : ∀ (r : ↑s), IsScalarTower R S (Sᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Sᵣ r)
H : ∀ (r : ↑s), Function.Bijective ⇑(toIntegralClosure R (Sᵣ r) B)
this✝² :
  ∀ (r : ↑s),
    IsLocalizedModule.Away (↑r)
      (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R ↥(integralClosure R B))).toLinearMap
φ : (r : ↑s) → ↥(integralClosure S (S ⊗[R] B)) →ₐ[S] ↥(integralClosure (Sᵣ r) (Sᵣ r ⊗[R] B)) :=
  fun r ↦
    ((Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R B)).comp
          (integralClosure S (S ⊗[R] B)).val).codRestrict
      (Subalgebra.restrictScalars S (integralClosure (Sᵣ r) (Sᵣ r ⊗[R] B))) ⋯
r : ↑s
this✝¹ : Algebra (S ⊗[R] B) (Sᵣ r ⊗[R] B) :=
  (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R B)).toAlgebra
this✝ : Algebra ↥(integralClosure S (S ⊗[R] B)) ↥(integralClosure (Sᵣ r) (Sᵣ r ⊗[R] B)) := (φ r).toAlgebra
this : IsScalarTower (↥(integralClosure S (S ⊗[R] B))) (↥(integralClosure (Sᵣ r) (Sᵣ r ⊗[R] B))) (Sᵣ r ⊗[R] B)
⊢ IsLocalizedModule.Away (↑r) (φ r).toLinearMap

Tactic:
have : IsLocalization (Algebra.algebraMapSubmonoid (S ⊗[R] B) (Submonoid.powers r.1))
        (Sᵣ r ⊗[R] B) := by
      refine IsLocalization.tensorProduct_tensorProduct _ _ (.powers r.1) _ ?_
      ext; simp [RingHom.algebraMap_toAlgebra]

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 : Set S
hs : Ideal.span s = ⊤
Sᵣ : ↑s → Type u_4
inst✝⁴ : (r : ↑s) → CommRing (Sᵣ r)
inst✝³ : (r : ↑s) → Algebra S (Sᵣ r)
inst✝² : (r : ↑s) → Algebra R (Sᵣ r)
inst✝¹ : ∀ (r : ↑s), IsScalarTower R S (Sᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Sᵣ r)
H : ∀ (r : ↑s), Function.Bijective ⇑(toIntegralClosure R (Sᵣ r) B)
this✝³ :
  ∀ (r : ↑s),
    IsLocalizedModule.Away (↑r)
      (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R ↥(integralClosure R B))).toLinearMap
φ : (r : ↑s) → ↥(integralClosure S (S ⊗[R] B)) →ₐ[S] ↥(integralClosure (Sᵣ r) (Sᵣ r ⊗[R] B)) :=
  fun r ↦
    ((Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R B)).comp
          (integralClosure S (S ⊗[R] B)).val).codRestrict
      (Subalgebra.restrictScalars S (integralClosure (Sᵣ r) (Sᵣ r ⊗[R] B))) ⋯
r : ↑s
this✝² : Algebra (S ⊗[R] B) (Sᵣ r ⊗[R] B) :=
  (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R B)).toAlgebra
this✝¹ : Algebra ↥(integralClosure S (S ⊗[R] B)) ↥(integralClosure (Sᵣ r) (Sᵣ r ⊗[R] B)) := (φ r).toAlgebra
this✝ : IsScalarTower (↥(integralClosure S (S ⊗[R] B))) (↥(integralClosure (Sᵣ r) (Sᵣ r ⊗[R] B))) (Sᵣ r ⊗[R] B)
this : IsLocalization (Algebra.algebraMapSubmonoid (S ⊗[R] B) (Submonoid.powers ↑r)) (Sᵣ r ⊗[R] B)
⊢ IsLocalizedModule.Away (↑r) (φ r).toLinearMap
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_4
x : MvPolynomial σ R ⊗[R] B
hx : x ∈ integralClosure (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] B)
e₀ : MvPolynomial σ R ⊗[R] B ≃ₐ[R] MvPolynomial σ B :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) B).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R B))
e₁ : MvPolynomial σ R ⊗[R] ↥(integralClosure R B) ≃ₐ[R] MvPolynomial σ ↥(integralClosure R B) :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) ↥(integralClosure R B)).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R ↥(integralClosure R B)))
e : MvPolynomial σ R ⊗[R] B ≃ₐ[MvPolynomial σ R] MvPolynomial σ B :=
  let __RingEquiv := e₀.toRingEquiv;
  { toEquiv := __RingEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
this : ∀ (n : σ →₀ ℕ), IsIntegral R (MvPolynomial.coeff n (e x))
⊢ ↑(e x).coeffs ⊆ Set.range ⇑(integralClosure R B).val.toRingHom

Tactic:
simp [Set.subset_def, mem_integralClosure_iff, MvPolynomial.mem_coeffs_iff,
      @forall_comm B, this]

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case mem
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]
hRS : integralClosure R S = ⊥
hφ : φ.Finite
hp : φ p * t ∈ conductor R (φ X)
algInst✝ : Algebra R[X] S := φ.toAlgebra
algebraizeInst✝ : Module.Finite R[X] S
this : IsScalarTower R R[X] S
n : S → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Submodule.span R[X] ↑s = ⊤
x✝ x : S
h : x ∈ ↑s
⊢ p.leadingCoeff ^ (s.sup n - n x + n x) • (t * x) ∈ φ.range

Tactic:
pow_add,

Goal state after:
case mem
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]
hRS : integralClosure R S = ⊥
hφ : φ.Finite
hp : φ p * t ∈ conductor R (φ X)
algInst✝ : Algebra R[X] S := φ.toAlgebra
algebraizeInst✝ : Module.Finite R[X] S
this : IsScalarTower R R[X] S
n : S → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Submodule.span R[X] ↑s = ⊤
x✝ x : S
h : x ∈ ↑s
⊢ (p.leadingCoeff ^ (s.sup n - n x) * p.leadingCoeff ^ n x) • (t * x) ∈ φ.range