awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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).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 : α
⊢ height x = 0 ↔ IsMin x

Tactic:
simpa [isMin_iff_forall_not_lt] using height_le_coe_iff (x := x) (n := 0)

Premises used: Order.height_le_coe_iff, isMin_iff_forall_not_lt
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ coheight x = 0 ↔ IsMax x

Tactic:
height_eq_zero (α := αᵒᵈ)

Premises used: Order.height_eq_zero, OrderDual, Order.coheight, IsMax
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ height x ≠ 0 ↔ ¬IsMin x

Tactic:
height_eq_zero.not

Premises used: Iff.not, Order.height_eq_zero
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ 0 < height x ↔ ¬IsMin x

Tactic:
simp [pos_iff_ne_zero]

Premises used: pos_iff_ne_zero
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ coheight x ≠ 0 ↔ ¬IsMax x

Tactic:
coheight_eq_zero.not

Premises used: Iff.not, Order.coheight_eq_zero
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ 0 < coheight x ↔ ¬IsMax x

Tactic:
simp [pos_iff_ne_zero]

Premises used: pos_iff_ne_zero
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_3
inst : Preorder α
inst_1 : OrderBot α
⊢ height.{u_3} (α := α) ⊥ = 0

Tactic:
simp
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_3
inst : Preorder α
inst_1 : OrderTop α
⊢ coheight.{u_3} (α := α) ⊤ = 0

Tactic:
simp
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
inst_1 : OrderBot α
h : ⊥ < x
rw : ¬IsMin x
⊢ 0 < height x

Tactic:
rw [height_pos]

Premises used: Order.height_pos
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
inst_1 : OrderBot α
h : ⊥ < x
⊢ ¬IsMin x

Tactic:
grind [not_isMin_iff]

Premises used: not_isMin_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
inst_1 : OrderTop α
h : x < ⊤
rw : ¬IsMax x
⊢ 0 < coheight x

Tactic:
rw [coheight_pos]

Premises used: Order.coheight_pos
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
inst_1 : OrderTop α
h : x < ⊤
⊢ ¬IsMax x

Tactic:
grind [not_isMax_iff]

Premises used: not_isMax_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
h : (↑n : ℕ∞) < height x
obtain : ∀ (m : ℕ) (hx : height x = (↑m : ℕ∞)), ∃ y < x, height y = (↑n : ℕ∞)
⊢ ∃ y < x, height y = (↑n : ℕ∞)

Tactic:
obtain ⟨m, hx : height x = m⟩ := Option.ne_none_iff_exists'.mp hfin.ne_top

Premises used: LT.lt.ne_top, Option.ne_none_iff_exists', Iff.mp, Order.height
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
h : (↑n : ℕ∞) < height x
m : ℕ
hx : height x = (↑m : ℕ∞)
⊢ LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑m : ℕ∞)

Tactic:
rw [hx] at h
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
h : (↑n : ℕ∞) < height x
m : ℕ
hx : height x = (↑m : ℕ∞)
h₁ : LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑m : ℕ∞)
⊢ height x = (↑m : ℕ∞)

Tactic:
rw [hx] at h
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
h : LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑m : ℕ∞)
hx : height x = (↑m : ℕ∞)
⊢ n < m

Tactic:
norm_cast at h
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = (↑m : ℕ∞)
h : n < m
obtain :
  ∀ (p : LTSeries α)
    (hp :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        x)
    (hlen :
      p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        m),
    ∃ y < x, height y = (↑n : ℕ∞)
⊢ ∃ y < x, height y = (↑n : ℕ∞)

Tactic:
obtain ⟨p, hp, hlen⟩ := exists_series_of_height_eq_coe x hx

Premises used: Order.exists_series_of_height_eq_coe
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = (↑m : ℕ∞)
h : n < m
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    m
⊢ n <
    p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1

Tactic:
lia
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = (↑m : ℕ∞)
h : n < m
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    m
h₁ :
  p.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (⟨n, ⋯⟩ :
          Fin
            (p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b}) +
              1)) <
      x ∧
    height
        (p.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          (⟨n, ⋯⟩ :
            Fin
              (p.length (r :=
                  {x : α × α |
                    match (motive := α × α → Prop) x with
                    | (a, b) => a < b}) +
                1))) =
      (↑n : ℕ∞)
⊢ ∃ y < x, height y = (↑n : ℕ∞)

Tactic:
use p ⟨n, by lia⟩

