awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
p : Ideal T
inst_7 : 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 :
  Eq.{u_3 + 1} (α := Subalgebra S T)
    (Subalgebra.saturation ⊥ (Submonoid.powers ((algebraMap S T : (a : S) → T) t)) ⋯ : Subalgebra S T)
    (⊤ : Subalgebra S T)
obtain : ∀ (m : ℕ) (hm : IsIntegral R (s ^ m * t)), ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
⊢ ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral R (r ^ m * x)

Tactic:
obtain ⟨m, hm⟩ := Hs t
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
p : Ideal T
inst_7 : 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 :
  Eq.{u_3 + 1} (α := Subalgebra S T)
    (Subalgebra.saturation ⊥ (Submonoid.powers ((algebraMap S T : (a : S) → T) t)) ⋯ : Subalgebra S T)
    (⊤ : Subalgebra S T)
m : ℕ
hm : IsIntegral R (s ^ m * t)
⊢ ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral R (r ^ m * x)

Tactic:
⟨algebraMap _ _ (s ^ (m + 1) * t), ?_, fun x ↦ ?_⟩

Premises used: HMul.hMul, Algebra.algebraMap, HPow.hPow, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
p : Ideal T
inst_7 : 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 :
  Eq.{u_3 + 1} (α := Subalgebra S T)
    (Subalgebra.saturation ⊥ (Submonoid.powers ((algebraMap S T : (a : S) → T) t)) ⋯ : Subalgebra S T)
    (⊤ : Subalgebra S T)
m : ℕ
hm : IsIntegral R (s ^ m * t)
refine_1 : ((algebraMap S T : (a : S) → T) (s ^ (m + 1) * t) : T) ∉ p
refine_2 :
  ∀ (x : T),
    ∃ (m_1 : ℕ), IsIntegral R (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) (s ^ (m + 1) * t) : T) m_1 * x)
⊢ ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral R (r ^ m * x)

Tactic:
refine ⟨algebraMap _ _ (s ^ (m + 1) * t), ?_, fun x ↦ ?_⟩
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
p : Ideal T
inst_7 : 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 :
  Eq.{u_3 + 1} (α := Subalgebra S T)
    (Subalgebra.saturation ⊥ (Submonoid.powers ((algebraMap S T : (a : S) → T) t)) ⋯ : Subalgebra S T)
    (⊤ : Subalgebra S T)
m : ℕ
hm : IsIntegral R (s ^ m * t)
⊢ ((algebraMap S T : (a : S) → T) (s ^ (m + 1) * t) : T) ∉ p

Tactic:
simpa using ‹p.IsPrime›.mul_notMem
      (mt ((inferInstance : (p.under S).IsPrime).mem_of_pow_mem (m + 1)) hsp) htp

Premises used: Ideal.IsPrime.mem_of_pow_mem, mt, inferInstance, Ideal.IsPrime.mul_notMem, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
p : Ideal T
inst_7 : 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 :
  Eq.{u_3 + 1} (α := Subalgebra S T)
    (Subalgebra.saturation ⊥ (Submonoid.powers ((algebraMap S T : (a : S) → T) t)) ⋯ : Subalgebra S T)
    (⊤ : Subalgebra S T)
m : ℕ
hm : IsIntegral R (s ^ m * t)
x : T
refine_2 :
  ∀ (n : ℕ) (a : S)
    (ha :
      (AlgHom.toRingHom (ofId S T) : (a : S) → T) a =
        (fun (x : ℕ) ↦ HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) t : T) x) n * x),
    ∃ (m_1 : ℕ), IsIntegral R (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) (s ^ (m + 1) * t) : T) m_1 * x)
⊢ ∃ (m_1 : ℕ), IsIntegral R (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) (s ^ (m + 1) * t) : T) m_1 * x)

Tactic:
obtain ⟨_, ⟨n, rfl⟩, a, ha⟩ := Ht.ge (Set.mem_univ x)

