awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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))
y : S
hx :
  Membership.mem (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) 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))
hIJ : p ≤ comap (F := R →+* S) (algebraMap R S) P
⊢ map (F := R →+* S) (algebraMap R S) p ≤ P
have hIJ₁ : LE.le (α := Ideal R) (under R P) (under R P)
Tactic: rw [Ideal.map_le_iff_le_comap, Ideal.LiesOver.over (p := p) (P := P)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
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))
⊢ 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 this : 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: 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)]
-- 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
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))
this :
  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))
⊢ 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 : ∀ (o : Finset S) (ho : (↑o : Set S) ⊆ (↑P : Set S))
  (hinj :
    Set.InjOn (β := 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) (↑o : Set S))
  (himgo :
    Finset.image (⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) o =
      s'),
  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 ⟨o, ho, hinj, himgo⟩ := s'.exists_subset_injOn_image_eq_of_surjOn (P : Set S) this
-- 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
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))
this :
  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))
o : Finset S
ho : (↑o : Set S) ⊆ (↑P : Set S)
hinj :
  Set.InjOn (β := 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) (↑o : Set S)
himgo :
  Finset.image (⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) o = s'
t : Finset S := Finset.image (⇑(algebraMap R S) : (a : R) → S) s ∪ o
h : P.height ≤ (↑t.card : ℕ∞)
⊢ 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 rw : P.height ≤ HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) (↑s'.card : ℕ∞)
Tactic: rw [← heq, ← heq']
-- 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
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))
this :
  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))
o : Finset S
ho : (↑o : Set S) ⊆ (↑P : Set S)
hinj :
  Set.InjOn (β := 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) (↑o : Set S)
himgo :
  Finset.image (⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) o = s'
t : Finset S := Finset.image (⇑(algebraMap R S) : (a : R) → S) s ∪ o
h : P.height ≤ (↑t.card : ℕ∞)
⊢ P.height ≤ HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) (↑s'.card : ℕ∞)
have apply : (↑t.card : ℕ∞) ≤ HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) (↑s'.card : ℕ∞)
Tactic: apply le_trans h
-- 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
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))
this :
  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))
o : Finset S
ho : (↑o : Set S) ⊆ (↑P : Set S)
hinj :
  Set.InjOn (β := 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) (↑o : Set S)
himgo :
  Finset.image (⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) o = s'
t : Finset S := Finset.image (⇑(algebraMap R S) : (a : R) → S) s ∪ o
h : P.height ≤ (↑t.card : ℕ∞)
⊢ (↑t.card : ℕ∞) ≤ HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) (↑s'.card : ℕ∞)
have norm_cast : t.card ≤ s.card + s'.card
Tactic: norm_cast
-- 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
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))
this :
  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))
o : Finset S
ho : (↑o : Set S) ⊆ (↑P : Set S)
hinj :
  Set.InjOn (β := 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) (↑o : Set S)
himgo :
  Finset.image (⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) o = s'
t : Finset S := Finset.image (⇑(algebraMap R S) : (a : R) → S) s ∪ o
h : P.height ≤ (↑t.card : ℕ∞)
⊢ t.card ≤ s.card + s'.card
have refine : o.card ≤ s'.card
Tactic: refine le_trans (Finset.card_union_le _ _) (add_le_add Finset.card_image_le ?_)
-- 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
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))
this :
  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))
o : Finset S
ho : (↑o : Set S) ⊆ (↑P : Set S)
hinj :
  Set.InjOn (β := 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) (↑o : Set S)
himgo :
  Finset.image (⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) o = s'
t : Finset S := Finset.image (⇑(algebraMap R S) : (a : R) → S) s ∪ o
h : P.height ≤ (↑t.card : ℕ∞)
⊢ o.card ≤ s'.card
have rw : o.card ≤
  Finset.card (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    (Finset.image (⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) o)
Tactic: rw [← himgo, Finset.card_image_of_injOn hinj]
-- 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
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))
this :
  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))
o : Finset S
ho : (↑o : Set S) ⊆ (↑P : Set S)
hinj :
  Set.InjOn (β := 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) (↑o : Set S)
himgo :
  Finset.image (⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) o = s'
t : Finset S := Finset.image (⇑(algebraMap R S) : (a : R) → S) s ∪ o
h : P.height ≤ (↑t.card : ℕ∞)
rw :
  o.card ≤
    Finset.card (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
      (Finset.image (⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) o)
⊢ o.card ≤ s'.card
have rw₁ : o.card ≤ o.card
Tactic: rw [← himgo, Finset.card_image_of_injOn hinj]
-- 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
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))
this :
  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))
o : Finset S
ho : (↑o : Set S) ⊆ (↑P : Set S)
hinj :
  Set.InjOn (β := 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) (↑o : Set S)
himgo :
  Finset.image (⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) o = s'
t : Finset S := Finset.image (⇑(algebraMap R S) : (a : R) → S) s ∪ o
⊢ 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 suffices : P.height ≤ (↑t.card : ℕ∞)
Tactic: 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]
-- 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
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))
this :
  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))
o : Finset S
ho : (↑o : Set S) ⊆ (↑P : Set S)
hinj :
  Set.InjOn (β := 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) (↑o : Set S)
himgo :
  Finset.image (⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) o = s'
t : Finset S := Finset.image (⇑(algebraMap R S) : (a : R) → S) s ∪ o
⊢ P.height ≤ (↑t.card : ℕ∞)
have refine : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes (span (↑t : Set S))) P
Tactic: refine Ideal.height_le_card_of_mem_minimalPrimes_span_finset ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
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))
this :
  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))
o : Finset S
ho : (↑o : Set S) ⊆ (↑P : Set S)
hinj :
  Set.InjOn (β := 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) (↑o : Set S)
himgo :
  Finset.image (⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) o = s'
t : Finset S := Finset.image (⇑(algebraMap R S) : (a : R) → S) s ∪ o
⊢ Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes (span (↑t : Set S))) P
have this₁ : Eq (α := Ideal S) (span (↑t : Set S)) (map (F := R →+* S) (algebraMap R S) (span (↑s : Set R)) ⊔ span (↑o : Set S))
Tactic: have : Ideal.span t = Ideal.map (algebraMap R S) (.span s) ⊔ .span o := by
    simp [t, Ideal.map_span]