awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.RelSeries
Goal:
p : LTSeries ℕ
i_1 j_1 :
  Fin
    (p.length (r :=
        {x : ℕ × ℕ |
          match (motive := ℕ × ℕ → Prop) x with
          | (a, b) => a < b}) +
      1)
i : ℕ
hi :
  i <
    p.length (r :=
        {x : ℕ × ℕ |
          match (motive := ℕ × ℕ → Prop) x with
          | (a, b) => a < b}) +
      1
j : ℕ
hj :
  i <
    p.length (r :=
        {x : ℕ × ℕ |
          match (motive := ℕ × ℕ → Prop) x with
          | (a, b) => a < b}) +
      1
⊢ p.toFun (r := {x : ℕ × ℕ | x.1 < x.2}) (⟨i, hi⟩ : Fin (p.length (r := {x : ℕ × ℕ | x.1 < x.2}) + 1)) + i ≤
    p.toFun (r := {x : ℕ × ℕ | x.1 < x.2}) (⟨i, hj⟩ : Fin (p.length (r := {x : ℕ × ℕ | x.1 < x.2}) + 1)) + i

Tactic:
simp
-- Module: Mathlib.Order.RelSeries
Goal:
p : LTSeries ℕ
i_1 j_1 :
  Fin
    (p.length (r :=
        {x : ℕ × ℕ |
          match (motive := ℕ × ℕ → Prop) x with
          | (a, b) => a < b}) +
      1)
i : ℕ
hi :
  i <
    p.length (r :=
        {x : ℕ × ℕ |
          match (motive := ℕ × ℕ → Prop) x with
          | (a, b) => a < b}) +
      1
j_2 j : ℕ
_hij : i ≤ j
ih :
  ∀
    (hj :
      j <
        p.length (r :=
            {x : ℕ × ℕ |
              match (motive := ℕ × ℕ → Prop) x with
              | (a, b) => a < b}) +
          1),
    p.toFun (r := {x : ℕ × ℕ | x.1 < x.2}) (⟨i, hi⟩ : Fin (p.length (r := {x : ℕ × ℕ | x.1 < x.2}) + 1)) + j ≤
      p.toFun (r := {x : ℕ × ℕ | x.1 < x.2}) (⟨j, hj⟩ : Fin (p.length (r := {x : ℕ × ℕ | x.1 < x.2}) + 1)) + i
hj :
  j + 1 <
    p.length (r :=
        {x : ℕ × ℕ |
          match (motive := ℕ × ℕ → Prop) x with
          | (a, b) => a < b}) +
      1
⊢ p.toFun (r := {x : ℕ × ℕ | x.1 < x.2}) (⟨i, hi⟩ : Fin (p.length (r := {x : ℕ × ℕ | x.1 < x.2}) + 1)) + j ≤
    p.toFun (r := {x : ℕ × ℕ | x.1 < x.2}) (⟨j, ⋯⟩ : Fin (p.length (r := {x : ℕ × ℕ | x.1 < x.2}) + 1)) + i

Tactic:
specialize ih (Nat.lt_of_succ_lt hj)

Premises used: Nat.lt_of_succ_lt
-- Module: Mathlib.Order.RelSeries
Goal:
p : LTSeries ℕ
i_1 j_1 :
  Fin
    (p.length (r :=
        {x : ℕ × ℕ |
          match (motive := ℕ × ℕ → Prop) x with
          | (a, b) => a < b}) +
      1)
i : ℕ
hi :
  i <
    p.length (r :=
        {x : ℕ × ℕ |
          match (motive := ℕ × ℕ → Prop) x with
          | (a, b) => a < b}) +
      1
j_2 j : ℕ
_hij : i ≤ j
hj :
  j + 1 <
    p.length (r :=
        {x : ℕ × ℕ |
          match (motive := ℕ × ℕ → Prop) x with
          | (a, b) => a < b}) +
      1
ih :
  p.toFun (r := {x : ℕ × ℕ | x.1 < x.2}) (⟨i, hi⟩ : Fin (p.length (r := {x : ℕ × ℕ | x.1 < x.2}) + 1)) + j ≤
    p.toFun (r := {x : ℕ × ℕ | x.1 < x.2}) (⟨j, ⋯⟩ : Fin (p.length (r := {x : ℕ × ℕ | x.1 < x.2}) + 1)) + i
⊢ j <
    p.length (r :=
      {x : ℕ × ℕ |
        match (motive := ℕ × ℕ → Prop) x with
        | (a, b) => a < b})

