awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : S
H : IsIntegral R s
h :
  ∃ (t : R),
    Membership.mem (γ := Submonoid R) R⁰ t ∧
      Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (t • s)
b : R
hb' : Membership.mem (γ := Submonoid R) R⁰ b
hb :
  ∀ i < Polynomial.natDegree (minpoly R s),
    Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (b • s ^ i)
n : ℕ
IH : ∀ m < n, Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (b • s ^ m)
hn : Polynomial.natDegree (minpoly R s) ≤ n
this :
  s ^ Polynomial.natDegree (minpoly R s) =
    -∑ x ∈ Finset.range (Polynomial.natDegree (minpoly R s)), Polynomial.coeff (minpoly R s) x • s ^ x
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S))
    (-∑ x ∈ Finset.range (Polynomial.natDegree (minpoly R s)),
        Polynomial.coeff (minpoly R s) x • b • s ^ (n - Polynomial.natDegree (minpoly R s) + x))
have h₁ : ∀ (i : ℕ) (hi : i ∈ Finset.range (Polynomial.natDegree (minpoly R s))), n - Polynomial.natDegree (minpoly R s) + i < n
Tactic: refine neg_mem (sum_mem fun i hi ↦ (AlgHom.range (Algebra.ofId _ _)).smul_mem (IH _ ?_) _)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : S
H : IsIntegral R s
h :
  ∃ (t : R),
    Membership.mem (γ := Submonoid R) R⁰ t ∧
      Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (t • s)
b : R
hb' : Membership.mem (γ := Submonoid R) R⁰ b
hb :
  ∀ i < Polynomial.natDegree (minpoly R s),
    Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (b • s ^ i)
n : ℕ
IH : ∀ m < n, Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (b • s ^ m)
hn : Polynomial.natDegree (minpoly R s) ≤ n
this :
  s ^ Polynomial.natDegree (minpoly R s) =
    -∑ x ∈ Finset.range (Polynomial.natDegree (minpoly R s)), Polynomial.coeff (minpoly R s) x • s ^ x
i : ℕ
hi : i ∈ Finset.range (Polynomial.natDegree (minpoly R s))
⊢ n - Polynomial.natDegree (minpoly R s) + i < n
have hi₁ : i < Polynomial.natDegree (minpoly R s)
Tactic: simp only [Finset.mem_range] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : S
H : IsIntegral R s
h :
  ∃ (t : R),
    Membership.mem (γ := Submonoid R) R⁰ t ∧
      Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (t • s)
b : R
hb' : Membership.mem (γ := Submonoid R) R⁰ b
hb :
  ∀ i < Polynomial.natDegree (minpoly R s),
    Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (b • s ^ i)
n : ℕ
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (b • s ^ n)
have h₁ : ∀ (n : ℕ)
  (IH : ∀ m < n, Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (b • s ^ m)),
  Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (b • s ^ n)
