awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
hab :
  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})
      (Fin.last
        (p.length (r :=
          {x : WithTop α × WithTop α |
            match (motive := WithTop α × WithTop α → Prop) x with
            | (a, b) => a < b})))
hbc :
  p.toFun (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      (Fin.last
        (p.length (r :=
          {x : WithTop α × WithTop α |
            match (motive := WithTop α × WithTop α → Prop) x with
            | (a, b) => a < b}))) <
    ⊤
b : WithTop α
⊢ p.toFun (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      i <
    ⊤

Tactic:
apply lt_of_le_of_lt

Premises used: lt_of_le_of_lt
-- 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)
⊢ 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})
      (Fin.last
        (p.length (r :=
          {x : WithTop α × WithTop α |
            match (motive := WithTop α × WithTop α → Prop) x with
            | (a, b) => a < b})))

Tactic:
p.monotone (Fin.le_last _)

Premises used: LTSeries.monotone, Fin.le_last
-- 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)
⊢ 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})
      (Fin.last
        (p.length (r :=
          {x : WithTop α × WithTop α |
            match (motive := WithTop α × WithTop α → Prop) x with
            | (a, b) => a < b})))

Tactic:
exact p.monotone (Fin.le_last _)

Premises used: LTSeries.monotone, Fin.le_last
-- 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)
hbc :
  ∀
    (hlast :
      p.toFun (r :=
          {x : WithTop α × WithTop α |
            match (motive := WithTop α × WithTop α → Prop) x with
            | (a, b) => a < b})
          (Fin.last
            (p.length (r :=
              {x : WithTop α × WithTop α |
                match (motive := WithTop α × WithTop α → Prop) x with
                | (a, b) => a < b}))) =
        (↑x : WithTop α))
    (i :
      Fin
        (p.length (r :=
            {x : WithTop α × WithTop α |
              match (motive := WithTop α × WithTop α → Prop) x with
              | (a, b) => a < b}) +
          1)),
    p.toFun (r :=
        {x : WithTop α × WithTop α |
          match (motive := WithTop α × WithTop α → Prop) x with
          | (a, b) => a < b})
        (Fin.last
          (p.length (r :=
            {x : WithTop α × WithTop α |
              match (motive := WithTop α × WithTop α → Prop) x with
              | (a, b) => a < b}))) <
      ⊤
⊢ p.toFun (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      (Fin.last
        (p.length (r :=
          {x : WithTop α × WithTop α |
            match (motive := WithTop α × WithTop α → Prop) x with
            | (a, b) => a < b}))) <
    ⊤

Tactic:
rw [RelSeries.last] at hlast

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

Tactic:
simp [hlast]
-- 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}))
⊢ Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    ((p.toFun (r :=
            {x : WithTop α × WithTop α |
              match (motive := WithTop α × WithTop α → Prop) x with
              | (a, b) => a < b})
            i.castSucc).untop
        ⋯,
      (p.toFun (r :=
            {x : WithTop α × WithTop α |
              match (motive := WithTop α × WithTop α → Prop) x with
              | (a, b) => a < b})
            i.succ).untop
        ⋯)

Tactic:
simpa [WithTop.untop_lt_iff, WithTop.coe_untop] using p.step i

Premises used: WithTop.coe_untop, WithTop.untop_lt_iff, RelSeries.step
-- 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 α)
p' : LTSeries α :=
  RelSeries.mk (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    (p.length (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b}))
    (fun
        (i :
          Fin
            (p.length (r :=
                {x : WithTop α × WithTop α |
                  match (motive := WithTop α × WithTop α → Prop) x with
                  | (a, b) => a < b}) +
              1)) ↦
      (p.toFun (r :=
            {x : WithTop α × WithTop α |
              match (motive := WithTop α × WithTop α → Prop) x with
              | (a, b) => a < b})
            i).untop
        ⋯)
    ⋯
⊢ RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p' =
    x

Tactic:
simp only [p', RelSeries.last, WithTop.untop_eq_iff, ← hlast]

Premises used: WithTop.untop_eq_iff, RelSeries.last
-- 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 α)
p' : LTSeries α :=
  RelSeries.mk (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    (p.length (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b}))
    (fun
        (i :
          Fin
            (p.length (r :=
                {x : WithTop α × WithTop α |
                  match (motive := WithTop α × WithTop α → Prop) x with
                  | (a, b) => a < b}) +
              1)) ↦
      (p.toFun (r :=
            {x : WithTop α × WithTop α |
              match (motive := WithTop α × WithTop α → Prop) x with
              | (a, b) => a < b})
            i).untop
        ⋯)
    ⋯
