awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
inst_2 : Nonempty α
hnottop : krullDim α < ⊤
a : α
this : height a < ⊤
⊢ coheight a < ⊤

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

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 α < ⊤
a : α
this_1 : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = (↑n : ℕ∞)
hch : coheight a = ⊤
⊢ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) ⊤ ≤
    ⨆ (p : LTSeries α),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)

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 α < ⊤
a : α
this_1 : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = (↑n : ℕ∞)
m : ℕ
hch : coheight a = (↑m : ℕ∞)
h :
  ∀ (p₁ : LTSeries α)
    (hlast :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p₁ =
        a)
    (hlen₁ :
      p₁.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n),
    HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) (↑m : ℕ∞) ≤
      ⨆ (p : LTSeries α),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞)
⊢ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) (↑m : ℕ∞) ≤
    ⨆ (p : LTSeries α),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)

Tactic:
obtain ⟨p₁, hlast, hlen₁⟩ := exists_series_of_height_eq_coe a hh

Premises used: Order.exists_series_of_height_eq_coe
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
inst_2 : Nonempty α
hnottop : krullDim α < ⊤
a : α
this_1 : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = (↑n : ℕ∞)
m : ℕ
hch : coheight a = (↑m : ℕ∞)
p₁ : LTSeries α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p₁ =
    a
hlen₁ :
  p₁.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    n
h :
  ∀ (p₂ : LTSeries α)
    (hhead :
      RelSeries.head (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p₂ =
        a)
    (hlen₂ :
      p₂.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        m),
    HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) (↑m : ℕ∞) ≤
      ⨆ (p : LTSeries α),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞)
⊢ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) (↑m : ℕ∞) ≤
    ⨆ (p : LTSeries α),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)

Tactic:
obtain ⟨p₂, hhead, hlen₂⟩ := exists_series_of_coheight_eq_coe a hch

Premises used: Order.exists_series_of_coheight_eq_coe
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
inst_2 : Nonempty α
hnottop : krullDim α < ⊤
a : α
this_1 : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = (↑n : ℕ∞)
m : ℕ
hch : coheight a = (↑m : ℕ∞)
p₁ : LTSeries α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p₁ =
    a
hlen₁ :
  p₁.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    n
p₂ : LTSeries α
hhead :
  RelSeries.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p₂ =
    a
hlen₂ :
  p₂.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    m
⊢ RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p₁ =
    RelSeries.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p₂

Tactic:
simp [*]
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
inst_2 : Nonempty α
hnottop : krullDim α < ⊤
a : α
this_1 : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = (↑n : ℕ∞)
m : ℕ
hch : coheight a = (↑m : ℕ∞)
p₁ : LTSeries α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p₁ =
    a
hlen₁ :
  p₁.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    n
p₂ : LTSeries α
hhead :
  RelSeries.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p₂ =
    a
hlen₂ :
  p₂.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    m
⊢ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) (↑m : ℕ∞) ≤
    (↑((RelSeries.smash (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p₁ p₂ ⋯).length
          (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)

Tactic:
simp [*]
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
inst_2 : Nonempty α
hnottop : krullDim α < ⊤
a : α
this_1 : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = (↑n : ℕ∞)
m : ℕ
hch : coheight a = (↑m : ℕ∞)
p₁ : LTSeries α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p₁ =
    a
hlen₁ :
  p₁.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    n
p₂ : LTSeries α
hhead :
  RelSeries.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p₂ =
    a
hlen₂ :
  p₂.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    m
⊢ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) (↑m : ℕ∞) ≤
    ⨆ (p : LTSeries α),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)

Tactic:
apply le_iSup_of_le ((p₁.smash p₂) (by simp [*])) (by simp [*])

Premises used: RelSeries.smash, le_iSup_of_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 : α
this_1 : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = (↑n : ℕ∞)
h :
  ∀ (x : ℕ∞) (hch : coheight a = x),
    (↑n : ℕ∞) + x ≤
      ⨆ (p : LTSeries α),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞)
⊢ (↑n : ℕ∞) + coheight a ≤
    ⨆ (p : LTSeries α),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)