Tactic: induction n using Nat.strong_induction_on with | h n IH =>
  obtain hn | hn := lt_or_ge n (minpoly R s).natDegree
  · exact hb _ (by simpa)
  have := minpoly.aeval R s
  rw [Polynomial.aeval_eq_sum_range, Finset.sum_range_succ, add_eq_zero_iff_eq_neg',
    Polynomial.coeff_natDegree, minpoly.monic H, one_smul] at this
  rw [← Nat.sub_add_cancel hn, pow_add, this, mul_neg, smul_neg, Finset.mul_sum, Finset.smul_sum]
  simp_rw [mul_smul_comm, ← pow_add, smul_comm b]
  refine neg_mem (sum_mem fun i hi ↦ (AlgHom.range (Algebra.ofId _ _)).smul_mem (IH _ ?_) _)
  simp only [Finset.mem_range] at hi
  lia
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : S
H : IsIntegral R s
M : Submonoid R
hM : M ≤ R⁰
inst_3 : IsLocalization M S
⊢ IsAlmostIntegral R s
have obtain : ∀ (s : R) (t : ↥M) (H : IsIntegral R (IsLocalization.mk' S s t)), IsAlmostIntegral R (IsLocalization.mk' S s t)
Tactic: obtain ⟨s, t, rfl⟩ := IsLocalization.exists_mk'_eq M s
Cleared hypotheses: s, H
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : S
H : IsAlmostIntegral R s
inst_3 : IsNoetherianRing R
H' : LE.le (α := Submonoid R) R⁰ (Submonoid.comap (F := R →+* S) (algebraMap R S) S⁰)
⊢ IsIntegral R s
have obtain : ∀ (r : R) (hr : Membership.mem (γ := Submonoid R) R⁰ r)
  (hr' : ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (r • s ^ n)),
  IsIntegral R s
Tactic: obtain ⟨r, hr, hr'⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : S
inst_3 : IsNoetherianRing R
H' : LE.le (α := Submonoid R) R⁰ (Submonoid.comap (F := R →+* S) (algebraMap R S) S⁰)
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (r • s ^ n)
⊢ LE.le (α := Submodule R S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[s] : Submodule R S)
    (Submodule.comap (M₂ := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
        (AlgHom.toLinearMap
            (IsScalarTower.toAlgHom R S (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))) :
          S →ₗ[R] Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
        (Submodule.span R
          (singleton (α := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
            (Localization.Away.invSelf ((algebraMap R S : (a : R) → S) r) :
              Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)))) :
      Submodule R S)
have rw : (↑(Submonoid.powers s) : Set S) ⊆
  (↑(Submodule.comap (M₂ := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
        (AlgHom.toLinearMap
            (IsScalarTower.toAlgHom R S (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))) :
          S →ₗ[R] Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
        (Submodule.span R
          (singleton (α := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
            (Localization.Away.invSelf ((algebraMap R S : (a : R) → S) r) :
              Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))))) :
    Set S)
Tactic: rw [Algebra.adjoin_eq_span, ← Submonoid.powers_eq_closure, Submodule.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : S
inst_3 : IsNoetherianRing R
H' : LE.le (α := Submonoid R) R⁰ (Submonoid.comap (F := R →+* S) (algebraMap R S) S⁰)
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (r • s ^ n)
n : ℕ
⊢ (fun (x : ℕ) ↦ s ^ x) n ∈
    (↑(Submodule.comap (M₂ := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
          (AlgHom.toLinearMap
              (IsScalarTower.toAlgHom R S (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))) :
            S →ₗ[R] Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
          (Submodule.span R
            (singleton (α := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
              (Localization.Away.invSelf ((algebraMap R S : (a : R) → S) r) :
                Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))))) :
      Set S)
have obtain : ∀ (a : R) (ha : ((algebraMap R S : R →+* S) : (a : R) → S) a = r • s ^ n),
  (fun (x : ℕ) ↦ s ^ x) n ∈
    (↑(Submodule.comap (M₂ := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
          (AlgHom.toLinearMap
              (IsScalarTower.toAlgHom R S (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))) :
            S →ₗ[R] Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
          (Submodule.span R
            (singleton (α := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
              (Localization.Away.invSelf ((algebraMap R S : (a : R) → S) r) :
                Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))))) :
      Set S)
Tactic: obtain ⟨a, ha⟩ := hr' n
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : S
inst_3 : IsNoetherianRing R
H' : LE.le (α := Submonoid R) R⁰ (Submonoid.comap (F := R →+* S) (algebraMap R S) S⁰)
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (r • s ^ n)
n : ℕ
a : R
ha : ((algebraMap R S : R →+* S) : (a : R) → S) a = r • s ^ n
⊢ (fun (x : ℕ) ↦ s ^ x) n ∈
    (↑(Submodule.comap (M₂ := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
          (AlgHom.toLinearMap
              (IsScalarTower.toAlgHom R S (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))) :
            S →ₗ[R] Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
          (Submodule.span R
            (singleton (α := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
              (Localization.Away.invSelf ((algebraMap R S : (a : R) → S) r) :
                Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))))) :
      Set S)
have refine : HSMul.hSMul (β := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)) a
    (Localization.Away.invSelf ((algebraMap R S : (a : R) → S) r) :
      Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)) =
  ((AlgHom.toLinearMap
          (IsScalarTower.toAlgHom R S (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))) :
        S →ₗ[R] Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)) :
      (a : S) → Localization.Away ((algebraMap R S : (a : R) → S) r))
    ((fun (x : ℕ) ↦ s ^ x) n)
Tactic: refine Submodule.mem_span_singleton.mpr ⟨a, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : S
inst_3 : IsNoetherianRing R
H' : LE.le (α := Submonoid R) R⁰ (Submonoid.comap (F := R →+* S) (algebraMap R S) S⁰)
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (r • s ^ n)
n : ℕ
a : R
ha : ((algebraMap R S : R →+* S) : (a : R) → S) a = r • s ^ n
⊢ HSMul.hSMul (β := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)) a
      (Localization.Away.invSelf ((algebraMap R S : (a : R) → S) r) :
        Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)) =
    ((AlgHom.toLinearMap
            (IsScalarTower.toAlgHom R S (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))) :
          S →ₗ[R] Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)) :
        (a : S) → Localization.Away ((algebraMap R S : (a : R) → S) r))
      ((fun (x : ℕ) ↦ s ^ x) n)
