awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : a < b
cases : ∀ (x : ℕ∞) (hfin : height a = x), x + 1 ≤ height b
⊢ height a + 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]

Premises used: Order.height, Order.add_one_le_of_lt
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x y : α
hyx : y < x
hfin : coheight x < ⊤
⊢ coheight x < coheight y

Tactic:
height_strictMono (α := αᵒᵈ) hyx hfin

Premises used: Order.height_strictMono, Order.coheight
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : b < a
hfin : coheight a = ⊤
rw : coheight a ≤ coheight b
⊢ ⊤ ≤ coheight b

Tactic:
rw [← hfin]
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : b < a
hfin : coheight a = ⊤
⊢ coheight a ≤ coheight b

Tactic:
gcongr
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : b < a
hfin : coheight a = ⊤
⊢ ⊤ ≤ coheight b

Tactic:
have : ⊤ ≤ coheight b := by
      rw [← hfin]
      gcongr
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : b < a
hfin : coheight a = ⊤
this : ⊤ ≤ coheight b
⊢ HAdd.hAdd (α := ℕ∞) ⊤ 1 ≤ coheight b

Tactic:
simp [this]
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : b < a
n : ℕ
hfin : coheight a = (↑n : ℕ∞)
coe : (↑n : ℕ∞) < coheight b
⊢ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ coheight b

Tactic:
apply Order.add_one_le_of_lt

Premises used: Order.add_one_le_of_lt
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : b < a
n : ℕ
hfin : coheight a = (↑n : ℕ∞)
coe : coheight a < coheight b
⊢ (↑n : ℕ∞) < coheight b

Tactic:
rw [← hfin]
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : b < a
n : ℕ
hfin : coheight a = (↑n : ℕ∞)
coe : coheight a < ⊤
⊢ coheight a < coheight b

Tactic:
gcongr
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : b < a
n : ℕ
hfin : coheight a = (↑n : ℕ∞)
⊢ coheight a < ⊤

Tactic:
simp [hfin]
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : b < a
cases : ∀ (x : ℕ∞) (hfin : coheight a = x), x + 1 ≤ coheight b
⊢ coheight a + 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]

Premises used: Order.add_one_le_of_lt, Order.coheight
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
x : α
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})) : ℕ∞))
⊢ height x ≤ height (f x)

Tactic:
simp only [height_eq_iSup_last_eq]

Premises used: Order.height_eq_iSup_last_eq
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
x : α
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})) : ℕ∞))
⊢ 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:
apply iSup₂_le

Premises used: iSup₂_le
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
x : α
p : LTSeries α
hlast : RelSeries.last (r := {x : α × α | x.1 < x.2}) p = x
⊢ RelSeries.last (r := {x : β × β | x.1 < x.2}) (p.map f hf) = f x

Tactic:
simp [hlast]
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
x : α
p : LTSeries α
hlast : RelSeries.last (r := {x : α × α | x.1 < x.2}) p = x
⊢ LE.le (α := ℕ∞) (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞)
    (↑((p.map f hf).length (r := {x : β × β | x.1 < x.2})) : ℕ∞)

Tactic:
simp
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
x : α
p : LTSeries α
hlast : RelSeries.last (r := {x : α × α | x.1 < x.2}) p = x
⊢ LE.le (α := ℕ∞) (↑(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:
apply le_iSup₂_of_le (p.map f hf) (by simp [hlast]) (by simp)

Premises used: LTSeries.map, le_iSup₂_of_le
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
x : α
hf₁ : StrictMono f
⊢ coheight x ≤ coheight (f x)

Tactic:
apply height_le_height_apply_of_strictMono (α := αᵒᵈ)

Premises used: Order.height_le_height_apply_of_strictMono
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
x : α
⊢ StrictMono f

Tactic:
fun _ _ h ↦ hf h

Premises used: StrictMono
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
x : α
⊢ StrictMono f

Tactic:
exact fun _ _ h ↦ hf h
-- Module: Mathlib.Order.KrullDimension
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)

Tactic:
le_antisymm (Order.coheight_le_coheight_apply_of_strictMono _ hf _) ?_

Premises used: le_antisymm, Order.coheight_le_coheight_apply_of_strictMono
-- Module: Mathlib.Order.KrullDimension
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 : α
refine : coheight (f a) ≤ coheight a
⊢ coheight a = coheight (f a)

Tactic:
refine le_antisymm (Order.coheight_le_coheight_apply_of_strictMono _ hf _) ?_

Premises used: le_antisymm, Order.coheight_le_coheight_apply_of_strictMono
-- Module: Mathlib.Order.KrullDimension
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

Tactic:
coheight_le_iff'.mpr fun p hp ↦ ?_

Premises used: Iff.mpr, Order.coheight_le_iff'
-- Module: Mathlib.Order.KrullDimension
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 : α
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
⊢ coheight (f a) ≤ coheight a

Tactic:
refine coheight_le_iff'.mpr fun p hp ↦ ?_

Premises used: Iff.mpr, Order.coheight_le_iff'
-- Module: Mathlib.Order.KrullDimension
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
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:
simp
-- Module: Mathlib.Order.KrullDimension
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
⊢ f a <
    p.head (r :=
      {x : β × β |
        match (motive := β × β → Prop) x with
        | (a, b) => a < b})

Tactic:
grind
-- Module: Mathlib.Order.KrullDimension
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
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
⊢ (↑((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)

Premises used: RelSeries.head
-- Module: Mathlib.Order.KrullDimension
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})
cons : coheight a' + 1 ≤ coheight 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:
grw [RelSeries.cons_length, Nat.cast_add, Nat.cast_one, ih a' ha'.symm]

Premises used: Nat.cast_add, RelSeries.cons_length, Eq.symm, Nat.cast_one
-- Module: Mathlib.Order.KrullDimension
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})
⊢ coheight a' + 1 ≤ coheight a

