awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst_7 : p.IsPrime
Q : Ideal S
inst_8 : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (Ideal.comap (F := R →+* SQ) (algebraMap R SQ) (Ideal.map (F := R →+* SQ) (algebraMap R SQ) p)) x
a : S
ha : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (x • a)
haQ : a ∉ Q
f : R[X]
hfm : f.Monic
hfa : Eq.{u_2 + 1} (α := S) ((aeval (x • a) : (a : R[X]) → S) f : S) (0 : S)
hf : ∀ (i : ℕ), i ≠ f.natDegree → f.coeff i ∈ p
⊢ x ∈ p
have exists_ideal_le_liesOver_of_lt : ∀ (i : ℕ) (hi : i ≠ natDegree (minpoly R a)) (hip : coeff (minpoly R a) i ∉ p), x ∈ p
Tactic: obtain ⟨i, hi, hip⟩ : ∃ i ≠ (minpoly R a).natDegree, (minpoly R a).coeff i ∉ p := by
    set g := minpoly R a
    by_contra! H
    have : g.map (Ideal.Quotient.mk p) = X ^ g.natDegree := by
      ext i
      obtain hi | rfl | hi := lt_trichotomy i g.natDegree
      · simpa [hi.ne, Ideal.Quotient.eq_zero_iff_mem] using H _ hi.ne
      · simp [g, minpoly.monic (Algebra.IsIntegral.isIntegral _)]
      · simp [coeff_eq_zero_of_natDegree_lt hi, hi.ne']
    have : Ideal.Quotient.mk (Ideal.map (algebraMap R S) p) (a ^ (minpoly R a).natDegree) = 0 := by
      simpa [← Ideal.Quotient.algebraMap_eq, aeval_algebraMap_apply, g] using
        congr(aeval (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p) a) $this).symm
    exact haQ (‹Q.IsPrime›.mem_of_pow_mem _
      (Ideal.map_le_iff_le_comap.mpr hpQ.le (Ideal.Quotient.eq_zero_iff_mem.mp this)))
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst_7 : p.IsPrime
Q : Ideal S
inst_8 : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (Ideal.comap (F := R →+* SQ) (algebraMap R SQ) (Ideal.map (F := R →+* SQ) (algebraMap R SQ) p)) x
a : S
ha : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (x • a)
haQ : a ∉ Q
f : R[X]
hfm : f.Monic
hfa : Eq.{u_2 + 1} (α := S) ((aeval (x • a) : (a : R[X]) → S) f : S) (0 : S)
hf : ∀ (i : ℕ), i ≠ f.natDegree → f.coeff i ∈ p
i : ℕ
hi : i ≠ natDegree (minpoly R a)
hip : coeff (minpoly R a) i ∉ p
⊢ x ∈ p
have pos : ∀ (hx0 : x = 0), x ∈ p
Tactic: by_cases hx0 : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst_7 : p.IsPrime
Q : Ideal S
inst_8 : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (Ideal.comap (F := R →+* SQ) (algebraMap R SQ) (Ideal.map (F := R →+* SQ) (algebraMap R SQ) p)) x
a : S
ha : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (x • a)
haQ : a ∉ Q
f : R[X]
hfm : f.Monic
hfa : Eq.{u_2 + 1} (α := S) ((aeval (x • a) : (a : R[X]) → S) f : S) (0 : S)
hf : ∀ (i : ℕ), i ≠ f.natDegree → f.coeff i ∈ p
i : ℕ
hi : i ≠ natDegree (minpoly R a)
hip : coeff (minpoly R a) i ∉ p
pos : ∀ (hx0 : x = 0), x ∈ p
⊢ x ∈ p
have neg : ∀ (hx0 : ¬x = 0), x ∈ p
Tactic: by_cases hx0 : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst_7 : p.IsPrime
Q : Ideal S
inst_8 : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (Ideal.comap (F := R →+* SQ) (algebraMap R SQ) (Ideal.map (F := R →+* SQ) (algebraMap R SQ) p)) x
a : S
ha : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (x • a)
haQ : a ∉ Q
f : R[X]
hfm : f.Monic
hfa : Eq.{u_2 + 1} (α := S) ((aeval (x • a) : (a : R[X]) → S) f : S) (0 : S)
hf : ∀ (i : ℕ), i ≠ f.natDegree → f.coeff i ∈ p
i : ℕ
hi : i ≠ natDegree (minpoly R a)
hip : coeff (minpoly R a) i ∉ p
hx0 : ¬x = 0
⊢ x ∈ p
have this₁ : ∀ (i : ℕ) (hi : i ≠ natDegree (minpoly R (x • a))),
  Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {x : R | ∃ i < f.natDegree, f.coeff i = x}))
    (coeff (minpoly R (x • a)) i)
