awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst : Preorder α
inst_1 : Preorder β
n : ℕ
lf : Fin n
f : Fin ((↑lf : ℕ) + 1) → α
mf : StrictMono f
lg : Fin n
g : Fin ((↑lg : ℕ) + 1) → α
mg : StrictMono g
e : Eq (α := LTSeries α) (mk (↑lf : ℕ) f ⋯) (mk (↑lg : ℕ) g ⋯)
⊢ RelSeries.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (mk (↑lf : ℕ) f ⋯) =
    RelSeries.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (mk (↑lg : ℕ) g ⋯)

Tactic:
have leq := congr($(e).length)
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst : Preorder α
inst_1 : Preorder β
n : ℕ
lf : Fin n
f : Fin ((↑lf : ℕ) + 1) → α
mf : StrictMono f
lg : Fin n
g : Fin ((↑lg : ℕ) + 1) → α
mg : StrictMono g
e : Eq (α := LTSeries α) (mk (↑lf : ℕ) f ⋯) (mk (↑lg : ℕ) g ⋯)
leq :
  RelSeries.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (mk (↑lf : ℕ) f ⋯) =
    RelSeries.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (mk (↑lg : ℕ) g ⋯)
⊢ lf = lg

Tactic:
rw [mk_length lf f mf, mk_length lg g mg, Fin.val_eq_val] at leq

Premises used: Fin.val, LTSeries.mk_length, Fin.val_eq_val
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst : Preorder α
inst_1 : Preorder β
n : ℕ
lf : Fin n
f : Fin ((↑lf : ℕ) + 1) → α
mf : StrictMono f
lg : Fin n
g : Fin ((↑lg : ℕ) + 1) → α
mg : StrictMono g
e : Eq (α := LTSeries α) (mk (↑lf : ℕ) f ⋯) (mk (↑lg : ℕ) g ⋯)
leq : lf = lg
subst :
  ∀ (g : Fin ((↑lf : ℕ) + 1) → α) (mg : StrictMono g) (e : Eq (α := LTSeries α) (mk (↑lf : ℕ) f ⋯) (mk (↑lf : ℕ) g ⋯)),
    Eq.{u_1 + 1} (α :=
      { f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α) //
        StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) })
      (Subtype.mk (p := fun (f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)) ↦
        StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)))
        (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lf f) mf)
      (Subtype.mk (p := fun (f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)) ↦
        StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)))
        (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lf g) mg)
⊢ Eq.{u_1 + 1} (α :=
    { f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α) //
      StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) })
    (Subtype.mk (p := fun (f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)) ↦
      StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)))
      (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lf f) mf)
    (Subtype.mk (p := fun (f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)) ↦
      StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)))
      (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lg g) mg)

Tactic:
subst leq
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst : Preorder α
inst_1 : Preorder β
n : ℕ
lf : Fin n
f : Fin ((↑lf : ℕ) + 1) → α
mf : StrictMono f
g : Fin ((↑lf : ℕ) + 1) → α
mg : StrictMono g
e : Eq (α := LTSeries α) (mk (↑lf : ℕ) f ⋯) (mk (↑lf : ℕ) g ⋯)
simp_rw : f = g
⊢ Eq.{u_1 + 1} (α :=
    { f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α) //
      StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)) })
    (Subtype.mk (p := fun (f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)) ↦
      StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)))
      (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lf f) mf)
    (Subtype.mk (p := fun (f : (l : Fin n) × (Fin ((↑l : ℕ) + 1) → α)) ↦
      StrictMono (f.snd (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α)))
      (Sigma.mk (β := fun (l : Fin n) ↦ Fin ((↑l : ℕ) + 1) → α) lf g) mg)

Tactic:
simp_rw [Subtype.mk_eq_mk, Sigma.mk.inj_iff, heq_eq_eq, true_and]

Premises used: heq_eq_eq, Subtype.mk_eq_mk, Sigma.mk.inj_iff, true_and
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst : Preorder α
inst_1 : Preorder β
n : ℕ
lf : Fin n
f : Fin ((↑lf : ℕ) + 1) → α
mf : StrictMono f
g : Fin ((↑lf : ℕ) + 1) → α
mg : StrictMono g
e : Eq (α := LTSeries α) (mk (↑lf : ℕ) f ⋯) (mk (↑lf : ℕ) g ⋯)
⊢ ∀
    (i :
      Fin
        (RelSeries.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            (mk (↑lf : ℕ) f ⋯) +
          1)),
    RelSeries.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (mk (↑lf : ℕ) f ⋯) i =
      RelSeries.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (mk (↑lf : ℕ) g ⋯) i

Tactic:
have feq := fun i ↦ congr($(e).toFun i)
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst : Preorder α
inst_1 : Preorder β
n : ℕ
lf : Fin n
f : Fin ((↑lf : ℕ) + 1) → α
mf : StrictMono f
g : Fin ((↑lf : ℕ) + 1) → α
mg : StrictMono g
e : Eq (α := LTSeries α) (mk (↑lf : ℕ) f ⋯) (mk (↑lf : ℕ) g ⋯)
feq rwa rwa₁ rwa₂ rwa₃ : ∀ (x : Fin ((↑lf : ℕ) + 1)), f x = g x
⊢ f = g