⊢ 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, WithTop.untop_eq_iff, ← hlast]
-- 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 α)
p' : LTSeries α :=
  RelSeries.mk (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    (p.length (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b}))
    (fun
        (i :
          Fin
            (p.length (r :=
                {x : WithTop α × WithTop α |
                  match (motive := WithTop α × WithTop α → Prop) x with
                  | (a, b) => a < b}) +
              1)) ↦
      (p.toFun (r :=
            {x : WithTop α × WithTop α |
              match (motive := WithTop α × WithTop α → Prop) x with
              | (a, b) => a < b})
            i).untop
        ⋯)
    ⋯
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 : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x

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

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

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

Tactic:
apply height_le

Premises used: Order.height_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
p' : LTSeries (WithTop α) := p.map (fun (a : α) ↦ (↑a : WithTop α)) ⋯
⊢ RelSeries.last (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      p' ≤
    (↑x : WithTop α)

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' : LTSeries (WithTop α) := p.map (fun (a : α) ↦ (↑a : WithTop α)) ⋯
⊢ LE.le (α := ℕ∞)
    (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)
    (↑(p'.length (r :=
          {x : WithTop α × WithTop α |
            match (motive := WithTop α × WithTop α → 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' : LTSeries (WithTop α) := p.map (fun (a : α) ↦ (↑a : WithTop α)) ⋯
⊢ (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height (↑x : WithTop α)

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 : WithBot α) = coheight x

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

Premises used: WithBot.some, WithBot, Order.height_coe_withTop, OrderDual, Order.coheight
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
rw :
  (↑(⨆ (y : WithTop α), ⨆ (_ : y < ⊤), height y + 1) : WithBot ℕ∞) =
    HAdd.hAdd (α := WithBot ℕ∞) (↑(⨆ (a : α), height a) : WithBot ℕ∞) 1
⊢ krullDim.{u_1} (WithTop α) = krullDim α + 1

Tactic:
rw [← height_top_eq_krullDim, krullDim_eq_iSup_height_of_nonempty, height_eq_iSup_lt_height]

Premises used: Order.krullDim_eq_iSup_height_of_nonempty, Order.height_eq_iSup_lt_height, Order.height_top_eq_krullDim
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
norm_cast : ⨆ (y : WithTop α), ⨆ (_ : y < ⊤), height y + 1 = HAdd.hAdd (α := ℕ∞) (⨆ (a : α), height a) 1
⊢ (↑(⨆ (y : WithTop α), ⨆ (_ : y < ⊤), height y + 1) : WithBot ℕ∞) =
    HAdd.hAdd (α := WithBot ℕ∞) (↑(⨆ (a : α), height a) : WithBot ℕ∞) 1

Tactic:
norm_cast
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
simp_rw : ⨆ (y : WithTop α), ⨆ (_ : y ≠ ⊤), height y + 1 = HAdd.hAdd (α := ℕ∞) (⨆ (a : α), height a) 1
⊢ ⨆ (y : WithTop α), ⨆ (_ : y < ⊤), height y + 1 = HAdd.hAdd (α := ℕ∞) (⨆ (a : α), height a) 1

Tactic:
simp_rw [WithTop.lt_top_iff_ne_top]

Premises used: WithTop.lt_top_iff_ne_top
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
rw : Eq (α := ℕ∞) (⨆ (x : { y : WithTop α // y ≠ ⊤ }), height (↑x : WithTop α) + 1) (⨆ (i : α), height i + 1)
⊢ ⨆ (y : WithTop α), ⨆ (_ : y ≠ ⊤), height y + 1 = HAdd.hAdd (α := ℕ∞) (⨆ (a : α), height a) 1

Tactic:
rw [ENat.iSup_add, iSup_subtype']

Premises used: iSup_subtype', ENat.iSup_add
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
symm : Eq (α := ℕ∞) (⨆ (i : α), height i + 1) (⨆ (x : { y : WithTop α // y ≠ ⊤ }), height (↑x : WithTop α) + 1)
⊢ Eq (α := ℕ∞) (⨆ (x : { y : WithTop α // y ≠ ⊤ }), height (↑x : WithTop α) + 1) (⨆ (i : α), height i + 1)

Tactic:
symm
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
apply :
  ∀ (x : α),
    height.{u_1} (α := WithTop α)
          (↑((Equiv.symm Equiv.withTopSubtypeNe : (a : α) → { y : WithTop α // y ≠ ⊤ }) x) : WithTop α) +
        1 =
      height x + 1
⊢ Eq (α := ℕ∞) (⨆ (i : α), height i + 1) (⨆ (x : { y : WithTop α // y ≠ ⊤ }), height (↑x : WithTop α) + 1)

Tactic:
apply Equiv.withTopSubtypeNe.symm.iSup_congr

Premises used: Equiv.symm, Equiv.withTopSubtypeNe, Equiv.iSup_congr
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ ∀ (x : α),
    height.{u_1} (α := WithTop α)
          (↑((Equiv.symm Equiv.withTopSubtypeNe : (a : α) → { y : WithTop α // y ≠ ⊤ }) x) : WithTop α) +
        1 =
      height x + 1

Tactic:
simp
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
rw : krullDim.{u_1} (WithBot α)ᵒᵈ
| krullDim.{u_1} (WithBot α)

Tactic:
rw [← krullDim_orderDual]

Premises used: Order.krullDim_orderDual
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
conv_lhs : krullDim.{u_1} (WithBot α)ᵒᵈ = krullDim α + 1
⊢ krullDim.{u_1} (WithBot α) = krullDim α + 1

Tactic:
conv_lhs => rw [← krullDim_orderDual]

Premises used: Order.krullDim_orderDual
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
rw : krullDim.{u_1} αᵒᵈ + 1
| krullDim α + 1

Tactic:
rw [← krullDim_orderDual]

Premises used: Order.krullDim_orderDual
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
conv_rhs : krullDim.{u_1} (WithBot α)ᵒᵈ = krullDim.{u_1} αᵒᵈ + 1
⊢ krullDim.{u_1} (WithBot α)ᵒᵈ = krullDim α + 1

Tactic:
conv_rhs => rw [← krullDim_orderDual]

Premises used: Order.krullDim_orderDual
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ krullDim.{u_1} (WithBot α)ᵒᵈ = krullDim.{u_1} αᵒᵈ + 1

Tactic:
krullDim_WithTop (α := αᵒᵈ)

Premises used: WithBot, Order.krullDim_WithTop, OrderDual
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ krullDim.{u_1} (WithBot α)ᵒᵈ = krullDim.{u_1} αᵒᵈ + 1

Tactic:
exact krullDim_WithTop (α := αᵒᵈ)

Premises used: Order.krullDim_WithTop
-- Module: Mathlib.Order.KrullDimension
Goal:
⊢ krullDim (WithTop ℕ) = ⊤

Tactic:
simp [← WithBot.coe_top, ← WithBot.coe_one, ← WithBot.coe_add]

Premises used: WithBot.coe_one, WithBot.coe_top, WithBot.coe_add
-- Module: Mathlib.Order.KrullDimension
Goal:
⊢ height (α := ℕ∞) ⊤ = ⊤

Tactic:
simp only [← WithBot.coe_eq_coe, height_top_eq_krullDim, krullDim_enat, WithBot.coe_top]

Premises used: Order.krullDim_enat, Order.height_top_eq_krullDim, WithBot.coe_top, WithBot.coe_eq_coe
-- Module: Mathlib.Order.KrullDimension
Goal:
n : ℕ
⊢ height (α := ℕ∞) (↑n : ℕ∞) = (↑n : ℕ∞)

Tactic:
(height_coe_withTop _).trans (height_nat _)

Premises used: Order.height_nat, Order.height_coe_withTop, ENat, Eq.trans
-- Module: Mathlib.Order.KrullDimension
Goal:
n : ℕ
⊢ height (α := ℕ∞) (↑n : ℕ∞) = (↑n : ℕ∞)

Tactic:
exact (height_coe_withTop _).trans (height_nat _)

Premises used: Order.height_nat, Order.height_coe_withTop, Eq.trans