awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
h : Nonempty α
h_1 : FiniteDimensionalOrder α
inr :
  n ≤
      RelSeries.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (LTSeries.longestOf α) →
    ∃ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n
inr₁ :
  (∃ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n) →
    n ≤
      RelSeries.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (LTSeries.longestOf α)
⊢ n ≤
      RelSeries.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (LTSeries.longestOf α) ↔
    ∃ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n

Tactic:
constructor
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
h : Nonempty α
h_1 : FiniteDimensionalOrder α
⊢ n ≤
      RelSeries.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (LTSeries.longestOf α) →
    ∃ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n

Tactic:
fun H ↦ ⟨(LTSeries.longestOf α).take ⟨_, Nat.lt_succ_of_le H⟩, rfl⟩

Premises used: LTSeries.longestOf, Fin.mk, Nat.lt_succ_of_le, RelSeries.take, Exists.intro, rfl
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
h : Nonempty α
h_1 : FiniteDimensionalOrder α
⊢ n ≤
      RelSeries.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (LTSeries.longestOf α) →
    ∃ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n

Tactic:
exact fun H ↦ ⟨(LTSeries.longestOf α).take ⟨_, Nat.lt_succ_of_le H⟩, rfl⟩
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
h : Nonempty α
h_1 : FiniteDimensionalOrder α
⊢ (∃ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n) →
    n ≤
      RelSeries.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (LTSeries.longestOf α)

Tactic:
fun ⟨l, hl⟩ ↦ hl ▸ l.longestOf_is_longest

Premises used: _private.0.Order.le_krullDim_iff.match_1, LTSeries.longestOf, Eq.rec, RelSeries.length, LE.le, LTSeries.longestOf_is_longest
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
h : Nonempty α
h_1 : FiniteDimensionalOrder α
⊢ (∃ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n) →
    n ≤
      RelSeries.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (LTSeries.longestOf α)

Tactic:
exact fun ⟨l, hl⟩ ↦ hl ▸ l.longestOf_is_longest
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
h : Nonempty α
h_1 : InfiniteDimensionalOrder α
⊢ (↑n : WithBot ℕ∞) ≤ krullDim α ↔
    ∃ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n

Tactic:
simpa [krullDim_eq_top] using SetRel.InfiniteDimensional.exists_relSeries_with_length n

Premises used: Order.krullDim_eq_top, SetRel.InfiniteDimensional.exists_relSeries_with_length
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ krullDim α =
    (↑(⨆ (p : LTSeries α),
          (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞)) :
      WithBot ℕ∞)

Tactic:
simp [krullDim, WithBot.coe_iSup (OrderTop.bddAbove _), WithBot.coe_natCast]

Premises used: OrderTop.bddAbove, Order.krullDim, WithBot.coe_iSup, WithBot.coe_natCast
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
zero :
  LT.lt (α := WithBot ℕ∞)
      (⨆ (p : LTSeries α),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          WithBot ℕ∞))
      (↑(↑0 : ℕ∞) : WithBot ℕ∞) ↔
    ∀ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) <
        0
succ :
  ∀ (n : ℕ),
    LT.lt (α := WithBot ℕ∞)
        (⨆ (p : LTSeries α),
          (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            WithBot ℕ∞))
        (↑(↑(n + 1) : ℕ∞) : WithBot ℕ∞) ↔
      ∀ (l : LTSeries α),
        l.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) <
          n + 1
⊢ LT.lt (α := WithBot ℕ∞)
      (⨆ (p : LTSeries α),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          WithBot ℕ∞))
      (↑(↑n : ℕ∞) : WithBot ℕ∞) ↔
    ∀ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) <
        n

Tactic:
rcases n with - | n
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
zero :
  Eq (α := WithBot ℕ∞)
      (⨆ (p : LTSeries α),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          WithBot ℕ∞))
      ⊥ ↔
    ∀ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) <
        0
⊢ LT.lt (α := WithBot ℕ∞)
      (⨆ (p : LTSeries α),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          WithBot ℕ∞))
      (↑(↑0 : ℕ∞) : WithBot ℕ∞) ↔
    ∀ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) <
        0

Tactic:
rw [ENat.coe_zero, ← bot_eq_zero, WithBot.lt_coe_bot]

