awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
neg :
  Eq.{u_6 + 1} (α := E)
    (((aeval ((algebraMap B E : (a : B) → E) x) : K[X] →ₐ[K] E) : (a : K[X]) → E)
        (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) :
      E)
    (0 : E)
⊢ ¬Eq (α := K[X]) (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) 0 ∧
    Eq.{u_6 + 1} (α := E)
      (((aeval ((algebraMap B E : (a : B) → E) x) : K[X] →ₐ[K] E) : (a : K[X]) → E)
          (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) :
        E)
      (0 : E)

Tactic:
refine ⟨minpoly.ne_zero (IsIntegral.isIntegral _), ?_⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
⊢ Eq.{u_6 + 1} (α := E)
    (((aeval ((algebraMap B E : (a : B) → E) x) : K[X] →ₐ[K] E) : (a : K[X]) → E)
        (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) :
      E)
    (0 : E)

Tactic:
simp [algebraMap_apply B L E, aeval_algebraMap_apply]

Premises used: IsScalarTower.algebraMap_apply, Polynomial.aeval_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
a b : 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 • a ^ n)
s : R
hs : Membership.mem (γ := Submonoid R) R⁰ s
hs' : ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (s • b ^ n)
⊢ Membership.mem (γ := Set S) {s : S | IsAlmostIntegral R s} (a * b)

Tactic:
⟨r * s, mul_mem hr hs, fun n ↦ ?_⟩

Premises used: HMul.hMul, Set.Mem, setOf, IsAlmostIntegral, And.intro, Exists.intro, MulMemClass.mul_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
a b : 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 • a ^ n)
s : R
hs : Membership.mem (γ := Submonoid R) R⁰ s
hs' : ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (s • b ^ n)
refine :
  ∀ (n : ℕ),
    Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) ((r * s) • (a * b) ^ n)
⊢ Membership.mem (γ := Set S) {s : S | IsAlmostIntegral R s} (a * b)

Tactic:
refine ⟨r * s, mul_mem hr hs, fun 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
a b : 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 • a ^ n)
s : R
hs : Membership.mem (γ := Submonoid R) R⁰ s
hs' : ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (s • b ^ n)
n : ℕ
rw : Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (r • a ^ n * s • b ^ n)
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) ((r * s) • (a * b) ^ n)

Tactic:
rw [mul_pow, mul_smul_mul_comm]

Premises used: mul_pow, mul_smul_mul_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
a b : 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 • a ^ n)
s : R
hs : Membership.mem (γ := Submonoid R) R⁰ s
hs' : ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (s • b ^ n)
n : ℕ
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (r • a ^ n * s • b ^ n)

Tactic:
mul_mem (hr' _) (hs' _)

Premises used: MulMemClass.mul_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
a b : 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 • a ^ n)
s : R
hs : Membership.mem (γ := Submonoid R) R⁰ s
hs' : ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (s • b ^ n)
n : ℕ
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (r • a ^ n * s • b ^ n)

Tactic:
exact mul_mem (hr' _) (hs' _)

Premises used: MulMemClass.mul_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
a b : 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 • a ^ n)
s : R
hs : Membership.mem (γ := Submonoid R) R⁰ s
hs' : ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (s • b ^ n)
⊢ Membership.mem (γ := Set S) {s : S | IsAlmostIntegral R s} (a + b)

Tactic:
⟨r * s, mul_mem hr hs, fun n ↦ ?_⟩

Premises used: HMul.hMul, Set.Mem, setOf, IsAlmostIntegral, And.intro, Exists.intro, MulMemClass.mul_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
a b : 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 • a ^ n)
s : R
hs : Membership.mem (γ := Submonoid R) R⁰ s
hs' : ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (s • b ^ n)
refine :
  ∀ (n : ℕ),
    Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) ((r * s) • (a + b) ^ n)
⊢ Membership.mem (γ := Set S) {s : S | IsAlmostIntegral R s} (a + b)