Tactic: have := Polynomial.coeff_mem_radical_span_coeff_of_dvd _ _ hfm
    (minpoly.monic (Algebra.IsIntegral.isIntegral _))
    (minpoly.isIntegrallyClosed_dvd (Algebra.IsIntegral.isIntegral _) hfa)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
this_1 : IsDomain R
p : Ideal R
inst_7 : p.IsPrime
Q : Ideal S
inst_8 : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (Ideal.comap (F := R →+* SQ) (algebraMap R SQ) (Ideal.map (F := R →+* SQ) (algebraMap R SQ) p)) x
a : S
ha : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (x • a)
haQ : a ∉ Q
f : R[X]
hfm : f.Monic
hfa : Eq.{u_2 + 1} (α := S) ((aeval (x • a) : (a : R[X]) → S) f : S) (0 : S)
hf : ∀ (i : ℕ), i ≠ f.natDegree → f.coeff i ∈ p
i : ℕ
hi : i ≠ natDegree (minpoly R a)
hip : coeff (minpoly R a) i ∉ p
hx0 : ¬x = 0
this :
  ∀ (i : ℕ) (hi : i ≠ natDegree (minpoly R (x • a))),
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {x : R | ∃ i < f.natDegree, f.coeff i = x}))
      (coeff (minpoly R (x • a)) i)
⊢ x ∈ p
have this₁ : ∀ (i : ℕ) (hi : i ≠ natDegree (minpoly R a)) (p : Submodule R R),
  Ideal.span {x : R | ∃ i < f.natDegree, f.coeff i = x} ≤ p →
    Ideal.IsPrime p → coeff (minpoly R a) i * x ^ (natDegree (minpoly R a) - i) ∈ p
Tactic: simp only [IsIntegrallyClosed.minpoly_smul hx0 (Algebra.IsIntegral.isIntegral _),
    natDegree_scaleRoots, coeff_scaleRoots, Ideal.radical_eq_sInf, Submodule.mem_sInf,
    Set.mem_setOf_eq, and_imp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
this_1 : IsDomain R
p : Ideal R
inst_7 : p.IsPrime
Q : Ideal S
inst_8 : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (Ideal.comap (F := R →+* SQ) (algebraMap R SQ) (Ideal.map (F := R →+* SQ) (algebraMap R SQ) p)) x
a : S
ha : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (x • a)
haQ : a ∉ Q
f : R[X]
hfm : f.Monic
hfa : Eq.{u_2 + 1} (α := S) ((aeval (x • a) : (a : R[X]) → S) f : S) (0 : S)
hf : ∀ (i : ℕ), i ≠ f.natDegree → f.coeff i ∈ p
i : ℕ
hi : i ≠ natDegree (minpoly R a)
hip : coeff (minpoly R a) i ∉ p
hx0 : ¬x = 0
this :
  ∀ (i : ℕ) (hi : i ≠ natDegree (minpoly R a)) (p : Submodule R R),
    Ideal.span {x : R | ∃ i < f.natDegree, f.coeff i = x} ≤ p →
      Ideal.IsPrime p → coeff (minpoly R a) i * x ^ (natDegree (minpoly R a) - i) ∈ p
⊢ x ∈ p
have neg : Ideal.span {x : R | ∃ i < f.natDegree, f.coeff i = x} ≤ p
Tactic: refine ‹p.IsPrime›.mem_of_pow_mem _ ((‹p.IsPrime›.mem_or_mem
    (this i hi p ?_ inferInstance)).resolve_left hip)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ (y : R), (algebraMap R B : (a : R) → B) y = x
⊢ IsIntegrallyClosedIn R A
have refine_1 : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B)
  (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := A) (⇑f : (a : A) → B) (⇑(algebraMap R A) : (a : R) → A))