Premises used: WithBot.lt_coe_bot, ENat.coe_zero, bot_eq_zero
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
⊢ Eq (α := WithBot ℕ∞)
      (⨆ (p : LTSeries α),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          WithBot ℕ∞))
      ⊥ ↔
    ∀ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) <
        0

Tactic:
simp
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
⊢ LT.lt (α := WithBot ℕ∞)
      (⨆ (p : LTSeries α),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          WithBot ℕ∞))
      (↑(↑(n + 1) : ℕ∞) : WithBot ℕ∞) ↔
    ∀ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) <
        n + 1

Tactic:
simp [ENat.WithBot.lt_add_one_iff, WithBot.coe_natCast]

Premises used: ENat.WithBot.lt_add_one_iff, WithBot.coe_natCast
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
⊢ krullDim α ≤ krullDim β

Tactic:
iSup_le fun p ↦ le_sSup ⟨p.map f hf, rfl⟩

Premises used: Order.krullDim, Exists.intro, iSup_le, le_sSup, LTSeries.map, rfl
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : ∀ ⦃a b : α⦄, f a < f b → a < b
hf' : Function.Surjective f
⊢ krullDim β ≤ krullDim α

Tactic:
iSup_le fun p ↦ le_sSup ⟨p.comap _ hf hf', rfl⟩

Premises used: Order.krullDim, Exists.intro, iSup_le, le_sSup, LTSeries.comap, rfl
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
⊢ krullDim α = krullDim β

Tactic:
le_antisymm (krullDim_le_of_strictMono _ f.strictMono) <|
    krullDim_le_of_strictMono _ f.symm.strictMono

Premises used: OrderIso.strictMono, OrderIso.symm, le_antisymm, Order.krullDim_le_of_strictMono
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
⊢ krullDim.{u_1} αᵒᵈ = krullDim α

Tactic:
le_antisymm (iSup_le fun i ↦ le_sSup ⟨i.reverse, rfl⟩) <|
    iSup_le fun i ↦ le_sSup ⟨i.reverse, rfl⟩

Premises used: RelSeries.reverse, le_antisymm, Exists.intro, iSup_le, le_sSup, rfl
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Nonempty α

Tactic:
have : Nonempty α := ⟨a⟩
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
this : Nonempty α
rw :
  (↑(height a) : WithBot ℕ∞) ≤
    (↑(⨆ (p : LTSeries α),
          (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞)) :
      WithBot ℕ∞)
⊢ (↑(height a) : WithBot ℕ∞) ≤ krullDim α

Tactic:
rw [krullDim_eq_iSup_length]

Premises used: Order.krullDim_eq_iSup_length
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
this : Nonempty α
simp : height a ≤ ⨆ (p : LTSeries α), (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞)
⊢ (↑(height a) : WithBot ℕ∞) ≤
    (↑(⨆ (p : LTSeries α),
          (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞)) :
      WithBot ℕ∞)

Tactic:
simp only [WithBot.coe_le_coe]

Premises used: WithBot.coe_le_coe
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
this : Nonempty α
⊢ height a ≤ ⨆ (p : LTSeries α), (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞)

Tactic:
height_le fun p _ ↦ le_iSup_of_le p le_rfl

Premises used: le_rfl, Order.height_le, le_iSup_of_le
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
this : Nonempty α
⊢ height a ≤ ⨆ (p : LTSeries α), (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞)

Tactic:
exact height_le fun p _ ↦ le_iSup_of_le p le_rfl

Premises used: le_rfl, Order.height_le, le_iSup_of_le
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ (↑(coheight a) : WithBot ℕ∞) ≤ krullDim α

Tactic:
simpa using height_le_krullDim (α := αᵒᵈ) a

Premises used: Order.height_le_krullDim
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : FiniteDimensionalOrder α
⊢ (↑(height
          (RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            (LTSeries.longestOf α))) :
      WithBot ℕ∞) =
    krullDim α

Tactic:
le_antisymm (height_le_krullDim _) ?_

Premises used: Order.height_le_krullDim, le_antisymm
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : FiniteDimensionalOrder α
refine :
  krullDim α ≤
    (↑(height
          (RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            (LTSeries.longestOf α))) :
      WithBot ℕ∞)
