awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
h : (↑n : ℕ∞) ≤ coheight 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}) =
        n
have obtain : ∀ (p : LTSeries αᵒᵈ)
  (hp :
    RelSeries.last (r :=
        {x : αᵒᵈ × αᵒᵈ |
          match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
          | (a, b) => a < b})
        p =
      a)
  (hl :
    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: obtain ⟨p, hp, hl⟩ := exists_series_of_le_height (α := αᵒᵈ) a h
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ height x = ⨆ (y : α), ⨆ (_ : y < x), height y + 1
have a : height x ≤ ⨆ (y : α), ⨆ (_ : y < x), height y + 1
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
a : height x ≤ ⨆ (y : α), ⨆ (_ : y < x), height y + 1
⊢ height x = ⨆ (y : α), ⨆ (_ : y < x), height y + 1
have a₁ : ⨆ (y : α), ⨆ (_ : y < x), height y + 1 ≤ height x
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ height x ≤ ⨆ (y : α), ⨆ (_ : y < x), height y + 1
have a : ∀ (p : LTSeries α),
  RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p =
      x →
    LE.le (α := ℕ∞)
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
      (⨆ (y : α), ⨆ (_ : y < x), height y + 1)
Tactic: apply height_le
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
n : ℕ
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    n + 1
⊢ LE.le (α := ℕ∞) (↑(n + 1) : ℕ∞) (⨆ (y : α), ⨆ (_ : y < x), height y + 1)
have a : LE.le (α := ℕ∞) (↑(n + 1) : ℕ∞)
  (⨆ (_ :
    (RelSeries.eraseLast (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p).last
        (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) <
      x),
    height
        ((RelSeries.eraseLast (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p).last
          (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) +
      1)
Tactic: apply le_iSup_of_le p.eraseLast.last
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
n : ℕ
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    n + 1
⊢ (RelSeries.eraseLast (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p).last
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) <
    x
have rw : (RelSeries.eraseLast (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p).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})
    p
Tactic: rw [← hp]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
n : ℕ
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    n + 1
⊢ LE.le (α := ℕ∞) (↑(n + 1) : ℕ∞)
    (⨆ (_ :
      (RelSeries.eraseLast (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p).last
          (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) <
        x),
      height
          ((RelSeries.eraseLast (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})
                p).last
            (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) +
        1)
have a : (↑(n + 1) : ℕ∞) ≤
  height
      ((RelSeries.eraseLast (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p).last
        (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})) +
    1
Tactic: apply le_iSup_of_le (by rw [← hp]; exact p.eraseLast_last_rel_last (by lia))
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
n : ℕ
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    n + 1
⊢ (↑(n + 1) : ℕ∞) ≤
    height
        ((RelSeries.eraseLast (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p).last
          (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) +
      1
have a : LE.le (α := ℕ∞) (↑(n + 1) : ℕ∞)
  (⨆ (p_1 : LTSeries α),
    ⨆ (_ :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p_1 =
        (RelSeries.eraseLast (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p).last
          (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})),
      HAdd.hAdd (α := ℕ∞)
        (↑(p_1.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞)
        1)
Tactic: rw [height_add_const]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
⊢ LE.le (α := ℕ∞)
    (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)
    (⨆ (y : α), ⨆ (_ : y < x), height y + 1)
have a : ∀ (x_1 : ℕ)
  (hlen :
    p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) =
      x_1),
  LE.le (α := ℕ∞) (↑x_1 : ℕ∞) (⨆ (y : α), ⨆ (_ : y < x), height y + 1)
Tactic: cases hlen : p.length with
    | zero => simp
    | succ n =>
      apply le_iSup_of_le p.eraseLast.last
      apply le_iSup_of_le (by rw [← hp]; exact p.eraseLast_last_rel_last (by lia))
      rw [height_add_const]
      apply le_iSup₂_of_le p.eraseLast (by rfl) (by simp [hlen])
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ ⨆ (y : α), ⨆ (_ : y < x), height y + 1 ≤ height x
have a : ∀ (i : α) (j : i < x), height i + 1 ≤ height x
Tactic: apply iSup₂_le
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x y : α
hyx : y < x
⊢ height y + 1 ≤ height x
have a : ⨆ (p : LTSeries α),
    ⨆ (_ :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        y),
      HAdd.hAdd (α := ℕ∞)
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞)
        1 ≤
  height x
Tactic: rw [height_add_const]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x y : α
hyx : y < x
⊢ ⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          y),
        HAdd.hAdd (α := ℕ∞)
          (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞)
          1 ≤
    height x
have a : ∀ (i : LTSeries α)
  (j :
    RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        i =
      y),
  HAdd.hAdd (α := ℕ∞)
      (↑(i.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
      1 ≤
    height x
Tactic: apply iSup₂_le
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
| height x ≤ (↑n : ℕ∞)
have rw : ∀ (i : α) (j : i < x), height i + 1 ≤ (↑n : ℕ∞)
Tactic: rw [height_eq_iSup_lt_height, iSup₂_le_iff]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
⊢ height x ≤ (↑n : ℕ∞) ↔ ∀ y < x, height y < (↑n : ℕ∞)
have conv_lhs : (∀ (i : α) (j : i < x), height i + 1 ≤ (↑n : ℕ∞)) ↔ ∀ y < x, height y < (↑n : ℕ∞)
Tactic: conv_lhs => rw [height_eq_iSup_lt_height, iSup₂_le_iff]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
⊢ (∀ (i : α) (j : i < x), height i + 1 ≤ (↑n : ℕ∞)) ↔ ∀ y < x, height y < (↑n : ℕ∞)
have a : ∀ y < x, height y + 1 ≤ (↑n : ℕ∞) ↔ height y < (↑n : ℕ∞)
Tactic: congr! 2 with y _
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
y : α
h : y < x
⊢ height y + 1 ≤ (↑n : ℕ∞) ↔ height y < (↑n : ℕ∞)
have a : HAdd.hAdd (α := ℕ∞) ⊤ 1 ≤ (↑n : ℕ∞) ↔ LT.lt (α := ℕ∞) ⊤ (↑n : ℕ∞)
Tactic: cases height y
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
y : α
h : y < x
a : HAdd.hAdd (α := ℕ∞) ⊤ 1 ≤ (↑n : ℕ∞) ↔ LT.lt (α := ℕ∞) ⊤ (↑n : ℕ∞)
⊢ height y + 1 ≤ (↑n : ℕ∞) ↔ height y < (↑n : ℕ∞)
have a₁ : ∀ (a : ℕ), HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) 1 ≤ (↑n : ℕ∞) ↔ LT.lt (α := ℕ∞) (↑a : ℕ∞) (↑n : ℕ∞)
Tactic: cases height y
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
y : α
h : y < x
a : ℕ
⊢ HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) 1 ≤ (↑n : ℕ∞) ↔ LT.lt (α := ℕ∞) (↑a : ℕ∞) (↑n : ℕ∞)
have a : a + 1 ≤ n ↔ a < n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
h : height x = ⊤
n : ℕ
⊢ ∃ (p : LTSeries α),
    RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        x ∧
      p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n
have apply : (↑n : ℕ∞) ≤ height x
Tactic: apply exists_series_of_le_height x (n := n)
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
h :
  ∀ (n : ℕ),
    ∃ (p : LTSeries α),
      RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          x ∧
        p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) =
          n
⊢ height x = ⊤
have rw : ¬∃ (x_1 : ℕ),
    ∀ (y : ℕ),
      Membership.mem (γ := Set ℕ)
          (Set.range
            fun
              (x_2 :
                { p : LTSeries α //
                  RelSeries.last (r :=
                      {x : α × α |
                        match (motive := α × α → Prop) x with
                        | (a, b) => a < b})
                      p =
                    x }) ↦
            (↑x_2 : LTSeries α).length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b}))
          y →
        y ≤ x_1
Tactic: rw [height_eq_iSup_last_eq, iSup_subtype', ENat.iSup_coe_eq_top, bddAbove_def]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
h :
  ∀ (n : ℕ),
    ∃ (p : LTSeries α),
      RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          x ∧
        p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) =
          n
⊢ ¬∃ (x_1 : ℕ),
      ∀ (y : ℕ),
        Membership.mem (γ := Set ℕ)
            (Set.range
              fun
                (x_2 :
                  { p : LTSeries α //
                    RelSeries.last (r :=
                        {x : α × α |
                          match (motive := α × α → Prop) x with
                          | (a, b) => a < b})
                        p =
                      x }) ↦
              (↑x_2 : LTSeries α).length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b}))
            y →
          y ≤ x_1
