awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hf : ¬conductor R ((f : (a : R[X]) → S) X) ≤ p
x : S
hxp : x ∉ p
hx : ∀ (a : S), x * a ∈ f.range
this : Algebra (Localization.AtPrime (R := ↥f.range) (Ideal.under (↥f.range) p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥f.range) p) p
e : Localization.AtPrime (R := ↥f.range) (Ideal.under (↥f.range) p) ≃ₐ[R] Localization.AtPrime p :=
  AlgEquiv.ofBijective
    (IsScalarTower.toAlgHom R (Localization.AtPrime (R := ↥f.range) (Ideal.under (↥f.range) p))
      (Localization.AtPrime p))
    ⋯
⊢ WeaklyQuasiFiniteAt R (S := ↥f.range) (Ideal.under (↥f.range) p)

Tactic:
.of_algHom_localization _ _ e.symm.toAlgHom e.symm.surjective

Premises used: AlgEquiv.toAlgHom, AlgEquiv.symm, Algebra.WeaklyQuasiFiniteAt.of_algHom_localization, AlgEquiv.surjective
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hf : ¬conductor R ((f : (a : R[X]) → S) X) ≤ p
x : S
hxp : x ∉ p
hx : ∀ (a : S), x * a ∈ f.range
this : Algebra (Localization.AtPrime (R := ↥f.range) (Ideal.under (↥f.range) p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥f.range) p) p
e : Localization.AtPrime (R := ↥f.range) (Ideal.under (↥f.range) p) ≃ₐ[R] Localization.AtPrime p :=
  AlgEquiv.ofBijective
    (IsScalarTower.toAlgHom R (Localization.AtPrime (R := ↥f.range) (Ideal.under (↥f.range) p))
      (Localization.AtPrime p))
    ⋯
⊢ WeaklyQuasiFiniteAt R (S := ↥f.range) (Ideal.under (↥f.range) p)

Tactic:
exact .of_algHom_localization _ _ e.symm.toAlgHom e.symm.surjective
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hf : ¬conductor R ((f : (a : R[X]) → S) X) ≤ p
x : S
hxp : x ∉ p
hx : ∀ (a : S), x * a ∈ f.range
⊢ WeaklyQuasiFiniteAt R (S := ↥f.range) (Ideal.under (↥f.range) p)

Tactic:
have : Algebra.WeaklyQuasiFiniteAt R (p.under f.range) := by
      let := Localization.AtPrime.algebraOfLiesOver (p.under f.range) p
      let e : Localization.AtPrime (p.under f.range) ≃ₐ[R] Localization.AtPrime p :=
        .ofBijective (IsScalarTower.toAlgHom _ _ _)
          (Localization.localRingHom_bijective_of_not_conductor_le hf
            (by simp [← AlgHom.map_adjoin_singleton f]) _)
      exact .of_algHom_localization _ _ e.symm.toAlgHom e.symm.surjective
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hf : ¬conductor R ((f : (a : R[X]) → S) X) ≤ p
x : S
hxp : x ∉ p
hx : ∀ (a : S), x * a ∈ f.range
this : WeaklyQuasiFiniteAt R (S := ↥f.range) (Ideal.under (↥f.range) p)
⊢ ZariskisMainProperty R (S := ↥f.range) (Ideal.under (↥f.range) p)

Tactic:
.of_adjoin_eq_top _ ⟨f X, X, rfl⟩ ?_

Premises used: _private.0.Algebra.ZariskisMainProperty.of_adjoin_eq_top, Subtype.mk, Exists.intro, Polynomial.X, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hf : ¬conductor R ((f : (a : R[X]) → S) X) ≤ p
x : S
hxp : x ∉ p
hx : ∀ (a : S), x * a ∈ f.range
this : WeaklyQuasiFiniteAt R (S := ↥f.range) (Ideal.under (↥f.range) p)
refine_1 :
  Eq (α := Subalgebra R ↥f.range) R[(Subtype.mk (p := fun (x : S) ↦ x ∈ f.range) ((f : (a : R[X]) → S) X) ⋯ : ↥f.range)]
    ⊤
⊢ ZariskisMainProperty R (S := ↥f.range) (Ideal.under (↥f.range) p)

Tactic:
refine .of_adjoin_eq_top _ ⟨f X, X, rfl⟩ ?_
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hf : ¬conductor R ((f : (a : R[X]) → S) X) ≤ p
x : S
hxp : x ∉ p
hx : ∀ (a : S), x * a ∈ f.range
this : WeaklyQuasiFiniteAt R (S := ↥f.range) (Ideal.under (↥f.range) p)
⊢ Eq (α := Subalgebra R ↥f.range) R[(Subtype.mk (p := fun (x : S) ↦ x ∈ f.range) ((f : (a : R[X]) → S) X) ⋯ : ↥f.range)]
    ⊤

Tactic:
simp [← (Subalgebra.map_injective (f := Subalgebra.val _) Subtype.val_injective).eq_iff,
      ← AlgHom.map_adjoin_singleton f, Subalgebra.range_val]

