awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.ZMod (goal)
Goal:
n : ℕ
⊢ IsReduced (ZMod n) ↔ Squarefree n ∨ n = 0
have rw : Ideal.IsRadical (RingHom.ker (F := ℤ →+* ZMod n) (Int.castRingHom (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]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod (goal)
Goal:
n : ℕ
rw : Ideal.IsRadical (RingHom.ker (F := ℤ →+* ZMod n) (Int.castRingHom (ZMod n))) ↔ Squarefree n ∨ n = 0
⊢ IsReduced (ZMod n) ↔ Squarefree n ∨ n = 0
have rw₁ : Ideal.IsRadical (R := ℤ) (Ideal.span {(↑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]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod (goal)
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
⊢ IsReduced (ZMod n) ↔ Squarefree n ∨ n = 0
have rw₂ : IsRadical (R := ℤ) (↑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]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod (goal)
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
⊢ IsReduced (ZMod n) ↔ Squarefree n ∨ n = 0
have rw₃ : Squarefree (R := ℤ) (↑n : ℤ) ∨ Eq (α := ℤ) (↑n : ℤ) 0 ↔ 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]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod (goal)
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
⊢ IsReduced (ZMod n) ↔ Squarefree n ∨ n = 0
have rw₄ : Squarefree n ∨ Eq (α := ℤ) (↑n : ℤ) 0 ↔ 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]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod (goal)
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
⊢ IsReduced (ZMod n) ↔ Squarefree n ∨ n = 0
have rw₅ : Squarefree n ∨ n = 0 ↔ 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]
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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, IsIntegral R r ∧ ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
have 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 sorry))
      (β :=
      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 sorry) :
          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 sorry)) :
        (a_1 : Localization.Away ⟨a, sorry⟩) →
          Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) ⟨a, sorry⟩))) ↔
  ∃ (r : S) (_ : IsIntegral R r) (_ : r ∉ p), ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
Tactic: simp only [ZariskisMainProperty, Subtype.exists, ← exists_prop, @exists_comm (_ ∉ p)]
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)
have 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 sorry))
      (β :=
      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 sorry) :
          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 sorry)) :
        (a : Localization.Away ⟨r, sorry⟩) →
          Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) ⟨r, sorry⟩)) ↔
    ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
Tactic: refine exists₃_congr fun r hr hrp ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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.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)
have 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 sorry) :
              S)
            m *
          a) ↔
  ∀ (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]
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)
have refine : ∀ (r : S) (hrp : r ∉ p) (H : ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)), IsIntegral R r
Tactic: refine zariskisMainProperty_iff.trans (exists_congr fun r ↦ and_congr_right fun hrp ↦
    and_iff_right_of_imp fun H ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)
⊢ IsIntegral R r
have obtain : ∀ (n : ℕ) (hn : IsIntegral R (r ^ n * r)), IsIntegral R r
Tactic: obtain ⟨n, hn⟩ := H r
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (hypothesis)
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
have hn₁ : IsIntegral R (r ^ (n + 1))
Tactic: rw [← pow_succ] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
⊢ ZariskisMainProperty R p
have rw : ∀ (H : ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral S (r ^ m * x)), ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
Tactic: rw [zariskisMainProperty_iff'] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)
⊢ ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
have 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)
Tactic: obtain ⟨r, hrp, H⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (hypothesis)
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)
⊢ ZariskisMainProperty R p
have h₃ : ∃ r ∉ Ideal.under S p, IsIntegral R r ∧ ∀ (x : S), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
Tactic: rw [zariskisMainProperty_iff] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)
⊢ ZariskisMainProperty R p
have rw : ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
Tactic: rw [zariskisMainProperty_iff']
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)
⊢ ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
have 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)
Tactic: obtain ⟨s, hsp, hs, Hs⟩ := h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)
⊢ ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
have 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)) sorry : Subalgebra S T)
      (⊤ : Subalgebra S T)),
  ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
Tactic: obtain ⟨t, htp, Ht⟩ := h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)
⊢ ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
have obtain : ∀ (m : ℕ) (hm : IsIntegral R (s ^ m * t)), ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
Tactic: obtain ⟨m, hm⟩ := Hs t
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)
have refine_1 : ((algebraMap S T : (a : S) → T) (s ^ (m + 1) * t) : T) ∉ p
Tactic: refine ⟨algebraMap _ _ (s ^ (m + 1) * t), ?_, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
⊢ ∃ r ∉ p, ∀ (x : T), ∃ (m : ℕ), IsIntegral R (r ^ m * x)
have 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)
Tactic: refine ⟨algebraMap _ _ (s ^ (m + 1) * t), ?_, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
⊢ ∃ (m_1 : ℕ), IsIntegral R (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) (s ^ (m + 1) * t) : T) m_1 * x)
have 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)
Tactic: obtain ⟨_, ⟨n, rfl⟩, a, ha⟩ := Ht.ge (Set.mem_univ x)
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
⊢ ∃ (m_1 : ℕ), IsIntegral R (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) (s ^ (m + 1) * t) : T) m_1 * x)
have 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)
Tactic: obtain ⟨k, hk⟩ := Hs a
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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)
have refine_2 : IsIntegral R (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) (s ^ (m + 1) * t) : T) (k + n) * x)
Tactic: refine ⟨k + n, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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 R (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) (s ^ (m + 1) * t) : T) (k + n) * x)
have 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))
Tactic: convert_to IsIntegral R (algebraMap S T ((s ^ ((m + 1) * n) * (s ^ m * t) ^ k * (s ^ k * a))))
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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))
⊢ IsIntegral R (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) (s ^ (m + 1) * t) : T) (k + n) * x)
have 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)
Tactic: convert_to IsIntegral R (algebraMap S T ((s ^ ((m + 1) * n) * (s ^ m * t) ^ k * (s ^ k * a))))