awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R : Type u_3
S : Type u_4
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
inst_6 : Module.Flat R S
⊢ HasGoingDown R S
have H : ∀ (P : Ideal S) [inst : P.IsPrime],
  Function.Surjective (α := PrimeSpectrum (Localization.AtPrime P)) (β :=
    PrimeSpectrum (Localization.AtPrime (Ideal.under R P)))
    (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) sorry))
Tactic: apply of_comap_localRingHom_surjective
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R : Type u_3
S : Type u_4
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
inst_6 : Module.Flat R S
P : Ideal S
hP : P.IsPrime
this : Algebra.{u_3, u_4} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
⊢ IsLocalHom (R := Localization.AtPrime (Ideal.under R P)) (S := Localization.AtPrime P) (F :=
    RingHom.{u_3, u_4} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P))
    (algebraMap (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P))
have rw : IsLocalHom (R := Localization.AtPrime (Ideal.under R P)) (S := Localization.AtPrime P) (F :=
  RingHom.{u_3, u_4} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P))
  (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) sorry)
Tactic: rw [RingHom.algebraMap_toAlgebra]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (hypothesis)
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R : Type u_3
S : Type u_4
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
inst_6 : Module.Flat R S
P : Ideal S
hP : P.IsPrime
this : Algebra.{u_3, u_4} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
⊢ Function.Surjective (α := PrimeSpectrum (Localization.AtPrime P)) (β :=
    PrimeSpectrum (Localization.AtPrime (Ideal.under R P)))
    (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
have this₁ : IsLocalHom (R := Localization.AtPrime (Ideal.under R P)) (S := Localization.AtPrime P) (F :=
  RingHom.{u_3, u_4} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P))
  (algebraMap (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P))
Tactic: have : IsLocalHom (algebraMap (Localization.AtPrime <| P.under R) (Localization.AtPrime P)) := by
    rw [RingHom.algebraMap_toAlgebra]
    exact Localization.isLocalHom_localRingHom (P.under R) P (algebraMap R S) Ideal.LiesOver.over
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingDown (hypothesis)
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R : Type u_3
S : Type u_4
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
inst_6 : Module.Flat R S
P : Ideal S
hP : P.IsPrime
this_1 : Algebra.{u_3, u_4} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
this :
  IsLocalHom (R := Localization.AtPrime (Ideal.under R P)) (S := Localization.AtPrime P) (F :=
    RingHom.{u_3, u_4} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P))
    (algebraMap (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P))
⊢ Function.Surjective (α := PrimeSpectrum (Localization.AtPrime P)) (β :=
    PrimeSpectrum (Localization.AtPrime (Ideal.under R P)))
    (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
have this₁ : Module.FaithfullyFlat.{u_3, u_4} (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P)
Tactic: have : Module.FaithfullyFlat (Localization.AtPrime (P.under R)) (Localization.AtPrime P) :=
    Module.FaithfullyFlat.of_flat_of_isLocalHom
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I : Ideal S
r : S
hr : r ∈ I
p : R[X]
hp : eval₂ f r p ∈ I
⊢ Membership.mem (γ := Ideal R) (comap f I) (p.coeff 0)
have hp₁ : HAdd.hAdd (β := S) (eval₂ f r p.divX * r) ((f : (a : R) → S) (p.coeff 0) : S) ∈ I
Tactic: rw [← p.divX_mul_X_add, eval₂_add, eval₂_C, eval₂_mul, eval₂_X] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I : Ideal S
r : S
hr : r ∈ I
p : R[X]
hp : HAdd.hAdd (β := S) (eval₂ f r p.divX * r) ((f : (a : R) → S) (p.coeff 0) : S) ∈ I
⊢ Membership.mem (γ := Ideal R) (comap f I) (p.coeff 0)
have refine : eval₂ f r p.divX * r ∈ I
Tactic: refine mem_comap.mpr ((I.add_mem_iff_right ?_).mp hp)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p : R[X]
⊢ p ≠ 0 → eval₂ f r p = 0 → ∃ (i : ℕ), p.coeff i ≠ 0 ∧ Membership.mem (γ := Ideal R) (comap f I) (p.coeff i)
have refine_1 : Ne.{u_1 + 1} (α := R[X]) 0 0 →
  eval₂ f r 0 = 0 →
    ∃ (i : ℕ), Ne.{u_1 + 1} (α := R) (coeff 0 i) 0 ∧ Membership.mem (γ := Ideal R) (comap f I) (coeff 0 i)
Tactic: refine p.recOnHorner ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p : R[X]
refine_1 :
  Ne.{u_1 + 1} (α := R[X]) 0 0 →
    eval₂ f r 0 = 0 →
      ∃ (i : ℕ), Ne.{u_1 + 1} (α := R) (coeff 0 i) 0 ∧ Membership.mem (γ := Ideal R) (comap f I) (coeff 0 i)
⊢ p ≠ 0 → eval₂ f r p = 0 → ∃ (i : ℕ), p.coeff i ≠ 0 ∧ Membership.mem (γ := Ideal R) (comap f I) (p.coeff i)
have refine_2 : ∀ (p : R[X]) (a : R),
  p.coeff 0 = 0 →
    a ≠ 0 →
      (p ≠ 0 → eval₂ f r p = 0 → ∃ (i : ℕ), p.coeff i ≠ 0 ∧ Membership.mem (γ := Ideal R) (comap f I) (p.coeff i)) →
        HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]) ≠ 0 →
          eval₂ f r (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])) = 0 →
            ∃ (i : ℕ),
              (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).coeff i ≠ 0 ∧
                Membership.mem (γ := Ideal R) (comap f I)
                  ((HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).coeff i)