Premises used: Eq.ge, Set.mem_univ, rfl
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
p : Ideal T
inst_7 : 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 :
  Eq.{u_3 + 1} (α := Subalgebra S T)
    (Subalgebra.saturation ⊥ (Submonoid.powers ((algebraMap S T : (a : S) → T) t)) ⋯ : Subalgebra S T)
    (⊤ : Subalgebra S T)
m : ℕ
hm : IsIntegral R (s ^ m * t)
x : T
n : ℕ
a : S
ha :
  (AlgHom.toRingHom (ofId S T) : (a : S) → T) a =
    (fun (x : ℕ) ↦ HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) t : T) x) n * x
refine_2 :
  ∀ (k : ℕ) (hk : IsIntegral R (s ^ k * a)),
    ∃ (m_1 : ℕ), IsIntegral R (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) (s ^ (m + 1) * t) : T) m_1 * x)
⊢ ∃ (m_1 : ℕ), IsIntegral R (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) (s ^ (m + 1) * t) : T) m_1 * x)

Tactic:
obtain ⟨k, hk⟩ := Hs a
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
p : Ideal T
inst_7 : 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 :
  Eq.{u_3 + 1} (α := Subalgebra S T)
    (Subalgebra.saturation ⊥ (Submonoid.powers ((algebraMap S T : (a : S) → T) t)) ⋯ : Subalgebra S T)
    (⊤ : Subalgebra S T)
m : ℕ
hm : IsIntegral R (s ^ m * t)
x : T
n : ℕ
a : S
ha :
  (AlgHom.toRingHom (ofId S T) : (a : S) → T) a =
    (fun (x : ℕ) ↦ HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) t : T) x) n * x
k : ℕ
hk : IsIntegral R (s ^ k * a)
⊢ ∃ (m_1 : ℕ), IsIntegral R (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) (s ^ (m + 1) * t) : T) m_1 * x)

Tactic:
⟨k + n, ?_⟩

Premises used: HAdd.hAdd, Exists.intro
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
p : Ideal T
inst_7 : 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 :
  Eq.{u_3 + 1} (α := Subalgebra S T)
    (Subalgebra.saturation ⊥ (Submonoid.powers ((algebraMap S T : (a : S) → T) t)) ⋯ : Subalgebra S T)
    (⊤ : Subalgebra S T)
m : ℕ
hm : IsIntegral R (s ^ m * t)
x : T
n : ℕ
a : S
ha :
  (AlgHom.toRingHom (ofId S T) : (a : S) → T) a =
    (fun (x : ℕ) ↦ HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) t : T) x) n * x
k : ℕ
hk : IsIntegral R (s ^ k * a)
refine_2 : IsIntegral R (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) (s ^ (m + 1) * t) : T) (k + n) * x)
⊢ ∃ (m_1 : ℕ), IsIntegral R (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) (s ^ (m + 1) * t) : T) m_1 * x)

Tactic:
refine ⟨k + n, ?_⟩
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
p : Ideal T
inst_7 : 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 :
  Eq.{u_3 + 1} (α := Subalgebra S T)
    (Subalgebra.saturation ⊥ (Submonoid.powers ((algebraMap S T : (a : S) → T) t)) ⋯ : Subalgebra S T)
    (⊤ : Subalgebra S T)
m : ℕ
hm : IsIntegral R (s ^ m * t)
x : T
n : ℕ
a : S
ha :
  (AlgHom.toRingHom (ofId S T) : (a : S) → T) a =
    (fun (x : ℕ) ↦ HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) t : T) x) n * x
k : ℕ
hk : IsIntegral R (s ^ k * a)
h :
  HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) (s ^ (m + 1) * t) : T) (k + n) * x =
    (algebraMap S T : (a : S) → T) (s ^ ((m + 1) * n) * (s ^ m * t) ^ k * (s ^ k * a))
