awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
x : α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
hlen0 :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
p' : RelSeries (α := α)
  {x : α × α |
    match (motive := α × α → Prop) x with
    | (a, b) => a < b} :=
  (RelSeries.eraseLast (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p).snoc
    (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    x ⋯
pos :
  (↑(p'.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x
⊢ (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x

Tactic:
suffices p'.length ≤ height x by
      simp only [RelSeries.snoc_length, RelSeries.eraseLast_length, Nat.cast_add, ENat.coe_sub,
        Nat.cast_one, p'] at this
      convert! this
      norm_cast
      lia
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
x : α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
hlen0 :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
p' : RelSeries (α := α)
  {x : α × α |
    match (motive := α × α → Prop) x with
    | (a, b) => a < b} :=
  (RelSeries.eraseLast (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p).snoc
    (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    x ⋯
⊢ (↑(p'.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x

Tactic:
le_iSup₂_of_le p' ?_ le_rfl

Premises used: le_rfl, le_iSup₂_of_le, Order.height
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
x : α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
hlen0 :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
p' : RelSeries (α := α)
  {x : α × α |
    match (motive := α × α → Prop) x with
    | (a, b) => a < b} :=
  (RelSeries.eraseLast (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p).snoc
    (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    x ⋯
pos :
  p'.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≤
    x
⊢ (↑(p'.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x

Tactic:
refine le_iSup₂_of_le p' ?_ le_rfl

Premises used: le_rfl, le_iSup₂_of_le
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
x : α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
hlen0 :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
p' : RelSeries (α := α)
  {x : α × α |
    match (motive := α × α → Prop) x with
    | (a, b) => a < b} :=
  (RelSeries.eraseLast (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p).snoc
    (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    x ⋯
⊢ p'.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≤
    x

Tactic:
simp [p']
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
x : α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
hlen0 :
  ¬p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) ≠
      0
⊢ (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x

Tactic:
simp_all
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries α
hhead :
  x ≤
    RelSeries.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p
⊢ (RelSeries.reverse (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:
simpa
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
⊢ (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height
      (RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p)

Tactic:
length_le_height le_rfl

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

Tactic:
length_le_coheight le_rfl

Premises used: Order.length_le_coheight, le_rfl
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
i :
  Fin
    (p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1)
⊢ (↑(↑i : ℕ) : ℕ∞) ≤
    height
      (p.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        i)

Tactic:
length_le_height_last (p := p.take i)

Premises used: RelSeries.last, Order.length_le_height_last
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
i :
  Fin
    (p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1)
⊢ (↑(↑i.rev : ℕ) : ℕ∞) ≤
    coheight
      (p.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        i)

Tactic:
simpa using index_le_height (α := αᵒᵈ) p.reverse i.rev

Premises used: RelSeries.reverse, Fin.rev, Order.index_le_height
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
h :
  (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) =
    height
      (RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p)
i :
  Fin
    (p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1)
⊢ height
      (p.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        i) =
    (↑(↑i : ℕ) : ℕ∞)

Tactic:
le_antisymm (height_le ?_) (index_le_height p i)

Premises used: Order.height_le, le_antisymm, Order.index_le_height
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
h :
  (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) =
    height
      (RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p)
i :
  Fin
    (p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1)
refine :
  ∀ (p_1 : LTSeries α),
    RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p_1 =
        p.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          i →
      LE.le (α := ℕ∞)
        (↑(p_1.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞)
        (↑(↑i : ℕ) : ℕ∞)
⊢ height
      (p.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        i) =
    (↑(↑i : ℕ) : ℕ∞)

Tactic:
refine le_antisymm (height_le ?_) (index_le_height p i)

Premises used: Order.height_le, le_antisymm, Order.index_le_height
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
h :
  (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) =
    height
      (RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p)
i :
  Fin
    (p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1)
p' : LTSeries α
hp' :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p' =
    p.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      i
⊢ RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p' =
    (RelSeries.drop (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p i).head
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})

Tactic:
simpa
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
h :
  (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) =
    height
      (RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p)
i :
  Fin
    (p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1)
p' : LTSeries α
hp' :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p' =
    p.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      i
⊢ (↑((RelSeries.smash (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p'
              (RelSeries.drop (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})
                p i)
              ⋯).length
          (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height
      ((RelSeries.smash (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p'
            (RelSeries.drop (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p i)
            ⋯).last
        (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}))

Tactic:
have hp'' := length_le_height_last (p := p'.smash (p.drop i) (by simpa))
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
h :
  (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) =
    height
      (RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p)
i :
  Fin
    (p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1)
p' : LTSeries α
hp' :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p' =
    p.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      i
hp'' :
  (↑((RelSeries.smash (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p'
              (RelSeries.drop (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})
                p i)
              ⋯).length
          (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height
      ((RelSeries.smash (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p'
            (RelSeries.drop (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p i)
            ⋯).last
        (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}))
⊢ (↑(p'.length (r := {x : α × α | x.1 < x.2})) : ℕ∞) +
      HSub.hSub (α := ℕ∞) (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞) (↑(↑i : ℕ) : ℕ∞) ≤
    (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞)

Tactic:
simp [← h] at hp''
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
i :
  Fin
    (p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1)
p' : LTSeries α
hp' :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p' =
    p.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      i
hp'' :
  (↑(p'.length (r := {x : α × α | x.1 < x.2})) : ℕ∞) +
      HSub.hSub (α := ℕ∞) (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞) (↑(↑i : ℕ) : ℕ∞) ≤
    (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞)
norm_cast :
  ∀
    (hp'' :
      p'.length (r := {x : α × α | x.1 < x.2}) + (p.length (r := {x : α × α | x.1 < x.2}) - (↑i : ℕ)) ≤
        p.length (r := {x : α × α | x.1 < x.2})),
    p'.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) ≤
      (↑i : ℕ)
⊢ LE.le (α := ℕ∞)
    (↑(p'.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)
    (↑(↑i : ℕ) : ℕ∞)

Tactic:
norm_cast at *
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
i :
  Fin
    (p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1)
p' : LTSeries α
hp' :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p' =
    p.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      i
hp'' :
  p'.length (r := {x : α × α | x.1 < x.2}) + (p.length (r := {x : α × α | x.1 < x.2}) - (↑i : ℕ)) ≤
    p.length (r := {x : α × α | x.1 < x.2})
⊢ p'.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≤
    (↑i : ℕ)

Tactic:
lia
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
h :
  (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) =
    coheight
      (RelSeries.head (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p)
i :
  Fin
    (p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1)
⊢ (↑((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})) :
      ℕ∞) =
    height
      ((RelSeries.reverse (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:
simpa
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
h :
  (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) =
    coheight
      (RelSeries.head (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p)
i :
  Fin
    (p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1)
⊢ coheight
      (p.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        i) =
    (↑(↑i.rev : ℕ) : ℕ∞)

Tactic:
simpa using height_eq_index_of_length_eq_height_last (α := αᵒᵈ) (p := p.reverse) (by simpa) i.rev

Premises used: Fin.rev, Order.height_eq_index_of_length_eq_height_last
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
⊢ Monotone.{u_1, 0} (α := α) height

Tactic:
fun _ _ hab ↦ biSup_mono (fun _ hla => hla.trans hab)

Premises used: biSup_mono, Monotone, LE.le.trans, Order.height
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
⊢ Antitone.{u_1, 0} (α := α) coheight

Tactic:
(height_mono (α := αᵒᵈ)).dual_left

Premises used: iSup, Monotone.dual_left, Order.height_mono, OrderDual, Order.height, Order.coheight
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
⊢ Nonempty.{max 1 (u_1 + 1)}
    { p : LTSeries α //
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a }

Tactic:
have hne : Nonempty { p : LTSeries α // p.last = a } := ⟨RelSeries.singleton _ a, rfl⟩
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
rw :
  ∀ (i : LTSeries α)
    (j :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          i =
        x),
    HAdd.hAdd (α := ℕ∞)
        (↑(i.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞)
        1 ≤
      height y
⊢ height x < height y

Tactic:
rw [← ENat.add_one_le_iff hfin.ne, height_add_const, iSup₂_le_iff]

Premises used: ENat.add_one_le_iff, _private.0.Order.height_add_const, iSup₂_le_iff, LT.lt.ne
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
p : LTSeries α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
⊢ Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p,
      y)

Tactic:
simp [*]
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
p : LTSeries α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
⊢ (↑((RelSeries.snoc (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p y ⋯).length
          (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height
      ((RelSeries.snoc (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p y ⋯).last
        (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}))

Tactic:
have := length_le_height_last (p := p.snoc y (by simp [*]))
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
p : LTSeries α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
this :
  (↑((RelSeries.snoc (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p y ⋯).length
          (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height
      ((RelSeries.snoc (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p y ⋯).last
        (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}))
⊢ HAdd.hAdd (α := ℕ∞)
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
      1 ≤
    height y

Tactic:
simpa using this
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : a < b
hfin : height a = ⊤
rw : height a ≤ height b
⊢ ⊤ ≤ height b

Tactic:
rw [← hfin]
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : a < b
hfin : height a = ⊤
⊢ height a ≤ height b

Tactic:
gcongr
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : a < b
hfin : height a = ⊤
⊢ ⊤ ≤ height b

Tactic:
have : ⊤ ≤ height b := by
      rw [← hfin]
      gcongr
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : a < b
hfin : height a = ⊤
this : ⊤ ≤ height b
⊢ HAdd.hAdd (α := ℕ∞) ⊤ 1 ≤ height b

Tactic:
simp [this]
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : a < b
n : ℕ
hfin : height a = (↑n : ℕ∞)
coe : (↑n : ℕ∞) < height b
⊢ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ height b

Tactic:
apply Order.add_one_le_of_lt

Premises used: Order.add_one_le_of_lt
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : a < b
n : ℕ
hfin : height a = (↑n : ℕ∞)
coe : height a < height b
⊢ (↑n : ℕ∞) < height b

Tactic:
rw [← hfin]
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : a < b
n : ℕ
hfin : height a = (↑n : ℕ∞)
coe : height a < ⊤
⊢ height a < height b

Tactic:
gcongr
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : a < b
n : ℕ
hfin : height a = (↑n : ℕ∞)
⊢ height a < ⊤

Tactic:
simp [hfin]