awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this_2 : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
H :
  Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
q : R'[X]
hq :
  IsIntegral R'
    (HSub.hSub (α := S') (β := S') ((algebraMap S S' : (a : S) → S') t : S')
      (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S') q :
        S'))
n : ℕ
q' : R[X]
e : map (algebraMap R R') q' = HSMul.hSMul (α := R) ((fun (x : ℕ) ↦ a ^ x) n) q
this :
  IsIntegral R' (A := S')
    ((algebraMap S S' : (a : S) → S') (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q' : S)) : S')
m : ℕ
hm :
  IsIntegral R (A := S')
    ((algebraMap S S' : (a : S) → S')
        (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ m) : S)
          (HSub.hSub (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ n) : S) t)
            ((φ : (a : R[X]) → S) q' : S))) :
      S')
k : ℕ
hk :
  IsIntegral R
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((fun (x : ℕ) ↦ a ^ x) k)
      (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ m) : S)
        (HSub.hSub (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ n) : S) t)
          ((φ : (a : R[X]) → S) q' : S))))
⊢ ∃ (q : R[X]) (n : ℕ), IsIntegral R (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q : S))

Tactic:
⟨C a ^ (k + m) * q', k + m + n, ?_⟩

Premises used: Polynomial.C, HMul.hMul, HPow.hPow, HAdd.hAdd, Exists.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this_2 : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
H :
  Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
q : R'[X]
hq :
  IsIntegral R'
    (HSub.hSub (α := S') (β := S') ((algebraMap S S' : (a : S) → S') t : S')
      (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S') q :
        S'))
n : ℕ
q' : R[X]
e : map (algebraMap R R') q' = HSMul.hSMul (α := R) ((fun (x : ℕ) ↦ a ^ x) n) q
this :
  IsIntegral R' (A := S')
    ((algebraMap S S' : (a : S) → S') (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q' : S)) : S')
m : ℕ
hm :
  IsIntegral R (A := S')
    ((algebraMap S S' : (a : S) → S')
        (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ m) : S)
          (HSub.hSub (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ n) : S) t)
            ((φ : (a : R[X]) → S) q' : S))) :
      S')
k : ℕ
hk :
  IsIntegral R
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((fun (x : ℕ) ↦ a ^ x) k)
      (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ m) : S)
        (HSub.hSub (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ n) : S) t)
          ((φ : (a : R[X]) → S) q' : S))))
refine :
  IsIntegral R
    (HSub.hSub (β := S) (a ^ (k + m + n) • t)
      ((φ : (a : R[X]) → S) (HPow.hPow (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (k + m) * q') : S))
⊢ ∃ (q : R[X]) (n : ℕ), IsIntegral R (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q : S))

Tactic:
refine ⟨C a ^ (k + m) * q', k + m + n, ?_⟩
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this_2 : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
H :
  Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
q : R'[X]
hq :
  IsIntegral R'
    (HSub.hSub (α := S') (β := S') ((algebraMap S S' : (a : S) → S') t : S')
      (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S') q :
        S'))
n : ℕ
q' : R[X]
e : map (algebraMap R R') q' = HSMul.hSMul (α := R) ((fun (x : ℕ) ↦ a ^ x) n) q
this :
  IsIntegral R' (A := S')
    ((algebraMap S S' : (a : S) → S') (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q' : S)) : S')
m : ℕ
hm :
  IsIntegral R (A := S')
    ((algebraMap S S' : (a : S) → S')
        (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ m) : S)
          (HSub.hSub (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ n) : S) t)
            ((φ : (a : R[X]) → S) q' : S))) :
      S')
k : ℕ
hk :
  IsIntegral R
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((fun (x : ℕ) ↦ a ^ x) k)
      (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ m) : S)
        (HSub.hSub (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ n) : S) t)
          ((φ : (a : R[X]) → S) q' : S))))
⊢ IsIntegral R
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((fun (x : ℕ) ↦ a ^ x) k)
      (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ m) : S)
        (HSub.hSub (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ n) : S) t)
          ((φ : (a : R[X]) → S) q' : S))))

Tactic:
hk
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this_2 : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
H :
  Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
q : R'[X]
hq :
  IsIntegral R'
    (HSub.hSub (α := S') (β := S') ((algebraMap S S' : (a : S) → S') t : S')
      (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S') q :
        S'))
n : ℕ
q' : R[X]
e : map (algebraMap R R') q' = HSMul.hSMul (α := R) ((fun (x : ℕ) ↦ a ^ x) n) q
this :
  IsIntegral R' (A := S')
    ((algebraMap S S' : (a : S) → S') (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q' : S)) : S')
m : ℕ
hm :
  IsIntegral R (A := S')
    ((algebraMap S S' : (a : S) → S')
        (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ m) : S)
          (HSub.hSub (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ n) : S) t)
            ((φ : (a : R[X]) → S) q' : S))) :
      S')
k : ℕ
hk :
  IsIntegral R
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((fun (x : ℕ) ↦ a ^ x) k)
      (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ m) : S)
        (HSub.hSub (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ n) : S) t)
          ((φ : (a : R[X]) → S) q' : S))))
h :
  HSub.hSub (β := S) (a ^ (k + m + n) • t)
      ((φ : (a : R[X]) → S) (HPow.hPow (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (k + m) * q') : S) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((fun (x : ℕ) ↦ a ^ x) k)
      (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ m) : S)
        (HSub.hSub (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ n) : S) t)
          ((φ : (a : R[X]) → S) q' : S)))
⊢ IsIntegral R
    (HSub.hSub (β := S) (a ^ (k + m + n) • t)
      ((φ : (a : R[X]) → S) (HPow.hPow (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (k + m) * q') : S))

Tactic:
convert! hk using 1
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this_2 : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
H :
  Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
q : R'[X]
hq :
  IsIntegral R'
    (HSub.hSub (α := S') (β := S') ((algebraMap S S' : (a : S) → S') t : S')
      (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S') q :
        S'))
n : ℕ
q' : R[X]
e : map (algebraMap R R') q' = HSMul.hSMul (α := R) ((fun (x : ℕ) ↦ a ^ x) n) q
this :
  IsIntegral R' (A := S')
    ((algebraMap S S' : (a : S) → S') (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q' : S)) : S')
m : ℕ
hm :
  IsIntegral R (A := S')
    ((algebraMap S S' : (a : S) → S')
        (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ m) : S)
          (HSub.hSub (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ n) : S) t)
            ((φ : (a : R[X]) → S) q' : S))) :
      S')
k : ℕ
hk :
  IsIntegral R
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((fun (x : ℕ) ↦ a ^ x) k)
      (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ m) : S)
        (HSub.hSub (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ n) : S) t)
          ((φ : (a : R[X]) → S) q' : S))))
h :
  HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) a : S) (k + m + n) * t -
      HMul.hMul (β := S) (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) a : S) (k + m))
        ((φ : (a : R[X]) → S) q' : S) =
    HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) a : S) k *
      (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) a : S) m *
        HSub.hSub (β := S) (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) a : S) n * t)
          ((φ : (a : R[X]) → S) q' : S))
⊢ HSub.hSub (β := S) (a ^ (k + m + n) • t)
      ((φ : (a : R[X]) → S) (HPow.hPow (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (k + m) * q') : S) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((fun (x : ℕ) ↦ a ^ x) k)
      (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ m) : S)
        (HSub.hSub (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ n) : S) t)
          ((φ : (a : R[X]) → S) q' : S)))

Tactic:
simp only [Algebra.smul_def, map_pow, ← Polynomial.algebraMap_eq, map_mul, AlgHom.commutes]

Premises used: map_pow, map_mul, AlgHom.commutes, Algebra.smul_def, Polynomial.algebraMap_eq
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this_2 : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
H :
  Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
q : R'[X]
hq :
  IsIntegral R'
    (HSub.hSub (α := S') (β := S') ((algebraMap S S' : (a : S) → S') t : S')
      (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S') q :
        S'))
n : ℕ
q' : R[X]
e : map (algebraMap R R') q' = HSMul.hSMul (α := R) ((fun (x : ℕ) ↦ a ^ x) n) q
this :
  IsIntegral R' (A := S')
    ((algebraMap S S' : (a : S) → S') (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q' : S)) : S')
m : ℕ
hm :
  IsIntegral R (A := S')
    ((algebraMap S S' : (a : S) → S')
        (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ m) : S)
          (HSub.hSub (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ n) : S) t)
            ((φ : (a : R[X]) → S) q' : S))) :
      S')
k : ℕ
hk :
  IsIntegral R
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((fun (x : ℕ) ↦ a ^ x) k)
      (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ m) : S)
        (HSub.hSub (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ n) : S) t)
          ((φ : (a : R[X]) → S) q' : S))))
⊢ HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) a : S) (k + m + n) * t -
      HMul.hMul (β := S) (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) a : S) (k + m))
        ((φ : (a : R[X]) → S) q' : S) =
    HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) a : S) k *
      (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) a : S) m *
        HSub.hSub (β := S) (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) a : S) n * t)
          ((φ : (a : R[X]) → S) q' : S))

Tactic:
ring
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
⊢ Module.Finite.{u_1, u_2} R[X] S

Tactic:
algebraize [φ.toRingHom]

Premises used: AlgHom.toRingHom
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
⊢ IsScalarTower R R[X] S

Tactic:
have : IsScalarTower R R[X] S := .of_algebraMap_eq' φ.comp_algebraMap.symm
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this : IsScalarTower R R[X] S
x : S
⊢ HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t * x ∈ φ.range

Tactic:
simpa [← AlgHom.map_adjoin_singleton] using hp x

Premises used: AlgHom.map_adjoin_singleton
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this : IsScalarTower R R[X] S
x : S
⊢ HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t * x ∈ φ.range

Tactic:
have : φ p * t * x ∈ φ.range := by simpa [← AlgHom.map_adjoin_singleton] using hp x
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this_1 : IsScalarTower R R[X] S
x : S
this : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t * x ∈ φ.range
⊢ HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t * x ∈ φ.range

Tactic:
this
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this_1 : IsScalarTower R R[X] S
x : S
this : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t * x ∈ φ.range
h : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) (t * x) = HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t * x
⊢ HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) (t * x) ∈ φ.range

Tactic:
convert! this using 1
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this_1 : IsScalarTower R R[X] S
x : S
this : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t * x ∈ φ.range
⊢ HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) (t * x) = HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t * x

Tactic:
ring
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this_1 : IsScalarTower R R[X] S
x : S
this : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t * x ∈ φ.range
obtain :
  ∀ (q : R[X]) (n : ℕ)
    (hn : IsIntegral R (HSub.hSub (β := S) (p.leadingCoeff ^ n • (t * x)) ((φ : (a : R[X]) → S) q : S))),
    ∃ (n : ℕ), p.leadingCoeff ^ n • (t * x) ∈ φ.range
⊢ ∃ (n : ℕ), p.leadingCoeff ^ n • (t * x) ∈ φ.range

Tactic:
obtain ⟨q, n, hn⟩ :=
      exists_isIntegral_leadingCoeff_pow_smul_sub_of_isIntegralElem_of_mul_mem_range φ _ p
        (hφ.to_isIntegral (t * x)) (by convert! this using 1; ring)

Premises used: HMul.hMul, exists_isIntegral_leadingCoeff_pow_smul_sub_of_isIntegralElem_of_mul_mem_range, RingHom.Finite.to_isIntegral
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this_1 : IsScalarTower R R[X] S
x : S
this : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t * x ∈ φ.range
q : R[X]
n : ℕ
hn : IsIntegral R (HSub.hSub (β := S) (p.leadingCoeff ^ n • (t * x)) ((φ : (a : R[X]) → S) q : S))
obtain :
  ∀ (r : R)
    (hr :
      (algebraMap R S : (a : R) → S) r =
        HSub.hSub (β := S) (p.leadingCoeff ^ n • (t * x)) ((φ : (a : R[X]) → S) q : S)),
    ∃ (n : ℕ), p.leadingCoeff ^ n • (t * x) ∈ φ.range
⊢ ∃ (n : ℕ), p.leadingCoeff ^ n • (t * x) ∈ φ.range

Tactic:
obtain ⟨r, hr : algebraMap _ _ r = _⟩ := hRS.le hn

Premises used: Eq.le
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this_1 : IsScalarTower R R[X] S
x : S
this : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t * x ∈ φ.range
q : R[X]
n : ℕ
hn : IsIntegral R (HSub.hSub (β := S) (p.leadingCoeff ^ n • (t * x)) ((φ : (a : R[X]) → S) q : S))
r : R
hr : (algebraMap R S : (a : R) → S) r = HSub.hSub (β := S) (p.leadingCoeff ^ n • (t * x)) ((φ : (a : R[X]) → S) q : S)
⊢ (φ.toRingHom : (a : R[X]) → S) (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) q) =
    p.leadingCoeff ^ n • (t * x)

Tactic:
simp [← Polynomial.algebraMap_eq, - Polynomial.algebraMap_apply, hr]

Premises used: Polynomial.algebraMap_apply, Polynomial.algebraMap_eq
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this_1 : IsScalarTower R R[X] S
x : S
this : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t * x ∈ φ.range
q : R[X]
n : ℕ
hn : IsIntegral R (HSub.hSub (β := S) (p.leadingCoeff ^ n • (t * x)) ((φ : (a : R[X]) → S) q : S))
r : R
hr : (algebraMap R S : (a : R) → S) r = HSub.hSub (β := S) (p.leadingCoeff ^ n • (t * x)) ((φ : (a : R[X]) → S) q : S)
⊢ ∃ (n : ℕ), p.leadingCoeff ^ n • (t * x) ∈ φ.range

Tactic:
exact ⟨n, (C r + q), by simp [← Polynomial.algebraMap_eq, - Polynomial.algebraMap_apply, hr]⟩