awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Set R
p : Ideal R
inst_2 : p.IsPrime
hrm : s ⊆ (↑p : Set R)
apply : span s ≤ p
apply₁ :
  height (R := HasQuotient.Quotient R (B := Ideal R) (span s))
        (map (F := R →+* HasQuotient.Quotient R (B := Ideal R) (span s)) (Quotient.mk (span s)) p) +
      (↑(Submodule.spanFinrank (span s)) : ℕ∞) ≤
    height (R := HasQuotient.Quotient R (B := Ideal R) (span s))
        (map (F := R →+* HasQuotient.Quotient R (B := Ideal R) (span s)) (Quotient.mk (span s)) p) +
      s.encard
⊢ p.height ≤
    height (R := HasQuotient.Quotient R (B := Ideal R) (span s))
        (map (F := R →+* HasQuotient.Quotient R (B := Ideal R) (span s)) (Quotient.mk (span s)) p) +
      s.encard

Tactic:
apply le_trans (Ideal.height_le_height_add_spanFinrank_of_le (I := span s) (p := p) ?_) ?_

Premises used: Ideal.height_le_height_add_spanFinrank_of_le, le_trans
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Set R
p : Ideal R
inst_2 : p.IsPrime
hrm rwa rwa₁ rwa₂ rwa₃ : s ⊆ (↑p : Set R)
⊢ span s ≤ p

Tactic:
rwa [span_le]

Premises used: Ideal.span_le
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Set R
p : Ideal R
inst_2 : p.IsPrime
hrm : s ⊆ (↑p : Set R)
bc : (↑(Submodule.spanFinrank (span s)) : ℕ∞) ≤ s.encard
⊢ height (R := HasQuotient.Quotient R (B := Ideal R) (span s))
        (map (F := R →+* HasQuotient.Quotient R (B := Ideal R) (span s)) (Quotient.mk (span s)) p) +
      (↑(Submodule.spanFinrank (span s)) : ℕ∞) ≤
    height (R := HasQuotient.Quotient R (B := Ideal R) (span s))
        (map (F := R →+* HasQuotient.Quotient R (B := Ideal R) (span s)) (Quotient.mk (span s)) p) +
      s.encard

Tactic:
gcongr
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Set R
p : Ideal R
inst_2 : p.IsPrime
hrm : s ⊆ (↑p : Set R)
⊢ (↑(Submodule.spanFinrank (span s)) : ℕ∞) ≤ s.encard

Tactic:
Submodule.spanFinrank_span_le_encard _

Premises used: Submodule.spanFinrank_span_le_encard
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Set R
p : Ideal R
inst_2 : p.IsPrime
hrm : s ⊆ (↑p : Set R)
⊢ (↑(Submodule.spanFinrank (span s)) : ℕ∞) ≤ s.encard

Tactic:
exact Submodule.spanFinrank_span_le_encard _

Premises used: Submodule.spanFinrank_span_le_encard
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
s : Set R
hs : s ⊆ (↑p : Set R)
⊢ (↑p.height : WithBot ℕ∞) ≤
    ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span s)) + (↑s.encard : WithBot ℕ∞)

Tactic:
le_trans (height_le_ringKrullDim_quotient_add_spanFinrank (I := .span s) ?_) ?_

Premises used: height_le_ringKrullDim_quotient_add_spanFinrank, le_trans
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
s : Set R
hs : s ⊆ (↑p : Set R)
refine_1 : span s ≤ p
refine_2 :
  ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span s)) +
      (↑(Submodule.spanFinrank (span s)) : WithBot ℕ∞) ≤
    ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span s)) + (↑s.encard : WithBot ℕ∞)
⊢ (↑p.height : WithBot ℕ∞) ≤
    ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span s)) + (↑s.encard : WithBot ℕ∞)

Tactic:
refine le_trans (height_le_ringKrullDim_quotient_add_spanFinrank (I := .span s) ?_) ?_

Premises used: height_le_ringKrullDim_quotient_add_spanFinrank, le_trans
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
s : Set R
hs : s ⊆ (↑p : Set R)
⊢ span s ≤ p

Tactic:
simpa [span_le]

