awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.ZMod
Goal:
n : ℕ
R : Type u_1
inst : Ring R
f g : R →+* ZMod n
h : Eq (α := Ideal R) (RingHom.ker f) (RingHom.ker g)
this :
  RingHom.comp
      (((f.liftOfRightInverse cast ⋯ :
            { g : R →+* ZMod n // LE.le (α := Ideal R) (RingHom.ker f) (RingHom.ker g) } ≃ (ZMod n →+* ZMod n)) :
          (a : { g : R →+* ZMod n // RingHom.ker f ≤ RingHom.ker g }) → ZMod n →+* ZMod n)
        (Subtype.mk (p := fun (g : R →+* ZMod n) ↦ LE.le (α := Ideal R) (RingHom.ker f) (RingHom.ker g)) g ⋯))
      f =
    (↑(Subtype.mk (p := fun (g : R →+* ZMod n) ↦ LE.le (α := Ideal R) (RingHom.ker f) (RingHom.ker g)) g ⋯) :
      R →+* ZMod n)
⊢ RingHom.comp
      (((f.liftOfRightInverse cast ⋯ :
            { g : R →+* ZMod n // LE.le (α := Ideal R) (RingHom.ker f) (RingHom.ker g) } ≃ (ZMod n →+* ZMod n)) :
          (a : { g : R →+* ZMod n // RingHom.ker f ≤ RingHom.ker g }) → ZMod n →+* ZMod n)
        (Subtype.mk (p := fun (g : R →+* ZMod n) ↦ LE.le (α := Ideal R) (RingHom.ker f) (RingHom.ker g)) g ⋯))
      f =
    g

Tactic:
rw [Subtype.coe_mk] at this

Premises used: Subtype.coe_mk
-- Module: Mathlib.RingTheory.ZMod
Goal:
n : ℕ
R : Type u_1
inst : Ring R
f g : R →+* ZMod n
h : Eq (α := Ideal R) (RingHom.ker f) (RingHom.ker g)
this :
  RingHom.comp
      (((f.liftOfRightInverse cast ⋯ :
            { g : R →+* ZMod n // LE.le (α := Ideal R) (RingHom.ker f) (RingHom.ker g) } ≃ (ZMod n →+* ZMod n)) :
          (a : { g : R →+* ZMod n // RingHom.ker f ≤ RingHom.ker g }) → ZMod n →+* ZMod n)
        (Subtype.mk (p := fun (g : R →+* ZMod n) ↦ LE.le (α := Ideal R) (RingHom.ker f) (RingHom.ker g)) g ⋯))
      f =
    g
rw :
  f =
    RingHom.comp
      (((f.liftOfRightInverse cast ⋯ :
            { g : R →+* ZMod n // LE.le (α := Ideal R) (RingHom.ker f) (RingHom.ker g) } ≃ (ZMod n →+* ZMod n)) :
          (a : { g : R →+* ZMod n // RingHom.ker f ≤ RingHom.ker g }) → ZMod n →+* ZMod n)
        (Subtype.mk (p := fun (g : R →+* ZMod n) ↦ LE.le (α := Ideal R) (RingHom.ker f) (RingHom.ker g)) g ⋯))
      f
rw₁ : f = RingHom.comp (RingHom.id (ZMod n)) f
rw₂ : ZMod n →+* ZMod n
rw₃ rw₄ : f = f
⊢ f = g

Tactic:
rw [← this, RingHom.ext_zmod (f.liftOfRightInverse _ _ ⟨g, _⟩) _, RingHom.id_comp]

Premises used: RingHom.liftOfRightInverse, Subtype.mk, RingHom.ext_zmod, DFunLike.coe, RingHom.id_comp
-- Module: Mathlib.RingTheory.ZMod
Goal:
n : ℕ
rw : Ideal.IsRadical (RingHom.ker (F := ℤ →+* ZMod n) (Int.castRingHom (ZMod n))) ↔ Squarefree n ∨ n = 0
rw₁ : Ideal.IsRadical (R := ℤ) (Ideal.span {(↑n : ℤ)}) ↔ Squarefree n ∨ n = 0
rw₂ : IsRadical (R := ℤ) (↑n : ℤ) ↔ Squarefree n ∨ n = 0
rw₃ : Squarefree (R := ℤ) (↑n : ℤ) ∨ Eq (α := ℤ) (↑n : ℤ) 0 ↔ Squarefree n ∨ n = 0
rw₄ : Squarefree n ∨ Eq (α := ℤ) (↑n : ℤ) 0 ↔ Squarefree n ∨ n = 0
rw₅ rw₆ : Squarefree n ∨ n = 0 ↔ Squarefree n ∨ n = 0
⊢ IsReduced (ZMod n) ↔ Squarefree n ∨ n = 0

Tactic:
rw [← RingHom.ker_isRadical_iff_reduced_of_surjective
      (ZMod.ringHom_surjective <| Int.castRingHom <| ZMod n),
      ZMod.ker_intCastRingHom, ← isRadical_iff_span_singleton, isRadical_iff_squarefree_or_zero,
      Int.squarefree_natCast, Nat.cast_eq_zero]

Premises used: RingHom.ker_isRadical_iff_reduced_of_surjective, isRadical_iff_squarefree_or_zero, isRadical_iff_span_singleton, ZMod, ZMod.ringHom_surjective, Nat.cast_eq_zero, Int.castRingHom, ZMod.ker_intCastRingHom, Int.squarefree_natCast
-- Module: Mathlib.RingTheory.ZMod
Goal:
n : ℕ
inst : Fact (Squarefree n)
⊢ IsReduced (ZMod n)

Tactic:
isReduced_zmod.2 <| Or.inl <| Fact.out

Premises used: Iff.mpr, isReduced_zmod, Or.inl, Fact.out
-- 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
simp :
  (∃ (a : S) (h : Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) (_ : a ∉ p),
      Function.Bijective (α :=
        Localization.Away
          (Subtype.mk (p := fun (a : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) a ⋯))
        (β :=
        Localization.Away (M := S)
          ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S)
              (Subtype.mk (p := fun (a : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) a ⋯) :
            S))
        (⇑(Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S)))
              (Subtype.mk (p := fun (a : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) a ⋯)) :
          (a_1 : Localization.Away ⟨a, ⋯⟩) →
            Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) ⟨a, ⋯⟩))) ↔
    ∃ (r : S) (_ : IsIntegral R r) (_ : r ∉ p), ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
⊢ ZariskisMainProperty R p ↔ ∃ r ∉ p, IsIntegral R r ∧ ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)

Tactic:
simp only [ZariskisMainProperty, Subtype.exists, ← exists_prop, @exists_comm (_ ∉ p)]

Premises used: Subtype.exists, exists_prop, Algebra.ZariskisMainProperty, exists_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
p : Ideal S
⊢ (∃ (a : S) (h : Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) (_ : a ∉ p),
      Function.Bijective (α :=
        Localization.Away
          (Subtype.mk (p := fun (a : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) a ⋯))
        (β :=
        Localization.Away (M := S)
          ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S)
              (Subtype.mk (p := fun (a : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) a ⋯) :
            S))
        (⇑(Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S)))
              (Subtype.mk (p := fun (a : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) a ⋯)) :
          (a_1 : Localization.Away ⟨a, ⋯⟩) →
            Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) ⟨a, ⋯⟩))) ↔
    ∃ (r : S) (_ : IsIntegral R r) (_ : r ∉ p), ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)

Tactic:
exists₃_congr fun r hr hrp ↦ ?_

Premises used: Set.Mem, setOf, RingHom.IsIntegralElem, IsIntegral, exists₃_congr
-- 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
refine :
  ∀ (r : S) (hr : Membership.mem (γ := Subalgebra R S) (integralClosure R S) r) (hrp : r ∉ p),
    Function.Bijective (α :=
        Localization.Away
          (Subtype.mk (p := fun (a : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) r ⋯))
        (β :=
        Localization.Away (M := S)
          ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S)
              (Subtype.mk (p := fun (a : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) r ⋯) :
            S))
        (⇑(Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S)))
              (Subtype.mk (p := fun (a : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) r ⋯)) :
          (a : Localization.Away ⟨r, ⋯⟩) →
            Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) ⟨r, ⋯⟩)) ↔
      ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
⊢ (∃ (a : S) (h : Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) (_ : a ∉ p),
      Function.Bijective (α :=
        Localization.Away
          (Subtype.mk (p := fun (a : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) a ⋯))
        (β :=
        Localization.Away (M := S)
          ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S)
              (Subtype.mk (p := fun (a : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) a ⋯) :
            S))
        (⇑(Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S)))
              (Subtype.mk (p := fun (a : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) a ⋯)) :
          (a_1 : Localization.Away ⟨a, ⋯⟩) →
            Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) ⟨a, ⋯⟩))) ↔
    ∃ (r : S) (_ : IsIntegral R r) (_ : r ∉ p), ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)

Tactic:
refine exists₃_congr fun r hr hrp ↦ ?_

Premises used: exists₃_congr
-- 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
r : S
hr : Membership.mem (γ := Subalgebra R S) (integralClosure R S) r
hrp : r ∉ p
⊢ Function.Injective (α :=
    Localization.Away
      (Subtype.mk (p := fun (a : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) r ⋯))
    (β :=
    Localization.Away (M := S)
      ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S)
          (Subtype.mk (p := fun (a : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) r ⋯) :
        S))
    (⇑(Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S)))
          (Subtype.mk (p := fun (a : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) r ⋯)) :
      (a : Localization.Away ⟨r, ⋯⟩) →
        Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) ⟨r, ⋯⟩))

