awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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
⊢ x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
have haveI : ∀ (this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)),
  x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
Tactic: classical
  haveI : FiniteDimensional (FractionRing A) (FractionRing B) := .of_isLocalization A B A⁰
  by_cases hx : x = 0
  · exact ⟨1, by simp [hx]⟩
  let K := FractionRing A
  let L := FractionRing B
  let E := AlgebraicClosure L
  suffices IsIntegral A ((algebraMap B L x)⁻¹ * (algebraMap A L (intNorm A B x))) by
    obtain ⟨y, hy⟩ := IsIntegrallyClosed.isIntegral_iff.mp <|
      _root_.IsIntegral.tower_top (A := B) this
    refine ⟨y, ?_⟩
    apply FaithfulSMul.algebraMap_injective B L
    rw [← algebraMap_apply, map_mul, hy, mul_inv_cancel_left₀]
    exact (map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective B L)).mpr hx
  rw [← isIntegral_algHom_iff (toAlgHom A L E)
    (FaithfulSMul.algebraMap_injective L E), coe_toAlgHom', map_mul, map_inv₀,
    algebraMap_apply A K L, algebraMap_intNorm (L := L), ← algebraMap_apply, ← algebraMap_apply,
    norm_eq_prod_roots _ (IsAlgClosed.splits _), ← Multiset.prod_erase
    (a := algebraMap B E x)]
  · have := IsTorsionFree.trans_faithfulSMul B L E
    rw [mul_pow, ← mul_pow_sub_one (Nat.pos_iff_ne_zero.1 Module.finrank_pos) (algebraMap B E x),
      mul_assoc, inv_mul_cancel_left₀]
    · refine IsIntegral.mul (IsIntegral.pow ?_ _)
        (IsIntegral.pow (IsIntegral.multiset_prod (fun a ha ↦ ⟨minpoly A x, minpoly.monic
          (IsIntegral.isIntegral x), ?_⟩)) _)
      · exact (isIntegral_algebraMap_iff (isTorsionFree_iff_algebraMap_injective.1 this)).mpr
          (IsIntegral.isIntegral x)
      · replace ha := Multiset.erase_subset _ _ ha
        suffices (aeval a) ((minpoly A x).map (algebraMap A K)) = 0 by simpa
        rw [← minpoly.isIntegrallyClosed_eq_field_fractions K L (IsIntegral.isIntegral x)]
        simp only [mem_roots', ne_eq, Polynomial.map_eq_zero, IsRoot.def, eval_map_algebraMap] at ha
        exact ha.2
    · exact (map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective B E)).mpr hx
  · simp only [mem_roots', ne_eq, Polynomial.map_eq_zero, IsRoot.def, eval_map_algebraMap]
    refine ⟨minpoly.ne_zero (IsIntegral.isIntegral _), ?_⟩
    simp [algebraMap_apply B L E, aeval_algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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
haveI haveI₁ haveI₂ :
  ∀ (this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)),
    x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
⊢ x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
have pos : ∀ (this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)) (hx : x = 0),
  x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
Tactic: classical
  haveI : FiniteDimensional (FractionRing A) (FractionRing B) := .of_isLocalization A B A⁰
  by_cases hx : x = 0
  · exact ⟨1, by simp [hx]⟩
  let K := FractionRing A
  let L := FractionRing B
  let E := AlgebraicClosure L
  suffices IsIntegral A ((algebraMap B L x)⁻¹ * (algebraMap A L (intNorm A B x))) by
    obtain ⟨y, hy⟩ := IsIntegrallyClosed.isIntegral_iff.mp <|
      _root_.IsIntegral.tower_top (A := B) this
    refine ⟨y, ?_⟩
    apply FaithfulSMul.algebraMap_injective B L
    rw [← algebraMap_apply, map_mul, hy, mul_inv_cancel_left₀]
    exact (map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective B L)).mpr hx
  rw [← isIntegral_algHom_iff (toAlgHom A L E)
    (FaithfulSMul.algebraMap_injective L E), coe_toAlgHom', map_mul, map_inv₀,
    algebraMap_apply A K L, algebraMap_intNorm (L := L), ← algebraMap_apply, ← algebraMap_apply,
    norm_eq_prod_roots _ (IsAlgClosed.splits _), ← Multiset.prod_erase
    (a := algebraMap B E x)]
  · have := IsTorsionFree.trans_faithfulSMul B L E
    rw [mul_pow, ← mul_pow_sub_one (Nat.pos_iff_ne_zero.1 Module.finrank_pos) (algebraMap B E x),
      mul_assoc, inv_mul_cancel_left₀]
    · refine IsIntegral.mul (IsIntegral.pow ?_ _)
        (IsIntegral.pow (IsIntegral.multiset_prod (fun a ha ↦ ⟨minpoly A x, minpoly.monic
          (IsIntegral.isIntegral x), ?_⟩)) _)
      · exact (isIntegral_algebraMap_iff (isTorsionFree_iff_algebraMap_injective.1 this)).mpr
          (IsIntegral.isIntegral x)
      · replace ha := Multiset.erase_subset _ _ ha
        suffices (aeval a) ((minpoly A x).map (algebraMap A K)) = 0 by simpa
        rw [← minpoly.isIntegrallyClosed_eq_field_fractions K L (IsIntegral.isIntegral x)]
        simp only [mem_roots', ne_eq, Polynomial.map_eq_zero, IsRoot.def, eval_map_algebraMap] at ha
        exact ha.2
    · exact (map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective B E)).mpr hx
  · simp only [mem_roots', ne_eq, Polynomial.map_eq_zero, IsRoot.def, eval_map_algebraMap]
    refine ⟨minpoly.ne_zero (IsIntegral.isIntegral _), ?_⟩
    simp [algebraMap_apply B L E, aeval_algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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
haveI haveI₁ haveI₂ :
  ∀ (this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)),
    x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
pos :
  ∀ (this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)) (hx : x = 0),
    x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