Tactic: refine p.recOnHorner ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p : R[X]
refine_1 :
  Ne.{u_1 + 1} (α := R[X]) 0 0 →
    eval₂ f r 0 = 0 →
      ∃ (i : ℕ), Ne.{u_1 + 1} (α := R) (coeff 0 i) 0 ∧ Membership.mem (γ := Ideal R) (comap f I) (coeff 0 i)
refine_2 :
  ∀ (p : R[X]) (a : R),
    p.coeff 0 = 0 →
      a ≠ 0 →
        (p ≠ 0 → eval₂ f r p = 0 → ∃ (i : ℕ), p.coeff i ≠ 0 ∧ Membership.mem (γ := Ideal R) (comap f I) (p.coeff i)) →
          HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]) ≠ 0 →
            eval₂ f r (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])) = 0 →
              ∃ (i : ℕ),
                (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).coeff i ≠ 0 ∧
                  Membership.mem (γ := Ideal R) (comap f I)
                    ((HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).coeff i)
⊢ p ≠ 0 → eval₂ f r p = 0 → ∃ (i : ℕ), p.coeff i ≠ 0 ∧ Membership.mem (γ := Ideal R) (comap f I) (p.coeff i)
have refine_3 : ∀ (p : R[X]),
  p ≠ 0 →
    (p ≠ 0 → eval₂ f r p = 0 → ∃ (i : ℕ), p.coeff i ≠ 0 ∧ Membership.mem (γ := Ideal R) (comap f I) (p.coeff i)) →
      p * X ≠ 0 →
        eval₂ f r (p * X) = 0 →
          ∃ (i : ℕ), (p * X).coeff i ≠ 0 ∧ Membership.mem (γ := Ideal R) (comap f I) ((p * X).coeff i)
Tactic: refine p.recOnHorner ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p_1 p : R[X]
a : R
coeff_eq_zero : p.coeff 0 = 0
a_ne_zero : a ≠ 0
h : p ≠ 0 → eval₂ f r p = 0 → ∃ (i : ℕ), p.coeff i ≠ 0 ∧ Membership.mem (γ := Ideal R) (comap f I) (p.coeff i)
h_1 : HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]) ≠ 0
hp : eval₂ f r (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])) = 0
⊢ ∃ (i : ℕ),
    (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).coeff i ≠ 0 ∧
      Membership.mem (γ := Ideal R) (comap f I) ((HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).coeff i)