Tactic:
cases hch : coheight a with
      | top => simp_all
      | coe m =>
        obtain ⟨p₁, hlast, hlen₁⟩ := exists_series_of_height_eq_coe a hh
        obtain ⟨p₂, hhead, hlen₂⟩ := exists_series_of_coheight_eq_coe a hch
        apply le_iSup_of_le ((p₁.smash p₂) (by simp [*])) (by simp [*])

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

Tactic:
cases hh : height a with
    | top => simp_all
    | coe n =>
      cases hch : coheight a with
      | top => simp_all
      | coe m =>
        obtain ⟨p₁, hlast, hlen₁⟩ := exists_series_of_height_eq_coe a hh
        obtain ⟨p₂, hhead, hlen₂⟩ := exists_series_of_coheight_eq_coe a hch
        apply le_iSup_of_le ((p₁.smash p₂) (by simp [*])) (by simp [*])

Premises used: Order.height, Order.coheight
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
h : IsEmpty α
inl : Eq (α := WithBot ℕ∞) ⊥ (⨆ (a : α), (↑(height a) : WithBot ℕ∞))
inl₁ inl₂ : Eq (α := WithBot ℕ∞) ⊥ ⊥
⊢ krullDim α = ⨆ (a : α), (↑(height a) : WithBot ℕ∞)

Tactic:
rw [krullDim_eq_bot, ciSup_of_empty]

Premises used: ciSup_of_empty, Order.krullDim_eq_bot
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
h : Nonempty α
inr : Eq (α := WithBot ℕ∞) (↑(⨆ (a : α), height a) : WithBot ℕ∞) (⨆ (a : α), (↑(height a) : WithBot ℕ∞))
inr₁ inr₂ : Eq (α := WithBot ℕ∞) (⨆ (i : α), (↑(height i) : WithBot ℕ∞)) (⨆ (a : α), (↑(height a) : WithBot ℕ∞))
⊢ krullDim α = ⨆ (a : α), (↑(height a) : WithBot ℕ∞)

Tactic:
rw [krullDim_eq_iSup_height_of_nonempty, WithBot.coe_iSup (OrderTop.bddAbove _)]

Premises used: OrderTop.bddAbove, Order.krullDim_eq_iSup_height_of_nonempty, WithBot.coe_iSup
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
⊢ IsEmpty α ∨ Nonempty α

Tactic:
cases isEmpty_or_nonempty α with
  | inl h => rw [krullDim_eq_bot, ciSup_of_empty]
  | inr h => rw [krullDim_eq_iSup_height_of_nonempty, WithBot.coe_iSup (OrderTop.bddAbove _)]

Premises used: OrderTop.bddAbove, isEmpty_or_nonempty, Order.krullDim_eq_iSup_height_of_nonempty, ciSup_of_empty, WithBot.coe_iSup, Order.krullDim_eq_bot
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
h : IsEmpty α
inl : Eq (α := WithBot ℕ∞) ⊥ (⨆ (a : α), (↑(coheight a) : WithBot ℕ∞))
inl₁ inl₂ : Eq (α := WithBot ℕ∞) ⊥ ⊥
⊢ krullDim α = ⨆ (a : α), (↑(coheight a) : WithBot ℕ∞)

Tactic:
rw [krullDim_eq_bot, ciSup_of_empty]

Premises used: ciSup_of_empty, Order.krullDim_eq_bot
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
h : Nonempty α
inr : Eq (α := WithBot ℕ∞) (↑(⨆ (a : α), coheight a) : WithBot ℕ∞) (⨆ (a : α), (↑(coheight a) : WithBot ℕ∞))
inr₁ inr₂ : Eq (α := WithBot ℕ∞) (⨆ (i : α), (↑(coheight i) : WithBot ℕ∞)) (⨆ (a : α), (↑(coheight a) : WithBot ℕ∞))
⊢ krullDim α = ⨆ (a : α), (↑(coheight a) : WithBot ℕ∞)

Tactic:
rw [krullDim_eq_iSup_coheight_of_nonempty, WithBot.coe_iSup (OrderTop.bddAbove _)]

Premises used: OrderTop.bddAbove, Order.krullDim_eq_iSup_coheight_of_nonempty, WithBot.coe_iSup
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
⊢ IsEmpty α ∨ Nonempty α