refine_2 :
  IsIntegral.{u_1, u_3} R (A := T)
    ((algebraMap S T : (a : S) → T) (s ^ ((m + 1) * n) * (s ^ m * t) ^ k * (s ^ k * a)) : T)
⊢ IsIntegral R (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) (s ^ (m + 1) * t) : T) (k + n) * x)

Tactic:
convert_to IsIntegral R (algebraMap S T ((s ^ ((m + 1) * n) * (s ^ m * t) ^ k * (s ^ k * a))))

Premises used: HMul.hMul, Algebra.algebraMap, IsIntegral, HPow.hPow, HAdd.hAdd, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
p : Ideal T
inst_7 : 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 :
  Eq.{u_3 + 1} (α := Subalgebra S T)
    (Subalgebra.saturation ⊥ (Submonoid.powers ((algebraMap S T : (a : S) → T) t)) ⋯ : Subalgebra S T)
    (⊤ : Subalgebra S T)
m : ℕ
hm : IsIntegral R (s ^ m * t)
x : T
n : ℕ
a : S
ha : (algebraMap S T : (a : S) → T) a = HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) t : T) n * x
k : ℕ
hk : IsIntegral R (s ^ k * a)
h :
  HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) s : T) m ^ k *
            HPow.hPow (α := T) (β := ℕ) ((algebraMap S T : (a : S) → T) s : T) 1 ^ k *
          HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) t : T) k *
        (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) s : T) m ^ n *
            HPow.hPow (α := T) (β := ℕ) ((algebraMap S T : (a : S) → T) s : T) 1 ^ n *
          HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) t : T) n) *
      x =
    HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) s : T) ((m + 1) * n) *
        (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) s : T) m ^ k *
          HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) t : T) k) *
      (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) s : T) k *
        (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) t : T) n * x))
⊢ HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) (s ^ (m + 1) * t) : T) (k + n) * x =
    (algebraMap S T : (a : S) → T) (s ^ ((m + 1) * n) * (s ^ m * t) ^ k * (s ^ k * a))

Tactic:
simp only [map_pow, map_mul, ha, pow_add, mul_pow]

Premises used: pow_add, map_pow, map_mul, mul_pow
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
p : Ideal T
inst_7 : 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 :
  Eq.{u_3 + 1} (α := Subalgebra S T)
    (Subalgebra.saturation ⊥ (Submonoid.powers ((algebraMap S T : (a : S) → T) t)) ⋯ : Subalgebra S T)
    (⊤ : Subalgebra S T)
m : ℕ
hm : IsIntegral R (s ^ m * t)
x : T
n : ℕ
a : S
ha : (algebraMap S T : (a : S) → T) a = HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) t : T) n * x
k : ℕ
hk : IsIntegral R (s ^ k * a)
⊢ HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) s : T) m ^ k *
            HPow.hPow (α := T) (β := ℕ) ((algebraMap S T : (a : S) → T) s : T) 1 ^ k *
          HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) t : T) k *
        (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) s : T) m ^ n *
            HPow.hPow (α := T) (β := ℕ) ((algebraMap S T : (a : S) → T) s : T) 1 ^ n *
          HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) t : T) n) *
      x =
    HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) s : T) ((m + 1) * n) *
        (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) s : T) m ^ k *
          HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) t : T) k) *
      (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) s : T) k *
        (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) t : T) n * x))

Tactic:
ring
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
p : Ideal T
inst_7 : 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 :
  Eq.{u_3 + 1} (α := Subalgebra S T)
    (Subalgebra.saturation ⊥ (Submonoid.powers ((algebraMap S T : (a : S) → T) t)) ⋯ : Subalgebra S T)
    (⊤ : Subalgebra S T)
m : ℕ
hm : IsIntegral R (s ^ m * t)
x : T
n : ℕ
a : S
ha :
  (AlgHom.toRingHom (ofId S T) : (a : S) → T) a =
    (fun (x : ℕ) ↦ HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) t : T) x) n * x
