awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this_2 : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
r : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))
h : (fun (q : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) ↦ q.IsPrime ∧ map (R := R) f (span {x}) ≤ q) r
hrp : r ≤ map f p
hr : r.IsPrime
hxr : map (R := R) f (span {x}) ≤ r
this : Membership.mem (γ := Submodule R R) (comap f r) x
refine_1 : x ∈ (↑(comap f r) : Set R) ∧ t ⊆ (↑(comap f r) : Set R)
⊢ LE.le (α := Ideal R) (span (insert x t)) (comap f r)

Tactic:
rw [span_le, Set.insert_subset_iff]

Premises used: Ideal.span_le, Set.insert_subset_iff
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this_2 : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
r : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))
h : (fun (q : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) ↦ q.IsPrime ∧ map (R := R) f (span {x}) ≤ q) r
hrp : r ≤ map f p
hr : r.IsPrime
hxr : map (R := R) f (span {x}) ≤ r
this : Membership.mem (γ := Submodule R R) (comap f r) x
⊢ x ∈ (↑(comap f r) : Set R) ∧ t ⊆ (↑(comap f r) : Set R)

Tactic:
⟨this, span_le.mp (mk_ker.symm.trans_le (ker_le_comap _))⟩

Premises used: Ideal.span_le, Eq.trans_le, Ideal.ker_le_comap, And.intro, Iff.mp, Ideal.mk_ker, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this_2 : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
r : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))
h : (fun (q : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) ↦ q.IsPrime ∧ map (R := R) f (span {x}) ≤ q) r
hrp : r ≤ map f p
hr : r.IsPrime
hxr : map (R := R) f (span {x}) ≤ r
this : Membership.mem (γ := Submodule R R) (comap f r) x
⊢ x ∈ (↑(comap f r) : Set R) ∧ t ⊆ (↑(comap f r) : Set R)

Tactic:
exact ⟨this, span_le.mp (mk_ker.symm.trans_le (ker_le_comap _))⟩
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
r : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))
h : (fun (q : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) ↦ q.IsPrime ∧ map (R := R) f (span {x}) ≤ q) r
hrp : r ≤ map f p
hr : r.IsPrime
hxr : map (R := R) f (span {x}) ≤ r
rw : comap f (map f p)
| p

Tactic:
rw [← sup_eq_left.mpr hI'p, ← (span t).mk_ker, RingHom.ker_eq_comap_bot,
      ← comap_map_of_surjective f hf p]

Premises used: Iff.mpr, sup_eq_left, Ideal.comap_map_of_surjective, RingHom.ker_eq_comap_bot, Ideal.mk_ker
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
r : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))
h : (fun (q : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) ↦ q.IsPrime ∧ map (R := R) f (span {x}) ≤ q) r
hrp : r ≤ map f p
hr : r.IsPrime
hxr : map (R := R) f (span {x}) ≤ r
refine_2 : LE.le (α := Ideal R) (comap f r) (comap f (map f p))
⊢ comap f r ≤ p

Tactic:
conv_rhs => rw [← sup_eq_left.mpr hI'p, ← (span t).mk_ker, RingHom.ker_eq_comap_bot,
      ← comap_map_of_surjective f hf p]

Premises used: Iff.mpr, sup_eq_left, Ideal.comap_map_of_surjective, RingHom.ker_eq_comap_bot, Ideal.mk_ker
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
r : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))
h : (fun (q : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) ↦ q.IsPrime ∧ map (R := R) f (span {x}) ≤ q) r
hrp : r ≤ map f p
hr : r.IsPrime
hxr : map (R := R) f (span {x}) ≤ r
⊢ LE.le (α := Ideal R) (comap f r) (comap f (map f p))

Tactic:
comap_mono hrp

Premises used: Set.Mem, Ideal.comap_mono
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
r : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))
h : (fun (q : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) ↦ q.IsPrime ∧ map (R := R) f (span {x}) ≤ q) r
hrp : r ≤ map f p
hr : r.IsPrime
hxr : map (R := R) f (span {x}) ≤ r
⊢ LE.le (α := Ideal R) (comap f r) (comap f (map f p))