Tactic:
lia
-- Module: Mathlib.Order.RelSeries
Goal:
p : LTSeries ℕ
i_1 j_1 :
  Fin
    (p.length (r :=
        {x : ℕ × ℕ |
          match (motive := ℕ × ℕ → Prop) x with
          | (a, b) => a < b}) +
      1)
i : ℕ
hi :
  i <
    p.length (r :=
        {x : ℕ × ℕ |
          match (motive := ℕ × ℕ → Prop) x with
          | (a, b) => a < b}) +
      1
j_2 j : ℕ
_hij : i ≤ j
hj :
  j + 1 <
    p.length (r :=
        {x : ℕ × ℕ |
          match (motive := ℕ × ℕ → Prop) x with
          | (a, b) => a < b}) +
      1
ih :
  p.toFun (r := {x : ℕ × ℕ | x.1 < x.2}) (⟨i, hi⟩ : Fin (p.length (r := {x : ℕ × ℕ | x.1 < x.2}) + 1)) + j ≤
    p.toFun (r := {x : ℕ × ℕ | x.1 < x.2}) (⟨j, ⋯⟩ : Fin (p.length (r := {x : ℕ × ℕ | x.1 < x.2}) + 1)) + i
⊢ p.toFun (r :=
      {x : ℕ × ℕ |
        match (motive := ℕ × ℕ → Prop) x with
        | (a, b) => a < b})
      (⟨j, ⋯⟩ :
        Fin
          (p.length (r :=
              {x : ℕ × ℕ |
                match (motive := ℕ × ℕ → Prop) x with
                | (a, b) => a < b}) +
            1)) <
    p.toFun (r :=
      {x : ℕ × ℕ |
        match (motive := ℕ × ℕ → Prop) x with
        | (a, b) => a < b})
      ⟨j + 1, ⋯⟩

Tactic:
have step : p ⟨j, _⟩ < p ⟨j + 1, _⟩ := p.step ⟨j, by lia⟩
-- Module: Mathlib.Order.RelSeries
Goal:
p : LTSeries ℕ
i_1 j_1 :
  Fin
    (p.length (r :=
        {x : ℕ × ℕ |
          match (motive := ℕ × ℕ → Prop) x with
          | (a, b) => a < b}) +
      1)
i : ℕ
hi :
  i <
    p.length (r :=
        {x : ℕ × ℕ |
          match (motive := ℕ × ℕ → Prop) x with
          | (a, b) => a < b}) +
      1
j_2 j : ℕ
_hij : i ≤ j
hj :
  j + 1 <
    p.length (r :=
        {x : ℕ × ℕ |
          match (motive := ℕ × ℕ → Prop) x with
          | (a, b) => a < b}) +
      1
ih :
  p.toFun (r := {x : ℕ × ℕ | x.1 < x.2}) (⟨i, hi⟩ : Fin (p.length (r := {x : ℕ × ℕ | x.1 < x.2}) + 1)) + j ≤
    p.toFun (r := {x : ℕ × ℕ | x.1 < x.2}) (⟨j, ⋯⟩ : Fin (p.length (r := {x : ℕ × ℕ | x.1 < x.2}) + 1)) + i
step :
  p.toFun (r :=
      {x : ℕ × ℕ |
        match (motive := ℕ × ℕ → Prop) x with
        | (a, b) => a < b})
      (⟨j, ⋯⟩ :
        Fin
          (p.length (r :=
              {x : ℕ × ℕ |
                match (motive := ℕ × ℕ → Prop) x with
                | (a, b) => a < b}) +
            1)) <
    p.toFun (r :=
      {x : ℕ × ℕ |
        match (motive := ℕ × ℕ → Prop) x with
        | (a, b) => a < b})
      ⟨j + 1, ⋯⟩
⊢ p.toFun (r := {x : ℕ × ℕ | x.1 < x.2}) (⟨i, hi⟩ : Fin (p.length (r := {x : ℕ × ℕ | x.1 < x.2}) + 1)) + (j + 1) ≤
    p.toFun (r := {x : ℕ × ℕ | x.1 < x.2}) (⟨j + 1, hj⟩ : Fin (p.length (r := {x : ℕ × ℕ | x.1 < x.2}) + 1)) + i

Tactic:
lia
-- Module: Mathlib.Order.RelSeries
Goal:
p : LTSeries ℕ
i_1 j_1 :
  Fin
    (p.length (r :=
        {x : ℕ × ℕ |
          match (motive := ℕ × ℕ → Prop) x with
          | (a, b) => a < b}) +
      1)
