awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
q : LTSeries { x_1 : α // x_1 ∈ Set.Iic x } :=
  LTSeries.mk
    (p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}))
    (fun
        (i :
          Fin
            (p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b}) +
              1)) ↦
      Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Set.Iic x)
        (p.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          i)
        ⋯)
    ⋯
a :
  LE.le (α := ℕ∞) (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞)
    (⨆ (p : LTSeries (↑(Set.Iic x) : Type u_1)),
      (↑(p.length (r := {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) | x_1.1 < x_1.2})) : ℕ∞))
⊢ LE.le (α := ℕ∞)
    (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)
    (⨆ (p : LTSeries (↑(Set.Iic x) : Type u_1)),
      ⨆ (_ :
        RelSeries.last (r :=
            {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
              match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_1 with
              | (a, b) => a < b})
            p ≤
          ⊤),
        (↑(p.length (r :=
              {x_2 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
                match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_2 with
                | (a, b) => a < b})) :
          ℕ∞))

Tactic:
simp only [le_top, iSup_pos, ge_iff_le]

Premises used: ge_iff_le, iSup_pos, le_top
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
q : LTSeries { x_1 : α // x_1 ∈ Set.Iic x } :=
  LTSeries.mk
    (p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}))
    (fun
        (i :
          Fin
            (p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b}) +
              1)) ↦
      Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Set.Iic x)
        (p.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          i)
        ⋯)
    ⋯
⊢ LE.le (α := ℕ∞) (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞)
    (⨆ (p : LTSeries (↑(Set.Iic x) : Type u_1)),
      (↑(p.length (r := {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) | x_1.1 < x_1.2})) : ℕ∞))

Tactic:
le_iSup (fun p ↦ (p.length : ℕ∞)) q

Premises used: setOf, le_iSup
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
q : LTSeries { x_1 : α // x_1 ∈ Set.Iic x } :=
  LTSeries.mk
    (p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}))
    (fun
        (i :
          Fin
            (p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b}) +
              1)) ↦
      Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Set.Iic x)
        (p.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          i)
        ⋯)
    ⋯
⊢ LE.le (α := ℕ∞) (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞)
    (⨆ (p : LTSeries (↑(Set.Iic x) : Type u_1)),
      (↑(p.length (r := {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) | x_1.1 < x_1.2})) : ℕ∞))

Tactic:
exact le_iSup (fun p ↦ (p.length : ℕ∞)) q