Tactic: refine ⟨Function.Injective.of_comp (f := f) ?_, fun hx => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ (y : R), (algebraMap R B : (a : R) → B) y = x
refine_1 :
  Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B)
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := A) (⇑f : (a : A) → B) (⇑(algebraMap R A) : (a : R) → A))
⊢ IsIntegrallyClosedIn R A
have refine_2 : ∀ {x : A} (hx : IsIntegral R x), ∃ (y : R), (algebraMap R A : (a : R) → A) y = x
Tactic: refine ⟨Function.Injective.of_comp (f := f) ?_, fun hx => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ (y : R), (algebraMap R B : (a : R) → B) y = x
refine_1 :
  Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B)
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := A) (⇑f : (a : A) → B) (⇑(algebraMap R A) : (a : R) → A))
refine_2 : ∀ {x : A} (hx : IsIntegral R x), ∃ (y : R), (algebraMap R A : (a : R) → A) y = x
⊢ IsIntegrallyClosedIn R A
have refine_3 : ∀ {x : A}, (∃ (y : R), (algebraMap R A : (a : R) → A) y = x) → IsIntegral R x
Tactic: refine ⟨Function.Injective.of_comp (f := f) ?_, fun hx => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ (y : R), (algebraMap R B : (a : R) → B) y = x
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B)
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := A) (⇑f : (a : A) → B) (⇑(algebraMap R A) : (a : R) → A))
have h : Eq (α := R → B)
  (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := A) (⇑f : (a : A) → B) (⇑(algebraMap R A) : (a : R) → A))
  (⇑(algebraMap R B) : (a : R) → B)
Tactic: convert! inj
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ (y : R), (algebraMap R B : (a : R) → B) y = x
x : A
hx : IsIntegral R x
⊢ ∃ (y : R), (algebraMap R A : (a : R) → A) y = x
have refine_2 : ∀ (y : R) (fx_eq : Eq.{u_3 + 1} (α := B) ((algebraMap R B : (a : R) → B) y : B) ((f : (a : A) → B) x : B)),
  ∃ (y : R), (algebraMap R A : (a : R) → A) y = x
Tactic: obtain ⟨y, fx_eq⟩ := cl.mp ((isIntegral_algHom_iff f hf).mpr hx)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ (y : R), (algebraMap R B : (a : R) → B) y = x
y : R
⊢ IsIntegral.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) y : A)
have refine_3 : IsIntegral.{u_1, u_3} R (A := B) ((f : (a : A) → B) ((algebraMap R A : (a : R) → A) y : A) : B)
Tactic: apply (isIntegral_algHom_iff f hf).mp
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
⊢ IsIntegrallyClosedIn R A ↔
    Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A) ∧
      ∀ {x : A}, IsIntegral R x → ∃ (y : R), (algebraMap R A : (a : R) → A) y = x
have mp : IsIntegrallyClosedIn R A →
  Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A) ∧
    ∀ {x : A}, IsIntegral R x → ∃ (y : R), (algebraMap R A : (a : R) → A) y = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
mp :
  IsIntegrallyClosedIn R A →
    Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A) ∧
      ∀ {x : A}, IsIntegral R x → ∃ (y : R), (algebraMap R A : (a : R) → A) y = x
⊢ IsIntegrallyClosedIn R A ↔
    Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A) ∧
      ∀ {x : A}, IsIntegral R x → ∃ (y : R), (algebraMap R A : (a : R) → A) y = x
have mpr : (Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A) ∧
    ∀ {x : A}, IsIntegral R x → ∃ (y : R), (algebraMap R A : (a : R) → A) y = x) →
  IsIntegrallyClosedIn R A
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
cl : ∀ {x : A}, IsIntegral R x → ∃ (y : R), (algebraMap R A : (a : R) → A) y = x
⊢ IsIntegrallyClosedIn R A
have mpr : ∀ {x : A}, (∃ (y : R), (algebraMap R A : (a : R) → A) y = x) → IsIntegral R x
Tactic: refine ⟨inj, by simp_all, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
A : Type u_2
inst : CommRing A
C : Type u_5
inst_1 : SetLike C A
inst_2 : SubringClass C A
S : C
⊢ IsIntegrallyClosedIn (↥S) A ↔ ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S
have rw : (∀ {x : A}, IsIntegral (↥S) x → ∃ (y : ↥S), (algebraMap (↥S) A : (a : ↥S) → A) y = x) ↔
  ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S
