-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I p : Ideal R
inst_2 : p.IsPrime
hrp : I ≤ p
let let₁ let₂ :
  p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
let₃ :
  let p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p;
  ∀ (this : p'.IsPrime),
    p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
let₄ :
  let p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p;
  ∀ (this : p'.IsPrime) (s : Finset (R ⧸ I))
    (hps : Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (span (↑s : Set (R ⧸ I)))) p')
    (hs : (↑s.card : ℕ∞) = p'.height),
    p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
let₅ :
  let p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p;
  ∀ (this : p'.IsPrime) (s : Finset (R ⧸ I))
    (hps : Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (span (↑s : Set (R ⧸ I)))) p')
    (hs : (↑s.card : ℕ∞) = p'.height) (hsp' : (↑s : Set (R ⧸ I)) ⊆ (↑p' : Set (R ⧸ I))),
    p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
let₆ :
  let p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p;
  ∀ (this : p'.IsPrime) (s : Finset (R ⧸ I))
    (hps : Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (span (↑s : Set (R ⧸ I)))) p')
    (hs : (↑s.card : ℕ∞) = p'.height) (hsp' : (↑s : Set (R ⧸ I)) ⊆ (↑p' : Set (R ⧸ I)))
    (this : Set.SurjOn (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑p : Set R) (↑s : Set (R ⧸ I))),
    p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
⊢ p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
have let₇ : let p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p;
∀ (this : p'.IsPrime) (s : Finset (R ⧸ I))
  (hps : Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (span (↑s : Set (R ⧸ I)))) p')
  (hs : (↑s.card : ℕ∞) = p'.height) (hsp' : (↑s : Set (R ⧸ I)) ⊆ (↑p' : Set (R ⧸ I)))
  (this : Set.SurjOn (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑p : Set R) (↑s : Set (R ⧸ I))) (o : Finset R)
  (hsubset : (↑o : Set R) ⊆ (↑p : Set R))
  (ho : Set.InjOn (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑o : Set R))
  (himgo : Finset.image (⇑(Quotient.mk I) : (a : R) → R ⧸ I) o = s),
  p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
Tactic: classical
  let p' := p.map (algebraMap R (R ⧸ I))
  have : p'.IsPrime := isPrime_map_quotientMk_of_isPrime hrp
  obtain ⟨s, hps, hs⟩ := exists_finset_card_eq_height_of_isNoetherianRing p'
  have hsp' : (s : Set (R ⧸ I)) ⊆ (p' : Set _) := fun _ hx ↦ hps.le (subset_span hx)
  have : Set.SurjOn (Ideal.Quotient.mk I) p s := by
    refine Set.SurjOn.mono subset_rfl hsp' fun x hx ↦ ?_
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    exact ⟨x, by simpa [hrp, sup_of_le_left, p'] using hx⟩
  obtain ⟨o, hsubset, ho, himgo⟩ := s.exists_subset_injOn_image_eq_of_surjOn (p : Set R) this
  have hI : I.FG := IsNoetherian.noetherian I
  let t : Finset R := o ∪ (Submodule.FG.finite_generators hI).toFinset
  suffices h : p.height ≤ t.card by
    refine le_trans h (hs ▸ ?_)
    norm_cast
    have : (Submodule.FG.finite_generators hI).toFinset.card = I.spanFinrank := by
      rw [← Set.ncard_eq_toFinset_card (hs := Submodule.FG.finite_generators hI)]
      exact Submodule.FG.generators_ncard hI
    grind
  refine Ideal.height_le_card_of_mem_minimalPrimes_span_finset ?_
  rw [Finset.coe_union, Set.Finite.coe_toFinset, span_union, sup_comm, span,
    Submodule.span_generators]
  refine Ideal.mem_minimalPrimes_sup hrp ?_
  convert! hps
  simp [Ideal.map_span, ← himgo]