awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x y : α
hyx : y < x
p : LTSeries α
hp :
  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:
apply le_iSup₂_of_le (p.snoc x (hp ▸ hyx)) (by simp) (by simp)

Premises used: Eq.rec, RelSeries.snoc, le_iSup₂_of_le, Eq.symm
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ coheight x = ⨆ (y : α), ⨆ (_ : y > x), coheight y + 1

Tactic:
height_eq_iSup_lt_height (α := αᵒᵈ) x

Premises used: Order.height_eq_iSup_lt_height, OrderDual, Order.coheight
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
rw : ∀ (i : α) (j : i < x), height i + 1 ≤ (↑n : ℕ∞)
| height x ≤ (↑n : ℕ∞)

Tactic:
rw [height_eq_iSup_lt_height, iSup₂_le_iff]

Premises used: Order.height_eq_iSup_lt_height, iSup₂_le_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
conv_lhs : (∀ (i : α) (j : i < x), height i + 1 ≤ (↑n : ℕ∞)) ↔ ∀ y < x, height y < (↑n : ℕ∞)
⊢ height x ≤ (↑n : ℕ∞) ↔ ∀ y < x, height y < (↑n : ℕ∞)

Tactic:
conv_lhs => rw [height_eq_iSup_lt_height, iSup₂_le_iff]

Premises used: Order.height_eq_iSup_lt_height, iSup₂_le_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
a : ∀ y < x, height y + 1 ≤ (↑n : ℕ∞) ↔ height y < (↑n : ℕ∞)
⊢ (∀ (i : α) (j : i < x), height i + 1 ≤ (↑n : ℕ∞)) ↔ ∀ y < x, height y < (↑n : ℕ∞)

Tactic:
congr! 2 with y _
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
y : α
h : y < x
a : HAdd.hAdd (α := ℕ∞) ⊤ 1 ≤ (↑n : ℕ∞) ↔ LT.lt (α := ℕ∞) ⊤ (↑n : ℕ∞)
a₁ : ∀ (a : ℕ), HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) 1 ≤ (↑n : ℕ∞) ↔ LT.lt (α := ℕ∞) (↑a : ℕ∞) (↑n : ℕ∞)
⊢ height y + 1 ≤ (↑n : ℕ∞) ↔ height y < (↑n : ℕ∞)

Tactic:
cases height y

Premises used: Order.height
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
y : α
h : y < x
⊢ HAdd.hAdd (α := ℕ∞) ⊤ 1 ≤ (↑n : ℕ∞) ↔ LT.lt (α := ℕ∞) ⊤ (↑n : ℕ∞)

Tactic:
simp
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
y : α
h : y < x
a_1 : ℕ
a a₁ a₂ a₃ : a_1 + 1 ≤ n ↔ a_1 < n
⊢ HAdd.hAdd (α := ℕ∞) (↑a_1 : ℕ∞) 1 ≤ (↑n : ℕ∞) ↔ LT.lt (α := ℕ∞) (↑a_1 : ℕ∞) (↑n : ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
⊢ coheight x ≤ (↑n : ℕ∞) ↔ ∀ y > x, coheight y < (↑n : ℕ∞)

Tactic:
height_le_coe_iff (α := αᵒᵈ)

Premises used: Order.height_le_coe_iff, OrderDual, Order.coheight
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
h : height x = ⊤
n : ℕ
apply : (↑n : ℕ∞) ≤ height x
⊢ ∃ (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:
apply exists_series_of_le_height x (n := n)

Premises used: Order.exists_series_of_le_height
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
h : height x = ⊤
n : ℕ
⊢ (↑n : ℕ∞) ≤ height x

Tactic:
simp [h]
-- Module: Mathlib.Order.KrullDimension
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
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
⊢ height x = ⊤

Tactic:
rw [height_eq_iSup_last_eq, iSup_subtype', ENat.iSup_coe_eq_top, bddAbove_def]

Premises used: iSup_subtype', ENat.iSup_coe_eq_top, bddAbove_def, Order.height_eq_iSup_last_eq
-- Module: Mathlib.Order.KrullDimension
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
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
⊢ ¬∃ (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:
push Not

Premises used: Not
-- Module: Mathlib.Order.KrullDimension
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 : ℕ
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
⊢ ∃ (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)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Order.KrullDimension
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 : ℕ
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
⊢ (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}))
      (Subtype.mk (p := fun (p : LTSeries α) ↦
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          x)
        p hlast) =
    p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})

Tactic:
simp [hp]
-- Module: Mathlib.Order.KrullDimension
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 : ℕ
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
⊢ n <
    p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})

Tactic:
simp [hp]
-- Module: Mathlib.Order.KrullDimension
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 : ℕ
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:
exact ⟨p.length, ⟨⟨⟨p, hlast⟩, by simp [hp]⟩, by simp [hp]⟩⟩
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ 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

Tactic:
height_eq_top_iff (α := αᵒᵈ) (x := x)

Premises used: Order.height_eq_top_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
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
⊢ 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

Tactic:
convert! height_eq_top_iff (α := αᵒᵈ) (x := x) using 2 with n

Premises used: Order.height_eq_top_iff
-- Module: Mathlib.Order.KrullDimension
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
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
⊢ (∃ (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
-- Module: Mathlib.Order.KrullDimension
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
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
⊢ ∃ (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:
use p.reverse

Premises used: RelSeries.reverse
-- Module: Mathlib.Order.KrullDimension
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
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
h₁ :
  (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
⊢ (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:
constructor
-- Module: Mathlib.Order.KrullDimension
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
⊢ (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

Tactic:
simpa
-- Module: Mathlib.Order.KrullDimension
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
⊢ (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:
simpa
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
p : LTSeries αᵒᵈ
hp :
  RelSeries.last (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
h :
  (RelSeries.reverse (r :=
            {x : αᵒᵈ × αᵒᵈ |
              match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
              | (a, b) => a < b})
            p).head
        (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
⊢ ∃ (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:
use p.reverse

Premises used: RelSeries.reverse
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
p : LTSeries αᵒᵈ
hp :
  RelSeries.last (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
h :
  (RelSeries.reverse (r :=
          {x : αᵒᵈ × αᵒᵈ |
            match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
            | (a, b) => a < b})
          p).head
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    x
h₁ :
  (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
⊢ (RelSeries.reverse (r :=
            {x : αᵒᵈ × αᵒᵈ |
              match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
              | (a, b) => a < b})
            p).head
        (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:
constructor
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
p : LTSeries αᵒᵈ
hp :
  RelSeries.last (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
⊢ (RelSeries.reverse (r :=
          {x : αᵒᵈ × αᵒᵈ |
            match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
            | (a, b) => a < b})
          p).head
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    x

Tactic:
simpa