awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst_2 : P.IsPrime
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
Pb : ¬P = ⊥
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
hR' : IsJacobsonRing.{u_5} (R ⧸ P')
p : R[X]
pP : p ∈ P
p0 :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) p) 0
x : R ⧸ P' := (map (Ideal.Quotient.mk P') p).leadingCoeff
⊢ x ≠ 0
have rwa : ¬x = 0
Tactic: rwa [Ne, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst_2 : P.IsPrime
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
Pb : ¬P = ⊥
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
hR' : IsJacobsonRing.{u_5} (R ⧸ P')
p : R[X]
pP : p ∈ P
p0 :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) p) 0
x : R ⧸ P' := (map (Ideal.Quotient.mk P') p).leadingCoeff
rwa : ¬x = 0
⊢ x ≠ 0
have rwa₁ : ¬map (Ideal.Quotient.mk P') p = 0
Tactic: rwa [Ne, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst_2 : P.IsPrime
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
Pb : ¬P = ⊥
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
hR' : IsJacobsonRing.{u_5} (R ⧸ P')
p : R[X]
pP : p ∈ P
p0 :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) p) 0
x : R ⧸ P' := (map (Ideal.Quotient.mk P') p).leadingCoeff
⊢ Eq.{u_5 + 1} (α := Ideal (R[X] ⧸ P)) (jacobson ⊥) ⊥
have hx : x ≠ 0
Tactic: have hx : x ≠ 0 := by rwa [Ne, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst_2 : P.IsPrime
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
Pb : ¬P = ⊥
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
hR' : IsJacobsonRing.{u_5} (R ⧸ P')
p : R[X]
pP : p ∈ P
p0 :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) p) 0
x : R ⧸ P' := (map (Ideal.Quotient.mk P') p).leadingCoeff
hx : x ≠ 0
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
hφ : Function.Injective (α := R ⧸ P') (β := R[X] ⧸ P) (⇑φ : (a : R ⧸ P') → R[X] ⧸ P) := ⋯
Rₘ : Type u_5 := Localization.Away x
Sₘ : Type u_5 := Localization (Submonoid.map φ (Submonoid.powers x))
⊢ Eq.{u_5 + 1} (α := Ideal (R[X] ⧸ P)) (jacobson ⊥) ⊥
have neg : RingHom.IsIntegral.{u_5, u_5} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ sorry)
Tactic: refine jacobson_bot_of_integral_localization (S := R[X] ⧸ P) (R := R ⧸ P') Rₘ Sₘ _ hφ _ hx ?_
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
⊢ IsJacobsonRing.{u_1} R[X]
have rw : ∀ (P : Ideal R[X]), P.IsPrime → P.jacobson = P
Tactic: rw [isJacobsonRing_iff_prime_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
⊢ I.jacobson = I
have hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
Tactic: have hi : Function.Surjective ↑i := ((Ideal.Quotient.mk I).comp C).rangeRestrict_surjective
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
f : R[X]
hf : Membership.mem (γ := Submodule R[X] R[X]) (RingHom.ker (mapRingHom i)) f
⊢ f ∈ I
have apply : ∀ (n : ℕ), Membership.mem (γ := Ideal R) (comap (F := R →+* R[X]) C I) (f.coeff n)
Tactic: apply polynomial_mem_ideal_of_coeff_mem_ideal I f
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
f : R[X]
hf : Membership.mem (γ := Submodule R[X] R[X]) (RingHom.ker (mapRingHom i)) f
n : ℕ
⊢ Membership.mem (γ := Ideal R) (comap (F := R →+* R[X]) C I) (f.coeff n)
have hf₁ : Eq.{u_1 + 1} (α := ↥(RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)))
  ((fun (g : (↥(RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)))[X]) ↦ g.coeff n)
    ((mapRingHom i : (a : R[X]) → (↥R')[X]) f))
  ((fun (g : (↥(RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)))[X]) ↦ g.coeff n) 0)
Tactic: replace hf := congrArg (fun g : Polynomial ((Ideal.Quotient.mk I).comp C).range => g.coeff n) hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
f : R[X]
n : ℕ
hf :
  Eq.{u_1 + 1} (α := ↥(RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)))
    ((fun (g : (↥(RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)))[X]) ↦ g.coeff n)
      ((mapRingHom i : (a : R[X]) → (↥R')[X]) f))
    ((fun (g : (↥(RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)))[X]) ↦ g.coeff n) 0)
⊢ Membership.mem (γ := Ideal R) (comap (F := R →+* R[X]) C I) (f.coeff n)
have hf₁ : Eq (α := ↥(RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)))
  (coeff (map (RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)) f) n) 0
Tactic: change (Polynomial.map ((Ideal.Quotient.mk I).comp C).rangeRestrict f).coeff n = 0 at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
f : R[X]
n : ℕ
hf :
  Eq (α := ↥(RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)))
    (coeff (map (RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)) f) n) 0
