awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}) x
hxy_1 : Membership.mem (γ := Ideal R) (under R P' : Ideal R) (x * y)
hxy : Membership.mem (γ := Ideal R) (under R P') x
⊢ Membership.mem (γ := Submodule R R) (Ideal.comap (F := R →+* S) (algebraMap R S) P') x

Tactic:
hxy

Premises used: Set.Mem
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}) x
hxy_1 : Membership.mem (γ := Ideal R) (under R P' : Ideal R) (x * y)
hxy : Membership.mem (γ := Ideal R) (under R P') x
⊢ Membership.mem (γ := Submodule R R) (Ideal.comap (F := R →+* S) (algebraMap R S) P') x

Tactic:
exact hxy
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}) x
hxy_1 : Membership.mem (γ := Ideal R) (under R P' : Ideal R) (x * y)
hxy : Membership.mem (γ := Ideal R) (under R P') y
⊢ Membership.mem (γ := Submodule R R) (Ideal.comap (F := R →+* S) (algebraMap R S) P') x

Tactic:
(hPM.le_bot ⟨Submonoid.mem_powers _, hxy⟩).elim

Premises used: Disjoint.le_bot, False.elim, And.intro, Submonoid.mem_powers
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}) x
hxy_1 : Membership.mem (γ := Ideal R) (under R P' : Ideal R) (x * y)
hxy : Membership.mem (γ := Ideal R) (under R P') y
⊢ Membership.mem (γ := Submodule R R) (Ideal.comap (F := R →+* S) (algebraMap R S) P') x

Tactic:
exact (hPM.le_bot ⟨Submonoid.mem_powers _, hxy⟩).elim

Premises used: Disjoint.le_bot, False.elim, And.intro, Submonoid.mem_powers
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
⊢ LE.le (α := Ideal R) (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I})
    (Ideal.comap (F := R →+* S) (algebraMap R S) P')

Tactic:
have : sInf { I : Ideal R | comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I } ≤
      comap (algebraMap R S) P' := by
    intro x hx
    have hxy : x * y ∈ (comap (algebraMap R S) P').jacobson := by
      rw [Ideal.jacobson, Ideal.mem_sInf]
      intro J hJ
      by_cases h : y ∈ J
      · exact J.mul_mem_left x h
      · exact J.mul_mem_right y ((mem_sInf.1 hx) ⟨hJ.left, ⟨hJ.right, h⟩⟩)
    rw [hP] at hxy
    rcases hP'.mem_or_mem hxy with hxy | hxy
    · exact hxy
    · exact (hPM.le_bot ⟨Submonoid.mem_powers _, hxy⟩).elim
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
this :
  LE.le (α := Ideal R) (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I})
    (Ideal.comap (F := R →+* S) (algebraMap R S) P')
⊢ LE.le (α := Ideal R) (under R P'.jacobson) (under R P')

Tactic:
le_trans ?_ this

Premises used: le_trans
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
this :
  LE.le (α := Ideal R) (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I})
    (Ideal.comap (F := R →+* S) (algebraMap R S) P')
refine :
  LE.le (α := Ideal R) (under R P'.jacobson)
    (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I})
⊢ LE.le (α := Ideal R) (under R P'.jacobson) (under R P')

Tactic:
refine le_trans ?_ this

Premises used: le_trans
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
this :
  LE.le (α := Ideal R) (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I})
    (Ideal.comap (F := R →+* S) (algebraMap R S) P')
rw :
  LE.le.{u_1} (α := Ideal R)
    (⨅ (I : Ideal R),
      ⨅ (_ :
        Membership.mem (γ := Set (Ideal R))
          (Set.image (α := Ideal S) (Ideal.comap (F := R →+* S) (algebraMap R S)) {J : Ideal S | P' ≤ J ∧ J.IsMaximal})
          I),
        I)
    (⨅ (a : Ideal R),
      ⨅ (_ :
        Membership.mem (γ := Set (Ideal R))
          {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} a),
        a)
⊢ LE.le (α := Ideal R) (under R P'.jacobson)
    (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I})

Tactic:
rw [Ideal.jacobson, under_def, comap_sInf', sInf_eq_iInf]

Premises used: Ideal.comap_sInf', Ideal.jacobson, sInf_eq_iInf, Ideal.under_def
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
this :
  LE.le (α := Ideal R) (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I})
    (Ideal.comap (F := R →+* S) (algebraMap R S) P')
⊢ LE.le.{u_1} (α := Ideal R)
    (⨅ (I : Ideal R),
      ⨅ (_ :
        Membership.mem (γ := Set (Ideal R))
          (Set.image (α := Ideal S) (Ideal.comap (F := R →+* S) (algebraMap R S)) {J : Ideal S | P' ≤ J ∧ J.IsMaximal})
          I),
        I)
    (⨅ (a : Ideal R),
      ⨅ (_ :
        Membership.mem (γ := Set (Ideal R))
          {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} a),
        a)

Tactic:
iInf_le_iInf_of_subset fun I ⟨hI, hIm, hyI⟩ => ⟨map (algebraMap R S) I, ⟨?_, ?_⟩⟩

Premises used: Algebra.algebraMap, Set.Mem, _private.0.isJacobsonRing_localization.match_1, setOf, Membership.mem, Ideal.map, LE.le, And, And.intro, Ideal.comap, Exists.intro, Ideal.IsMaximal, Set.image, iInf_le_iInf_of_subset
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
this :
  LE.le (α := Ideal R) (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I})
    (Ideal.comap (F := R →+* S) (algebraMap R S) P')
refine_1 :
  ∀ (I : Ideal R),
    Membership.mem (γ := Set (Ideal R))
        {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} I →
      ∀ (hI : Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I) (hIm : I.IsMaximal) (hyI : y ∉ I),
        Membership.mem (γ := Set (Ideal S)) {J : Ideal S | P' ≤ J ∧ J.IsMaximal}
          (Ideal.map (F := R →+* S) (algebraMap R S) I)
refine_2 :
  ∀ (I : Ideal R),
    Membership.mem (γ := Set (Ideal R))
        {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} I →
      ∀ (hI : Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I) (hIm : I.IsMaximal) (hyI : y ∉ I),
        Ideal.comap (F := R →+* S) (algebraMap R S) (Ideal.map (F := R →+* S) (algebraMap R S) I) = I
⊢ LE.le.{u_1} (α := Ideal R)
    (⨅ (I : Ideal R),
      ⨅ (_ :
        Membership.mem (γ := Set (Ideal R))
          (Set.image (α := Ideal S) (Ideal.comap (F := R →+* S) (algebraMap R S)) {J : Ideal S | P' ≤ J ∧ J.IsMaximal})
          I),
        I)
    (⨅ (a : Ideal R),
      ⨅ (_ :
        Membership.mem (γ := Set (Ideal R))
          {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} a),
        a)

Tactic:
refine iInf_le_iInf_of_subset fun I ⟨hI, hIm, hyI⟩ => ⟨map (algebraMap R S) I, ⟨?_, ?_⟩⟩
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
this :
  LE.le (α := Ideal R) (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I})
    (Ideal.comap (F := R →+* S) (algebraMap R S) P')
I : Ideal R
h :
  Membership.mem (γ := Set (Ideal R))
    {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} I
hI : Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I
hIm : I.IsMaximal
hyI : y ∉ I
⊢ Membership.mem (γ := Set (Ideal S)) {J : Ideal S | P' ≤ J ∧ J.IsMaximal} (Ideal.map (F := R →+* S) (algebraMap R S) I)

Tactic:
⟨le_trans (IsLocalization.map_under (powers y) S P').symm.le (map_mono hI),
      isMaximal_of_isMaximal_disjoint y I hIm hyI⟩

Premises used: Set.Mem, setOf, Eq.le, IsLocalization.map_under, And.intro, Submonoid.powers, IsLocalization.isMaximal_of_isMaximal_disjoint, Ideal.map_mono, Eq.symm, le_trans
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
this :
  LE.le (α := Ideal R) (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I})
    (Ideal.comap (F := R →+* S) (algebraMap R S) P')
I : Ideal R
h :
  Membership.mem (γ := Set (Ideal R))
    {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} I
hI : Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I
hIm : I.IsMaximal
hyI : y ∉ I
⊢ Membership.mem (γ := Set (Ideal S)) {J : Ideal S | P' ≤ J ∧ J.IsMaximal} (Ideal.map (F := R →+* S) (algebraMap R S) I)

Tactic:
exact ⟨le_trans (IsLocalization.map_under (powers y) S P').symm.le (map_mono hI),
      isMaximal_of_isMaximal_disjoint y I hIm hyI⟩
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
this :
  LE.le (α := Ideal R) (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I})
    (Ideal.comap (F := R →+* S) (algebraMap R S) P')
I : Ideal R
h :
  Membership.mem (γ := Set (Ideal R))
    {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} I
hI : Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I
hIm : I.IsMaximal
hyI : y ∉ I
⊢ Ideal.comap (F := R →+* S) (algebraMap R S) (Ideal.map (F := R →+* S) (algebraMap R S) I) = I

Tactic:
IsLocalization.under_map_of_isPrime_disjoint _ S hIm.isPrime <|
      (disjoint_powers_iff_notMem_of_isPrime y).2 hyI

Premises used: Iff.mpr, Ideal.IsMaximal.isPrime, Ideal.disjoint_powers_iff_notMem_of_isPrime, IsLocalization.under_map_of_isPrime_disjoint
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
this :
  LE.le (α := Ideal R) (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I})
    (Ideal.comap (F := R →+* S) (algebraMap R S) P')
I : Ideal R
h :
  Membership.mem (γ := Set (Ideal R))
    {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} I
hI : Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I
hIm : I.IsMaximal
hyI : y ∉ I
⊢ Ideal.comap (F := R →+* S) (algebraMap R S) (Ideal.map (F := R →+* S) (algebraMap R S) I) = I

Tactic:
exact IsLocalization.under_map_of_isPrime_disjoint _ S hIm.isPrime <|
      (disjoint_powers_iff_notMem_of_isPrime y).2 hyI

Premises used: Iff.mpr, Ideal.IsMaximal.isPrime, Ideal.disjoint_powers_iff_notMem_of_isPrime, IsLocalization.under_map_of_isPrime_disjoint
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
⊢ Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0})) p

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

Premises used: Polynomial.induction_on
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
refine_1 :
  ∀ (a : R),
    Membership.mem (α := R[X]) (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0}))
      ((C : (a : R) → R[X]) a : R[X])
refine_2 :
  ∀ (p q : R[X]),
    Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0})) p →
      Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0})) q →
        Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0})) (p + q)
refine_3 :
  ∀ (n : ℕ) (a : R),
    Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0}))
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0}))
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
⊢ Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0})) p

