awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
⊢ 1 ∈ HPow.hPow (β := ℕ) I 0

Tactic:
simp
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
i : ℕ
h : ¬i = 0
⊢ 0 ∈ I ^ i

Tactic:
simp
-- Module: Mathlib.RingTheory.ReesAlgebra
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 : ℕ
rw : a.coeff i + b.coeff i ∈ I ^ i
⊢ (a + b).coeff i ∈ I ^ i

Tactic:
rw [coeff_add]

Premises used: Polynomial.coeff_add
-- Module: Mathlib.RingTheory.ReesAlgebra
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.coeff i + b.coeff i ∈ I ^ i

Tactic:
Ideal.add_mem _ (hf i) (hg i)

Premises used: Ideal.add_mem
-- Module: Mathlib.RingTheory.ReesAlgebra
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.coeff i + b.coeff i ∈ I ^ i

Tactic:
exact Ideal.add_mem _ (hf i) (hg i)

Premises used: Ideal.add_mem
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
r : R
i : ℕ
rw : Membership.mem (α := R) (I ^ i) (if i = 0 then (algebraMap R R : (a : R) → R) r else 0 : R)
⊢ coeff ((algebraMap R R[X] : (a : R) → R[X]) r) i ∈ I ^ i

Tactic:
rw [algebraMap_apply, coeff_C]

Premises used: Polynomial.algebraMap_apply, Polynomial.coeff_C
-- Module: Mathlib.RingTheory.ReesAlgebra
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)
neg : ∀ (h : ¬i = 0), 0 ∈ I ^ i
⊢ Membership.mem (α := R) (I ^ i) (if i = 0 then (algebraMap R R : (a : R) → R) r else 0 : R)

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.ReesAlgebra
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
pos : Membership.mem (α := R) (HPow.hPow (β := ℕ) I 0) ((algebraMap R R : (a : R) → R) r : R)
⊢ Membership.mem (α := R) (I ^ i) ((algebraMap R R : (a : R) → R) r : R)

Tactic:
subst h
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
r : R
⊢ Membership.mem (α := R) (HPow.hPow (β := ℕ) I 0) ((algebraMap R R : (a : R) → R) r : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.ReesAlgebra
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
⊢ 0 ∈ I ^ i

Tactic:
simp
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R : Type u
inst : CommRing R
I : Ideal R
f : R[X]
⊢ f ∈ reesAlgebra I ↔ ∀ (i : ℕ), f.coeff i ∈ I ^ i

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R : Type u
inst : CommRing R
I : Ideal R
f : R[X]
h : ∀ (a : ℕ), f.coeff a ∈ I ^ a ↔ a ∈ f.support → f.coeff a ∈ I ^ a
⊢ f ∈ reesAlgebra I ↔ ∀ i ∈ f.support, f.coeff i ∈ I ^ i

Tactic:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R : Type u
inst : CommRing R
I : Ideal R
f : R[X]
a : ℕ
h : f.coeff a = 0 → f.coeff a ∈ I ^ a
⊢ f.coeff a ∈ I ^ a ↔ a ∈ f.support → f.coeff a ∈ I ^ a

Tactic:
rw [mem_support_iff, Iff.comm, Classical.imp_iff_right_iff, Ne, ← imp_iff_not_or]

Premises used: Polynomial.mem_support_iff, Ne, imp_iff_not_or, Classical.imp_iff_right_iff, Iff.comm
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R : Type u
inst : CommRing R
I : Ideal R
f : R[X]
a : ℕ
⊢ f.coeff a = 0 → f.coeff a ∈ I ^ a

Tactic:
fun e => e.symm ▸ (I ^ a).zero_mem

Premises used: Eq.rec, Ideal.zero_mem, HPow.hPow, Eq.symm
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R : Type u
inst : CommRing R
I : Ideal R
f : R[X]
a : ℕ
⊢ f.coeff a = 0 → f.coeff a ∈ I ^ a

Tactic:
exact fun e => e.symm ▸ (I ^ a).zero_mem
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R : Type u
inst : CommRing R
I : Ideal R
i : ℕ
r : R
⊢ Membership.mem (α := R[X]) (reesAlgebra I) ((monomial i : (a : R) → R[X]) r : R[X]) ↔ r ∈ I ^ i

Tactic:
simp +contextual [mem_reesAlgebra_iff_support, coeff_monomial, ←
    imp_iff_not_or]

Premises used: mem_reesAlgebra_iff_support, Polynomial.coeff_monomial, imp_iff_not_or
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R : Type u
inst : CommRing R
I : Ideal R
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:
Subalgebra.algebraMap_mem _ _

Premises used: Set.Mem, Subalgebra.algebraMap_mem
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R : Type u
inst : CommRing R
I : Ideal R
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:
exact Subalgebra.algebraMap_mem _ _

Premises used: Subalgebra.algebraMap_mem
-- Module: Mathlib.RingTheory.ReesAlgebra
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)
⊢ r ∈ I * I ^ n