Premises used: le_iSup
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
a :
  ∀ (i : LTSeries (↑(Set.Iic x) : Type u_1)),
    LE.le (α := ℕ∞)
      (⨆ (_ :
        RelSeries.last (r :=
            {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
              match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_1 with
              | (a, b) => a < b})
            i ≤
          ⊤),
        (↑(i.length (r :=
              {x_2 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
                match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_2 with
                | (a, b) => a < b})) :
          ℕ∞))
      (⨆ (p : LTSeries α),
        ⨆ (_ :
          RelSeries.last (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p ≤
            x),
          (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞))
⊢ LE.le (α := ℕ∞)
    (⨆ (p : LTSeries (↑(Set.Iic x) : Type u_1)),
      ⨆ (_ :
        RelSeries.last (r :=
            {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
              match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_1 with
              | (a, b) => a < b})
            p ≤
          ⊤),
        (↑(p.length (r :=
              {x_2 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
                match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_2 with
                | (a, b) => a < b})) :
          ℕ∞))
    (⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p ≤
          x),
        (↑(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:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries (↑(Set.Iic x) : Type u_1)
a :
  ∀
    (i :
      RelSeries.last (r :=
          {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
            match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_1 with
            | (a, b) => a < b})
          p ≤
        ⊤),
    LE.le (α := ℕ∞)
      (↑(p.length (r :=
            {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
              match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_1 with
              | (a, b) => a < b})) :
        ℕ∞)
      (⨆ (p : LTSeries α),
        ⨆ (_ :
          RelSeries.last (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p ≤
            x),
          (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞))
⊢ LE.le (α := ℕ∞)
    (⨆ (_ :
      RelSeries.last (r :=
          {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
            match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_1 with
            | (a, b) => a < b})
          p ≤
        ⊤),
      (↑(p.length (r :=
            {x_2 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
              match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_2 with
              | (a, b) => a < b})) :
        ℕ∞))
    (⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p ≤
          x),
        (↑(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:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries (↑(Set.Iic x) : Type u_1)
i :
  RelSeries.last (r :=
      {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
        match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_1 with
        | (a, b) => a < b})
      p ≤
    ⊤
⊢ StrictMono (β := α) fun (y : (↑(Set.Iic x) : Type u_1)) ↦ (↑y : α)

Tactic:
have mono : StrictMono (fun (y : Set.Iic x) ↦ y.1) := fun _ _ h ↦ h
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries (↑(Set.Iic x) : Type u_1)
i :
  RelSeries.last (r :=
      {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
        match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_1 with
        | (a, b) => a < b})
      p ≤
    ⊤
mono : StrictMono (β := α) fun (y : (↑(Set.Iic x) : Type u_1)) ↦ (↑y : α)
a :
  LE.le (α := ℕ∞)
    (↑((p.map (fun (x_1 : (↑(Set.Iic x) : Type u_1)) ↦ (↑x_1 : α)) mono).length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)
    (⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p ≤
          x),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞))
⊢ LE.le (α := ℕ∞)
    (↑(p.length (r :=
          {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
            match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_1 with
            | (a, b) => a < b})) :
      ℕ∞)
    (⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p ≤
          x),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞))

Tactic:
rw [← LTSeries.map_length p (fun x ↦ x.1) mono, ]

Premises used: LTSeries.map_length, Subtype.val
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries (↑(Set.Iic x) : Type u_1)
i :
  RelSeries.last (r :=
      {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
        match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_1 with
        | (a, b) => a < b})
      p ≤
    ⊤
mono : StrictMono (β := α) fun (y : (↑(Set.Iic x) : Type u_1)) ↦ (↑y : α)
⊢ LE.le (α := ℕ∞)
    (↑((p.map (fun (x_1 : (↑(Set.Iic x) : Type u_1)) ↦ (↑x_1 : α)) mono).length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)
    (⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p ≤
          x),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞))

Tactic:
le_iSup₂ (f := fun p hp ↦ (p.length : ℕ∞)) (p.map (fun x ↦ x.1) mono) ?_

Premises used: le_iSup₂, LTSeries.map, Subtype.val
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries (↑(Set.Iic x) : Type u_1)
i :
  RelSeries.last (r :=
      {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
        match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_1 with
        | (a, b) => a < b})
      p ≤
    ⊤
mono : StrictMono (β := α) fun (y : (↑(Set.Iic x) : Type u_1)) ↦ (↑y : α)
a :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (p.map (fun (x_1 : (↑(Set.Iic x) : Type u_1)) ↦ (↑x_1 : α)) mono) ≤
    x
⊢ LE.le (α := ℕ∞)
    (↑((p.map (fun (x_1 : (↑(Set.Iic x) : Type u_1)) ↦ (↑x_1 : α)) mono).length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)
    (⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p ≤
          x),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞))

Tactic:
refine le_iSup₂ (f := fun p hp ↦ (p.length : ℕ∞)) (p.map (fun x ↦ x.1) mono) ?_

Premises used: le_iSup₂, LTSeries.map, Subtype.val
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries (↑(Set.Iic x) : Type u_1)
i :
  RelSeries.last (r :=
      {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
        match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_1 with
        | (a, b) => a < b})
      p ≤
    ⊤
mono : StrictMono (β := α) fun (y : (↑(Set.Iic x) : Type u_1)) ↦ (↑y : α)
⊢ RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (p.map (fun (x_1 : (↑(Set.Iic x) : Type u_1)) ↦ (↑x_1 : α)) mono) ≤
    x

Tactic:
(p.toFun (Fin.last p.length)).2

Premises used: RelSeries.last, Set.Mem, setOf, RelSeries.length, Fin.last, RelSeries.toFun, Set.Iic, Subtype.property
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries (↑(Set.Iic x) : Type u_1)
i :
  RelSeries.last (r :=
      {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
        match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_1 with
        | (a, b) => a < b})
      p ≤
    ⊤
mono : StrictMono (β := α) fun (y : (↑(Set.Iic x) : Type u_1)) ↦ (↑y : α)
⊢ RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (p.map (fun (x_1 : (↑(Set.Iic x) : Type u_1)) ↦ (↑x_1 : α)) mono) ≤
    x

Tactic:
exact (p.toFun (Fin.last p.length)).2

Premises used: RelSeries.length, Fin.last, RelSeries.toFun, Subtype.property
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_3
inst : Preorder α
x : α
rw : (↑(height x) : WithBot ℕ∞) = krullDim.{u_3} (↑(Set.Ici x) : Type u_3)ᵒᵈ
⊢ (↑(coheight x) : WithBot ℕ∞) = krullDim.{u_3} (↑(Set.Ici x) : Type u_3)

Tactic:
rw [coheight, ← krullDim_orderDual, Order.krullDim_eq_of_orderIso (OrderIso.refl _)]

Premises used: Order.krullDim_eq_of_orderIso, Order.krullDim_orderDual, Order.coheight, OrderIso.refl
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_3
inst : Preorder α
x : α
⊢ (↑(height x) : WithBot ℕ∞) = krullDim.{u_3} (↑(Set.Ici x) : Type u_3)ᵒᵈ

Tactic:
height_eq_krullDim_Iic _

Premises used: Set.Ici, Set.Mem, setOf, Order.height_eq_krullDim_Iic, OrderDual
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_3
inst : Preorder α
x : α
⊢ (↑(height x) : WithBot ℕ∞) = krullDim.{u_3} (↑(Set.Ici x) : Type u_3)ᵒᵈ

Tactic:
exact height_eq_krullDim_Iic _

Premises used: Order.height_eq_krullDim_Iic
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
pos : ∀ (h : Nonempty α), FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤
neg : ∀ (h : ¬Nonempty α), FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤
⊢ FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤

Tactic:
by_cases h : Nonempty α

Premises used: Nonempty
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
h : Nonempty α
⊢ FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤

Tactic:
simp [← not_infiniteDimensionalOrder_iff, ← krullDim_eq_top_iff]

Premises used: not_infiniteDimensionalOrder_iff, Order.krullDim_eq_top_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
h : ¬Nonempty α
neg : FiniteDimensionalOrder α → krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤
neg₁ : krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤ → FiniteDimensionalOrder α
⊢ FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤

Tactic:
constructor
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
h : ¬Nonempty α
⊢ FiniteDimensionalOrder α → krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤

Tactic:
(fun h1 ↦ False.elim (h (LTSeries.nonempty_of_finiteDimensionalOrder α)))

Premises used: LTSeries.nonempty_of_finiteDimensionalOrder, False.elim
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
h : ¬Nonempty α
⊢ FiniteDimensionalOrder α → krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤

Tactic:
exact (fun h1 ↦ False.elim (h (LTSeries.nonempty_of_finiteDimensionalOrder α)))
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
h : ¬Nonempty α
⊢ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤ → FiniteDimensionalOrder α

Tactic:
(fun h1 ↦ False.elim (h1.1 (krullDim_eq_bot_iff.mpr (not_nonempty_iff.mp h))))

Premises used: Iff.mpr, False.elim, Order.krullDim_eq_bot_iff, not_nonempty_iff, And.left, Iff.mp
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
h : ¬Nonempty α
⊢ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤ → FiniteDimensionalOrder α

Tactic:
exact (fun h1 ↦ False.elim (h1.1 (krullDim_eq_bot_iff.mpr (not_nonempty_iff.mp h))))

Premises used: False.elim
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : FiniteDimensionalOrder α
⊢ krullDim α ≠ ⊥

Tactic:
(finiteDimensionalOrder_iff_krullDim_ne_bot_and_top.mp ‹_›).1

Premises used: Order.finiteDimensionalOrder_iff_krullDim_ne_bot_and_top, And.left, Iff.mp
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : FiniteDimensionalOrder α
⊢ krullDim α ≠ ⊤

Tactic:
(finiteDimensionalOrder_iff_krullDim_ne_bot_and_top.mp ‹_›).2

Premises used: Order.finiteDimensionalOrder_iff_krullDim_ne_bot_and_top, And.right, Iff.mp
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : FiniteDimensionalOrder α
x : α
rw : (↑(coheight x) : WithBot ℕ∞) < (↑⊤ : WithBot ℕ∞)
⊢ coheight x < ⊤

Tactic:
rw [← WithBot.coe_lt_coe]

Premises used: WithBot.coe_lt_coe
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : FiniteDimensionalOrder α
x : α
apply : krullDim α < (↑⊤ : WithBot ℕ∞)
⊢ (↑(coheight x) : WithBot ℕ∞) < (↑⊤ : WithBot ℕ∞)

Tactic:
apply lt_of_le_of_lt (coheight_le_krullDim x)

Premises used: lt_of_le_of_lt, Order.coheight_le_krullDim
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : FiniteDimensionalOrder α
x : α
⊢ krullDim α < (↑⊤ : WithBot ℕ∞)

Tactic:
simpa using krullDim_ne_top_of_finiteDimensionalOrder.lt_top

Premises used: Ne.lt_top, Order.krullDim_ne_top_of_finiteDimensionalOrder
-- Module: Mathlib.Order.KrullDimension
Goal:
n m : ℕ
e : n ≤ m
α : Type u_1
inst : Preorder α
inst_1 : KrullDimLE n α
⊢ KrullDimLE m α

Tactic:
⟨KrullDimLE.krullDim_le (n := n).trans (Nat.cast_le.mpr e)⟩

Premises used: Iff.mpr, Order.KrullDimLE.mk, Order.KrullDimLE.krullDim_le, Nat.cast_le, LE.le.trans
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Subsingleton α
⊢ KrullDimLE 0 α

Tactic:
⟨krullDim_nonpos_of_subsingleton⟩

Premises used: Order.KrullDimLE.mk, Order.krullDim_nonpos_of_subsingleton
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
rw : krullDim α ≤ 1 ∧ 1 ≤ krullDim α ↔ IsSimpleOrder α
rw₁ : (∀ (x : α), x = ⊥ ∨ x = ⊤) ∧ 1 ≤ krullDim α ↔ IsSimpleOrder α
rw₂ : (∀ (x : α), x = ⊥ ∨ x = ⊤) ∧ 0 < krullDim α ↔ IsSimpleOrder α
rw₃ : (∀ (x : α), x = ⊥ ∨ x = ⊤) ∧ Nontrivial α ↔ IsSimpleOrder α
rw₄ : (∀ (x : α), x = ⊥ ∨ x = ⊤) ∧ Nontrivial α ↔ Nontrivial α ∧ ∀ (a : α), a = ⊥ ∨ a = ⊤
rw₅ rw₆ : (Nontrivial α ∧ ∀ (x : α), x = ⊥ ∨ x = ⊤) ↔ Nontrivial α ∧ ∀ (a : α), a = ⊥ ∨ a = ⊤
⊢ krullDim α = 1 ↔ IsSimpleOrder α

Tactic:
rw [le_antisymm_iff, krullDim_le_one_iff_of_boundedOrder, WithBot.one_le_iff_pos,
    Order.krullDim_pos_iff_of_orderBot, isSimpleOrder_iff, and_comm]

Premises used: and_comm, Order.krullDim_le_one_iff_of_boundedOrder, isSimpleOrder_iff, le_antisymm_iff, Order.krullDim_pos_iff_of_orderBot, WithBot.one_le_iff_pos
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
⊢ krullDim α = 1

Tactic:
krullDim_eq_one_iff_of_boundedOrder.mpr ‹_›

Premises used: Iff.mpr, Order.krullDim_eq_one_iff_of_boundedOrder
-- Module: Mathlib.Order.KrullDimension
Goal:
n : ℕ
ih : ∀ m < n, height m = (↑m : ℕ∞)
ind : height n ≤ (↑n : ℕ∞)
ind₁ : (↑n : ℕ∞) ≤ height n
⊢ height n = (↑n : ℕ∞)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.KrullDimension
Goal:
n : ℕ
ih : ∀ m < n, height m = (↑m : ℕ∞)
ind : ∀ y < n, height y < (↑n : ℕ∞)
⊢ height n ≤ (↑n : ℕ∞)

Tactic:
apply height_le_coe_iff.mpr

Premises used: Iff.mpr, Order.height_le_coe_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
n : ℕ
ih : ∀ m < n, height m = (↑m : ℕ∞)
⊢ ∀ y < n, height y < (↑n : ℕ∞)

Tactic:
simp +contextual only [ih, Nat.cast_lt, implies_true]

Premises used: implies_true, Nat.cast_lt
-- Module: Mathlib.Order.KrullDimension
Goal:
n : ℕ
ih : ∀ m < n, height m = (↑m : ℕ∞)
⊢ (↑n : ℕ∞) ≤ height n

Tactic:
length_le_height_last (p := LTSeries.range n)

Premises used: RelSeries.last, Order.length_le_height_last
-- Module: Mathlib.Order.KrullDimension
Goal:
n : ℕ
ih : ∀ m < n, height m = (↑m : ℕ∞)
⊢ (↑n : ℕ∞) ≤ height n

Tactic:
exact length_le_height_last (p := LTSeries.range n)

Premises used: Order.length_le_height_last
-- Module: Mathlib.Order.KrullDimension
Goal:
n : ℕ
ind : ∀ (n : ℕ) (ih : ∀ m < n, height m = (↑m : ℕ∞)), height n = (↑n : ℕ∞)
⊢ height n = (↑n : ℕ∞)

Tactic:
induction n using Nat.strongRecOn with | ind n ih =>
  apply le_antisymm
  · apply height_le_coe_iff.mpr
    simp +contextual only [ih, Nat.cast_lt, implies_true]
  · exact length_le_height_last (p := LTSeries.range n)

Premises used: Iff.mpr, Order.height_le_coe_iff, le_antisymm, implies_true, Nat.cast_lt, Order.length_le_height_last
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
obtain : ∀ (f : ℕ → (↑(Set.Ioi a) : Type u_1)) (hstrictmono : StrictMono f), coheight a = ⊤
⊢ coheight a = ⊤

Tactic:
obtain ⟨f, hstrictmono⟩ := Nat.exists_strictMono ↑(Set.Ioi a)

Premises used: Nat.exists_strictMono, Set.Ioi, Set.Elem
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
f : ℕ → (↑(Set.Ioi a) : Type u_1)
hstrictmono : StrictMono f
apply :
  ∀ (n : ℕ),
    ∃ (p : LTSeries α),
      RelSeries.head (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          a ∧
        p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) =
          n
⊢ coheight a = ⊤

Tactic:
apply coheight_eq_top_iff.mpr

Premises used: Iff.mpr, Order.coheight_eq_top_iff