mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hv : IsTrivialOn K v
hlt : 1 < v RatFunc.X
p : K[X]
hp : p ≠ 0
⊢ v ↑p = v RatFunc.X ^ p.natDegree

Tactic:
by
  convert! valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X .X hlt hp
  ext p
  nth_rw 1 [RatFunc.X, ← aeval_X_left_apply p (R := K)]
  exact (aeval_algebraMap_apply K⟮X⟯ X p).symm

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
σ : Type w
hσ : Finite σ
⊢ ∀ {α β : Type w} (a : α ≃ β),
    (∀ {f : MvPolynomial α S},
        (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f →
          ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)) →
      ∀ {f : MvPolynomial β S},
        (algebraMap (MvPolynomial β R) (MvPolynomial β S)).IsIntegralElem f → ∀ (n : β →₀ ℕ), IsIntegral R (coeff n f)

pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
⊢ ∀ {f : MvPolynomial PEmpty.{w + 1} S},
    (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).IsIntegralElem f →
      ∀ (n : PEmpty.{w + 1} →₀ ℕ), IsIntegral R (coeff n f)

pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
⊢ ∀ {α : Type w} [Fintype α],
    (∀ {f : MvPolynomial α S},
        (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f →
          ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)) →
      ∀ {f : MvPolynomial (Option α) S},
        (algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)).IsIntegralElem f →
          ∀ (n : Option α →₀ ℕ), IsIntegral R (coeff n f)

Tactic:
· intro α β e IH f H n
    have := @IH (rename e.symm f) (.of_map (g := (rename e).toRingHom)
      (rename_injective _ e.injective) <| .of_comp (f := (rename e.symm).toRingHom)
        (by convert H <;> aesop)) (n.embDomain e.symm)
    simpa [Finsupp.embDomain_eq_mapDomain, coeff_rename_mapDomain _ e.symm.injective] using! this

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
⊢ ∀ {f : MvPolynomial PEmpty.{w + 1} S},
    (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).IsIntegralElem f →
      ∀ (n : PEmpty.{w + 1} →₀ ℕ), IsIntegral R (coeff n f)

R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
⊢ ∀ {α : Type w} [Fintype α],
    (∀ {f : MvPolynomial α S},
        (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f →
          ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)) →
      ∀ {f : MvPolynomial (Option α) S},
        (algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)).IsIntegralElem f →
          ∀ (n : Option α →₀ ℕ), IsIntegral R (coeff n f)
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: case refine_4
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
f : R[X] →ₐ[R] S
hf : Function.Surjective ⇑f
p : Ideal R
inst✝ : p.IsPrime
⊢ (Ideal.Quotient.liftₐ (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)) (aeval (1 ⊗ₜ[R] f X))
          ⋯).comp
      (Algebra.TensorProduct.lift
        (Algebra.ofId p.ResidueField
          (p.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)))
        (f.liftOfSurjective hf
          ((Ideal.Quotient.mkₐ R (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))).comp
            (mapAlgHom (Algebra.ofId R p.ResidueField)))
          ⋯)
        ⋯) =
    AlgHom.id p.ResidueField (p.Fiber S)

Tactic:
· ext x
    obtain ⟨x, rfl⟩ := hf x
    simpa using aeval_algHom_apply
      ((Algebra.TensorProduct.includeRight : S →ₐ[_] p.Fiber S).comp f) X x

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

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
P : Ideal ↑R
hP : P.IsPrime
this : LocallyQuasiFinite (Spec.map (CommRingCat.ofHom (algebraMap P.ResidueField (P.Fiber ↑S))))
⊢ Module.Finite P.ResidueField (P.Fiber ↑S)

Tactic:
simp only [HasRingHomProperty.Spec_iff (P := @LocallyQuasiFinite), CommRingCat.hom_ofHom,
      RingHom.quasiFinite_algebraMap] at this
    exact .of_quasiFinite

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

Goal state before:
pp: 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 : K[X]
q✝ : K⟮X⟯
q r : K[X]
x✝ : r ≠ 0
⊢ (c • p) • RatFunc.mk q r = c • p • RatFunc.mk q r

Tactic:
rw [← mk_smul, smul_assoc, mk_smul, mk_smul]

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 : 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))) ⋯
this : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (φ r).toLinearMap
⊢ Function.Bijective ⇑(toIntegralClosure R S B)

