awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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
have 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])
Tactic: refine Polynomial.induction_on p ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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])
⊢ Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0})) p
have 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)
Tactic: refine Polynomial.induction_on p ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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)
⊢ Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0})) p
have 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)))
Tactic: refine Polynomial.induction_on p ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
r : R
⊢ 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])
have 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])
Tactic: apply Subring.subset_closure
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
r : R
⊢ Membership.mem (α := R[X]) (γ := Set R[X]) (insert X {f : R[X] | f.degree ≤ 0}) ((C : (a : R) → R[X]) r : R[X])
have refine_1 : Membership.mem (α := R[X]) (γ := Set R[X]) {f : R[X] | f.degree ≤ 0} ((C : (a : R) → R[X]) r : R[X])
Tactic: apply Set.mem_insert_of_mem
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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 (γ := 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)))
have 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)
Tactic: rw [pow_succ, ← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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 (γ := 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)
have refine_3 : Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0})) X
Tactic: apply Subring.mul_mem _ hr
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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 (γ := Subring R[X]) (Subring.closure (insert X {f : R[X] | f.degree ≤ 0})) X
have refine_3 : Membership.mem (γ := Set R[X]) (insert X {f : R[X] | f.degree ≤ 0}) X
Tactic: apply Subring.subset_closure
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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ₘ φ ⋯
⊢ RingHom.IsIntegral.{u_3, u_4} (R := Rₘ) (A := Sₘ)
    (IsLocalization.map (M :=
      Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))) Sₘ (quotientMap P C ⋯)
      ⋯)
have hφ' : φ.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
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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ₘ
⊢ 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
have 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 sorry)
      sorry)
    p
Tactic: obtain ⟨⟨p', ⟨q, hq⟩⟩, hp⟩ := IsLocalization.surj M' p
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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')
⊢ 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
have 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 sorry : (a : R ⧸ comap C P) → R[X] ⧸ P) q') sorry).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 sorry : (a : R ⧸ comap C P) → R[X] ⧸ P) q')
                sorry) :
            (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 sorry)
      sorry)
    p
Tactic: obtain ⟨q', hq', rfl⟩ := hq
Cleared hypotheses: q, hq, hp
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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
⊢ 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
have 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 sorry)
      sorry)
    p
Tactic: obtain ⟨q'', hq''⟩ := isUnit_iff_exists_inv'.1 (IsLocalization.map_units Rₘ (⟨q', hq'⟩ : M))
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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
⊢ 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
have 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
Tactic: refine (hp.symm ▸ this).of_mul_unit φ' p (algebraMap (R[X] ⧸ P) Sₘ (φ q')) q'' ?_
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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ₘ) =
    1
have 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ₘ)
Tactic: rw [← φ'.map_one, ← congr_arg φ' hq'', φ'.map_mul, ← φ'.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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
⊢ 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
have suffices : φ'.IsIntegralElem ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) 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]