k : ℕ
hk : IsIntegral R (s ^ k * a)
⊢ IsIntegral.{u_1, u_3} R (A := T)
    ((algebraMap S T : (a : S) → T) (s ^ ((m + 1) * n) * (s ^ m * t) ^ k * (s ^ k * a)) : T)

Tactic:
.algebraMap (.mul ((hs.pow _).mul (hm.pow _)) hk)

Premises used: IsIntegral.mul, IsIntegral.pow, IsIntegral.algebraMap
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
p : Ideal T
inst_7 : 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 :
  Eq.{u_3 + 1} (α := Subalgebra S T)
    (Subalgebra.saturation ⊥ (Submonoid.powers ((algebraMap S T : (a : S) → T) t)) ⋯ : Subalgebra S T)
    (⊤ : Subalgebra S T)
m : ℕ
hm : IsIntegral R (s ^ m * t)
x : T
n : ℕ
a : S
ha :
  (AlgHom.toRingHom (ofId S T) : (a : S) → T) a =
    (fun (x : ℕ) ↦ HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) t : T) x) n * x
k : ℕ
hk : IsIntegral R (s ^ k * a)
⊢ IsIntegral.{u_1, u_3} R (A := T)
    ((algebraMap S T : (a : S) → T) (s ^ ((m + 1) * n) * (s ^ m * t) ^ k * (s ^ k * a)) : T)

Tactic:
exact .algebraMap (.mul ((hs.pow _).mul (hm.pow _)) 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
p : Ideal S
inst_3 : p.IsPrime
inst_4 : Algebra.IsIntegral R S
⊢ ZariskisMainProperty R p

Tactic:
zariskisMainProperty_iff'.mpr ⟨1, p.primeCompl.one_mem,
    fun _ ↦ ⟨0, Algebra.IsIntegral.isIntegral _⟩⟩

Premises used: Iff.mpr, Algebra.IsIntegral.isIntegral, HMul.hMul, Algebra.zariskisMainProperty_iff', Submonoid.one_mem, HPow.hPow, And.intro, Exists.intro, Ideal.primeCompl, OfNat.ofNat
-- 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 : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
rw : HMul.hMul (α := St) ((algebraMap S St : (a : S) → St) t : St) t' = 1
rw₁ rw₂ : Eq.{u_2 + 1} (α := St) 1 1
⊢ HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1

Tactic:
rw [mul_comm, IsLocalization.Away.mul_invSelf]

Premises used: IsLocalization.Away.mul_invSelf, mul_comm
-- 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 : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
⊢ HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1

Tactic:
have ht't : t' * algebraMap S St t = 1 := by rw [mul_comm, IsLocalization.Away.mul_invSelf]
-- 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 : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)]
this_1 : Algebra ↥R₁ ↥R₂ := R₂.algebra
this_2 : Algebra (↥R₂) St := R₂.toAlgebra
this : Algebra (↥R₁) St := R₁.toAlgebra
⊢ IsScalarTower (↥R₁) (↥R₂) St

Tactic:
haveI : IsScalarTower R₁ R₂ St := Subalgebra.isScalarTower_mid _
-- 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 : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)]
this_1 : Algebra ↥R₁ ↥R₂ := R₂.algebra
this_2 : Algebra (↥R₂) St := R₂.toAlgebra
this_3 : Algebra (↥R₁) St := R₁.toAlgebra
this : IsScalarTower (↥R₁) (↥R₂) St
inl : Subsingleton.{u_2 + 1} ↥R₁ → Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂
inr : Nontrivial.{u_2} ↥R₁ → Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂
⊢ Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂

Tactic:
cases subsingleton_or_nontrivial R₁

