awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
rw :
  ⨆ (p : LTSeries α),
        ⨆ (_ :
          RelSeries.last (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p ≤
            a),
          (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) ≤
      n ↔
    ∀ ⦃p : LTSeries α⦄,
      RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p ≤
          a →
        (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) ≤
          n
⊢ height a ≤ n ↔
    ∀ ⦃p : LTSeries α⦄,
      RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p ≤
          a →
        (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) ≤
          n
have rw₁ : (∀ (i : LTSeries α)
    (j :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          i ≤
        a),
    (↑(i.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞) ≤
      n) ↔
  ∀ ⦃p : LTSeries α⦄,
    RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p ≤
        a →
      (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
        n
Tactic: rw [height, iSup₂_le_iff]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
⊢ coheight a ≤ n ↔
    ∀ ⦃p : LTSeries α⦄,
      a ≤
          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})) :
            ℕ∞) ≤
          n
have rw : ⨆ (p : LTSeries α),
      ⨆ (_ :
        a ≤
          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})) :
          ℕ∞) ≤
    n ↔
  ∀ ⦃p : LTSeries α⦄,
    a ≤
        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})) :
          ℕ∞) ≤
        n
Tactic: rw [coheight_eq, iSup₂_le_iff]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
rw :
  ⨆ (p : LTSeries α),
        ⨆ (_ :
          a ≤
            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})) :
            ℕ∞) ≤
      n ↔
    ∀ ⦃p : LTSeries α⦄,
      a ≤
          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})) :
            ℕ∞) ≤
          n
⊢ coheight a ≤ n ↔
    ∀ ⦃p : LTSeries α⦄,
      a ≤
          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})) :
            ℕ∞) ≤
          n
have rw₁ : (∀ (i : LTSeries α)
    (j :
      a ≤
        RelSeries.head (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          i),
    (↑(i.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞) ≤
      n) ↔
  ∀ ⦃p : LTSeries α⦄,
    a ≤
        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})) :
          ℕ∞) ≤
        n