Tactic:
cases isEmpty_or_nonempty α with
  | inl h => rw [krullDim_eq_bot, ciSup_of_empty]
  | inr h => rw [krullDim_eq_iSup_coheight_of_nonempty, WithBot.coe_iSup (OrderTop.bddAbove _)]

Premises used: OrderTop.bddAbove, Order.krullDim_eq_iSup_coheight_of_nonempty, isEmpty_or_nonempty, ciSup_of_empty, WithBot.coe_iSup, Order.krullDim_eq_bot
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
rw :
  (↑(height.{u_1} (α := α) ⊤) : WithBot ℕ∞) =
    (↑(⨆ (p : LTSeries α),
          (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞)) :
      WithBot ℕ∞)
⊢ (↑(height.{u_1} (α := α) ⊤) : 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 α
inst_1 : OrderTop α
simp : height.{u_1} (α := α) ⊤ = ⨆ (p : LTSeries α), (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞)
⊢ (↑(height.{u_1} (α := α) ⊤) : WithBot ℕ∞) =
    (↑(⨆ (p : LTSeries α),
          (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞)) :
      WithBot ℕ∞)

Tactic:
simp only [WithBot.coe_inj]

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

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
⊢ height.{u_1} (α := α) ⊤ ≤ ⨆ (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 α
inst_1 : OrderTop α
⊢ height.{u_1} (α := α) ⊤ ≤ ⨆ (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 α
inst_1 : OrderTop α
⊢ ⨆ (p : LTSeries α), (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞) ≤ height.{u_1} (α := α) ⊤

Tactic:
iSup_le fun _ => length_le_height le_top

Premises used: Order.length_le_height, le_top, iSup_le
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
⊢ ⨆ (p : LTSeries α), (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞) ≤ height.{u_1} (α := α) ⊤

Tactic:
exact iSup_le fun _ => length_le_height le_top

Premises used: Order.length_le_height, le_top, iSup_le
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
rw : (↑(coheight.{u_1} (α := α) ⊥) : WithBot ℕ∞) = krullDim.{u_1} αᵒᵈ
⊢ (↑(coheight.{u_1} (α := α) ⊥) : WithBot ℕ∞) = krullDim α

Tactic:
rw [← krullDim_orderDual]

Premises used: Order.krullDim_orderDual
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
⊢ (↑(coheight.{u_1} (α := α) ⊥) : WithBot ℕ∞) = krullDim.{u_1} αᵒᵈ

Tactic:
height_top_eq_krullDim (α := αᵒᵈ)

Premises used: Order.height_top_eq_krullDim, Order.coheight
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
⊢ (↑(coheight.{u_1} (α := α) ⊥) : WithBot ℕ∞) = krullDim.{u_1} αᵒᵈ

Tactic:
exact height_top_eq_krullDim (α := αᵒᵈ)

Premises used: Order.height_top_eq_krullDim
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
rw :
  Eq (α := ℕ∞)
    (⨆ (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})) :
          ℕ∞))
    (⨆ (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})) :
          ℕ∞))
⊢ (↑(height x) : WithBot ℕ∞) = krullDim.{u_1} (↑(Set.Iic x) : Type u_1)

Tactic:
rw [← height_top_eq_krullDim, height, height, WithBot.coe_inj]

Premises used: Order.height_top_eq_krullDim, WithBot.coe_inj, Order.height
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
a :
  LE.le (α := ℕ∞)
    (⨆ (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})) :
          ℕ∞))
    (⨆ (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})) :
          ℕ∞))
a₁ :
  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})) :
          ℕ∞))
⊢ Eq (α := ℕ∞)
    (⨆ (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})) :
          ℕ∞))
    (⨆ (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:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
a :
  ∀ (i : LTSeries α),
    LE.le (α := ℕ∞)
      (⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            i ≤
          x),
        (↑(i.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})) :
            ℕ∞))
⊢ LE.le (α := ℕ∞)
    (⨆ (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})) :
          ℕ∞))
    (⨆ (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:
apply iSup_le

Premises used: iSup_le
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries α
a :
  ∀
    (i :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p ≤
        x),
    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})) :
            ℕ∞))
⊢ LE.le (α := ℕ∞)
    (⨆ (_ :
      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})) :
        ℕ∞))
    (⨆ (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:
apply iSup_le

Premises used: iSup_le