-- Mathlib/RingTheory/Jacobson/Ring.lean
lemma mem_closure_X_union_C {R : Type*} [Ring R] (p : R[X]) :
    p ∈ Subring.closure (insert X {f | f.degree ≤ 0} : Set R[X])

Proof state:
case refine_1.a.a
R : Type u_1
inst✝ : Ring R
p : R[X]
r : R
⊢ C r ∈ {f | f.degree ≤ 0}

Tactic:
exact degree_C_le

Result:
no goals

Proof state:
case refine_2
R : Type u_1
inst✝ : Ring R
p p1 p2 : R[X]
h1 : p1 ∈ Subring.closure (insert X {f | f.degree ≤ 0})
h2 : p2 ∈ Subring.closure (insert X {f | f.degree ≤ 0})
⊢ p1 + p2 ∈ Subring.closure (insert X {f | f.degree ≤ 0})

Tactic:
exact Subring.add_mem _ h1 h2

Result:
no goals

Proof state:
case refine_3
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
r : R
hr : C r * X ^ n ∈ Subring.closure (insert X {f | f.degree ≤ 0})
⊢ C r * X ^ n * X ∈ Subring.closure (insert X {f | f.degree ≤ 0})

Tactic:
apply Subring.mul_mem _ hr

Result:
case refine_3
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
r : R
hr : C r * X ^ n ∈ Subring.closure (insert X {f | f.degree ≤ 0})
⊢ X ∈ Subring.closure (insert X {f | f.degree ≤ 0})

Proof state:
case refine_3
R : Type u_1
inst✝ : Ring R
p : R[X]
⊢ ∀ (n : ℕ) (a : R),
    C a * X ^ n ∈ Subring.closure (insert X {f | f.degree ≤ 0}) →
      C a * X ^ (n + 1) ∈ Subring.closure (insert X {f | f.degree ≤ 0})

Tactic:
intros n r hr

Result:
case refine_3
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
r : R
hr : C r * X ^ n ∈ Subring.closure (insert X {f | f.degree ≤ 0})
⊢ C r * X ^ (n + 1) ∈ Subring.closure (insert X {f | f.degree ≤ 0})

Proof state:
case refine_1.a
R : Type u_1
inst✝ : Ring R
p : R[X]
r : R
⊢ C r ∈ insert X {f | f.degree ≤ 0}

Tactic:
apply Set.mem_insert_of_mem

Result:
case refine_1.a.a
R : Type u_1
inst✝ : Ring R
p : R[X]
r : R
⊢ C r ∈ {f | f.degree ≤ 0}

Proof state:
R : Type u_1
inst✝ : Ring R
p : R[X]
⊢ p ∈ Subring.closure (insert X {f | f.degree ≤ 0})

Tactic:
refine Polynomial.induction_on p ?_ ?_ ?_

Result:
case refine_1
R : Type u_1
inst✝ : Ring R
p : R[X]
⊢ ∀ (a : R), C a ∈ Subring.closure (insert X {f | f.degree ≤ 0})

case refine_2
R : Type u_1
inst✝ : Ring R
p : R[X]
⊢ ∀ (p q : R[X]),
    p ∈ Subring.closure (insert X {f | f.degree ≤ 0}) →
      q ∈ Subring.closure (insert X {f | f.degree ≤ 0}) → p + q ∈ Subring.closure (insert X {f | f.degree ≤ 0})

case refine_3
R : Type u_1
inst✝ : Ring R
p : R[X]
⊢ ∀ (n : ℕ) (a : R),
    C a * X ^ n ∈ Subring.closure (insert X {f | f.degree ≤ 0}) →
      C a * X ^ (n + 1) ∈ Subring.closure (insert X {f | f.degree ≤ 0})

Proof state:
case refine_3
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
r : R
hr : C r * X ^ n ∈ Subring.closure (insert X {f | f.degree ≤ 0})
⊢ C r * X ^ (n + 1) ∈ Subring.closure (insert X {f | f.degree ≤ 0})

Tactic:
rw [pow_succ, ← mul_assoc]

Result:
case refine_3
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
r : R
hr : C r * X ^ n ∈ Subring.closure (insert X {f | f.degree ≤ 0})
⊢ C r * X ^ n * X ∈ Subring.closure (insert X {f | f.degree ≤ 0})

Proof state:
case refine_1
R : Type u_1
inst✝ : Ring R
p : R[X]
r : R
⊢ C r ∈ Subring.closure (insert X {f | f.degree ≤ 0})

Tactic:
apply Subring.subset_closure

Result:
case refine_1.a
R : Type u_1
inst✝ : Ring R
p : R[X]
r : R
⊢ C r ∈ insert X {f | f.degree ≤ 0}

Proof state:
case refine_3
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
r : R
hr : C r * X ^ n ∈ Subring.closure (insert X {f | f.degree ≤ 0})
⊢ X ∈ Subring.closure (insert X {f | f.degree ≤ 0})

Tactic:
apply Subring.subset_closure

Result:
case refine_3.a
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
r : R
hr : C r * X ^ n ∈ Subring.closure (insert X {f | f.degree ≤ 0})
⊢ X ∈ insert X {f | f.degree ≤ 0}

Proof state:
case refine_2
R : Type u_1
inst✝ : Ring R
p : R[X]
⊢ ∀ (p q : R[X]),
    p ∈ Subring.closure (insert X {f | f.degree ≤ 0}) →
      q ∈ Subring.closure (insert X {f | f.degree ≤ 0}) → p + q ∈ Subring.closure (insert X {f | f.degree ≤ 0})

Tactic:
intros p1 p2 h1 h2

Result:
case refine_2
R : Type u_1
inst✝ : Ring R
p p1 p2 : R[X]
h1 : p1 ∈ Subring.closure (insert X {f | f.degree ≤ 0})
h2 : p2 ∈ Subring.closure (insert X {f | f.degree ≤ 0})
⊢ p1 + p2 ∈ Subring.closure (insert X {f | f.degree ≤ 0})

Proof state:
case refine_1
R : Type u_1
inst✝ : Ring R
p : R[X]
⊢ ∀ (a : R), C a ∈ Subring.closure (insert X {f | f.degree ≤ 0})

Tactic:
intro r

Result:
case refine_1
R : Type u_1
inst✝ : Ring R
p : R[X]
r : R
⊢ C r ∈ Subring.closure (insert X {f | f.degree ≤ 0})

Proof state:
case refine_3.a
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
r : R
hr : C r * X ^ n ∈ Subring.closure (insert X {f | f.degree ≤ 0})
⊢ X ∈ insert X {f | f.degree ≤ 0}

Tactic:
apply Set.mem_insert

Result:
no goals