⊢ (↑(height
          (RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            (LTSeries.longestOf α))) :
      WithBot ℕ∞) =
    krullDim α

Tactic:
refine le_antisymm (height_le_krullDim _) ?_

Premises used: Order.height_le_krullDim, le_antisymm
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : FiniteDimensionalOrder α
rw :
  LE.le (α := WithBot ℕ∞)
    (↑(RelSeries.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          (LTSeries.longestOf α)) :
      WithBot ℕ∞)
    (↑(⨆ (p : LTSeries α),
          ⨆ (_ :
            RelSeries.last (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})
                p ≤
              RelSeries.last (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})
                (LTSeries.longestOf α)),
            (↑(p.length (r :=
                  {x : α × α |
                    match (motive := α × α → Prop) x with
                    | (a, b) => a < b})) :
              ℕ∞)) :
      WithBot ℕ∞)
⊢ krullDim α ≤
    (↑(height
          (RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            (LTSeries.longestOf α))) :
      WithBot ℕ∞)

Tactic:
rw [krullDim_eq_length_of_finiteDimensionalOrder, height]

Premises used: Order.krullDim_eq_length_of_finiteDimensionalOrder, Order.height
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : FiniteDimensionalOrder α
norm_cast :
  LE.le (α := ℕ∞)
    (↑(RelSeries.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          (LTSeries.longestOf α)) :
      ℕ∞)
    (⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p ≤
          RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            (LTSeries.longestOf α)),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞))
⊢ LE.le (α := WithBot ℕ∞)
    (↑(RelSeries.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          (LTSeries.longestOf α)) :
      WithBot ℕ∞)
    (↑(⨆ (p : LTSeries α),
          ⨆ (_ :
            RelSeries.last (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})
                p ≤
              RelSeries.last (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})
                (LTSeries.longestOf α)),
            (↑(p.length (r :=
                  {x : α × α |
                    match (motive := α × α → Prop) x with
                    | (a, b) => a < b})) :
              ℕ∞)) :
      WithBot ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : FiniteDimensionalOrder α
⊢ LE.le (α := ℕ∞)
    (↑(RelSeries.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          (LTSeries.longestOf α)) :
      ℕ∞)
    (⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p ≤
          RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            (LTSeries.longestOf α)),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞))

Tactic:
le_iSup_iff.mpr <| fun _ h ↦ iSup_le_iff.mp (h _) le_rfl

Premises used: Iff.mpr, le_rfl, LTSeries.longestOf, Iff.mp, iSup_le_iff, le_iSup_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : FiniteDimensionalOrder α
⊢ LE.le (α := ℕ∞)
    (↑(RelSeries.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          (LTSeries.longestOf α)) :
      ℕ∞)
    (⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p ≤
          RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            (LTSeries.longestOf α)),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞))

Tactic:
exact le_iSup_iff.mpr <| fun _ h ↦ iSup_le_iff.mp (h _) le_rfl