Tactic: rw [coheight_eq, iSup₂_le_iff]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
h :
  ∀ (p : LTSeries α),
    RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a →
      (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
        n
⊢ height a ≤ n
have apply : ∀ ⦃p : LTSeries α⦄,
  RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p ≤
      a →
    (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞) ≤
      n
Tactic: apply height_le_iff.mpr
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
h :
  ∀ (p : LTSeries α),
    RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a →
      (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
        n
p : LTSeries α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    a
⊢ (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    n
have inr : ∀
  (this :
    ∀ {α : Type u_1} [inst : Preorder α] {a : α} {n : ℕ∞}
      (h :
        ∀ (p : LTSeries α),
          RelSeries.last (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})
                p =
              a →
            (↑(p.length (r :=
                    {x : α × α |
                      match (motive := α × α → Prop) x with
                      | (a, b) => a < b})) :
                ℕ∞) ≤
              n)
      ⦃p : LTSeries α⦄
      (hlast :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p ≤
          a)
      (hlenpos :
        p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) ≠
          0),
      (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
        n)
  (hlenpos :
    ¬p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) ≠
        0),
  (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    n
Tactic: wlog hlenpos : p.length ≠ 0
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
a : α
n : ℕ∞
h :
  ∀ (p : LTSeries α),
    RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a →
      (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
        n
p : LTSeries α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    a
hlenpos :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
p' : RelSeries (α := α)
  {x : α × α |
    match (motive := α × α → Prop) x with
    | (a, b) => a < b} :=
  (RelSeries.eraseLast (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p).snoc
    (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    a ⋯
⊢ p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    p'.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
have simp : p.length (r := {x : α × α | x.1 < x.2}) = p.length (r := {x : α × α | x.1 < x.2}) - 1 + 1
Tactic: simp [p']
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
a : α
n : ℕ∞
h :
  ∀ (p : LTSeries α),
    RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a →
      (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
        n
p : LTSeries α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    a
hlenpos :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
p' : RelSeries (α := α)
  {x : α × α |
    match (motive := α × α → Prop) x with
    | (a, b) => a < b} :=
  (RelSeries.eraseLast (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p).snoc
    (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    a ⋯
⊢ (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    n
have rw : (↑(p'.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})) :
    ℕ∞) ≤
  n
Tactic: rw [show p.length = p'.length by simp [p']; lia]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
a : α
n : ℕ∞
h :
  ∀ (p : LTSeries α),
    RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a →
      (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
        n
p : LTSeries α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    a
hlenpos :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
p' : RelSeries (α := α)
  {x : α × α |
    match (motive := α × α → Prop) x with
    | (a, b) => a < b} :=
  (RelSeries.eraseLast (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p).snoc
    (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    a ⋯
⊢ (↑(p'.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    n
have a₁ : p'.last (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}) =
  a
Tactic: apply h
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
⊢ height a ≤ n ↔
    ∀ ⦃p : LTSeries α⦄,
      RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          a →
        (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) ≤
          n
have mp : height a ≤ n →
  ∀ ⦃p : LTSeries α⦄,
    RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a →
      (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
        n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
mp :
  height a ≤ n →
    ∀ ⦃p : LTSeries α⦄,
      RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          a →
        (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) ≤
          n
⊢ height a ≤ n ↔
    ∀ ⦃p : LTSeries α⦄,
      RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          a →
        (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) ≤
          n
have mpr : (∀ ⦃p : LTSeries α⦄,
    RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a →
      (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
        n) →
  height a ≤ n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
⊢ height a ≤ n →
    ∀ ⦃p : LTSeries α⦄,
      RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          a →
        (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) ≤
          n
have mp : (∀ ⦃p : LTSeries α⦄,
    RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p ≤
        a →
      (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
        n) →
  ∀ ⦃p : LTSeries α⦄,
    RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a →
      (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
        n
Tactic: rw [height_le_iff]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ height a =
    ⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          a),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞)
have H : ∀ (c : ℕ∞),
  height a ≤ c ↔
    ⨆ (p : LTSeries α),
        ⨆ (_ :
          RelSeries.last (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p =
            a),
          (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) ≤
      c
Tactic: apply eq_of_forall_ge_iff
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
⊢ height a ≤ n ↔
    ⨆ (p : LTSeries α),
        ⨆ (_ :
          RelSeries.last (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p =
            a),
          (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) ≤
      n
have H : (∀ ⦃p : LTSeries α⦄,
    RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a →
      (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
        n) ↔
  ⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          a),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
    n
Tactic: rw [height_le_iff', iSup₂_le_iff]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
H :
  (∀ ⦃p : LTSeries α⦄,
      RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          a →
        (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) ≤
          n) ↔
    ⨆ (p : LTSeries α),
        ⨆ (_ :
          RelSeries.last (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p =
            a),
          (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) ≤
      n
⊢ height a ≤ n ↔
    ⨆ (p : LTSeries α),
        ⨆ (_ :
          RelSeries.last (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p =
            a),
          (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) ≤
      n
have H₁ : (∀ ⦃p : LTSeries α⦄,
    RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a →
      (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
        n) ↔
  ∀ (i : LTSeries α)
    (j :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          i =
        a),
    (↑(i.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞) ≤
      n
Tactic: rw [height_le_iff', iSup₂_le_iff]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ height a =
    ⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.head (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          a),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞)
have rw : Eq (α := ℕ∞)
  (⨆ (p : LTSeries αᵒᵈ),
    ⨆ (_ :
      RelSeries.last (r :=
          {x : αᵒᵈ × αᵒᵈ |
            match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
            | (a, b) => a < b})
          p =
        a),
      (↑(p.length (r :=
            {x : αᵒᵈ × αᵒᵈ |
              match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞))
  (⨆ (p : LTSeries α),
    ⨆ (_ :
      RelSeries.head (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞))
Tactic: rw [height_eq_iSup_last_eq]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
⊢ coheight a ≤ n ↔
    ∀ ⦃p : LTSeries α⦄,
      RelSeries.head (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          a →
        (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) ≤
          n
have rw : ⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.head (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          a),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
    n ↔
  ∀ ⦃p : LTSeries α⦄,
    RelSeries.head (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a →
      (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
        n
Tactic: rw [coheight_eq_iSup_head_eq, iSup₂_le_iff]