Tactic:
rw [pow_succ'] at hr

Premises used: pow_succ'
-- Module: Mathlib.RingTheory.ReesAlgebra
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])

Tactic:
Submodule.smul_induction_on hr ?_ ?_

Premises used: Submodule.smul_induction_on
-- Module: Mathlib.RingTheory.ReesAlgebra
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])
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])
⊢ 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:
refine Submodule.smul_induction_on hr ?_ ?_
-- Module: Mathlib.RingTheory.ReesAlgebra
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
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]))
⊢ 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])

Tactic:
rw [add_comm n 1, smul_eq_mul, ← monomial_mul_monomial]

Premises used: add_comm, smul_eq_mul, OfNat.ofNat, Polynomial.monomial_mul_monomial
-- Module: Mathlib.RingTheory.ReesAlgebra
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 (γ := 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:
Subalgebra.mul_mem _ (Algebra.subset_adjoin (Set.mem_image_of_mem _ hr)) (hn hs)

Premises used: Subalgebra.mul_mem, Set.Mem, Algebra.subset_adjoin, Set.mem_image_of_mem
-- Module: Mathlib.RingTheory.ReesAlgebra
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 (γ := 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:
exact Subalgebra.mul_mem _ (Algebra.subset_adjoin (Set.mem_image_of_mem _ hr)) (hn hs)

Premises used: Subalgebra.mul_mem, Algebra.subset_adjoin, Set.mem_image_of_mem
-- Module: Mathlib.RingTheory.ReesAlgebra
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])
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]))
⊢ 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:
rw [map_add]

Premises used: map_add
-- Module: Mathlib.RingTheory.ReesAlgebra
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 (γ := 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:
Subalgebra.add_mem _ hx hy

Premises used: Set.Mem, Subalgebra.add_mem
-- Module: Mathlib.RingTheory.ReesAlgebra
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 (γ := 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:
exact Subalgebra.add_mem _ hx hy

Premises used: Subalgebra.add_mem
-- Module: Mathlib.RingTheory.ReesAlgebra
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])
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])
⊢ 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])

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

Premises used: map_add, add_comm, Subalgebra.algebraMap_mem, smul_eq_mul, OfNat.ofNat, pow_succ', Polynomial.monomial_mul_monomial
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R : Type u
inst : CommRing R
I : Ideal R
a : Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]) ≤ reesAlgebra I
a₁ : reesAlgebra I ≤ Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X])
⊢ Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]) = reesAlgebra I

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R : Type u
inst : CommRing R
I : Ideal R
apply : (↑(Submodule.map (monomial 1) I) : Set R[X]) ⊆ (↑(reesAlgebra I) : Set R[X])
⊢ Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]) ≤ reesAlgebra I

Tactic:
apply Algebra.adjoin_le _

Premises used: Algebra.adjoin_le
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R : Type u
inst : CommRing R
I : Ideal R
r : R
hr : r ∈ (↑I : Set R)
rwa rwa₁ rwa₂ rwa₃ : r ∈ I
⊢ r ∈ HPow.hPow (β := ℕ) I 1

Tactic:
rwa [pow_one]

Premises used: pow_one
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R : Type u
inst : CommRing R
I : Ideal R
r : R
hr : r ∈ (↑I : Set R)
⊢ Membership.mem (α := R[X]) (↑(reesAlgebra I) : Set R[X]) ((monomial 1 : (a : R) → R[X]) r : R[X])

Tactic:
exact reesAlgebra.monomial_mem.mpr (by rwa [pow_one])

Premises used: Iff.mpr, reesAlgebra.monomial_mem
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R : Type u
inst : CommRing R
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
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))
⊢ Membership.mem (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X])) p

Tactic:
rw [p.as_sum_support]

Premises used: Polynomial.as_sum_support
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R : Type u
inst : CommRing R
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
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])
⊢ 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:
apply Subalgebra.sum_mem _ _