Premises used: Ideal.span_le
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
s : Set R
hs : s ⊆ (↑p : Set R)
refine_2 : (↑(Submodule.spanFinrank (span s)) : WithBot ℕ∞) ≤ (↑s.encard : WithBot ℕ∞)
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span s)) +
      (↑(Submodule.spanFinrank (span s)) : WithBot ℕ∞) ≤
    ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span s)) + (↑s.encard : WithBot ℕ∞)

Tactic:
gcongr
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
s : Set R
hs : s ⊆ (↑p : Set R)
refine_2 : (↑(Submodule.spanFinrank (span s)) : ℕ∞) ≤ s.encard
⊢ (↑(Submodule.spanFinrank (span s)) : WithBot ℕ∞) ≤ (↑s.encard : WithBot ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
s : Set R
hs : s ⊆ (↑p : Set R)
⊢ (↑(Submodule.spanFinrank (span s)) : ℕ∞) ≤ s.encard

Tactic:
Submodule.spanFinrank_span_le_encard _

Premises used: Submodule.spanFinrank_span_le_encard
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
s : Set R
hs : s ⊆ (↑p : Set R)
⊢ (↑(Submodule.spanFinrank (span s)) : ℕ∞) ≤ s.encard

Tactic:
exact Submodule.spanFinrank_span_le_encard _

Premises used: Submodule.spanFinrank_span_le_encard
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
r : R
p : Ideal R
inst_2 : p.IsPrime
hrm : r ∈ p
⊢ {r} ⊆ (↑p : Set R)

Tactic:
simpa
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
r : R
p : Ideal R
inst_2 : p.IsPrime
hrm : r ∈ p
h : 1 = Set.encard (α := R) {r}
⊢ p.height ≤
    height (R := HasQuotient.Quotient R (B := Ideal R) (span {r}))
        (map (F := R →+* HasQuotient.Quotient R (B := Ideal R) (span {r})) (Quotient.mk (span {r})) p) +
      1

Tactic:
convert! height_le_height_add_encard_of_subset { r } (p := p) (by simpa)

Premises used: Ideal.height_le_height_add_encard_of_subset, Singleton.singleton
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
r : R
p : Ideal R
inst_2 : p.IsPrime
hrm : r ∈ p
⊢ 1 = Set.encard (α := R) {r}

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
r : R
p : Ideal R
inst_2 : p.IsPrime
hrp : r ∈ p
⊢ {r} ⊆ (↑p : Set R)

Tactic:
simpa
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
r : R
p : Ideal R
inst_2 : p.IsPrime
hrp : r ∈ p
h : 1 = (↑(Set.encard (α := R) {r}) : WithBot ℕ∞)
⊢ (↑p.height : WithBot ℕ∞) ≤ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span {r})) + 1

Tactic:
convert! Ideal.height_le_ringKrullDim_quotient_add_encard { r } (by simpa)

Premises used: Ideal.height_le_ringKrullDim_quotient_add_encard, Singleton.singleton
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
r : R
p : Ideal R
inst_2 : p.IsPrime
hrp : r ∈ p
⊢ 1 = (↑(Set.encard (α := R) {r}) : WithBot ℕ∞)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Set R
hs : s ⊆ (↑(Ring.jacobson R) : Set R)
⊢ ringKrullDim R ≤ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span s)) + (↑s.encard : WithBot ℕ∞)

Tactic:
le_trans (ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank (Ideal.span s) ?_) ?_

Premises used: ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank, Ideal.span, le_trans
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Set R
hs : s ⊆ (↑(Ring.jacobson R) : Set R)
refine_1 : LE.le (α := Ideal R) (Ideal.span s) (Ring.jacobson R)
refine_2 :
  ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span s)) +
      (↑(Submodule.spanFinrank (Ideal.span s)) : WithBot ℕ∞) ≤
    ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span s)) + (↑s.encard : WithBot ℕ∞)
⊢ ringKrullDim R ≤ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span s)) + (↑s.encard : WithBot ℕ∞)

Tactic:
refine le_trans (ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank (Ideal.span s) ?_) ?_

Premises used: ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank, Ideal.span, le_trans
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Set R
hs : s ⊆ (↑(Ring.jacobson R) : Set R)
⊢ LE.le (α := Ideal R) (Ideal.span s) (Ring.jacobson R)

Tactic:
simpa [Ideal.span_le]