Premises used: Subtype.val_injective, Function.Injective.eq_iff, Subalgebra.range_val, Subalgebra.map_injective, AlgHom.map_adjoin_singleton
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hf : ¬conductor R ((f : (a : R[X]) → S) X) ≤ p
x : S
hxp : x ∉ p
hx : ∀ (a : S), x * a ∈ f.range
⊢ x ∈ f.range

Tactic:
simpa using hx 1

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hf : ¬conductor R ((f : (a : R[X]) → S) X) ≤ p
x : S
hxp : x ∉ p
hx : ∀ (a : S), x * a ∈ f.range
refine_2 :
  ∀ (s : S),
    Membership.mem (γ := Subalgebra (↥f.range) S) ⊤ s →
      Membership.mem (γ := Subalgebra (↥f.range) S) ⊥
        ((fun (x_2 : ℕ) ↦
              HPow.hPow (α := S)
                ((algebraMap (↥f.range) S : (a : ↥f.range) → S) (Subtype.mk (p := fun (x : S) ↦ x ∈ f.range) x ⋯) : S)
                x_2)
            1 *
          s)
⊢ ∃ r ∉ Ideal.under (↥f.range) p,
    Eq (α := Subalgebra (↥f.range) S)
      (Subalgebra.saturation ⊥ (Submonoid.powers ((algebraMap (↥f.range) S : (a : ↥f.range) → S) r)) ⋯ :
        Subalgebra (↥f.range) S)
      (⊤ : Subalgebra (↥f.range) S)

Tactic:
refine ⟨⟨x, by simpa using hx 1⟩, hxp, top_le_iff.mp fun s _ ↦ ⟨_, ⟨1, rfl⟩, ?_⟩⟩
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R S : Type u
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
p : Ideal S
inst_6 : p.IsPrime
inst_7 : WeaklyQuasiFiniteAt R p
f : R[X] →ₐ[R] S
H : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hf : ¬conductor R ((f : (a : R[X]) → S) X) ≤ p
x : S
hxp : x ∉ p
hx : ∀ (a : S), x * a ∈ f.range
s : S
h : Membership.mem (γ := Subalgebra (↥f.range) S) ⊤ s
⊢ Membership.mem (γ := Subalgebra (↥f.range) S) ⊥
    ((fun (x_1 : ℕ) ↦
          HPow.hPow (α := S)
            ((algebraMap (↥f.range) S : (a : ↥f.range) → S) (Subtype.mk (p := fun (x : S) ↦ x ∈ f.range) x ⋯) : S) x_1)
        1 *
      s)

Tactic:
simpa [Algebra.mem_bot] using hx s

Premises used: Algebra.mem_bot
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin 0) R →ₐ[R] S
hf : f.Finite
rw : RingHom.Finite (algebraMap R S)
⊢ Module.Finite R S

Tactic:
rw [← RingHom.finite_algebraMap]

Premises used: RingHom.finite_algebraMap
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin 0) R →ₐ[R] S
hf : f.Finite
⊢ (f.comp MvPolynomial.C).Finite

Tactic:
RingHom.Finite.comp hf (RingHom.Finite.of_surjective _ (MvPolynomial.C_surjective _))

Premises used: RingHom.Finite.comp, MvPolynomial.C_surjective, RingHom.Finite.of_surjective
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin 0) R →ₐ[R] S
hf : f.Finite
h : algebraMap R S = f.comp MvPolynomial.C
⊢ RingHom.Finite (algebraMap R S)

Tactic:
convert! RingHom.Finite.comp hf (RingHom.Finite.of_surjective _ (MvPolynomial.C_surjective _))

Premises used: RingHom.Finite.comp, MvPolynomial.C_surjective, RingHom.Finite.of_surjective
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin 0) R →ₐ[R] S
hf : f.Finite
⊢ algebraMap R S = f.comp MvPolynomial.C

Tactic:
f.comp_algebraMap.symm

Premises used: AlgHom.comp_algebraMap, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Eq.symm, MvPolynomial.C
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin 0) R →ₐ[R] S
hf : f.Finite
⊢ algebraMap R S = f.comp MvPolynomial.C

Tactic:
exact f.comp_algebraMap.symm

Premises used: AlgHom.comp_algebraMap, Eq.symm
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin 0) R →ₐ[R] S
hf : f.Finite
⊢ Module.Finite R S

Tactic:
have : Module.Finite R S := by
      rw [← RingHom.finite_algebraMap]
      convert! RingHom.Finite.comp hf (RingHom.Finite.of_surjective _ (MvPolynomial.C_surjective _))
      exact f.comp_algebraMap.symm
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin 0) R →ₐ[R] S
hf : f.Finite
this : Module.Finite R S
⊢ ZariskisMainProperty R p

Tactic:
.of_isIntegral _

Premises used: Algebra.ZariskisMainProperty.of_isIntegral
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin 0) R →ₐ[R] S
hf : f.Finite
this : Module.Finite R S
⊢ ZariskisMainProperty R p

Tactic:
exact .of_isIntegral _
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S) (hf : f.Finite), ZariskisMainProperty R p
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S :=
  f.comp
    (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →ₐ[R] MvPolynomial (Fin (n + 1)) R)
this : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
⊢ IsScalarTower R (MvPolynomial (Fin n) R) S

Tactic:
have : IsScalarTower R (MvPolynomial (Fin n) R) S := .of_algebraMap_eq fun r ↦
      (f.commutes r).symm.trans congr(f ($(MvPolynomial.finSuccEquiv_comp_C_eq_C n) r)).symm
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S) (hf : f.Finite), ZariskisMainProperty R p
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S :=
  f.comp
    (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →ₐ[R] MvPolynomial (Fin (n + 1)) R)
this_1 : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
⊢ WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p

Tactic:
.of_restrictScalars R _ _

Premises used: Algebra.WeaklyQuasiFiniteAt.of_restrictScalars
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S) (hf : f.Finite), ZariskisMainProperty R p
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S :=
  f.comp
    (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →ₐ[R] MvPolynomial (Fin (n + 1)) R)
this_1 : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
⊢ WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p

Tactic:
exact .of_restrictScalars R _ _
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S) (hf : f.Finite), ZariskisMainProperty R p
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S :=
  f.comp
    (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →ₐ[R] MvPolynomial (Fin (n + 1)) R)
this_1 : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
⊢ WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p

Tactic:
have : Algebra.WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p := by
      exact .of_restrictScalars R _ _
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S) (hf : f.Finite), ZariskisMainProperty R p
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S :=
  f.comp
    (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →ₐ[R] MvPolynomial (Fin (n + 1)) R)
this_1 : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
⊢ ZariskisMainProperty (MvPolynomial (Fin n) R) p

Tactic:
have := ZariskisMainProperty.of_algHom_polynomial p f''
      (RingHom.Finite.comp hf (MvPolynomial.finSuccEquiv R n).symm.toRingEquiv.finite)
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S) (hf : f.Finite), ZariskisMainProperty R p
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S :=
  f.comp
    (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →ₐ[R] MvPolynomial (Fin (n + 1)) R)
this_1 : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this_3 : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this : ZariskisMainProperty (MvPolynomial (Fin n) R) p
succ :
  ∀ (r : S) (hrp : r ∉ p) (hr : IsIntegral (MvPolynomial (Fin n) R) r) (m : (x : S) → ℕ)
    (hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)), ZariskisMainProperty R p
⊢ ZariskisMainProperty R p

Tactic:
choose r hrp hr m hm using zariskisMainProperty_iff.mp this

Premises used: Algebra.zariskisMainProperty_iff, Iff.mp
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S) (hf : f.Finite), ZariskisMainProperty R p
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S :=
  f.comp
    (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →ₐ[R] MvPolynomial (Fin (n + 1)) R)
this_1 : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this_3 : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
rw :
  RingHom.FiniteType
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : MvPolynomial (Fin (n + 1)) R →+* S)
      (algebraMap R (MvPolynomial (Fin (n + 1)) R)))
⊢ FiniteType R S

Tactic:
rw [← RingHom.finiteType_algebraMap, ← f.comp_algebraMap]

Premises used: RingHom.finiteType_algebraMap, AlgHom.comp_algebraMap
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S) (hf : f.Finite), ZariskisMainProperty R p
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S :=
  f.comp
    (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →ₐ[R] MvPolynomial (Fin (n + 1)) R)
this_1 : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this_3 : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
⊢ RingHom.FiniteType
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : MvPolynomial (Fin (n + 1)) R →+* S)
      (algebraMap R (MvPolynomial (Fin (n + 1)) R)))

Tactic:
RingHom.FiniteType.comp hf.finiteType (RingHom.finiteType_algebraMap.mpr inferInstance)

Premises used: Iff.mpr, RingHom.finiteType_algebraMap, AlgHom.Finite.finiteType, inferInstance, RingHom.FiniteType.comp
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S) (hf : f.Finite), ZariskisMainProperty R p
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S :=
  f.comp
    (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →ₐ[R] MvPolynomial (Fin (n + 1)) R)
this_1 : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this_3 : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
⊢ RingHom.FiniteType
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : MvPolynomial (Fin (n + 1)) R →+* S)
      (algebraMap R (MvPolynomial (Fin (n + 1)) R)))

Tactic:
exact RingHom.FiniteType.comp hf.finiteType (RingHom.finiteType_algebraMap.mpr inferInstance)

Premises used: Iff.mpr, RingHom.finiteType_algebraMap, AlgHom.Finite.finiteType, inferInstance, RingHom.FiniteType.comp
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S) (hf : f.Finite), ZariskisMainProperty R p
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S :=
  f.comp
    (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →ₐ[R] MvPolynomial (Fin (n + 1)) R)
this_1 : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this_3 : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
succ : ∀ (s : Finset S) (hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤), ZariskisMainProperty R p
⊢ ZariskisMainProperty R p

Tactic:
obtain ⟨⟨s, hs⟩⟩ : Algebra.FiniteType R S := by
      rw [← RingHom.finiteType_algebraMap, ← f.comp_algebraMap]
      exact RingHom.FiniteType.comp hf.finiteType (RingHom.finiteType_algebraMap.mpr inferInstance)

Premises used: Algebra.FiniteType