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

Goal state before:
pp: case pos.inl
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x * y).denom = 0
this : Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom = 0
h✝ : Polynomial.eval₂ f a x.denom = 0
⊢ Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
      (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)

pp: case pos.inr
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x * y).denom = 0
this : Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom = 0
h✝ : Polynomial.eval₂ f a y.denom = 0
⊢ Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
      (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)

Tactic:
<;>

Goal state after:
case pos.inl
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x * y).denom = 0
this : Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom = 0
h✝ : Polynomial.eval₂ f a x.denom = 0
⊢ Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
      (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)

case pos.inr
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x * y).denom = 0
this : Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom = 0
h✝ : Polynomial.eval₂ f a y.denom = 0
⊢ Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
      (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)
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
⊢ (algEquivOfTranscendental f h).symm (AdjoinSimple.gen K f) = X

Tactic:
simp [algEquivOfTranscendental, ← algebraMap_eq_gen_self]

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

Goal state before:
pp: case e'_5
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
α β : Type w
e : α ≃ β
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial β S
H : (algebraMap (MvPolynomial β R) (MvPolynomial β S)).IsIntegralElem f
n : β →₀ ℕ
⊢ ((rename ⇑e).comp (algebraMap (MvPolynomial α R) (MvPolynomial α S))).comp (rename ⇑e.symm).toRingHom =
    algebraMap (MvPolynomial β R) (MvPolynomial β S)

pp: case e'_6
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
α β : Type w
e : α ≃ β
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial β S
H : (algebraMap (MvPolynomial β R) (MvPolynomial β S)).IsIntegralElem f
n : β →₀ ℕ
⊢ (rename ⇑e).toRingHom ((rename ⇑e.symm) f) = f

Tactic:
<;>

Goal state after:
case e'_5
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
α β : Type w
e : α ≃ β
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial β S
H : (algebraMap (MvPolynomial β R) (MvPolynomial β S)).IsIntegralElem f
n : β →₀ ℕ
⊢ ((rename ⇑e).comp (algebraMap (MvPolynomial α R) (MvPolynomial α S))).comp (rename ⇑e.symm).toRingHom =
    algebraMap (MvPolynomial β R) (MvPolynomial β S)

case e'_6
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
α β : Type w
e : α ≃ β
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial β S
H : (algebraMap (MvPolynomial β R) (MvPolynomial β S)).IsIntegralElem f
n : β →₀ ℕ
⊢ (rename ⇑e).toRingHom ((rename ⇑e.symm) f) = f
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
hs : s ∉ I
hr : map (algebraMap R I.ResidueField) r = s • x
⊢ r ∈ J

Tactic:
apply_fun aeval (algebraMap R[X] J.ResidueField X) at hr

Goal state after:
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
hs : s ∉ I
hr :
  (aeval ((algebraMap R[X] J.ResidueField) X)) (map (algebraMap R I.ResidueField) r) =
    (aeval ((algebraMap R[X] J.ResidueField) X)) (s • x)
⊢ r ∈ J
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: case e'_5.hC
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
H : (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).IsIntegralElem f
n : PEmpty.{w + 1} →₀ ℕ
r : R
m : PEmpty.{w + 1} →₀ ℕ
⊢ coeff m
      (((((isEmptyAlgEquiv S PEmpty.{w + 1}).symm.toRingEquiv.toRingHom.comp (algebraMap R S)).comp
              (isEmptyAlgEquiv R PEmpty.{w + 1}).toRingEquiv.toRingHom).comp
          C)
        r) =
    coeff m (((algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).comp C) r)

pp: case e'_5.hX
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
H : (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).IsIntegralElem f
n : PEmpty.{w + 1} →₀ ℕ
r : PEmpty.{w + 1}
m : PEmpty.{w + 1} →₀ ℕ
⊢ coeff m
      ((((isEmptyAlgEquiv S PEmpty.{w + 1}).symm.toRingEquiv.toRingHom.comp (algebraMap R S)).comp
          (isEmptyAlgEquiv R PEmpty.{w + 1}).toRingEquiv.toRingHom)
        (X r)) =
    coeff m ((algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)) (X r))

