awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsIntegrallyClosed R
inst_4 : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst_5 : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
this_1 : Algebra S K := g.toAlgebra
this_2 : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem • x)
z : R
hz : (algebraMap R K : (a : R) → K) z = Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem • x
rw :
  (algebraMap R K : (a : R) → K) z =
    HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem) : R) : K) x
⊢ (RingHom.comp (algebraMap R K) (RingHom.id R) : (a : R) → K) z =
    HMul.hMul (α := K)
      ((RingHom.comp (algebraMap R K) (RingHom.id R) : (a : R) → K)
          (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem) : R) :
        K)
      x
have rw₁ : Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem • x =
  HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem) : R) : K) x
Tactic: rw [RingHom.comp_id, hz, ← Algebra.smul_def, Submonoid.mk_smul]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsIntegrallyClosed R
inst_4 : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst_5 : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
this_1 : Algebra S K := g.toAlgebra
this_2 : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem • x)
z : R
hz : (algebraMap R K : (a : R) → K) z = Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem • x
rw :
  (algebraMap R K : (a : R) → K) z =
    HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem) : R) : K) x
rw₁ :
  Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem • x =
    HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem) : R) : K) x
⊢ (RingHom.comp (algebraMap R K) (RingHom.id R) : (a : R) → K) z =
    HMul.hMul (α := K)
      ((RingHom.comp (algebraMap R K) (RingHom.id R) : (a : R) → K)
          (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem) : R) :
        K)
      x
have rw₂ : Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem • x = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem) : R) • x
Tactic: rw [RingHom.comp_id, hz, ← Algebra.smul_def, Submonoid.mk_smul]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsIntegrallyClosed R
inst_4 : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst_5 : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
this_1 : Algebra S K := g.toAlgebra
this_2 : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem • x)
z : R
hz : (algebraMap R K : (a : R) → K) z = Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem • x
rw :
  (algebraMap R K : (a : R) → K) z =
    HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem) : R) : K) x
rw₁ :
  Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem • x =
    HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem) : R) : K) x
rw₂ : Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem • x = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem) : R) • x
⊢ (RingHom.comp (algebraMap R K) (RingHom.id R) : (a : R) → K) z =
    HMul.hMul (α := K)
      ((RingHom.comp (algebraMap R K) (RingHom.id R) : (a : R) → K)
          (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem) : R) :
        K)
      x
have rw₃ : y • x = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem) : R) • x
Tactic: rw [RingHom.comp_id, hz, ← Algebra.smul_def, Submonoid.mk_smul]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_4
inst : CommRing R
inst_1 : Ring S
inst_2 : Ring T
f : R →+* S
x : S
hx : f.IsIntegralElem x
g : S →+* T
⊢ (g.comp f).IsIntegralElem ((g : (a : S) → T) x)
have obtain : ∀ (p : R[X]) (hp : p.Monic) (hx : eval₂ f x p = 0), (g.comp f).IsIntegralElem ((g : (a : S) → T) x)
Tactic: obtain ⟨p, hp, hx⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_4
inst : CommRing R
inst_1 : Ring S
inst_2 : Ring T
f : R →+* S
x : S
g : S →+* T
p : R[X]
hp : p.Monic
hx : eval₂ f x p = 0
⊢ eval₂ (g.comp f) ((g : (a : S) → T) x) p = 0
have simp_rw : ∀ (hx : eval x (Polynomial.map f p) = 0),
  Eq.{u_4 + 1} (α := T) ((g : (a : S) → T) (eval x (Polynomial.map f p)) : T) (0 : T)
Tactic: simp_rw [← hom_eval₂, eval₂_eq_eval_map] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_4
inst : CommRing R
inst_1 : Ring S
inst_2 : Ring T
f : R →+* S
g : S →+* T
hg : Function.Injective.{u_2 + 1, u_4 + 1} (α := S) (β := T) (⇑g : (a : S) → T)
x : S
hx : (g.comp f).IsIntegralElem ((g : (a : S) → T) x)
⊢ f.IsIntegralElem x
have obtain : ∀ (p : R[X]) (hp : p.Monic) (hx : eval₂ (g.comp f) ((g : (a : S) → T) x) p = 0), f.IsIntegralElem x
Tactic: obtain ⟨p, hp, hx⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring T
f : R →+* S
g : S →+* T
x : T
hx : (g.comp f).IsIntegralElem x
⊢ g.IsIntegralElem x
have obtain : ∀ (p : R[X]) (hp : p.Monic) (hx : eval₂ (g.comp f) x p = 0), g.IsIntegralElem x
Tactic: obtain ⟨p, hp, hx⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_6
C : Type u_7
F : Type u_8
inst_3 : Ring B
inst_4 : Ring C
inst_5 : Algebra R B
inst_6 : Algebra A B
inst_7 : Algebra R C
inst_8 : IsScalarTower R A B
inst_9 : Algebra A C
inst_10 : IsScalarTower R A C
b : B
inst_11 : FunLike F B C
inst_12 : AlgHomClass F A B C
f : F
hb : IsIntegral R b
⊢ IsIntegral.{u_1, u_7} R (A := C) ((f : (a : B) → C) b : C)
have rw : RingHom.IsIntegralElem
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(AlgHom.restrictScalars R (↑f : B →ₐ[A] C)) : B →+* C)
    (algebraMap R B))
  ((f : (a : B) → C) b)
