-- Mathlib/Order/SuccPred/Archimedean.lean
lemma le_total_of_codirected {r v₁ v₂ : α} (h₁ : r ≤ v₁) (h₂ : r ≤ v₂) : v₁ ≤ v₂ ∨ v₂ ≤ v₁

Proof state:
case h.intro
α✝ : Type u_1
inst✝³ : Preorder α✝
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n k : ℕ
h : n ≤ n + k
⊢ succ^[n] r ≤ succ^[k] (succ^[n] r)

Tactic:
apply Order.le_succ_iterate

Result:
no goals

Proof state:
case intro.intro.inr
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n m : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [inst_2 : IsSuccArchimedean α] {r : α} (n m : ℕ),
    n ≤ m → succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
h : ¬n ≤ m
⊢ succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r

Tactic:
rw [Or.comm]

Result:
case intro.intro.inr
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n m : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [inst_2 : IsSuccArchimedean α] {r : α} (n m : ℕ),
    n ≤ m → succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
h : ¬n ≤ m
⊢ succ^[m] r ≤ succ^[n] r ∨ succ^[n] r ≤ succ^[m] r

Proof state:
case h
α✝ : Type u_1
inst✝³ : Preorder α✝
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n m : ℕ
h : n ≤ m
⊢ succ^[n] r ≤ succ^[m] r

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h

Result:
case h.intro
α✝ : Type u_1
inst✝³ : Preorder α✝
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n k : ℕ
h : n ≤ n + k
⊢ succ^[n] r ≤ succ^[n + k] r

Proof state:
case h.intro
α✝ : Type u_1
inst✝³ : Preorder α✝
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n k : ℕ
h : n ≤ n + k
⊢ succ^[n] r ≤ succ^[n + k] r

Tactic:
rw [Nat.add_comm, Function.iterate_add, Function.comp_apply]

Result:
case h.intro
α✝ : Type u_1
inst✝³ : Preorder α✝
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n k : ℕ
h : n ≤ n + k
⊢ succ^[n] r ≤ succ^[k] (succ^[n] r)

Proof state:
case intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₂ : α
h₂ : r ≤ v₂
n : ℕ
h₁ : r ≤ succ^[n] r
⊢ succ^[n] r ≤ v₂ ∨ v₂ ≤ succ^[n] r

Tactic:
obtain ⟨m, rfl⟩ := h₂.exists_succ_iterate

Result:
case intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n : ℕ
h₁ : r ≤ succ^[n] r
m : ℕ
h₂ : r ≤ succ^[m] r
⊢ succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r

Proof state:
case intro.intro.inr
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n m : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [inst_2 : IsSuccArchimedean α] {r : α} (n m : ℕ),
    n ≤ m → succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
h : ¬n ≤ m
⊢ succ^[m] r ≤ succ^[n] r ∨ succ^[n] r ≤ succ^[m] r

Tactic:
apply this

Result:
case intro.intro.inr.h
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n m : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [inst_2 : IsSuccArchimedean α] {r : α} (n m : ℕ),
    n ≤ m → succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
h : ¬n ≤ m
⊢ m ≤ n

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
⊢ v₁ ≤ v₂ ∨ v₂ ≤ v₁

Tactic:
obtain ⟨n, rfl⟩ := h₁.exists_succ_iterate

Result:
case intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₂ : α
h₂ : r ≤ v₂
n : ℕ
h₁ : r ≤ succ^[n] r
⊢ succ^[n] r ≤ v₂ ∨ v₂ ≤ succ^[n] r

Proof state:
case intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n m : ℕ
⊢ succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r

Tactic:
wlog h : n ≤ m

Result:
case intro.intro.inr
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n m : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [inst_2 : IsSuccArchimedean α] {r : α} (n m : ℕ),
    n ≤ m → succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
h : ¬n ≤ m
⊢ succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r

α✝ : Type u_1
inst✝³ : Preorder α✝
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n m : ℕ
h : n ≤ m
⊢ succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r

Proof state:
case intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n : ℕ
h₁ : r ≤ succ^[n] r
m : ℕ
h₂ : r ≤ succ^[m] r
⊢ succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r

Tactic:
clear h₁ h₂

Result:
case intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n m : ℕ
⊢ succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r

Proof state:
case intro.intro.inr.h
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n m : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [inst_2 : IsSuccArchimedean α] {r : α} (n m : ℕ),
    n ≤ m → succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
h : ¬n ≤ m
⊢ m ≤ n

Tactic:
exact Nat.le_of_not_ge h

Result:
no goals

Proof state:
α✝ : Type u_1
inst✝³ : Preorder α✝
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n m : ℕ
h : n ≤ m
⊢ succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r

Tactic:
left

Result:
case h
α✝ : Type u_1
inst✝³ : Preorder α✝
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n m : ℕ
h : n ≤ m
⊢ succ^[n] r ≤ succ^[m] r