Premises used: Fin.mk, RelSeries.toFun
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = (↑m : ℕ∞)
h : n < m
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    m
h₁ :
  p.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (⟨n, ⋯⟩ :
        Fin
          (p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b}) +
            1)) <
    x
h₂ :
  height
      (p.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (⟨n, ⋯⟩ :
          Fin
            (p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b}) +
              1))) =
    (↑n : ℕ∞)
⊢ p.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (⟨n, ⋯⟩ :
          Fin
            (p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b}) +
              1)) <
      x ∧
    height
        (p.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          (⟨n, ⋯⟩ :
            Fin
              (p.length (r :=
                  {x : α × α |
                    match (motive := α × α → Prop) x with
                    | (a, b) => a < b}) +
                1))) =
      (↑n : ℕ∞)

Tactic:
constructor
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = (↑m : ℕ∞)
h : n < m
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    m
h₁ :
  p.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (⟨n, ⋯⟩ :
        Fin
          (p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b}) +
            1)) <
    RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p
⊢ p.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (⟨n, ⋯⟩ :
        Fin
          (p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b}) +
            1)) <
    x

Tactic:
rw [← hp]
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = (↑m : ℕ∞)
h : n < m
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    m
h₁ :
  (⟨n, ⋯⟩ :
      Fin
        (p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) +
          1)) <
    Fin.last
      (p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}))
⊢ p.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (⟨n, ⋯⟩ :
        Fin
          (p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b}) +
            1)) <
    RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p

Tactic:
apply LTSeries.strictMono

Premises used: LTSeries.strictMono
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = (↑m : ℕ∞)
h : n < m
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    m
h₁ : n < p.length (r := {x : α × α | x.1 < x.2})
⊢ (⟨n, ⋯⟩ :
      Fin
        (p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) +
          1)) <
    Fin.last
      (p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}))

Tactic:
simp [Fin.last]

Premises used: Fin.last
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = (↑m : ℕ∞)
h : n < m
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    m
⊢ n < p.length (r := {x : α × α | x.1 < x.2})

Tactic:
lia
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = (↑m : ℕ∞)
h : n < m
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    m
⊢ (↑(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:
simp [hlen, hp, hx]
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = (↑m : ℕ∞)
h : n < m
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    m
⊢ height
      (p.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (⟨n, ⋯⟩ :
          Fin
            (p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b}) +
              1))) =
    (↑n : ℕ∞)

Tactic:
exact height_eq_index_of_length_eq_height_last (by simp [hlen, hp, hx]) ⟨n, by lia⟩

Premises used: Fin.mk, Order.height_eq_index_of_length_eq_height_last
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
hfin : coheight x < ⊤
⊢ (↑n : ℕ∞) < coheight x ↔ ∃ y > x, coheight y = (↑n : ℕ∞)

Tactic:
coe_lt_height_iff (α := αᵒᵈ) hfin

Premises used: OrderDual, Order.coe_lt_height_iff, Order.coheight
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
inr :
  ∀
    (this :
      ∀ {α : Type u_1} [inst : Preorder α] {x : α} {n : ℕ} (hfin : height x < ⊤),
        height x = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔
          height x < ⊤ ∧ (∃ y < x, height y = (↑n : ℕ∞)) ∧ ∀ y < x, height y ≤ (↑n : ℕ∞))
    (hfin : ¬height x < ⊤),
    height x = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔
      height x < ⊤ ∧ (∃ y < x, height y = (↑n : ℕ∞)) ∧ ∀ y < x, height y ≤ (↑n : ℕ∞)
wlog :
  ∀ {α : Type u_1} [inst : Preorder α] {x : α} {n : ℕ} (hfin : height x < ⊤),
    height x = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔
      height x < ⊤ ∧ (∃ y < x, height y = (↑n : ℕ∞)) ∧ ∀ y < x, height y ≤ (↑n : ℕ∞)
⊢ height x = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔
    height x < ⊤ ∧ (∃ y < x, height y = (↑n : ℕ∞)) ∧ ∀ y < x, height y ≤ (↑n : ℕ∞)

Tactic:
wlog hfin : height x < ⊤

Premises used: Order.height
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] {x : α} {n : ℕ} (hfin : height x < ⊤),
    height x = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔
      height x < ⊤ ∧ (∃ y < x, height y = (↑n : ℕ∞)) ∧ ∀ y < x, height y ≤ (↑n : ℕ∞)