⊢ Membership.mem (γ := Ideal R) (comap (F := R →+* R[X]) C I) (f.coeff n)
have hf₁ : Eq.{u_1 + 1} (α := R[X] ⧸ I)
  (↑((RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C) : (a : R) → ↥((Ideal.Quotient.mk I).comp C).range)
        (f.coeff n)) :
    R[X] ⧸ I)
  (↑0 : R[X] ⧸ I)
Tactic: rw [coeff_map, Subtype.ext_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
f : R[X]
n : ℕ
hf :
  Eq.{u_1 + 1} (α := R[X] ⧸ I)
    (↑((RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C) : (a : R) → ↥((Ideal.Quotient.mk I).comp C).range)
          (f.coeff n)) :
      R[X] ⧸ I)
    (↑0 : R[X] ⧸ I)
⊢ Membership.mem (γ := Ideal R) (comap (F := R →+* R[X]) C I) (f.coeff n)
have rwa : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) (f.coeff n) : R[X])
Tactic: rwa [mem_comap, ← Quotient.eq_zero_iff_mem, ← RingHom.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
f : R[X]
n : ℕ
hf :
  Eq.{u_1 + 1} (α := R[X] ⧸ I)
    (↑((RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C) : (a : R) → ↥((Ideal.Quotient.mk I).comp C).range)
          (f.coeff n)) :
      R[X] ⧸ I)
    (↑0 : R[X] ⧸ I)
rwa : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) (f.coeff n) : R[X])
⊢ Membership.mem (γ := Ideal R) (comap (F := R →+* R[X]) C I) (f.coeff n)
have rwa₁ : Eq (α := R[X] ⧸ I) ((Ideal.Quotient.mk I : (a : R[X]) → R[X] ⧸ I) ((C : (a : R) → R[X]) (f.coeff n)) : R[X] ⧸ I)
  (0 : R[X] ⧸ I)
Tactic: rwa [mem_comap, ← Quotient.eq_zero_iff_mem, ← RingHom.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
f : R[X]
n : ℕ
hf :
  Eq.{u_1 + 1} (α := R[X] ⧸ I)
    (↑((RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C) : (a : R) → ↥((Ideal.Quotient.mk I).comp C).range)
          (f.coeff n)) :
      R[X] ⧸ I)
    (↑0 : R[X] ⧸ I)
rwa : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) (f.coeff n) : R[X])
rwa₁ :
  Eq (α := R[X] ⧸ I) ((Ideal.Quotient.mk I : (a : R[X]) → R[X] ⧸ I) ((C : (a : R) → R[X]) (f.coeff n)) : R[X] ⧸ I)
    (0 : R[X] ⧸ I)