Tactic:
<;>

Goal state after:
case e'_5.hC
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
H : (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).IsIntegralElem f
n : PEmpty.{w + 1} →₀ ℕ
r : R
m : PEmpty.{w + 1} →₀ ℕ
⊢ coeff m
      (((((isEmptyAlgEquiv S PEmpty.{w + 1}).symm.toRingEquiv.toRingHom.comp (algebraMap R S)).comp
              (isEmptyAlgEquiv R PEmpty.{w + 1}).toRingEquiv.toRingHom).comp
          C)
        r) =
    coeff m (((algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).comp C) r)

case e'_5.hX
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
H : (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).IsIntegralElem f
n : PEmpty.{w + 1} →₀ ℕ
r : PEmpty.{w + 1}
m : PEmpty.{w + 1} →₀ ℕ
⊢ coeff m
      ((((isEmptyAlgEquiv S PEmpty.{w + 1}).symm.toRingEquiv.toRingHom.comp (algebraMap R S)).comp
          (isEmptyAlgEquiv R PEmpty.{w + 1}).toRingEquiv.toRingHom)
        (X r)) =
    coeff m ((algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)) (X r))
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case inr.hb
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
f : R⟮X⟯
p q p' q' : R[X]
hq : q ∈ R[X]⁰
hq' : q' ∈ R[X]⁰
h : q' * p = q * p'
h✝ : Nontrivial R
⊢ φ q ≠ 0

pp: case inr.hd
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
f : R⟮X⟯
p q p' q' : R[X]
hq : q ∈ R[X]⁰
hq' : q' ∈ R[X]⁰
h : q' * p = q * p'
h✝ : Nontrivial R
⊢ φ q' ≠ 0

Tactic:
<;>

Goal state after:
case inr.hb
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
f : R⟮X⟯
p q p' q' : R[X]
hq : q ∈ R[X]⁰
hq' : q' ∈ R[X]⁰
h : q' * p = q * p'
h✝ : Nontrivial R
⊢ φ q ≠ 0

