awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
n : ℕ
inst_1 : p.IsPrime
a :
  ∀ (a : Ideal R) (a_1 : a.IsPrime),
    (Equiv.symm
                (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                  fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
              (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
            (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a a_1) <
          { asIdeal := p, isPrime := inst_1 : PrimeSpectrum R } →
        Order.height (α := PrimeSpectrum R)
            ((Equiv.symm
                    (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                      fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
                  (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
                (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a a_1) :
              PrimeSpectrum R) <
          (↑n : ℕ∞) ↔
      a < p → a.height < (↑n : ℕ∞)
⊢ (∀ (a : Ideal R) (b : a.IsPrime),
      (Equiv.symm
                (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                  fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
              (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
            (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a b) <
          { asIdeal := p, isPrime := inst_1 : PrimeSpectrum R } →
        Order.height (α := PrimeSpectrum R)
            ((Equiv.symm
                    (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                      fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
                  (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
                (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a b) :
              PrimeSpectrum R) <
          (↑n : ℕ∞)) ↔
    ∀ (q : Ideal R), q.IsPrime → q < p → q.height < (↑n : ℕ∞)

Tactic:
congr!
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
n : ℕ
inst_1 : p.IsPrime
a_1 : Ideal R
h : a_1.IsPrime
a :
  (Equiv.symm
              (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
            (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
          (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a_1 h) <
        { asIdeal := p, isPrime := inst_1 : PrimeSpectrum R } →
      Order.height (α := PrimeSpectrum R)
          ((Equiv.symm
                  (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
                (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
              (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a_1 h) :
            PrimeSpectrum R) <
        (↑n : ℕ∞) ↔
    a_1 < p → Order.height { asIdeal := a_1, isPrime := h : PrimeSpectrum R } < (↑n : ℕ∞)
⊢ (Equiv.symm
              (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
            (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
          (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a_1 h) <
        { asIdeal := p, isPrime := inst_1 : PrimeSpectrum R } →
      Order.height (α := PrimeSpectrum R)
          ((Equiv.symm
                  (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
                (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
              (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a_1 h) :
            PrimeSpectrum R) <
        (↑n : ℕ∞) ↔
    a_1 < p → a_1.height < (↑n : ℕ∞)

Tactic:
rw [height_eq_primeHeight, primeHeight]

Premises used: _private.0.Ideal.primeHeight, _private.0.Ideal.height_eq_primeHeight
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
n : ℕ
inst_1 : p.IsPrime
a : Ideal R
h : a.IsPrime
⊢ (Equiv.symm
              (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
            (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
          (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a h) <
        { asIdeal := p, isPrime := inst_1 : PrimeSpectrum R } →
      Order.height (α := PrimeSpectrum R)
          ((Equiv.symm
                  (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
                (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
              (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a h) :
            PrimeSpectrum R) <
        (↑n : ℕ∞) ↔
    a < p → Order.height { asIdeal := a, isPrime := h : PrimeSpectrum R } < (↑n : ℕ∞)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
n : ℕ
inst_1 : p.IsPrime
inst_2 : IsNoetherianRing R
rw :
  (∀ (q : Ideal R), q.IsPrime → q < p → q.height < (↑n : ℕ∞)) ↔
    ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < (↑n : ℕ∞)
⊢ p.height ≤ (↑n : ℕ∞) ↔
    ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < (↑n : ℕ∞)

Tactic:
rw [Ideal.height_le_iff]

Premises used: Ideal.height_le_iff
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
n : ℕ
inst_1 : p.IsPrime
inst_2 : IsNoetherianRing R
mp :
  (∀ (q : Ideal R), q.IsPrime → q < p → q.height < (↑n : ℕ∞)) →
    ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < (↑n : ℕ∞)
mpr :
  (∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < (↑n : ℕ∞)) →
    ∀ (q : Ideal R), q.IsPrime → q < p → q.height < (↑n : ℕ∞)
⊢ (∀ (q : Ideal R), q.IsPrime → q < p → q.height < (↑n : ℕ∞)) ↔
    ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < (↑n : ℕ∞)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
n : ℕ
inst_1 : p.IsPrime
inst_2 : IsNoetherianRing R
H : ∀ (q : Ideal R), q.IsPrime → q < p → q.height < (↑n : ℕ∞)
q : Ideal R
hq : q.IsPrime
e : q < p
mp : (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < (↑n : ℕ∞)
⊢ (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < (↑n : ℕ∞)

Tactic:
_
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
n : ℕ
inst_1 : p.IsPrime
inst_2 : IsNoetherianRing R
H : ∀ (q : Ideal R), q.IsPrime → q < p → q.height < (↑n : ℕ∞)
q : Ideal R
hq : q.IsPrime
e : q < p
h : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p
⊢ q.height < (↑n : ℕ∞)

Tactic:
H q hq e
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
n : ℕ
inst_1 : p.IsPrime
inst_2 : IsNoetherianRing R
H : ∀ (q : Ideal R), q.IsPrime → q < p → q.height < (↑n : ℕ∞)
q : Ideal R
hq : q.IsPrime
e : q < p
h : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p
⊢ q.height < (↑n : ℕ∞)

Tactic:
exact H q hq e
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
n : ℕ
inst_1 : p.IsPrime
inst_2 : IsNoetherianRing R
H : ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < (↑n : ℕ∞)
q : Ideal R
hq : q.IsPrime
e : q < p
mpr :
  ∀ (x : Ideal R) (hx : x.IsPrime)
    (hqx : Subtype.mk (p := fun (I : Ideal R) ↦ I.IsPrime) q hq ≤ Subtype.mk (p := fun (I : Ideal R) ↦ I.IsPrime) x hx)
    (hxp :
      Subtype.mk (p := fun (I : Ideal R) ↦ I.IsPrime) x hx ⋖ Subtype.mk (p := fun (I : Ideal R) ↦ I.IsPrime) p inst_1),
    q.height < (↑n : ℕ∞)
⊢ q.height < (↑n : ℕ∞)

Tactic:
obtain ⟨⟨x, hx⟩, hqx, hxp⟩ :=
      @exists_le_covBy_of_lt { I : Ideal R // I.IsPrime } ⟨q, hq⟩ ⟨p, ‹_›⟩ _ _ e

Premises used: exists_le_covBy_of_lt
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
n : ℕ
inst_1 : p.IsPrime
inst_2 : IsNoetherianRing R
H : ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < (↑n : ℕ∞)
q : Ideal R
hq : q.IsPrime
e : q < p
x : Ideal R
hx : x.IsPrime
hqx : Subtype.mk (p := fun (I : Ideal R) ↦ I.IsPrime) q hq ≤ Subtype.mk (p := fun (I : Ideal R) ↦ I.IsPrime) x hx
hxp : Subtype.mk (p := fun (I : Ideal R) ↦ I.IsPrime) x hx ⋖ Subtype.mk (p := fun (I : Ideal R) ↦ I.IsPrime) p inst_1
⊢ q.height < (↑n : ℕ∞)

Tactic:
(Ideal.height_mono hqx).trans_lt
      (H _ hx hxp.1 (fun I hI e ↦ hxp.2 (show Subtype.mk x hx < ⟨I, hI⟩ from e)))

Premises used: Ideal.height_mono, And.right, And.left, LE.le.trans_lt
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
n : ℕ
inst_1 : p.IsPrime
inst_2 : IsNoetherianRing R
H : ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < (↑n : ℕ∞)
q : Ideal R
hq : q.IsPrime
e : q < p
x : Ideal R
hx : x.IsPrime
hqx : Subtype.mk (p := fun (I : Ideal R) ↦ I.IsPrime) q hq ≤ Subtype.mk (p := fun (I : Ideal R) ↦ I.IsPrime) x hx
hxp : Subtype.mk (p := fun (I : Ideal R) ↦ I.IsPrime) x hx ⋖ Subtype.mk (p := fun (I : Ideal R) ↦ I.IsPrime) p inst_1
⊢ q.height < (↑n : ℕ∞)

Tactic:
exact (Ideal.height_mono hqx).trans_lt
      (H _ hx hxp.1 (fun I hI e ↦ hxp.2 (show Subtype.mk x hx < ⟨I, hI⟩ from e)))

Premises used: Ideal.height_mono, And.right, And.left, LE.le.trans_lt
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
e : R ≃+* S
p : Ideal S
inst_2 : p.IsPrime
rw :
  Order.height (α := PrimeSpectrum R) { asIdeal := comap e p, isPrime := ⋯ : PrimeSpectrum R } =
    Order.height.{u_1} (α := PrimeSpectrum R)
      ((PrimeSpectrum.comapEquiv e.symm : (a : PrimeSpectrum S) → PrimeSpectrum R) { asIdeal := p, isPrime := inst_2 } :
        PrimeSpectrum R)
⊢ height (comap e p) = p.height

Tactic:
rw [height_eq_primeHeight, height_eq_primeHeight, primeHeight, primeHeight,
    ← Order.height_orderIso (PrimeSpectrum.comapEquiv e.symm) ⟨p, ‹_›⟩]

Premises used: _private.0.Ideal.primeHeight, PrimeSpectrum.mk, PrimeSpectrum.comapEquiv, Order.height_orderIso, RingEquiv.symm, _private.0.Ideal.height_eq_primeHeight
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
e : R ≃+* S
p : Ideal S
inst_2 : p.IsPrime
⊢ Eq (α := Ideal R) (map (F := S →+* R) (↑e.symm : S →+* R) p) (comap e.symm.symm p)

Tactic:
have := p.map_comap_of_equiv e.symm
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
e : R ≃+* S
p : Ideal S
inst_2 : p.IsPrime
this : Eq (α := Ideal R) (map (F := S →+* R) (↑e.symm : S →+* R) p) (comap e.symm.symm p)
⊢ Order.height (α := PrimeSpectrum R) { asIdeal := comap e p, isPrime := ⋯ : PrimeSpectrum R } =
    Order.height.{u_1} (α := PrimeSpectrum R)
      ((PrimeSpectrum.comapEquiv e.symm : (a : PrimeSpectrum S) → PrimeSpectrum R) { asIdeal := p, isPrime := inst_2 } :
        PrimeSpectrum R)

Tactic:
congr
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
e : R ≃+* S
I : Ideal S
⊢ height (comap e I) = I.height

Tactic:
(Equiv.iInf_congr e.idealComapOrderIso fun J ↦ (Equiv.iInf_congr ?_ fun h ↦ ?_).symm).symm

Premises used: Equiv.iInf_congr, Eq.symm, Ideal.height
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
e : R ≃+* S
I : Ideal S
refine_1 :
  (J : Ideal S) →
    J ∈ I.minimalPrimes ≃
      Membership.mem (α := Ideal R) (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap e I))
        (((↑e.idealComapOrderIso : Ideal S ≃ Ideal R) : (a : Ideal S) → Ideal R) J : Ideal R)
refine_2 :
  ∀ (J : Ideal S) (h : J ∈ I.minimalPrimes),
    primeHeight.{u_1} (R := R) (((↑e.idealComapOrderIso : Ideal S ≃ Ideal R) : (a : Ideal S) → Ideal R) J) =
      J.primeHeight
⊢ height (comap e I) = I.height

Tactic:
refine (Equiv.iInf_congr e.idealComapOrderIso fun J ↦ (Equiv.iInf_congr ?_ fun h ↦ ?_).symm).symm

Premises used: Equiv.iInf_congr, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
e : R ≃+* S
I J : Ideal S
refine_1 :
  J ∈ I.minimalPrimes ↔
    Membership.mem (α := Ideal R) (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap e I))
      (((↑e.idealComapOrderIso : Ideal S ≃ Ideal R) : (a : Ideal S) → Ideal R) J : Ideal R)
⊢ J ∈ I.minimalPrimes ≃
    Membership.mem (α := Ideal R) (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap e I))
      (((↑e.idealComapOrderIso : Ideal S ≃ Ideal R) : (a : Ideal S) → Ideal R) J : Ideal R)

Tactic:
refine .ofIff ?_
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
e : R ≃+* S
I J : Ideal S
refine_1 :
  J ∈ I.minimalPrimes ↔
    Membership.mem (α := Ideal R) (γ := Set (Ideal R)) (comap (F := R →+* S) (↑e : R →+* S) '' I.minimalPrimes)
      (((↑e.idealComapOrderIso : Ideal S ≃ Ideal R) : (a : Ideal S) → Ideal R) J : Ideal R)
⊢ J ∈ I.minimalPrimes ↔
    Membership.mem (α := Ideal R) (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap e I))
      (((↑e.idealComapOrderIso : Ideal S ≃ Ideal R) : (a : Ideal S) → Ideal R) J : Ideal R)

Tactic:
rw [← Ideal.comap_coe,
      Ideal.comap_minimalPrimes_eq_of_surjective (f := (↑e : R →+* S)) e.surjective]

Premises used: RingEquiv.surjective, Ideal.comap_minimalPrimes_eq_of_surjective, Ideal.comap_coe
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
e : R ≃+* S
I J : Ideal S
⊢ J ∈ I.minimalPrimes ↔
    Membership.mem (α := Ideal R) (γ := Set (Ideal R)) (comap (F := R →+* S) (↑e : R →+* S) '' I.minimalPrimes)
      (((↑e.idealComapOrderIso : Ideal S ≃ Ideal R) : (a : Ideal S) → Ideal R) J : Ideal R)

Tactic:
e.idealComapOrderIso.injective.mem_set_image.symm

Premises used: Set.Mem, RingEquiv.idealComapOrderIso, OrderIso.injective, Ideal.comap, Iff.symm, Function.Injective.mem_set_image
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
e : R ≃+* S
I J : Ideal S
⊢ J ∈ I.minimalPrimes ↔
    Membership.mem (α := Ideal R) (γ := Set (Ideal R)) (comap (F := R →+* S) (↑e : R →+* S) '' I.minimalPrimes)
      (((↑e.idealComapOrderIso : Ideal S ≃ Ideal R) : (a : Ideal S) → Ideal R) J : Ideal R)

Tactic:
exact e.idealComapOrderIso.injective.mem_set_image.symm

Premises used: RingEquiv.idealComapOrderIso, OrderIso.injective, Iff.symm, Function.Injective.mem_set_image
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
e : R ≃+* S
I J : Ideal S
h : J ∈ I.minimalPrimes
⊢ J.IsPrime

Tactic:
have : J.IsPrime := h.isPrime
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
e : R ≃+* S
I J : Ideal S
h : J ∈ I.minimalPrimes
this : J.IsPrime
⊢ primeHeight.{u_1} (R := R) (((↑e.idealComapOrderIso : Ideal S ≃ Ideal R) : (a : Ideal S) → Ideal R) J) = J.primeHeight

Tactic:
simp only [EquivLike.coe_coe, RingEquiv.idealComapOrderIso_apply,
      ← Ideal.height_eq_primeHeight, RingEquiv.height_comap_of_isPrime]

Premises used: RingEquiv.idealComapOrderIso_apply, _private.0.RingEquiv.height_comap_of_isPrime, EquivLike.coe_coe, _private.0.Ideal.height_eq_primeHeight
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
e : R ≃+* S
I : Ideal R
rw : height (comap e.symm I) = I.height
rw₁ rw₂ : I.height = I.height
⊢ height.{u_2} (R := S) (map e I) = I.height

Tactic:
rw [← Ideal.comap_symm e, height_comap]

Premises used: Ideal.comap_symm, RingEquiv.height_comap
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
rw :
  (∀ (i : PrimeSpectrum R), (↑(Order.height i) : WithBot ℕ∞) ≤ n) ↔
    ∀ ⦃p : Ideal R⦄, p.IsPrime → (↑p.height : WithBot ℕ∞) ≤ n
⊢ ringKrullDim R ≤ n ↔ ∀ ⦃p : Ideal R⦄, p.IsPrime → (↑p.height : WithBot ℕ∞) ≤ n

Tactic:
rw [ringKrullDim, Order.krullDim_eq_iSup_height, iSup_le_iff]

Premises used: Order.krullDim_eq_iSup_height, ringKrullDim, iSup_le_iff
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
⊢ (∀ (i : PrimeSpectrum R), (↑(Order.height i) : WithBot ℕ∞) ≤ n) ↔
    ∀ ⦃p : Ideal R⦄, p.IsPrime → (↑p.height : WithBot ℕ∞) ≤ n

Tactic:
⟨fun h p hp ↦ ?_, fun h p ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
refine_1 :
  ∀ (h : ∀ (i : PrimeSpectrum R), (↑(Order.height i) : WithBot ℕ∞) ≤ n) (p : Ideal R) (hp : p.IsPrime),
    (↑p.height : WithBot ℕ∞) ≤ n
refine_2 :
  ∀ (h : ∀ ⦃p : Ideal R⦄, p.IsPrime → (↑p.height : WithBot ℕ∞) ≤ n) (p : PrimeSpectrum R),
    (↑(Order.height p) : WithBot ℕ∞) ≤ n
⊢ (∀ (i : PrimeSpectrum R), (↑(Order.height i) : WithBot ℕ∞) ≤ n) ↔
    ∀ ⦃p : Ideal R⦄, p.IsPrime → (↑p.height : WithBot ℕ∞) ≤ n

Tactic:
refine ⟨fun h p hp ↦ ?_, fun h p ↦ ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
h : ∀ (i : PrimeSpectrum R), (↑(Order.height i) : WithBot ℕ∞) ≤ n
p : Ideal R
hp : p.IsPrime
refine_1 : (↑p.primeHeight : WithBot ℕ∞) ≤ n
⊢ (↑p.height : WithBot ℕ∞) ≤ n

Tactic:
rw [Ideal.height_eq_primeHeight]

Premises used: _private.0.Ideal.height_eq_primeHeight
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
h : ∀ (i : PrimeSpectrum R), (↑(Order.height i) : WithBot ℕ∞) ≤ n
p : Ideal R
hp : p.IsPrime
⊢ (↑p.primeHeight : WithBot ℕ∞) ≤ n

Tactic:
h ⟨p, hp⟩

Premises used: _private.0.Ideal.primeHeight, PrimeSpectrum.mk
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
h : ∀ (i : PrimeSpectrum R), (↑(Order.height i) : WithBot ℕ∞) ≤ n
p : Ideal R
hp : p.IsPrime
⊢ (↑p.primeHeight : WithBot ℕ∞) ≤ n

Tactic:
exact h ⟨p, hp⟩

Premises used: PrimeSpectrum.mk
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
h : ∀ ⦃p : Ideal R⦄, p.IsPrime → (↑p.height : WithBot ℕ∞) ≤ n
p : PrimeSpectrum R
⊢ (↑p.asIdeal.height : WithBot ℕ∞) ≤ n

Tactic:
specialize h p.2

Premises used: PrimeSpectrum.isPrime
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
p : PrimeSpectrum R
h : (↑p.asIdeal.height : WithBot ℕ∞) ≤ n
refine_2 refine_2₁ refine_2₂ refine_2₃ :
  ∀ (h : (↑p.asIdeal.primeHeight : WithBot ℕ∞) ≤ n), (↑(Order.height p) : WithBot ℕ∞) ≤ n
⊢ (↑(Order.height p) : WithBot ℕ∞) ≤ n

Tactic:
rwa [Ideal.height_eq_primeHeight] at h

Premises used: _private.0.Ideal.height_eq_primeHeight
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
rw :
  (∀ ⦃p : Ideal R⦄, p.IsPrime → (↑p.height : WithBot ℕ∞) ≤ n) ↔
    ∀ ⦃m : Ideal R⦄, m.IsMaximal → (↑m.height : WithBot ℕ∞) ≤ n
⊢ ringKrullDim R ≤ n ↔ ∀ ⦃m : Ideal R⦄, m.IsMaximal → (↑m.height : WithBot ℕ∞) ≤ n

Tactic:
rw [ringKrullDim_le_iff_height_le]

Premises used: ringKrullDim_le_iff_height_le
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
⊢ (∀ ⦃p : Ideal R⦄, p.IsPrime → (↑p.height : WithBot ℕ∞) ≤ n) ↔
    ∀ ⦃m : Ideal R⦄, m.IsMaximal → (↑m.height : WithBot ℕ∞) ≤ n

Tactic:
⟨fun h m hm ↦ h hm.isPrime, fun h p hp ↦ ?_⟩

Premises used: Ideal.IsMaximal.isPrime, Iff.intro
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
refine :
  ∀ (h : ∀ ⦃m : Ideal R⦄, m.IsMaximal → (↑m.height : WithBot ℕ∞) ≤ n) (p : Ideal R) (hp : p.IsPrime),
    (↑p.height : WithBot ℕ∞) ≤ n
⊢ (∀ ⦃p : Ideal R⦄, p.IsPrime → (↑p.height : WithBot ℕ∞) ≤ n) ↔
    ∀ ⦃m : Ideal R⦄, m.IsMaximal → (↑m.height : WithBot ℕ∞) ≤ n

Tactic:
refine ⟨fun h m hm ↦ h hm.isPrime, fun h p hp ↦ ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
h : ∀ ⦃m : Ideal R⦄, m.IsMaximal → (↑m.height : WithBot ℕ∞) ≤ n
p : Ideal R
hp : p.IsPrime
obtain : ∀ (m : Ideal R) (hm : m.IsMaximal) (hle : p ≤ m), (↑p.height : WithBot ℕ∞) ≤ n
⊢ (↑p.height : WithBot ℕ∞) ≤ n

Tactic:
obtain ⟨m, hm, hle⟩ := p.exists_le_maximal hp.ne_top

Premises used: Ideal.exists_le_maximal, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
h : ∀ ⦃m : Ideal R⦄, m.IsMaximal → (↑m.height : WithBot ℕ∞) ≤ n
p : Ideal R
hp : p.IsPrime
m : Ideal R
hm : m.IsMaximal
hle : p ≤ m
⊢ (↑p.height : WithBot ℕ∞) ≤ n

Tactic:
le_trans ?_ (h hm)

Premises used: le_trans
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
h : ∀ ⦃m : Ideal R⦄, m.IsMaximal → (↑m.height : WithBot ℕ∞) ≤ n
p : Ideal R
hp : p.IsPrime
m : Ideal R
hm : m.IsMaximal
hle : p ≤ m
refine : (↑p.height : WithBot ℕ∞) ≤ (↑m.height : WithBot ℕ∞)
⊢ (↑p.height : WithBot ℕ∞) ≤ n

Tactic:
refine le_trans ?_ (h hm)

Premises used: le_trans
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
h : ∀ ⦃m : Ideal R⦄, m.IsMaximal → (↑m.height : WithBot ℕ∞) ≤ n
p : Ideal R
hp : p.IsPrime
m : Ideal R
hm : m.IsMaximal
hle : p ≤ m
norm_cast : p.height ≤ m.height
⊢ (↑p.height : WithBot ℕ∞) ≤ (↑m.height : WithBot ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
h : ∀ ⦃m : Ideal R⦄, m.IsMaximal → (↑m.height : WithBot ℕ∞) ≤ n
p : Ideal R
hp : p.IsPrime
m : Ideal R
hm : m.IsMaximal
hle : p ≤ m
⊢ p.height ≤ m.height

Tactic:
Ideal.height_mono hle

Premises used: Ideal.height_mono
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
h : ∀ ⦃m : Ideal R⦄, m.IsMaximal → (↑m.height : WithBot ℕ∞) ≤ n
p : Ideal R
hp : p.IsPrime
m : Ideal R
hm : m.IsMaximal
hle : p ≤ m
⊢ p.height ≤ m.height

Tactic:
exact Ideal.height_mono hle

Premises used: Ideal.height_mono
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal A
inst_4 : J.IsPrime
rw :
  Order.krullDim.{u_2} (↑(Set.Iic { asIdeal := J, isPrime := inst_4 : PrimeSpectrum A }) : Type u_2) =
    Order.krullDim.{u_1} (↑(Set.Iic { asIdeal := comap (F := R →+* A) (algebraMap R A) J, isPrime := ⋯ }) : Type u_1)
⊢ height (comap (F := R →+* A) (algebraMap R A) J) = J.height

Tactic:
rw [eq_comm, Ideal.height_eq_primeHeight, Ideal.height_eq_primeHeight, Ideal.primeHeight,
    Ideal.primeHeight, ← WithBot.coe_inj, Order.height_eq_krullDim_Iic,
    Order.height_eq_krullDim_Iic]

Premises used: _private.0.Ideal.primeHeight, eq_comm, Order.height_eq_krullDim_Iic, WithBot.coe_inj, _private.0.Ideal.height_eq_primeHeight
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal A
inst_4 : J.IsPrime
e : OrderIso.{u_2, u_1} { p : Ideal A // p.IsPrime }
  { p : Ideal R // p.IsPrime ∧ Disjoint (↑S : Set R) (↑p : Set R) } :=
  orderIsoOfPrime S A
⊢ ∀ (p : Ideal R) (hp : p ≤ comap (F := R →+* A) (algebraMap R A) J), Disjoint (↑S : Set R) (↑p : Set R)

Tactic:
have H (p : Ideal R) (hp : p ≤ J.comap (algebraMap R A)) : Disjoint (S : Set R) p :=
    Set.disjoint_of_subset_right hp (e ⟨_, ‹J.IsPrime›⟩).2.2