i : ℕ
hi :
  i <
    p.length (r :=
        {x : ℕ × ℕ |
          match (motive := ℕ × ℕ → Prop) x with
          | (a, b) => a < b}) +
      1
j : ℕ
hj :
  j <
    p.length (r :=
        {x : ℕ × ℕ |
          match (motive := ℕ × ℕ → Prop) x with
          | (a, b) => a < b}) +
      1
hij : i ≤ j
base :
  ∀
    (hj :
      i <
        p.length (r :=
            {x : ℕ × ℕ |
              match (motive := ℕ × ℕ → Prop) x with
              | (a, b) => a < b}) +
          1),
    p.toFun (r := {x : ℕ × ℕ | x.1 < x.2}) (⟨i, hi⟩ : Fin (p.length (r := {x : ℕ × ℕ | x.1 < x.2}) + 1)) + i ≤
      p.toFun (r := {x : ℕ × ℕ | x.1 < x.2}) (⟨i, hj⟩ : Fin (p.length (r := {x : ℕ × ℕ | x.1 < x.2}) + 1)) + i
succ :
  ∀ (j : ℕ) (_hij : i ≤ j)
    (ih :
      ∀
        (hj :
          j <
            p.length (r :=
                {x : ℕ × ℕ |
                  match (motive := ℕ × ℕ → Prop) x with
                  | (a, b) => a < b}) +
              1),
        p.toFun (r := {x : ℕ × ℕ | x.1 < x.2}) (⟨i, hi⟩ : Fin (p.length (r := {x : ℕ × ℕ | x.1 < x.2}) + 1)) + j ≤
          p.toFun (r := {x : ℕ × ℕ | x.1 < x.2}) (⟨j, hj⟩ : Fin (p.length (r := {x : ℕ × ℕ | x.1 < x.2}) + 1)) + i)
    (hj :
      j + 1 <
        p.length (r :=
            {x : ℕ × ℕ |
              match (motive := ℕ × ℕ → Prop) x with
              | (a, b) => a < b}) +
          1),
    p.toFun (r := {x : ℕ × ℕ | x.1 < x.2}) (⟨i, hi⟩ : Fin (p.length (r := {x : ℕ × ℕ | x.1 < x.2}) + 1)) + (j + 1) ≤
      p.toFun (r := {x : ℕ × ℕ | x.1 < x.2}) (⟨j + 1, hj⟩ : Fin (p.length (r := {x : ℕ × ℕ | x.1 < x.2}) + 1)) + i
⊢ p.toFun (r := {x : ℕ × ℕ | x.1 < x.2}) (⟨i, hi⟩ : Fin (p.length (r := {x : ℕ × ℕ | x.1 < x.2}) + 1)) + j ≤
    p.toFun (r := {x : ℕ × ℕ | x.1 < x.2}) (⟨j, hj⟩ : Fin (p.length (r := {x : ℕ × ℕ | x.1 < x.2}) + 1)) + i

Tactic:
induction j, hij using Nat.le_induction with
  | base => simp
  | succ j _hij ih =>
    specialize ih (Nat.lt_of_succ_lt hj)
    have step : p ⟨j, _⟩ < p ⟨j + 1, _⟩ := p.step ⟨j, by lia⟩
    norm_cast at *; lia
-- Module: Mathlib.Order.RelSeries
Goal:
p : LTSeries ℤ
i j :
  Fin
    (p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1)
hij : i ≤ j
have :
  ∀ (i : ℕ)
    (hi :
      i <
        p.length (r :=
            {x : ℤ × ℤ |
              match (motive := ℤ × ℤ → Prop) x with
              | (a, b) => a < b}) +
          1)
    (hij :
      (⟨i, hi⟩ :
          Fin
            (p.length (r :=
                {x : ℤ × ℤ |
                  match (motive := ℤ × ℤ → Prop) x with
                  | (a, b) => a < b}) +
              1)) ≤
        j),
    p.toFun (r :=
          {x : ℤ × ℤ |
            match (motive := ℤ × ℤ → Prop) x with
            | (a, b) => a < b})
          (⟨i, hi⟩ :
            Fin
              (p.length (r :=
                  {x : ℤ × ℤ |
                    match (motive := ℤ × ℤ → Prop) x with
                    | (a, b) => a < b}) +
                1)) +
        (↑(↑j : ℕ) : ℤ) ≤
      p.toFun (r :=
          {x : ℤ × ℤ |
            match (motive := ℤ × ℤ → Prop) x with
            | (a, b) => a < b})
          j +
        (↑(↑(⟨i, hi⟩ :
                  Fin
                    (p.length (r :=
                        {x : ℤ × ℤ |
                          match (motive := ℤ × ℤ → Prop) x with
                          | (a, b) => a < b}) +
                      1)) :
              ℕ) :
          ℤ)
