-- Mathlib/Order/KrullDimension.lean
/--
The Krull dimension is the supremum of the elements' height plus coheight.
-/
lemma krullDim_eq_iSup_height_add_coheight_of_nonempty [Nonempty α] :
    krullDim α = ↑(⨆ (a : α), height a + coheight a)

Proof state:
case h.coe.top
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this✝ : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = ↑n
hch : coheight a = ⊤
⊢ ↑n + ⊤ ≤ ⨆ p, ↑p.length

Tactic:
simp_all

Result:
no goals

Proof state:
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this✝ : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = ↑n
m : ℕ
hch : coheight a = ↑m
p₁ : LTSeries α
hlast : RelSeries.last p₁ = a
hlen₁ : p₁.length = n
p₂ : LTSeries α
hhead : RelSeries.head p₂ = a
hlen₂ : p₂.length = m
⊢ ↑n + ↑m ≤ ↑(RelSeries.smash p₁ p₂ ⋯).length

Tactic:
simp [*]

Result:
no goals

Proof state:
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
⊢ ⨆ a, height a + coheight a ≤ ⨆ p, ↑p.length

Tactic:
apply iSup_le

Result:
case h
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
⊢ ∀ (i : α), height i + coheight i ≤ ⨆ p, ↑p.length

Proof state:
case h.coe
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this✝ : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = ↑n
⊢ ↑n + coheight a ≤ ⨆ p, ↑p.length

Tactic:
cases hch : coheight a with
| top => simp_all
| coe m =>
  obtain ⟨p₁, hlast, hlen₁⟩ := exists_series_of_height_eq_coe a hh
  obtain ⟨p₂, hhead, hlen₂⟩ := exists_series_of_coheight_eq_coe a hch
  apply le_iSup_of_le ((p₁.smash p₂) (by simp [*])) (by simp [*])

Result:
no goals

Proof state:
case h
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
⊢ height a + coheight a ≤ ⨆ p, ↑p.length

Tactic:
have : height a < ⊤ := WithBot.coe_lt_coe.mp (lt_of_le_of_lt (height_le_krullDim a) hnottop)

Result:
case h
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this : height a < ⊤
⊢ height a + coheight a ≤ ⨆ p, ↑p.length

Proof state:
case h.coe.coe.intro.intro
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this✝ : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = ↑n
m : ℕ
hch : coheight a = ↑m
p₁ : LTSeries α
hlast : RelSeries.last p₁ = a
hlen₁ : p₁.length = n
⊢ ↑n + ↑m ≤ ⨆ p, ↑p.length

Tactic:
obtain ⟨p₂, hhead, hlen₂⟩ := exists_series_of_coheight_eq_coe a hch

Result:
case h.coe.coe.intro.intro.intro.intro
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this✝ : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = ↑n
m : ℕ
hch : coheight a = ↑m
p₁ : LTSeries α
hlast : RelSeries.last p₁ = a
hlen₁ : p₁.length = n
p₂ : LTSeries α
hhead : RelSeries.head p₂ = a
hlen₂ : p₂.length = m
⊢ ↑n + ↑m ≤ ⨆ p, ↑p.length

Proof state:
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this✝ : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = ↑n
m : ℕ
hch : coheight a = ↑m
p₁ : LTSeries α
hlast : RelSeries.last p₁ = a
hlen₁ : p₁.length = n
p₂ : LTSeries α
hhead : RelSeries.head p₂ = a
hlen₂ : p₂.length = m
⊢ RelSeries.last p₁ = RelSeries.head p₂

Tactic:
simp [*]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ∀ (x : α), height x ≤ height x + coheight x

Tactic:
simp

Result:
no goals

Proof state:
case h
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this : height a < ⊤
⊢ height a + coheight a ≤ ⨆ p, ↑p.length

Tactic:
have : coheight a < ⊤ := WithBot.coe_lt_coe.mp (lt_of_le_of_lt (coheight_le_krullDim a) hnottop)

Result:
case h
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this✝ : height a < ⊤
this : coheight a < ⊤
⊢ height a + coheight a ≤ ⨆ p, ↑p.length

Proof state:
case h.top
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this✝ : height a < ⊤
this : coheight a < ⊤
hh : height a = ⊤
⊢ ⊤ + coheight a ≤ ⨆ p, ↑p.length

Tactic:
simp_all

Result:
no goals

Proof state:
case a.inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
this :
  ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Nonempty α],
    krullDim α < ⊤ → ↑(⨆ a, height a + coheight a) ≤ krullDim α
hnottop : ¬krullDim α < ⊤
⊢ ↑(⨆ a, height a + coheight a) ≤ krullDim α

Tactic:
simp_all

Result:
no goals

Proof state:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ↑(⨆ a, height a + coheight a) ≤ krullDim α

Tactic:
wlog hnottop : krullDim α < ⊤

Result:
case a.inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
this :
  ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Nonempty α],
    krullDim α < ⊤ → ↑(⨆ a, height a + coheight a) ≤ krullDim α
hnottop : ¬krullDim α < ⊤
⊢ ↑(⨆ a, height a + coheight a) ≤ krullDim α

α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
⊢ ↑(⨆ a, height a + coheight a) ≤ krullDim α

Proof state:
case h
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
⊢ ∀ (i : α), height i + coheight i ≤ ⨆ p, ↑p.length

Tactic:
intro a

Result:
case h
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
⊢ height a + coheight a ≤ ⨆ p, ↑p.length

Proof state:
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
⊢ ↑(⨆ a, height a + coheight a) ≤ krullDim α

Tactic:
rw [krullDim_eq_iSup_length, WithBot.coe_le_coe]

Result:
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
⊢ ⨆ a, height a + coheight a ≤ ⨆ p, ↑p.length

Proof state:
case h
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this✝ : height a < ⊤
this : coheight a < ⊤
⊢ height a + coheight a ≤ ⨆ p, ↑p.length

Tactic:
cases hh : height a with
| top => simp_all
| coe n =>
  cases hch : coheight a with
  | top => simp_all
  | coe m =>
    obtain ⟨p₁, hlast, hlen₁⟩ := exists_series_of_height_eq_coe a hh
    obtain ⟨p₂, hhead, hlen₂⟩ := exists_series_of_coheight_eq_coe a hch
    apply le_iSup_of_le ((p₁.smash p₂) (by simp [*])) (by simp [*])

Result:
no goals

Proof state:
case h.coe.coe.intro.intro.intro.intro
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this✝ : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = ↑n
m : ℕ
hch : coheight a = ↑m
p₁ : LTSeries α
hlast : RelSeries.last p₁ = a
hlen₁ : p₁.length = n
p₂ : LTSeries α
hhead : RelSeries.head p₂ = a
hlen₂ : p₂.length = m
⊢ ↑n + ↑m ≤ ⨆ p, ↑p.length

Tactic:
apply le_iSup_of_le ((p₁.smash p₂) (by simp [*])) (by simp [*])

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ BddAbove (Set.range fun a => height a + coheight a)

Tactic:
bddDefault

Result:
no goals

Proof state:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ⨆ a, height a ≤ ⨆ a, height a + coheight a

Tactic:
apply ciSup_mono (by bddDefault) (by simp)

Result:
no goals