awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
hne :
  Nonempty.{max 1 (u_1 + 1)}
    { p : LTSeries α //
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a }
⊢ height a + n =
    ⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          a),
        (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) +
          n
have rw : (⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          a),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞)) +
    n =
  ⨆ (p : LTSeries α),
    ⨆ (_ :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a),
      (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) +
        n
Tactic: rw [height_eq_iSup_last_eq, iSup_subtype', iSup_subtype', ENat.iSup_add]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
hne :
  Nonempty.{max 1 (u_1 + 1)}
    { p : LTSeries α //
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a }
rw :
  (⨆ (p : LTSeries α),
        ⨆ (_ :
          RelSeries.last (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p =
            a),
          (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞)) +
      n =
    ⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          a),
        (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) +
          n
⊢ height a + n =
    ⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          a),
        (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) +
          n
have rw₁ : (⨆ (x :
      { p : LTSeries α //
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          a }),
      (↑((↑x : LTSeries α).length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)) +
    n =
  ⨆ (p : LTSeries α),
    ⨆ (_ :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a),
      (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) +
        n
Tactic: rw [height_eq_iSup_last_eq, iSup_subtype', iSup_subtype', ENat.iSup_add]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
hne :
  Nonempty.{max 1 (u_1 + 1)}
    { p : LTSeries α //
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a }
rw :
  (⨆ (p : LTSeries α),
        ⨆ (_ :
          RelSeries.last (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p =
            a),
          (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞)) +
      n =
    ⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          a),
        (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) +
          n
rw₁ :
  (⨆ (x :
        { p : LTSeries α //
          RelSeries.last (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p =
            a }),
        (↑((↑x : LTSeries α).length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞)) +
      n =
    ⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          a),
        (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) +
          n
⊢ height a + n =
    ⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          a),
        (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) +
          n
have rw₂ : (⨆ (x :
      { p : LTSeries α //
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          a }),
      (↑((↑x : LTSeries α).length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)) +
    n =
  ⨆ (x :
    { p : LTSeries α //
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a }),
    (↑((↑x : LTSeries α).length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞) +
      n
Tactic: rw [height_eq_iSup_last_eq, iSup_subtype', iSup_subtype', ENat.iSup_add]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
⊢ height x < height y
have rw : ∀ (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 y
Tactic: rw [← ENat.add_one_le_iff hfin.ne, height_add_const, iSup₂_le_iff]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
p : LTSeries α
hlast :
  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 y
have this : (↑((RelSeries.snoc (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p y sorry).length
        (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})) :
    ℕ∞) ≤
  height
    ((RelSeries.snoc (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p y sorry).last
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}))
Tactic: have := length_le_height_last (p := p.snoc y (by simp [*]))
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : a < b
hfin : height a = ⊤
⊢ ⊤ ≤ height b
have rw : height a ≤ height b
Tactic: rw [← hfin]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : a < b
hfin : height a = ⊤
⊢ HAdd.hAdd (α := ℕ∞) ⊤ 1 ≤ height b
have this : ⊤ ≤ height b
Tactic: have : ⊤ ≤ height b := by
      rw [← hfin]
      gcongr
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : a < b
n : ℕ
hfin : height a = (↑n : ℕ∞)
⊢ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ height b
have coe : (↑n : ℕ∞) < height b
Tactic: apply Order.add_one_le_of_lt
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : a < b
n : ℕ
hfin : height a = (↑n : ℕ∞)
⊢ (↑n : ℕ∞) < height b
have coe : height a < height b
Tactic: rw [← hfin]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : a < b
n : ℕ
hfin : height a = (↑n : ℕ∞)
⊢ height a < height b
have coe : height a < ⊤
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : a < b
⊢ height a + 1 ≤ height b
have cases : ∀ (x : ℕ∞) (hfin : height a = x), x + 1 ≤ height b
Tactic: cases hfin : height a with
  | top =>
    have : ⊤ ≤ height b := by
      rw [← hfin]
      gcongr
    simp [this]
  | coe n =>
    apply Order.add_one_le_of_lt
    rw [← hfin]
    gcongr
    simp [hfin]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : b < a
hfin : coheight a = ⊤
⊢ ⊤ ≤ coheight b
have rw : coheight a ≤ coheight b
Tactic: rw [← hfin]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : b < a
hfin : coheight a = ⊤
⊢ HAdd.hAdd (α := ℕ∞) ⊤ 1 ≤ coheight b
have this : ⊤ ≤ coheight b
Tactic: have : ⊤ ≤ coheight b := by
      rw [← hfin]
      gcongr
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : b < a
n : ℕ
hfin : coheight a = (↑n : ℕ∞)
⊢ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ coheight b
have coe : (↑n : ℕ∞) < coheight b
Tactic: apply Order.add_one_le_of_lt
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : b < a
n : ℕ
hfin : coheight a = (↑n : ℕ∞)
⊢ (↑n : ℕ∞) < coheight b
have coe : coheight a < coheight b
Tactic: rw [← hfin]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : b < a
n : ℕ
hfin : coheight a = (↑n : ℕ∞)
⊢ coheight a < coheight b
have coe : coheight a < ⊤
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : b < a
⊢ coheight a + 1 ≤ coheight b
have cases : ∀ (x : ℕ∞) (hfin : coheight a = x), x + 1 ≤ coheight b
Tactic: cases hfin : coheight a with
  | top =>
    have : ⊤ ≤ coheight b := by
      rw [← hfin]
      gcongr
    simp [this]
  | coe n =>
    apply Order.add_one_le_of_lt
    rw [← hfin]
    gcongr
    simp [hfin]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
x : α
⊢ height x ≤ height (f x)
have simp : LE.le (α := ℕ∞)
  (⨆ (p : LTSeries α),
    ⨆ (_ : RelSeries.last (r := {x : α × α | x.1 < x.2}) p = x), (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞))
  (⨆ (p : LTSeries β),
    ⨆ (_ : RelSeries.last (r := {x : β × β | x.1 < x.2}) p = f x), (↑(p.length (r := {x : β × β | x.1 < x.2})) : ℕ∞))
Tactic: simp only [height_eq_iSup_last_eq]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
x : α
⊢ LE.le (α := ℕ∞)
    (⨆ (p : LTSeries α),
      ⨆ (_ : RelSeries.last (r := {x : α × α | x.1 < x.2}) p = x), (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞))
    (⨆ (p : LTSeries β),
      ⨆ (_ : RelSeries.last (r := {x : β × β | x.1 < x.2}) p = f x), (↑(p.length (r := {x : β × β | x.1 < x.2})) : ℕ∞))
have h : ∀ (i : LTSeries α) (j : RelSeries.last (r := {x : α × α | x.1 < x.2}) i = x),
  LE.le (α := ℕ∞) (↑(i.length (r := {x : α × α | x.1 < x.2})) : ℕ∞)
    (⨆ (p : LTSeries β),
      ⨆ (_ : RelSeries.last (r := {x : β × β | x.1 < x.2}) p = f x), (↑(p.length (r := {x : β × β | x.1 < x.2})) : ℕ∞))
Tactic: apply iSup₂_le
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
x : α
⊢ coheight x ≤ coheight (f x)
have hf₁ : StrictMono f
Tactic: apply height_le_height_apply_of_strictMono (α := αᵒᵈ)
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α) (b : β), f a < b → ∃ (a' : α), a < a' ∧ f a' = b
a : α
⊢ coheight a = coheight (f a)
have refine : coheight (f a) ≤ coheight a
Tactic: refine le_antisymm (Order.coheight_le_coheight_apply_of_strictMono _ hf _) ?_
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α) (b : β), f a < b → ∃ (a' : α), a < a' ∧ f a' = b
a : α
⊢ coheight (f a) ≤ coheight a
have refine : ∀ (p : LTSeries β)
  (hp :
    RelSeries.head (r :=
        {x : β × β |
          match (motive := β × β → Prop) x with
          | (a, b) => a < b})
        p =
      f a),
  (↑(p.length (r :=
          {x : β × β |
            match (motive := β × β → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    coheight a
Tactic: refine coheight_le_iff'.mpr fun p hp ↦ ?_
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α) (b : β), f a < b → ∃ (a' : α), a < a' ∧ f a' = b
p :
  RelSeries (α := β)
    {x : β × β |
      match (motive := β × β → Prop) x with
      | (a, b) => a < b}
x : β
hx :
  Membership.mem (γ := SetRel β β)
    {x : β × β |
      match (motive := β × β → Prop) x with
      | (a, b) => a < b}
    (x,
      p.head (r :=
        {x : β × β |
          match (motive := β × β → Prop) x with
          | (a, b) => a < b}))
ih :
  ∀ (a : α)
    (hp :
      p.head (r :=
          {x : β × β |
            match (motive := β × β → Prop) x with
            | (a, b) => a < b}) =
        f a),
    (↑(p.length (r :=
            {x : β × β |
              match (motive := β × β → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞) ≤
      coheight a
a : α
hp : x = f a
⊢ (↑((p.cons (r :=
              {x : β × β |
                match (motive := β × β → Prop) x with
                | (a, b) => a < b})
              x hx).length
          (r :=
          {x : β × β |
            match (motive := β × β → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    coheight a
have cons : ∀ (a' : α) (haa' : a < a')
  (ha' :
    f a' =
      p.head (r :=
        {x : β × β |
          match (motive := β × β → Prop) x with
          | (a, b) => a < b})),
  (↑((p.cons (r :=
              {x : β × β |
                match (motive := β × β → Prop) x with
                | (a, b) => a < b})
              x hx).length
          (r :=
          {x : β × β |
            match (motive := β × β → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    coheight a
Tactic: obtain ⟨a', haa', ha'⟩ := h a p.head (by grind)
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α) (b : β), f a < b → ∃ (a' : α), a < a' ∧ f a' = b
p :
  RelSeries (α := β)
    {x : β × β |
      match (motive := β × β → Prop) x with
      | (a, b) => a < b}
x : β
hx :
  Membership.mem (γ := SetRel β β)
    {x : β × β |
      match (motive := β × β → Prop) x with
      | (a, b) => a < b}
    (x,
      p.head (r :=
        {x : β × β |
          match (motive := β × β → Prop) x with
          | (a, b) => a < b}))
ih :
  ∀ (a : α)
    (hp :
      p.head (r :=
          {x : β × β |
            match (motive := β × β → Prop) x with
            | (a, b) => a < b}) =
        f a),
    (↑(p.length (r :=
            {x : β × β |
              match (motive := β × β → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞) ≤
      coheight a
a : α
hp : x = f a
a' : α
haa' : a < a'
ha' :
  f a' =
    p.head (r :=
      {x : β × β |
        match (motive := β × β → Prop) x with
        | (a, b) => a < b})
⊢ (↑((p.cons (r :=
              {x : β × β |
                match (motive := β × β → Prop) x with
                | (a, b) => a < b})
              x hx).length
          (r :=
          {x : β × β |
            match (motive := β × β → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    coheight a
have cons : coheight a' + 1 ≤ coheight a
Tactic: grw [RelSeries.cons_length, Nat.cast_add, Nat.cast_one, ih a' ha'.symm]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α) (b : β), f a < b → ∃ (a' : α), a < a' ∧ f a' = b
a : α
p : LTSeries β
hp :
  RelSeries.head (r :=
      {x : β × β |
        match (motive := β × β → Prop) x with
        | (a, b) => a < b})
      p =
    f a
⊢ (↑(p.length (r :=
          {x : β × β |
            match (motive := β × β → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    coheight a
have singleton : ∀ (x : β) (a : α)
  (hp :
    RelSeries.head (r :=
        {x : β × β |
          match (motive := β × β → Prop) x with
          | (a, b) => a < b})
        (RelSeries.singleton
          {x : β × β |
            match (motive := β × β → Prop) x with
            | (a, b) => a < b}
          x) =
      f a),
  (↑(RelSeries.length (r :=
          {x : β × β |
            match (motive := β × β → Prop) x with
            | (a, b) => a < b})
          (RelSeries.singleton
            {x : β × β |
              match (motive := β × β → Prop) x with
              | (a, b) => a < b}
            x)) :
      ℕ∞) ≤
    coheight a
Tactic: induction p using RelSeries.inductionOn generalizing a with
  | singleton x => simp
  | cons p x hx ih =>
    simp only [RelSeries.head_cons] at hp
    obtain ⟨a', haa', ha'⟩ := h a p.head (by grind)
    grw [RelSeries.cons_length, Nat.cast_add, Nat.cast_one, ih a' ha'.symm]
    exact coheight_add_one_le haa'
Cleared hypotheses: a, p, hp
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α) (b : β), f a < b → ∃ (a' : α), a < a' ∧ f a' = b
a : α
p : LTSeries β
hp :
  RelSeries.head (r :=
      {x : β × β |
        match (motive := β × β → Prop) x with
        | (a, b) => a < b})
      p =
    f a
singleton :
  ∀ (x : β) (a : α)
    (hp :
      RelSeries.head (r :=
          {x : β × β |
            match (motive := β × β → Prop) x with
            | (a, b) => a < b})
          (RelSeries.singleton
            {x : β × β |
              match (motive := β × β → Prop) x with
              | (a, b) => a < b}
            x) =
        f a),
    (↑(RelSeries.length (r :=
            {x : β × β |
              match (motive := β × β → Prop) x with
              | (a, b) => a < b})
            (RelSeries.singleton
              {x : β × β |
                match (motive := β × β → Prop) x with
                | (a, b) => a < b}
              x)) :
        ℕ∞) ≤
      coheight a
⊢ (↑(p.length (r :=
          {x : β × β |
            match (motive := β × β → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    coheight a
have cons : ∀
  (p :
    RelSeries (α := β)
      {x : β × β |
        match (motive := β × β → Prop) x with
        | (a, b) => a < b})
  (x : β)
  (hx :
    Membership.mem (γ := SetRel β β)
      {x : β × β |
        match (motive := β × β → Prop) x with
        | (a, b) => a < b}
      (x,
        p.head (r :=
          {x : β × β |
            match (motive := β × β → Prop) x with
            | (a, b) => a < b})))
  (ih :
    ∀ (a : α)
      (hp :
        p.head (r :=
            {x : β × β |
              match (motive := β × β → Prop) x with
              | (a, b) => a < b}) =
          f a),
      (↑(p.length (r :=
              {x : β × β |
                match (motive := β × β → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
        coheight a)
  (a : α)
  (hp :
    (p.cons (r :=
            {x : β × β |
              match (motive := β × β → Prop) x with
              | (a, b) => a < b})
            x hx).head
        (r :=
        {x : β × β |
          match (motive := β × β → Prop) x with
          | (a, b) => a < b}) =
      f a),
  (↑((p.cons (r :=
              {x : β × β |
                match (motive := β × β → Prop) x with
                | (a, b) => a < b})
              x hx).length
          (r :=
          {x : β × β |
            match (motive := β × β → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    coheight a
Tactic: induction p using RelSeries.inductionOn generalizing a with
  | singleton x => simp
  | cons p x hx ih =>
    simp only [RelSeries.head_cons] at hp
    obtain ⟨a', haa', ha'⟩ := h a p.head (by grind)
    grw [RelSeries.cons_length, Nat.cast_add, Nat.cast_one, ih a' ha'.symm]
    exact coheight_add_one_le haa'
Cleared hypotheses: a, p, hp
-- Lean 4 proof step from Mathlib.Order.KrullDimension (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α), ∀ b < f a, ∃ a' < a, f a' = b
a : α
⊢ height a = height (f a)
have this : coheight (α := αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) =
  coheight (α := βᵒᵈ) ((OrderDual.toDual : (a : β) → βᵒᵈ) (f a) : βᵒᵈ)
Tactic: have : coheight (OrderDual.toDual a) = coheight (OrderDual.toDual (f a)) :=
    coheight_eq_of_strictMono (α := αᵒᵈ) (β := βᵒᵈ) (f := OrderDual.toDual ∘ f ∘ OrderDual.toDual)
    (strictMono_dual_iff.mp hf) (fun a b hab ↦ h a b hab) _
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
x : α
⊢ height.{u_2} (α := β) ((f : (a : α) → β) x : β) = height x
have a : height.{u_2} (α := β) ((f : (a : α) → β) x : β) ≤ height x
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
x : α
a : height.{u_2} (α := β) ((f : (a : α) → β) x : β) ≤ height x
⊢ height.{u_2} (α := β) ((f : (a : α) → β) x : β) = height x
have a₁ : height x ≤ height.{u_2} (α := β) ((f : (a : α) → β) x : β)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_3
inst : Nonempty α
f : α → ℕ∞
n : ℕ
h : Eq (α := ℕ∞) (⨆ (x : α), f x) (↑n : ℕ∞)
⊢ ∃ (x : α), f x = (↑n : ℕ∞)
have obtain : ∀ (x : α) (hx : Eq (α := ℕ∞) ((fun (x : α) ↦ f x) x) (sSup (Set.range fun (x : α) ↦ f x))), ∃ (x : α), f x = (↑n : ℕ∞)
Tactic: obtain ⟨x, hx⟩ := ENat.sSup_mem_of_nonempty_of_lt_top (h ▸ ENat.coe_lt_top _)