awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
f : ℕ → (↑(Set.Ioi a) : Type u_1)
hstrictmono : StrictMono f
m : ℕ
use :
  RelSeries.head (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (RelSeries.mk (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          m (fun (i : Fin (m + 1)) ↦ if i = 0 then a else (↑(f (↑i : ℕ)) : α)) ⋯) =
      a ∧
    RelSeries.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (RelSeries.mk (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          m (fun (i : Fin (m + 1)) ↦ if i = 0 then a else (↑(f (↑i : ℕ)) : α)) ⋯) =
      m
use₁ :
  ∀ (i : Fin m),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (if i.castSucc = 0 then a else (↑(f (↑i.castSucc : ℕ)) : α), if i.succ = 0 then a else (↑(f (↑i.succ : ℕ)) : α))
⊢ ∃ (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}) =
        m

Tactic:
use { length := m, toFun := fun i => if i = 0 then a else f i, step := ?step }
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
f : ℕ → (↑(Set.Ioi a) : Type u_1)
hstrictmono : StrictMono f
m : ℕ
⊢ RelSeries.head (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (RelSeries.mk (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          m (fun (i : Fin (m + 1)) ↦ if i = 0 then a else (↑(f (↑i : ℕ)) : α)) ⋯) =
      a ∧
    RelSeries.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (RelSeries.mk (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          m (fun (i : Fin (m + 1)) ↦ if i = 0 then a else (↑(f (↑i : ℕ)) : α)) ⋯) =
      m

Tactic:
simp [RelSeries.head]

Premises used: RelSeries.head
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
f : ℕ → (↑(Set.Ioi a) : Type u_1)
hstrictmono : StrictMono f
m : ℕ
⊢ RelSeries.head (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (RelSeries.mk (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          m (fun (i : Fin (m + 1)) ↦ if i = 0 then a else (↑(f (↑i : ℕ)) : α)) ⋯) =
      a ∧
    RelSeries.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (RelSeries.mk (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          m (fun (i : Fin (m + 1)) ↦ if i = 0 then a else (↑(f (↑i : ℕ)) : α)) ⋯) =
      m

Tactic:
case h => simp [RelSeries.head]

Premises used: RelSeries.head
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
f : ℕ → (↑(Set.Ioi a) : Type u_1)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
pos :
  ∀ (hzero : i = 0),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (if (⟨i, hi⟩ : Fin m).castSucc = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).castSucc : ℕ)) : α),
        if (⟨i, hi⟩ : Fin m).succ = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).succ : ℕ)) : α))
neg :
  ∀ (hzero : ¬i = 0),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (if (⟨i, hi⟩ : Fin m).castSucc = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).castSucc : ℕ)) : α),
        if (⟨i, hi⟩ : Fin m).succ = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).succ : ℕ)) : α))
⊢ Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (if (⟨i, hi⟩ : Fin m).castSucc = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).castSucc : ℕ)) : α),
      if (⟨i, hi⟩ : Fin m).succ = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).succ : ℕ)) : α))

Tactic:
by_cases hzero : i = 0
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
f : ℕ → (↑(Set.Ioi a) : Type u_1)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : i = 0
pos :
  ∀ (hi : 0 < m),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (if (⟨0, hi⟩ : Fin m).castSucc = 0 then a else (↑(f (↑(⟨0, hi⟩ : Fin m).castSucc : ℕ)) : α),
        if (⟨0, hi⟩ : Fin m).succ = 0 then a else (↑(f (↑(⟨0, hi⟩ : Fin m).succ : ℕ)) : α))
⊢ Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (if (⟨i, hi⟩ : Fin m).castSucc = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).castSucc : ℕ)) : α),
      if (⟨i, hi⟩ : Fin m).succ = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).succ : ℕ)) : α))

Tactic:
subst i
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
f : ℕ → (↑(Set.Ioi a) : Type u_1)
hstrictmono : StrictMono f
m : ℕ
hi : 0 < m
⊢ Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (if (⟨0, hi⟩ : Fin m).castSucc = 0 then a else (↑(f (↑(⟨0, hi⟩ : Fin m).castSucc : ℕ)) : α),
      if (⟨0, hi⟩ : Fin m).succ = 0 then a else (↑(f (↑(⟨0, hi⟩ : Fin m).succ : ℕ)) : α))

Tactic:
(f 1).prop

