awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this_2 : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
H :
  Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
q : R'[X]
hq :
  IsIntegral R'
    (HSub.hSub (α := S') (β := S') ((algebraMap S S' : (a : S) → S') t : S')
      (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S') q :
        S'))
n : ℕ
q' : R[X]
e : map (algebraMap R R') q' = HSMul.hSMul (α := R) ((fun (x : ℕ) ↦ a ^ x) n) q
this :
  IsIntegral R' (A := S')
    ((algebraMap S S' : (a : S) → S') (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q' : S)) : S')
m : ℕ
hm :
  IsIntegral R (A := S')
    ((algebraMap S S' : (a : S) → S')
        (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ m) : S)
          (HSub.hSub (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ n) : S) t)
            ((φ : (a : R[X]) → S) q' : S))) :
      S')
k : ℕ
hk :
  IsIntegral R
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((fun (x : ℕ) ↦ a ^ x) k)
      (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ m) : S)
        (HSub.hSub (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ n) : S) t)
          ((φ : (a : R[X]) → S) q' : S))))
⊢ IsIntegral R
    (HSub.hSub (β := S) (a ^ (k + m + n) • t)
      ((φ : (a : R[X]) → S) (HPow.hPow (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (k + m) * q') : S))
have h : HSub.hSub (β := S) (a ^ (k + m + n) • t)
    ((φ : (a : R[X]) → S) (HPow.hPow (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (k + m) * q') : S) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((fun (x : ℕ) ↦ a ^ x) k)
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ m) : S)
      (HSub.hSub (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ n) : S) t)
        ((φ : (a : R[X]) → S) q' : S)))
Tactic: convert! hk using 1
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
ht : φ.IsIntegralElem t
hp : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) a : S)
this_1 : Algebra R' S' := RingHom.toAlgebra (Localization.awayMap (algebraMap R S) a)
this_2 : IsScalarTower R R' S'
ha : IsUnit (M := R') ((algebraMap R R' : (a : R) → R') a : R')
H :
  Eq (α := RingHom.{u_1, u_2} R[X] S')
    (RingHom.comp (AlgHom.toRingHom (R := R') (aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X))))
        (mapRingHom (algebraMap R R')) :
      RingHom.{u_1, u_2} R[X] S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (↑φ : R[X] →+* S) :
      RingHom.{u_1, u_2} R[X] S')
q : R'[X]
hq :
  IsIntegral R'
    (HSub.hSub (α := S') (β := S') ((algebraMap S S' : (a : S) → S') t : S')
      (((aeval ((algebraMap S S' : (a : S) → S') ((φ : (a : R[X]) → S) X)) : R'[X] →ₐ[R'] S') : (a : R'[X]) → S') q :
        S'))
n : ℕ
q' : R[X]
e : map (algebraMap R R') q' = HSMul.hSMul (α := R) ((fun (x : ℕ) ↦ a ^ x) n) q
this :
  IsIntegral R' (A := S')
    ((algebraMap S S' : (a : S) → S') (HSub.hSub (β := S) (a ^ n • t) ((φ : (a : R[X]) → S) q' : S)) : S')
m : ℕ
hm :
  IsIntegral R (A := S')
    ((algebraMap S S' : (a : S) → S')
        (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ m) : S)
          (HSub.hSub (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ n) : S) t)
            ((φ : (a : R[X]) → S) q' : S))) :
      S')
k : ℕ
hk :
  IsIntegral R
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((fun (x : ℕ) ↦ a ^ x) k)
      (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ m) : S)
        (HSub.hSub (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ n) : S) t)
          ((φ : (a : R[X]) → S) q' : S))))
⊢ HSub.hSub (β := S) (a ^ (k + m + n) • t)
      ((φ : (a : R[X]) → S) (HPow.hPow (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (k + m) * q') : S) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((fun (x : ℕ) ↦ a ^ x) k)
      (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ m) : S)
        (HSub.hSub (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (a ^ n) : S) t)
          ((φ : (a : R[X]) → S) q' : S)))
have h : HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) a : S) (k + m + n) * t -
    HMul.hMul (β := S) (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) a : S) (k + m))
      ((φ : (a : R[X]) → S) q' : S) =
  HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) a : S) k *
    (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) a : S) m *
      HSub.hSub (β := S) (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) a : S) n * t)
        ((φ : (a : R[X]) → S) q' : S))
Tactic: simp only [Algebra.smul_def, map_pow, ← Polynomial.algebraMap_eq, map_mul, AlgHom.commutes]
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
⊢ ∃ (n : ℕ), Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) (p.leadingCoeff ^ n • t)
have algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
Tactic: algebraize [φ.toRingHom]
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
⊢ ∃ (n : ℕ), Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) (p.leadingCoeff ^ n • t)
have this : IsScalarTower R R[X] S
Tactic: have : IsScalarTower R R[X] S := .of_algebraMap_eq' φ.comp_algebraMap.symm
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this : IsScalarTower R R[X] S
x : S
⊢ ∃ (n : ℕ), p.leadingCoeff ^ n • (t * x) ∈ φ.range
have this₁ : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t * x ∈ φ.range
Tactic: have : φ p * t * x ∈ φ.range := by simpa [← AlgHom.map_adjoin_singleton] using hp x
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this_1 : IsScalarTower R R[X] S
x : S
this : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t * x ∈ φ.range
⊢ HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) (t * x) ∈ φ.range
have h : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) (t * x) = HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t * x
Tactic: convert! this using 1
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this_1 : IsScalarTower R R[X] S
x : S
this : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t * x ∈ φ.range
⊢ ∃ (n : ℕ), p.leadingCoeff ^ n • (t * x) ∈ φ.range
have obtain : ∀ (q : R[X]) (n : ℕ)
  (hn : IsIntegral R (HSub.hSub (β := S) (p.leadingCoeff ^ n • (t * x)) ((φ : (a : R[X]) → S) q : S))),
  ∃ (n : ℕ), p.leadingCoeff ^ n • (t * x) ∈ φ.range
Tactic: obtain ⟨q, n, hn⟩ :=
      exists_isIntegral_leadingCoeff_pow_smul_sub_of_isIntegralElem_of_mul_mem_range φ _ p
        (hφ.to_isIntegral (t * x)) (by convert! this using 1; ring)
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this_1 : IsScalarTower R R[X] S
x : S
this : HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t * x ∈ φ.range
q : R[X]
n : ℕ
hn : IsIntegral R (HSub.hSub (β := S) (p.leadingCoeff ^ n • (t * x)) ((φ : (a : R[X]) → S) q : S))
⊢ ∃ (n : ℕ), p.leadingCoeff ^ n • (t * x) ∈ φ.range
have obtain : ∀ (r : R)
  (hr :
    (algebraMap R S : (a : R) → S) r = HSub.hSub (β := S) (p.leadingCoeff ^ n • (t * x)) ((φ : (a : R[X]) → S) q : S)),
  ∃ (n : ℕ), p.leadingCoeff ^ n • (t * x) ∈ φ.range
Tactic: obtain ⟨r, hr : algebraMap _ _ r = _⟩ := hRS.le hn
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this : IsScalarTower R R[X] S
⊢ ∃ (n : ℕ), Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) (p.leadingCoeff ^ n • t)
have this₁ : ∀ (x : S), ∃ (n : ℕ), p.leadingCoeff ^ n • (t * x) ∈ φ.range
Tactic: have (x : _) : ∃ n, p.leadingCoeff ^ n • (t * x) ∈ φ.range := by
    have : φ p * t * x ∈ φ.range := by simpa [← AlgHom.map_adjoin_singleton] using hp x
    obtain ⟨q, n, hn⟩ :=
      exists_isIntegral_leadingCoeff_pow_smul_sub_of_isIntegralElem_of_mul_mem_range φ _ p
        (hφ.to_isIntegral (t * x)) (by convert! this using 1; ring)
    obtain ⟨r, hr : algebraMap _ _ r = _⟩ := hRS.le hn
    exact ⟨n, (C r + q), by simp [← Polynomial.algebraMap_eq, - Polynomial.algebraMap_apply, hr]⟩
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this_1 : IsScalarTower R R[X] S
this : ∀ (x : S), ∃ (n : ℕ), p.leadingCoeff ^ n • (t * x) ∈ φ.range
⊢ ∃ (n : ℕ), Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) (p.leadingCoeff ^ n • t)
have choose : ∀ (n : (x : S) → ℕ) (hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range),
  ∃ (n : ℕ), Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) (p.leadingCoeff ^ n • t)
Tactic: choose n hn using this
Cleared hypotheses: this
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this : IsScalarTower R R[X] S
n : (x : S) → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
⊢ ∃ (n : ℕ), Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) (p.leadingCoeff ^ n • t)
have obtain : ∀ (s : Finset S) (hs : Eq (α := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) ⊤),
  ∃ (n : ℕ), Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) (p.leadingCoeff ^ n • t)
Tactic: obtain ⟨s, hs⟩ := Module.Finite.fg_top (R := R[X]) (M := S)
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this : IsScalarTower R R[X] S
n : (x : S) → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Eq (α := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) ⊤
⊢ ∃ (n : ℕ), Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S) (p.leadingCoeff ^ n • t)
have refine : ∀ (x : S), Membership.mem (γ := Subalgebra R S) R[((φ : (a : R[X]) → S) X : S)] (p.leadingCoeff ^ s.sup n • t * x)
Tactic: refine ⟨s.sup n, fun x ↦ ?_⟩
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this : IsScalarTower R R[X] S
n : (x : S) → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Eq (α := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) ⊤
x : S
⊢ Membership.mem (γ := Subalgebra R S) R[((φ : (a : R[X]) → S) X : S)] (p.leadingCoeff ^ s.sup n • t * x)
have rw : p.leadingCoeff ^ s.sup n • (t * x) ∈ φ.range
Tactic: rw [← AlgHom.map_adjoin_singleton, adjoin_X, Algebra.map_top, Algebra.smul_mul_assoc]
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this : IsScalarTower R R[X] S
n : (x : S) → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Eq (α := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) ⊤
x_1 x : S
h : x ∈ (↑s : Set S)
⊢ p.leadingCoeff ^ s.sup n • (t * x) ∈ φ.range
have mem : p.leadingCoeff ^ (s.sup n - n x) • p.leadingCoeff ^ n x • (t * x) ∈ φ.range
Tactic: rw [← Nat.sub_add_cancel (s.le_sup h), pow_add, mul_smul]
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this : IsScalarTower R R[X] S
n : (x : S) → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Eq (α := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) ⊤
x_1 : S
a : R[X]
x : S
hx : Membership.mem (γ := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) x
IH : p.leadingCoeff ^ s.sup n • (t * x) ∈ φ.range
⊢ p.leadingCoeff ^ s.sup n • (t * a • x) ∈ φ.range
have smul : HMul.hMul (α := S) ((algebraMap R[X] S : (a : R[X]) → S) a : S) (p.leadingCoeff ^ s.sup n • (t * x)) ∈ φ.range
Tactic: rw [mul_smul_comm, smul_comm, Algebra.smul_def]
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (conductor R ((φ : (a : R[X]) → S) X) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
algInst : Algebra.{u_1, u_2} R[X] S := φ.toAlgebra
algebraizeInst : Module.Finite.{u_1, u_2} R[X] S
this : IsScalarTower R R[X] S
n : (x : S) → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Eq (α := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) ⊤
x : S
⊢ p.leadingCoeff ^ s.sup n • (t * x) ∈ φ.range
have x₁ : Membership.mem (γ := Submodule.{u_1, u_2} R[X] S) (Submodule.span R[X] (↑s : Set S)) x
Tactic: induction hs.ge (Set.mem_univ x) using Submodule.span_induction with
  | mem x h =>
    rw [← Nat.sub_add_cancel (s.le_sup h), pow_add, mul_smul]
    exact Subalgebra.smul_mem _ (hn _) _
  | zero => simp
  | add x y _ _ hx hy => simpa only [mul_add, smul_add] using add_mem hx hy
  | smul a x hx IH =>
    rw [mul_smul_comm, smul_comm, Algebra.smul_def]
    exact mul_mem (AlgHom.mem_range_self _ _) IH
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
i : ℕ
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
have inr : ∀
  (this :
    ∀ (p : R[X])
      (hp :
        Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
          (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
      (i : ℕ) (hi : i = p.natDegree),
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t))
  (hi : ¬i = p.natDegree),
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
Tactic: wlog hi : i = p.natDegree generalizing p i
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
i : ℕ
inr :
  ∀
    (this :
      ∀ (p : R[X])
        (hp :
          Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
            (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
        (i : ℕ) (hi : i = p.natDegree),
        Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t))
    (hi : ¬i = p.natDegree),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
have wlog : ∀ (p : R[X])
  (hp :
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
      (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
  (i : ℕ) (hi : i = p.natDegree),
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
Tactic: wlog hi : i = p.natDegree generalizing p i
Cleared hypotheses: hp, i
-- 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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : Eq (α := Subalgebra R S) (integralClosure R S) ⊥
hφ : φ.Finite
hp :
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
    (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)
i : ℕ
this :
  ∀ (p : R[X])
    (hp :
      Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
        (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t))
    (i : ℕ) (hi : i = p.natDegree),
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
⊢ Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.coeff i • t)
have this₁ : ∀ (p : R[X])
  (hp :
    Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S)
      (HMul.hMul (α := S) ((φ : (a : R[X]) → S) p : S) t)),
  Membership.mem (γ := Ideal S) (Ideal.radical (conductor R ((φ : (a : R[X]) → S) X)) : Ideal S) (p.leadingCoeff • t)
Tactic: simp only [forall_eq, coeff_natDegree] at this
Cleared hypotheses: this