Tactic:
coheight_add_one_le haa'

Premises used: Order.coheight_add_one_le
-- Module: Mathlib.Order.KrullDimension
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})
⊢ coheight a' + 1 ≤ coheight a

Tactic:
exact coheight_add_one_le haa'

Premises used: Order.coheight_add_one_le
-- Module: Mathlib.Order.KrullDimension
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
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
⊢ (↑(p.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'

Premises used: RelSeries.head_cons, Nat.cast_add, RelSeries.cons_length, RelSeries.head, Singleton.singleton, Nat.cast_one
-- Module: Mathlib.Order.KrullDimension
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 : α
⊢ 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) _
-- Module: Mathlib.Order.KrullDimension
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 : α
this :
  coheight (α := αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) =
    coheight (α := βᵒᵈ) ((OrderDual.toDual : (a : β) → βᵒᵈ) (f a) : βᵒᵈ)
⊢ height a = height (f a)

Tactic:
simpa [Order.coheight_toDual] using this

Premises used: Order.coheight_toDual
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
x : α
a : height.{u_2} (α := β) ((f : (a : α) → β) x : β) ≤ height x
a₁ : height x ≤ height.{u_2} (α := β) ((f : (a : α) → β) x : β)
⊢ height.{u_2} (α := β) ((f : (a : α) → β) x : β) = height x

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
x : α
⊢ height.{u_2} (α := β) ((f : (a : α) → β) x : β) ≤ height x

Tactic:
simpa using height_le_height_apply_of_strictMono _ f.symm.strictMono (f x)

Premises used: OrderIso.strictMono, OrderIso.symm, Order.height_le_height_apply_of_strictMono, DFunLike.coe
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
x : α
⊢ height x ≤ height.{u_2} (α := β) ((f : (a : α) → β) x : β)

Tactic:
height_le_height_apply_of_strictMono _ f.strictMono x

Premises used: OrderIso.strictMono, Order.height_le_height_apply_of_strictMono
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
x : α
⊢ height x ≤ height.{u_2} (α := β) ((f : (a : α) → β) x : β)

Tactic:
exact height_le_height_apply_of_strictMono _ f.strictMono x

Premises used: OrderIso.strictMono, Order.height_le_height_apply_of_strictMono
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
x : α
⊢ coheight.{u_2} (α := β) ((f : (a : α) → β) x : β) = coheight x

Tactic:
height_orderIso (α := αᵒᵈ) f.dual x

Premises used: Order.height_orderIso, OrderIso.dual, Order.coheight
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_3
inst : Nonempty α
f : α → ℕ∞
n : ℕ
h : Eq (α := ℕ∞) (⨆ (x : α), f x) (↑n : ℕ∞)
obtain :
  ∀ (x : α) (hx : Eq (α := ℕ∞) ((fun (x : α) ↦ f x) x) (sSup (Set.range fun (x : α) ↦ f x))), ∃ (x : α), f x = (↑n : ℕ∞)
⊢ ∃ (x : α), f x = (↑n : ℕ∞)

Tactic:
obtain ⟨x, hx⟩ := ENat.sSup_mem_of_nonempty_of_lt_top (h ▸ ENat.coe_lt_top _)

Premises used: ENat.sSup_mem_of_nonempty_of_lt_top
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_3
inst : Nonempty α
f : α → ℕ∞
n : ℕ
h : Eq (α := ℕ∞) (⨆ (x : α), f x) (↑n : ℕ∞)
x : α
hx : Eq (α := ℕ∞) ((fun (x : α) ↦ f x) x) (sSup (Set.range fun (x : α) ↦ f x))
h₁ : f x = (↑n : ℕ∞)
⊢ ∃ (x : α), f x = (↑n : ℕ∞)

Tactic:
use x
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_3
inst : Nonempty α
f : α → ℕ∞
n : ℕ
h : Eq (α := ℕ∞) (⨆ (x : α), f x) (↑n : ℕ∞)
x : α
hx : Eq (α := ℕ∞) ((fun (x : α) ↦ f x) x) (sSup (Set.range fun (x : α) ↦ f x))
⊢ f x = (↑n : ℕ∞)

Tactic:
simpa [hx] using h
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
h : (↑n : ℕ∞) ≤ height a
⊢ Nonempty.{max 1 (u_1 + 1)}
    { p : LTSeries α //
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a }

Tactic:
have hne : Nonempty { p : LTSeries α // p.last = a } := ⟨RelSeries.singleton _ a, rfl⟩
-- Module: Mathlib.Order.KrullDimension
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 }
ha : height a = ⊤
⊢ ¬∃ (x : ℕ),
      ∀ (y : ℕ),
        Membership.mem (γ := Set ℕ)
            (Set.range
              fun
                (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}))
            y →
          y ≤ x

Tactic:
rw [height_eq_iSup_last_eq, iSup_subtype', ENat.iSup_coe_eq_top, bddAbove_def] at ha

Premises used: iSup_subtype', ENat.iSup_coe_eq_top, bddAbove_def, Order.height_eq_iSup_last_eq