awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ (x : α) (h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = (↑m_1 : ℕ∞)),
      height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑m_1 : ℕ∞) + (↑m : ℕ∞)
x : α
h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = (↑n : ℕ∞)
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
h_len :
  HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑n : ℕ∞) + (↑m : ℕ∞) <
    (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)
i : Fin
  (p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) +
    1) :=
  ⟨p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) -
      (m + 1),
    ⋯⟩
⊢ LT.lt.{u_2} (α := β)
    ((f : (a : α) → β)
        (p.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          i) :
      β)
    ((f : (a : α) → β) x : β)

Tactic:
(f.monotone ((p.monotone (Fin.le_last _)).trans hp)).lt_of_not_ge fun h'' ↦ ?_

Premises used: LE.le.lt_of_not_ge, OrderHom.monotone, LE.le.trans, LTSeries.monotone, Fin.le_last
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ (x : α) (h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = (↑m_1 : ℕ∞)),
      height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑m_1 : ℕ∞) + (↑m : ℕ∞)
x : α
h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = (↑n : ℕ∞)
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
h_len :
  HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑n : ℕ∞) + (↑m : ℕ∞) <
    (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)
i : Fin
  (p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) +
    1) :=
  ⟨p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) -
      (m + 1),
    ⋯⟩
coe :
  ∀
    (h'' :
      LE.le.{u_2} (α := β) ((f : (a : α) → β) x : β)
        ((f : (a : α) → β)
            (p.toFun (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              i) :
          β)),
    False
⊢ LT.lt.{u_2} (α := β)
    ((f : (a : α) → β)
        (p.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          i) :
      β)
    ((f : (a : α) → β) x : β)

Tactic:
refine (f.monotone ((p.monotone (Fin.le_last _)).trans hp)).lt_of_not_ge fun h'' ↦ ?_

Premises used: LE.le.lt_of_not_ge, OrderHom.monotone, LE.le.trans, LTSeries.monotone, Fin.le_last
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ (x : α) (h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = (↑m_1 : ℕ∞)),
      height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑m_1 : ℕ∞) + (↑m : ℕ∞)
x : α
h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = (↑n : ℕ∞)
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
h_len :
  HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑n : ℕ∞) + (↑m : ℕ∞) <
    (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)
i : Fin
  (p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) +
    1) :=
  ⟨p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) -
      (m + 1),
    ⋯⟩
h'' :
  LE.le.{u_2} (α := β) ((f : (a : α) → β) x : β)
    ((f : (a : α) → β)
        (p.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          i) :
      β)
q' : LTSeries α :=
  RelSeries.drop (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    p i
q : LTSeries (↑(Set.preimage (β := β) (⇑f : (a : α) → β) (singleton (α := β) ((f : (a : α) → β) x : β))) : Type u_1) :=
  RelSeries.mk (r :=
    {x_1 :
      (↑(Set.preimage (β := β) (⇑f : (a : α) → β) (singleton (α := β) ((f : (a : α) → β) x : β))) : Type u_1) ×
        (↑(Set.preimage (β := β) (⇑f : (a : α) → β) (singleton (α := β) ((f : (a : α) → β) x : β))) : Type u_1) |
      match (motive :=
        (↑(Set.preimage (β := β) (⇑f : (a : α) → β) (singleton (α := β) ((f : (a : α) → β) x : β))) : Type u_1) ×
            (↑(Set.preimage (β := β) (⇑f : (a : α) → β) (singleton (α := β) ((f : (a : α) → β) x : β))) : Type u_1) →
          Prop)
        x_1 with
      | (a, b) => a < b})
    (q'.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}))
    (fun
        (j :
          Fin
            (q'.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b}) +
              1)) ↦
      Subtype.mk (p := fun (x_1 : α) ↦
        Membership.mem (γ := Set α)
          (Set.preimage (β := β) (⇑f : (a : α) → β) (singleton (α := β) ((f : (a : α) → β) x : β))) x_1)
        (q'.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          j)
        ⋯)
    ⋯
this : p.length (r := {x : α × α | x.1 < x.2}) ≤ m + (p.length (r := {x : α × α | x.1 < x.2}) - (m + 1))
⊢ p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) >
    m

Tactic:
have : p.length > m := ENat.coe_lt_coe.mp ((le_add_left le_rfl).trans_lt h_len)
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ (x : α) (h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = (↑m_1 : ℕ∞)),
      height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑m_1 : ℕ∞) + (↑m : ℕ∞)
x : α
h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = (↑n : ℕ∞)
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
h_len :
  HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑n : ℕ∞) + (↑m : ℕ∞) <
    (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)
