awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
p : LTSeries α
hp :
  RelSeries.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
hl :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    n
⊢ (RelSeries.reverse (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p).last
        (r :=
        {x : αᵒᵈ × αᵒᵈ |
          match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
          | (a, b) => a < b}) =
      x ∧
    (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
have h : (RelSeries.reverse (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p).last
    (r :=
    {x : αᵒᵈ × αᵒᵈ |
      match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
      | (a, b) => a < b}) =
  x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
p : LTSeries α
hp :
  RelSeries.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
hl :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    n
h :
  (RelSeries.reverse (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p).last
      (r :=
      {x : αᵒᵈ × αᵒᵈ |
        match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
        | (a, b) => a < b}) =
    x
⊢ (RelSeries.reverse (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p).last
        (r :=
        {x : αᵒᵈ × αᵒᵈ |
          match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
          | (a, b) => a < b}) =
      x ∧
    (RelSeries.reverse (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p).length
        (r :=
        {x : αᵒᵈ × αᵒᵈ |
          match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
          | (a, b) => a < b}) =
      n
have h₁ : (RelSeries.reverse (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p).length
    (r :=
    {x : αᵒᵈ × αᵒᵈ |
      match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
      | (a, b) => a < b}) =
  n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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
⊢ ∃ (p : LTSeries α),
    RelSeries.head (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        x ∧
      p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n
have h : (RelSeries.reverse (r :=
          {x : αᵒᵈ × αᵒᵈ |
            match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
            | (a, b) => a < b})
          p).head
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    x ∧
  (RelSeries.reverse (r :=
          {x : αᵒᵈ × αᵒᵈ |
            match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
            | (a, b) => a < b})
          p).length
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    n
Tactic: use p.reverse
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
p : LTSeries αᵒᵈ
hp :
  RelSeries.last (r :=
      {x : αᵒᵈ × αᵒᵈ |
        match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
        | (a, b) => a < b})
      p =
    x
hl :
  p.length (r :=
      {x : αᵒᵈ × αᵒᵈ |
        match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
        | (a, b) => a < b}) =
    n
⊢ (RelSeries.reverse (r :=
            {x : αᵒᵈ × αᵒᵈ |
              match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
              | (a, b) => a < b})
            p).head
        (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) =
      x ∧
    (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
have h : (RelSeries.reverse (r :=
        {x : αᵒᵈ × αᵒᵈ |
          match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
          | (a, b) => a < b})
        p).head
    (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}) =
  x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
p : LTSeries αᵒᵈ
hp :
  RelSeries.last (r :=
      {x : αᵒᵈ × αᵒᵈ |
        match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
        | (a, b) => a < b})
      p =
    x
hl :
  p.length (r :=
      {x : αᵒᵈ × αᵒᵈ |
        match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
        | (a, b) => a < b}) =
    n
h :
  (RelSeries.reverse (r :=
          {x : αᵒᵈ × αᵒᵈ |
            match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
            | (a, b) => a < b})
          p).head
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    x
⊢ (RelSeries.reverse (r :=
            {x : αᵒᵈ × αᵒᵈ |
              match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
              | (a, b) => a < b})
            p).head
        (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) =
      x ∧
    (RelSeries.reverse (r :=
            {x : αᵒᵈ × αᵒᵈ |
              match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
              | (a, b) => a < b})
            p).length
        (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) =
      n
have h₁ : (RelSeries.reverse (r :=
        {x : αᵒᵈ × αᵒᵈ |
          match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
          | (a, b) => a < b})
        p).length
    (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}) =
  n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
inst_1 : OrderBot α
h : ⊥ < x
⊢ 0 < height x
have rw : ¬IsMin x
Tactic: rw [height_pos]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
inst_1 : OrderTop α
h : x < ⊤
⊢ 0 < coheight x
have rw : ¬IsMax x
Tactic: rw [coheight_pos]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
h : (↑n : ℕ∞) < height x
⊢ ∃ y < x, height y = (↑n : ℕ∞)
have obtain : ∀ (m : ℕ) (hx : height x = (↑m : ℕ∞)), ∃ y < x, height y = (↑n : ℕ∞)
Tactic: obtain ⟨m, hx : height x = m⟩ := Option.ne_none_iff_exists'.mp hfin.ne_top
-- Lean 4 proof step from Mathlib.Order.KrullDimension (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
h : (↑n : ℕ∞) < height x
m : ℕ
hx : height x = (↑m : ℕ∞)
⊢ ∃ y < x, height y = (↑n : ℕ∞)
have h₁ : LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑m : ℕ∞)
Tactic: rw [hx] at h
Cleared hypotheses: h, hx
-- Lean 4 proof step from Mathlib.Order.KrullDimension (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
h : LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑m : ℕ∞)
hx : height x = (↑m : ℕ∞)
⊢ ∃ y < x, height y = (↑n : ℕ∞)
have h₁ : n < m
Tactic: norm_cast at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = (↑m : ℕ∞)
h : n < m
⊢ ∃ y < x, height y = (↑n : ℕ∞)
have 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 : ℕ∞)
Tactic: obtain ⟨p, hp, hlen⟩ := exists_series_of_height_eq_coe x hx
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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
⊢ ∃ y < x, height y = (↑n : ℕ∞)
have h₁ : p.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (⟨n, sorry⟩ :
        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, sorry⟩ :
          Fin
            (p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b}) +
              1))) =
    (↑n : ℕ∞)
Tactic: use p ⟨n, by lia⟩
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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.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 : ℕ∞)
have h₁ : p.toFun (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    (⟨n, sorry⟩ :
      Fin
        (p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) +
          1)) <
  x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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
⊢ 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 : ℕ∞)
have h₂ : height
    (p.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (⟨n, sorry⟩ :
        Fin
          (p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b}) +
            1))) =
  (↑n : ℕ∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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.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
have h₁ : p.toFun (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    (⟨n, sorry⟩ :
      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: rw [← hp]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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.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
have h₁ : (⟨n, sorry⟩ :
    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: apply LTSeries.strictMono
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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, ⋯⟩ :
      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}))
have h₁ : n < p.length (r := {x : α × α | x.1 < x.2})
Tactic: simp [Fin.last]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
⊢ height x = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔
    height x < ⊤ ∧ (∃ y < x, height y = (↑n : ℕ∞)) ∧ ∀ y < x, height y ≤ (↑n : ℕ∞)
have 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 : ℕ∞)
Tactic: wlog hfin : height x < ⊤
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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 : ℕ∞)
⊢ height x = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔
    height x < ⊤ ∧ (∃ y < x, height y = (↑n : ℕ∞)) ∧ ∀ y < x, height y ≤ (↑n : ℕ∞)
