awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.GoingDown
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))
⊢ 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
-- Module: Mathlib.RingTheory.Ideal.GoingDown
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_2 :
  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))
this : Module.FaithfullyFlat.{u_3, u_4} (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) ⋯))

Tactic:
apply PrimeSpectrum.comap_surjective_of_faithfullyFlat

Premises used: PrimeSpectrum.comap_surjective_of_faithfullyFlat
-- Module: Mathlib.RingTheory.Ideal.GoingUp
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
⊢ 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

Premises used: Polynomial.divX_mul_X_add, Polynomial.eval₂_mul, Polynomial.eval₂_X, Polynomial.eval₂_C, Polynomial.eval₂_add
-- Module: Mathlib.RingTheory.Ideal.GoingUp
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)

Tactic:
mem_comap.mpr ((I.add_mem_iff_right ?_).mp hp)

Premises used: Iff.mpr, Ideal.add_mem_iff_right, Iff.mp, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Ideal.GoingUp
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
refine : eval₂ f r p.divX * r ∈ I
⊢ Membership.mem (γ := Ideal R) (comap f I) (p.coeff 0)

Tactic:
refine mem_comap.mpr ((I.add_mem_iff_right ?_).mp hp)

Premises used: Iff.mpr, Ideal.add_mem_iff_right, Iff.mp, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Ideal.GoingUp
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
⊢ eval₂ f r p.divX * r ∈ I

Tactic:
I.mul_mem_left _ hr

Premises used: Set.Mem, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Ideal.GoingUp
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
⊢ eval₂ f r p.divX * r ∈ I

Tactic:
exact I.mul_mem_left _ hr

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Ideal.GoingUp
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 = 0
⊢ Membership.mem (γ := Ideal R) (comap f I) (p.coeff 0)

Tactic:
coeff_zero_mem_comap_of_root_mem_of_eval_mem hr (hp.symm ▸ I.zero_mem)

Premises used: Ideal.coeff_zero_mem_comap_of_root_mem_of_eval_mem, Eq.rec, Ideal.zero_mem, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.GoingUp
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)

Tactic:
p.recOnHorner ?_ ?_ ?_

Premises used: Polynomial.recOnHorner
-- Module: Mathlib.RingTheory.Ideal.GoingUp
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)
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)
⊢ p ≠ 0 → eval₂ f r p = 0 → ∃ (i : ℕ), p.coeff i ≠ 0 ∧ Membership.mem (γ := Ideal R) (comap f I) (p.coeff i)

Tactic:
refine p.recOnHorner ?_ ?_ ?_
-- Module: Mathlib.RingTheory.Ideal.GoingUp
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]
h : 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:
contradiction
-- Module: Mathlib.RingTheory.Ideal.GoingUp
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
refine_2 :
  (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)) →
    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:
_
-- Module: Mathlib.RingTheory.Ideal.GoingUp
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)
refine_2 :
  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)
⊢ 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:
_
-- Module: Mathlib.RingTheory.Ideal.GoingUp
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)

Tactic:
⟨0, ?_, coeff_zero_mem_comap_of_root_mem hr hp⟩

Premises used: And.intro, Exists.intro, OfNat.ofNat, Ideal.coeff_zero_mem_comap_of_root_mem
-- Module: Mathlib.RingTheory.Ideal.GoingUp
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
refine_2 : (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).coeff 0 ≠ 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 ⟨0, ?_, coeff_zero_mem_comap_of_root_mem hr hp⟩
-- Module: Mathlib.RingTheory.Ideal.GoingUp
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
⊢ (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).coeff 0 ≠ 0

Tactic:
simp [coeff_eq_zero, a_ne_zero]
-- Module: Mathlib.RingTheory.Ideal.GoingUp
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)
refine_3 :
  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)
⊢ 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:
_
-- Module: Mathlib.RingTheory.Ideal.GoingUp
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
⊢ eval₂ f r p * r = 0

Tactic:
rw [eval₂_mul, eval₂_X] at hp

Premises used: Polynomial.eval₂_mul, Polynomial.eval₂_X
-- Module: Mathlib.RingTheory.Ideal.GoingUp
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
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)
⊢ ∃ (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)
-- Module: Mathlib.RingTheory.Ideal.GoingUp
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)

Tactic:
⟨i + 1, ?_, ?_⟩

Premises used: HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.GoingUp
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
refine_3₁ : Membership.mem (γ := Ideal R) (comap f I) ((p * X).coeff (i + 1))
⊢ ∃ (i : ℕ), (p * X).coeff i ≠ 0 ∧ Membership.mem (γ := Ideal R) (comap f I) ((p * X).coeff i)

Tactic:
refine ⟨i + 1, ?_, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.GoingUp
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)
⊢ (p * X).coeff (i + 1) ≠ 0

Tactic:
simp [hi]
-- Module: Mathlib.RingTheory.Ideal.GoingUp
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)
⊢ Membership.mem (γ := Ideal R) (comap f I) ((p * X).coeff (i + 1))

Tactic:
simpa [hi] using mem
-- Module: Mathlib.RingTheory.Ideal.GoingUp
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)

Tactic:
quotientMap_injective' (le_of_eq ?_)

Premises used: Ideal.quotientMap_injective', le_of_eq
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
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
⊢ 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)

Tactic:
refine quotientMap_injective' (le_of_eq ?_)

Premises used: Ideal.quotientMap_injective', le_of_eq
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
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
⊢ 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:
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)]

Premises used: Polynomial.C, Polynomial.map_surjective, Ideal.Quotient.mk, Ideal.Quotient.mk_surjective, Ideal.comap_map_of_surjective, Polynomial.mapRingHom, Ideal.comap
-- Module: Mathlib.RingTheory.Ideal.GoingUp
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

Tactic:
le_antisymm (sup_le le_rfl ?_) (le_sup_of_le_left le_rfl)

Premises used: le_rfl, le_sup_of_le_left, le_antisymm, sup_le
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
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
⊢ 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:
refine le_antisymm (sup_le le_rfl ?_) (le_sup_of_le_left le_rfl)

Premises used: le_rfl, le_sup_of_le_left, le_antisymm, sup_le
-- Module: Mathlib.RingTheory.Ideal.GoingUp
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

Tactic:
fun p hp =>
    polynomial_mem_ideal_of_coeff_mem_ideal P p fun n => Ideal.Quotient.eq_zero_iff_mem.mp ?_

Premises used: Set.Mem, Ideal.polynomial_mem_ideal_of_coeff_mem_ideal, Ideal.Quotient.eq_zero_iff_mem, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
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))
⊢ 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 fun p hp =>
    polynomial_mem_ideal_of_coeff_mem_ideal P p fun n => Ideal.Quotient.eq_zero_iff_mem.mp ?_

Premises used: Ideal.polynomial_mem_ideal_of_coeff_mem_ideal, Ideal.Quotient.eq_zero_iff_mem, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
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:
simpa only [coeff_map, coe_mapRingHom] using ext_iff.mp (Ideal.mem_bot.mp (mem_comap.mp hp)) n

Premises used: Ideal.mem_bot, Polynomial.coeff_map, Polynomial.ext_iff, Polynomial.coe_mapRingHom, Iff.mp, Ideal.mem_comap