-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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)
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)
obtain₂ :
  ∀ (s : Finset R) (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p)
    (heq : (↑s.card : ℕ∞) = p.height),
    let 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),
      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)
have obtain₃ : ∀ (s : Finset R) (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p)
  (heq : (↑s.card : ℕ∞) = p.height),
  let 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))),
    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: classical
  obtain ⟨s, hp, heq⟩ := p.exists_finset_card_eq_height_of_isNoetherianRing
  let P' := P.map (Ideal.Quotient.mk <| p.map (algebraMap R S))
  obtain ⟨s', hP', heq'⟩ := P'.exists_finset_card_eq_height_of_isNoetherianRing
  have hsP'sub : (s' : Set <| S ⧸ (Ideal.map (algebraMap R S) p)) ⊆ (P' : Set <| S ⧸ _) :=
    fun x hx ↦ hP'.le (Ideal.subset_span hx)
  have : Set.SurjOn (Ideal.Quotient.mk (p.map (algebraMap R S))) P s' := by
    refine Set.SurjOn.mono subset_rfl hsP'sub fun x hx ↦ ?_
    obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective x
    rw [SetLike.mem_coe, Ideal.mem_quotient_iff_mem] at hx
    · use y, hx
    · rw [Ideal.map_le_iff_le_comap, Ideal.LiesOver.over (p := p) (P := P)]
  obtain ⟨o, ho, hinj, himgo⟩ := s'.exists_subset_injOn_image_eq_of_surjOn (P : Set S) this
  let t : Finset S := Finset.image (algebraMap R S) s ∪ o
  suffices h : P.height ≤ t.card by
    rw [← heq, ← heq']
    apply le_trans h
    norm_cast
    refine le_trans (Finset.card_union_le _ _) (add_le_add Finset.card_image_le ?_)
    rw [← himgo, Finset.card_image_of_injOn hinj]
  refine Ideal.height_le_card_of_mem_minimalPrimes_span_finset ?_
  have : Ideal.span t = Ideal.map (algebraMap R S) (.span s) ⊔ .span o := by
    simp [t, Ideal.map_span]
  refine this ▸ map_sup_mem_minimalPrimes_of_map_quotientMk_mem_minimalPrimes hp (span_le.mpr ho) ?_
  convert! hP'
  simp [Ideal.map_span, ← himgo]