⊢ p.toFun (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b})
        i +
      (↑(↑j : ℕ) : ℤ) ≤
    p.toFun (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b})
        j +
      (↑(↑i : ℕ) : ℤ)

Tactic:
have ⟨i, hi⟩ := i
-- Module: Mathlib.Order.RelSeries
Goal:
p : LTSeries ℤ
i_1 j :
  Fin
    (p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1)
i : ℕ
hi :
  i <
    p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1
hij :
  (⟨i, hi⟩ :
      Fin
        (p.length (r :=
            {x : ℤ × ℤ |
              match (motive := ℤ × ℤ → Prop) x with
              | (a, b) => a < b}) +
          1)) ≤
    j
have :
  ∀ (j : ℕ)
    (hj :
      j <
        p.length (r :=
            {x : ℤ × ℤ |
              match (motive := ℤ × ℤ → Prop) x with
              | (a, b) => a < b}) +
          1)
    (hij :
      (⟨i, hi⟩ :
          Fin
            (p.length (r :=
                {x : ℤ × ℤ |
                  match (motive := ℤ × ℤ → Prop) x with
                  | (a, b) => a < b}) +
              1)) ≤
        ⟨j, hj⟩),
    p.toFun (r :=
          {x : ℤ × ℤ |
            match (motive := ℤ × ℤ → Prop) x with
            | (a, b) => a < b})
          (⟨i, hi⟩ :
            Fin
              (p.length (r :=
                  {x : ℤ × ℤ |
                    match (motive := ℤ × ℤ → Prop) x with
                    | (a, b) => a < b}) +
                1)) +
        (↑(↑(⟨j, hj⟩ :
                  Fin
                    (p.length (r :=
                        {x : ℤ × ℤ |
                          match (motive := ℤ × ℤ → Prop) x with
                          | (a, b) => a < b}) +
                      1)) :
              ℕ) :
          ℤ) ≤
      p.toFun (r :=
          {x : ℤ × ℤ |
            match (motive := ℤ × ℤ → Prop) x with
            | (a, b) => a < b})
          (⟨j, hj⟩ :
            Fin
              (p.length (r :=
                  {x : ℤ × ℤ |
                    match (motive := ℤ × ℤ → Prop) x with
                    | (a, b) => a < b}) +
                1)) +
        (↑(↑(⟨i, hi⟩ :
                  Fin
                    (p.length (r :=
                        {x : ℤ × ℤ |
                          match (motive := ℤ × ℤ → Prop) x with
                          | (a, b) => a < b}) +
                      1)) :
              ℕ) :
          ℤ)
⊢ p.toFun (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b})
        (⟨i, hi⟩ :
          Fin
            (p.length (r :=
                {x : ℤ × ℤ |
                  match (motive := ℤ × ℤ → Prop) x with
                  | (a, b) => a < b}) +
              1)) +
      (↑(↑j : ℕ) : ℤ) ≤
    p.toFun (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b})
        j +
      (↑(↑(⟨i, hi⟩ :
                Fin
                  (p.length (r :=
                      {x : ℤ × ℤ |
                        match (motive := ℤ × ℤ → Prop) x with
                        | (a, b) => a < b}) +
                    1)) :
            ℕ) :
        ℤ)

Tactic:
have ⟨j, hj⟩ := j
-- Module: Mathlib.Order.RelSeries
Goal:
p : LTSeries ℤ
i_1 j_1 :
  Fin
    (p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1)
i : ℕ
hi :
  i <
    p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1
j : ℕ
hj :
  j <
    p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1
hij :
  (⟨i, hi⟩ :
      Fin
        (p.length (r :=
            {x : ℤ × ℤ |
              match (motive := ℤ × ℤ → Prop) x with
              | (a, b) => a < b}) +
          1)) ≤
    ⟨j, hj⟩
⊢ i ≤ j

Tactic:
simp only [Fin.mk_le_mk] at hij