Tactic:
rwa [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
p : LTSeries α
f : α → β
hf : StrictMono f
⊢ RelSeries.head (r :=
      {x : β × β |
        match (motive := β × β → Prop) x with
        | (a, b) => a < b})
      (p.map f hf) =
    f
      (RelSeries.head (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p)

Tactic:
rfl

Premises used: setOf, RelSeries.head, rfl
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
p : LTSeries α
f : α → β
hf : StrictMono f
⊢ RelSeries.last (r :=
      {x : β × β |
        match (motive := β × β → Prop) x with
        | (a, b) => a < b})
      (p.map f hf) =
    f
      (RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p)

Tactic:
rfl

Premises used: RelSeries.last, setOf, rfl
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst : Preorder α
inst_1 : Preorder β
p : LTSeries β
f : α → β
comap : ∀ ⦃x y : α⦄, f x < f y → x < y
surjective : Function.Surjective f
i j :
  Fin
    (p.length (r :=
        {x : β × β |
          match (motive := β × β → Prop) x with
          | (a, b) => a < b}) +
      1)
h : i < j
⊢ f
      ((fun
            (i :
              Fin
                (p.length (r :=
                    {x : β × β |
                      match (motive := β × β → Prop) x with
                      | (a, b) => a < b}) +
                  1)) ↦
          Exists.choose (p := fun (a : α) ↦
            f a =
              p.toFun (r :=
                {x : β × β |
                  match (motive := β × β → Prop) x with
                  | (a, b) => a < b})
                i)
            ⋯)
        i) <
    f
      ((fun
            (i :
              Fin
                (p.length (r :=
                    {x : β × β |
                      match (motive := β × β → Prop) x with
                      | (a, b) => a < b}) +
                  1)) ↦
          Exists.choose (p := fun (a : α) ↦
            f a =
              p.toFun (r :=
                {x : β × β |
                  match (motive := β × β → Prop) x with
                  | (a, b) => a < b})
                i)
            ⋯)
        j)

Tactic:
simpa only [(surjective _).choose_spec] using p.strictMono h

Premises used: Exists.choose_spec, LTSeries.strictMono
-- Module: Mathlib.Order.RelSeries
Goal:
n : ℕ
⊢ (range n).length (r :=
      {x : ℕ × ℕ |
        match (motive := ℕ × ℕ → Prop) x with
        | (a, b) => a < b}) =
    n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.RelSeries
Goal:
n : ℕ
i : Fin (n + 1)
⊢ (range n).toFun (r :=
      {x : ℕ × ℕ |
        match (motive := ℕ × ℕ → Prop) x with
        | (a, b) => a < b})
      i =
    (↑i : ℕ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.RelSeries
Goal:
n : ℕ
⊢ RelSeries.head (r :=
      {x : ℕ × ℕ |
        match (motive := ℕ × ℕ → Prop) x with
        | (a, b) => a < b})
      (range n) =
    0

Tactic:
rfl

Premises used: Nat.mod, RelSeries.head, rfl
-- Module: Mathlib.Order.RelSeries
Goal:
n : ℕ
⊢ RelSeries.last (r :=
      {x : ℕ × ℕ |
        match (motive := ℕ × ℕ → Prop) x with
        | (a, b) => a < b})
      (range n) =
    n

Tactic:
rfl

Premises used: RelSeries.last, rfl
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : WellFoundedLT α
inst_2 : WellFoundedGT α
s : Fin (HAdd.hAdd (α := ℕ) 0 1) → α
h :
  ∀ (i : Fin 0),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (s i.castSucc, s i.succ)
⊢ ∃ (t :
    RelSeries (α := α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ⋖ b})
    (i :
    Fin
        ((RelSeries.mk (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})
                0 s h).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)),
    t.toFun (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b}) ∘
          (⇑i : (a : Fin ({ length := 0, toFun := s, step := h }.length + 1)) → Fin (t.length + 1)) =
        (RelSeries.mk (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              0 s h).toFun
          (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) ∧
      Eq (α :=
          Fin
            (t.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a ⋖ b}) +
              1))
          ((i : (a : Fin ({ length := 0, toFun := s, step := h }.length + 1)) → Fin (t.length + 1)) 0) 0 ∧
        Eq (α :=
          Fin
            (t.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a ⋖ b}) +
              1))
          ((i : (a : Fin ({ length := 0, toFun := s, step := h }.length + 1)) → Fin (t.length + 1))
              (Fin.last
                ((RelSeries.mk (r :=
                      {x : α × α |
                        match (motive := α × α → Prop) x with
                        | (a, b) => a < b})
                      0 s h).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))

Tactic:
exact ⟨⟨0, s, nofun⟩, (Equiv.refl _).toEmbedding, rfl, rfl, rfl⟩
-- Module: Mathlib.Order.RelSeries
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 =
    ⊥
this :
  ∀ {α : Type u_3} [inst : PartialOrder α] [inst_4 : BoundedOrder α] [WellFoundedLT α] [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)),
      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}) ∧
        t.head (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a ⋖ b}) =
            ⊥ ∧
          t.last (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a ⋖ b}) =
            ⊤
h₂ :
  ¬RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        s =
      ⊤
⊢ (RelSeries.snoc (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          s ⊤ ⋯).head
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    ⊥

Tactic:
simp [h₁]
-- Module: Mathlib.Order.RelSeries
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 =
    ⊥
this :
  ∀ {α : Type u_3} [inst : PartialOrder α] [inst_4 : BoundedOrder α] [WellFoundedLT α] [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)),
      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}) ∧
        t.head (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a ⋖ b}) =
            ⊥ ∧
          t.last (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a ⋖ b}) =
            ⊤
h₂ :
  ¬RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        s =
      ⊤
⊢ (RelSeries.snoc (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          s ⊤ ⋯).last
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    ⊤

Tactic:
simp
-- 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 *