have refine_2 : (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).coeff 0 ≠ 0
Tactic: refine ⟨0, ?_, coeff_zero_mem_comap_of_root_mem hr hp⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p_1 p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ (i : ℕ), p.coeff i ≠ 0 ∧ Membership.mem (γ := Ideal R) (comap f I) (p.coeff i)
h : p * X ≠ 0
hp : eval₂ f r (p * X) = 0
⊢ ∃ (i : ℕ), (p * X).coeff i ≠ 0 ∧ Membership.mem (γ := Ideal R) (comap f I) ((p * X).coeff i)
have hp₁ : eval₂ f r p * r = 0
Tactic: rw [eval₂_mul, eval₂_X] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p_1 p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ (i : ℕ), p.coeff i ≠ 0 ∧ Membership.mem (γ := Ideal R) (comap f I) (p.coeff i)
h : p * X ≠ 0
hp : eval₂ f r p * r = 0
⊢ ∃ (i : ℕ), (p * X).coeff i ≠ 0 ∧ Membership.mem (γ := Ideal R) (comap f I) ((p * X).coeff i)
have refine_3 : ∀ (i : ℕ) (hi : p.coeff i ≠ 0) (mem : Membership.mem (γ := Ideal R) (comap f I) (p.coeff i)),
  ∃ (i : ℕ), (p * X).coeff i ≠ 0 ∧ Membership.mem (γ := Ideal R) (comap f I) ((p * X).coeff i)
