-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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) : ℕ∞)
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) : ℕ∞)
let₈ 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) (hI : I.FG),
    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))) (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) (hI : I.FG),
    let t := o ∪ ⋯.toFinset (s := Submodule.generators I);
    p.height ≤ (↑t.card : ℕ∞)
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) (hI : I.FG),
    let t := o ∪ ⋯.toFinset (s := Submodule.generators I);
    Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑t : Set R))) p
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) (hI : I.FG),
    p ∈ (I ⊔ span (↑o : Set R)).minimalPrimes
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) (hI : I.FG),
    Membership.mem (γ := Set (Ideal (R ⧸ I)))
      (Ideal.minimalPrimes (map (F := R →+* R ⧸ I) (Quotient.mk I) (span (↑o : Set R))))
      (map (F := R →+* R ⧸ I) (Quotient.mk I) p)
h :
  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) (hI : I.FG),
    Quotient.commSemiring I = CommRing.toCommSemiring →
      Eq (α := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) (span (↑o : Set R))) (span (↑s : Set (R ⧸ I)))
⊢ 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]

Premises used: Ideal.map_span, Ideal.mem_minimalPrimes_sup, Set.Finite.coe_toFinset, sup_comm, Ideal.span, Ideal.span_union, Ideal.height_le_card_of_mem_minimalPrimes_span_finset, Submodule.span_generators, Finset.coe_union