awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ Membership.mem (α := α × α) (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    ((match (motive :=
          Fin
              (p.length (r :=
                    {x : WithBot α × WithBot α |
                      match (motive := WithBot α × WithBot α → Prop) x with
                      | (a, b) => a < b}) -
                  1 +
                1) →
            α)
          i.castSucc with
        | ⟨i, hi⟩ =>
          (p.toFun (r :=
                {x : WithBot α × WithBot α |
                  match (motive := WithBot α × WithBot α → Prop) x with
                  | (a, b) => a < b})
                ⟨i + 1, ⋯⟩).unbot
            ⋯,
        match (motive :=
          Fin
              (p.length (r :=
                    {x : WithBot α × WithBot α |
                      match (motive := WithBot α × WithBot α → Prop) x with
                      | (a, b) => a < b}) -
                  1 +
                1) →
            α)
          i.succ with
        | ⟨i, hi⟩ =>
          (p.toFun (r :=
                {x : WithBot α × WithBot α |
                  match (motive := WithBot α × WithBot α → Prop) x with
                  | (a, b) => a < b})
                ⟨i + 1, ⋯⟩).unbot
            ⋯) :
      α × α)

Tactic:
simpa [WithBot.unbot_lt_iff] using p.step ⟨i + 1, by lia⟩

Premises used: WithBot.unbot_lt_iff, Fin.mk, Fin.val, HAdd.hAdd, RelSeries.step, OfNat.ofNat
-- 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
p' : LTSeries α :=
  RelSeries.mk (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    (p.length (r :=
        {x : WithBot α × WithBot α |
          match (motive := WithBot α × WithBot α → Prop) x with
          | (a, b) => a < b}) -
      1)
    (fun
        (x :
          Fin
            (p.length (r :=
                  {x : WithBot α × WithBot α |
                    match (motive := WithBot α × WithBot α → Prop) x with
                    | (a, b) => a < b}) -
                1 +
              1)) ↦
      match (motive :=
        Fin
            (p.length (r :=
                  {x : WithBot α × WithBot α |
                    match (motive := WithBot α × WithBot α → Prop) x with
                    | (a, b) => a < b}) -
                1 +
              1) →
          α)
        x with
      | ⟨i, hi⟩ =>
        (p.toFun (r :=
              {x : WithBot α × WithBot α |
                match (motive := WithBot α × WithBot α → Prop) x with
                | (a, b) => a < b})
              ⟨i + 1, ⋯⟩).unbot
          ⋯)
    ⋯
simp :
  p.toFun (r := {x : WithBot α × WithBot α | x.1 < x.2})
      (⟨p.length (r := {x : WithBot α × WithBot α | x.1 < x.2}) - 1 + 1, ⋯⟩ :
        Fin (p.length (r := {x : WithBot α × WithBot α | x.1 < x.2}) + 1)) =
    p.toFun (r := {x : WithBot α × WithBot α | x.1 < x.2}) ⟨p.length (r := {x : WithBot α × WithBot α | x.1 < x.2}), ⋯⟩
⊢ RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p' =
    x

Tactic:
simp only [p', RelSeries.last, WithBot.unbot_eq_iff, ← hlast, Fin.last]

Premises used: WithBot.unbot_eq_iff, RelSeries.last, Fin.last
-- 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
p' : LTSeries α :=
  RelSeries.mk (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    (p.length (r :=
        {x : WithBot α × WithBot α |
          match (motive := WithBot α × WithBot α → Prop) x with
          | (a, b) => a < b}) -
      1)
    (fun
        (x :
          Fin
            (p.length (r :=
                  {x : WithBot α × WithBot α |
                    match (motive := WithBot α × WithBot α → Prop) x with
                    | (a, b) => a < b}) -
                1 +
              1)) ↦
      match (motive :=
        Fin
            (p.length (r :=
                  {x : WithBot α × WithBot α |
                    match (motive := WithBot α × WithBot α → Prop) x with
                    | (a, b) => a < b}) -
                1 +
              1) →
          α)
        x with
      | ⟨i, hi⟩ =>
        (p.toFun (r :=
              {x : WithBot α × WithBot α |
                match (motive := WithBot α × WithBot α → Prop) x with
                | (a, b) => a < b})
              ⟨i + 1, ⋯⟩).unbot
          ⋯)
    ⋯
e_a :
  p.length (r := {x : WithBot α × WithBot α | x.1 < x.2}) - 1 + 1 =
    p.length (r := {x : WithBot α × WithBot α | x.1 < x.2})
⊢ p.toFun (r := {x : WithBot α × WithBot α | x.1 < x.2})
      (⟨p.length (r := {x : WithBot α × WithBot α | x.1 < x.2}) - 1 + 1, ⋯⟩ :
        Fin (p.length (r := {x : WithBot α × WithBot α | x.1 < x.2}) + 1)) =
    p.toFun (r := {x : WithBot α × WithBot α | x.1 < x.2}) ⟨p.length (r := {x : WithBot α × WithBot α | x.1 < x.2}), ⋯⟩

Tactic:
congr
-- 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
p' : LTSeries α :=
  RelSeries.mk (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    (p.length (r :=
        {x : WithBot α × WithBot α |
          match (motive := WithBot α × WithBot α → Prop) x with
          | (a, b) => a < b}) -
      1)
    (fun
        (x :
          Fin
            (p.length (r :=
                  {x : WithBot α × WithBot α |
                    match (motive := WithBot α × WithBot α → Prop) x with
                    | (a, b) => a < b}) -
                1 +
              1)) ↦
      match (motive :=
        Fin
            (p.length (r :=
                  {x : WithBot α × WithBot α |
                    match (motive := WithBot α × WithBot α → Prop) x with
                    | (a, b) => a < b}) -
                1 +
              1) →
          α)
        x with
      | ⟨i, hi⟩ =>
        (p.toFun (r :=
              {x : WithBot α × WithBot α |
                match (motive := WithBot α × WithBot α → Prop) x with
                | (a, b) => a < b})
              ⟨i + 1, ⋯⟩).unbot
          ⋯)
    ⋯
⊢ p.length (r := {x : WithBot α × WithBot α | x.1 < x.2}) - 1 + 1 =
    p.length (r := {x : WithBot α × WithBot α | x.1 < x.2})

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
p' : LTSeries α :=
  RelSeries.mk (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    (p.length (r :=
        {x : WithBot α × WithBot α |
          match (motive := WithBot α × WithBot α → Prop) x with
          | (a, b) => a < b}) -
      1)
    (fun
        (x :
          Fin
            (p.length (r :=
                  {x : WithBot α × WithBot α |
                    match (motive := WithBot α × WithBot α → Prop) x with
                    | (a, b) => a < b}) -
                1 +
              1)) ↦
      match (motive :=
        Fin
            (p.length (r :=
                  {x : WithBot α × WithBot α |
                    match (motive := WithBot α × WithBot α → Prop) x with
                    | (a, b) => a < b}) -
                1 +
              1) →
          α)
        x with
      | ⟨i, hi⟩ =>
        (p.toFun (r :=
              {x : WithBot α × WithBot α |
                match (motive := WithBot α × WithBot α → Prop) x with
                | (a, b) => a < b})
              ⟨i + 1, ⋯⟩).unbot
          ⋯)
    ⋯
⊢ RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p' =
    x

Tactic:
have hlast' : p'.last = x := by
      simp only [p', RelSeries.last, WithBot.unbot_eq_iff, ← hlast, Fin.last]
      congr
      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
p' : LTSeries α :=
  RelSeries.mk (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    (p.length (r :=
        {x : WithBot α × WithBot α |
          match (motive := WithBot α × WithBot α → Prop) x with
          | (a, b) => a < b}) -
      1)
    (fun
        (x :
          Fin
            (p.length (r :=
                  {x : WithBot α × WithBot α |
                    match (motive := WithBot α × WithBot α → Prop) x with
                    | (a, b) => a < b}) -
                1 +
              1)) ↦
      match (motive :=
        Fin
            (p.length (r :=
                  {x : WithBot α × WithBot α |
                    match (motive := WithBot α × WithBot α → Prop) x with
                    | (a, b) => a < b}) -
                1 +
              1) →
          α)
        x with
      | ⟨i, hi⟩ =>
        (p.toFun (r :=
              {x : WithBot α × WithBot α |
                match (motive := WithBot α × WithBot α → Prop) x with
                | (a, b) => a < b})
              ⟨i + 1, ⋯⟩).unbot
          ⋯)
    ⋯
hlast' :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p' =
    x
this :
  (↑(p'.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height
      (RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p')
⊢ (↑(p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x + 1

Tactic:
simpa [p', hlast'] using this
-- 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
p' : LTSeries α :=
  RelSeries.mk (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    (p.length (r :=
        {x : WithBot α × WithBot α |
          match (motive := WithBot α × WithBot α → Prop) x with
          | (a, b) => a < b}) -
      1)
    (fun
        (x :
          Fin
            (p.length (r :=
                  {x : WithBot α × WithBot α |
                    match (motive := WithBot α × WithBot α → Prop) x with
                    | (a, b) => a < b}) -
                1 +
              1)) ↦
      match (motive :=
        Fin
            (p.length (r :=
                  {x : WithBot α × WithBot α |
                    match (motive := WithBot α × WithBot α → Prop) x with
                    | (a, b) => a < b}) -
                1 +
              1) →
          α)
        x with
      | ⟨i, hi⟩ =>
        (p.toFun (r :=
              {x : WithBot α × WithBot α |
                match (motive := WithBot α × WithBot α → Prop) x with
                | (a, b) => a < b})
              ⟨i + 1, ⋯⟩).unbot
          ⋯)
    ⋯
hlast' :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p' =
    x
suffices :
  (↑(p'.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height
      (RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p')
⊢ (↑(p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x + 1

Tactic:
suffices p'.length ≤ height p'.last by
      simpa [p', hlast'] using this
-- 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
p' : LTSeries α :=
  RelSeries.mk (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    (p.length (r :=
        {x : WithBot α × WithBot α |
          match (motive := WithBot α × WithBot α → Prop) x with
          | (a, b) => a < b}) -
      1)
    (fun
        (x :
          Fin
            (p.length (r :=
                  {x : WithBot α × WithBot α |
                    match (motive := WithBot α × WithBot α → Prop) x with
                    | (a, b) => a < b}) -
                1 +
              1)) ↦
      match (motive :=
        Fin
            (p.length (r :=
                  {x : WithBot α × WithBot α |
                    match (motive := WithBot α × WithBot α → Prop) x with
                    | (a, b) => a < b}) -
                1 +
              1) →
          α)
        x with
      | ⟨i, hi⟩ =>
        (p.toFun (r :=
              {x : WithBot α × WithBot α |
                match (motive := WithBot α × WithBot α → Prop) x with
                | (a, b) => a < b})
              ⟨i + 1, ⋯⟩).unbot
          ⋯)
    ⋯
hlast' :
  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})) :
      ℕ∞) ≤
    height
      (RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p')

Tactic:
apply length_le_height_last

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

Tactic:
rw [height_add_const]

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

Tactic:
apply iSup₂_le

Premises used: iSup₂_le
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
⊢ Membership.mem (γ := SetRel (WithBot α) (WithBot α))
    {x : WithBot α × WithBot α |
      match (motive := WithBot α × WithBot α → Prop) x with
      | (a, b) => a < b}
    (⊥,
      RelSeries.head (r :=
        {x : WithBot α × WithBot α |
          match (motive := WithBot α × WithBot α → Prop) x with
          | (a, b) => a < b})
        (p.map (fun (a : α) ↦ (↑a : WithBot α)) ⋯))

Tactic:
simp
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
p' : RelSeries (α := WithBot α)
  {x : WithBot α × WithBot α |
    match (motive := WithBot α × WithBot α → Prop) x with
    | (a, b) => a < b} :=
  RelSeries.cons (r :=
    {x : WithBot α × WithBot α |
      match (motive := WithBot α × WithBot α → Prop) x with
      | (a, b) => a < b})
    (p.map (fun (a : α) ↦ (↑a : WithBot α)) ⋯) ⊥ ⋯
⊢ p'.last (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b}) ≤
    (↑x : WithBot α)

Tactic:
simp [p', hlast]
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
p' : RelSeries (α := WithBot α)
  {x : WithBot α × WithBot α |
    match (motive := WithBot α × WithBot α → Prop) x with
    | (a, b) => a < b} :=
  RelSeries.cons (r :=
    {x : WithBot α × WithBot α |
      match (motive := WithBot α × WithBot α → Prop) x with
      | (a, b) => a < b})
    (p.map (fun (a : α) ↦ (↑a : WithBot α)) ⋯) ⊥ ⋯
⊢ HAdd.hAdd (α := ℕ∞)
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
      1 ≤
    (↑(p'.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)

Tactic:
simp [p']
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
p' : RelSeries (α := WithBot α)
  {x : WithBot α × WithBot α |
    match (motive := WithBot α × WithBot α → Prop) x with
    | (a, b) => a < b} :=
  RelSeries.cons (r :=
    {x : WithBot α × WithBot α |
      match (motive := WithBot α × WithBot α → Prop) x with
      | (a, b) => a < b})
    (p.map (fun (a : α) ↦ (↑a : WithBot α)) ⋯) ⊥ ⋯
⊢ HAdd.hAdd (α := ℕ∞)
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
      1 ≤
    height (↑x : WithBot α)

Tactic:
apply le_iSup₂_of_le p' (by simp [p', hlast]) (by simp [p'])

Premises used: le_iSup₂_of_le
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ coheight (↑x : WithTop α) = coheight x + 1

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

Premises used: WithTop.some, OrderDual, Order.height_coe_withBot, Order.coheight, WithTop
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
a : height (↑x : WithTop α) ≤ height x
a₁ : height x ≤ height (↑x : WithTop α)
⊢ height (↑x : WithTop α) = height x

Tactic:
apply le_antisymm

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

Tactic:
apply height_le

Premises used: Order.height_le
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries (WithTop α)
hlast :
  RelSeries.last (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithTop α)
i :
  Fin
    (p.length (r :=
        {x : WithTop α × WithTop α |
          match (motive := WithTop α × WithTop α → Prop) x with
          | (a, b) => a < b}) +
      1)
apply :
  p.toFun (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      i <
    ⊤
⊢ p.toFun (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      i ≠
    ⊤

Tactic:
apply WithTop.lt_top_iff_ne_top.mp

Premises used: Iff.mp, WithTop.lt_top_iff_ne_top