i : Fin
  (p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) +
    1) :=
  ⟨p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) -
      (m + 1),
    ⋯⟩
h'' :
  LE.le.{u_2} (α := β) ((f : (a : α) → β) x : β)
    ((f : (a : α) → β)
        (p.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          i) :
      β)
q' : LTSeries α :=
  RelSeries.drop (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    p i
q : LTSeries (↑(Set.preimage (β := β) (⇑f : (a : α) → β) (singleton (α := β) ((f : (a : α) → β) x : β))) : Type u_1) :=
  RelSeries.mk (r :=
    {x_1 :
      (↑(Set.preimage (β := β) (⇑f : (a : α) → β) (singleton (α := β) ((f : (a : α) → β) x : β))) : Type u_1) ×
        (↑(Set.preimage (β := β) (⇑f : (a : α) → β) (singleton (α := β) ((f : (a : α) → β) x : β))) : Type u_1) |
      match (motive :=
        (↑(Set.preimage (β := β) (⇑f : (a : α) → β) (singleton (α := β) ((f : (a : α) → β) x : β))) : Type u_1) ×
            (↑(Set.preimage (β := β) (⇑f : (a : α) → β) (singleton (α := β) ((f : (a : α) → β) x : β))) : Type u_1) →
          Prop)
        x_1 with
      | (a, b) => a < b})
    (q'.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}))
    (fun
        (j :
          Fin
            (q'.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b}) +
              1)) ↦
      Subtype.mk (p := fun (x_1 : α) ↦
        Membership.mem (γ := Set α)
          (Set.preimage (β := β) (⇑f : (a : α) → β) (singleton (α := β) ((f : (a : α) → β) x : β))) x_1)
        (q'.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          j)
        ⋯)
    ⋯
this_1 : p.length (r := {x : α × α | x.1 < x.2}) ≤ m + (p.length (r := {x : α × α | x.1 < x.2}) - (m + 1))
this :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) >
    m
⊢ False

Tactic:
lia
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
x : α
n : ℕ
h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = (↑n : ℕ∞)
coe :
  ∀ (n : ℕ)
    (ih :
      ∀ m_1 < n,
        ∀ (x : α) (h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = (↑m_1 : ℕ∞)),
          height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑m_1 : ℕ∞) + (↑m : ℕ∞))
    (x : α) (h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = (↑n : ℕ∞)),
    height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑n : ℕ∞) + (↑m : ℕ∞)
⊢ height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑n : ℕ∞) + (↑m : ℕ∞)