Tactic: obtain ⟨i, hi, mem⟩ := ih p_nonzero (r_non_zero_divisor hp)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p_1 p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ (i : ℕ), p.coeff i ≠ 0 ∧ Membership.mem (γ := Ideal R) (comap f I) (p.coeff i)
h : p * X ≠ 0
hp : eval₂ f r p * r = 0
i : ℕ
hi : p.coeff i ≠ 0
mem : Membership.mem (γ := Ideal R) (comap f I) (p.coeff i)
⊢ ∃ (i : ℕ), (p * X).coeff i ≠ 0 ∧ Membership.mem (γ := Ideal R) (comap f I) ((p * X).coeff i)
have refine_3 : (p * X).coeff (i + 1) ≠ 0
Tactic: refine ⟨i + 1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p_1 p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ (i : ℕ), p.coeff i ≠ 0 ∧ Membership.mem (γ := Ideal R) (comap f I) (p.coeff i)
h : p * X ≠ 0
hp : eval₂ f r p * r = 0
i : ℕ
hi : p.coeff i ≠ 0
mem : Membership.mem (γ := Ideal R) (comap f I) (p.coeff i)
refine_3 : (p * X).coeff (i + 1) ≠ 0
⊢ ∃ (i : ℕ), (p * X).coeff i ≠ 0 ∧ Membership.mem (γ := Ideal R) (comap f I) ((p * X).coeff i)
have refine_3₁ : Membership.mem (γ := Ideal R) (comap f I) ((p * X).coeff (i + 1))
Tactic: refine ⟨i + 1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
⊢ Function.Injective (α := R[X] ⧸ P) (β :=
    HasQuotient.Quotient (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X] (B :=
      Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
      (map (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
        (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) P))
    (⇑(quotientMap
          (map (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
            (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) P)
          (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) ⋯) :
      (a : R[X] ⧸ P) → (R ⧸ comap C P)[X] ⧸ map (mapRingHom (Quotient.mk (comap C P))) P)
have refine : comap (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P)))
    (map (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
      (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) P) =
  P
Tactic: refine quotientMap_injective' (le_of_eq ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
⊢ comap (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
      (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P)))
      (map (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
        (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) P) =
    P
have rw : P ⊔
    comap (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
      (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) ⊥ =
  P
Tactic: rw [comap_map_of_surjective (mapRingHom (Ideal.Quotient.mk (P.comap (C : R →+* R[X]))))
      (map_surjective (Ideal.Quotient.mk (P.comap (C : R →+* R[X]))) Ideal.Quotient.mk_surjective)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
⊢ P ⊔
      comap (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
        (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) ⊥ =
    P
have refine : comap (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) ⊥ ≤
  P
Tactic: refine le_antisymm (sup_le le_rfl ?_) (le_sup_of_le_left le_rfl)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
⊢ comap (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
      (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) ⊥ ≤
    P
have refine : ∀ (p : R[X])
  (hp :
    Membership.mem (γ := Submodule R[X] R[X])
      (comap (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
        (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) ⊥)
      p)
  (n : ℕ),
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))
    ((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 => Ideal.Quotient.eq_zero_iff_mem.mp ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
⊢ ∃ p ∈ P,
    Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
      (Polynomial.map (Quotient.mk (comap (F := R →+* R[X]) C P)) p) 0
have obtain : ∀ (m : ↥P) (hm : m ≠ 0),
  ∃ p ∈ P,
    Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
      (Polynomial.map (Quotient.mk (comap (F := R →+* R[X]) C P)) p) 0
Tactic: obtain ⟨m, hm⟩ := Submodule.nonzero_mem_of_bot_lt (bot_lt_iff_ne_bot.mpr Pb)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
m : ↥P
hm : m ≠ 0
⊢ ∃ p ∈ P,
    Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
      (Polynomial.map (Quotient.mk (comap (F := R →+* R[X]) C P)) p) 0
have refine : ∀
  (pp0 :
    Eq (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
      (Polynomial.map (Quotient.mk (comap (F := R →+* R[X]) C P)) (↑m : R[X])) 0),
  (↑m : R[X]) = 0
Tactic: refine ⟨m, Submodule.coe_mem m, fun pp0 => hm (Submodule.coe_eq_zero.mp ?_)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
m : ↥P
hm : m ≠ 0
pp0 :
  Eq (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (Polynomial.map (Quotient.mk (comap (F := R →+* R[X]) C P)) (↑m : R[X])) 0
⊢ (↑m : R[X]) = 0
have R₁ : Function.Injective (α := R[X]) (β := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
  (⇑(mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) : (a : R[X]) → (R ⧸ comap C P)[X])
Tactic: refine
    (injective_iff_map_eq_zero (Polynomial.mapRingHom (Ideal.Quotient.mk
      (P.comap (C : R →+* R[X]))))).mp
      ?_ _ pp0
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
m : ↥P
hm : m ≠ 0
pp0 :
  Eq (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (Polynomial.map (Quotient.mk (comap (F := R →+* R[X]) C P)) (↑m : R[X])) 0
⊢ Function.Injective (α := R[X]) (β := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (⇑(mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) : (a : R[X]) → (R ⧸ comap C P)[X])
have refine : Eq (α := Ideal R)
  (RingHom.ker (F := R →+* HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))
    (Quotient.mk (comap (F := R →+* R[X]) C P)))
  ⊥
Tactic: refine map_injective _ ((RingHom.injective_iff_ker_eq_bot (Ideal.Quotient.mk (P.comap C))).mpr ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
m : ↥P
hm : m ≠ 0
pp0 :
  Eq (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (Polynomial.map (Quotient.mk (comap (F := R →+* R[X]) C P)) (↑m : R[X])) 0
⊢ Eq (α := Ideal R)
    (RingHom.ker (F := R →+* HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))
      (Quotient.mk (comap (F := R →+* R[X]) C P)))
    ⊥
have rw : Eq (α := Ideal R) (comap (F := R →+* R[X]) C P) ⊥
Tactic: rw [mk_ker]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I J : Ideal S
inst_2 : I.IsPrime
hIJ : I ≤ J
r : S
hr : r ∈ (↑J : Set S) \ (↑I : Set S)
p : R[X]
p_ne_zero :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap f I))[X]) (Polynomial.map (Quotient.mk (comap f I)) p) 0
hpI : eval₂ f r p ∈ I
⊢ ∃ (i : ℕ), p.coeff i ∈ (↑(comap f J) : Set R) \ (↑(comap f I) : Set R)
have hrJ : r ∈ (↑J : Set S)
Tactic: obtain ⟨hrJ, hrI⟩ := hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I J : Ideal S
inst_2 : I.IsPrime
hIJ : I ≤ J
r : S
hr : r ∈ (↑J : Set S) \ (↑I : Set S)
p : R[X]
p_ne_zero :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap f I))[X]) (Polynomial.map (Quotient.mk (comap f I)) p) 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ (↑J : Set S)
⊢ ∃ (i : ℕ), p.coeff i ∈ (↑(comap f J) : Set R) \ (↑(comap f I) : Set R)
have hrI : r ∉ (↑I : Set S)
Tactic: obtain ⟨hrJ, hrI⟩ := hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I J : Ideal S
inst_2 : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap f I))[X]) (Polynomial.map (Quotient.mk (comap f I)) p) 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ (↑J : Set S)
hrI : r ∉ (↑I : Set S)
⊢ ∃ (i : ℕ), p.coeff i ∈ (↑(comap f J) : Set R) \ (↑(comap f I) : Set R)
have rbar_ne_zero : Ne (α := S ⧸ I) ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I) (0 : S ⧸ I)
Tactic: have rbar_ne_zero : Ideal.Quotient.mk I r ≠ 0 := mt (Quotient.mk_eq_zero I).mp hrI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I J : Ideal S
inst_2 : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap f I))[X]) (Polynomial.map (Quotient.mk (comap f I)) p) 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ (↑J : Set S)
hrI : r ∉ (↑I : Set S)
rbar_ne_zero : Ne (α := S ⧸ I) ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I) (0 : S ⧸ I)
⊢ ∃ (i : ℕ), p.coeff i ∈ (↑(comap f J) : Set R) \ (↑(comap f I) : Set R)
have rbar_mem_J : Membership.mem (α := S ⧸ I) (γ := Ideal (S ⧸ I)) (map (F := S →+* S ⧸ I) (Quotient.mk I) J)
  ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I)