Premises used: Ideal.span_le
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Set R
hs : s ⊆ (↑(Ring.jacobson R) : Set R)
refine_2 : (↑(Submodule.spanFinrank (Ideal.span s)) : WithBot ℕ∞) ≤ (↑s.encard : WithBot ℕ∞)
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span s)) +
      (↑(Submodule.spanFinrank (Ideal.span s)) : WithBot ℕ∞) ≤
    ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span s)) + (↑s.encard : WithBot ℕ∞)

Tactic:
gcongr
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Set R
hs : s ⊆ (↑(Ring.jacobson R) : Set R)
refine_2 : (↑(Submodule.spanFinrank (Ideal.span s)) : ℕ∞) ≤ s.encard
⊢ (↑(Submodule.spanFinrank (Ideal.span s)) : WithBot ℕ∞) ≤ (↑s.encard : WithBot ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Set R
hs : s ⊆ (↑(Ring.jacobson R) : Set R)
⊢ (↑(Submodule.spanFinrank (Ideal.span s)) : ℕ∞) ≤ s.encard

Tactic:
Submodule.spanFinrank_span_le_encard _

Premises used: Submodule.spanFinrank_span_le_encard
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Set R
hs : s ⊆ (↑(Ring.jacobson R) : Set R)
⊢ (↑(Submodule.spanFinrank (Ideal.span s)) : ℕ∞) ≤ s.encard

Tactic:
exact Submodule.spanFinrank_span_le_encard _

Premises used: Submodule.spanFinrank_span_le_encard
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Finset R
hs : (↑s : Set R) ⊆ (↑(Ring.jacobson R) : Set R)
⊢ ringKrullDim R ≤
    ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span (↑s : Set R))) +
      (↑(↑s : Set R).encard : WithBot ℕ∞)

Tactic:
ringKrullDim_le_ringKrullDim_quotient_add_encard s hs

Premises used: ringKrullDim_le_ringKrullDim_quotient_add_encard
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Finset R
hs : (↑s : Set R) ⊆ (↑(Ring.jacobson R) : Set R)
h : (↑s.card : WithBot ℕ∞) = (↑(↑s : Set R).encard : WithBot ℕ∞)
⊢ ringKrullDim R ≤
    ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span (↑s : Set R))) + (↑s.card : WithBot ℕ∞)

Tactic:
convert! ringKrullDim_le_ringKrullDim_quotient_add_encard s hs