Tactic:
exact comap_mono hrp

Premises used: Ideal.comap_mono
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I p : Ideal R
hp : p ∈ I.minimalPrimes
rw : ∀ (i : { s : Finset R // Submodule.span R (↑s : Set R) = I }), p.height ≤ (↑(↑i : Finset R).card : ℕ∞)
⊢ p.height ≤ (Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I)

Tactic:
rw [I.spanRank_toENat_eq_iInf_finset_card, le_iInf_iff]

Premises used: le_iInf_iff, Submodule.spanRank_toENat_eq_iInf_finset_card
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
n : ℕ
H :
  ∀ m < n,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
      (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
      p.height ≤ (↑m : ℕ∞)
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
s : Finset R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
hn : s.card = n
⊢ s.card ≤ n

Tactic:
replace hn : s.card ≤ n := hn.le
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
n : ℕ
H :
  ∀ m < n,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
      (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
      p.height ≤ (↑m : ℕ∞)
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
s : Finset R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
hn : s.card ≤ n
⊢ p.IsPrime

Tactic:
have := hp.isPrime
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
s : Finset R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
this : p.IsPrime
H :
  ∀ m < 0,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
      (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
      p.height ≤ (↑m : ℕ∞)
hn : s.card ≤ 0
h : Membership.mem (γ := Set (Ideal R)) {p : Ideal R | IsMinimalPrime p} p
⊢ p.height ≤ (↑0 : ℕ∞)

Tactic:
rw [ENat.coe_zero, nonpos_iff_eq_zero, height_eq_zero_iff, minimalPrimes]

Premises used: Ideal.height_eq_zero_iff, minimalPrimes, ENat.coe_zero, nonpos_iff_eq_zero
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
s : Finset R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
this : p.IsPrime
H :
  ∀ m < 0,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
      (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
      p.height ≤ (↑m : ℕ∞)
hn : s.card ≤ 0
⊢ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | IsMinimalPrime p} p

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
s : Finset R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
this : p.IsPrime
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
      (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
      p.height ≤ (↑m : ℕ∞)
hn : s.card ≤ n + 1
h :
  ∀
    (this :
      ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
        (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (this : p.IsPrime)
        (n : ℕ)
        (H :
          ∀ m < n + 1,
            ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
              (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
              p.height ≤ (↑m : ℕ∞))
        (hn : s.card ≤ n + 1) (hR : ∃ (x : IsLocalRing R), p = maximalIdeal R), p.height ≤ (↑(n + 1) : ℕ∞))
    (hR : ¬∃ (x : IsLocalRing R), p = maximalIdeal R), p.height ≤ (↑(n + 1) : ℕ∞)
wlog :
  ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
    (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (this : p.IsPrime) (n : ℕ)
    (H :
      ∀ m < n + 1,
        ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
          (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
          p.height ≤ (↑m : ℕ∞))
    (hn : s.card ≤ n + 1) (hR : ∃ (x : IsLocalRing R), p = maximalIdeal R), p.height ≤ (↑(n + 1) : ℕ∞)
⊢ p.height ≤ (↑(n + 1) : ℕ∞)

Tactic:
wlog hR : ∃ (_ : IsLocalRing R), p = maximalIdeal R

Premises used: IsLocalRing
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
s : Finset R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
this_1 : p.IsPrime
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
      (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
      p.height ≤ (↑m : ℕ∞)
hn : s.card ≤ n + 1
this :
  ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
    (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (this : p.IsPrime) (n : ℕ)
    (H :
      ∀ m < n + 1,
        ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
          (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
          p.height ≤ (↑m : ℕ∞))
    (hn : s.card ≤ n + 1) (hR : ∃ (x : IsLocalRing R), p = maximalIdeal R), p.height ≤ (↑(n + 1) : ℕ∞)
hR : ¬∃ (x : IsLocalRing R), p = maximalIdeal R
h :
  ∀
    (hp :
      Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R)))
        (under R (B := Localization (M := R) p.primeCompl) (maximalIdeal (Localization (M := R) p.primeCompl))))
    (n : ℕ)
    (H :
      ∀ m < n + 1,
        ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
          (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
          p.height ≤ (↑m : ℕ∞))
    (hn : s.card ≤ n + 1)
    (this :
      ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
        (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (this : p.IsPrime)
        (n : ℕ)
        (H :
          ∀ m < n + 1,
            ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
              (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
              p.height ≤ (↑m : ℕ∞))
        (hn : s.card ≤ n + 1) (hR : ∃ (x : IsLocalRing R), p = maximalIdeal R), p.height ≤ (↑(n + 1) : ℕ∞))
    (hR : ¬∃ (x : IsLocalRing R), p = maximalIdeal R),
    height (under R (B := Localization (M := R) p.primeCompl) (maximalIdeal (Localization (M := R) p.primeCompl))) ≤
      (↑(n + 1) : ℕ∞)
⊢ p.height ≤ (↑(n + 1) : ℕ∞)

Tactic:
rw [← Localization.AtPrime.under_maximalIdeal (I := p)] at hp ⊢

Premises used: Localization.AtPrime.under_maximalIdeal
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
s : Finset R
this_1 : p.IsPrime
hp :
  Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R)))
    (under R (B := Localization (M := R) p.primeCompl) (maximalIdeal (Localization (M := R) p.primeCompl)))
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
      (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
      p.height ≤ (↑m : ℕ∞)
hn : s.card ≤ n + 1
this :
  ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
    (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (this : p.IsPrime) (n : ℕ)
    (H :
      ∀ m < n + 1,
        ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
          (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
          p.height ≤ (↑m : ℕ∞))
    (hn : s.card ≤ n + 1) (hR : ∃ (x : IsLocalRing R), p = maximalIdeal R), p.height ≤ (↑(n + 1) : ℕ∞)
hR : ¬∃ (x : IsLocalRing R), p = maximalIdeal R
h :
  height.{u_1} (R := Localization (M := R) p.primeCompl) (maximalIdeal (Localization (M := R) p.primeCompl)) ≤
    (↑(n + 1) : ℕ∞)
⊢ height (under R (B := Localization (M := R) p.primeCompl) (maximalIdeal (Localization (M := R) p.primeCompl))) ≤
    (↑(n + 1) : ℕ∞)

Tactic:
rw [IsLocalization.height_under p.primeCompl]

Premises used: IsLocalization.height_under, Ideal.primeCompl
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
s : Finset R
this_1 : p.IsPrime
hp :
  Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R)))
    (under R (B := Localization (M := R) p.primeCompl) (maximalIdeal (Localization (M := R) p.primeCompl)))
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
      (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
      p.height ≤ (↑m : ℕ∞)
hn : s.card ≤ n + 1
this :
  ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
    (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (this : p.IsPrime) (n : ℕ)
    (H :
      ∀ m < n + 1,
        ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
          (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
          p.height ≤ (↑m : ℕ∞))
    (hn : s.card ≤ n + 1) (hR : ∃ (x : IsLocalRing R), p = maximalIdeal R), p.height ≤ (↑(n + 1) : ℕ∞)
hR : ¬∃ (x : IsLocalRing R), p = maximalIdeal R
h :
  ∀
    (hp :
      Membership.mem (γ := Set (Ideal (Localization (M := R) p.primeCompl)))
        (Ideal.minimalPrimes
          (span
            ((⇑(algebraMap R (Localization (M := R) p.primeCompl)) : (a : R) → Localization p.primeCompl) ''
              (↑s : Set R))))
        (maximalIdeal (Localization (M := R) p.primeCompl)))
    (n : ℕ)
    (H :
      ∀ m < n + 1,
        ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
          (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
          p.height ≤ (↑m : ℕ∞))
    (hn : s.card ≤ n + 1)
    (this :
      ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
        (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (this : p.IsPrime)
        (n : ℕ)
        (H :
          ∀ m < n + 1,
            ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
              (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
              p.height ≤ (↑m : ℕ∞))
        (hn : s.card ≤ n + 1) (hR : ∃ (x : IsLocalRing R), p = maximalIdeal R), p.height ≤ (↑(n + 1) : ℕ∞))
    (hR : ¬∃ (x : IsLocalRing R), p = maximalIdeal R),
    height.{u_1} (R := Localization (M := R) p.primeCompl) (maximalIdeal (Localization (M := R) p.primeCompl)) ≤
      (↑(n + 1) : ℕ∞)
⊢ height.{u_1} (R := Localization (M := R) p.primeCompl) (maximalIdeal (Localization (M := R) p.primeCompl)) ≤
    (↑(n + 1) : ℕ∞)

Tactic:
rw [← Set.mem_preimage, ← IsLocalization.minimalPrimes_map p.primeCompl, map_span] at hp

Premises used: IsLocalization.minimalPrimes_map, Ideal.map_span, Ideal.primeCompl, Set.mem_preimage
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
s : Finset R
this_1 : p.IsPrime
hp :
  Membership.mem (γ := Set (Ideal (Localization (M := R) p.primeCompl)))
    (Ideal.minimalPrimes
      (span
        ((⇑(algebraMap R (Localization (M := R) p.primeCompl)) : (a : R) → Localization p.primeCompl) '' (↑s : Set R))))
    (maximalIdeal (Localization (M := R) p.primeCompl))
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
      (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
      p.height ≤ (↑m : ℕ∞)
hn : s.card ≤ n + 1
this :
  ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
    (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (this : p.IsPrime) (n : ℕ)
    (H :
      ∀ m < n + 1,
        ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
          (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
          p.height ≤ (↑m : ℕ∞))
    (hn : s.card ≤ n + 1) (hR : ∃ (x : IsLocalRing R), p = maximalIdeal R), p.height ≤ (↑(n + 1) : ℕ∞)
hR : ¬∃ (x : IsLocalRing R), p = maximalIdeal R
⊢ Membership.mem (γ := Set (Ideal (Localization (M := R) p.primeCompl)))
    (Ideal.minimalPrimes
      (span
        (↑(Finset.image (⇑(algebraMap R (Localization (M := R) p.primeCompl)) : (a : R) → Localization p.primeCompl)
              s) :
          Set (Localization p.primeCompl))))
    (maximalIdeal (Localization (M := R) p.primeCompl))

Tactic:
simpa using hp
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
s : Finset R
this_1 : p.IsPrime
hp :
  Membership.mem (γ := Set (Ideal (Localization (M := R) p.primeCompl)))
    (Ideal.minimalPrimes
      (span
        ((⇑(algebraMap R (Localization (M := R) p.primeCompl)) : (a : R) → Localization p.primeCompl) '' (↑s : Set R))))
    (maximalIdeal (Localization (M := R) p.primeCompl))
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
      (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
      p.height ≤ (↑m : ℕ∞)
hn : s.card ≤ n + 1
this :
  ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
    (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (this : p.IsPrime) (n : ℕ)
    (H :
      ∀ m < n + 1,
        ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
          (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
          p.height ≤ (↑m : ℕ∞))
    (hn : s.card ≤ n + 1) (hR : ∃ (x : IsLocalRing R), p = maximalIdeal R), p.height ≤ (↑(n + 1) : ℕ∞)
hR : ¬∃ (x : IsLocalRing R), p = maximalIdeal R
⊢ height.{u_1} (R := Localization (M := R) p.primeCompl) (maximalIdeal (Localization (M := R) p.primeCompl)) ≤
    (↑(n + 1) : ℕ∞)

Tactic:
exact this _ (s.image (algebraMap R (Localization p.primeCompl))) (by simpa using hp)
          inferInstance _ H (Finset.card_image_le.trans hn) ⟨inferInstance, rfl⟩

Premises used: Algebra.algebraMap, inferInstance, Localization, Finset.card_image_le, Exists.intro, Ideal.primeCompl, LE.le.trans, DFunLike.coe, Finset.image, rfl