awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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ₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = RingHom.comp (Ideal.Quotient.mk P) C
p : Sₘ
obtain :
  ∀ (p' q : R[X] ⧸ P) (hq : q ∈ M')
    (hp :
      HMul.hMul (β := Sₘ) p
          ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ)
              (↑(p', Subtype.mk (p := fun (x : R[X] ⧸ P) ↦ x ∈ M') q hq).2 : R[X] ⧸ P) :
            Sₘ) =
        (algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) (p', Subtype.mk (p := fun (x : R[X] ⧸ P) ↦ x ∈ M') q hq).1),
    RingHom.IsIntegralElem.{u_3, u_4} (R := Rₘ)
      (IsLocalization.map (M :=
        Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))) Sₘ
        (quotientMap P C ⋯) ⋯)
      p
⊢ RingHom.IsIntegralElem.{u_3, u_4} (R := Rₘ)
    (IsLocalization.map (M :=
      Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))) Sₘ (quotientMap P C ⋯)
      ⋯)
    p

Tactic:
obtain ⟨⟨p', ⟨q, hq⟩⟩, hp⟩ := IsLocalization.surj M' p

Premises used: IsLocalization.surj
-- 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ₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = RingHom.comp (Ideal.Quotient.mk P) C
p : Sₘ
p' q : R[X] ⧸ P
hq : q ∈ M'
hp :
  HMul.hMul (β := Sₘ) p
      ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ)
          (↑(p', Subtype.mk (p := fun (x : R[X] ⧸ P) ↦ x ∈ M') q hq).2 : R[X] ⧸ P) :
        Sₘ) =
    (algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) (p', Subtype.mk (p := fun (x : R[X] ⧸ P) ↦ x ∈ M') q hq).1
this : φ'.IsIntegralElem ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) p')
obtain :
  ∀ (q' : HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))
    (hq' :
      q' ∈
        (↑(Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))) :
          Set (R ⧸ comap C P)))
    (hp :
      HMul.hMul (β := Sₘ) p
          ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ)
              ((↑(p',
                        Subtype.mk (p := fun (x : R[X] ⧸ P) ↦ x ∈ M')
                          ((quotientMap P C ⋯ : (a : R ⧸ comap C P) → R[X] ⧸ P) q') ⋯).2 :
                  R[X] ⧸ P) :
                R[X] ⧸ P) :
            Sₘ) =
        (algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ)
          ((p',
                Subtype.mk (p := fun (x : R[X] ⧸ P) ↦ x ∈ M') ((quotientMap P C ⋯ : (a : R ⧸ comap C P) → R[X] ⧸ P) q')
                  ⋯) :
              (R[X] ⧸ P) × ↥M').1),
    RingHom.IsIntegralElem.{u_3, u_4} (R := Rₘ)
      (IsLocalization.map (M :=
        Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))) Sₘ
        (quotientMap P C ⋯) ⋯)
      p
⊢ RingHom.IsIntegralElem.{u_3, u_4} (R := Rₘ)
    (IsLocalization.map (M :=
      Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))) Sₘ (quotientMap P C ⋯)
      ⋯)
    p

Tactic:
obtain ⟨q', hq', rfl⟩ := hq

Premises used: rfl
-- 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ₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = RingHom.comp (Ideal.Quotient.mk P) C
p : Sₘ
p' : R[X] ⧸ P
this : φ'.IsIntegralElem ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) p')
q' : HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P)
hq' :
  q' ∈
    (↑(Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))) :
      Set (R ⧸ comap C P))