Tactic: have rbar_mem_J : Ideal.Quotient.mk I r ∈ J.map (Ideal.Quotient.mk I) := mem_map_of_mem _ hrJ
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I J : Ideal S
inst_2 : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap f I))[X]) (Polynomial.map (Quotient.mk (comap f I)) p) 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ (↑J : Set S)
hrI : r ∉ (↑I : Set S)
rbar_ne_zero : Ne (α := S ⧸ I) ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I) (0 : S ⧸ I)
rbar_mem_J :
  Membership.mem (α := S ⧸ I) (γ := Ideal (S ⧸ I)) (map (F := S →+* S ⧸ I) (Quotient.mk I) J)
    ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I)
⊢ ∃ (i : ℕ), p.coeff i ∈ (↑(comap f J) : Set R) \ (↑(comap f I) : Set R)
have quotient_f : ∀ (x : R),
  Membership.mem (γ := Ideal R) (comap f I) x →
    Eq.{u_2 + 1} (α := S ⧸ I)
      (((RingHom.comp (Quotient.mk I) f : RingHom.{u_1, u_2} R (S ⧸ I)) : (a : R) → S ⧸ I) x : S ⧸ I) (0 : S ⧸ I)
Tactic: have quotient_f : ∀ x ∈ I.comap f, (Ideal.Quotient.mk I).comp f x = 0 := by
    simp [Quotient.eq_zero_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I J : Ideal S
inst_2 : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap f I))[X]) (Polynomial.map (Quotient.mk (comap f I)) p) 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ (↑J : Set S)
hrI : r ∉ (↑I : Set S)
rbar_ne_zero : Ne (α := S ⧸ I) ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I) (0 : S ⧸ I)
rbar_mem_J :
  Membership.mem (α := S ⧸ I) (γ := Ideal (S ⧸ I)) (map (F := S →+* S ⧸ I) (Quotient.mk I) J)
    ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I)
quotient_f :
  ∀ (x : R),
    Membership.mem (γ := Ideal R) (comap f I) x →
      Eq.{u_2 + 1} (α := S ⧸ I)
        (((RingHom.comp (Quotient.mk I) f : RingHom.{u_1, u_2} R (S ⧸ I)) : (a : R) → S ⧸ I) x : S ⧸ I) (0 : S ⧸ I)
⊢ eval₂ (Quotient.lift (comap f I) (RingHom.comp (Quotient.mk I) f) quotient_f) ((Quotient.mk I : (a : S) → S ⧸ I) r)
      (Polynomial.map (Quotient.mk (comap f I)) p) =
    0
have h : eval₂ (Quotient.lift (comap f I) (RingHom.comp (Quotient.mk I) f) quotient_f) ((Quotient.mk I : (a : S) → S ⧸ I) r)
    (Polynomial.map (Quotient.mk (comap f I)) p) =
  (Quotient.mk I : (a : S) → S ⧸ I) (eval₂ f r p)
Tactic: convert! Quotient.eq_zero_iff_mem.mpr hpI