Tactic: rw [IsIntegral, ← ((AlgHomClass.toAlgHom f).restrictScalars R).comp_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (hypothesis)
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
⊢ Eq (α := Submodule R A) (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A))
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[x])
have a : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (hypothesis)
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
h : Nontrivial A
⊢ Eq (α := Submodule R A) (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A))
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[x])
have hf1 : f ≠ 1
Tactic: have hf1 : f ≠ 1 := by rintro rfl; simp [one_ne_zero' A] at hfx
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
h : Nontrivial A
hf1 : f ≠ 1
⊢ Eq (α := Submodule R A) (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A))
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[x])
have refine_1 : ∀ (s : A) (hs : s ∈ (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A)),
  s ∈ (↑((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[x] : Submodule R A) : Set A)
Tactic: refine (span_le.mpr fun s hs ↦ ?_).antisymm fun r hr ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
h : Nontrivial A
hf1 : f ≠ 1
refine_1 :
  ∀ (s : A) (hs : s ∈ (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A)),
    s ∈ (↑((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[x] : Submodule R A) : Set A)
⊢ Eq (α := Submodule R A) (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A))
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[x])
have refine_2 : ∀ (r : A)
  (hr :
    Membership.mem (γ := Submodule R A)
      ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[x] : Submodule R A) r),
  Membership.mem (γ := Submodule R A)
    (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A)) r
Tactic: refine (span_le.mpr fun s hs ↦ ?_).antisymm fun r hr ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
h : Nontrivial A
hf1 : f ≠ 1
s : A
hs : s ∈ (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A)
⊢ s ∈ (↑((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[x] : Submodule R A) : Set A)
have refine_1 : ∀ (k : ℕ) (hs : x ^ k ∈ (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A)),
  x ^ k ∈ (↑((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[x] : Submodule R A) : Set A)
Tactic: rcases Finset.mem_image.1 (SetLike.mem_coe.mp hs) with ⟨k, -, rfl⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (hypothesis)
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
h : Nontrivial A
hf1 : f ≠ 1
r : A
hr :
  Membership.mem (γ := Submodule R A)
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) R[x] : Submodule R A) r
⊢ Membership.mem (γ := Submodule R A)
    (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A)) r
have hr₁ : Membership.mem (γ := Subalgebra R A) (AlgHom.range (aeval x)) r
Tactic: rw [Subalgebra.mem_toSubmodule, Algebra.adjoin_singleton_eq_range_aeval] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
h : Nontrivial A
hf1 : f ≠ 1
r : A
hr : Membership.mem (γ := Subalgebra R A) (AlgHom.range (aeval x)) r
⊢ Membership.mem (γ := Submodule R A)
    (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A)) r
have refine_2 : ∀ (p : R[X])
  (hr : Membership.mem (α := A) (γ := Subalgebra R A) (AlgHom.range (aeval x)) ((aeval x : (a : R[X]) → A) p : A)),
  Membership.mem (α := A) (γ := Submodule R A)
    (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A))
    ((aeval x : (a : R[X]) → A) p : A)
Tactic: rcases (aeval x).mem_range.mp hr with ⟨p, rfl⟩
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
h : Nontrivial A
hf1 : f ≠ 1
p : R[X]
hr : Membership.mem (α := A) (γ := Subalgebra R A) (AlgHom.range (aeval x)) ((aeval x : (a : R[X]) → A) p : A)
⊢ Membership.mem (α := A) (γ := Submodule R A)
    (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A))
    ((aeval x : (a : R[X]) → A) p : A)
have refine_2 : Membership.mem (γ := Submodule R A)
  (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A))
  (∑ n ∈ (p %ₘ f).support,
    eval₂ (algebraMap R A) x
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((p %ₘ f).coeff n) : R[X]) (HPow.hPow (α := R[X]) X n)))
Tactic: rw [← modByMonic_add_div p f, map_add, map_mul, hfx,
      zero_mul, add_zero, ← sum_C_mul_X_pow_eq (p %ₘ f), aeval_def, eval₂_sum, sum_def]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