have push : ∀ (x_1 : ℕ),
  ∃ (y : ℕ),
    Membership.mem (γ := Set ℕ)
        (Set.range
          fun
            (x_2 :
              { p : LTSeries α //
                RelSeries.last (r :=
                    {x : α × α |
                      match (motive := α × α → Prop) x with
                      | (a, b) => a < b})
                    p =
                  x }) ↦
          (↑x_2 : LTSeries α).length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}))
        y ∧
      x_1 < y
Tactic: push Not
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
h :
  ∀ (n : ℕ),
    ∃ (p : LTSeries α),
      RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          x ∧
        p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) =
          n
n : ℕ
⊢ ∃ (y : ℕ),
    Membership.mem (γ := Set ℕ)
        (Set.range
          fun
            (x_1 :
              { p : LTSeries α //
                RelSeries.last (r :=
                    {x : α × α |
                      match (motive := α × α → Prop) x with
                      | (a, b) => a < b})
                    p =
                  x }) ↦
          (↑x_1 : LTSeries α).length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}))
        y ∧
      n < y
have obtain : ∀ (p : LTSeries α)
  (hlast :
    RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p =
      x)
  (hp :
    p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) =
      n + 1),
  ∃ (y : ℕ),
    Membership.mem (γ := Set ℕ)
        (Set.range
          fun
            (x_1 :
              { p : LTSeries α //
                RelSeries.last (r :=
                    {x : α × α |
                      match (motive := α × α → Prop) x with
                      | (a, b) => a < b})
                    p =
                  x }) ↦
          (↑x_1 : LTSeries α).length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}))
        y ∧
      n < y