hfin : ¬height x < ⊤
⊢ height x = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔
    height x < ⊤ ∧ (∃ y < x, height y = (↑n : ℕ∞)) ∧ ∀ y < x, height y ≤ (↑n : ℕ∞)

Tactic:
simp_all [← Nat.cast_add_one, -Nat.cast_add]

Premises used: Nat.cast_add, Nat.cast_add_one
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
simp : height x = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔ (∃ y < x, height y = (↑n : ℕ∞)) ∧ ∀ y < x, height y ≤ (↑n : ℕ∞)
⊢ height x = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔
    height x < ⊤ ∧ (∃ y < x, height y = (↑n : ℕ∞)) ∧ ∀ y < x, height y ≤ (↑n : ℕ∞)

Tactic:
simp only [hfin, true_and]

Premises used: true_and
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
trans : height x = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔ (↑n : ℕ∞) < height x ∧ height x ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
trans₁ :
  (↑n : ℕ∞) < height x ∧ height x ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔
    (∃ y < x, height y = (↑n : ℕ∞)) ∧ ∀ y < x, height y ≤ (↑n : ℕ∞)
⊢ height x = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔ (∃ y < x, height y = (↑n : ℕ∞)) ∧ ∀ y < x, height y ≤ (↑n : ℕ∞)

Tactic:
trans n < height x ∧ height x ≤ n + 1

Premises used: Order.height
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
rw :
  HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ height x ∧ height x ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔
    (↑n : ℕ∞) < height x ∧ height x ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
⊢ height x = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔ (↑n : ℕ∞) < height x ∧ height x ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1

Tactic:
rw [le_antisymm_iff, and_comm]

Premises used: and_comm, le_antisymm_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ height x ∧ height x ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔
    (↑n : ℕ∞) < height x ∧ height x ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1

Tactic:
simp [ENat.add_one_le_iff]

Premises used: ENat.add_one_le_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
a : (↑n : ℕ∞) < height x ↔ ∃ y < x, height y = (↑n : ℕ∞)
a₁ : height x ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔ ∀ y < x, height y ≤ (↑n : ℕ∞)
⊢ (↑n : ℕ∞) < height x ∧ height x ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔
    (∃ y < x, height y = (↑n : ℕ∞)) ∧ ∀ y < x, height y ≤ (↑n : ℕ∞)

Tactic:
congr! 1
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ (↑n : ℕ∞) < height x ↔ ∃ y < x, height y = (↑n : ℕ∞)

Tactic:
coe_lt_height_iff hfin

Premises used: Order.coe_lt_height_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ (↑n : ℕ∞) < height x ↔ ∃ y < x, height y = (↑n : ℕ∞)

Tactic:
exact coe_lt_height_iff hfin

Premises used: Order.coe_lt_height_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔ ∀ y < x, height y ≤ (↑n : ℕ∞)

Tactic:
simpa [hfin, ENat.lt_add_one_iff] using height_le_coe_iff (x := x) (n := n + 1)

Premises used: Order.height_le_coe_iff, ENat.lt_add_one_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
⊢ coheight x = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔
    coheight x < ⊤ ∧ (∃ y > x, coheight y = (↑n : ℕ∞)) ∧ ∀ y > x, coheight y ≤ (↑n : ℕ∞)

Tactic:
height_eq_coe_add_one_iff (α := αᵒᵈ)

Premises used: Order.height_eq_coe_add_one_iff, OrderDual, Order.coheight
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
inr :
  ∀
    (this :
      ∀ {α : Type u_1} [inst : Preorder α] {x : α} {n : ℕ} (hfin : height x < ⊤),
        height x = (↑n : ℕ∞) ↔
          height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1) ∧ ∀ y < x, height y < (↑n : ℕ∞))
    (hfin : ¬height x < ⊤),
    height x = (↑n : ℕ∞) ↔
      height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1) ∧ ∀ y < x, height y < (↑n : ℕ∞)
wlog :
  ∀ {α : Type u_1} [inst : Preorder α] {x : α} {n : ℕ} (hfin : height x < ⊤),
    height x = (↑n : ℕ∞) ↔
      height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1) ∧ ∀ y < x, height y < (↑n : ℕ∞)
⊢ height x = (↑n : ℕ∞) ↔
    height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1) ∧ ∀ y < x, height y < (↑n : ℕ∞)

Tactic:
wlog hfin : height x < ⊤

