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 }
ha :
  ¬∃ (x : ℕ),
      ∀ (y : ℕ),
        Membership.mem (γ := Set ℕ)
            (Set.range
              fun
                (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}))
            y →
          y ≤ x
top :
  ∀
    (ha :
      ∀ (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),
    ∃ (x : ℕ),
      ∀ (y : ℕ),
        Membership.mem (γ := Set ℕ)
            (Set.range
              fun
                (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}))
            y →
          y ≤ 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

Tactic:
contrapose! ha
-- 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 }
ha :
  ∀ (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
h :
  ∀ (y : ℕ),
    Membership.mem (γ := Set ℕ)
        (Set.range
          fun
            (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}))
        y →
      y ≤ n
⊢ ∃ (x : ℕ),
    ∀ (y : ℕ),
      Membership.mem (γ := Set ℕ)
          (Set.range
            fun
              (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}))
          y →
        y ≤ x

Tactic:
use n
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
n m : ℕ
p : LTSeries α
hne :
  Nonempty.{max 1 (u_1 + 1)}
    { p_1 : LTSeries α //
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p_1 =
        RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p }
ha :
  ∀ (p_1 : LTSeries α)
    (_ :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p_1 =
        RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p),
    p_1.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) ≠
      n
hp : p.length (r := {x : α × α | x.1 < x.2}) = m
h : ∀ (hnm : n < m), False
⊢ m ≤ n

Tactic:
by_contra! hnm
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
n m : ℕ
p : LTSeries α
hne :
  Nonempty.{max 1 (u_1 + 1)}
    { p_1 : LTSeries α //
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p_1 =
        RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p }
ha :
  ∀ (p_1 : LTSeries α)
    (_ :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p_1 =
        RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p),
    p_1.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) ≠
      n
hp : p.length (r := {x : α × α | x.1 < x.2}) = m
hnm : n < m
⊢ m - n <
    p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1

Tactic:
lia
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
n m : ℕ
p : LTSeries α
hne :
  Nonempty.{max 1 (u_1 + 1)}
    { p_1 : LTSeries α //
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p_1 =
        RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p }
ha :
  ∀ (p_1 : LTSeries α)
    (_ :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p_1 =
        RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p),
    p_1.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) ≠
      n
hp : p.length (r := {x : α × α | x.1 < x.2}) = m
hnm : n < m
⊢ (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))).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:
simp
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
n m : ℕ
p : LTSeries α
hne :
  Nonempty.{max 1 (u_1 + 1)}
    { p_1 : LTSeries α //
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p_1 =
        RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p }
ha :
  ∀ (p_1 : LTSeries α)
    (_ :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p_1 =
        RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p),
    p_1.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) ≠
      n
hp : p.length (r := {x : α × α | x.1 < x.2}) = m
hnm : n < m
⊢ p.length (r := {x : α × α | x.1 < x.2}) - (m - n) = n

Tactic:
lia
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
n m : ℕ
p : LTSeries α
hne :
  Nonempty.{max 1 (u_1 + 1)}
    { p_1 : LTSeries α //
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p_1 =
        RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p }
ha :
  ∀ (p_1 : LTSeries α)
    (_ :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p_1 =
        RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p),
    p_1.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) ≠
      n
hp : p.length (r := {x : α × α | x.1 < x.2}) = m
hnm : n < m
⊢ False

Tactic:
apply ha (p.drop ⟨m-n, by lia⟩) (by simp) (by simp; lia)

Premises used: HSub.hSub, Fin.mk, RelSeries.drop
-- 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 }
m : ℕ
ha : height a = (↑m : ℕ∞)
⊢ n ≤ m

Tactic:
rw [ha, Nat.cast_le] at h

Premises used: Nat.cast_le
-- 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 }
m : ℕ
ha : height a = (↑m : ℕ∞)
h₁ : n ≤ m
⊢ height a = (↑m : ℕ∞)

Tactic:
rw [ha, Nat.cast_le] at h

Premises used: Nat.cast_le
-- 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 : height a = (↑m : ℕ∞)
⊢ 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 : ℕ∞)

Tactic:
rw [height_eq_iSup_last_eq, iSup_subtype'] at ha

Premises used: iSup_subtype', Order.height_eq_iSup_last_eq
-- 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 : ℕ∞)
coe :
  ∀ (p : LTSeries α)
    (hlast :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a)
    (hlen :
      Eq (α := ℕ∞)
        (↑((↑(Subtype.mk (p := fun (p : LTSeries α) ↦
                      RelSeries.last (r :=
                          {x : α × α |
                            match (motive := α × α → Prop) x with
                            | (a, b) => a < b})
                          p =
                        a)
                      p hlast) :
                  LTSeries α).length
              (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞)
        (↑m : ℕ∞)),
    ∃ (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:
obtain ⟨⟨p, hlast⟩, hlen⟩ := exists_eq_iSup_of_iSup_eq_coe ha

Premises used: _private.0.Order.exists_eq_iSup_of_iSup_eq_coe
-- 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 :
  Eq (α := ℕ∞)
    (↑((↑(Subtype.mk (p := fun (p : LTSeries α) ↦
                  RelSeries.last (r :=
                      {x : α × α |
                        match (motive := α × α → Prop) x with
                        | (a, b) => a < b})
                      p =
                    a)
                  p hlast) :
              LTSeries α).length
          (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)
    (↑m : ℕ∞)
⊢ p.length (r := {x : α × α | x.1 < x.2}) = m

Tactic:
simp only [Nat.cast_inj] at hlen

Premises used: Nat.cast_inj
-- 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 - n <
    p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1

Tactic:
lia
-- 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₁ :
  (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))).last
        (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) =
      a ∧
    (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
⊢ ∃ (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:
use p.drop ⟨m-n, by lia⟩

Premises used: HSub.hSub, Fin.mk, RelSeries.drop
-- 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₁ :
  (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))).last
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    a
h₂ :
  (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
⊢ (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))).last
        (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) =
      a ∧
    (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:
constructor
-- 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
⊢ (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))).last
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    a

Tactic:
simp [hlast]