awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ ∀
    (x :
      RelSeries (α := αᵒᵈ)
        {x : αᵒᵈ × αᵒᵈ |
          match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
          | (a, b) => a < b}),
    Eq (α := ℕ∞)
      (⨆ (_ :
        a ≤
          RelSeries.head (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            (({
                  toFun :=
                    RelSeries.reverse (r :=
                      {x : αᵒᵈ × αᵒᵈ |
                        match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
                        | (a, b) => a < b}),
                  invFun :=
                    RelSeries.reverse (r :=
                      SetRel.inv
                        {x : αᵒᵈ × αᵒᵈ |
                          match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
                          | (a, b) => a < b}),
                  left_inv := ⋯, right_inv := ⋯ } :
                (a :
                    RelSeries
                      {x : αᵒᵈ × αᵒᵈ |
                        match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
                        | (a, b) => a < b}) →
                  RelSeries
                    (SetRel.inv
                      {x : αᵒᵈ × αᵒᵈ |
                        match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
                        | (a, b) => a < b}))
              x)),
        (↑(RelSeries.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              (({
                    toFun :=
                      RelSeries.reverse (r :=
                        {x : αᵒᵈ × αᵒᵈ |
                          match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
                          | (a, b) => a < b}),
                    invFun :=
                      RelSeries.reverse (r :=
                        SetRel.inv
                          {x : αᵒᵈ × αᵒᵈ |
                            match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
                            | (a, b) => a < b}),
                    left_inv := ⋯, right_inv := ⋯ } :
                  (a :
                      RelSeries
                        {x : αᵒᵈ × αᵒᵈ |
                          match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
                          | (a, b) => a < b}) →
                    RelSeries
                      (SetRel.inv
                        {x : αᵒᵈ × αᵒᵈ |
                          match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
                          | (a, b) => a < b}))
                x)) :
          ℕ∞))
      (⨆ (_ :
        x.last (r :=
            {x : αᵒᵈ × αᵒᵈ |
              match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
              | (a, b) => a < b}) ≤
          a),
        (↑(x.length (r :=
              {x : αᵒᵈ × αᵒᵈ |
                match (motive := αᵒᵈ × αᵒᵈ → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞))

Tactic:
congr! 1
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
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₁ rw₂ :
  (∀ (i : LTSeries α)
      (j :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            i ≤
          a),
      (↑(i.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

Tactic:
rw [height, iSup₂_le_iff]

Premises used: iSup₂_le_iff, Order.height
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
rw :
  ⨆ (p : LTSeries α),
        ⨆ (_ :
          a ≤
            RelSeries.head (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})) :
            ℕ∞) ≤
      n ↔
    ∀ ⦃p : LTSeries α⦄,
      a ≤
          RelSeries.head (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})) :
            ℕ∞) ≤
          n
rw₁ rw₂ :
  (∀ (i : LTSeries α)
      (j :
        a ≤
          RelSeries.head (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            i),
      (↑(i.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
        n) ↔
    ∀ ⦃p : LTSeries α⦄,
      a ≤
          RelSeries.head (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})) :
            ℕ∞) ≤
          n
⊢ coheight a ≤ n ↔
    ∀ ⦃p : LTSeries α⦄,
      a ≤
          RelSeries.head (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})) :
            ℕ∞) ≤
          n

Tactic:
rw [coheight_eq, iSup₂_le_iff]

Premises used: iSup₂_le_iff, Order.coheight_eq
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
h :
  ∀ (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
apply :
  ∀ ⦃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

Tactic:
apply height_le_iff.mpr

Premises used: Iff.mpr, Order.height_le_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
h :
  ∀ (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 α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    a
this :
  ∀ {α : Type u_1} [inst : Preorder α] {a : α} {n : ℕ∞}
    (h :
      ∀ (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 α⦄
    (hlast :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p ≤
        a)
    (hlenpos :
      p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) ≠
        0),
    (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞) ≤
      n
hlenpos :
  ¬p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) ≠
      0
⊢ (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    n

Tactic:
simp_all
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
a : α
n : ℕ∞
h :
  ∀ (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 α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    a
hlenpos :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
⊢ p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0

Tactic:
simp_all
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
a : α
n : ℕ∞
h :
  ∀ (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 α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    a
hlenpos :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
p' : RelSeries (α := α)
  {x : α × α |
    match (motive := α × α → Prop) x with
    | (a, b) => a < b} :=
  (RelSeries.eraseLast (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p).snoc
    (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    a ⋯
simp : p.length (r := {x : α × α | x.1 < x.2}) = p.length (r := {x : α × α | x.1 < x.2}) - 1 + 1
⊢ p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    p'.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})

Tactic:
simp [p']
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
a : α
n : ℕ∞
h :
  ∀ (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 α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    a
hlenpos :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
p' : RelSeries (α := α)
  {x : α × α |
    match (motive := α × α → Prop) x with
    | (a, b) => a < b} :=
  (RelSeries.eraseLast (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p).snoc
    (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    a ⋯
⊢ p.length (r := {x : α × α | x.1 < x.2}) = p.length (r := {x : α × α | x.1 < x.2}) - 1 + 1

Tactic:
lia
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
a : α
n : ℕ∞
h :
  ∀ (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 α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    a
hlenpos :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
p' : RelSeries (α := α)
  {x : α × α |
    match (motive := α × α → Prop) x with
    | (a, b) => a < b} :=
  (RelSeries.eraseLast (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p).snoc
    (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    a ⋯
rw :
  (↑(p'.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    n
⊢ (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    n

Tactic:
rw [show p.length = p'.length by simp [p']; lia]
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
a : α
n : ℕ∞
h :
  ∀ (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 α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    a
hlenpos :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
p' : RelSeries (α := α)
  {x : α × α |
    match (motive := α × α → Prop) x with
    | (a, b) => a < b} :=
  (RelSeries.eraseLast (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p).snoc
    (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    a ⋯
a₁ :
  p'.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    a
⊢ (↑(p'.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    n

Tactic:
apply h
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
a : α
n : ℕ∞
h :
  ∀ (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 α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    a
hlenpos :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0
p' : RelSeries (α := α)
  {x : α × α |
    match (motive := α × α → Prop) x with
    | (a, b) => a < b} :=
  (RelSeries.eraseLast (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p).snoc
    (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    a ⋯
⊢ p'.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    a

Tactic:
simp [p']
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
mp :
  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
mpr :
  (∀ ⦃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
⊢ 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

Tactic:
constructor
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
mp :
  (∀ ⦃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

Tactic:
rw [height_le_iff]

Premises used: Order.height_le_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
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) →
    ∀ ⦃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:
fun h p hlast => h (le_of_eq hlast)

Premises used: le_of_eq
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
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) →
    ∀ ⦃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:
exact fun h p hlast => h (le_of_eq hlast)
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
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) →
    height a ≤ n

Tactic:
height_le

Premises used: Order.height_le
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
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) →
    height a ≤ n

Tactic:
exact height_le

Premises used: Order.height_le
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
H :
  ∀ (c : ℕ∞),
    height a ≤ c ↔
      ⨆ (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})) :
              ℕ∞) ≤
        c
⊢ height a =
    ⨆ (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})) :
          ℕ∞)

Tactic:
apply eq_of_forall_ge_iff

Premises used: eq_of_forall_ge_iff