Premises used: Set.Ioi, Set.Mem, setOf, Subtype.prop, OfNat.ofNat, ite
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
f : ℕ → (↑(Set.Ioi a) : Type u_1)
hstrictmono : StrictMono f
m : ℕ
hi : 0 < m
⊢ Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (if (⟨0, hi⟩ : Fin m).castSucc = 0 then a else (↑(f (↑(⟨0, hi⟩ : Fin m).castSucc : ℕ)) : α),
      if (⟨0, hi⟩ : Fin m).succ = 0 then a else (↑(f (↑(⟨0, hi⟩ : Fin m).succ : ℕ)) : α))

Tactic:
exact (f 1).prop

Premises used: Subtype.prop, OfNat.ofNat
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
f : ℕ → (↑(Set.Ioi a) : Type u_1)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : ¬i = 0
this : f i < f (i + 1)
⊢ Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (if (⟨i, hi⟩ : Fin m).castSucc = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).castSucc : ℕ)) : α),
      if (⟨i, hi⟩ : Fin m).succ = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).succ : ℕ)) : α))

Tactic:
simp [Fin.ext_iff, hzero, this]

Premises used: Fin.ext_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
f : ℕ → (↑(Set.Ioi a) : Type u_1)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : ¬i = 0
neg : f i < f (i + 1)
⊢ Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (if (⟨i, hi⟩ : Fin m).castSucc = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).castSucc : ℕ)) : α),
      if (⟨i, hi⟩ : Fin m).succ = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).succ : ℕ)) : α))

Tactic:
suffices f i < f (i + 1) by simp [Fin.ext_iff, hzero, this]
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
f : ℕ → (↑(Set.Ioi a) : Type u_1)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : ¬i = 0
neg : i < i + 1
⊢ f i < f (i + 1)

Tactic:
apply hstrictmono
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
f : ℕ → (↑(Set.Ioi a) : Type u_1)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : ¬i = 0
⊢ i < i + 1

Tactic:
lia
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
f : ℕ → (↑(Set.Ioi a) : Type u_1)
hstrictmono : StrictMono f
m : ℕ
case case₁ :
  ∀ (h : Fin m),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (if h.castSucc = 0 then a else (↑(f (↑h.castSucc : ℕ)) : α), if h.succ = 0 then a else (↑(f (↑h.succ : ℕ)) : α))
case₂ case₃ :
  ∀ (h : Fin m) (i : ℕ) (hi : i < m),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (if (⟨i, hi⟩ : Fin m).castSucc = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).castSucc : ℕ)) : α),
        if (⟨i, hi⟩ : Fin m).succ = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).succ : ℕ)) : α))
case₄ :
  ∀ (i : ℕ) (hi : i < m),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (if (⟨i, hi⟩ : Fin m).castSucc = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).castSucc : ℕ)) : α),
        if (⟨i, hi⟩ : Fin m).succ = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).succ : ℕ)) : α))
pos :
  ∀ (i : ℕ) (hi : i < m) (hzero : i = 0),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (if (⟨i, hi⟩ : Fin m).castSucc = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).castSucc : ℕ)) : α),
        if (⟨i, hi⟩ : Fin m).succ = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).succ : ℕ)) : α))
neg neg₁ :
  ∀ (i : ℕ) (hi : i < m) (hzero : ¬i = 0),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (if (⟨i, hi⟩ : Fin m).castSucc = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).castSucc : ℕ)) : α),
        if (⟨i, hi⟩ : Fin m).succ = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).succ : ℕ)) : α))
⊢ ∀ (i : Fin m),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (if i.castSucc = 0 then a else (↑(f (↑i.castSucc : ℕ)) : α), if i.succ = 0 then a else (↑(f (↑i.succ : ℕ)) : α))

Tactic:
case step =>
    intro ⟨i, hi⟩
    by_cases hzero : i = 0
    · subst i
      exact (f 1).prop
    · suffices f i < f (i + 1) by simp [Fin.ext_iff, hzero, this]
      apply hstrictmono
      lia

Premises used: Subtype.prop, OfNat.ofNat
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMinOrder α
a : α
⊢ height a = ⊤

Tactic:
coheight_of_noMaxOrder (α := αᵒᵈ) a

Premises used: Order.coheight_of_noMaxOrder, OrderDual, Order.coheight
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMaxOrder α
⊢ krullDim α = ⊤