have 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 : ℕ∞)
Tactic: wlog hfin : height x < ⊤
Cleared hypotheses: x, n
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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 ↔
    height x < ⊤ ∧ (∃ y < x, height y = (↑n : ℕ∞)) ∧ ∀ y < x, height y ≤ (↑n : ℕ∞)
have simp : height x = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔ (∃ y < x, height y = (↑n : ℕ∞)) ∧ ∀ y < x, height y ≤ (↑n : ℕ∞)
Tactic: simp only [hfin, true_and]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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 : ℕ∞)) ∧ ∀ y < x, height y ≤ (↑n : ℕ∞)
have trans : height x = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔ (↑n : ℕ∞) < height x ∧ height x ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
Tactic: trans n < height x ∧ height x ≤ n + 1
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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
⊢ height x = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔ (∃ y < x, height y = (↑n : ℕ∞)) ∧ ∀ y < x, height y ≤ (↑n : ℕ∞)
have trans₁ : (↑n : ℕ∞) < height x ∧ 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
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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 ↔ (↑n : ℕ∞) < height x ∧ height x ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
have rw : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ height x ∧ height x ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔
  (↑n : ℕ∞) < height x ∧ height x ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
Tactic: rw [le_antisymm_iff, and_comm]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ (↑n : ℕ∞) < height x ∧ height x ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔
    (∃ y < x, height y = (↑n : ℕ∞)) ∧ ∀ y < x, height y ≤ (↑n : ℕ∞)
have a : (↑n : ℕ∞) < height x ↔ ∃ y < x, height y = (↑n : ℕ∞)
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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 : ℕ∞)
⊢ (↑n : ℕ∞) < height x ∧ height x ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔
    (∃ y < x, height y = (↑n : ℕ∞)) ∧ ∀ y < x, height y ≤ (↑n : ℕ∞)
have a₁ : height x ≤ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔ ∀ y < x, height y ≤ (↑n : ℕ∞)
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
⊢ height x = (↑n : ℕ∞) ↔
    height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1) ∧ ∀ y < x, height y < (↑n : ℕ∞)
have 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 : ℕ∞)
Tactic: wlog hfin : height x < ⊤
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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 : ℕ∞)
⊢ height x = (↑n : ℕ∞) ↔
    height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1) ∧ ∀ y < x, height y < (↑n : ℕ∞)
have 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 : ℕ∞)
Tactic: wlog hfin : height x < ⊤
Cleared hypotheses: x, n
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : 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 : ℕ∞)
have simp : height x = (↑n : ℕ∞) ↔ (n = 0 ∨ ∃ y < x, height y = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1) ∧ ∀ y < x, height y < (↑n : ℕ∞)
Tactic: simp only [hfin, true_and]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x = (↑n : ℕ∞) ↔ (n = 0 ∨ ∃ y < x, height y = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1) ∧ ∀ y < x, height y < (↑n : ℕ∞)
have cases : height x = (↑0 : ℕ∞) ↔
  (Eq (α := ℕ) 0 0 ∨ ∃ y < x, height y = HSub.hSub (α := ℕ∞) (↑0 : ℕ∞) 1) ∧ ∀ y < x, height y < (↑0 : ℕ∞)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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 : ℕ∞)
⊢ height x = (↑n : ℕ∞) ↔ (n = 0 ∨ ∃ y < x, height y = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1) ∧ ∀ y < x, height y < (↑n : ℕ∞)
have succ : ∀ (n : ℕ),
  height x = (↑(n + 1) : ℕ∞) ↔
    (n + 1 = 0 ∨ ∃ y < x, height y = HSub.hSub (α := ℕ∞) (↑(n + 1) : ℕ∞) 1) ∧ ∀ y < x, height y < (↑(n + 1) : ℕ∞)
Tactic: cases n
Cleared hypotheses: n