Tactic:
IsLocalization.map_injective_of_injective _ _ _ Subtype.val_injective

Premises used: IsLocalization.map_injective_of_injective
-- 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
r : S
hr : Membership.mem (γ := Subalgebra R S) (integralClosure R S) r
hrp : r ∉ p
⊢ Function.Injective (α :=
    Localization.Away
      (Subtype.mk (p := fun (a : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) r ⋯))
    (β :=
    Localization.Away (M := S)
      ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S)
          (Subtype.mk (p := fun (a : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) r ⋯) :
        S))
    (⇑(Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S)))
          (Subtype.mk (p := fun (a : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) r ⋯)) :
      (a : Localization.Away ⟨r, ⋯⟩) →
        Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) ⟨r, ⋯⟩))

Tactic:
exact IsLocalization.map_injective_of_injective _ _ _ Subtype.val_injective

Premises used: IsLocalization.map_injective_of_injective
-- 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
r : S
hr : Membership.mem (γ := Subalgebra R S) (integralClosure R S) r
hrp : r ∉ p
rw :
  (∀ (a : S),
      ∃ (b : ↥(integralClosure R S)) (m : ℕ),
        (AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) b =
          HPow.hPow (α := S)
              ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S)
                  (Subtype.mk (p := fun (a : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) r ⋯) :
                S)
              m *
            a) ↔
    ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