h : Nontrivial A
hf1 : f ≠ 1
p : R[X]
hr : Membership.mem (α := A) (γ := Subalgebra R A) (AlgHom.range (aeval x)) ((aeval x : (a : R[X]) → A) p : A)
⊢ Membership.mem (γ := Submodule R A)
    (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A))
    (∑ n ∈ (p %ₘ f).support,
      eval₂ (algebraMap R A) x
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((p %ₘ f).coeff n) : R[X]) (HPow.hPow (α := R[X]) X n)))
have refine_2 : ∀ (k : ℕ) (hkq : k ∈ (p %ₘ f).support),
  Membership.mem (γ := Submodule R A)
    (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A))
    (eval₂ (algebraMap R A) x
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((p %ₘ f).coeff k) : R[X]) (HPow.hPow (α := R[X]) X k)))
Tactic: refine sum_mem fun k hkq ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_6
A : Type u_7
inst : CommRing R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : Eq.{u_7 + 1} (α := A) ((aeval x : (a : R[X]) → A) f : A) (0 : A)
h : Nontrivial A
hf1 : f ≠ 1
p : R[X]
hr : Membership.mem (α := A) (γ := Subalgebra R A) (AlgHom.range (aeval x)) ((aeval x : (a : R[X]) → A) p : A)
k : ℕ
hkq : k ∈ (p %ₘ f).support
⊢ Membership.mem (γ := Submodule R A)
    (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A))
    (eval₂ (algebraMap R A) x
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((p %ₘ f).coeff k) : R[X]) (HPow.hPow (α := R[X]) X k)))
have refine_2 : Membership.mem (γ := Submodule R A)
  (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set A)) ((p %ₘ f).coeff k • x ^ k)
Tactic: rw [C_mul_X_pow_eq_monomial, eval₂_monomial, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x : B
hx : IsIntegral R x
⊢ FG.{u_1, u_3} (R := R) (M := B) ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) R[x])
have rcases : ∀ (f : R[X]) (hfm : f.Monic) (hfx : eval₂ (algebraMap R B) x f = 0),
  FG.{u_1, u_3} (R := R) (M := B) ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) R[x])
Tactic: rcases hx with ⟨f, hfm, hfx⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x : B
f : R[X]
hfm : f.Monic
hfx : eval₂ (algebraMap R B) x f = 0
⊢ FG.{u_1, u_3} (R := R) (M := B) ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) R[x])
have h : Eq (α := Submodule R B) (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set B))
  ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) R[x])
Tactic: use (Finset.range <| f.natDegree).image (x ^ ·)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x : B
hx : IsIntegral R x
⊢ FG.{u_1, u_3} (R := R) (M := B) ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) R[x])
have rcases : ∀ (f : R[X]) (hfm : f.Monic) (hfx : eval₂ (algebraMap R B) x f = 0),
  FG.{u_1, u_3} (R := R) (M := B) ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) R[x])
Tactic: classical
  rcases hx with ⟨f, hfm, hfx⟩
  use (Finset.range <| f.natDegree).image (x ^ ·)
  exact span_range_natDegree_eq_adjoin hfm (by rwa [aeval_def])
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x : B
hx : IsIntegral R x
rcases :
  ∀ (f : R[X]) (hfm : f.Monic) (hfx : eval₂ (algebraMap R B) x f = 0),
    FG.{u_1, u_3} (R := R) (M := B) ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) R[x])
⊢ FG.{u_1, u_3} (R := R) (M := B) ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) R[x])
have h : ∀ (f : R[X]) (hfm : f.Monic) (hfx : eval₂ (algebraMap R B) x f = 0),
  Eq (α := Submodule R B) (span R (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range f.natDegree)) : Set B))
    ((Subalgebra.toSubmodule : (a : Subalgebra R B) → Submodule R B) R[x])