⊢ Membership.mem (γ := Ideal R) (comap (F := R →+* R[X]) C I) (f.coeff n)
have rwa₂ : Eq (α := R[X] ⧸ I) ((RingHom.comp (Ideal.Quotient.mk I) C : (a : R) → R[X] ⧸ I) (f.coeff n) : R[X] ⧸ I) (0 : R[X] ⧸ I)
Tactic: rwa [mem_comap, ← Quotient.eq_zero_iff_mem, ← RingHom.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
⊢ I.jacobson = I
have hi' : RingHom.ker (mapRingHom i) ≤ I
Tactic: have hi' : RingHom.ker (mapRingHom i) ≤ I := by
    intro f hf
    apply polynomial_mem_ideal_of_coeff_mem_ideal I f
    intro n
    replace hf := congrArg (fun g : Polynomial ((Ideal.Quotient.mk I).comp C).range => g.coeff n) hf
    change (Polynomial.map ((Ideal.Quotient.mk I).comp C).rangeRestrict f).coeff n = 0 at hf
    rw [coeff_map, Subtype.ext_iff] at hf
    rwa [mem_comap, ← Quotient.eq_zero_iff_mem, ← RingHom.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
hi' : RingHom.ker (mapRingHom i) ≤ I
⊢ I.jacobson = I
have R'_jacob : IsJacobsonRing.{u_1} ↥R'
Tactic: have R'_jacob : IsJacobsonRing R' := isJacobsonRing_of_surjective ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing.{u_1} ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
⊢ I.jacobson = I
have h_surj : Function.Surjective (α := R[X]) (β := (↥R')[X]) (⇑(mapRingHom i) : (a : R[X]) → (↥R')[X])
Tactic: have h_surj : Function.Surjective (mapRingHom i) := Polynomial.map_surjective i hi
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing.{u_1} ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective (α := R[X]) (β := (↥R')[X]) (⇑(mapRingHom i) : (a : R[X]) → (↥R')[X])
⊢ I.jacobson = I
have this : J.IsPrime
Tactic: have : IsPrime J := map_isPrime_of_surjective h_surj hi'
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing.{u_1} ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective (α := R[X]) (β := (↥R')[X]) (⇑(mapRingHom i) : (a : R[X]) → (↥R')[X])
this : J.IsPrime
h : J.jacobson = J
⊢ I.jacobson = I
have h₁ : Eq (α := Ideal R[X]) (comap (mapRingHom i) J.jacobson) (comap (mapRingHom i) J)
Tactic: replace h := congrArg (comap (Polynomial.mapRingHom i)) h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing.{u_1} ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective (α := R[X]) (β := (↥R')[X]) (⇑(mapRingHom i) : (a : R[X]) → (↥R')[X])
this : J.IsPrime
h : Eq (α := Ideal R[X]) (comap (mapRingHom i) J.jacobson) (comap (mapRingHom i) J)
⊢ I.jacobson = I
have h₁ : I.jacobson ⊔ comap (mapRingHom i) ⊥ = I ⊔ comap (mapRingHom i) ⊥
Tactic: rw [← map_jacobson_of_surjective h_surj hi', comap_map_of_surjective _ h_surj,
      comap_map_of_surjective _ h_surj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing.{u_1} ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective (α := R[X]) (β := (↥R')[X]) (⇑(mapRingHom i) : (a : R[X]) → (↥R')[X])
this : J.IsPrime
h : I.jacobson ⊔ comap (mapRingHom i) ⊥ = I ⊔ comap (mapRingHom i) ⊥
⊢ I.jacobson = I
have refine : I.jacobson ≤ I
Tactic: refine le_antisymm ?_ le_jacobson
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing.{u_1} ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective (α := R[X]) (β := (↥R')[X]) (⇑(mapRingHom i) : (a : R[X]) → (↥R')[X])
this : J.IsPrime
⊢ I.jacobson = I
have suffices : J.jacobson = J
Tactic: suffices h : J.jacobson = J by
    replace h := congrArg (comap (Polynomial.mapRingHom i)) h
    rw [← map_jacobson_of_surjective h_surj hi', comap_map_of_surjective _ h_surj,
      comap_map_of_surjective _ h_surj] at h
    refine le_antisymm ?_ le_jacobson
    exact le_trans (le_sup_of_le_left le_rfl) (le_trans (le_of_eq h) (sup_le le_rfl hi'))
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing.{u_1} ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective (α := R[X]) (β := (↥R')[X]) (⇑(mapRingHom i) : (a : R[X]) → (↥R')[X])
this : J.IsPrime
⊢ J.jacobson = J
have apply : ∀ (x : ↥R'), Membership.mem (α := (↥R')[X]) J ((C : (a : ↥R') → (↥R')[X]) x : (↥R')[X]) → x = 0
Tactic: apply isJacobsonRing_polynomial_of_domain R' J
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ IsJacobsonRing.{u_1} R[X] ↔ IsJacobsonRing R
have refine : IsJacobsonRing.{u_1} R[X] → IsJacobsonRing R
Tactic: refine ⟨?_, isJacobsonRing_polynomial_of_isJacobsonRing⟩
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : Nontrivial R
hR : IsJacobsonRing R
hP' : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
⊢ RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk P) C)
have refine : RingHom.IsIntegral (quotientMap P C sorry)
Tactic: refine (isIntegral_quotientMap_iff _).mp ?_
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : Nontrivial R
hR : IsJacobsonRing R
hP' : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
P' : Ideal R := comap (F := R →+* R[X]) C P
pX : R[X]
hpX : pX ∈ P
hp0 :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX) 0
a : R ⧸ P' := (map (Ideal.Quotient.mk P') pX).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
⊢ RingHom.IsIntegral (quotientMap P C ⋯)
have hP'_prime : P'.IsPrime
Tactic: have hP'_prime : P'.IsPrime := comap_isPrime C P
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : Nontrivial R
hR : IsJacobsonRing R
hP' : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
P' : Ideal R := comap (F := R →+* R[X]) C P
pX : R[X]
hpX : pX ∈ P
hp0 :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX) 0
a : R ⧸ P' := (map (Ideal.Quotient.mk P') pX).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
hP'_prime : P'.IsPrime
⊢ RingHom.IsIntegral (quotientMap P C ⋯)
have hM : 0 ∉ M
Tactic: have hM : (0 : R ⧸ P') ∉ M := fun ⟨n, hn⟩ =>
    hp0 <| leadingCoeff_eq_zero.mp (eq_zero_of_pow_eq_zero hn)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : IsJacobsonRing R
P' : Ideal R := comap (F := R →+* R[X]) C P
⊢ RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk P) C)
have this : P'.IsPrime
Tactic: have : P'.IsPrime := comap_isPrime C P
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : IsJacobsonRing R
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
⊢ RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk P) C)
have hf : Function.Surjective (α := R[X]) (β := (R ⧸ P')[X]) (⇑f : (a : R[X]) → (R ⧸ P')[X])
Tactic: have hf : Function.Surjective ↑f := map_surjective (Ideal.Quotient.mk P') Quotient.mk_surjective
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : IsJacobsonRing R
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective (α := R[X]) (β := (R ⧸ P')[X]) (⇑f : (a : R[X]) → (R ⧸ P')[X])
⊢ P = comap f (Ideal.map f P)
have rw : P = P ⊔ comap f ⊥
Tactic: rw [comap_map_of_surjective _ hf]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : IsJacobsonRing R
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective (α := R[X]) (β := (R ⧸ P')[X]) (⇑f : (a : R[X]) → (R ⧸ P')[X])
⊢ P = P ⊔ comap f ⊥
have refine : comap f ⊥ ≤ P
Tactic: refine le_antisymm (le_sup_of_le_left le_rfl) (sup_le le_rfl ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : IsJacobsonRing R
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective (α := R[X]) (β := (R ⧸ P')[X]) (⇑f : (a : R[X]) → (R ⧸ P')[X])
⊢ comap f ⊥ ≤ P
have refine : ∀ (p : R[X]) (hp : Membership.mem (γ := Submodule R[X] R[X]) (comap f ⊥) p) (n : ℕ),
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))
    ((Ideal.Quotient.mk (comap (F := R →+* R[X]) C P) : (a : R) → R ⧸ comap C P) (p.coeff n) :
      HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))
    (0 : HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))