case inr.hd
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
f : R⟮X⟯
p q p' q' : R[X]
hq : q ∈ R[X]⁰
hq' : q' ∈ R[X]⁰
h : q' * p = q * p'
h✝ : Nontrivial R
⊢ φ q' ≠ 0
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case left
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ C ((q.leadingCoeff / (a.leadingCoeff⁻¹ * (gcd p q).leadingCoeff))⁻¹ * a.leadingCoeff⁻¹⁻¹) * (p / gcd p q) =
    C (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹ * (p / gcd p q)

pp: case right
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ C ((q.leadingCoeff / (a.leadingCoeff⁻¹ * (gcd p q).leadingCoeff))⁻¹ * a.leadingCoeff⁻¹⁻¹) * (q / gcd p q) =
    C (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹ * (q / gcd p q)

Tactic:
<;>

Goal state after:
case left
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ C ((q.leadingCoeff / (a.leadingCoeff⁻¹ * (gcd p q).leadingCoeff))⁻¹ * a.leadingCoeff⁻¹⁻¹) * (p / gcd p q) =
    C (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹ * (p / gcd p q)

case right
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ C ((q.leadingCoeff / (a.leadingCoeff⁻¹ * (gcd p q).leadingCoeff))⁻¹ * a.leadingCoeff⁻¹⁻¹) * (q / gcd p q) =
    C (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹ * (q / gcd p q)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case left.e_a.e_6
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ (q.leadingCoeff / (a.leadingCoeff⁻¹ * (gcd p q).leadingCoeff))⁻¹ * a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹

pp: case right.e_a.e_6
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ (q.leadingCoeff / (a.leadingCoeff⁻¹ * (gcd p q).leadingCoeff))⁻¹ * a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹

Tactic:
<;>

Goal state after:
case left.e_a.e_6
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ (q.leadingCoeff / (a.leadingCoeff⁻¹ * (gcd p q).leadingCoeff))⁻¹ * a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹

case right.e_a.e_6
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ (q.leadingCoeff / (a.leadingCoeff⁻¹ * (gcd p q).leadingCoeff))⁻¹ * a.leadingCoeff⁻¹⁻¹ =
    (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case e'_2
K : Type u
inst✝ : Field K
⊢ 0 = (algebraMap K[X] K⟮X⟯) 0 / (algebraMap K[X] K⟮X⟯) 1

pp: case e'_3
K : Type u
inst✝ : Field K
⊢ 0 = C (1 / gcd 0 1).leadingCoeff⁻¹ * (0 / gcd 0 1)

Tactic:
<;>

Goal state after:
case e'_2
K : Type u
inst✝ : Field K
⊢ 0 = (algebraMap K[X] K⟮X⟯) 0 / (algebraMap K[X] K⟮X⟯) 1

case e'_3
K : Type u
inst✝ : Field K
⊢ 0 = C (1 / gcd 0 1).leadingCoeff⁻¹ * (0 / gcd 0 1)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case e'_2
K : Type u
inst✝ : Field K
⊢ 1 = (algebraMap K[X] K⟮X⟯) 1 / (algebraMap K[X] K⟮X⟯) 1

pp: case e'_3
K : Type u
inst✝ : Field K
⊢ 1 = C (1 / gcd 1 1).leadingCoeff⁻¹ * (1 / gcd 1 1)

Tactic:
<;>

Goal state after:
case e'_2
K : Type u
inst✝ : Field K
⊢ 1 = (algebraMap K[X] K⟮X⟯) 1 / (algebraMap K[X] K⟮X⟯) 1

case e'_3
K : Type u
inst✝ : Field K
⊢ 1 = C (1 / gcd 1 1).leadingCoeff⁻¹ * (1 / gcd 1 1)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case e'_2
K : Type u
inst✝ : Field K
p : K[X]
⊢ (algebraMap K[X] K⟮X⟯) p = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) 1

pp: case e'_3
K : Type u
inst✝ : Field K
p : K[X]
⊢ p = C (1 / gcd p 1).leadingCoeff⁻¹ * (p / gcd p 1)

Tactic:
<;>

Goal state after:
case e'_2
K : Type u
inst✝ : Field K
p : K[X]
⊢ (algebraMap K[X] K⟮X⟯) p = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) 1

case e'_3
K : Type u
inst✝ : Field K
p : K[X]
⊢ p = C (1 / gcd p 1).leadingCoeff⁻¹ * (p / gcd p 1)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case e'_2
K : Type u
inst✝ : Field K
⊢ 0 = (algebraMap K[X] K⟮X⟯) 0 / (algebraMap K[X] K⟮X⟯) 1

pp: case e'_3
K : Type u
inst✝ : Field K
⊢ 1 = C (1 / gcd 0 1).leadingCoeff⁻¹ * (1 / gcd 0 1)

Tactic:
<;>

Goal state after:
case e'_2
K : Type u
inst✝ : Field K
⊢ 0 = (algebraMap K[X] K⟮X⟯) 0 / (algebraMap K[X] K⟮X⟯) 1

case e'_3
K : Type u
inst✝ : Field K
⊢ 1 = C (1 / gcd 0 1).leadingCoeff⁻¹ * (1 / gcd 0 1)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case e'_2
K : Type u
inst✝ : Field K
p : K[X]
⊢ (algebraMap K[X] K⟮X⟯) p = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) 1

pp: case e'_3
K : Type u
inst✝ : Field K
p : K[X]
⊢ 1 = C (1 / gcd p 1).leadingCoeff⁻¹ * (1 / gcd p 1)

Tactic:
<;>

Goal state after:
case e'_2
K : Type u
inst✝ : Field K
p : K[X]
⊢ (algebraMap K[X] K⟮X⟯) p = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) 1

case e'_3
K : Type u
inst✝ : Field K
p : K[X]
⊢ 1 = C (1 / gcd p 1).leadingCoeff⁻¹ * (1 / gcd p 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
T : Type u_4
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
H : Function.Bijective ⇑(toIntegralClosure R S B)
H' : Function.Bijective ⇑(toIntegralClosure S T (S ⊗[R] B))
⊢ Function.Bijective ⇑(toIntegralClosure R T B)

Tactic:
let e := (Algebra.TensorProduct.cancelBaseChange ..).symm.trans <|
      (Algebra.TensorProduct.congr (.refl (R := T) (A₁ := T)) (.ofBijective _ H)).trans <|
      (AlgEquiv.ofBijective _ H').trans <|
      (AlgEquiv.mapIntegralClosure (Algebra.TensorProduct.cancelBaseChange ..))

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
T : Type u_4
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
H : Function.Bijective ⇑(toIntegralClosure R S B)
H' : Function.Bijective ⇑(toIntegralClosure S T (S ⊗[R] B))
e : T ⊗[R] ↥(integralClosure R B) ≃ₐ[T] ↥(integralClosure T (T ⊗[R] B)) :=
  (Algebra.TensorProduct.cancelBaseChange R S T T ↥(integralClosure R B)).symm.trans
    ((Algebra.TensorProduct.congr AlgEquiv.refl (AlgEquiv.ofBijective (toIntegralClosure R S B) H)).trans
      ((AlgEquiv.ofBijective (toIntegralClosure S T (S ⊗[R] B)) H').trans
        (Algebra.TensorProduct.cancelBaseChange R S T T B).mapIntegralClosure))
⊢ Function.Bijective ⇑(toIntegralClosure R T B)
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
M : Submonoid R
inst✝ : IsLocalization M S
⊢ Function.Bijective ⇑(toIntegralClosure R S B)

Tactic:
by
  let φ : integralClosure R B →ₐ[R] integralClosure S (S ⊗[R] B) :=
    AlgHom.codRestrict (Algebra.TensorProduct.includeRight.comp (integralClosure R B).val)
      ((integralClosure S (S ⊗[R] B)).restrictScalars R) fun ⟨x, hx⟩ ↦ by
    refine .of_comp (f := algebraMap R S) ?_
    convert!
      RingHom.IsIntegralElem.map hx
        (Algebra.TensorProduct.includeRight : B →ₐ[R] S ⊗[R] B).toRingHom
    simp [← IsScalarTower.algebraMap_eq]
  let := φ.toAlgebra
  have := IsScalarTower.of_algebraMap_eq' φ.comp_algebraMap.symm
  have : IsScalarTower (integralClosure R B) (integralClosure S (S ⊗[R] B)) (S ⊗[R] B) :=
    .of_algebraMap_eq' rfl
  have := IsLocalization.integralClosure (S := B) M (Rf := S) (Sf := S ⊗[R] B)
  convert!
    (IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (integralClosure R B) M)
        (S ⊗[R] integralClosure R B) (integralClosure S (S ⊗[R] B))).bijective
  rw [← AlgHom.coe_restrictScalars' R, ← AlgEquiv.coe_restrictScalars R, ← AlgEquiv.coe_toAlgHom]
  congr 1
  ext1
  · apply IsLocalization.algHom_ext M; ext
  · ext x
    dsimp [toIntegralClosure]
    simp [← Algebra.TensorProduct.right_algebraMap_apply]
    rfl

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
φ : 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
⊢ eval₂ ((algebraMap (↥R₂) St).comp ↑(aeval ⟨(algebraMap S St) (φ X), ⋯⟩)) ((algebraMap S St) t) q = 0

Tactic:
← map_zero (algebraMap S St),

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p r : 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
⊢ eval₂ ((algebraMap (↥R₂) St).comp ↑(aeval ⟨(algebraMap S St) (φ X), ⋯⟩)) ((algebraMap S St) t) q = (algebraMap S St) 0