Tactic:
refine ⟨r * s, mul_mem hr hs, fun 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
a b : 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 • a ^ n)
s : R
hs : Membership.mem (γ := Submonoid R) R⁰ s
hs' : ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (s • b ^ n)
n : ℕ
simp :
  Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S))
    (∑ x ∈ Finset.range (n + 1), r • a ^ x * s • b ^ (n - x) * (↑(n.choose x) : S))
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) ((r * s) • (a + b) ^ n)

Tactic:
simp only [add_pow, Finset.smul_sum, ← smul_mul_assoc _ (_ * _),
      ← smul_mul_smul_comm _ (a ^ _)]

Premises used: HMul.hMul, smul_mul_assoc, smul_mul_smul_comm, HPow.hPow, Finset.smul_sum, add_pow
-- 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
a b : 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 • a ^ n)
s : R
hs : Membership.mem (γ := Submonoid R) R⁰ s
hs' : ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (s • b ^ n)
n i : ℕ
h : i ∈ Finset.range (n + 1)
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (↑(n.choose i) : S)

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
a b : 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 • a ^ n)
s : R
hs : Membership.mem (γ := Submonoid R) R⁰ s
hs' : ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (s • b ^ n)
n : ℕ
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S))
    (∑ x ∈ Finset.range (n + 1), r • a ^ x * s • b ^ (n - x) * (↑(n.choose x) : S))

Tactic:
exact sum_mem fun i _ ↦ mul_mem (mul_mem (hr' _) (hs' _)) (by simp)

Premises used: sum_mem, MulMemClass.mul_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
r : R
⊢ ∀ (n : ℕ),
    Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S))
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n))

Tactic:
simp [← map_pow]

Premises used: map_pow
-- 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
x : S
⊢ Membership.mem (γ := Subalgebra R S) (completeIntegralClosure R S) x ↔ IsAlmostIntegral R x

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, 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 : 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)
obtain :
  ∀ (t : R) (ht : Membership.mem (γ := Submonoid R) R⁰ t)
    (ht' : Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (t • s)),
    ∃ (b : R),
      Membership.mem (γ := Submonoid R) R⁰ b ∧
        ∀ i < Polynomial.natDegree (minpoly R s),
          Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (b • s ^ i)
⊢ ∃ (b : R),
    Membership.mem (γ := Submonoid R) R⁰ b ∧
      ∀ i < Polynomial.natDegree (minpoly R s),
        Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (b • s ^ i)

Tactic:
obtain ⟨t, ht, ht'⟩ := 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
H : IsIntegral R s
t : R
ht : Membership.mem (γ := Submonoid R) R⁰ t
ht' : Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (t • s)
⊢ ∃ (b : R),
    Membership.mem (γ := Submonoid R) R⁰ b ∧
      ∀ i < Polynomial.natDegree (minpoly R s),
        Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (b • s ^ i)

Tactic:
⟨t ^ (minpoly R s).natDegree, pow_mem ht _, fun i hi ↦ ?_⟩

Premises used: minpoly, HPow.hPow, And.intro, Exists.intro, pow_mem, Polynomial.natDegree
-- 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
t : R
ht : Membership.mem (γ := Submonoid R) R⁰ t
ht' : Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (t • s)
refine :
  ∀ (i : ℕ) (hi : i < Polynomial.natDegree (minpoly R s)),
    Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S))
      (t ^ Polynomial.natDegree (minpoly R s) • s ^ i)
⊢ ∃ (b : R),
    Membership.mem (γ := Submonoid R) R⁰ b ∧
      ∀ i < Polynomial.natDegree (minpoly R s),
        Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (b • s ^ i)

Tactic:
refine ⟨t ^ (minpoly R s).natDegree, pow_mem ht _, fun i hi ↦ ?_⟩
-- 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
t : R
ht : Membership.mem (γ := Submonoid R) R⁰ t
ht' : Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (t • s)
i : ℕ
hi : i < Polynomial.natDegree (minpoly R s)
rw :
  Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S))
    (t ^ (Polynomial.natDegree (minpoly R s) - i) • (t • s) ^ i)
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S))
    (t ^ Polynomial.natDegree (minpoly R s) • s ^ i)

Tactic:
rw [← Nat.sub_add_cancel hi.le, pow_add, mul_smul, ← smul_pow]

