-- Mathlib/Order/KrullDimension.lean
lemma height_eq_coe_iff {x : α} {n : ℕ} :
    height x = n ↔
      height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = n - 1) ∧ (∀ y < x, height y < n)

Proof state:
case succ
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n✝ : ℕ
⊢ height x = ↑(n✝ + 1) ↔ (n✝ + 1 = 0 ∨ ∃ y < x, height y = ↑(n✝ + 1) - 1) ∧ ∀ y < x, height y < ↑(n✝ + 1)

Tactic:
case succ n =>
  simp only [Nat.cast_add, Nat.cast_one, add_eq_zero, one_ne_zero, and_false, false_or]
  rw [height_eq_coe_add_one_iff]
  simp only [hfin, true_and]
  congr! 3
  rename_i y _
  cases height y <;> simp; norm_cast; omega

Result:
no goals

Proof state:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
⊢ height x = ↑(n + 1) ↔ (n + 1 = 0 ∨ ∃ y < x, height y = ↑(n + 1) - 1) ∧ ∀ y < x, height y < ↑(n + 1)

Tactic:
simp only [Nat.cast_add, Nat.cast_one, add_eq_zero, one_ne_zero, and_false, false_or]

Result:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
⊢ height x = ↑n + 1 ↔ (∃ y < x, height y = ↑n + 1 - 1) ∧ ∀ y < x, height y < ↑n + 1

Proof state:
case a.h.e'_2.h.h'.a.coe
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
y : α
a✝¹ : y < x
a✝ : ℕ
⊢ a✝ ≤ n ↔ a✝ < n + 1

Tactic:
omega

Result:
no goals

Proof state:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
⊢ height x = ↑n + 1 ↔ (∃ y < x, height y = ↑n + 1 - 1) ∧ ∀ y < x, height y < ↑n + 1

Tactic:
rw [height_eq_coe_add_one_iff]

Result:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
⊢ (height x < ⊤ ∧ (∃ y < x, height y = ↑n) ∧ ∀ y < x, height y ≤ ↑n) ↔
    (∃ y < x, height y = ↑n + 1 - 1) ∧ ∀ y < x, height y < ↑n + 1

Proof state:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
⊢ height x = ↑0 ↔ (0 = 0 ∨ ∃ y < x, height y = ↑0 - 1) ∧ ∀ y < x, height y < ↑0

Tactic:
simp [isMin_iff_forall_not_lt]

Result:
no goals

Proof state:
case zero
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
⊢ height x = ↑0 ↔ (0 = 0 ∨ ∃ y < x, height y = ↑0 - 1) ∧ ∀ y < x, height y < ↑0

case succ
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n✝ : ℕ
⊢ height x = ↑(n✝ + 1) ↔ (n✝ + 1 = 0 ∨ ∃ y < x, height y = ↑(n✝ + 1) - 1) ∧ ∀ y < x, height y < ↑(n✝ + 1)

Tactic:
case zero => simp [isMin_iff_forall_not_lt]

Result:
case succ
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n✝ : ℕ
⊢ height x = ↑(n✝ + 1) ↔ (n✝ + 1 = 0 ∨ ∃ y < x, height y = ↑(n✝ + 1) - 1) ∧ ∀ y < x, height y < ↑(n✝ + 1)

Proof state:
case a.h.e'_2.h.h'.a
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
y : α
a✝ : y < x
⊢ height y ≤ ↑n ↔ height y < ↑n + 1

Tactic:
cases height y <;> simp

Result:
case a.h.e'_2.h.h'.a.coe
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
y : α
a✝¹ : y < x
a✝ : ℕ
⊢ a✝ ≤ n ↔ ↑a✝ < ↑n + 1

Proof state:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
⊢ ((∃ y < x, height y = ↑n) ∧ ∀ y < x, height y ≤ ↑n) ↔ (∃ y < x, height y = ↑n + 1 - 1) ∧ ∀ y < x, height y < ↑n + 1

Tactic:
congr! 3

Result:
case a.h.e'_2.h.h'.a
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
a✝¹ : α
a✝ : a✝¹ < x
⊢ height a✝¹ ≤ ↑n ↔ height a✝¹ < ↑n + 1

Proof state:
case a.h.e'_2.h.h'.a
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
a✝¹ : α
a✝ : a✝¹ < x
⊢ height a✝¹ ≤ ↑n ↔ height a✝¹ < ↑n + 1

Tactic:
rename_i y _

Result:
case a.h.e'_2.h.h'.a
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
y : α
a✝ : y < x
⊢ height y ≤ ↑n ↔ height y < ↑n + 1

Proof state:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x = ↑n ↔ height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = ↑n - 1) ∧ ∀ y < x, height y < ↑n

Tactic:
simp only [hfin, true_and]

Result:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x = ↑n ↔ (n = 0 ∨ ∃ y < x, height y = ↑n - 1) ∧ ∀ y < x, height y < ↑n

Proof state:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x = ↑n ↔ (n = 0 ∨ ∃ y < x, height y = ↑n - 1) ∧ ∀ y < x, height y < ↑n

Tactic:
cases n

Result:
case zero
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
⊢ height x = ↑0 ↔ (0 = 0 ∨ ∃ y < x, height y = ↑0 - 1) ∧ ∀ y < x, height y < ↑0

case succ
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n✝ : ℕ
⊢ height x = ↑(n✝ + 1) ↔ (n✝ + 1 = 0 ∨ ∃ y < x, height y = ↑(n✝ + 1) - 1) ∧ ∀ y < x, height y < ↑(n✝ + 1)

Proof state:
case inr
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] {x : α} {n : ℕ},
    height x < ⊤ → (height x = ↑n ↔ height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = ↑n - 1) ∧ ∀ y < x, height y < ↑n)
hfin : ¬height x < ⊤
⊢ height x = ↑n ↔ height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = ↑n - 1) ∧ ∀ y < x, height y < ↑n

Tactic:
simp_all

Result:
no goals

Proof state:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
⊢ (height x < ⊤ ∧ (∃ y < x, height y = ↑n) ∧ ∀ y < x, height y ≤ ↑n) ↔
    (∃ y < x, height y = ↑n + 1 - 1) ∧ ∀ y < x, height y < ↑n + 1

Tactic:
simp only [hfin, true_and]

Result:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
⊢ ((∃ y < x, height y = ↑n) ∧ ∀ y < x, height y ≤ ↑n) ↔ (∃ y < x, height y = ↑n + 1 - 1) ∧ ∀ y < x, height y < ↑n + 1

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
⊢ height x = ↑n ↔ height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = ↑n - 1) ∧ ∀ y < x, height y < ↑n

Tactic:
wlog hfin : height x < ⊤

Result:
case inr
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] {x : α} {n : ℕ},
    height x < ⊤ → (height x = ↑n ↔ height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = ↑n - 1) ∧ ∀ y < x, height y < ↑n)
hfin : ¬height x < ⊤
⊢ height x = ↑n ↔ height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = ↑n - 1) ∧ ∀ y < x, height y < ↑n

α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x = ↑n ↔ height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = ↑n - 1) ∧ ∀ y < x, height y < ↑n

Proof state:
case a.h.e'_2.h.h'.a.coe
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
y : α
a✝¹ : y < x
a✝ : ℕ
⊢ a✝ ≤ n ↔ ↑a✝ < ↑n + 1

Tactic:
norm_cast

Result:
case a.h.e'_2.h.h'.a.coe
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
y : α
a✝¹ : y < x
a✝ : ℕ
⊢ a✝ ≤ n ↔ a✝ < n + 1