have suffices : HMul.hMul (β := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
    (HMul.hMul (α := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)) (β :=
      Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
      ((algebraMap S (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)) :
            (a : S) → Localization.Away ((algebraMap R S : (a : R) → S) r))
          (s ^ n) :
        Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
      ((algebraMap S (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)) :
            (a : S) → Localization.Away ((algebraMap R S : (a : R) → S) r))
          ((algebraMap R S : (a : R) → S) r) :
        Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)))
    (Localization.Away.invSelf ((algebraMap R S : (a : R) → S) r) :
      Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)) =
  (algebraMap S (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)) :
      (a : S) → Localization.Away ((algebraMap R S : (a : R) → S) r))
    (s ^ n)
Tactic: suffices algebraMap _ _ (s ^ n) * algebraMap _ _ ((algebraMap R S) r) *
        Localization.Away.invSelf ((algebraMap R S) r) = algebraMap S _ (s ^ n) by
      simpa [Algebra.smul_def, IsScalarTower.algebraMap_apply R S (Localization.Away _),
        ha, mul_assoc, mul_left_comm] using this
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : S
inst_3 : IsNoetherianRing R
H' : LE.le (α := Submonoid R) R⁰ (Submonoid.comap (F := R →+* S) (algebraMap R S) S⁰)
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (r • s ^ n)
f : ↥R[s] →ₗ[R]
  ↥(Submodule.span R
      (singleton (α := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
        (Localization.Away.invSelf ((algebraMap R S : (a : R) → S) r) :
          Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)))) :=
  LinearMap.restrict
    (AlgHom.toLinearMap
      (IsScalarTower.toAlgHom R S (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))))
    ⋯
⊢ Function.Injective (α := S) (β := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
    (⇑(algebraMap S (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))) :
      (a : S) → Localization.Away ((algebraMap R S : (a : R) → S) r))
have hM : LE.le.{u_2} (α := Submonoid S) (Submonoid.powers ((algebraMap R S : (a : R) → S) r) : Submonoid S) (S⁰ : Submonoid S)
Tactic: apply IsLocalization.injective (M := .powers (algebraMap R S r))
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : S
inst_3 : IsNoetherianRing R
H' : LE.le (α := Submonoid R) R⁰ (Submonoid.comap (F := R →+* S) (algebraMap R S) S⁰)
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (r • s ^ n)
f : ↥R[s] →ₗ[R]
  ↥(Submodule.span R
      (singleton (α := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
        (Localization.Away.invSelf ((algebraMap R S : (a : R) → S) r) :
          Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)))) :=
  LinearMap.restrict
    (AlgHom.toLinearMap
      (IsScalarTower.toAlgHom R S (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))))
    ⋯