Tactic:
simp [krullDim_eq_iSup_coheight, coheight_of_noMaxOrder]

Premises used: Order.coheight_of_noMaxOrder, Order.krullDim_eq_iSup_coheight
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMinOrder α
⊢ krullDim α = ⊤

Tactic:
simp [krullDim_eq_iSup_height, height_of_noMinOrder]

Premises used: Order.height_of_noMinOrder, Order.krullDim_eq_iSup_height
-- Module: Mathlib.Order.KrullDimension
Goal:
n : ℕ
⊢ coheight n = ⊤

Tactic:
coheight_of_noMaxOrder ..

Premises used: Order.coheight_of_noMaxOrder
-- Module: Mathlib.Order.KrullDimension
Goal:
⊢ krullDim ℕ = ⊤

Tactic:
krullDim_of_noMaxOrder ..

Premises used: Order.krullDim_of_noMaxOrder
-- Module: Mathlib.Order.KrullDimension
Goal:
n : ℤ
⊢ height n = ⊤

Tactic:
height_of_noMinOrder ..

Premises used: Order.height_of_noMinOrder
-- Module: Mathlib.Order.KrullDimension
Goal:
n : ℤ
⊢ coheight n = ⊤

Tactic:
coheight_of_noMaxOrder ..

Premises used: Order.coheight_of_noMaxOrder
-- Module: Mathlib.Order.KrullDimension
Goal:
⊢ krullDim ℤ = ⊤

Tactic:
krullDim_of_noMaxOrder ..

Premises used: Order.krullDim_of_noMaxOrder
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
a : height (↑x : WithBot α) ≤ height x + 1
a₁ : height x + 1 ≤ height (↑x : WithBot α)
⊢ height (↑x : WithBot α) = height x + 1

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
a :
  ∀ (p : LTSeries (WithBot α)),
    RelSeries.last (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b})
          p =
        (↑x : WithBot α) →
      (↑(p.length (r :=
              {x : WithBot α × WithBot α |
                match (motive := WithBot α × WithBot α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
        height x + 1
⊢ height (↑x : WithBot α) ≤ height x + 1

Tactic:
apply height_le

Premises used: Order.height_le
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries (WithBot α)
hlast :
  RelSeries.last (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithBot α)
a :
  ∀
    (this :
      ∀ {α : Type u_1} [inst : Preorder α] (x : α) (p : LTSeries (WithBot α))
        (hlast :
          RelSeries.last (r :=
              {x : WithBot α × WithBot α |
                match (motive := WithBot α × WithBot α → Prop) x with
                | (a, b) => a < b})
              p =
            (↑x : WithBot α))
        (hlenpos :
          p.length (r :=
              {x : WithBot α × WithBot α |
                match (motive := WithBot α × WithBot α → Prop) x with
                | (a, b) => a < b}) ≠
            0),
        (↑(p.length (r :=
                {x : WithBot α × WithBot α |
                  match (motive := WithBot α × WithBot α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) ≤
          height x + 1)
    (hlenpos :
      ¬p.length (r :=
            {x : WithBot α × WithBot α |
              match (motive := WithBot α × WithBot α → Prop) x with
              | (a, b) => a < b}) ≠
          0),
    (↑(p.length (r :=
            {x : WithBot α × WithBot α |
              match (motive := WithBot α × WithBot α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞) ≤
      height x + 1
wlog :
  ∀ {α : Type u_1} [inst : Preorder α] (x : α) (p : LTSeries (WithBot α))
    (hlast :
      RelSeries.last (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b})
          p =
        (↑x : WithBot α))
    (hlenpos :
      p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b}) ≠
        0),
    (↑(p.length (r :=
            {x : WithBot α × WithBot α |
              match (motive := WithBot α × WithBot α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞) ≤
      height x + 1
⊢ (↑(p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x + 1

Tactic:
wlog hlenpos : p.length ≠ 0

Premises used: RelSeries.length
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries (WithBot α)
hlast :
  RelSeries.last (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithBot α)
this :
  ∀ {α : Type u_1} [inst : Preorder α] (x : α) (p : LTSeries (WithBot α))
    (hlast :
      RelSeries.last (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b})
          p =
        (↑x : WithBot α))
    (hlenpos :
      p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b}) ≠
        0),
    (↑(p.length (r :=
            {x : WithBot α × WithBot α |
              match (motive := WithBot α × WithBot α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞) ≤
      height x + 1
hlenpos :
  ¬p.length (r :=
        {x : WithBot α × WithBot α |
          match (motive := WithBot α × WithBot α → Prop) x with
          | (a, b) => a < b}) ≠
      0
⊢ (↑(p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x + 1

Tactic:
simp_all
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
p : LTSeries (WithBot α)
hlast :
  RelSeries.last (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithBot α)
hlenpos :
  p.length (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b}) ≠
    0
x_1 :
  Fin
    (p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b}) -
        1 +
      1)
i : ℕ
hi :
  i <
    p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b}) -
        1 +
      1
⊢ i + 1 <
    p.length (r :=
        {x : WithBot α × WithBot α |
          match (motive := WithBot α × WithBot α → Prop) x with
          | (a, b) => a < b}) +
      1

Tactic:
lia
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
p : LTSeries (WithBot α)
hlast :
  RelSeries.last (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithBot α)
hlenpos :
  p.length (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b}) ≠
    0
x_1 :
  Fin
    (p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b}) -
        1 +
      1)
i : ℕ
hi :
  i <
    p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b}) -
        1 +
      1
apply :
  RelSeries.head (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})
      p <
    p.toFun (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})
      ⟨i + 1, ⋯⟩
⊢ p.toFun (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})
      (⟨i + 1, ⋯⟩ :
        Fin
          (p.length (r :=
              {x : WithBot α × WithBot α |
                match (motive := WithBot α × WithBot α → Prop) x with
                | (a, b) => a < b}) +
            1)) ≠
    ⊥

Tactic:
apply ne_bot_of_gt (b := p.head)

Premises used: ne_bot_of_gt
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
p : LTSeries (WithBot α)
hlast :
  RelSeries.last (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithBot α)
hlenpos :
  p.length (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b}) ≠
    0
x_1 :
  Fin
    (p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b}) -
        1 +
      1)
i : ℕ
hi :
  i <
    p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b}) -
        1 +
      1
a :
  0 <
    (⟨i + 1, ⋯⟩ :
      Fin
        (p.length (r :=
            {x : WithBot α × WithBot α |
              match (motive := WithBot α × WithBot α → Prop) x with
              | (a, b) => a < b}) +
          1))
⊢ RelSeries.head (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})
      p <
    p.toFun (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})
      ⟨i + 1, ⋯⟩