Tactic: refine fun p hp =>
      polynomial_mem_ideal_of_coeff_mem_ideal P p fun n => Quotient.eq_zero_iff_mem.mp ?_
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : IsJacobsonRing R
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective (α := R[X]) (β := (R ⧸ P')[X]) (⇑f : (a : R[X]) → (R ⧸ P')[X])
⊢ RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk P) C)
have hPJ : P = comap f (Ideal.map f P)
Tactic: have hPJ : P = (P.map f).comap f := by
    rw [comap_map_of_surjective _ hf]
    refine le_antisymm (le_sup_of_le_left le_rfl) (sup_le le_rfl ?_)
    refine fun p hp =>
      polynomial_mem_ideal_of_coeff_mem_ideal P p fun n => Quotient.eq_zero_iff_mem.mp ?_
    simpa only [f, coeff_map, coe_mapRingHom] using (Polynomial.ext_iff.mp hp) n
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : IsJacobsonRing R
⊢ IsMaximal (comap (F := R →+* R[X]) C P)
have rw : IsMaximal (comap (F := R →+* R[X] ⧸ P) (RingHom.comp (Ideal.Quotient.mk P) C) ⊥)
Tactic: rw [← @mk_ker _ _ P, RingHom.ker_eq_comap_bot, comap_comap]