Premises used: Subalgebra.sum_mem
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R : Type u
inst : CommRing R
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
i : ℕ
⊢ Membership.mem (α := R[X]) (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
    ((monomial i : (a : R) → R[X]) (p.coeff i) : R[X])

Tactic:
monomial_mem_adjoin_monomial (hp i)

Premises used: monomial_mem_adjoin_monomial
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R : Type u
inst : CommRing R
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
i : ℕ
⊢ Membership.mem (α := R[X]) (γ := Subalgebra R R[X]) (Algebra.adjoin R (↑(Submodule.map (monomial 1) I) : Set R[X]))
    ((monomial i : (a : R) → R[X]) (p.coeff i) : R[X])

Tactic:
exact monomial_mem_adjoin_monomial (hp i)

Premises used: monomial_mem_adjoin_monomial
-- Module: Mathlib.RingTheory.ReesAlgebra
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

Tactic:
obtain ⟨s, hs⟩ := hI
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R : Type u
inst : CommRing R
I : Ideal R
s : Finset R
hs : Ideal.span (↑s : Set R) = I
rw : Subalgebra.FG (Algebra.adjoin R (↑(Submodule.map (monomial 1) (Ideal.span (↑s : Set R))) : Set R[X]))
⊢ (reesAlgebra I).FG

Tactic:
rw [← adjoin_monomial_eq_reesAlgebra, ← hs]

Premises used: adjoin_monomial_eq_reesAlgebra
-- Module: Mathlib.RingTheory.ReesAlgebra
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 (↑(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]))
⊢ Subalgebra.FG (Algebra.adjoin R (↑(Submodule.map (monomial 1) (Ideal.span (↑s : Set R))) : Set R[X]))

Tactic:
use s.image (monomial 1)

Premises used: Polynomial.monomial, OfNat.ofNat, DFunLike.coe, Finset.image
-- Module: Mathlib.RingTheory.ReesAlgebra
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.map (monomial 1) (Ideal.span (↑s : Set R))) : Set R[X]))
⊢ 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:
rw [Finset.coe_image]

Premises used: Finset.coe_image
-- Module: Mathlib.RingTheory.ReesAlgebra
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]))
h₁ 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)))
⊢ 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]))

Tactic:
rw [Submodule.map_span, Algebra.adjoin_span]

Premises used: Algebra.adjoin_span, Submodule.map_span
-- Module: Mathlib.RingTheory.ReesAlgebra
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]))
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]))
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) (Submodule.span R (↑s : Set R))) : Set R[X]))
⊢ (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]

Premises used: adjoin_monomial_eq_reesAlgebra, Algebra.adjoin_span, Finset.coe_image, Submodule.map_span
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
⊢ Algebra.FiniteType R ↥(reesAlgebra I)

Tactic:
⟨(reesAlgebra I).fg_top.mpr (reesAlgebra.fg <| IsNoetherian.noetherian I)⟩

Premises used: Iff.mpr, IsNoetherian.noetherian, reesAlgebra.fg, Subalgebra.fg_top, Algebra.FiniteType.mk, reesAlgebra
-- Module: Mathlib.RingTheory.ReesAlgebra
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
⊢ IsNoetherianRing.{u} ↥(reesAlgebra I)

Tactic:
Algebra.FiniteType.isNoetherianRing R _

Premises used: Set.Mem, Algebra.FiniteType.isNoetherianRing
-- Module: Mathlib.RingTheory.Regular.Category
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
x : M
⊢ Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) r ⊤)
      (((HSMul.hSMul (β := Submodule R M) r ⊤).mkQ : (a : M) → M ⧸ r • ⊤) x : M ⧸ HSMul.hSMul (β := Submodule R M) r ⊤)
      (0 : M ⧸ HSMul.hSMul (β := Submodule R M) r ⊤) ↔
    Membership.mem (γ := Set M) (Set.range (ι := M) (⇑((lsmul R M : (a : R) → M →ₗ[R] M) r : M →ₗ[R] M) : (a : M) → M))
      x

Tactic:
simp [Submodule.mem_smul_pointwise_iff_exists, Submodule.mem_smul_pointwise_iff_exists]

Premises used: Submodule.mem_smul_pointwise_iff_exists
-- Module: Mathlib.RingTheory.Regular.Category
Goal:
R : Type u
inst : CommRing R
M : ModuleCat.{v, u} R
r : R
⊢ (M.smulShortComplex r).f = HSMul.hSMul (β := M ⟶ M) r (𝟙 M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Regular.Category
Goal:
R : Type u
inst : CommRing R
M : ModuleCat.{v, u} R
r : R
⊢ (M.smulShortComplex r).Exact

Tactic:
ModuleCat.shortComplex_exact _ (LinearMap.exact_lsmul_mkQ_smul_top M r)

Premises used: LinearMap.exact_lsmul_mkQ_smul_top, ModuleCat.carrier, ModuleCat.shortComplex_exact