Premises used: pow_add, LT.lt.le, Nat.sub_add_cancel, smul_pow, SemigroupAction.mul_smul
-- 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
t : R
ht : Membership.mem (γ := Submonoid R) R⁰ t
ht' : Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (t • s)
i : ℕ
hi : i < Polynomial.natDegree (minpoly R s)
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S))
    (t ^ (Polynomial.natDegree (minpoly R s) - i) • (t • s) ^ i)

Tactic:
(AlgHom.range (Algebra.ofId _ _)).smul_mem (Subalgebra.pow_mem _ ht' _) _

Premises used: Set.Mem, Subalgebra.smul_mem, Algebra.ofId, Subalgebra.pow_mem, AlgHom.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
t : R
ht : Membership.mem (γ := Submonoid R) R⁰ t
ht' : Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (t • s)
i : ℕ
hi : i < Polynomial.natDegree (minpoly R s)
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S))
    (t ^ (Polynomial.natDegree (minpoly R s) - i) • (t • s) ^ i)

Tactic:
exact (AlgHom.range (Algebra.ofId _ _)).smul_mem (Subalgebra.pow_mem _ ht' _) _

Premises used: Subalgebra.smul_mem, Algebra.ofId, Subalgebra.pow_mem, AlgHom.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)
obtain :
  ∀ (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)),
    IsAlmostIntegral R s
⊢ IsAlmostIntegral R s

Tactic:
obtain ⟨b, hb', hb⟩ :
      ∃ b ∈ R⁰, ∀ i < (minpoly R s).natDegree, (b • s ^ i) ∈ (algebraMap R S).range := by
    obtain ⟨t, ht, ht'⟩ := h
    refine ⟨t ^ (minpoly R s).natDegree, pow_mem ht _, fun i hi ↦ ?_⟩
    rw [← Nat.sub_add_cancel hi.le, pow_add, mul_smul, ← smul_pow]
    exact (AlgHom.range (Algebra.ofId _ _)).smul_mem (Subalgebra.pow_mem _ ht' _) _

Premises used: Algebra.algebraMap, minpoly, RingHom.range, Polynomial.natDegree
-- 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)
⊢ IsAlmostIntegral R s

Tactic:
⟨b, hb', fun n ↦ ?_⟩

Premises used: IsAlmostIntegral, And.intro, 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
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)
refine : ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (b • s ^ n)
⊢ IsAlmostIntegral R s

Tactic:
refine ⟨b, hb', fun 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
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)
h₁ :
  ∀ (hn : n < Polynomial.natDegree (minpoly R s)),
    Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (b • s ^ n)
h₂ :
  ∀ (hn : Polynomial.natDegree (minpoly R s) ≤ n),
    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:
obtain hn | hn := lt_or_ge n (minpoly R s).natDegree

Premises used: minpoly, lt_or_ge, Polynomial.natDegree
-- 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 : n < Polynomial.natDegree (minpoly R s)
⊢ n < Polynomial.natDegree (minpoly R s)

Tactic:
simpa
-- 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 : n < Polynomial.natDegree (minpoly R s)
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (b • s ^ n)

Tactic:
exact hb _ (by simpa)
-- 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
⊢ Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : Polynomial R) → S) (minpoly R s) : S) (0 : S)

Tactic:
have := minpoly.aeval 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
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 : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : Polynomial R) → S) (minpoly R s) : S) (0 : S)
⊢ s ^ Polynomial.natDegree (minpoly R s) =
    -∑ x ∈ Finset.range (Polynomial.natDegree (minpoly R s)), Polynomial.coeff (minpoly R s) x • s ^ x

Tactic:
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

Premises used: minpoly.monic, add_eq_zero_iff_eq_neg', Polynomial.coeff_natDegree, one_smul, Polynomial.aeval_eq_sum_range, Finset.sum_range_succ
-- 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)),
        b • (s ^ (n - 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)) (b • s ^ n)

Tactic:
rw [← Nat.sub_add_cancel hn, pow_add, this, mul_neg, smul_neg, Finset.mul_sum, Finset.smul_sum]

Premises used: Finset.mul_sum, pow_add, smul_neg, Nat.sub_add_cancel, Finset.smul_sum, mul_neg