Tactic: classical
  rcases hx with ⟨f, hfm, hfx⟩
  use (Finset.range <| f.natDegree).image (x ^ ·)
  exact span_range_natDegree_eq_adjoin hfm (by rwa [aeval_def])
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x : B
n : ℕ
hn : 0 < n
hx : IsIntegral R (x ^ n)
p : R[X]
hmonic : p.Monic
heval : eval₂ (algebraMap R B) (x ^ n) p = 0
⊢ eval₂ (algebraMap R B) x ((expand R n : (a : R[X]) → R[X]) p) = 0
have rwa : Eq.{u_3 + 1} (α := B) ((aeval x : (a : R[X]) → B) ((expand R n : (a : R[X]) → R[X]) p : R[X]) : B) (0 : B)
Tactic: rwa [← aeval_def, expand_aeval]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
B : Type u_3
inst : CommRing R
inst_1 : Ring B
inst_2 : Algebra R B
x : B
n : ℕ
hn : 0 < n
hx : IsIntegral R (x ^ n)
p : R[X]
hmonic : p.Monic
heval : eval₂ (algebraMap R B) (x ^ n) p = 0
rwa : Eq.{u_3 + 1} (α := B) ((aeval x : (a : R[X]) → B) ((expand R n : (a : R[X]) → R[X]) p : R[X]) : B) (0 : B)
⊢ eval₂ (algebraMap R B) x ((expand R n : (a : R[X]) → R[X]) p) = 0
have rwa₁ : Eq.{u_3 + 1} (α := B) ((aeval (x ^ n) : (a : R[X]) → B) p : B) (0 : B)
Tactic: rwa [← aeval_def, expand_aeval]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
x : A
p_1 : R[X]
monic : p_1.Monic
deg : p_1.natDegree ≠ 0
hx : IsIntegral.{u_1, u_2} R (A := A) ((aeval x : (a : R[X]) → A) p_1 : A)
p : R[X]
hmonic : p.Monic
heval : eval₂ (algebraMap R A) ((aeval x : (a : R[X]) → A) p_1) p = 0
⊢ eval₂ (algebraMap R A) x (p.comp p_1) = 0
have rwa : eval₂ (algebraMap R A) (eval₂ (algebraMap R A) x p_1) p = 0
Tactic: rwa [eval₂_comp, ← aeval_def x]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
T : Type u_7
U : Type u_8
inst : CommRing R
inst_1 : Ring S
inst_2 : CommRing T
inst_3 : Ring U
inst_4 : Algebra R S
inst_5 : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = ψ.comp (algebraMap R S)
a : S
ha : IsIntegral R a
p : R[X]
hp : p.Monic ∧ eval₂ (algebraMap R S) a p = 0
⊢ eval₂ (algebraMap T U) ((ψ : (a : S) → U) a) (Polynomial.map φ p) = 0
have rw : Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (algebraMap T U) (Polynomial.map φ p)) : U) (0 : U)
Tactic: rw [← eval_map, map_map, h, ← map_map, eval_map, eval₂_at_apply, eval_map, hp.2, ψ.map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
T : Type u_7
U : Type u_8
inst : CommRing R
inst_1 : Ring S
inst_2 : CommRing T
inst_3 : Ring U
inst_4 : Algebra R S
inst_5 : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = ψ.comp (algebraMap R S)
a : S
ha : IsIntegral R a
p : R[X]
hp : p.Monic ∧ eval₂ (algebraMap R S) a p = 0
rw :
  Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (algebraMap T U) (Polynomial.map φ p)) : U) (0 : U)
⊢ eval₂ (algebraMap T U) ((ψ : (a : S) → U) a) (Polynomial.map φ p) = 0
have rw₁ : Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (RingHom.comp (algebraMap T U) φ) p) : U) (0 : U)
Tactic: rw [← eval_map, map_map, h, ← map_map, eval_map, eval₂_at_apply, eval_map, hp.2, ψ.map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
T : Type u_7
U : Type u_8
inst : CommRing R
inst_1 : Ring S
inst_2 : CommRing T
inst_3 : Ring U
inst_4 : Algebra R S
inst_5 : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = ψ.comp (algebraMap R S)
a : S
ha : IsIntegral R a
p : R[X]
hp : p.Monic ∧ eval₂ (algebraMap R S) a p = 0
rw :
  Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (algebraMap T U) (Polynomial.map φ p)) : U) (0 : U)
rw₁ :
  Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (RingHom.comp (algebraMap T U) φ) p) : U) (0 : U)
⊢ eval₂ (algebraMap T U) ((ψ : (a : S) → U) a) (Polynomial.map φ p) = 0
have rw₂ : Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (ψ.comp (algebraMap R S)) p) : U) (0 : U)
Tactic: rw [← eval_map, map_map, h, ← map_map, eval_map, eval₂_at_apply, eval_map, hp.2, ψ.map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
T : Type u_7
U : Type u_8
inst : CommRing R
inst_1 : Ring S
inst_2 : CommRing T
inst_3 : Ring U
inst_4 : Algebra R S
inst_5 : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = ψ.comp (algebraMap R S)
a : S
ha : IsIntegral R a
p : R[X]
hp : p.Monic ∧ eval₂ (algebraMap R S) a p = 0
rw :
  Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (algebraMap T U) (Polynomial.map φ p)) : U) (0 : U)
rw₁ :
  Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (RingHom.comp (algebraMap T U) φ) p) : U) (0 : U)
rw₂ : Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map (ψ.comp (algebraMap R S)) p) : U) (0 : U)
⊢ eval₂ (algebraMap T U) ((ψ : (a : S) → U) a) (Polynomial.map φ p) = 0
have rw₃ : Eq.{u_8 + 1} (α := U) (eval ((ψ : (a : S) → U) a) (Polynomial.map ψ (Polynomial.map (algebraMap R S) p)) : U) (0 : U)
Tactic: rw [← eval_map, map_map, h, ← map_map, eval_map, eval₂_at_apply, eval_map, hp.2, ψ.map_zero]