⊢ x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
have neg : ∀ (this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)) (hx : ¬x = 0),
  x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
Tactic: classical
  haveI : FiniteDimensional (FractionRing A) (FractionRing B) := .of_isLocalization A B A⁰
  by_cases hx : x = 0
  · exact ⟨1, by simp [hx]⟩
  let K := FractionRing A
  let L := FractionRing B
  let E := AlgebraicClosure L
  suffices IsIntegral A ((algebraMap B L x)⁻¹ * (algebraMap A L (intNorm A B x))) by
    obtain ⟨y, hy⟩ := IsIntegrallyClosed.isIntegral_iff.mp <|
      _root_.IsIntegral.tower_top (A := B) this
    refine ⟨y, ?_⟩
    apply FaithfulSMul.algebraMap_injective B L
    rw [← algebraMap_apply, map_mul, hy, mul_inv_cancel_left₀]
    exact (map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective B L)).mpr hx
  rw [← isIntegral_algHom_iff (toAlgHom A L E)
    (FaithfulSMul.algebraMap_injective L E), coe_toAlgHom', map_mul, map_inv₀,
    algebraMap_apply A K L, algebraMap_intNorm (L := L), ← algebraMap_apply, ← algebraMap_apply,
    norm_eq_prod_roots _ (IsAlgClosed.splits _), ← Multiset.prod_erase
    (a := algebraMap B E x)]
  · have := IsTorsionFree.trans_faithfulSMul B L E
    rw [mul_pow, ← mul_pow_sub_one (Nat.pos_iff_ne_zero.1 Module.finrank_pos) (algebraMap B E x),
      mul_assoc, inv_mul_cancel_left₀]
    · refine IsIntegral.mul (IsIntegral.pow ?_ _)
        (IsIntegral.pow (IsIntegral.multiset_prod (fun a ha ↦ ⟨minpoly A x, minpoly.monic
          (IsIntegral.isIntegral x), ?_⟩)) _)
      · exact (isIntegral_algebraMap_iff (isTorsionFree_iff_algebraMap_injective.1 this)).mpr
          (IsIntegral.isIntegral x)
      · replace ha := Multiset.erase_subset _ _ ha
        suffices (aeval a) ((minpoly A x).map (algebraMap A K)) = 0 by simpa
        rw [← minpoly.isIntegrallyClosed_eq_field_fractions K L (IsIntegral.isIntegral x)]
        simp only [mem_roots', ne_eq, Polynomial.map_eq_zero, IsRoot.def, eval_map_algebraMap] at ha
        exact ha.2
    · exact (map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective B E)).mpr hx
  · simp only [mem_roots', ne_eq, Polynomial.map_eq_zero, IsRoot.def, eval_map_algebraMap]
    refine ⟨minpoly.ne_zero (IsIntegral.isIntegral _), ?_⟩
    simp [algebraMap_apply B L E, aeval_algebraMap_apply]
-- 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
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)
have refine : ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) ((r * s) • (a * b) ^ n)
Tactic: refine ⟨r * s, mul_mem hr hs, fun 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
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 * s) • (a * b) ^ n)
have rw : Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (r • a ^ n * s • b ^ n)
Tactic: rw [mul_pow, mul_smul_mul_comm]
-- 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
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)
have refine : ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) ((r * s) • (a + b) ^ n)
Tactic: refine ⟨r * s, mul_mem hr hs, fun 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
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 * s) • (a + b) ^ n)
have 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))
Tactic: simp only [add_pow, Finset.smul_sum, ← smul_mul_assoc _ (_ * _),
      ← smul_mul_smul_comm _ (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
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),
    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)
have 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)
Tactic: obtain ⟨t, ht, ht'⟩ := 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
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)
have 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)
Tactic: refine ⟨t ^ (minpoly R s).natDegree, pow_mem ht _, fun i 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
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) • s ^ i)
have 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)
Tactic: rw [← Nat.sub_add_cancel hi.le, pow_add, mul_smul, ← smul_pow]
-- 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)
⊢ IsAlmostIntegral R s
have 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
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' _) _
-- 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)
⊢ IsAlmostIntegral R s
have refine : ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (b • s ^ n)
Tactic: refine ⟨b, hb', fun 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
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)
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (b • s ^ n)
have 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)
Tactic: obtain hn | hn := lt_or_ge n (minpoly R s).natDegree
-- 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)
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)
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (b • s ^ n)
have 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)
Tactic: obtain hn | hn := lt_or_ge n (minpoly R s).natDegree
-- 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
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (b • s ^ n)
have this : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : Polynomial R) → S) (minpoly R s) : S) (0 : S)
Tactic: have := minpoly.aeval R s
-- 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 : Eq.{u_2 + 1} (α := S) ((Polynomial.aeval s : (a : Polynomial R) → S) (minpoly R s) : S) (0 : S)
⊢ Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R S)) (b • s ^ n)
have this₁ : 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
Cleared hypotheses: 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
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)) (b • s ^ n)
have 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))
Tactic: rw [← Nat.sub_add_cancel hn, pow_add, this, mul_neg, smul_neg, Finset.mul_sum, Finset.smul_sum]
-- 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)),
        b • (s ^ (n - Polynomial.natDegree (minpoly R s)) * Polynomial.coeff (minpoly R s) x • s ^ x))
have 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))
Tactic: simp_rw [mul_smul_comm, ← pow_add, smul_comm b]