Tactic:
apply p.strictMono

Premises used: LTSeries.strictMono
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
p : LTSeries (WithBot α)
hlast :
  RelSeries.last (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithBot α)
hlenpos :
  p.length (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b}) ≠
    0
x_1 :
  Fin
    (p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b}) -
        1 +
      1)
i : ℕ
hi :
  i <
    p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b}) -
        1 +
      1
⊢ 0 <
    (⟨i + 1, ⋯⟩ :
      Fin
        (p.length (r :=
            {x : WithBot α × WithBot α |
              match (motive := WithBot α × WithBot α → Prop) x with
              | (a, b) => a < b}) +
          1))

Tactic:
compare_gt_iff_gt.mp rfl

Premises used: compare_gt_iff_gt, Iff.mp, rfl
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
p : LTSeries (WithBot α)
hlast :
  RelSeries.last (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithBot α)
hlenpos :
  p.length (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b}) ≠
    0
x_1 :
  Fin
    (p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b}) -
        1 +
      1)
i : ℕ
hi :
  i <
    p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b}) -
        1 +
      1
⊢ 0 <
    (⟨i + 1, ⋯⟩ :
      Fin
        (p.length (r :=
            {x : WithBot α × WithBot α |
              match (motive := WithBot α × WithBot α → Prop) x with
              | (a, b) => a < b}) +
          1))

Tactic:
exact compare_gt_iff_gt.mp rfl

Premises used: compare_gt_iff_gt, Iff.mp
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
p : LTSeries (WithBot α)
hlast :
  RelSeries.last (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithBot α)
hlenpos :
  p.length (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b}) ≠
    0
i :
  Fin
    (p.length (r :=
        {x : WithBot α × WithBot α |
          match (motive := WithBot α × WithBot α → Prop) x with
          | (a, b) => a < b}) -
      1)
⊢ (↑i : ℕ) + 1 <
    p.length (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})

Tactic:
lia