⊢ Function.Bijective (α :=
      Localization.Away
        (Subtype.mk (p := fun (a : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) r ⋯))
      (β :=
      Localization.Away (M := S)
        ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S)
            (Subtype.mk (p := fun (a : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) r ⋯) :
          S))
      (⇑(Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S)))
            (Subtype.mk (p := fun (a : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) r ⋯)) :
        (a : Localization.Away ⟨r, ⋯⟩) →
          Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) ⟨r, ⋯⟩)) ↔
    ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)

Tactic:
rw [Function.Bijective, and_iff_right
    (by exact IsLocalization.map_injective_of_injective _ _ _ Subtype.val_injective),
    Localization.awayMap_surjective_iff]

Premises used: Localization.awayMap_surjective_iff, and_iff_right, Function.Bijective
-- 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
r : S
hr : Membership.mem (γ := Subalgebra R S) (integralClosure R S) r
hrp : r ∉ p
⊢ (∀ (a : S),
      ∃ (b : ↥(integralClosure R S)) (m : ℕ),
        (AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) b =
          HPow.hPow (α := S)
              ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S)
                  (Subtype.mk (p := fun (a : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) a) r ⋯) :
                S)
              m *
            a) ↔
    ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)

Tactic:
simp [mem_integralClosure_iff]

Premises used: mem_integralClosure_iff
-- 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
⊢ ZariskisMainProperty R p ↔ ∃ r ∉ p, ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)

Tactic:
zariskisMainProperty_iff.trans (exists_congr fun r ↦ and_congr_right fun hrp ↦
    and_iff_right_of_imp fun H ↦ ?_)