Premises used: Iff.mpr, le_rfl, Iff.mp, iSup_le_iff, le_iSup_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
a : krullDim α ≤ (↑(⨆ (a : α), height a) : WithBot ℕ∞)
a₁ : (↑(⨆ (a : α), height a) : WithBot ℕ∞) ≤ krullDim α
⊢ krullDim α = (↑(⨆ (a : α), height a) : WithBot ℕ∞)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
a :
  ∀ (i : LTSeries α),
    LE.le (α := WithBot ℕ∞)
      (↑(i.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞)
      (↑(⨆ (a : α), height a) : WithBot ℕ∞)
⊢ krullDim α ≤ (↑(⨆ (a : α), height a) : WithBot ℕ∞)

Tactic:
apply iSup_le

Premises used: iSup_le
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
p : LTSeries α
a :
  LE.le (α := ℕ∞)
    (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)
    (⨆ (a : α), height a)
⊢ LE.le (α := WithBot ℕ∞)
    (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      WithBot ℕ∞)
    (↑(⨆ (a : α), height a) : WithBot ℕ∞)

Tactic:
suffices p.length ≤ ⨆ (a : α), height a from (WithBot.unbotD_le_iff fun _ => this).mp this
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
p : LTSeries α
⊢ LE.le (α := ℕ∞)
    (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)
    (⨆ (a : α), height a)

Tactic:
apply le_iSup_of_le p.last (length_le_height_last (p := p))

Premises used: RelSeries.last, le_iSup_of_le, Order.length_le_height_last
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ BddAbove (Set.range.{0, u_1 + 1} (ι := α) height)

Tactic:
bddDefault
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
a : ⨆ (i : α), (↑(height i) : WithBot ℕ∞) ≤ krullDim α
⊢ (↑(⨆ (a : α), height a) : WithBot ℕ∞) ≤ krullDim α

Tactic:
rw [WithBot.coe_iSup (by bddDefault)]

Premises used: WithBot.coe_iSup
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
a : ∀ (i : α), (↑(height i) : WithBot ℕ∞) ≤ krullDim α
⊢ ⨆ (i : α), (↑(height i) : WithBot ℕ∞) ≤ krullDim α

Tactic:
apply iSup_le

Premises used: iSup_le
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ ∀ (i : α), (↑(height i) : WithBot ℕ∞) ≤ krullDim α

Tactic:
apply height_le_krullDim

Premises used: Order.height_le_krullDim
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ krullDim α = (↑(⨆ (a : α), coheight a) : WithBot ℕ∞)

Tactic:
simpa using krullDim_eq_iSup_height_of_nonempty (α := αᵒᵈ)

Premises used: Order.krullDim_eq_iSup_height_of_nonempty
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
a : krullDim α ≤ (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞)
a₁ : (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞) ≤ krullDim α
⊢ krullDim α = (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
a : LE.le (α := ℕ∞) (⨆ (a : α), height a) (⨆ (a : α), height a + coheight a)
⊢ krullDim α ≤ (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞)

Tactic:
rw [krullDim_eq_iSup_height_of_nonempty, WithBot.coe_le_coe]

Premises used: Order.krullDim_eq_iSup_height_of_nonempty, WithBot.coe_le_coe
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ BddAbove (α := ℕ∞) (Set.range fun (a : α) ↦ height a + coheight a)

Tactic:
bddDefault
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ ∀ (x : α), height x ≤ height x + coheight x

Tactic:
simp
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ LE.le (α := ℕ∞) (⨆ (a : α), height a) (⨆ (a : α), height a + coheight a)

Tactic:
apply ciSup_mono (by bddDefault) (by simp)

Premises used: ciSup_mono
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
a :
  ∀
    (this :
      ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α] (hnottop : krullDim α < ⊤),
        (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞) ≤ krullDim α)
    (hnottop : ¬krullDim α < ⊤), (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞) ≤ krullDim α
wlog :
  ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α] (hnottop : krullDim α < ⊤),
    (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞) ≤ krullDim α
⊢ (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞) ≤ krullDim α

Tactic:
wlog hnottop : krullDim α < ⊤

Premises used: Order.krullDim
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
this :
  ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α] (hnottop : krullDim α < ⊤),
    (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞) ≤ krullDim α
hnottop : ¬krullDim α < ⊤
⊢ (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞) ≤ krullDim α

Tactic:
simp_all
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
inst_2 : Nonempty α
hnottop : krullDim α < ⊤
rw :
  LE.le (α := ℕ∞) (⨆ (a : α), height a + coheight a)
    (⨆ (p : LTSeries α),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞))
⊢ (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞) ≤ krullDim α

Tactic:
rw [krullDim_eq_iSup_length, WithBot.coe_le_coe]

Premises used: Order.krullDim_eq_iSup_length, WithBot.coe_le_coe
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
inst_2 : Nonempty α
hnottop : krullDim α < ⊤
h :
  ∀ (i : α),
    height i + coheight i ≤
      ⨆ (p : LTSeries α),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞)
⊢ LE.le (α := ℕ∞) (⨆ (a : α), height a + coheight a)
    (⨆ (p : LTSeries α),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞))

Tactic:
apply iSup_le

Premises used: iSup_le
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
inst_2 : Nonempty α
hnottop : krullDim α < ⊤
a : α
⊢ height a < ⊤

Tactic:
have : height a < ⊤ := WithBot.coe_lt_coe.mp (lt_of_le_of_lt (height_le_krullDim a) hnottop)