hp :
  HMul.hMul (β := Sₘ) p
      ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ)
          ((↑(p',
                    Subtype.mk (p := fun (x : R[X] ⧸ P) ↦ x ∈ M')
                      ((quotientMap P C ⋯ : (a : R ⧸ comap C P) → R[X] ⧸ P) q') ⋯).2 :
              R[X] ⧸ P) :
            R[X] ⧸ P) :
        Sₘ) =
    (algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ)
      ((p', Subtype.mk (p := fun (x : R[X] ⧸ P) ↦ x ∈ M') ((quotientMap P C ⋯ : (a : R ⧸ comap C P) → R[X] ⧸ P) q') ⋯) :
          (R[X] ⧸ P) × ↥M').1
obtain :
  ∀ (q'' : Rₘ)
    (hq'' :
      HMul.hMul (β := Rₘ) q''
          ((algebraMap (R ⧸ P') Rₘ : (a : R ⧸ P') → Rₘ)
              (↑(Subtype.mk (p := fun (x : R ⧸ P') ↦ x ∈ M) q' hq') : R ⧸ P') :
            Rₘ) =
        1),
    RingHom.IsIntegralElem.{u_3, u_4} (R := Rₘ)
      (IsLocalization.map (M :=
        Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))) Sₘ
        (quotientMap P C ⋯) ⋯)
      p
⊢ RingHom.IsIntegralElem.{u_3, u_4} (R := Rₘ)
    (IsLocalization.map (M :=
      Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))) Sₘ (quotientMap P C ⋯)
      ⋯)
    p

Tactic:
obtain ⟨q'', hq''⟩ := isUnit_iff_exists_inv'.1 (IsLocalization.map_units Rₘ (⟨q', hq'⟩ : M))

Premises used: Subtype.mk, Iff.mp, IsLocalization.map_units, isUnit_iff_exists_inv'
-- 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ₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = RingHom.comp (Ideal.Quotient.mk P) C
p : Sₘ
p' : R[X] ⧸ P
this : φ'.IsIntegralElem ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) p')
q' : HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P)
hq' :
  q' ∈
    (↑(Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))) :
      Set (R ⧸ comap C P))
