mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ Ideal.ResidueField.mapₐ p Q (ofId R S) ⋯ = AlgHom.restrictScalars R (ofId p.ResidueField Q.ResidueField)

Tactic:
ext

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

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
p : Ideal T
inst✝ : p.IsPrime
s : S
hsp : s ∉ Ideal.under S p
hs : IsIntegral R s
Hs : ∀ (x : S), ∃ m, IsIntegral R (s ^ m * x)
t : S
htp : t ∉ Ideal.under S p
Ht : ⊥.saturation (Submonoid.powers ((algebraMap S T) t)) ⋯ = ⊤
m : ℕ
hm : IsIntegral R (s ^ m * t)
x : T
n : ℕ
a : S
ha : (ofId S T).toRingHom a = (fun x ↦ (algebraMap S T) t ^ x) n * x
k : ℕ
hk : IsIntegral R (s ^ k * a)
⊢ (algebraMap S T) (s ^ (m + 1) * t) ^ (k + n) * x =
    (algebraMap S T) (s ^ ((m + 1) * n) * (s ^ m * t) ^ k * (s ^ k * a))

Tactic:
simp only [AlgHom.toRingHom_eq_coe, Algebra.toRingHom_ofId] at ha

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
p : Ideal T
inst✝ : p.IsPrime
s : S
hsp : s ∉ Ideal.under S p
hs : IsIntegral R s
Hs : ∀ (x : S), ∃ m, IsIntegral R (s ^ m * x)
t : S
htp : t ∉ Ideal.under S p
Ht : ⊥.saturation (Submonoid.powers ((algebraMap S T) t)) ⋯ = ⊤
m : ℕ
hm : IsIntegral R (s ^ m * t)
x : T
n : ℕ
a : S
ha : (algebraMap S T) a = (algebraMap S T) t ^ n * x
k : ℕ
hk : IsIntegral R (s ^ k * a)
⊢ (algebraMap S T) (s ^ (m + 1) * t) ^ (k + n) * x =
    (algebraMap S T) (s ^ ((m + 1) * n) * (s ^ m * t) ^ k * (s ^ k * a))
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
H :
  Polynomial.map (algebraMap S S') (derivative f * y %ₘ f) =
    (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum
⊢ ∃ g, φ (derivative f) * φ y = φ g ∧ ∀ (i : ℕ), IsIntegral R (g.coeff i)

Tactic:
have H' (a : S') (ham : a ∈ m) : IsIntegral R (aeval a y) := by
    let ψ : B →ₐ[R] S' := AlgHom.liftOfSurjective _ hφ ((aeval a).restrictScalars R) <| by
      rw [hfx, Ideal.span_le]
      suffices (m.map (a - ·)).prod = 0 by simpa [← eval_map_algebraMap, hm, eval_multiset_prod]
      rw [Multiset.prod_eq_zero]
      simpa using ⟨a, ham, by simp⟩
    simpa [ψ] using hy.map ψ

Goal state after:
case inr
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
H :
  Polynomial.map (algebraMap S S') (derivative f * y %ₘ f) =
    (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum
H' : ∀ a ∈ m, IsIntegral R ((aeval a) y)
⊢ ∃ g, φ (derivative f) * φ y = φ g ∧ ∀ (i : ℕ), IsIntegral R (g.coeff i)
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

Goal state after:
case e_f.h₁
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
x✝ : R
⊢ (((algebraMap (↥R₂) St).comp ↑(aeval ⟨(algebraMap S St) (φ X), ⋯⟩)).comp C) x✝ =
    (((algebraMap S St).comp φ.toRingHom).comp C) x✝

case h₂
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 := ⋯
t' : St := ⋯
ht't : t' * (algebraMap S St) t = 1
R₁ : Subalgebra R St := ⋯
R₂ : Subalgebra (↥R₁) St := ⋯
this✝³ : Algebra ↥R₁ ↥R₂ := ⋯
this✝² : Algebra (↥R₂) St := ⋯
this✝¹ : Algebra (↥R₁) St := ⋯
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), ⋯⟩)) X = ((algebraMap S St).comp φ.toRingHom) X
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)
⊢ (aeval ((algebraMap S S') (φ X))).comp (mapRingHom (algebraMap R R')) = (algebraMap S S').comp ↑φ

Tactic:
ext

Goal state after:
case h₁
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)
x✝ : R
⊢ (((aeval ((algebraMap S S') (φ X))).comp (mapRingHom (algebraMap R R'))).comp C) x✝ =
    (((algebraMap S S').comp ↑φ).comp C) x✝

case h₂
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 := ⋯
R' : Type u_1 := ⋯
S' : Type u_2 := ⋯
this✝ : Algebra R' S' := ⋯
this : IsScalarTower R R' S'
ha : IsUnit ((algebraMap R R') a)
⊢ ((aeval ((algebraMap S S') (φ X))).comp (mapRingHom (algebraMap R R'))) X = ((algebraMap S S').comp ↑φ) X
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
H :
  Polynomial.map (algebraMap S S') (derivative f * y %ₘ f) =
    (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum
H' : ∀ a ∈ m, IsIntegral R ((aeval a) y)
a : S'
ham : a ∈ m
⊢ IsIntegral R[X] (C ((aeval a) y))

Tactic:
· simpa [isIntegral_iff_isIntegral_coeff, coeff_C, apply_ite, isIntegral_zero] using H' a ham

Goal state after:
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
inst✝⁴ : FaithfulSMul R S
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
this✝⁴ : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective ⇑f
hx : IsStronglyTranscendental R (f X)
hf : aeval (f X) = f
this✝³ : Algebra R[X] S := f.toAlgebra
this✝² : IsScalarTower R R[X] S
this✝¹ : Module.Finite R[X] S
this✝ : FaithfulSMul R[X] S
this : Ideal.map C (Ideal.under R P) < Ideal.under R[X] P
Q : Ideal S
hQ : Q < P
left✝ : Q.IsPrime
e : Ideal.map C (Ideal.under R P) = Ideal.under R[X] Q
⊢ Ideal.under R (Ideal.map C (Ideal.under R P)) = Ideal.under R P

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FaithfulSMul R S
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
this✝⁴ : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective ⇑f
hx : IsStronglyTranscendental R (f X)
hf : aeval (f X) = f
this✝³ : Algebra R[X] S := f.toAlgebra
this✝² : IsScalarTower R R[X] S
this✝¹ : Module.Finite R[X] S
this✝ : FaithfulSMul R[X] S
this : Ideal.map C (Ideal.under R P) < Ideal.under R[X] P
Q : Ideal S
hQ : Q < P
left✝ : Q.IsPrime
e : Ideal.map C (Ideal.under R P) = Ideal.under R[X] Q
x✝ : R
⊢ x✝ ∈ Ideal.under R (Ideal.map C (Ideal.under R P)) ↔ x✝ ∈ Ideal.under R P
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
⊢ f = (AlgHom.restrictScalars R g).comp ((↑(TensorProduct.comm R S R')).comp (IsScalarTower.toAlgHom R S (S ⊗[R] R')))

Tactic:
ext

Goal state after:
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
x✝ : S
⊢ f x✝ =
    ((AlgHom.restrictScalars R g).comp ((↑(TensorProduct.comm R S R')).comp (IsScalarTower.toAlgHom R S (S ⊗[R] R'))))
      x✝
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
inst✝⁴ : IsReduced S
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝³ : P.IsPrime
inst✝² : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsReduced S]
    {x : S},
    (aeval x).Finite →
      ∀ (P : Ideal S) [inst_4 : P.IsPrime] [WeaklyQuasiFiniteAt R P],
        IsDomain S ∧ FaithfulSMul R S → ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : p ∈ ⊥.minimalPrimes
hpP : p ≤ P
inst✝¹ : p.IsPrime
inst✝ : (Ideal.map (Ideal.Quotient.mk p) P).IsPrime
inst : WeaklyQuasiFiniteAt (R ⧸ Ideal.under R p) (Ideal.map (Ideal.Quotient.mk p) P)
⊢ (aeval ((Ideal.Quotient.mk p) x)).comp (mapRingHom (Ideal.Quotient.mk (Ideal.under R p))) =
    (Ideal.Quotient.mk p).comp (aeval x).toRingHom

Tactic:
ext

Goal state after:
case h₁
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsReduced S
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝³ : P.IsPrime
inst✝² : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsReduced S]
    {x : S},
    (aeval x).Finite →
      ∀ (P : Ideal S) [inst_4 : P.IsPrime] [WeaklyQuasiFiniteAt R P],
        IsDomain S ∧ FaithfulSMul R S → ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : p ∈ ⊥.minimalPrimes
hpP : p ≤ P
inst✝¹ : p.IsPrime
inst✝ : (Ideal.map (Ideal.Quotient.mk p) P).IsPrime
inst : WeaklyQuasiFiniteAt (R ⧸ Ideal.under R p) (Ideal.map (Ideal.Quotient.mk p) P)
x✝ : R
⊢ (((aeval ((Ideal.Quotient.mk p) x)).comp (mapRingHom (Ideal.Quotient.mk (Ideal.under R p)))).comp C) x✝ =
    (((Ideal.Quotient.mk p).comp (aeval x).toRingHom).comp C) x✝

case h₂
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsReduced S
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝³ : P.IsPrime
inst✝² : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsReduced S]
    {x : S},
    (aeval x).Finite →
      ∀ (P : Ideal S) [inst_4 : P.IsPrime] [WeaklyQuasiFiniteAt R P],
        IsDomain S ∧ FaithfulSMul R S → ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : p ∈ ⊥.minimalPrimes
hpP : p ≤ P
inst✝¹ : p.IsPrime
inst✝ : (Ideal.map (Ideal.Quotient.mk p) P).IsPrime
inst : WeaklyQuasiFiniteAt (R ⧸ Ideal.under R p) (Ideal.map (Ideal.Quotient.mk p) P)
⊢ ((aeval ((Ideal.Quotient.mk p) x)).comp (mapRingHom (Ideal.Quotient.mk (Ideal.under R p)))) X =
    ((Ideal.Quotient.mk p).comp (aeval x).toRingHom) X
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
⊢ Submodule.comap (↑↑(taylorEquiv r)) R[X]_n = R[X]_n

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
x✝ : R[X]
⊢ x✝ ∈ Submodule.comap (↑↑(taylorEquiv r)) R[X]_n ↔ x✝ ∈ R[X]_n
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : f.natDegree = 0
⊢ f.sylvesterDeriv.updateRow ⟨2 * f.natDegree - 2, ⋯⟩ (f.leadingCoeff • f.sylvesterDeriv ⟨2 * f.natDegree - 2, ⋯⟩) =
    (derivative f).sylvester f (f.natDegree - 1) f.natDegree

Tactic:
ext ⟨i, hi⟩; lia

Goal state after:
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
inst : Algebra ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this : IsLocalization.Away ((algebraMap ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)) r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)
⊢ 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:
change IsLocalization.Away ((algebraMap Γ(Y, U.1) (integralClosure Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1))) r)
    (integralClosure Γ(Y, Y.basicOpen r) Γ(X, f ⁻¹ᵁ Y.basicOpen r))

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
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this : IsLocalization.Away ((algebraMap ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)) r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)
⊢ IsLocalization.Away ((algebraMap ↑Γ(Y, ↑U) ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U))) r)
    ↥(integralClosure ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r))
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R S : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : R[X] →ₐ[R] S), f.Finite → integralClosure R S = ⊥ → ZariskisMainProperty R p
H : ¬integralClosure R S = ⊥
inst✝ : Algebra (↥(integralClosure R S)) (Localization.AtPrime p) := OreLocalization.instAlgebra
inst : WeaklyQuasiFiniteAt (↥(integralClosure R S)) p
⊢ (aeval (f X)).comp (mapRingHom (algebraMap R ↥(integralClosure R S))) = f.toRingHom

Tactic:
ext

Goal state after:
case h₁
R S : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : R[X] →ₐ[R] S), f.Finite → integralClosure R S = ⊥ → ZariskisMainProperty R p
H : ¬integralClosure R S = ⊥
inst✝ : Algebra (↥(integralClosure R S)) (Localization.AtPrime p) := OreLocalization.instAlgebra
inst : WeaklyQuasiFiniteAt (↥(integralClosure R S)) p
x✝ : R
⊢ (((aeval (f X)).comp (mapRingHom (algebraMap R ↥(integralClosure R S)))).comp C) x✝ = (f.comp C) x✝

case h₂
R S : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
hf : f.Finite
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : R[X] →ₐ[R] S), f.Finite → integralClosure R S = ⊥ → ZariskisMainProperty R p
H : ¬integralClosure R S = ⊥
inst✝ : Algebra (↥(integralClosure R S)) (Localization.AtPrime p) := ⋯
inst : WeaklyQuasiFiniteAt (↥(integralClosure R S)) p
⊢ ((aeval (f X)).comp (mapRingHom (algebraMap R ↥(integralClosure R S)))) X = f.toRingHom X