Premises used: Algebra.zariskisMainProperty_iff, and_congr_right, exists_congr, Iff.trans, and_iff_right_of_imp
-- 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
refine : ∀ (r : S) (hrp : r ∉ p) (H : ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)), IsIntegral R r
⊢ ZariskisMainProperty R p ↔ ∃ r ∉ p, ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)

Tactic:
refine zariskisMainProperty_iff.trans (exists_congr fun r ↦ and_congr_right fun hrp ↦
    and_iff_right_of_imp fun H ↦ ?_)

Premises used: Algebra.zariskisMainProperty_iff, and_congr_right, exists_congr, Iff.trans, and_iff_right_of_imp
-- 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
r : S
hrp : r ∉ p
H : ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
obtain : ∀ (n : ℕ) (hn : IsIntegral R (r ^ n * r)), IsIntegral R r
⊢ IsIntegral R r

Tactic:
obtain ⟨n, hn⟩ := H r
-- 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
r : S
hrp : r ∉ p
H : ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
n : ℕ
hn : IsIntegral R (r ^ n * r)
⊢ IsIntegral R (r ^ (n + 1))

Tactic:
rw [← pow_succ] at hn

Premises used: pow_succ
-- 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
r : S
hrp : r ∉ p
H : ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
n : ℕ
hn : IsIntegral R (r ^ (n + 1))
⊢ 0 < n + 1

Tactic:
simp
-- 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
r : S
hrp : r ∉ p
H : ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
n : ℕ
hn : IsIntegral R (r ^ (n + 1))
⊢ IsIntegral R r

Tactic:
exact (IsIntegral.pow_iff (by simp)).mp hn

Premises used: IsIntegral.pow_iff, Iff.mp
-- 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
p : Ideal S
r : S
h : IsIntegral R r
⊢ LE.le (α := Submonoid S) (Submonoid.powers r)
    (Subsemiring.toSubmonoid (Subalgebra.toSubsemiring (integralClosure R S)))

Tactic:
simpa [Submonoid.powers_le]

Premises used: Submonoid.powers_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
p : Ideal S
⊢ ZariskisMainProperty R p ↔
    ∃ r ∉ p, ∃ (h : IsIntegral R r), Subalgebra.saturation (integralClosure R S) (Submonoid.powers r) ⋯ = ⊤

Tactic:
simp [zariskisMainProperty_iff, ← top_le_iff, SetLike.le_def,
    Submonoid.mem_powers_iff, mem_integralClosure_iff]

Premises used: Algebra.zariskisMainProperty_iff, SetLike.le_def, mem_integralClosure_iff, top_le_iff, Submonoid.mem_powers_iff
-- 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
inst_7 : Algebra.IsIntegral R S
p : Ideal T
H : ZariskisMainProperty S p
rw :
  ∀ (H : ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral S (r ^ m * x)),
    ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
⊢ ZariskisMainProperty R p

Tactic:
rw [zariskisMainProperty_iff'] at H ⊢

Premises used: Algebra.zariskisMainProperty_iff'
-- 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
inst_7 : Algebra.IsIntegral R S
p : Ideal T
H : ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral S (r ^ m * x)
obtain :
  ∀ (r : T) (hrp : r ∉ p) (H : ∀ (x : T), ∃ (m : ℕ), IsIntegral S (r ^ m * x)),
    ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
⊢ ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral R (r ^ m * x)

Tactic:
obtain ⟨r, hrp, H⟩ := H
-- 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
inst_7 : Algebra.IsIntegral R S
p : Ideal T
r : T
hrp : r ∉ p
H : ∀ (x : T), ∃ (m : ℕ), IsIntegral S (r ^ m * x)
⊢ ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral R (r ^ m * x)

Tactic:
⟨r, hrp, fun x ↦ ⟨_, isIntegral_trans _ (H x).choose_spec⟩⟩

Premises used: Exists.choose_spec, HMul.hMul, isIntegral_trans, HPow.hPow, And.intro, Exists.intro, Exists.choose
-- 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
inst_7 : Algebra.IsIntegral R S
p : Ideal T
r : T
hrp : r ∉ p
H : ∀ (x : T), ∃ (m : ℕ), IsIntegral S (r ^ m * x)
⊢ ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral R (r ^ m * x)

Tactic:
exact ⟨r, hrp, fun x ↦ ⟨_, isIntegral_trans _ (H x).choose_spec⟩⟩
-- 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
h₁ : ZariskisMainProperty R (Ideal.under S p)
r : S
⊢ LE.le.{u_3} (α := Submonoid T) (Submonoid.powers ((algebraMap S T : (a : S) → T) r) : Submonoid T)
    (Subsemiring.toSubmonoid (Subalgebra.toSubsemiring.{u_2, u_3} (R := S) ⊥) : Submonoid T)

Tactic:
simp [Submonoid.powers_le]

Premises used: Submonoid.powers_le
-- 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
h₁ : ZariskisMainProperty R (Ideal.under S p)
h₂ :
  ∃ r ∉ Ideal.under S p,
    Eq.{u_3 + 1} (α := Subalgebra S T)
      (Subalgebra.saturation ⊥ (Submonoid.powers ((algebraMap S T : (a : S) → T) r)) ⋯ : Subalgebra S T)
      (⊤ : Subalgebra S T)
⊢ ∃ r ∉ Ideal.under S p, IsIntegral R r ∧ ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)

