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
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
h₁ :
  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))
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S))
    (-∑ x ∈ Finset.range (Polynomial.natDegree (minpoly R s)),
        b • (s ^ (n - Polynomial.natDegree (minpoly R s)) * Polynomial.coeff (minpoly R s) x • s ^ x))

Tactic:
simp_rw [mul_smul_comm, ← pow_add, smul_comm b]

Premises used: pow_add, mul_smul_comm, SMulCommClass.smul_comm
-- 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
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))

Tactic:
neg_mem (sum_mem fun i hi ↦ (AlgHom.range (Algebra.ofId _ _)).smul_mem (IH _ ?_) _)

Premises used: HSub.hSub, minpoly, Polynomial.coeff, Subalgebra.smul_mem, Algebra.ofId, HAdd.hAdd, Polynomial.natDegree, sum_mem, AlgHom.range, NegMemClass.neg_mem
-- 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
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
h₁ :
  ∀ (i : ℕ) (hi : i ∈ Finset.range (Polynomial.natDegree (minpoly R s))), n - Polynomial.natDegree (minpoly R s) + i < n
⊢ 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))

Tactic:
refine neg_mem (sum_mem fun i hi ↦ (AlgHom.range (Algebra.ofId _ _)).smul_mem (IH _ ?_) _)

Premises used: Subalgebra.smul_mem, Algebra.ofId, sum_mem, AlgHom.range, NegMemClass.neg_mem
-- 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
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))
⊢ i < Polynomial.natDegree (minpoly R s)

Tactic:
simp only [Finset.mem_range] at hi

Premises used: Finset.mem_range
-- 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
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 < Polynomial.natDegree (minpoly R s)
⊢ n - Polynomial.natDegree (minpoly R s) + i < n

Tactic:
lia
-- 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
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 : ℕ
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)
⊢ 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

Premises used: Finset.mul_sum, minpoly.monic, add_eq_zero_iff_eq_neg', Polynomial.coeff_natDegree, pow_add, smul_neg, Finset.mem_range, minpoly, one_smul, Polynomial.aeval_eq_sum_range, Finset.smul_sum, mul_smul_comm, lt_or_ge, SMulCommClass.smul_comm, Polynomial.natDegree, Finset.sum_range_succ, mul_neg
-- 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
H : IsIntegral R s
M : Submonoid R
hM : M ≤ R⁰
inst_3 : IsLocalization M S
obtain : ∀ (s : R) (t : ↥M) (H : IsIntegral R (IsLocalization.mk' S s t)), IsAlmostIntegral R (IsLocalization.mk' S s t)
⊢ IsAlmostIntegral R s

Tactic:
obtain ⟨s, t, rfl⟩ := IsLocalization.exists_mk'_eq M s

Premises used: rfl, IsLocalization.exists_mk'_eq
-- 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
M : Submonoid R
hM : M ≤ R⁰
inst_3 : IsLocalization M S
s : R
t : ↥M
H : IsIntegral R (IsLocalization.mk' S s t)
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S))
    ((↑t : R) • IsLocalization.mk' S s t)

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
M : Submonoid R
hM : M ≤ R⁰
inst_3 : IsLocalization M S
s : R
t : ↥M
H : IsIntegral R (IsLocalization.mk' S s t)
⊢ IsAlmostIntegral R (IsLocalization.mk' S s t)

Tactic:
exact H.isAlmostIntegral_of_exists_smul_mem_range ⟨t, hM t.2, by simp⟩

Premises used: IsIntegral.isAlmostIntegral_of_exists_smul_mem_range, And.intro, Exists.intro, Subtype.val, Subtype.property
-- 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 : IsFractionRing R S
s : S
H : IsIntegral R s
⊢ IsAlmostIntegral R s

Tactic:
H.isAlmostIntegral_of_isLocalization _ le_rfl

Premises used: le_rfl, IsIntegral.isAlmostIntegral_of_isLocalization
-- 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 : IsFractionRing R S
⊢ LE.le (α := Subalgebra R S) (integralClosure R S) (completeIntegralClosure R S)

Tactic:
fun _ h ↦ h.isAlmostIntegral

Premises used: IsIntegral.isAlmostIntegral, Set.Mem, setOf, IsAlmostIntegral
-- 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
H : IsAlmostIntegral R s
inst_3 : IsNoetherianRing R
H' : LE.le (α := Submonoid R) R⁰ (Submonoid.comap (F := R →+* S) (algebraMap R S) S⁰)
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
⊢ IsIntegral R s

Tactic:
obtain ⟨r, hr, hr'⟩ := H
-- 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)
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)
⊢ 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)

Tactic:
rw [Algebra.adjoin_eq_span, ← Submonoid.powers_eq_closure, Submodule.span_le]

Premises used: Submonoid.powers_eq_closure, Algebra.adjoin_eq_span, Submodule.span_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)
n : ℕ
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)
⊢ (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
-- 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
⊢ (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:
Submodule.mem_span_singleton.mpr ⟨a, ?_⟩

Premises used: Iff.mpr, iInf, Set.Mem, Set.iInter, setOf, Submodule.mem_span_singleton, Set.preimage, Exists.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
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
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)
⊢ (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:
refine Submodule.mem_span_singleton.mpr ⟨a, ?_⟩

Premises used: Iff.mpr, Submodule.mem_span_singleton, Exists.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
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
this :
  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)
⊢ 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:
simpa [Algebra.smul_def, IsScalarTower.algebraMap_apply R S (Localization.Away _),
        ha, mul_assoc, mul_left_comm] using this

Premises used: mul_assoc, Localization.Away, mul_left_comm, Algebra.smul_def, IsScalarTower.algebraMap_apply
-- 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
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)
⊢ 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:
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