Premises used: Fin.mk_le_mk
-- Module: Mathlib.Order.RelSeries
Goal:
p : LTSeries ℤ
i_1 j_1 :
  Fin
    (p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1)
i : ℕ
hi :
  i <
    p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1
j : ℕ
hj :
  j <
    p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1
hij : i ≤ j
simp :
  p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨i, hi⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) + (↑j : ℤ) ≤
    p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨j, hj⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) + (↑i : ℤ)
⊢ p.toFun (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b})
        (⟨i, hi⟩ :
          Fin
            (p.length (r :=
                {x : ℤ × ℤ |
                  match (motive := ℤ × ℤ → Prop) x with
                  | (a, b) => a < b}) +
              1)) +
      (↑(↑(⟨j, hj⟩ :
                Fin
                  (p.length (r :=
                      {x : ℤ × ℤ |
                        match (motive := ℤ × ℤ → Prop) x with
                        | (a, b) => a < b}) +
                    1)) :
            ℕ) :
        ℤ) ≤
    p.toFun (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b})
        (⟨j, hj⟩ :
          Fin
            (p.length (r :=
                {x : ℤ × ℤ |
                  match (motive := ℤ × ℤ → Prop) x with
                  | (a, b) => a < b}) +
              1)) +
      (↑(↑(⟨i, hi⟩ :
                Fin
                  (p.length (r :=
                      {x : ℤ × ℤ |
                        match (motive := ℤ × ℤ → Prop) x with
                        | (a, b) => a < b}) +
                    1)) :
            ℕ) :
        ℤ)

Tactic:
simp only at *
-- Module: Mathlib.Order.RelSeries
Goal:
p : LTSeries ℤ
i_1 j_1 :
  Fin
    (p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1)
i : ℕ
hi :
  i <
    p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1
j : ℕ
hj :
  i <
    p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1
⊢ p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨i, hi⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) + (↑i : ℤ) ≤
    p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨i, hj⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) + (↑i : ℤ)

Tactic:
simp
-- Module: Mathlib.Order.RelSeries
Goal:
p : LTSeries ℤ
i_1 j_1 :
  Fin
    (p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1)
i : ℕ
hi :
  i <
    p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1
j_2 j : ℕ
_hij : i ≤ j
ih :
  ∀
    (hj :
      j <
        p.length (r :=
            {x : ℤ × ℤ |
              match (motive := ℤ × ℤ → Prop) x with
              | (a, b) => a < b}) +
          1),
    p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨i, hi⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) + (↑j : ℤ) ≤
      p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨j, hj⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) + (↑i : ℤ)
hj :
  j + 1 <
    p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1
⊢ p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨i, hi⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) + (↑j : ℤ) ≤
    p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨j, ⋯⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) + (↑i : ℤ)

Tactic:
specialize ih (Nat.lt_of_succ_lt hj)

Premises used: Nat.lt_of_succ_lt
-- Module: Mathlib.Order.RelSeries
Goal:
p : LTSeries ℤ
i_1 j_1 :
  Fin
    (p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1)
i : ℕ
hi :
  i <
    p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1
j_2 j : ℕ
_hij : i ≤ j
hj :
  j + 1 <
    p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1
ih :
  p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨i, hi⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) + (↑j : ℤ) ≤
    p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨j, ⋯⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) + (↑i : ℤ)
⊢ j <
    p.length (r :=
      {x : ℤ × ℤ |
        match (motive := ℤ × ℤ → Prop) x with
        | (a, b) => a < b})

Tactic:
lia
-- Module: Mathlib.Order.RelSeries
Goal:
p : LTSeries ℤ
i_1 j_1 :
  Fin
    (p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1)
i : ℕ
hi :
  i <
    p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1
j_2 j : ℕ
_hij : i ≤ j
hj :
  j + 1 <
    p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1
ih :
  p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨i, hi⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) + (↑j : ℤ) ≤
    p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨j, ⋯⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) + (↑i : ℤ)
⊢ p.toFun (r :=
      {x : ℤ × ℤ |
        match (motive := ℤ × ℤ → Prop) x with
        | (a, b) => a < b})
      (⟨j, ⋯⟩ :
        Fin
          (p.length (r :=
              {x : ℤ × ℤ |
                match (motive := ℤ × ℤ → Prop) x with
                | (a, b) => a < b}) +
            1)) <
    p.toFun (r :=
      {x : ℤ × ℤ |
        match (motive := ℤ × ℤ → Prop) x with
        | (a, b) => a < b})
      ⟨j + 1, ⋯⟩