Tactic:
rw [zariskisMainProperty_iff] at h₁

Premises used: Algebra.zariskisMainProperty_iff
-- 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
h₁ : ZariskisMainProperty R (Ideal.under S p)
h₂ :
  ∃ r ∉ Ideal.under S p,
    Eq.{u_3 + 1} (α := Subalgebra S T)
      (Subalgebra.saturation ⊥ (Submonoid.powers ((algebraMap S T : (a : S) → T) r)) ⋯ : Subalgebra S T)
      (⊤ : Subalgebra S T)
h₃ : ∃ r ∉ Ideal.under S p, IsIntegral R r ∧ ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
⊢ ∃ r ∉ Ideal.under S p,
    Eq.{u_3 + 1} (α := Subalgebra S T)
      (Subalgebra.saturation ⊥ (Submonoid.powers ((algebraMap S T : (a : S) → T) r)) ⋯ : Subalgebra S T)
      (⊤ : Subalgebra S T)

Tactic:
rw [zariskisMainProperty_iff] at h₁

Premises used: Algebra.zariskisMainProperty_iff
-- 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
h₁ : ∃ r ∉ Ideal.under S p, IsIntegral R r ∧ ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
h₂ :
  ∃ r ∉ Ideal.under S p,
    Eq.{u_3 + 1} (α := Subalgebra S T)
      (Subalgebra.saturation ⊥ (Submonoid.powers ((algebraMap S T : (a : S) → T) r)) ⋯ : Subalgebra S T)
      (⊤ : Subalgebra S T)
rw : ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
⊢ ZariskisMainProperty R p

Tactic:
rw [zariskisMainProperty_iff']

Premises used: Algebra.zariskisMainProperty_iff'
-- 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
h₁ : ∃ r ∉ Ideal.under S p, IsIntegral R r ∧ ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
h₂ :
  ∃ r ∉ Ideal.under S p,
    Eq.{u_3 + 1} (α := Subalgebra S T)
      (Subalgebra.saturation ⊥ (Submonoid.powers ((algebraMap S T : (a : S) → T) r)) ⋯ : Subalgebra S T)
      (⊤ : Subalgebra S T)
obtain :
  ∀ (s : S) (hsp : s ∉ Ideal.under S p) (hs : IsIntegral R s) (Hs : ∀ (x : S), ∃ (m : ℕ), IsIntegral R (s ^ m * x)),
    ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
⊢ ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral R (r ^ m * x)

Tactic:
obtain ⟨s, hsp, hs, Hs⟩ := h₁
-- 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
h₂ :
  ∃ r ∉ Ideal.under S p,
    Eq.{u_3 + 1} (α := Subalgebra S T)
      (Subalgebra.saturation ⊥ (Submonoid.powers ((algebraMap S T : (a : S) → T) r)) ⋯ : Subalgebra S T)
      (⊤ : Subalgebra S T)
s : S
hsp : s ∉ Ideal.under S p
hs : IsIntegral R s
Hs : ∀ (x : S), ∃ (m : ℕ), IsIntegral R (s ^ m * x)
obtain :
  ∀ (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)),
    ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
⊢ ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral R (r ^ m * x)

Tactic:
obtain ⟨t, htp, Ht⟩ := h₂