⊢ Function.Injective (α := ↥R[s]) (β :=
    ↥(Submodule.span R
        (singleton (α := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
          (Localization.Away.invSelf ((algebraMap R S : (a : R) → S) r) :
            Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)))))
    (⇑f : (a : ↥R[s]) → ↥(R ∙ Localization.Away.invSelf ((algebraMap R S : (a : R) → S) r)))
have this : Function.Injective (α := S) (β := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
  (⇑(algebraMap S (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))) :
    (a : S) → Localization.Away ((algebraMap R S : (a : R) → S) r))
Tactic: have : Function.Injective (algebraMap S (Localization.Away (algebraMap R S r))) := by
      apply IsLocalization.injective (M := .powers (algebraMap R S r))
      exact Submonoid.powers_le.mpr (H' hr)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : S
inst_3 : IsNoetherianRing R
H' : LE.le (α := Submonoid R) R⁰ (Submonoid.comap (F := R →+* S) (algebraMap R S) S⁰)
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (r • s ^ n)
f : ↥R[s] →ₗ[R]
  ↥(Submodule.span R
      (singleton (α := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
        (Localization.Away.invSelf ((algebraMap R S : (a : R) → S) r) :
          Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)))) :=
  LinearMap.restrict
    (AlgHom.toLinearMap
      (IsScalarTower.toAlgHom R S (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))))
    ⋯
⊢ IsIntegral R s
have this : Function.Injective (α := ↥R[s]) (β :=
  ↥(Submodule.span R
      (singleton (α := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
        (Localization.Away.invSelf ((algebraMap R S : (a : R) → S) r) :
          Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)))))
  (⇑f : (a : ↥R[s]) → ↥(R ∙ Localization.Away.invSelf ((algebraMap R S : (a : R) → S) r)))
Tactic: have : Function.Injective f := by
    have : Function.Injective (algebraMap S (Localization.Away (algebraMap R S r))) := by
      apply IsLocalization.injective (M := .powers (algebraMap R S r))
      exact Submonoid.powers_le.mpr (H' hr)
    exact fun x y e ↦ Subtype.ext (this congr($e))
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : S
inst_3 : IsNoetherianRing R
H' : LE.le (α := Submonoid R) R⁰ (Submonoid.comap (F := R →+* S) (algebraMap R S) S⁰)
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (r • s ^ n)
f : ↥R[s] →ₗ[R]
  ↥(Submodule.span R
      (singleton (α := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
        (Localization.Away.invSelf ((algebraMap R S : (a : R) → S) r) :
          Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)))) :=
  LinearMap.restrict
    (AlgHom.toLinearMap
      (IsScalarTower.toAlgHom R S (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))))
    ⋯
this :
  Function.Injective (α := ↥R[s]) (β :=
    ↥(Submodule.span R
        (singleton (α := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
          (Localization.Away.invSelf ((algebraMap R S : (a : R) → S) r) :
            Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)))))
    (⇑f : (a : ↥R[s]) → ↥(R ∙ Localization.Away.invSelf ((algebraMap R S : (a : R) → S) r)))
⊢ Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[s])
have rw : Module.Finite.{u_1, u_2} R ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[s] : Submodule R S)
Tactic: rw [← Module.Finite.iff_fg]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : S
inst_3 : IsNoetherianRing R
H' : LE.le (α := Submonoid R) R⁰ (Submonoid.comap (F := R →+* S) (algebraMap R S) S⁰)
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (r • s ^ n)
f : ↥R[s] →ₗ[R]
  ↥(Submodule.span R
      (singleton (α := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
        (Localization.Away.invSelf ((algebraMap R S : (a : R) → S) r) :
          Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)))) :=
  LinearMap.restrict
    (AlgHom.toLinearMap
      (IsScalarTower.toAlgHom R S (Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))))
    ⋯