hp :
  HMul.hMul (β := Sₘ) p
      ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ)
          ((↑(p',
                    Subtype.mk (p := fun (x : R[X] ⧸ P) ↦ x ∈ M')
                      ((quotientMap P C ⋯ : (a : R ⧸ comap C P) → R[X] ⧸ P) q') ⋯).2 :
              R[X] ⧸ P) :
            R[X] ⧸ P) :
        Sₘ) =
    (algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ)
      ((p', Subtype.mk (p := fun (x : R[X] ⧸ P) ↦ x ∈ M') ((quotientMap P C ⋯ : (a : R ⧸ comap C P) → R[X] ⧸ P) q') ⋯) :
          (R[X] ⧸ P) × ↥M').1
q'' : Rₘ
hq'' :
  HMul.hMul (β := Rₘ) q''
      ((algebraMap (R ⧸ P') Rₘ : (a : R ⧸ P') → Rₘ) (↑(Subtype.mk (p := fun (x : R ⧸ P') ↦ x ∈ M) q' hq') : R ⧸ P') :
        Rₘ) =
    1
refine :
  HMul.hMul (α := Sₘ) (β := Sₘ) ((φ' : (a : Rₘ) → Sₘ) q'' : Sₘ)
      ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) ((φ : (a : R ⧸ P') → R[X] ⧸ P) q' : R[X] ⧸ P) : Sₘ) =
    1
⊢ RingHom.IsIntegralElem.{u_3, u_4} (R := Rₘ)
    (IsLocalization.map (M :=
      Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))) Sₘ (quotientMap P C ⋯)
      ⋯)
    p

Tactic:
refine (hp.symm ▸ this).of_mul_unit φ' p (algebraMap (R[X] ⧸ P) Sₘ (φ q')) q'' ?_
-- 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ₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = RingHom.comp (Ideal.Quotient.mk P) C
p : Sₘ
p' : R[X] ⧸ P
this : φ'.IsIntegralElem ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) p')
q' : HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P)
hq' :
  q' ∈
    (↑(Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))) :
      Set (R ⧸ comap C P))
hp :
  HMul.hMul (β := Sₘ) p
      ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ)
          ((↑(p',
                    Subtype.mk (p := fun (x : R[X] ⧸ P) ↦ x ∈ M')
                      ((quotientMap P C ⋯ : (a : R ⧸ comap C P) → R[X] ⧸ P) q') ⋯).2 :
              R[X] ⧸ P) :
            R[X] ⧸ P) :
        Sₘ) =
    (algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ)
      ((p', Subtype.mk (p := fun (x : R[X] ⧸ P) ↦ x ∈ M') ((quotientMap P C ⋯ : (a : R ⧸ comap C P) → R[X] ⧸ P) q') ⋯) :
          (R[X] ⧸ P) × ↥M').1
q'' : Rₘ
hq'' :
  HMul.hMul (β := Rₘ) q''
      ((algebraMap (R ⧸ P') Rₘ : (a : R ⧸ P') → Rₘ) (↑(Subtype.mk (p := fun (x : R ⧸ P') ↦ x ∈ M) q' hq') : R ⧸ P') :
        Rₘ) =
    1
rw :
  HMul.hMul (α := Sₘ) (β := Sₘ) ((φ' : (a : Rₘ) → Sₘ) q'' : Sₘ)
      ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) ((φ : (a : R ⧸ P') → R[X] ⧸ P) q' : R[X] ⧸ P) : Sₘ) =
    HMul.hMul (α := Sₘ) (β := Sₘ) ((φ' : (a : Rₘ) → Sₘ) q'' : Sₘ)
      ((φ'.comp (algebraMap (R ⧸ P') Rₘ) : (a : R ⧸ P') → Sₘ)
          (↑(Subtype.mk (p := fun (x : R ⧸ P') ↦ x ∈ M) q' hq') : R ⧸ P') :
        Sₘ)
⊢ HMul.hMul (α := Sₘ) (β := Sₘ) ((φ' : (a : Rₘ) → Sₘ) q'' : Sₘ)
      ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) ((φ : (a : R ⧸ P') → R[X] ⧸ P) q' : R[X] ⧸ P) : Sₘ) =
    1

Tactic:
rw [← φ'.map_one, ← congr_arg φ' hq'', φ'.map_mul, ← φ'.comp_apply]

Premises used: RingHom.map_one, congr_arg, RingHom.comp_apply, RingHom.map_mul, DFunLike.coe
-- 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ₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = RingHom.comp (Ideal.Quotient.mk P) C
p : Sₘ
p' : R[X] ⧸ P
this : φ'.IsIntegralElem ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) p')
q' : HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P)
hq' :
  q' ∈
    (↑(Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))) :
      Set (R ⧸ comap C P))
hp :
  HMul.hMul (β := Sₘ) p
      ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ)
          ((↑(p',
                    Subtype.mk (p := fun (x : R[X] ⧸ P) ↦ x ∈ M')
                      ((quotientMap P C ⋯ : (a : R ⧸ comap C P) → R[X] ⧸ P) q') ⋯).2 :
              R[X] ⧸ P) :
            R[X] ⧸ P) :
        Sₘ) =
    (algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ)
      ((p', Subtype.mk (p := fun (x : R[X] ⧸ P) ↦ x ∈ M') ((quotientMap P C ⋯ : (a : R ⧸ comap C P) → R[X] ⧸ P) q') ⋯) :
          (R[X] ⧸ P) × ↥M').1
q'' : Rₘ
hq'' :
  HMul.hMul (β := Rₘ) q''
      ((algebraMap (R ⧸ P') Rₘ : (a : R ⧸ P') → Rₘ) (↑(Subtype.mk (p := fun (x : R ⧸ P') ↦ x ∈ M) q' hq') : R ⧸ P') :
        Rₘ) =
    1
⊢ HMul.hMul (α := Sₘ) (β := Sₘ) ((φ' : (a : Rₘ) → Sₘ) q'' : Sₘ)
      ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) ((φ : (a : R ⧸ P') → R[X] ⧸ P) q' : R[X] ⧸ P) : Sₘ) =
    HMul.hMul (α := Sₘ) (β := Sₘ) ((φ' : (a : Rₘ) → Sₘ) q'' : Sₘ)
      ((φ'.comp (algebraMap (R ⧸ P') Rₘ) : (a : R ⧸ P') → Sₘ)
          (↑(Subtype.mk (p := fun (x : R ⧸ P') ↦ x ∈ M) q' hq') : R ⧸ P') :
        Sₘ)

Tactic:
simp only [φ', IsLocalization.map_comp _, RingHom.comp_apply]

Premises used: IsLocalization.map_comp, RingHom.comp_apply
-- 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ₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = RingHom.comp (Ideal.Quotient.mk P) C
p : Sₘ
p' q : R[X] ⧸ P
hq : q ∈ M'
hp :
  HMul.hMul (β := Sₘ) p
      ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ)
          (↑(p', Subtype.mk (p := fun (x : R[X] ⧸ P) ↦ x ∈ M') q hq).2 : R[X] ⧸ P) :
        Sₘ) =
    (algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) (p', Subtype.mk (p := fun (x : R[X] ⧸ P) ↦ x ∈ M') q hq).1
suffices : φ'.IsIntegralElem ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) p')
⊢ RingHom.IsIntegralElem.{u_3, u_4} (R := Rₘ)
    (IsLocalization.map (M :=
      Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))) Sₘ (quotientMap P C ⋯)
      ⋯)
    p

Tactic:
suffices φ'.IsIntegralElem (algebraMap (R[X] ⧸ P) Sₘ p') by
    obtain ⟨q', hq', rfl⟩ := hq
    obtain ⟨q'', hq''⟩ := isUnit_iff_exists_inv'.1 (IsLocalization.map_units Rₘ (⟨q', hq'⟩ : M))
    refine (hp.symm ▸ this).of_mul_unit φ' p (algebraMap (R[X] ⧸ P) Sₘ (φ q')) q'' ?_
    rw [← φ'.map_one, ← congr_arg φ' hq'', φ'.map_mul, ← φ'.comp_apply]
    simp only [φ', IsLocalization.map_comp _, RingHom.comp_apply]
-- 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ₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = RingHom.comp (Ideal.Quotient.mk P) C
p : Sₘ
p' q : R[X] ⧸ P
hq : q ∈ M'
hp :
  HMul.hMul (β := Sₘ) p ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) q : Sₘ) =
    (algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) p'
⊢ φ'.IsIntegralElem ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) p')

Tactic:
@IsIntegral.of_mem_closure'' Rₘ _ Sₘ _ φ'
    ((algebraMap (R[X] ⧸ P) Sₘ).comp (Ideal.Quotient.mk P) '' insert X { p | p.degree ≤ 0 }) ?_
    ((algebraMap (R[X] ⧸ P) Sₘ) p') ?_

Premises used: Algebra.algebraMap, Ideal.Quotient.mk, setOf, Insert.insert, Polynomial.degree, LE.le, Polynomial, HasQuotient.Quotient, RingHom.comp, IsIntegral.of_mem_closure'', Set.image, OfNat.ofNat, Polynomial.X, DFunLike.coe
-- 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ₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = RingHom.comp (Ideal.Quotient.mk P) C
p : Sₘ
p' q : R[X] ⧸ P
hq : q ∈ M'
hp :
  HMul.hMul (β := Sₘ) p ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) q : Sₘ) =
    (algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) p'
refine_1 :
  ∀ (x : Sₘ),
    Membership.mem (γ := Set Sₘ)
        (Set.image (α := R[X]) (⇑(RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P)) : (a : R[X]) → Sₘ)
          (insert X {p : R[X] | p.degree ≤ 0}))
        x →
      φ'.IsIntegralElem x
refine_2 :
  Membership.mem.{u_4, u_4} (α := Sₘ) (γ := Subring Sₘ)
    (Subring.closure
      (Set.image (α := R[X]) (⇑(RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P)) : (a : R[X]) → Sₘ)
        (insert X {p : R[X] | p.degree ≤ 0})))
    ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) p' : Sₘ)
⊢ φ'.IsIntegralElem ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) p')

Tactic:
refine @IsIntegral.of_mem_closure'' Rₘ _ Sₘ _ φ'
    ((algebraMap (R[X] ⧸ P) Sₘ).comp (Ideal.Quotient.mk P) '' insert X { p | p.degree ≤ 0 }) ?_
    ((algebraMap (R[X] ⧸ P) Sₘ) p') ?_

Premises used: Algebra.algebraMap, Ideal.Quotient.mk, setOf, Insert.insert, Polynomial.degree, LE.le, Polynomial, HasQuotient.Quotient, RingHom.comp, IsIntegral.of_mem_closure'', Set.image, OfNat.ofNat, Polynomial.X, DFunLike.coe