awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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
⊢ 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
have 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
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
Cleared hypotheses: hj, hij
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
p : LTSeries ℤ
i j :
  Fin
    (p.length (r :=
        {x : ℤ × ℤ |
          match (motive := ℤ × ℤ → Prop) x with
          | (a, b) => a < b}) +
      1)
hij : i ≤ j
⊢ 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 : ℕ) : ℤ)
have 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)) :
            ℕ) :
        ℤ)
Tactic: have ⟨i, hi⟩ := i
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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
⊢ 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)) :
            ℕ) :
        ℤ)
have 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)) :
            ℕ) :
        ℤ)
Tactic: have ⟨j, hj⟩ := j
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Order.RelSeries (hypothesis)
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⟩
⊢ 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)) :
            ℕ) :
        ℤ)
have hij₁ : i ≤ j
Tactic: simp only [Fin.mk_le_mk] at hij
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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
⊢ 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)) :
            ℕ) :
        ℤ)
have 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 : ℤ)
Tactic: simp only at *
-- Lean 4 proof step from Mathlib.Order.RelSeries (hypothesis)
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 + 1) : ℤ) ≤
    p.toFun (r := {x : ℤ × ℤ | x.1 < x.2}) (⟨j + 1, hj⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) + (↑i : ℤ)
have 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, sorry⟩ : Fin (p.length (r := {x : ℤ × ℤ | x.1 < x.2}) + 1)) + (↑i : ℤ)
Tactic: specialize ih (Nat.lt_of_succ_lt hj)
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Order.RelSeries (hypothesis)
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 : ℤ × ℤ | 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 : ℤ)
have step : p.toFun (r :=
    {x : ℤ × ℤ |
      match (motive := ℤ × ℤ → Prop) x with
      | (a, b) => a < b})
    (⟨j, sorry⟩ :
      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, sorry⟩
Tactic: have step : p ⟨j, _⟩ < p ⟨j + 1, _⟩:= p.step ⟨j, by lia⟩
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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
⊢ 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 : ℤ)
have 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 : ℤ)
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
Cleared hypotheses: hj, hij
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
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 : ℤ)
⊢ 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 : ℤ)
have 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 : ℤ)
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
Cleared hypotheses: hj, hij
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Fintype α
s : LTSeries α
⊢ s.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) <
    Fintype.card α
have by_contra! : ∀
  (h :
    Fintype.card α ≤
      s.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})),
  False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Fintype α
s : LTSeries α
h :
  Fintype.card α ≤
    s.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
⊢ Fintype.card α <
    Fintype.card
      (Fin
        (s.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) +
          1))
have rw : Fintype.card α <
  s.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) +
    1
Tactic: rw [Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Fintype α
s : LTSeries α
h :
  Fintype.card α ≤
    s.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
⊢ False
have obtain : ∀
  (i j :
    Fin
      (s.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) +
        1))
  (hn : i ≠ j)
  (he :
    s.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        i =
      s.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        j),
  False
Tactic: obtain ⟨i, j, hn, he⟩ := Fintype.exists_ne_map_eq_of_card_lt s (by rw [Fintype.card_fin]; lia)
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Fintype α
s : LTSeries α
h :
  Fintype.card α ≤
    s.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
i j :
  Fin
    (s.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1)
hn : i ≠ j
he :
  s.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      i =
    s.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      j
⊢ False
have inr : ∀
  (this :
    ∀
      (i j :
        Fin
          (s.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b}) +
            1))
      (hn : i ≠ j)
      (he :
        s.toFun (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            i =
          s.toFun (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            j)
      (hl : i < j), False)
  (hl : ¬i < j), False
Tactic: wlog hl : i < j generalizing i j
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Fintype α
s : LTSeries α
h :
  Fintype.card α ≤
    s.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
i j :
  Fin
    (s.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1)
hn : i ≠ j
he :
  s.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      i =
    s.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      j
inr :
  ∀
    (this :
      ∀
        (i j :
          Fin
            (s.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b}) +
              1))
        (hn : i ≠ j)
        (he :
          s.toFun (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              i =
            s.toFun (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              j)
        (hl : i < j), False)
    (hl : ¬i < j), False
⊢ False
have wlog : ∀
  (i j :
    Fin
      (s.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) +
        1))
  (hn : i ≠ j)
  (he :
    s.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        i =
      s.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        j)
  (hl : i < j), False
Tactic: wlog hl : i < j generalizing i j
Cleared hypotheses: i, j, hn, he
-- Lean 4 proof step from Mathlib.Order.RelSeries (hypothesis)
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s_1 : SetRel β β
inst : Preorder α
inst_1 : Preorder β
inst_2 : Fintype α
inst_3 : DecidableLT α
s : LTSeries α
⊢ Membership.mem (γ := Finset (LTSeries α))
    (Finset.map (α :=
      { f : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α) //
        StrictMono (f.snd (β := fun (l : Fin (Fintype.card α)) ↦ Fin ((↑l : ℕ) + 1) → α)) })
      (injStrictMono (Fintype.card α)) Finset.univ)
    s
have bl : s.length (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}) <
  Fintype.card α
Tactic: have bl := s.length_lt_card