awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
hne :
  Nonempty.{max 1 (u_1 + 1)}
    { p : LTSeries α //
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a }
m : ℕ
h : n ≤ m
ha :
  Eq (α := ℕ∞)
    (⨆ (x :
      { p : LTSeries α //
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          a }),
      (↑((↑x : LTSeries α).length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞))
    (↑m : ℕ∞)
p : LTSeries α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    a
hlen : p.length (r := {x : α × α | x.1 < x.2}) = m
h₁ : m - (m - n) = n
⊢ (RelSeries.drop (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p
          (⟨m - n, ⋯⟩ :
            Fin
              (p.length (r :=
                  {x : α × α |
                    match (motive := α × α → Prop) x with
                    | (a, b) => a < b}) +
                1))).length
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    n

Tactic:
simp [hlen]
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
hne :
  Nonempty.{max 1 (u_1 + 1)}
    { p : LTSeries α //
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a }
m : ℕ
h : n ≤ m
ha :
  Eq (α := ℕ∞)
    (⨆ (x :
      { p : LTSeries α //
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          a }),
      (↑((↑x : LTSeries α).length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞))
    (↑m : ℕ∞)
p : LTSeries α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    a
hlen : p.length (r := {x : α × α | x.1 < x.2}) = m
⊢ m - (m - n) = n

Tactic:
lia
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
h : (↑n : ℕ∞) ≤ height a
hne :
  Nonempty.{max 1 (u_1 + 1)}
    { p : LTSeries α //
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a }
cases :
  ∀ (x : ℕ∞) (ha : height a = x),
    ∃ (p : LTSeries α),
      RelSeries.last (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
⊢ ∃ (p : LTSeries α),
    RelSeries.last (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

Tactic:
cases ha : height a with
  | top =>
    clear h
    rw [height_eq_iSup_last_eq, iSup_subtype', ENat.iSup_coe_eq_top, bddAbove_def] at ha
    contrapose! ha
    use n
    rintro m ⟨⟨p, rfl⟩, hp⟩
    simp only at hp
    by_contra! hnm
    apply ha (p.drop ⟨m-n, by lia⟩) (by simp) (by simp; lia)
  | coe m =>
    rw [ha, Nat.cast_le] at h
    rw [height_eq_iSup_last_eq, iSup_subtype'] at ha
    obtain ⟨⟨p, hlast⟩, hlen⟩ := exists_eq_iSup_of_iSup_eq_coe ha
    simp only [Nat.cast_inj] at hlen
    use p.drop ⟨m-n, by lia⟩
    constructor
    · simp [hlast]
    · simp [hlen]; lia

Premises used: iSup_subtype', Nat.cast_inj, ENat.iSup_coe_eq_top, Nat.cast_le, Order.height, bddAbove_def, Order.height_eq_iSup_last_eq, rfl
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
h : (↑n : ℕ∞) ≤ coheight a
obtain :
  ∀ (p : LTSeries αᵒᵈ)
    (hp :
      RelSeries.last (r :=
          {x : αᵒᵈ × αᵒᵈ |
            match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
            | (a, b) => a < b})
          p =
        a)
    (hl :
      p.length (r :=
          {x : αᵒᵈ × αᵒᵈ |
            match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
            | (a, b) => a < b}) =
        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
⊢ ∃ (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

Tactic:
obtain ⟨p, hp, hl⟩ := exists_series_of_le_height (α := αᵒᵈ) a h

Premises used: Order.exists_series_of_le_height
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
h : (↑n : ℕ∞) ≤ coheight a
p : LTSeries αᵒᵈ
hp :
  RelSeries.last (r :=
      {x : αᵒᵈ × αᵒᵈ |
        match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
        | (a, b) => a < b})
      p =
    a
hl :
  p.length (r :=
      {x : αᵒᵈ × αᵒᵈ |
        match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
        | (a, b) => a < b}) =
    n
⊢ (RelSeries.reverse (r :=
          {x : αᵒᵈ × αᵒᵈ |
            match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
            | (a, b) => a < b})
          p).head
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    a

Tactic:
simpa
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
h : (↑n : ℕ∞) ≤ coheight a
p : LTSeries αᵒᵈ
hp :
  RelSeries.last (r :=
      {x : αᵒᵈ × αᵒᵈ |
        match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
        | (a, b) => a < b})
      p =
    a
hl :
  p.length (r :=
      {x : αᵒᵈ × αᵒᵈ |
        match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
        | (a, b) => a < b}) =
    n
⊢ (RelSeries.reverse (r :=
          {x : αᵒᵈ × αᵒᵈ |
            match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
            | (a, b) => a < b})
          p).length
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    n

Tactic:
simpa
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
h : (↑n : ℕ∞) ≤ coheight a
p : LTSeries αᵒᵈ
hp :
  RelSeries.last (r :=
      {x : αᵒᵈ × αᵒᵈ |
        match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
        | (a, b) => a < b})
      p =
    a
hl :
  p.length (r :=
      {x : αᵒᵈ × αᵒᵈ |
        match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
        | (a, b) => a < b}) =
    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

Tactic:
exact ⟨p.reverse, by simpa, by simpa⟩
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
h : height a = (↑n : ℕ∞)
⊢ ∃ (p : LTSeries α),
    RelSeries.last (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

Tactic:
exists_series_of_le_height a (le_of_eq h.symm)

Premises used: Order.exists_series_of_le_height, le_of_eq, Eq.symm
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
h : coheight a = (↑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

Tactic:
exists_series_of_le_coheight a (le_of_eq h.symm)

Premises used: Order.exists_series_of_le_coheight, le_of_eq, Eq.symm
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
a : height x ≤ ⨆ (y : α), ⨆ (_ : y < x), height y + 1
a₁ : ⨆ (y : α), ⨆ (_ : y < x), height y + 1 ≤ height x
⊢ height x = ⨆ (y : α), ⨆ (_ : y < x), height y + 1

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
a :
  ∀ (p : LTSeries α),
    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})) :
          ℕ∞)
        (⨆ (y : α), ⨆ (_ : y < x), height y + 1)
⊢ height x ≤ ⨆ (y : α), ⨆ (_ : y < x), height y + 1

Tactic:
apply height_le

Premises used: Order.height_le
-- 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
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    0
⊢ LE.le (α := ℕ∞) (↑0 : ℕ∞) (⨆ (y : α), ⨆ (_ : y < x), height y + 1)

Tactic:
simp
-- 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
n : ℕ
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    n + 1
a :
  LE.le (α := ℕ∞) (↑(n + 1) : ℕ∞)
    (⨆ (_ :
      (RelSeries.eraseLast (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p).last
          (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) <
        x),
      height
          ((RelSeries.eraseLast (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})
                p).last
            (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) +
        1)
⊢ LE.le (α := ℕ∞) (↑(n + 1) : ℕ∞) (⨆ (y : α), ⨆ (_ : y < x), height y + 1)

Tactic:
apply le_iSup_of_le p.eraseLast.last

Premises used: RelSeries.last, RelSeries.eraseLast, le_iSup_of_le
-- 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
n : ℕ
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    n + 1
rw :
  (RelSeries.eraseLast (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p).last
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) <
    RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p
⊢ (RelSeries.eraseLast (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p).last
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) <
    x

Tactic:
rw [← hp]
-- 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
n : ℕ
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    n + 1
⊢ p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0

Tactic:
lia
-- 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
n : ℕ
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    n + 1
⊢ (RelSeries.eraseLast (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p).last
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) <
    RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p

Tactic:
exact p.eraseLast_last_rel_last (by lia)

Premises used: RelSeries.eraseLast_last_rel_last
-- 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
n : ℕ
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    n + 1
a :
  (↑(n + 1) : ℕ∞) ≤
    height
        ((RelSeries.eraseLast (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p).last
          (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) +
      1
⊢ LE.le (α := ℕ∞) (↑(n + 1) : ℕ∞)
    (⨆ (_ :
      (RelSeries.eraseLast (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p).last
          (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) <
        x),
      height
          ((RelSeries.eraseLast (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})
                p).last
            (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) +
        1)

Tactic:
apply le_iSup_of_le (by rw [← hp]; exact p.eraseLast_last_rel_last (by lia))

Premises used: le_iSup_of_le
-- 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
n : ℕ
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    n + 1
a :
  LE.le (α := ℕ∞) (↑(n + 1) : ℕ∞)
    (⨆ (p_1 : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p_1 =
          (RelSeries.eraseLast (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})
                p).last
            (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})),
        HAdd.hAdd (α := ℕ∞)
          (↑(p_1.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞)
          1)
⊢ (↑(n + 1) : ℕ∞) ≤
    height
        ((RelSeries.eraseLast (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p).last
          (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) +
      1

Tactic:
rw [height_add_const]

Premises used: _private.0.Order.height_add_const
-- 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
n : ℕ
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    n + 1
⊢ (RelSeries.eraseLast (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p).last
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    (RelSeries.eraseLast (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p).last
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})

Tactic:
rfl
-- 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
n : ℕ
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    n + 1
⊢ (↑(n + 1) : ℕ∞) ≤
    HAdd.hAdd (α := ℕ∞)
      (↑((RelSeries.eraseLast (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})
                p).length
            (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
      1

Tactic:
simp [hlen]
-- 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
n : ℕ
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    n + 1
⊢ LE.le (α := ℕ∞) (↑(n + 1) : ℕ∞)
    (⨆ (p_1 : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p_1 =
          (RelSeries.eraseLast (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})
                p).last
            (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})),
        HAdd.hAdd (α := ℕ∞)
          (↑(p_1.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞)
          1)

Tactic:
apply le_iSup₂_of_le p.eraseLast (by rfl) (by simp [hlen])

Premises used: RelSeries.eraseLast, le_iSup₂_of_le
-- 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
a :
  ∀ (x_1 : ℕ)
    (hlen :
      p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        x_1),
    LE.le (α := ℕ∞) (↑x_1 : ℕ∞) (⨆ (y : α), ⨆ (_ : y < x), height y + 1)
⊢ LE.le (α := ℕ∞)
    (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)
    (⨆ (y : α), ⨆ (_ : y < x), height y + 1)

Tactic:
cases hlen : p.length with
    | zero => simp
    | succ n =>
      apply le_iSup_of_le p.eraseLast.last
      apply le_iSup_of_le (by rw [← hp]; exact p.eraseLast_last_rel_last (by lia))
      rw [height_add_const]
      apply le_iSup₂_of_le p.eraseLast (by rfl) (by simp [hlen])

Premises used: Order.succ, RelSeries.last, RelSeries.length, RelSeries.eraseLast, _private.0.Order.height_add_const, le_iSup_of_le, le_iSup₂_of_le
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
a : ∀ (i : α) (j : i < x), height i + 1 ≤ height x
⊢ ⨆ (y : α), ⨆ (_ : y < x), height y + 1 ≤ height x

Tactic:
apply iSup₂_le

Premises used: iSup₂_le
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x y : α
hyx : y < x
a :
  ⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          y),
        HAdd.hAdd (α := ℕ∞)
          (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞)
          1 ≤
    height x
⊢ height y + 1 ≤ height x

Tactic:
rw [height_add_const]

Premises used: _private.0.Order.height_add_const
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x y : α
hyx : y < x
a :
  ∀ (i : LTSeries α)
    (j :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          i =
        y),
    HAdd.hAdd (α := ℕ∞)
        (↑(i.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞)
        1 ≤
      height x
⊢ ⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          y),
        HAdd.hAdd (α := ℕ∞)
          (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞)
          1 ≤
    height x

Tactic:
apply iSup₂_le

Premises used: iSup₂_le
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x y : α
hyx : y < x
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    y
⊢ (RelSeries.snoc (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p x ⋯).last
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≤
    x

Tactic:
simp
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x y : α
hyx : y < x
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    y
⊢ HAdd.hAdd (α := ℕ∞)
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
      1 ≤
    (↑((RelSeries.snoc (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p x ⋯).length
          (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)

Tactic:
simp