Tactic: rw [isIntegrallyClosedIn_iff, and_iff_right (FaithfulSMul.algebraMap_injective _ _)]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
A : Type u_2
inst : CommRing A
C : Type u_5
inst_1 : SetLike C A
inst_2 : SubringClass C A
S : C
inst_3 : IsFractionRing (↥S) A
⊢ IsIntegrallyClosed.{u_2} ↥S ↔ ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S
have rw : (∀ {x : A}, IsIntegral (↥S) x → ∃ (y : ↥S), (algebraMap (↥S) A : (a : ↥S) → A) y = x) ↔
  ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S
Tactic: rw [isIntegrallyClosed_iff A]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
A : Type u_2
inst : CommRing A
C : Type u_5
inst_1 : SetLike C A
inst_2 : SubringClass C A
S : C
T : Subring A
inst_3 : IsIntegrallyClosedIn (↥T) A
⊢ Subalgebra.toSubring (R := ↥S) (integralClosure (↥S) A) ≤ T ↔ ofClass S ≤ T
have rw : (∀ (a : A) (b : a ∈ S),
    Membership.mem (α := A) T ((algebraMap (↥S) A : (a : ↥S) → A) (Subtype.mk (p := fun (a : A) ↦ a ∈ S) a b) : A)) ↔
  ∀ ⦃x : A⦄, Membership.mem (γ := Subring A) (ofClass S) x → x ∈ T
Tactic: rw [integralClosure_le_iff, Subtype.forall, SetLike.le_def]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hRA : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ Eq (α := Subalgebra R A) (integralClosure R A) ⊥ ↔ IsIntegrallyClosedIn R A
have refine : LE.le (α := Subalgebra R A) (integralClosure R A) ⊥ ↔ IsIntegrallyClosedIn R A
Tactic: refine eq_bot_iff.trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hRA : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ LE.le (α := Subalgebra R A) (integralClosure R A) ⊥ ↔ IsIntegrallyClosedIn R A
have mp : LE.le (α := Subalgebra R A) (integralClosure R A) ⊥ → IsIntegrallyClosedIn R A
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hRA : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
mp : LE.le (α := Subalgebra R A) (integralClosure R A) ⊥ → IsIntegrallyClosedIn R A
⊢ LE.le (α := Subalgebra R A) (integralClosure R A) ⊥ ↔ IsIntegrallyClosedIn R A
have mpr : IsIntegrallyClosedIn R A → LE.le (α := Subalgebra R A) (integralClosure R A) ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hRA : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
h : LE.le (α := Subalgebra R A) (integralClosure R A) ⊥
⊢ IsIntegrallyClosedIn R A
have mp : ∀ {x : A}, (∃ (y : R), (algebraMap R A : (a : R) → A) y = x) → IsIntegral R x
Tactic: refine ⟨ hRA, fun hx => Set.mem_range.mp (Algebra.mem_bot.mp (h hx)), ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hRA : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
h : IsIntegrallyClosedIn R A
x : A
hx : Membership.mem (γ := Subalgebra R A) (integralClosure R A) x
⊢ Membership.mem (γ := Subalgebra R A) ⊥ x
have mpr : ∃ (y : R), (algebraMap R A : (a : R) → A) y = x
Tactic: rw [Algebra.mem_bot, Set.mem_range]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : IsIntegrallyClosedIn A B
inst_8 : Algebra.IsIntegral R A
⊢ IsIntegralClosure A R B
have refine : ∀ {x : B}, (∃ (y : A), (algebraMap A B : (a : A) → B) y = x) → IsIntegral R x
Tactic: refine ⟨IsIntegralClosure.algebraMap_injective _ A _, fun {x} ↦
    ⟨fun hx ↦ IsIntegralClosure.isIntegral_iff.mp (IsIntegral.tower_top (A := A) hx), ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f_1 : R ≃+* S
h : IsIntegrallyClosed R
x : Algebra S R := f_1.symm.toRingHom.toAlgebra
f : S ≃ₐ[S] R := AlgEquiv.ofRingEquiv (f := f_1.symm) ⋯
g : AlgEquiv.{u_2, u_2, u_1} S (FractionRing S) (FractionRing R) := IsFractionRing.algEquivOfAlgEquiv f
⊢ IsIntegrallyClosed S
have refine : ∀ {x : FractionRing S} (hx : IsIntegral S x),
  ∃ (y : S), (algebraMap S (FractionRing S) : (a : S) → FractionRing S) y = x
