awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
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
⊢ 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:
simp [mul_assoc, Localization.Away.invSelf, Localization.mk_eq_mk']

Premises used: Localization.mk_eq_mk', mul_assoc, Localization.Away.invSelf
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
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))))
    ⋯
hM :
  LE.le.{u_2} (α := Submonoid S) (Submonoid.powers ((algebraMap R S : (a : R) → S) r) : Submonoid S) (S⁰ : Submonoid 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))

Tactic:
apply IsLocalization.injective (M := .powers (algebraMap R S r))

Premises used: IsLocalization.injective
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
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))))
    ⋯
⊢ LE.le.{u_2} (α := Submonoid S) (Submonoid.powers ((algebraMap R S : (a : R) → S) r) : Submonoid S) (S⁰ : Submonoid S)

Tactic:
Submonoid.powers_le.mpr (H' hr)

Premises used: Iff.mpr, Set.Mem, Submonoid.powers_le
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
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))))
    ⋯
⊢ LE.le.{u_2} (α := Submonoid S) (Submonoid.powers ((algebraMap R S : (a : R) → S) r) : Submonoid S) (S⁰ : Submonoid S)

Tactic:
exact Submonoid.powers_le.mpr (H' hr)

Premises used: Iff.mpr, Submonoid.powers_le
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
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))

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)
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
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 (α := 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))
⊢ 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:
fun x y e ↦ Subtype.ext (this congr($e))

Premises used: congrArg, id, Function.Injective, Subtype.val, Subtype.ext
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
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 (α := 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))
⊢ 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:
exact fun x y e ↦ Subtype.ext (this congr($e))

Premises used: id, Subtype.ext
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
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)))

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))
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
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)))
rw : Module.Finite.{u_1, u_2} R ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[s] : Submodule R S)
⊢ Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[s])

Tactic:
rw [← Module.Finite.iff_fg]

Premises used: Module.Finite.iff_fg
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
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)))
⊢ Module.Finite.{u_1, u_2} R ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[s] : Submodule R S)

Tactic:
.of_injective f this

Premises used: Module.Finite.of_injective
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
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)))
⊢ Module.Finite.{u_1, u_2} R ↥((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[s] : Submodule R S)

Tactic:
exact .of_injective f this
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
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])

Tactic:
have : (Algebra.adjoin R {s}).toSubmodule.FG := by
    rw [← Module.Finite.iff_fg]
    exact .of_injective f this
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
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_1 :
  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)))
this : Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[s])
⊢ IsIntegral R s

Tactic:
.of_mem_of_fg _ this _ (Algebra.self_mem_adjoin_singleton R s)

Premises used: IsIntegral.of_mem_of_fg, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
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_1 :
  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)))
this : Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[s])
⊢ IsIntegral R s

Tactic:
exact .of_mem_of_fg _ this _ (Algebra.self_mem_adjoin_singleton R s)
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
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
⊢ IsDomain R

Tactic:
have := IsDomain.of_faithfulSMul R S
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
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
this : IsDomain R
x : R
⊢ Membership.mem (γ := Submonoid R) R⁰ x →
    Membership.mem (γ := Submonoid R) (Submonoid.comap (F := R →+* S) (algebraMap R S) S⁰) x

Tactic:
simp
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
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
this : IsDomain R
⊢ IsIntegral R s

Tactic:
exact H.isIntegral_of_nonZeroDivisors_le_comap fun _ ↦ by simp

Premises used: IsAlmostIntegral.isIntegral_of_nonZeroDivisors_le_comap
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
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 R
inst_5 : IsFractionRing R S
s : S
⊢ IsAlmostIntegral R s ↔ IsIntegral R s

Tactic:
letI := IsFractionRing.isDomain R (K := S)
  ⟨IsAlmostIntegral.isIntegral, IsIntegral.isAlmostIntegral⟩

Premises used: IsIntegral.isAlmostIntegral, IsAlmostIntegral.isIntegral, Iff.intro
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
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 R
inst_5 : IsFractionRing R S
⊢ Eq (α := Subalgebra R S) (completeIntegralClosure R S) (integralClosure R S)

Tactic:
SetLike.ext fun _ ↦ isAlmostIntegral_iff_isIntegral

Premises used: isAlmostIntegral_iff_isIntegral, SetLike.ext
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : Ring R
I : Ideal R
⊢ I ≤ I.jacobson

Tactic:
fun _ hx => mem_sInf.mpr fun _ hJ => hJ.left hx

Premises used: Iff.mpr, Set.Mem, Ideal.mem_sInf, And.left
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : Ring R
I : Ideal R
⊢ I.jacobson.jacobson = I.jacobson

Tactic:
le_antisymm (sInf_le_sInf fun _ hJ => ⟨sInf_le hJ, hJ.2⟩) le_jacobson

Premises used: sInf_le_sInf, le_antisymm, And.right, sInf_le, And.intro, Ideal.le_jacobson
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : Ring R
⊢ Eq.{u + 1} (α := Ideal R) (jacobson ⊤) ⊤

Tactic:
eq_top_iff.2 le_jacobson

Premises used: Iff.mpr, eq_top_iff, Ideal.le_jacobson