Premises used: Membership.mem, Subtype, subsingleton_or_nontrivial
-- 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 : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)]
this_1 : Algebra ↥R₁ ↥R₂ := R₂.algebra
this_2 : Algebra (↥R₂) St := R₂.toAlgebra
this_3 : Algebra (↥R₁) St := R₁.toAlgebra
this : IsScalarTower (↥R₁) (↥R₂) St
h : Subsingleton.{u_2 + 1} ↥R₁
⊢ Subsingleton.{u_2 + 1} ↥R₂

Tactic:
have := (algebraMap R₁ R₂).codomain_trivial
-- 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 : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)]
this_1 : Algebra ↥R₁ ↥R₂ := R₂.algebra
this_2 : Algebra (↥R₂) St := R₂.toAlgebra
this_3 : Algebra (↥R₁) St := R₁.toAlgebra
this_4 : IsScalarTower (↥R₁) (↥R₂) St
h : Subsingleton.{u_2 + 1} ↥R₁
this : Subsingleton.{u_2 + 1} ↥R₂
⊢ Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂

Tactic:
⟨(Subsingleton.elim · 0 ▸ isIntegral_zero)⟩

Premises used: Eq.rec, isIntegral_zero, Subsingleton.elim, OfNat.ofNat, Eq.symm, Algebra.IsIntegral.mk
-- 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 : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)]
this_1 : Algebra ↥R₁ ↥R₂ := R₂.algebra
this_2 : Algebra (↥R₂) St := R₂.toAlgebra
this_3 : Algebra (↥R₁) St := R₁.toAlgebra
this_4 : IsScalarTower (↥R₁) (↥R₂) St
h : Subsingleton.{u_2 + 1} ↥R₁
this : Subsingleton.{u_2 + 1} ↥R₂
⊢ Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂

Tactic:
exact ⟨(Subsingleton.elim · 0 ▸ isIntegral_zero)⟩
-- 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 : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)]
this_1 : Algebra ↥R₁ ↥R₂ := R₂.algebra
this_2 : Algebra (↥R₂) St := R₂.toAlgebra
this_3 : Algebra (↥R₁) St := R₁.toAlgebra
this : IsScalarTower (↥R₁) (↥R₂) St
h : Nontrivial.{u_2} ↥R₁
inr : IsIntegral ↥R₁ (A := St) ((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)
⊢ Algebra.IsIntegral.{u_2, u_2} ↥R₁ ↥R₂

Tactic:
rw [← le_integralClosure_iff_isIntegral, Algebra.adjoin_le_iff, Set.singleton_subset_iff,
      SetLike.mem_coe, mem_integralClosure_iff]

Premises used: Set.singleton_subset_iff, le_integralClosure_iff_isIntegral, mem_integralClosure_iff, Algebra.adjoin_le_iff, SetLike.mem_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 : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t = (φ : (a : R[X]) → S) r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : HMul.hMul (β := St) t' ((algebraMap S St : (a : S) → St) t : St) = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)]
this_1 : Algebra ↥R₁ ↥R₂ := R₂.algebra
this_2 : Algebra (↥R₂) St := R₂.toAlgebra
this_3 : Algebra (↥R₁) St := R₁.toAlgebra
this : IsScalarTower (↥R₁) (↥R₂) St
h : Nontrivial.{u_2} ↥R₁
⊢ IsIntegral ↥R₁ (A := St) ((algebraMap S St : (a : S) → St) ((φ : (a : R[X]) → S) X) : St)

Tactic:
⟨p.map (algebraMap R R₁) - C ⟨t', Algebra.self_mem_adjoin_singleton R t'⟩ *
        r.map (algebraMap R R₁), (hpm.map _).sub_of_left (degree_lt_degree ?_), ?_⟩

Premises used: Polynomial.C, HMul.hMul, Algebra.algebraMap, HSub.hSub, Membership.mem, Subtype, RingHom.IsIntegralElem, IsIntegral, Polynomial.Monic.sub_of_left, Polynomial.degree_lt_degree, And.intro, Exists.intro, Polynomial.map, Polynomial.Monic.map, DFunLike.coe