Tactic:
refine Polynomial.induction_on p ?_ ?_ ?_
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
r : R
refine_1 :
  Membership.mem (α := R[X]) (γ := Set R[X]) (insert X {f : R[X] | f.degree ≤ 0}) ((C : (a : R) → R[X]) r : R[X])
⊢ Membership.mem (α := R[X]) (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0}))
    ((C : (a : R) → R[X]) r : R[X])

Tactic:
apply Subring.subset_closure

Premises used: Subring.subset_closure
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
r : R
refine_1 : Membership.mem (α := R[X]) (γ := Set R[X]) {f : R[X] | f.degree ≤ 0} ((C : (a : R) → R[X]) r : R[X])
⊢ Membership.mem (α := R[X]) (γ := Set R[X]) (insert X {f : R[X] | f.degree ≤ 0}) ((C : (a : R) → R[X]) r : R[X])

Tactic:
apply Set.mem_insert_of_mem

Premises used: Set.mem_insert_of_mem
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
r : R
⊢ Membership.mem (α := R[X]) (γ := Set R[X]) {f : R[X] | f.degree ≤ 0} ((C : (a : R) → R[X]) r : R[X])

Tactic:
degree_C_le

Premises used: Set.Mem, setOf, Polynomial.degree_C_le
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
r : R
⊢ Membership.mem (α := R[X]) (γ := Set R[X]) {f : R[X] | f.degree ≤ 0} ((C : (a : R) → R[X]) r : R[X])

