-- Mathlib/Order/SuccPred/Archimedean.lean
lemma SuccOrder.forall_ne_bot_iff
    [Nontrivial α] [PartialOrder α] [OrderBot α] [SuccOrder α] [IsSuccArchimedean α]
    (P : α → Prop) :
    (∀ i, i ≠ ⊥ → P i) ↔ (∀ i, P (SuccOrder.succ i))

Proof state:
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
i : α
hi : i ≠ ⊥
⊢ P i

Tactic:
obtain ⟨j, rfl⟩ := exists_succ_iterate_of_le (bot_le : ⊥ ≤ i)

Result:
case intro
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
⊢ P (Order.succ^[j] ⊥)

Proof state:
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
⊢ (∀ (i : α), i ≠ ⊥ → P i) ↔ ∀ (i : α), P (succ i)

Tactic:
refine ⟨fun h i ↦ h _ (Order.succ_ne_bot i), fun h i hi ↦ ?_⟩

Result:
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
i : α
hi : i ≠ ⊥
⊢ P i

Proof state:
case intro
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
hj : 0 < j
⊢ P (Order.succ^[j] ⊥)

Tactic:
rw [← Nat.succ_pred_eq_of_pos hj]

Result:
case intro
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
hj : 0 < j
⊢ P (Order.succ^[j.pred.succ] ⊥)

Proof state:
case intro
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
hj : 0 < j
⊢ P (Order.succ (Order.succ^[j.pred] ⊥))

Tactic:
apply h

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
⊢ P (Order.succ^[j] ⊥)

Tactic:
have hj : 0 < j := by apply Nat.pos_of_ne_zero; contrapose! hi; simp [hi]

Result:
case intro
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
hj : 0 < j
⊢ P (Order.succ^[j] ⊥)

Proof state:
case a
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : j = 0
⊢ Order.succ^[j] ⊥ = ⊥

Tactic:
simp [hi]

Result:
no goals

Proof state:
case a
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
⊢ j ≠ 0

Tactic:
contrapose! hi

Result:
case a
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : j = 0
⊢ Order.succ^[j] ⊥ = ⊥

Proof state:
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
⊢ 0 < j

Tactic:
apply Nat.pos_of_ne_zero

Result:
case a
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
⊢ j ≠ 0

Proof state:
case intro
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
hj : 0 < j
⊢ P (Order.succ^[j.pred.succ] ⊥)

Tactic:
simp only [Function.iterate_succ', Function.comp_apply]

Result:
case intro
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
hj : 0 < j
⊢ P (Order.succ (Order.succ^[j.pred] ⊥))