awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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
suffices : 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)

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]
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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 : ℕ∞)

Tactic:
Ideal.height_le_card_of_mem_minimalPrimes_span_finset ?_

Premises used: Ideal.height_le_card_of_mem_minimalPrimes_span_finset
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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
refine : Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes (span (↑t : Set S))) P
⊢ P.height ≤ (↑t.card : ℕ∞)

Tactic:
refine Ideal.height_le_card_of_mem_minimalPrimes_span_finset ?_

Premises used: Ideal.height_le_card_of_mem_minimalPrimes_span_finset
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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
⊢ Eq (α := Ideal S) (span (↑t : Set S)) (map (F := R →+* S) (algebraMap R S) (span (↑s : Set R)) ⊔ span (↑o : Set S))

Tactic:
simp [t, Ideal.map_span]

Premises used: Ideal.map_span
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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
⊢ 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]
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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_1 :
  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
this :
  Eq (α := Ideal S) (span (↑t : Set S)) (map (F := R →+* S) (algebraMap R S) (span (↑s : Set R)) ⊔ span (↑o : Set S))
⊢ Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes (span (↑t : Set S))) P

Tactic:
this ▸ map_sup_mem_minimalPrimes_of_map_quotientMk_mem_minimalPrimes hp (span_le.mpr ho) ?_

Premises used: Ideal.span_le, Iff.mpr, Ideal.map_sup_mem_minimalPrimes_of_map_quotientMk_mem_minimalPrimes, Eq.rec, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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_1 :
  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
this :
  Eq (α := Ideal S) (span (↑t : Set S)) (map (F := R →+* S) (algebraMap R S) (span (↑s : Set R)) ⊔ span (↑o : Set S))
refine :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes
      (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)) (span (↑o : Set S))))
    (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)
⊢ Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes (span (↑t : Set S))) P

Tactic:
refine this ▸ map_sup_mem_minimalPrimes_of_map_quotientMk_mem_minimalPrimes hp (span_le.mpr ho) ?_
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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_1 :
  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
this :
  Eq (α := Ideal S) (span (↑t : Set S)) (map (F := R →+* S) (algebraMap R S) (span (↑s : Set R)) ⊔ span (↑o : Set S))
⊢ 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'

Tactic:
hP'
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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_1 :
  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
this :
  Eq (α := Ideal S) (span (↑t : Set S)) (map (F := R →+* S) (algebraMap R S) (span (↑s : Set R)) ⊔ span (↑o : Set S))
h :
  Eq.{u_2 + 1} (α := CommSemiring (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)))
      (Quotient.commSemiring (map (F := R →+* S) (algebraMap R S) p)) CommRing.toCommSemiring →
    Eq (α := 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)) (span (↑o : Set S)))
      (span (↑s' : Set (S ⧸ map (algebraMap R S) p)))
⊢ Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes
      (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)) (span (↑o : Set S))))
    (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:
convert! hP'
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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_1 :
  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
this :
  Eq (α := Ideal S) (span (↑t : Set S)) (map (F := R →+* S) (algebraMap R S) (span (↑s : Set R)) ⊔ span (↑o : Set S))
e_2 :
  Eq.{u_2 + 1} (α := CommSemiring (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)))
    (Quotient.commSemiring (map (F := R →+* S) (algebraMap R S) p)) CommRing.toCommSemiring
⊢ Eq (α := 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)) (span (↑o : Set S)))
    (span (↑s' : Set (S ⧸ map (algebraMap R S) p)))

Tactic:
simp [Ideal.map_span, ← himgo]

Premises used: Ideal.map_span
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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
inst_5 : Algebra.HasGoingDown R S
p : Ideal R
inst_6 : p.IsPrime
P : Ideal S
inst_7 : P.IsPrime
inst_8 : P.LiesOver 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:
le_antisymm (height_le_height_add_of_liesOver p P) ?_

Premises used: Ideal.height_le_height_add_of_liesOver, le_antisymm
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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
inst_5 : Algebra.HasGoingDown R S
p : Ideal R
inst_6 : p.IsPrime
P : Ideal S
inst_7 : P.IsPrime
inst_8 : P.LiesOver p
refine :
  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 =
    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:
refine le_antisymm (height_le_height_add_of_liesOver p P) ?_

Premises used: Ideal.height_le_height_add_of_liesOver, le_antisymm