-- Mathlib/RingTheory/ReesAlgebra.lean
theorem monomial_mem_adjoin_monomial {I : Ideal R} {n : ℕ} {r : R} (hr : r ∈ I ^ n) :
    monomial n r ∈ Algebra.adjoin R (Submodule.map (monomial 1 : R →ₗ[R] R[X]) I : Set R[X])

Proof state:
case zero
R : Type u
inst✝ : CommRing R
I : Ideal R
r : R
hr : r ∈ I ^ 0
⊢ (monomial 0) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
exact Subalgebra.algebraMap_mem _ _

Result:
no goals

Proof state:
case succ.smul
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r✝ : R
hr✝ : r✝ ∈ I * I ^ n
r : R
hr : r ∈ I
s : R
hs : s ∈ I ^ n
⊢ (monomial 1) r * (monomial n) s ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
exact Subalgebra.mul_mem _ (Algebra.subset_adjoin (Set.mem_image_of_mem _ hr)) (hn hs)

Result:
no goals

Proof state:
case succ.add
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
x y : R
hx : (monomial n.succ) x ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
hy : (monomial n.succ) y ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
⊢ (monomial n.succ) x + (monomial n.succ) y ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
exact Subalgebra.add_mem _ hx hy

Result:
no goals

Proof state:
case succ.smul
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
⊢ ∀ r ∈ I, ∀ n_1 ∈ I ^ n, (monomial n.succ) (r • n_1) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
intro r hr s hs

Result:
case succ.smul
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r✝ : R
hr✝ : r✝ ∈ I * I ^ n
r : R
hr : r ∈ I
s : R
hs : s ∈ I ^ n
⊢ (monomial n.succ) (r • s) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Proof state:
case succ
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
⊢ (monomial (n + 1)) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
apply Submodule.smul_induction_on
  (p := fun r => (monomial (Nat.succ n)) r ∈ Algebra.adjoin R (Submodule.map (monomial 1) I)) hr

Result:
case succ.smul
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
⊢ ∀ r ∈ I, ∀ n_1 ∈ I ^ n, (monomial n.succ) (r • n_1) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

case succ.add
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
⊢ ∀ (x y : R),
    (monomial n.succ) x ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I) →
      (monomial n.succ) y ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I) →
        (monomial n.succ) (x + y) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Proof state:
case succ.smul
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r✝ : R
hr✝ : r✝ ∈ I * I ^ n
r : R
hr : r ∈ I
s : R
hs : s ∈ I ^ n
⊢ (monomial n.succ) (r • s) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
rw [Nat.succ_eq_one_add, smul_eq_mul, ← monomial_mul_monomial]

Result:
case succ.smul
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r✝ : R
hr✝ : r✝ ∈ I * I ^ n
r : R
hr : r ∈ I
s : R
hs : s ∈ I ^ n
⊢ (monomial 1) r * (monomial n) s ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Proof state:
case succ
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I ^ (n + 1)
⊢ (monomial (n + 1)) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
rw [pow_succ'] at hr

Result:
case succ
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
⊢ (monomial (n + 1)) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Proof state:
case succ.add
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
x y : R
hx : (monomial n.succ) x ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
hy : (monomial n.succ) y ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
⊢ (monomial n.succ) (x + y) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
rw [monomial_add]

Result:
case succ.add
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
x y : R
hx : (monomial n.succ) x ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
hy : (monomial n.succ) y ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
⊢ (monomial n.succ) x + (monomial n.succ) y ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Proof state:
case succ.add
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
⊢ ∀ (x y : R),
    (monomial n.succ) x ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I) →
      (monomial n.succ) y ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I) →
        (monomial n.succ) (x + y) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
intro x y hx hy

Result:
case succ.add
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
x y : R
hx : (monomial n.succ) x ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
hy : (monomial n.succ) y ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
⊢ (monomial n.succ) (x + y) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
r : R
hr : r ∈ I ^ n
⊢ (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
induction' n with n hn generalizing r

Result:
case zero
R : Type u
inst✝ : CommRing R
I : Ideal R
r : R
hr : r ∈ I ^ 0
⊢ (monomial 0) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

case succ
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I ^ (n + 1)
⊢ (monomial (n + 1)) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)