Premises used: ringKrullDim_le_ringKrullDim_quotient_add_encard
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Finset R
hs : (↑s : Set R) ⊆ (↑(Ring.jacobson R) : Set R)
h h₁ h₂ h₃ : s.card = s.card
⊢ (↑s.card : WithBot ℕ∞) = (↑(↑s : Set R).encard : WithBot ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
p : Ideal R
inst_5 : p.IsPrime
P : Ideal S
inst_6 : P.IsPrime
inst_7 : P.LiesOver p
obtain :
  ∀ (s : Finset R) (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p)
    (heq : (↑s.card : ℕ∞) = p.height),
    P.height ≤
      p.height +
        height (R := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
          (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
            (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)
⊢ P.height ≤
    p.height +
      height (R := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
          (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)

Tactic:
obtain ⟨s, hp, heq⟩ := p.exists_finset_card_eq_height_of_isNoetherianRing

Premises used: Ideal.exists_finset_card_eq_height_of_isNoetherianRing
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
p : Ideal R
inst_5 : p.IsPrime
P : Ideal S
inst_6 : P.IsPrime
inst_7 : P.LiesOver p
s : Finset R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
heq : (↑s.card : ℕ∞) = p.height
P' : Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) :=
  map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P
obtain :
  ∀ (s' : Finset (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)))
    (hP' :
      Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
        (Ideal.minimalPrimes (span (↑s' : Set (S ⧸ map (algebraMap R S) p)))) P')
    (heq' : (↑s'.card : ℕ∞) = P'.height),
    P.height ≤
      p.height +
        height (R := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
          (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
            (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)
⊢ P.height ≤
    p.height +
      height (R := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
          (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)

Tactic:
obtain ⟨s', hP', heq'⟩ := P'.exists_finset_card_eq_height_of_isNoetherianRing

Premises used: Ideal.exists_finset_card_eq_height_of_isNoetherianRing
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
p : Ideal R
inst_5 : p.IsPrime
P : Ideal S
inst_6 : P.IsPrime
inst_7 : P.LiesOver p
s : Finset R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
heq : (↑s.card : ℕ∞) = p.height
P' : Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) :=
  map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P
s' : Finset (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
hP' :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes (span (↑s' : Set (S ⧸ map (algebraMap R S) p)))) P'
heq' : (↑s'.card : ℕ∞) = P'.height
⊢ (↑s' : Set (S ⧸ map (algebraMap R S) p)) ⊆ (↑P' : Set (S ⧸ map (algebraMap R S) p))

Tactic:
have hsP'sub : (s' : Set <| S ⧸ (Ideal.map (algebraMap R S) p)) ⊆ (P' : Set <| S ⧸ _) :=
    fun x hx ↦ hP'.le (Ideal.subset_span hx)
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
p : Ideal R
inst_5 : p.IsPrime
P : Ideal S
inst_6 : P.IsPrime
inst_7 : P.LiesOver p
s : Finset R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
heq : (↑s.card : ℕ∞) = p.height
P' : Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) :=
  map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P
s' : Finset (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
hP' :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes (span (↑s' : Set (S ⧸ map (algebraMap R S) p)))) P'
heq' : (↑s'.card : ℕ∞) = P'.height
hsP'sub : (↑s' : Set (S ⧸ map (algebraMap R S) p)) ⊆ (↑P' : Set (S ⧸ map (algebraMap R S) p))
⊢ Set.SurjOn (⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p)
    (↑P : Set S) (↑s' : Set (S ⧸ map (algebraMap R S) p))

Tactic:
Set.SurjOn.mono subset_rfl hsP'sub fun x hx ↦ ?_

Premises used: Set.SurjOn.mono, subset_rfl
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
p : Ideal R
inst_5 : p.IsPrime
P : Ideal S
inst_6 : P.IsPrime
inst_7 : P.LiesOver p
s : Finset R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
heq : (↑s.card : ℕ∞) = p.height
P' : Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) :=
  map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P
s' : Finset (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
hP' :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes (span (↑s' : Set (S ⧸ map (algebraMap R S) p)))) P'
heq' : (↑s'.card : ℕ∞) = P'.height
hsP'sub : (↑s' : Set (S ⧸ map (algebraMap R S) p)) ⊆ (↑P' : Set (S ⧸ map (algebraMap R S) p))
refine :
  ∀ (x : HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    (hx : x ∈ (↑P' : Set (S ⧸ map (algebraMap R S) p))),
    Membership.mem (γ := Set (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)))
      ((⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) '' (↑P : Set S))
      x
⊢ Set.SurjOn (⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p)
    (↑P : Set S) (↑s' : Set (S ⧸ map (algebraMap R S) p))

Tactic:
refine Set.SurjOn.mono subset_rfl hsP'sub fun x hx ↦ ?_

Premises used: Set.SurjOn.mono, subset_rfl
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
p : Ideal R
inst_5 : p.IsPrime
P : Ideal S
inst_6 : P.IsPrime
inst_7 : P.LiesOver p
s : Finset R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
heq : (↑s.card : ℕ∞) = p.height
P' : Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) :=
  map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P
s' : Finset (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
hP' :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes (span (↑s' : Set (S ⧸ map (algebraMap R S) p)))) P'
heq' : (↑s'.card : ℕ∞) = P'.height
hsP'sub : (↑s' : Set (S ⧸ map (algebraMap R S) p)) ⊆ (↑P' : Set (S ⧸ map (algebraMap R S) p))
x : HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)
hx : x ∈ (↑P' : Set (S ⧸ map (algebraMap R S) p))
obtain :
  ∀ (y : S)
    (hx :
      Membership.mem (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (↑P' : Set (S ⧸ map (algebraMap R S) p))
        ((Quotient.mk (map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ map (algebraMap R S) p) y :
          HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))),
    Membership.mem (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) (γ :=
      Set (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)))
      ((⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) '' (↑P : Set S))
      ((Quotient.mk (map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ map (algebraMap R S) p) y :
        HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
⊢ Membership.mem (γ := Set (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)))
    ((⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) '' (↑P : Set S)) x

Tactic:
obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, rfl