awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst_7 : r.LiesOver q
inst_8 : Module.Flat S T
hr : ¬r.IsPrime
⊢ r.ramificationIdx' R = q.ramificationIdx' R * r.ramificationIdx' S
have neg : 0 = q.ramificationIdx' R * r.ramificationIdx' S
Tactic: rw [ramificationIdx'_of_not_isPrime r R hr, ramificationIdx'_of_not_isPrime r S hr, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst_7 : r.LiesOver q
inst_8 : Module.Flat S T
hr : ¬r.IsPrime
neg : 0 = q.ramificationIdx' R * r.ramificationIdx' S
⊢ r.ramificationIdx' R = q.ramificationIdx' R * r.ramificationIdx' S
have neg₁ : 0 = q.ramificationIdx' R * 0
Tactic: rw [ramificationIdx'_of_not_isPrime r R hr, ramificationIdx'_of_not_isPrime r S hr, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst_7 : r.LiesOver q
inst_8 : Module.Flat S T
hr : ¬r.IsPrime
neg : 0 = q.ramificationIdx' R * r.ramificationIdx' S
neg₁ : 0 = q.ramificationIdx' R * 0
⊢ r.ramificationIdx' R = q.ramificationIdx' R * r.ramificationIdx' S
have neg₂ : Eq (α := ℕ) 0 0
Tactic: rw [ramificationIdx'_of_not_isPrime r R hr, ramificationIdx'_of_not_isPrime r S hr, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
a b : R[X]
hf : Membership.mem (γ := Set R[X]) {f : R[X] | ∀ (i : ℕ), f.coeff i ∈ I ^ i} a
hg : Membership.mem (γ := Set R[X]) {f : R[X] | ∀ (i : ℕ), f.coeff i ∈ I ^ i} b
i : ℕ
⊢ (a * b).coeff i ∈ I ^ i
have rw : ∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, a.coeff x.1 * b.coeff x.2 ∈ I ^ i
Tactic: rw [coeff_mul]
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
a b : R[X]
hf : Membership.mem (γ := Set R[X]) {f : R[X] | ∀ (i : ℕ), f.coeff i ∈ I ^ i} a
hg : Membership.mem (γ := Set R[X]) {f : R[X] | ∀ (i : ℕ), f.coeff i ∈ I ^ i} b
i : ℕ
⊢ ∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, a.coeff x.1 * b.coeff x.2 ∈ I ^ i
have a : ∀ c ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, a.coeff c.1 * b.coeff c.2 ∈ I ^ i
Tactic: apply Ideal.sum_mem
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
a b : R[X]
hf : Membership.mem (γ := Set R[X]) {f : R[X] | ∀ (i : ℕ), f.coeff i ∈ I ^ i} a
hg : Membership.mem (γ := Set R[X]) {f : R[X] | ∀ (i : ℕ), f.coeff i ∈ I ^ i} b
i j k : ℕ
e : (j, k) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i
⊢ a.coeff (j, k).1 * b.coeff (j, k).2 ∈ I ^ i
have a : a.coeff (j, k).1 * b.coeff (j, k).2 ∈ I ^ (j, k).1 * I ^ (j, k).2
Tactic: rw [← Finset.mem_antidiagonal.mp e, pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
i : ℕ
⊢ coeff 1 i ∈ I ^ i
have rw : (if i = 0 then 1 else 0) ∈ I ^ i
Tactic: rw [coeff_one]
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
i : ℕ
⊢ (if i = 0 then 1 else 0) ∈ I ^ i
have pos : ∀ (h : i = 0), 1 ∈ I ^ i
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
i : ℕ
pos : ∀ (h : i = 0), 1 ∈ I ^ i
⊢ (if i = 0 then 1 else 0) ∈ I ^ i
have neg : ∀ (h : ¬i = 0), 0 ∈ I ^ i
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
i : ℕ
h : i = 0
⊢ 1 ∈ I ^ i
have pos : 1 ∈ HPow.hPow (β := ℕ) I 0
Tactic: subst h
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
a b : R[X]
hf : Membership.mem (γ := Set R[X]) {f : R[X] | ∀ (i : ℕ), f.coeff i ∈ I ^ i} a
hg : Membership.mem (γ := Set R[X]) {f : R[X] | ∀ (i : ℕ), f.coeff i ∈ I ^ i} b
i : ℕ
⊢ (a + b).coeff i ∈ I ^ i
have rw : a.coeff i + b.coeff i ∈ I ^ i
Tactic: rw [coeff_add]
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
r : R
i : ℕ
⊢ coeff ((algebraMap R R[X] : (a : R) → R[X]) r) i ∈ I ^ i
have rw : Membership.mem (α := R) (I ^ i) (if i = 0 then (algebraMap R R : (a : R) → R) r else 0 : R)
Tactic: rw [algebraMap_apply, coeff_C]
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
r : R
i : ℕ
⊢ Membership.mem (α := R) (I ^ i) (if i = 0 then (algebraMap R R : (a : R) → R) r else 0 : R)
have pos : ∀ (h : i = 0), Membership.mem (α := R) (I ^ i) ((algebraMap R R : (a : R) → R) r : R)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
r : R
i : ℕ
pos : ∀ (h : i = 0), Membership.mem (α := R) (I ^ i) ((algebraMap R R : (a : R) → R) r : R)
⊢ Membership.mem (α := R) (I ^ i) (if i = 0 then (algebraMap R R : (a : R) → R) r else 0 : R)
have neg : ∀ (h : ¬i = 0), 0 ∈ I ^ i
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
r : R
i : ℕ
h : i = 0
⊢ Membership.mem (α := R) (I ^ i) ((algebraMap R R : (a : R) → R) r : R)
have pos : Membership.mem (α := R) (HPow.hPow (β := ℕ) I 0) ((algebraMap R R : (a : R) → R) r : R)
Tactic: subst h
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
f : R[X]
⊢ f ∈ reesAlgebra I ↔ ∀ i ∈ f.support, f.coeff i ∈ I ^ i
have h : ∀ (a : ℕ), f.coeff a ∈ I ^ a ↔ a ∈ f.support → f.coeff a ∈ I ^ a
Tactic: apply forall_congr'
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
f : R[X]
a : ℕ
⊢ f.coeff a ∈ I ^ a ↔ a ∈ f.support → f.coeff a ∈ I ^ a
have h : f.coeff a = 0 → f.coeff a ∈ I ^ a
Tactic: rw [mem_support_iff, Iff.comm, Classical.imp_iff_right_iff, Ne, ← imp_iff_not_or]
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (hypothesis)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
n : ℕ
hn :
  ∀ {r : R} (hr : r ∈ I ^ n),
    Membership.mem (α := R[X]) (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
      ((monomial n : (a : R) → R[X]) r : R[X])
r : R
hr : r ∈ I ^ (n + 1)
⊢ Membership.mem (α := R[X]) (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
    ((monomial (n + 1) : (a : R) → R[X]) r : R[X])
have hr₁ : r ∈ I * I ^ n
Tactic: rw [pow_succ'] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
n : ℕ
hn :
  ∀ {r : R} (hr : r ∈ I ^ n),
    Membership.mem (α := R[X]) (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
      ((monomial n : (a : R) → R[X]) r : R[X])
r : R
hr : r ∈ I * I ^ n
⊢ Membership.mem (α := R[X]) (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
    ((monomial (n + 1) : (a : R) → R[X]) r : R[X])
have succ : ∀ r ∈ I,
  ∀ n_1 ∈ I ^ n,
    Membership.mem (α := R[X]) (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
      ((monomial (n + 1) : (a : R) → R[X]) (r • n_1) : R[X])
Tactic: refine Submodule.smul_induction_on hr ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
n : ℕ
hn :
  ∀ {r : R} (hr : r ∈ I ^ n),
    Membership.mem (α := R[X]) (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
      ((monomial n : (a : R) → R[X]) r : R[X])
r : R
hr : r ∈ I * I ^ n
succ :
  ∀ r ∈ I,
    ∀ n_1 ∈ I ^ n,
      Membership.mem (α := R[X]) (γ := Subalgebra R R[X])
        (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
        ((monomial (n + 1) : (a : R) → R[X]) (r • n_1) : R[X])
⊢ Membership.mem (α := R[X]) (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
    ((monomial (n + 1) : (a : R) → R[X]) r : R[X])
have succ₁ : ∀ (x y : R),
  Membership.mem (α := R[X]) (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
      ((monomial (n + 1) : (a : R) → R[X]) x : R[X]) →
    Membership.mem (α := R[X]) (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
        ((monomial (n + 1) : (a : R) → R[X]) y : R[X]) →
      Membership.mem (α := R[X]) (γ := Subalgebra R R[X])
        (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
        ((monomial (n + 1) : (a : R) → R[X]) (x + y) : R[X])
Tactic: refine Submodule.smul_induction_on hr ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
n : ℕ
hn :
  ∀ {r : R} (hr : r ∈ I ^ n),
    Membership.mem (α := R[X]) (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
      ((monomial n : (a : R) → R[X]) r : R[X])
r_1 : R
hr_1 : r_1 ∈ I * I ^ n
r : R
hr : r ∈ I
s : R
hs : s ∈ I ^ n
⊢ Membership.mem (α := R[X]) (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
    ((monomial (n + 1) : (a : R) → R[X]) (r • s) : R[X])
have succ : Membership.mem (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
  (HMul.hMul (α := R[X]) (β := R[X]) ((monomial 1 : (a : R) → R[X]) r : R[X]) ((monomial n : (a : R) → R[X]) s : R[X]))
Tactic: rw [add_comm n 1, smul_eq_mul, ← monomial_mul_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
n : ℕ
hn :
  ∀ {r : R} (hr : r ∈ I ^ n),
    Membership.mem (α := R[X]) (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
      ((monomial n : (a : R) → R[X]) r : R[X])
r : R
hr : r ∈ I * I ^ n
x y : R
hx :
  Membership.mem (α := R[X]) (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
    ((monomial (n + 1) : (a : R) → R[X]) x : R[X])
hy :
  Membership.mem (α := R[X]) (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
    ((monomial (n + 1) : (a : R) → R[X]) y : R[X])
⊢ Membership.mem (α := R[X]) (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
    ((monomial (n + 1) : (a : R) → R[X]) (x + y) : R[X])
have succ : Membership.mem (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
  (HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial (n + 1) : (a : R) → R[X]) x : R[X])
    ((monomial (n + 1) : (a : R) → R[X]) y : R[X]))
Tactic: rw [map_add]
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
n : ℕ
r : R
hr : r ∈ I ^ n
⊢ Membership.mem (α := R[X]) (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
    ((monomial n : (a : R) → R[X]) r : R[X])
have zero : ∀ {r : R} (hr : r ∈ HPow.hPow (β := ℕ) I 0),
  Membership.mem (α := R[X]) (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
    ((monomial 0 : (a : R) → R[X]) r : R[X])
Tactic: induction n generalizing r with
  | zero => exact Subalgebra.algebraMap_mem _ _
  | succ n hn =>
    rw [pow_succ'] at hr
    refine Submodule.smul_induction_on hr ?_ ?_
    · intro r hr s hs
      rw [add_comm n 1, smul_eq_mul, ← monomial_mul_monomial]
      exact Subalgebra.mul_mem _ (Algebra.subset_adjoin (Set.mem_image_of_mem _ hr)) (hn hs)
    · intro x y hx hy
      rw [map_add]
      exact Subalgebra.add_mem _ hx hy
Cleared hypotheses: n, r, hr
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
n : ℕ
r : R
hr : r ∈ I ^ n
zero :
  ∀ {r : R} (hr : r ∈ HPow.hPow (β := ℕ) I 0),
    Membership.mem (α := R[X]) (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
      ((monomial 0 : (a : R) → R[X]) r : R[X])
⊢ Membership.mem (α := R[X]) (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
    ((monomial n : (a : R) → R[X]) r : R[X])
have succ : ∀ (n : ℕ)
  (hn :
    ∀ {r : R} (hr : r ∈ I ^ n),
      Membership.mem (α := R[X]) (γ := Subalgebra R R[X])
        (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X])) ((monomial n : (a : R) → R[X]) r : R[X]))
  {r : R} (hr : r ∈ I ^ (n + 1)),
  Membership.mem (α := R[X]) (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
    ((monomial (n + 1) : (a : R) → R[X]) r : R[X])
Tactic: induction n generalizing r with
  | zero => exact Subalgebra.algebraMap_mem _ _
  | succ n hn =>
    rw [pow_succ'] at hr
    refine Submodule.smul_induction_on hr ?_ ?_
    · intro r hr s hs
      rw [add_comm n 1, smul_eq_mul, ← monomial_mul_monomial]
      exact Subalgebra.mul_mem _ (Algebra.subset_adjoin (Set.mem_image_of_mem _ hr)) (hn hs)
    · intro x y hx hy
      rw [map_add]
      exact Subalgebra.add_mem _ hx hy
Cleared hypotheses: n, r, hr
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
⊢ Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]) = reesAlgebra I
have a : Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]) ≤ reesAlgebra I
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
a : Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]) ≤ reesAlgebra I
⊢ Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]) = reesAlgebra I
have a₁ : reesAlgebra I ≤ Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X])
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
⊢ Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]) ≤ reesAlgebra I
have apply : (↑(Submodule.map (monomial 1) I) : Set R[X]) ⊆ (↑(reesAlgebra I) : Set R[X])
Tactic: apply Algebra.adjoin_le _
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
r : R
hr : r ∈ (↑I : Set R)
⊢ r ∈ HPow.hPow (β := ℕ) I 1
have rwa : r ∈ I
Tactic: rwa [pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
⊢ Membership.mem (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X])) p
have a : Membership.mem (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
  (∑ i ∈ p.support, (monomial i : (a : R) → R[X]) (p.coeff i))
Tactic: rw [p.as_sum_support]
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
⊢ Membership.mem (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
    (∑ i ∈ p.support, (monomial i : (a : R) → R[X]) (p.coeff i))
have apply : ∀ x ∈ p.support,
  Membership.mem (α := R[X]) (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
    ((monomial x : (a : R) → R[X]) (p.coeff x) : R[X])
Tactic: apply Subalgebra.sum_mem _ _
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hI : I.FG
⊢ (reesAlgebra I).FG
have obtain : ∀ (s : Finset R) (hs : Ideal.span (↑s : Set R) = I), (reesAlgebra I).FG
Tactic: obtain ⟨s, hs⟩ := hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
s : Finset R
hs : Ideal.span (↑s : Set R) = I
⊢ (reesAlgebra I).FG
have rw : Subalgebra.FG (Algebra.adjoin R (↑(Submodule.map (monomial 1) (Ideal.span (↑s : Set R))) : Set R[X]))
Tactic: rw [← adjoin_monomial_eq_reesAlgebra, ← hs]
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
s : Finset R
hs : Ideal.span (↑s : Set R) = I
⊢ Subalgebra.FG (Algebra.adjoin R (↑(Submodule.map (monomial 1) (Ideal.span (↑s : Set R))) : Set R[X]))
have h : Eq (α := Subalgebra R R[X]) (Algebra.adjoin R (↑(Finset.image (⇑(monomial 1) : (a : R) → R[X]) s) : Set R[X]))
  (Algebra.adjoin R (↑(Submodule.map (monomial 1) (Ideal.span (↑s : Set R))) : Set R[X]))
Tactic: use s.image (monomial 1)
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
s : Finset R
hs : Ideal.span (↑s : Set R) = I
⊢ Eq (α := Subalgebra R R[X]) (Algebra.adjoin R (↑(Finset.image (⇑(monomial 1) : (a : R) → R[X]) s) : Set R[X]))
    (Algebra.adjoin R (↑(Submodule.map (monomial 1) (Ideal.span (↑s : Set R))) : Set R[X]))
have h : Eq (α := Subalgebra R R[X]) (Algebra.adjoin R ((⇑(monomial 1) : (a : R) → R[X]) '' (↑s : Set R)))
  (Algebra.adjoin R (↑(Submodule.map (monomial 1) (Ideal.span (↑s : Set R))) : Set R[X]))
Tactic: rw [Finset.coe_image]
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
s : Finset R
hs : Ideal.span (↑s : Set R) = I
⊢ Eq (α := Subalgebra R R[X]) (Algebra.adjoin R ((⇑(monomial 1) : (a : R) → R[X]) '' (↑s : Set R)))
    (Algebra.adjoin R (↑(Submodule.map (monomial 1) (Submodule.span R (↑s : Set R))) : Set R[X]))
have h : Eq (α := Subalgebra R R[X]) (Algebra.adjoin R ((⇑(monomial 1) : (a : R) → R[X]) '' (↑s : Set R)))
  (Algebra.adjoin R (↑(Submodule.span R ((⇑(monomial 1) : (a : R) → R[X]) '' (↑s : Set R))) : Set R[X]))
Tactic: rw [Submodule.map_span, Algebra.adjoin_span]
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
s : Finset R
hs : Ideal.span (↑s : Set R) = I
h :
  Eq (α := Subalgebra R R[X]) (Algebra.adjoin R ((⇑(monomial 1) : (a : R) → R[X]) '' (↑s : Set R)))
    (Algebra.adjoin R (↑(Submodule.span R ((⇑(monomial 1) : (a : R) → R[X]) '' (↑s : Set R))) : Set R[X]))
⊢ Eq (α := Subalgebra R R[X]) (Algebra.adjoin R ((⇑(monomial 1) : (a : R) → R[X]) '' (↑s : Set R)))
    (Algebra.adjoin R (↑(Submodule.map (monomial 1) (Submodule.span R (↑s : Set R))) : Set R[X]))
have h₁ : Eq (α := Subalgebra R R[X]) (Algebra.adjoin R ((⇑(monomial 1) : (a : R) → R[X]) '' (↑s : Set R)))
  (Algebra.adjoin R ((⇑(monomial 1) : (a : R) → R[X]) '' (↑s : Set R)))
Tactic: rw [Submodule.map_span, Algebra.adjoin_span]
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hI : I.FG
⊢ (reesAlgebra I).FG
have obtain : ∀ (s : Finset R) (hs : Ideal.span (↑s : Set R) = I), (reesAlgebra I).FG
Tactic: classical
    obtain ⟨s, hs⟩ := hI
    rw [← adjoin_monomial_eq_reesAlgebra, ← hs]
    use s.image (monomial 1)
    rw [Finset.coe_image]
    change
      _ =
        Algebra.adjoin R
          (Submodule.map (monomial 1 : R →ₗ[R] R[X]) (Submodule.span R ↑s) : Set R[X])
    rw [Submodule.map_span, Algebra.adjoin_span]
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hI : I.FG
obtain : ∀ (s : Finset R) (hs : Ideal.span (↑s : Set R) = I), (reesAlgebra I).FG
⊢ (reesAlgebra I).FG
have obtain₁ : ∀ (s : Finset R) (hs : Ideal.span (↑s : Set R) = I),
  Subalgebra.FG (Algebra.adjoin R (↑(Submodule.map (monomial 1) (Ideal.span (↑s : Set R))) : Set R[X]))
Tactic: classical
    obtain ⟨s, hs⟩ := hI
    rw [← adjoin_monomial_eq_reesAlgebra, ← hs]
    use s.image (monomial 1)
    rw [Finset.coe_image]
    change
      _ =
        Algebra.adjoin R
          (Submodule.map (monomial 1 : R →ₗ[R] R[X]) (Submodule.span R ↑s) : Set R[X])
    rw [Submodule.map_span, Algebra.adjoin_span]
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hI : I.FG
obtain : ∀ (s : Finset R) (hs : Ideal.span (↑s : Set R) = I), (reesAlgebra I).FG
obtain₁ :
  ∀ (s : Finset R) (hs : Ideal.span (↑s : Set R) = I),
    Subalgebra.FG (Algebra.adjoin R (↑(Submodule.map (monomial 1) (Ideal.span (↑s : Set R))) : Set R[X]))
⊢ (reesAlgebra I).FG
have h : ∀ (s : Finset R) (hs : Ideal.span (↑s : Set R) = I),
  Eq (α := Subalgebra R R[X]) (Algebra.adjoin R (↑(Finset.image (⇑(monomial 1) : (a : R) → R[X]) s) : Set R[X]))
    (Algebra.adjoin R (↑(Submodule.map (monomial 1) (Ideal.span (↑s : Set R))) : Set R[X]))
Tactic: classical
    obtain ⟨s, hs⟩ := hI
    rw [← adjoin_monomial_eq_reesAlgebra, ← hs]
    use s.image (monomial 1)
    rw [Finset.coe_image]
    change
      _ =
        Algebra.adjoin R
          (Submodule.map (monomial 1 : R →ₗ[R] R[X]) (Submodule.span R ↑s) : Set R[X])
    rw [Submodule.map_span, Algebra.adjoin_span]
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.ReesAlgebra (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hI : I.FG
obtain : ∀ (s : Finset R) (hs : Ideal.span (↑s : Set R) = I), (reesAlgebra I).FG
obtain₁ :
  ∀ (s : Finset R) (hs : Ideal.span (↑s : Set R) = I),
    Subalgebra.FG (Algebra.adjoin R (↑(Submodule.map (monomial 1) (Ideal.span (↑s : Set R))) : Set R[X]))
h :
  ∀ (s : Finset R) (hs : Ideal.span (↑s : Set R) = I),
    Eq (α := Subalgebra R R[X]) (Algebra.adjoin R (↑(Finset.image (⇑(monomial 1) : (a : R) → R[X]) s) : Set R[X]))
      (Algebra.adjoin R (↑(Submodule.map (monomial 1) (Ideal.span (↑s : Set R))) : Set R[X]))
⊢ (reesAlgebra I).FG
have h₁ : ∀ (s : Finset R) (hs : Ideal.span (↑s : Set R) = I),
  Eq (α := Subalgebra R R[X]) (Algebra.adjoin R ((⇑(monomial 1) : (a : R) → R[X]) '' (↑s : Set R)))
    (Algebra.adjoin R (↑(Submodule.map (monomial 1) (Ideal.span (↑s : Set R))) : Set R[X]))
Tactic: classical
    obtain ⟨s, hs⟩ := hI
    rw [← adjoin_monomial_eq_reesAlgebra, ← hs]
    use s.image (monomial 1)
    rw [Finset.coe_image]
    change
      _ =
        Algebra.adjoin R
          (Submodule.map (monomial 1 : R →ₗ[R] R[X]) (Submodule.span R ↑s) : Set R[X])
    rw [Submodule.map_span, Algebra.adjoin_span]
Cleared hypotheses: hI