Tactic:
exact degree_C_le

Premises used: Polynomial.degree_C_le
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : Ring R
p p1 p2 : R[X]
h1 : Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0})) p1
h2 : Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0})) p2
⊢ Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0})) (p1 + p2)

Tactic:
Subring.add_mem _ h1 h2

Premises used: Subring.add_mem, Set.Mem
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : Ring R
p p1 p2 : R[X]
h1 : Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0})) p1
h2 : Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0})) p2
⊢ Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0})) (p1 + p2)

Tactic:
exact Subring.add_mem _ h1 h2

Premises used: Subring.add_mem
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
n : ℕ
r : R
hr :
  Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0}))
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
refine_3 :
  Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0}))
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n) * X)
⊢ Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0}))
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))

Tactic:
rw [pow_succ, ← mul_assoc]

Premises used: pow_succ, mul_assoc
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
n : ℕ
r : R
hr :
  Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0}))
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
refine_3 : Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0})) X
⊢ Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0}))
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n) * X)

Tactic:
apply Subring.mul_mem _ hr

Premises used: Subring.mul_mem
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
n : ℕ
r : R
hr :
  Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0}))
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
refine_3 : Membership.mem (γ := Set R[X]) (insert X {f : R[X] | f.degree ≤ 0}) X
⊢ Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0})) X

Tactic:
apply Subring.subset_closure

Premises used: Subring.subset_closure
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
n : ℕ
r : R
hr :
  Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0}))
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ Membership.mem (γ := Set R[X]) (insert X {f : R[X] | f.degree ≤ 0}) X

Tactic:
apply Set.mem_insert

Premises used: Set.mem_insert
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst_1 : CommRing Rₘ
inst_2 : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst_3 : Algebra.{u_1, u_3} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P)) Rₘ
inst_4 :
  IsLocalization.Away (R := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))
    (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX)) Rₘ
inst_5 : Algebra.{u_1, u_4} (R[X] ⧸ P) Sₘ
inst_6 :
  IsLocalization
    (Submonoid.map (F := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P) →+* R[X] ⧸ P)
      (quotientMap P C ⋯) (Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))))
    Sₘ
P' : Ideal R := comap (F := R →+* R[X]) C P
M : Submonoid (R ⧸ P') := Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (F := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P) →+* R[X] ⧸ P)
    (quotientMap P C ⋯) (Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX)))
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
⊢ φ.comp (Ideal.Quotient.mk P') = RingHom.comp (Ideal.Quotient.mk P) C

Tactic:
have hφ' : φ.comp (Ideal.Quotient.mk P') = (Ideal.Quotient.mk P).comp C := rfl