Tactic: refine (isIntegrallyClosed_iff (FractionRing S)).mpr (fun hx ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f_1 : R ≃+* S
h : IsIntegrallyClosed R
x : Algebra S R := f_1.symm.toRingHom.toAlgebra
f : S ≃ₐ[S] R := AlgEquiv.ofRingEquiv (f := f_1.symm) ⋯
g : AlgEquiv.{u_2, u_2, u_1} S (FractionRing S) (FractionRing R) := IsFractionRing.algEquivOfAlgEquiv f
x_1 : FractionRing S
hx : IsIntegral S x_1
⊢ ∃ (y : S), (algebraMap S (FractionRing S) : (a : S) → FractionRing S) y = x_1
have rcases : ∀ (z : R)
  (hz :
    Eq (α := FractionRing R) ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) z : FractionRing R)
      ((g : (a : FractionRing S) → FractionRing R) x_1 : FractionRing R)),
  ∃ (y : S), (algebraMap S (FractionRing S) : (a : S) → FractionRing S) y = x_1
Tactic: rcases (isIntegrallyClosed_iff _).mp h ((isIntegral_algEquiv g).mpr hx).tower_top with ⟨z, hz⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (hypothesis)
Goal:
R : Type u_4
K : Type u_5
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : FaithfulSMul R K
inst_4 : IsIntegrallyClosedIn R K
⊢ IsIntegrallyClosed R
have this : IsDomain R
Tactic: have : IsDomain R := (FaithfulSMul.algebraMap_injective R K).isDomain _
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_4
K : Type u_5
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : FaithfulSMul R K
inst_4 : IsIntegrallyClosedIn R K
this : IsDomain R
f : FractionRing R →ₐ[R] K :=
  IsFractionRing.liftAlgHom.{u_4, u_4, u_4, u_5} (R := R) (A := R) (K := FractionRing R) (L := K) (g :=
    Algebra.ofId R K) ⋯
⊢ IsIntegrallyClosed R
have rw : ∀ {x : FractionRing R}, IsIntegral R x → ∃ (y : R), (algebraMap R (FractionRing R) : (a : R) → FractionRing R) y = x
Tactic: rw [isIntegrallyClosed_iff (K := FractionRing R)]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_4
K : Type u_5
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : FaithfulSMul R K
inst_4 : IsIntegrallyClosedIn R K
this : IsDomain R
f : FractionRing R →ₐ[R] K :=
  IsFractionRing.liftAlgHom.{u_4, u_4, u_4, u_5} (R := R) (A := R) (K := FractionRing R) (L := K) (g :=
    Algebra.ofId R K) ⋯
x : FractionRing R
hx : IsIntegral R x
⊢ ∃ (y : R), (algebraMap R (FractionRing R) : (a : R) → FractionRing R) y = x
have h : ∀ (x_1 : R),
  (algebraMap R (FractionRing R) : (a : R) → FractionRing R) x_1 = x ↔
    Eq.{u_5 + 1} (α := K) ((algebraMap R K : (a : R) → K) x_1 : K) ((f : (a : FractionRing R) → K) x : K)
Tactic: convert! (IsIntegralClosure.isIntegral_iff (A := R)).mp (hx.map f)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : Algebra R U
inst_7 : Algebra S U
inst_8 : Algebra T U
inst_9 : IsScalarTower S T U
inst_10 : IsScalarTower R T U
inst_11 : IsIntegralClosure S R T
inst_12 : IsIntegrallyClosedIn T U
⊢ IsIntegralClosure S R U
have refine_1 : Function.Injective.{u_5 + 1, u_7 + 1} (α := S) (β := U) (⇑(algebraMap S U) : (a : S) → U)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : Algebra R U
inst_7 : Algebra S U
inst_8 : Algebra T U
inst_9 : IsScalarTower S T U
inst_10 : IsScalarTower R T U
inst_11 : IsIntegralClosure S R T
inst_12 : IsIntegrallyClosedIn T U
refine_1 : Function.Injective.{u_5 + 1, u_7 + 1} (α := S) (β := U) (⇑(algebraMap S U) : (a : S) → U)
⊢ IsIntegralClosure S R U
have refine_2 : ∀ {x : U}, IsIntegral R x ↔ ∃ (y : S), (algebraMap S U : (a : S) → U) y = x
Tactic: refine ⟨?_, ?_⟩