Tactic:
refine bijective_of_isLocalized_span s hs (F := (toIntegralClosure R S B).toLinearMap)
    (fun r ↦ (Sᵣ r) ⊗[R] integralClosure R B)
    (fun r ↦ (Algebra.TensorProduct.map (Algebra.ofId _ _) (.id _ _)).toLinearMap)
    (fun r ↦ integralClosure (Sᵣ r) ((Sᵣ r) ⊗[R] B))
    (fun r ↦ (φ r).toLinearMap) fun r ↦ ?_

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))) ⋯
this : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (φ r).toLinearMap
r : ↑s
⊢ Function.Bijective
    ⇑((IsLocalizedModule.map (Submonoid.powers ↑r)
          (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R ↥(integralClosure R B))).toLinearMap
          (φ r).toLinearMap)
        (toIntegralClosure R S B).toLinearMap)
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 • (t * x) ∈ φ.range

Tactic:
rw [← Nat.sub_add_cancel (s.le_sup h), pow_add, mul_smul]

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
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : Module.Finite R S
inst✝ : IsUnramifiedAt R Q
this✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q'
ht : (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤
p : Ideal R := Ideal.under R Q
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this : Algebra (Localization.AtPrime (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
⊢ (Ideal.under (↥R[t]) Q).primesOver S = {Q}

pp: case refine_2
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : Module.Finite R S
inst✝ : IsUnramifiedAt R Q
this✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q'
ht : (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤
p : Ideal R := Ideal.under R Q
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this : Algebra (Localization.AtPrime (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
⊢ Function.Surjective ⇑(algebraMap (Ideal.under (↥R[t]) Q).ResidueField Q.ResidueField)

Tactic:
· refine Set.ext fun Q' ↦ ⟨fun ⟨_, _⟩ ↦ ?_, fun e ↦ by exact ⟨e ▸ inferInstance, ⟨e ▸ rfl⟩⟩⟩
    by_contra! H
    have : Q'.LiesOver p := .trans _ (Q.under (R[t])) _
    exact htQ (SetLike.le_def.mp (Q'.over_def (Q.under (R[t]))).ge
      (x := ⟨t, self_mem_adjoin_singleton _ _⟩) (htQ' Q' ⟨‹_›, ‹_›⟩ H))

Goal state after:
case refine_2
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : Module.Finite R S
inst✝ : IsUnramifiedAt R Q
this✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q'
ht : (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤
p : Ideal R := Ideal.under R Q
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this : Algebra (Localization.AtPrime (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
⊢ Function.Surjective ⇑(algebraMap (Ideal.under (↥R[t]) Q).ResidueField Q.ResidueField)
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
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : FinitePresentation R S
inst✝ : IsSmoothAt R p
f : S
hfp : f ∉ p
H✝ : IsStandardSmooth R (Localization.Away f)
n : ℕ
φ : MvPolynomial (Fin n) R →+* Localization.Away f
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg✝ : φ.Etale
algInst✝ : Algebra (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst✝ : Etale (MvPolynomial (Fin n) R) (Localization.Away f)
this✝² : IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f)
this✝¹ : (Ideal.map (algebraMap S (Localization.Away f)) p).IsPrime
g₀ : Localization.Away f
H : IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ : IsLocalization.mk' (Localization.Away f) g ⟨(fun x ↦ f ^ x) m, ⋯⟩ = g₀
hg : g ∉ p
this✝ : IsLocalization.Away (f * g) (Localization.Away g₀)
e : Localization.Away g₀ ≃ₐ[S] Localization.Away (f * g) :=
  IsLocalization.algEquiv (Submonoid.powers (f * g)) (Localization.Away g₀) (Localization.Away (f * g))
this : Algebra (MvPolynomial (Fin n) R) (Localization.Away (f * g)) :=
  (e.toRingEquiv.toRingHom.comp (algebraMap (MvPolynomial (Fin n) R) (Localization.Away g₀))).toAlgebra
⊢ IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away (f * g))

Tactic:
refine .of_algebraMap_eq' ?_

Goal state after:
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : FinitePresentation R S
inst✝ : IsSmoothAt R p
f : S
hfp : f ∉ p
H✝ : IsStandardSmooth R (Localization.Away f)
n : ℕ
φ : MvPolynomial (Fin n) R →+* Localization.Away f
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg✝ : φ.Etale
algInst✝ : Algebra (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst✝ : Etale (MvPolynomial (Fin n) R) (Localization.Away f)
this✝² : IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f)
this✝¹ : (Ideal.map (algebraMap S (Localization.Away f)) p).IsPrime
g₀ : Localization.Away f
H : IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ : IsLocalization.mk' (Localization.Away f) g ⟨(fun x ↦ f ^ x) m, ⋯⟩ = g₀
hg : g ∉ p
this✝ : IsLocalization.Away (f * g) (Localization.Away g₀)
e : Localization.Away g₀ ≃ₐ[S] Localization.Away (f * g) :=
  IsLocalization.algEquiv (Submonoid.powers (f * g)) (Localization.Away g₀) (Localization.Away (f * g))
this : Algebra (MvPolynomial (Fin n) R) (Localization.Away (f * g)) :=
  (e.toRingEquiv.toRingHom.comp (algebraMap (MvPolynomial (Fin n) R) (Localization.Away g₀))).toAlgebra
⊢ algebraMap R (Localization.Away (f * g)) =
    (algebraMap (MvPolynomial (Fin n) R) (Localization.Away (f * g))).comp (algebraMap R (MvPolynomial (Fin n) R))
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
K : Type u_4
L : Type u_5
inst✝²⁵ : Field K
inst✝²⁴ : Field L
inst✝²³ : Algebra R K
inst✝²² : Algebra R L
inst✝²¹ : Algebra S L
inst✝²⁰ : Algebra K L
inst✝¹⁹ : IsScalarTower R K L
inst✝¹⁸ : IsScalarTower R S L
inst✝¹⁷ : IsFractionRing R K
inst✝¹⁶ : IsFractionRing S L
R' : Type u_6
S' : Type u_7
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' S'
inst✝¹¹ : Algebra R S'
inst✝¹⁰ : Algebra S' L
inst✝⁹ : Algebra R' L
inst✝⁸ : IsScalarTower R' S' L
inst✝⁷ : Algebra R' K
inst✝⁶ : IsScalarTower R' K L
inst✝⁵ : IsScalarTower R R' S'
inst✝⁴ : FaithfulSMul S' L
inst✝³ : IsIntegralClosure R' R K
inst✝² : IsScalarTower R R' K
f : S →ₐ[R] S'
hf₁ : Function.Surjective ⇑(TensorProduct.lift (ofId R' S') f ⋯)
hf₂ : (algebraMap S' L).comp f.toRingHom = algebraMap S L
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this✝⁷ : IsDomain S'
this✝⁶ : IsDomain R
this✝⁵ : Algebra.IsIntegral R R'
this✝⁴ : FaithfulSMul R' K
this✝³ : FaithfulSMul R R'
this✝² : FaithfulSMul R' L
this✝¹ : FaithfulSMul R' S'
this✝ : IsIntegrallyClosedIn R' K
this : IsIntegrallyClosed R'
g : R' ⊗[R] S →ₐ[R'] S' := TensorProduct.lift (ofId R' S') f ⋯
hf₃ : Function.Injective ⇑f
hf₄ : f.IsIntegral
H₁ : IsStronglyTranscendental R' (f x)
H₂ : (aeval (f x)).Finite
Q : Ideal S'
isPrime✝ : Q.IsPrime
hQ : PrimeSpectrum.comap f.toRingHom { asIdeal := Q, isPrime := isPrime✝ } = { asIdeal := P, isPrime := inst✝¹ }
⊢ P = Ideal.comap TensorProduct.includeRight.toRingHom (Ideal.comap g.toRingHom Q)

Tactic:
by
    rw [Ideal.comap_comap]
    convert! congr(($hQ.symm).1)
    ext; simp [g]

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

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
a✝ : Nontrivial R
i : Fin n
⊢ (LinearMap.toMatrix (degreeLT.basis R n) (degreeLT.basis R n)) (↑(taylorLinearEquiv r n)) i i = 1

Tactic:
rw [LinearMap.toMatrix_apply, degreeLT.basis_repr, ← natDegree_X_pow (R := R) (i : ℕ)]

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
a✝ : Nontrivial R
i : Fin n
⊢ (↑(↑(taylorLinearEquiv r n) ((degreeLT.basis R n) i))).coeff (X ^ ↑i).natDegree = 1
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
⊢ IsIntegralHom (fromNormalization f)

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsIntegralHom) _
    (iSup_affineOpens_eq_top _)]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
⊢ ∀ (i : ↑Y.affineOpens), IsIntegralHom (fromNormalization f ∣_ ↑i)
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case e'_3
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
this : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
H :
  toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U =
    (f ⁻¹ᵁ ↑U).ι ''ᵁ ((f ⁻¹ᵁ ↑U).ι ≫ toNormalization f) ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U
⊢ (normalization f).presheaf.map (eqToHom ⋯).op ≫
      (appIso ((normalizationOpenCover f).f U) ⊤).hom ≫
        (ΓSpecIso ((normalizationDiagram f).obj (Opposite.op ((toOpensFunctor Y).obj U)))).hom ≫
          CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val ≫ X.presheaf.map (eqToHom ⋯).op =
    (((app ((normalizationOpenCover f).f U) (fromNormalization f ⁻¹ᵁ ↑U) ≫
            app (Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val))
              ((normalizationOpenCover f).f U ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U)) ≫
          app (f ⁻¹ᵁ ↑U).toSpecΓ
            ((TopologicalSpace.Opens.map
                  (Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val)).base).obj
              ((TopologicalSpace.Opens.map ((normalizationOpenCover f).f U).base).obj (fromNormalization f ⁻¹ᵁ ↑U)))) ≫
        X.presheaf.map ((opensFunctor (f ⁻¹ᵁ ↑U).ι).map (eqToHom ⋯)).op) ≫
      X.presheaf.map (eqToHom H).op

Tactic:
simp only [eqToHom_op, Hom.appIso_hom, Category.assoc, Scheme.Hom.naturality_assoc, eqToHom_unop,
    ← Functor.map_comp_assoc, eqToHom_map (TopologicalSpace.Opens.map _), eqToHom_trans]

Goal state after:
case e'_3
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
this : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
H :
  toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U =
    (f ⁻¹ᵁ ↑U).ι ''ᵁ ((f ⁻¹ᵁ ↑U).ι ≫ toNormalization f) ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U
⊢ app ((normalizationOpenCover f).f U) (fromNormalization f ⁻¹ᵁ ↑U) ≫
      ((normalizationOpenCover f).X U).presheaf.map (eqToHom ⋯) ≫
        (ΓSpecIso ((normalizationDiagram f).obj (Opposite.op ((toOpensFunctor Y).obj U)))).hom ≫
          CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val ≫ X.presheaf.map (eqToHom ⋯) =
    app ((normalizationOpenCover f).f U) (fromNormalization f ⁻¹ᵁ ↑U) ≫
      app (Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val))
          ((normalizationOpenCover f).f U ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U) ≫
        app (f ⁻¹ᵁ ↑U).toSpecΓ
            ((TopologicalSpace.Opens.map
                  (Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val)).base).obj
              ((TopologicalSpace.Opens.map ((normalizationOpenCover f).f U).base).obj (fromNormalization f ⁻¹ᵁ ↑U))) ≫
          X.presheaf.map ((opensFunctor (f ⁻¹ᵁ ↑U).ι).map (eqToHom ⋯)).op ≫ X.presheaf.map (eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst✝ : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
⊢ Spec.map
        (appLE f₂ (↑U) (f₂ ⁻¹ᵁ ↑U) ⋯ ≫
          CommRingCat.ofHom
            ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ ↑U) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
              (integralClosure ↑Γ(Y, toOpens U) ↑Γ(X, f ⁻¹ᵁ toOpens U)) ⋯)) ≫
      ⋯.fromSpec =
    (Spec.map ((normalizationDiagramMap f).app (Opposite.op (toOpens U))) ≫ ⋯.isoSpec.inv) ≫ (↑U).ι

Tactic:
rw [Category.assoc]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst✝ : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
⊢ Spec.map
        (appLE f₂ (↑U) (f₂ ⁻¹ᵁ ↑U) ⋯ ≫
          CommRingCat.ofHom
            ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ ↑U) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
              (integralClosure ↑Γ(Y, toOpens U) ↑Γ(X, f ⁻¹ᵁ toOpens U)) ⋯)) ≫
      ⋯.fromSpec =
    Spec.map ((normalizationDiagramMap f).app (Opposite.op (toOpens U))) ≫ ⋯.isoSpec.inv ≫ (↑U).ι