-- Mathlib/Order/SuccPred/Tree.lean
@[simp]
lemma pred_findAtom (r : α) : Order.pred (findAtom r) = ⊥

Proof state:
case succ
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
n✝ : ℕ
h : Nat.find ⋯ = n✝ + 1
⊢ Order.pred (Order.pred^[n✝ + 1 - 1] r) = ⊥

Tactic:
simp only [Nat.add_sub_cancel_right, ← Function.iterate_succ_apply', Nat.succ_eq_add_one]

Result:
case succ
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
n✝ : ℕ
h : Nat.find ⋯ = n✝ + 1
⊢ Order.pred^[n✝ + 1] r = ⊥

Proof state:
case succ
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
n✝ : ℕ
h : Nat.find ⋯ = n✝ + 1
⊢ Order.pred^[n✝ + 1] r = ⊥

Tactic:
rw [← h]

Result:
case succ
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
n✝ : ℕ
h : Nat.find ⋯ = n✝ + 1
⊢ Order.pred^[Nat.find ⋯] r = ⊥

Proof state:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
n : ℕ
h : Nat.find ⋯ = n
⊢ Order.pred (Order.pred^[n - 1] r) = ⊥

Tactic:
cases n

Result:
case zero
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Nat.find ⋯ = 0
⊢ Order.pred (Order.pred^[0 - 1] r) = ⊥

case succ
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
n✝ : ℕ
h : Nat.find ⋯ = n✝ + 1
⊢ Order.pred (Order.pred^[n✝ + 1 - 1] r) = ⊥

Proof state:
case zero
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Nat.find ⋯ = 0
this : r = ⊥
⊢ Order.pred (Order.pred^[0 - 1] r) = ⊥

Tactic:
simp [this]

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Nat.find ⋯ = 0
⊢ Order.pred^[0] r = ⊥

Tactic:
rw [← h]

Result:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Nat.find ⋯ = 0
⊢ Order.pred^[Nat.find ⋯] r = ⊥

Proof state:
case zero
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Nat.find ⋯ = 0
this : Order.pred^[0] r = ⊥
⊢ Order.pred (Order.pred^[0 - 1] r) = ⊥

Tactic:
simp only [Function.iterate_zero, id_eq] at this

Result:
case zero
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Nat.find ⋯ = 0
this : r = ⊥
⊢ Order.pred (Order.pred^[0 - 1] r) = ⊥

Proof state:
case succ
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
n✝ : ℕ
h : Nat.find ⋯ = n✝ + 1
⊢ Order.pred^[Nat.find ⋯] r = ⊥

Tactic:
apply Nat.find_spec (bot_le (a := r)).exists_pred_iterate

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
⊢ Order.pred (findAtom r) = ⊥

Tactic:
unfold findAtom

Result:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
⊢ Order.pred (Order.pred^[Nat.find ⋯ - 1] r) = ⊥

Proof state:
case zero
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Nat.find ⋯ = 0
⊢ Order.pred (Order.pred^[0 - 1] r) = ⊥

Tactic:
have : Order.pred^[0] r = ⊥ := by
  rw [← h]
  apply Nat.find_spec (bot_le (a := r)).exists_pred_iterate

Result:
case zero
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Nat.find ⋯ = 0
this : Order.pred^[0] r = ⊥
⊢ Order.pred (Order.pred^[0 - 1] r) = ⊥

Proof state:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Nat.find ⋯ = 0
⊢ Order.pred^[Nat.find ⋯] r = ⊥

Tactic:
apply Nat.find_spec (bot_le (a := r)).exists_pred_iterate

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
⊢ Order.pred (Order.pred^[Nat.find ⋯ - 1] r) = ⊥

Tactic:
generalize h : Nat.find (bot_le (a := r)).exists_pred_iterate = n

Result:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
n : ℕ
h : Nat.find ⋯ = n
⊢ Order.pred (Order.pred^[n - 1] r) = ⊥