this :
  Function.Injective (α := ↥R[s]) (β :=
    ↥(Submodule.span R
        (singleton (α := Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
          (Localization.Away.invSelf ((algebraMap R S : (a : R) → S) r) :
            Localization.Away (M := S) ((algebraMap R S : (a : R) → S) r : S)))))
    (⇑f : (a : ↥R[s]) → ↥(R ∙ Localization.Away.invSelf ((algebraMap R S : (a : R) → S) r)))
⊢ IsIntegral R s
have this₁ : Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[s])
Tactic: have : (Algebra.adjoin R {s}).toSubmodule.FG := by
    rw [← Module.Finite.iff_fg]
    exact .of_injective f this
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsNoetherianRing R
inst_4 : IsDomain S
inst_5 : FaithfulSMul R S
s : S
H : IsAlmostIntegral R s
⊢ IsIntegral R s
have this : IsDomain R
Tactic: have := IsDomain.of_faithfulSMul R S
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : Ring R
⊢ Eq (α := Ideal R) (jacobson ⊥) (Ring.jacobson R)
have simp_rw : Eq (α := Ideal R) (sInf {J : Ideal R | ⊥ ≤ J ∧ J.IsMaximal}) (Ring.jacobson R)
Tactic: simp_rw [jacobson, Ring.jacobson, Module.jacobson, bot_le, true_and, isMaximal_def]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : Ring R
simp_rw : Eq (α := Ideal R) (sInf {J : Ideal R | ⊥ ≤ J ∧ J.IsMaximal}) (Ring.jacobson R)
⊢ Eq (α := Ideal R) (jacobson ⊥) (Ring.jacobson R)
have simp_rw₁ : Eq (α := Ideal R) (sInf {J : Ideal R | ⊥ ≤ J ∧ J.IsMaximal} : Ideal R) (Module.jacobson R R : Submodule R R)
Tactic: simp_rw [jacobson, Ring.jacobson, Module.jacobson, bot_le, true_and, isMaximal_def]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : Ring R
simp_rw : Eq (α := Ideal R) (sInf {J : Ideal R | ⊥ ≤ J ∧ J.IsMaximal}) (Ring.jacobson R)
simp_rw₁ : Eq (α := Ideal R) (sInf {J : Ideal R | ⊥ ≤ J ∧ J.IsMaximal} : Ideal R) (Module.jacobson R R : Submodule R R)
⊢ Eq (α := Ideal R) (jacobson ⊥) (Ring.jacobson R)
have simp_rw₂ : Eq.{u + 1} (α := Ideal R) (sInf {J : Ideal R | ⊥ ≤ J ∧ J.IsMaximal}) (sInf {m : Submodule R R | IsCoatom m})
Tactic: simp_rw [jacobson, Ring.jacobson, Module.jacobson, bot_le, true_and, isMaximal_def]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : Ring R
simp_rw : Eq (α := Ideal R) (sInf {J : Ideal R | ⊥ ≤ J ∧ J.IsMaximal}) (Ring.jacobson R)
simp_rw₁ : Eq (α := Ideal R) (sInf {J : Ideal R | ⊥ ≤ J ∧ J.IsMaximal} : Ideal R) (Module.jacobson R R : Submodule R R)
simp_rw₂ : Eq.{u + 1} (α := Ideal R) (sInf {J : Ideal R | ⊥ ≤ J ∧ J.IsMaximal}) (sInf {m : Submodule R R | IsCoatom m})
⊢ Eq (α := Ideal R) (jacobson ⊥) (Ring.jacobson R)
have simp_rw₃ : Eq.{u + 1} (α := Ideal R) (sInf {J : Ideal R | True ∧ J.IsMaximal}) (sInf {m : Submodule R R | IsCoatom m})
Tactic: simp_rw [jacobson, Ring.jacobson, Module.jacobson, bot_le, true_and, isMaximal_def]