Tactic:
have step : p ⟨j, _⟩ < p ⟨j + 1, _⟩:= p.step ⟨j, by lia⟩
-- Module: Mathlib.Order.RelSeries
Goal:
p : LTSeries ℤ
i_1 j_1 :
  Fin
    (p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1)
i : ℕ
hi :
  i <
    p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1
j_2 j : ℕ
_hij : i ≤ j
hj :
  j + 1 <
    p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1
ih :
  p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨i, hi⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) + (↑j : ℤ) ≤
    p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨j, ⋯⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) + (↑i : ℤ)
step :
  p.toFun (r :=
      {x : ℤ × ℤ |
        match (motive := ℤ × ℤ → Prop) x with
        | (a, b) => a < b})
      (⟨j, ⋯⟩ :
        Fin
          (p.length (r :=
              {x : ℤ × ℤ |
                match (motive := ℤ × ℤ → Prop) x with
                | (a, b) => a < b}) +
            1)) <
    p.toFun (r :=
      {x : ℤ × ℤ |
        match (motive := ℤ × ℤ → Prop) x with
        | (a, b) => a < b})
      ⟨j + 1, ⋯⟩
⊢ p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨i, hi⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) +
      (↑(j + 1) : ℤ) ≤
    p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨j + 1, hj⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) + (↑i : ℤ)

Tactic:
lia
-- Module: Mathlib.Order.RelSeries
Goal:
p : LTSeries ℤ
i_1 j_1 :
  Fin
    (p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1)
i : ℕ
hi :
  i <
    p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1
j : ℕ
hj :
  j <
    p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1
hij : i ≤ j
base :
  ∀
    (hj :
      i <
        p.length (r :=
            {x : ℤ × ℤ |
              match (motive := ℤ × ℤ → Prop) x with
              | (a, b) => a < b}) +
          1),
    p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨i, hi⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) + (↑i : ℤ) ≤
      p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨i, hj⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) + (↑i : ℤ)
succ :
  ∀ (j : ℕ) (_hij : i ≤ j)
    (ih :
      ∀
        (hj :
          j <
            p.length (r :=
                {x : ℤ × ℤ |
                  match (motive := ℤ × ℤ → Prop) x with
                  | (a, b) => a < b}) +
              1),
        p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨i, hi⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) +
            (↑j : ℤ) ≤
          p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨j, hj⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) +
            (↑i : ℤ))
    (hj :
      j + 1 <
        p.length (r :=
            {x : ℤ × ℤ |
              match (motive := ℤ × ℤ → Prop) x with
              | (a, b) => a < b}) +
          1),
    p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨i, hi⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) +
        (↑(j + 1) : ℤ) ≤
      p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨j + 1, hj⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) +
        (↑i : ℤ)
⊢ p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨i, hi⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) + (↑j : ℤ) ≤
    p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨j, hj⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) + (↑i : ℤ)

Tactic:
induction j, hij using Nat.le_induction with
  | base => simp
  | succ j _hij ih =>
    specialize ih (Nat.lt_of_succ_lt hj)
    have step : p ⟨j, _⟩ < p ⟨j + 1, _⟩:= p.step ⟨j, by lia⟩
    norm_cast at *; lia
-- Module: Mathlib.Order.RelSeries
Goal:
p : LTSeries ℕ
⊢ RelSeries.head (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}) ≤
    RelSeries.last (r :=
      {x : ℕ × ℕ |
        match (motive := ℕ × ℕ → Prop) x with
        | (a, b) => a < b})
      p

Tactic:
LTSeries.apply_add_index_le_apply_add_index_nat _ _ (Fin.last _) (Fin.zero_le _)

Premises used: RelSeries.last, Fin.zero_le, LTSeries.apply_add_index_le_apply_add_index_nat, Fin.last, RelSeries.head
-- Module: Mathlib.Order.RelSeries
Goal:
p : LTSeries ℤ
⊢ RelSeries.head (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})) :
        ℤ) ≤
    RelSeries.last (r :=
      {x : ℤ × ℤ |
        match (motive := ℤ × ℤ → Prop) x with
        | (a, b) => a < b})
      p

Tactic:
simpa using LTSeries.apply_add_index_le_apply_add_index_int _ _ (Fin.last _) (Fin.zero_le _)

Premises used: Fin.zero_le, Fin.last, LTSeries.apply_add_index_le_apply_add_index_int