Tactic: obtain ⟨p, hlast, hp⟩ := h (n + 1)
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ coheight x = ⊤ ↔
    ∀ (n : ℕ),
      ∃ (p : LTSeries α),
        RelSeries.head (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p =
            x ∧
          p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b}) =
            n
have h : ∀ (n : ℕ),
  (∃ (p : LTSeries α),
      RelSeries.head (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          x ∧
        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 =
          x ∧
        p.length (r :=
            {x : αᵒᵈ × αᵒᵈ |
              match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
              | (a, b) => a < b}) =
          n
Tactic: convert! height_eq_top_iff (α := αᵒᵈ) (x := x) using 2 with n
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
⊢ (∃ (p : LTSeries α),
      RelSeries.head (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          x ∧
        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 =
          x ∧
        p.length (r :=
            {x : αᵒᵈ × αᵒᵈ |
              match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
              | (a, b) => a < b}) =
          n
have h : (∃ (p : LTSeries α),
    RelSeries.head (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        x ∧
      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 =
        x ∧
      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 α
x : α
n : ℕ
h :
  (∃ (p : LTSeries α),
      RelSeries.head (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          x ∧
        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 =
          x ∧
        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 =
          x ∧
        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 =
          x ∧
        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 =
        x ∧
      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 =
        x ∧
      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 α
x : α
n : ℕ
p : LTSeries α
hp :
  RelSeries.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
hl :
  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 =
        x ∧
      p.length (r :=
          {x : αᵒᵈ × αᵒᵈ |
            match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
            | (a, b) => a < b}) =
        n
have h : (RelSeries.reverse (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p).last
      (r :=
      {x : αᵒᵈ × αᵒᵈ |
        match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
        | (a, b) => a < b}) =
    x ∧
  (RelSeries.reverse (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p).length
      (r :=
      {x : αᵒᵈ × αᵒᵈ |
        match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
        | (a, b) => a < b}) =
    n
Tactic: use p.reverse