Premises used: Order.height
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] {x : α} {n : ℕ} (hfin : height x < ⊤),
    height x = (↑n : ℕ∞) ↔
      height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1) ∧ ∀ y < x, height y < (↑n : ℕ∞)
hfin : ¬height x < ⊤
⊢ height x = (↑n : ℕ∞) ↔
    height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1) ∧ ∀ y < x, height y < (↑n : ℕ∞)

Tactic:
simp_all
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
simp :
  height x = (↑n : ℕ∞) ↔ (n = 0 ∨ ∃ y < x, height y = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1) ∧ ∀ y < x, height y < (↑n : ℕ∞)
⊢ height x = (↑n : ℕ∞) ↔
    height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1) ∧ ∀ y < x, height y < (↑n : ℕ∞)

Tactic:
simp only [hfin, true_and]

Premises used: true_and
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
cases :
  height x = (↑0 : ℕ∞) ↔
    (Eq (α := ℕ) 0 0 ∨ ∃ y < x, height y = HSub.hSub (α := ℕ∞) (↑0 : ℕ∞) 1) ∧ ∀ y < x, height y < (↑0 : ℕ∞)
succ :
  ∀ (n : ℕ),
    height x = (↑(n + 1) : ℕ∞) ↔
      (n + 1 = 0 ∨ ∃ y < x, height y = HSub.hSub (α := ℕ∞) (↑(n + 1) : ℕ∞) 1) ∧ ∀ y < x, height y < (↑(n + 1) : ℕ∞)
⊢ height x = (↑n : ℕ∞) ↔ (n = 0 ∨ ∃ y < x, height y = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1) ∧ ∀ y < x, height y < (↑n : ℕ∞)

Tactic:
cases n
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
hfin : height x < ⊤
⊢ height x = (↑0 : ℕ∞) ↔
    (Eq (α := ℕ) 0 0 ∨ ∃ y < x, height y = HSub.hSub (α := ℕ∞) (↑0 : ℕ∞) 1) ∧ ∀ y < x, height y < (↑0 : ℕ∞)

Tactic:
simp [isMin_iff_forall_not_lt]

Premises used: isMin_iff_forall_not_lt
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
hfin : height x < ⊤
⊢ height x = (↑0 : ℕ∞) ↔
    (Eq (α := ℕ) 0 0 ∨ ∃ y < x, height y = HSub.hSub (α := ℕ∞) (↑0 : ℕ∞) 1) ∧ ∀ y < x, height y < (↑0 : ℕ∞)

Tactic:
case zero => simp [isMin_iff_forall_not_lt]

Premises used: isMin_iff_forall_not_lt
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
simp :
  height x = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔
    (∃ y < x, height y = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 - 1) ∧ ∀ y < x, height y < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
⊢ height x = (↑(n + 1) : ℕ∞) ↔
    (n + 1 = 0 ∨ ∃ y < x, height y = HSub.hSub (α := ℕ∞) (↑(n + 1) : ℕ∞) 1) ∧ ∀ y < x, height y < (↑(n + 1) : ℕ∞)

Tactic:
simp only [Nat.cast_add, Nat.cast_one, add_eq_zero, one_ne_zero, and_false, false_or]

Premises used: false_or, Nat.cast_add, and_false, add_eq_zero, one_ne_zero, Nat.cast_one
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
rw :
  (height x < ⊤ ∧ (∃ y < x, height y = (↑n : ℕ∞)) ∧ ∀ y < x, height y ≤ (↑n : ℕ∞)) ↔
    (∃ y < x, height y = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 - 1) ∧ ∀ y < x, height y < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
⊢ height x = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔
    (∃ y < x, height y = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 - 1) ∧ ∀ y < x, height y < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1

Tactic:
rw [height_eq_coe_add_one_iff]

Premises used: Order.height_eq_coe_add_one_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
simp :
  ((∃ y < x, height y = (↑n : ℕ∞)) ∧ ∀ y < x, height y ≤ (↑n : ℕ∞)) ↔
    (∃ y < x, height y = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 - 1) ∧ ∀ y < x, height y < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
⊢ (height x < ⊤ ∧ (∃ y < x, height y = (↑n : ℕ∞)) ∧ ∀ y < x, height y ≤ (↑n : ℕ∞)) ↔
    (∃ y < x, height y = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 - 1) ∧ ∀ y < x, height y < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1

Tactic:
simp only [hfin, true_and]

Premises used: true_and