Tactic:
induction n using Nat.strong_induction_on generalizing x with | h n ih =>
    refine height_le_iff.mpr fun p hp ↦ le_of_not_gt fun h_len ↦ ?_
    let i : Fin (p.length + 1) := ⟨p.length - (m + 1), Nat.sub_lt_succ p.length _⟩
    suffices h'' : f (p i) < f x by
      obtain ⟨n', hn'⟩ : ∃ (n' : ℕ), n' = height (f (p i)) := ENat.ne_top_iff_exists.mp
        ((height_mono h''.le).trans_lt (h' ▸ ENat.coe_lt_top _)).ne
      have h_lt : n' < n := ENat.coe_lt_coe.mp
        (h' ▸ hn' ▸ height_strictMono h'' (hn' ▸ ENat.coe_lt_top _))
      have := (length_le_height_last (p := p.take i)).trans <| ih n' h_lt (p i) hn'.symm
      rw [RelSeries.take_length, ENat.coe_sub, Nat.cast_add, Nat.cast_one, tsub_le_iff_right,
        add_assoc, add_comm _ (_ + 1), ← add_assoc, ← mul_add_one] at this
      refine not_lt_of_ge ?_ (h_len.trans_le this)
      gcongr
      rwa [← ENat.coe_one, ← ENat.coe_add, ENat.coe_le_coe]
    refine (f.monotone ((p.monotone (Fin.le_last _)).trans hp)).lt_of_not_ge fun h'' ↦ ?_
    let q' : LTSeries α := p.drop i
    let q : LTSeries (f ⁻¹' {f x}) := ⟨q'.length, fun j ↦ ⟨q' j, le_antisymm
      (f.monotone (le_trans (b := q'.last) (q'.monotone (Fin.le_last _)) (p.last_drop _ ▸ hp)))
      (le_trans (b := f q'.head) (p.head_drop _ ▸ h'')
        (f.monotone (q'.monotone (Fin.zero_le _))))⟩, fun i ↦ q'.step i⟩
    have := (LTSeries.length_le_krullDim q).trans (h (f x))
    simp only [RelSeries.drop_length, Nat.cast_le, tsub_le_iff_right, q', i, q] at this
    have : p.length > m := ENat.coe_lt_coe.mp ((le_add_left le_rfl).trans_lt h_len)
    lia

Premises used: Iff.mpr, le_of_not_gt, tsub_le_iff_right, Order.height_le_iff, Nat.cast_le, RelSeries.drop_length
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
x : α
n : ℕ∞
h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = n
top :
  ∀ (h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = ⊤),
    height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * ⊤ + (↑m : ℕ∞)
coe :
  ∀ (n : ℕ) (h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = (↑n : ℕ∞)),
    height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑n : ℕ∞) + (↑m : ℕ∞)
⊢ height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * n + (↑m : ℕ∞)

Tactic:
cases n with | top => simp | coe n =>
    induction n using Nat.strong_induction_on generalizing x with | h n ih =>
    refine height_le_iff.mpr fun p hp ↦ le_of_not_gt fun h_len ↦ ?_
    let i : Fin (p.length + 1) := ⟨p.length - (m + 1), Nat.sub_lt_succ p.length _⟩
    suffices h'' : f (p i) < f x by
      obtain ⟨n', hn'⟩ : ∃ (n' : ℕ), n' = height (f (p i)) := ENat.ne_top_iff_exists.mp
        ((height_mono h''.le).trans_lt (h' ▸ ENat.coe_lt_top _)).ne
      have h_lt : n' < n := ENat.coe_lt_coe.mp
        (h' ▸ hn' ▸ height_strictMono h'' (hn' ▸ ENat.coe_lt_top _))
      have := (length_le_height_last (p := p.take i)).trans <| ih n' h_lt (p i) hn'.symm
      rw [RelSeries.take_length, ENat.coe_sub, Nat.cast_add, Nat.cast_one, tsub_le_iff_right,
        add_assoc, add_comm _ (_ + 1), ← add_assoc, ← mul_add_one] at this
      refine not_lt_of_ge ?_ (h_len.trans_le this)
      gcongr
      rwa [← ENat.coe_one, ← ENat.coe_add, ENat.coe_le_coe]
    refine (f.monotone ((p.monotone (Fin.le_last _)).trans hp)).lt_of_not_ge fun h'' ↦ ?_
    let q' : LTSeries α := p.drop i
    let q : LTSeries (f ⁻¹' {f x}) := ⟨q'.length, fun j ↦ ⟨q' j, le_antisymm
      (f.monotone (le_trans (b := q'.last) (q'.monotone (Fin.le_last _)) (p.last_drop _ ▸ hp)))
      (le_trans (b := f q'.head) (p.head_drop _ ▸ h'')
        (f.monotone (q'.monotone (Fin.zero_le _))))⟩, fun i ↦ q'.step i⟩
    have := (LTSeries.length_le_krullDim q).trans (h (f x))
    simp only [RelSeries.drop_length, Nat.cast_le, tsub_le_iff_right, q', i, q] at this
    have : p.length > m := ENat.coe_lt_coe.mp ((le_add_left le_rfl).trans_lt h_len)
    lia

Premises used: Iff.mpr, le_of_not_gt, tsub_le_iff_right, Order.height_le_iff, Nat.cast_le, RelSeries.drop_length
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
x : α
h₁ :
  ∀ (x : βᵒᵈ),
    krullDim.{u_1}
        (↑(Set.preimage (β := βᵒᵈ)
              (⇑((OrderHom.dual : (a : α →o β) → αᵒᵈ →o βᵒᵈ) f : OrderHom.{u_1, u_2} αᵒᵈ βᵒᵈ) : (a : αᵒᵈ) → βᵒᵈ) {x}) :
          Type u_1) ≤
      (↑m : WithBot ℕ∞)
⊢ height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * height.{u_2} (α := βᵒᵈ) ((f : (a : α) → β) x : β) + (↑m : ℕ∞)

Tactic:
apply height_le_of_krullDim_preimage_le (f := f.dual)

Premises used: Order.height_le_of_krullDim_preimage_le, OrderHom.dual, DFunLike.coe
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
x : α
⊢ ∀ (x : βᵒᵈ),
    krullDim.{u_1}
        (↑(Set.preimage (β := βᵒᵈ)
              (⇑((OrderHom.dual : (a : α →o β) → αᵒᵈ →o βᵒᵈ) f : OrderHom.{u_1, u_2} αᵒᵈ βᵒᵈ) : (a : αᵒᵈ) → βᵒᵈ) {x}) :
          Type u_1) ≤
      (↑m : WithBot ℕ∞)

Tactic:
fun x ↦ le_of_eq_of_le (krullDim_orderDual (α := f ⁻¹' {x})) (h x)

Premises used: Order.krullDim_orderDual, le_of_eq_of_le
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
x : α
⊢ ∀ (x : βᵒᵈ),
    krullDim.{u_1}
        (↑(Set.preimage (β := βᵒᵈ)
              (⇑((OrderHom.dual : (a : α →o β) → αᵒᵈ →o βᵒᵈ) f : OrderHom.{u_1, u_2} αᵒᵈ βᵒᵈ) : (a : αᵒᵈ) → βᵒᵈ) {x}) :
          Type u_1) ≤
      (↑m : WithBot ℕ∞)

Tactic:
exact fun x ↦ le_of_eq_of_le (krullDim_orderDual (α := f ⁻¹' {x})) (h x)

Premises used: Order.krullDim_orderDual, le_of_eq_of_le
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
rw :
  ∀ (i : α),
    (↑(height i) : WithBot ℕ∞) ≤
      (HAdd.hAdd (α := WithBot ℕ∞) (↑m : WithBot ℕ∞) 1 * ⨆ (a : β), (↑(height a) : WithBot ℕ∞)) + (↑m : WithBot ℕ∞)
⊢ krullDim α ≤ HAdd.hAdd (α := WithBot ℕ∞) (↑m : WithBot ℕ∞) 1 * krullDim β + (↑m : WithBot ℕ∞)

Tactic:
rw [Order.krullDim_eq_iSup_height, Order.krullDim_eq_iSup_height, iSup_le_iff]

Premises used: Order.krullDim_eq_iSup_height, iSup_le_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
⊢ ∀ (i : α),
    (↑(height i) : WithBot ℕ∞) ≤
      (HAdd.hAdd (α := WithBot ℕ∞) (↑m : WithBot ℕ∞) 1 * ⨆ (a : β), (↑(height a) : WithBot ℕ∞)) + (↑m : WithBot ℕ∞)

Tactic:
fun x ↦ (WithBot.coe_mono (height_le_of_krullDim_preimage_le f h x)).trans ?_

Premises used: Order.height_le_of_krullDim_preimage_le, WithBot.coe_mono, LE.le.trans
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
refine :
  ∀ (x : α),
    (fun (a : ℕ∞) ↦ (↑a : WithBot ℕ∞))
        (HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * height.{u_2} (α := β) ((f : (a : α) → β) x : β) + (↑m : ℕ∞)) ≤
      (HAdd.hAdd (α := WithBot ℕ∞) (↑m : WithBot ℕ∞) 1 * ⨆ (a : β), (↑(height a) : WithBot ℕ∞)) + (↑m : WithBot ℕ∞)
⊢ ∀ (i : α),
    (↑(height i) : WithBot ℕ∞) ≤
      (HAdd.hAdd (α := WithBot ℕ∞) (↑m : WithBot ℕ∞) 1 * ⨆ (a : β), (↑(height a) : WithBot ℕ∞)) + (↑m : WithBot ℕ∞)

Tactic:
refine fun x ↦ (WithBot.coe_mono (height_le_of_krullDim_preimage_le f h x)).trans ?_

Premises used: Order.height_le_of_krullDim_preimage_le, WithBot.coe_mono, LE.le.trans
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
x : α
bc : 0 ≤ HAdd.hAdd (α := WithBot ℕ∞) (↑m : WithBot ℕ∞) 1
bc₁ : (↑(height.{u_2} (α := β) ((f : (a : α) → β) x : β)) : WithBot ℕ∞) ≤ ⨆ (a : β), (↑(height a) : WithBot ℕ∞)
⊢ HAdd.hAdd (α := WithBot ℕ∞) (↑m : WithBot ℕ∞) 1 * (↑(height.{u_2} (α := β) ((f : (a : α) → β) x : β)) : WithBot ℕ∞) +
      (↑m : WithBot ℕ∞) ≤
    (HAdd.hAdd (α := WithBot ℕ∞) (↑m : WithBot ℕ∞) 1 * ⨆ (a : β), (↑(height a) : WithBot ℕ∞)) + (↑m : WithBot ℕ∞)

Tactic:
gcongr
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
x : α
⊢ 0 ≤ HAdd.hAdd (α := WithBot ℕ∞) (↑m : WithBot ℕ∞) 1

Tactic:
right_eq_inf.mp rfl

Premises used: Iff.mp, right_eq_inf, rfl
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
x : α
⊢ (↑(height.{u_2} (α := β) ((f : (a : α) → β) x : β)) : WithBot ℕ∞) ≤ ⨆ (a : β), (↑(height a) : WithBot ℕ∞)

Tactic:
le_iSup_iff.mpr fun b a ↦ a (f x)

Premises used: Iff.mpr, le_iSup_iff, DFunLike.coe
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
x : α
⊢ 0 ≤ HAdd.hAdd (α := WithBot ℕ∞) (↑m : WithBot ℕ∞) 1

Tactic:
exacts [right_eq_inf.mp rfl, le_iSup_iff.mpr fun b a ↦ a (f x)]

Premises used: Iff.mpr, Iff.mp, le_iSup_iff, DFunLike.coe, right_eq_inf
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α → β
h_mono : Monotone f
h : ∀ (x : β), krullDim.{u_1} (↑(f ⁻¹' {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
⊢ krullDim α ≤ HAdd.hAdd (α := WithBot ℕ∞) (↑m : WithBot ℕ∞) 1 * krullDim β + (↑m : WithBot ℕ∞)

Tactic:
Order.krullDim_le_of_krullDim_preimage_le ⟨f, h_mono⟩ h

Premises used: Order.krullDim_le_of_krullDim_preimage_le, OrderHom.mk
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
e : α ↪o β
⊢ ∀ (b : β), Subsingleton.{u_1 + 1} (↑(Set.preimage (β := β) (⇑e : (a : α) → β) {b}) : Type u_1)

Tactic:
have (b : β) : Subsingleton (e ⁻¹' {b}) := Set.Subsingleton.coe_sort <|
    Set.Subsingleton.preimage Set.subsingleton_singleton e.injective
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
e : α ↪o β
this : ∀ (b : β), Subsingleton.{u_1 + 1} (↑(Set.preimage (β := β) (⇑e : (a : α) → β) {b}) : Type u_1)
⊢ krullDim α ≤ krullDim β

Tactic:
simpa using Order.krullDim_le_of_krullDim_preimage_le' e e.monotone fun _ ↦
    Order.krullDim_nonpos_of_subsingleton

Premises used: OrderEmbedding.monotone, Order.krullDim_nonpos_of_subsingleton, DFunLike.coe, Order.krullDim_le_of_krullDim_preimage_le'
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
α : Type u_2
inst : Lattice α
c : LatticeCon α
x y : α
h : (c.toSetoid : α → α → Prop) (x ⊓ y) (x ⊔ y)
⊢ x ≈ x ⊓ y

Tactic:
simpa using c.inf (c.refl x) (c.symm h)

Premises used: LatticeCon.inf, Setoid.symm, Setoid.refl
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
α : Type u_2
inst : Lattice α
c : LatticeCon α
x y : α
h : (c.toSetoid : α → α → Prop) (x ⊓ y) (x ⊔ y)
⊢ x ⊓ y ≈ y

Tactic:
simpa using c.inf h (c.refl y)

Premises used: LatticeCon.inf, Setoid.refl
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
α : Type u_2
inst : Lattice α
c : LatticeCon α
x y : α
h : (c.toSetoid : α → α → Prop) x y
⊢ x ⊓ y ≈ y

Tactic:
simpa using c.inf h (c.refl y)

Premises used: LatticeCon.inf, Setoid.refl
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
α : Type u_2
inst : Lattice α
c : LatticeCon α
x y : α
h : (c.toSetoid : α → α → Prop) x y
⊢ y ≈ x ⊔ y

Tactic:
simpa using c.sup (c.symm h) (c.refl y)

Premises used: LatticeCon.sup, Setoid.symm, Setoid.refl
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
α : Type u_2
inst : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
a b c d : α
hab : a ≤ b
hbd : b ≤ d
hac : a ≤ c
hcd : c ≤ d
had : r a d
this : r (b ⊓ c ⊓ (b ⊔ c)) (d ⊓ (b ⊔ c))
⊢ r b c

Tactic:
simpa [h₂, inf_eq_right.mpr (sup_le hbd hcd)] using this

Premises used: Iff.mpr, sup_le, inf_eq_right
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
α : Type u_2
inst : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
a b c d : α
hab : a ≤ b
hbd : b ≤ d
hac : a ≤ c
hcd : c ≤ d
had : r a d
suffices : r (b ⊓ c ⊓ (b ⊔ c)) (d ⊓ (b ⊔ c))
⊢ r b c

Tactic:
suffices r (b ⊓ c ⊓ (b ⊔ c)) (d ⊓ (b ⊔ c)) by
    simpa [h₂, inf_eq_right.mpr (sup_le hbd hcd)] using this
-- Module: Mathlib.Order.Lattice.Congruence
Goal:
α : Type u_2
inst : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
a b c d : α
hab : a ≤ b
hbd : b ≤ d
hac : a ≤ c
hcd : c ≤ d
had : r a d
apply : r (b ⊓ c) d
⊢ r (b ⊓ c ⊓ (b ⊔ c)) (d ⊓ (b ⊔ c))

Tactic:
apply (h₄ (inf_le_of_left_le hbd) _).1

Premises used: inf_le_of_left_le, And.left