awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : WellFoundedLT α
inst_3 : WellFoundedGT α
s : LTSeries α
h₁ :
  RelSeries.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      s =
    ⊥
h₂ :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      s =
    ⊤
t :
  RelSeries (α := α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ⋖ b}
i :
  Fin
      (s.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) +
        1) ↪
    Fin
      (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b}) +
        1)
hit :
  t.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a ⋖ b}) ∘
      (⇑i : (a : Fin (s.length + 1)) → Fin (t.length + 1)) =
    s.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
hi₁ :
  Eq (α :=
    Fin
      (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b}) +
        1))
    ((i : (a : Fin (s.length + 1)) → Fin (t.length + 1)) 0) 0
hi₂ :
  Eq (α :=
    Fin
      (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b}) +
        1))
    ((i : (a : Fin (s.length + 1)) → Fin (t.length + 1))
        (Fin.last
          (s.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}))) :
      Fin
        (t.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b}) +
          1))
    (Fin.last
        (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b})) :
      Fin
        (t.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b}) +
          1))
refine_1 :
  t.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ⋖ b}) =
    RelSeries.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      s
⊢ t.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ⋖ b}) =
    ⊥
have refine_1₁ : t.toFun (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ⋖ b})
    0 =
  RelSeries.head (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    s
Tactic: rw [← h₁, RelSeries.head, RelSeries.head, ← hi₁, ← hit, Function.comp]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : WellFoundedLT α
inst_3 : WellFoundedGT α
s : LTSeries α
h₁ :
  RelSeries.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      s =
    ⊥
h₂ :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      s =
    ⊤
t :
  RelSeries (α := α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ⋖ b}
i :
  Fin
      (s.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) +
        1) ↪
    Fin
      (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b}) +
        1)
hit :
  t.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a ⋖ b}) ∘
      (⇑i : (a : Fin (s.length + 1)) → Fin (t.length + 1)) =
    s.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
hi₁ :
  Eq (α :=
    Fin
      (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b}) +
        1))
    ((i : (a : Fin (s.length + 1)) → Fin (t.length + 1)) 0) 0
hi₂ :
  Eq (α :=
    Fin
      (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b}) +
        1))
    ((i : (a : Fin (s.length + 1)) → Fin (t.length + 1))
        (Fin.last
          (s.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}))) :
      Fin
        (t.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b}) +
          1))
    (Fin.last
        (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b})) :
      Fin
        (t.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b}) +
          1))
refine_1 :
  t.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ⋖ b}) =
    RelSeries.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      s
refine_1₁ :
  t.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ⋖ b})
      0 =
    RelSeries.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      s
⊢ t.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ⋖ b}) =
    ⊥
have refine_1₂ : t.toFun (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ⋖ b})
    0 =
  s.toFun (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    0
Tactic: rw [← h₁, RelSeries.head, RelSeries.head, ← hi₁, ← hit, Function.comp]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : WellFoundedLT α
inst_3 : WellFoundedGT α
s : LTSeries α
h₁ :
  RelSeries.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      s =
    ⊥
h₂ :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      s =
    ⊤
t :
  RelSeries (α := α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ⋖ b}
i :
  Fin
      (s.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) +
        1) ↪
    Fin
      (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b}) +
        1)
hit :
  t.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a ⋖ b}) ∘
      (⇑i : (a : Fin (s.length + 1)) → Fin (t.length + 1)) =
    s.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
hi₁ :
  Eq (α :=
    Fin
      (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b}) +
        1))
    ((i : (a : Fin (s.length + 1)) → Fin (t.length + 1)) 0) 0
hi₂ :
  Eq (α :=
    Fin
      (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b}) +
        1))
    ((i : (a : Fin (s.length + 1)) → Fin (t.length + 1))
        (Fin.last
          (s.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}))) :
      Fin
        (t.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b}) +
          1))
    (Fin.last
        (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b})) :
      Fin
        (t.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b}) +
          1))
⊢ t.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ⋖ b}) =
    ⊤
have refine_2 : t.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})
    s
Tactic: rw [← h₂, RelSeries.last, RelSeries.last, ← hi₂, ← hit, Function.comp]
-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : WellFoundedLT α
inst_3 : WellFoundedGT α
s : LTSeries α
h₁ :
  RelSeries.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      s =
    ⊥
h₂ :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      s =
    ⊤
t :
  RelSeries (α := α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ⋖ b}
i :
  Fin
      (s.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) +
        1) ↪
    Fin
      (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b}) +
        1)
hit :
  t.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a ⋖ b}) ∘
      (⇑i : (a : Fin (s.length + 1)) → Fin (t.length + 1)) =
    s.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
hi₁ :
  Eq (α :=
    Fin
      (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b}) +
        1))
    ((i : (a : Fin (s.length + 1)) → Fin (t.length + 1)) 0) 0
hi₂ :
  Eq (α :=
    Fin
      (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b}) +
        1))
    ((i : (a : Fin (s.length + 1)) → Fin (t.length + 1))
        (Fin.last
          (s.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}))) :
      Fin
        (t.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b}) +
          1))
    (Fin.last
        (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b})) :
      Fin
        (t.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b}) +
          1))
refine_2 :
  t.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})
      s
⊢ t.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ⋖ b}) =
    ⊤
have refine_2₁ : t.toFun (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ⋖ b})
    (Fin.last
      (t.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})
    s
Tactic: rw [← h₂, RelSeries.last, RelSeries.last, ← hi₂, ← hit, Function.comp]
-- 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