[GOAL]
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n : ℕ
h₀ : x 0 ≤ y 0
hx : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
⊢ x n ≤ y n
[PROOFSTEP]
induction' n with n ihn
[GOAL]
case zero
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n : ℕ
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)
hy✝ : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
hx : ∀ (k : ℕ), k < Nat.zero → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < Nat.zero → f (y k) ≤ y (k + 1)
⊢ x Nat.zero ≤ y Nat.zero
[PROOFSTEP]
exact h₀
[GOAL]
case succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n✝ : ℕ
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n✝ → x (k + 1) ≤ f (x k)
hy✝ : ∀ (k : ℕ), k < n✝ → f (y k) ≤ y (k + 1)
n : ℕ
ihn : (∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n ≤ y n
hx : ∀ (k : ℕ), k < Nat.succ n → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < Nat.succ n → f (y k) ≤ y (k + 1)
⊢ x (Nat.succ n) ≤ y (Nat.succ n)
[PROOFSTEP]
refine' (hx _ n.lt_succ_self).trans ((hf $ ihn _ _).trans (hy _ n.lt_succ_self))
[GOAL]
case succ.refine'_1
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n✝ : ℕ
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n✝ → x (k + 1) ≤ f (x k)
hy✝ : ∀ (k : ℕ), k < n✝ → f (y k) ≤ y (k + 1)
n : ℕ
ihn : (∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n ≤ y n
hx : ∀ (k : ℕ), k < Nat.succ n → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < Nat.succ n → f (y k) ≤ y (k + 1)
⊢ ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)
case succ.refine'_2
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n✝ : ℕ
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n✝ → x (k + 1) ≤ f (x k)
hy✝ : ∀ (k : ℕ), k < n✝ → f (y k) ≤ y (k + 1)
n : ℕ
ihn : (∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n ≤ y n
hx : ∀ (k : ℕ), k < Nat.succ n → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < Nat.succ n → f (y k) ≤ y (k + 1)
⊢ ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
[PROOFSTEP]
exact fun k hk => hx _ (hk.trans n.lt_succ_self)
[GOAL]
case succ.refine'_2
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n✝ : ℕ
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n✝ → x (k + 1) ≤ f (x k)
hy✝ : ∀ (k : ℕ), k < n✝ → f (y k) ≤ y (k + 1)
n : ℕ
ihn : (∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n ≤ y n
hx : ∀ (k : ℕ), k < Nat.succ n → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < Nat.succ n → f (y k) ≤ y (k + 1)
⊢ ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
[PROOFSTEP]
exact fun k hk => hy _ (hk.trans n.lt_succ_self)
[GOAL]
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n : ℕ
hn : 0 < n
h₀ : x 0 ≤ y 0
hx : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
⊢ x n < y n
[PROOFSTEP]
induction' n with n ihn
[GOAL]
case zero
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n : ℕ
hn✝ : 0 < n
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)
hy✝ : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
hn : 0 < Nat.zero
hx : ∀ (k : ℕ), k < Nat.zero → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < Nat.zero → f (y k) ≤ y (k + 1)
⊢ x Nat.zero < y Nat.zero
[PROOFSTEP]
exact hn.false.elim
[GOAL]
case succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n✝ : ℕ
hn✝ : 0 < n✝
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n✝ → x (k + 1) < f (x k)
hy✝ : ∀ (k : ℕ), k < n✝ → f (y k) ≤ y (k + 1)
n : ℕ
ihn : 0 < n → (∀ (k : ℕ), k < n → x (k + 1) < f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n < y n
hn : 0 < Nat.succ n
hx : ∀ (k : ℕ), k < Nat.succ n → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < Nat.succ n → f (y k) ≤ y (k + 1)
⊢ x (Nat.succ n) < y (Nat.succ n)
[PROOFSTEP]
suffices x n ≤ y n from (hx n n.lt_succ_self).trans_le ((hf this).trans $ hy n n.lt_succ_self)
[GOAL]
case succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n✝ : ℕ
hn✝ : 0 < n✝
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n✝ → x (k + 1) < f (x k)
hy✝ : ∀ (k : ℕ), k < n✝ → f (y k) ≤ y (k + 1)
n : ℕ
ihn : 0 < n → (∀ (k : ℕ), k < n → x (k + 1) < f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n < y n
hn : 0 < Nat.succ n
hx : ∀ (k : ℕ), k < Nat.succ n → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < Nat.succ n → f (y k) ≤ y (k + 1)
⊢ x n ≤ y n
[PROOFSTEP]
cases n with
| zero => exact h₀
| succ n =>
  refine' (ihn n.zero_lt_succ (fun k hk => hx _ _) fun k hk => hy _ _).le <;> exact hk.trans n.succ.lt_succ_self
[GOAL]
case succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n✝ : ℕ
hn✝ : 0 < n✝
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n✝ → x (k + 1) < f (x k)
hy✝ : ∀ (k : ℕ), k < n✝ → f (y k) ≤ y (k + 1)
n : ℕ
ihn : 0 < n → (∀ (k : ℕ), k < n → x (k + 1) < f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n < y n
hn : 0 < Nat.succ n
hx : ∀ (k : ℕ), k < Nat.succ n → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < Nat.succ n → f (y k) ≤ y (k + 1)
⊢ x n ≤ y n
[PROOFSTEP]
cases n with
| zero => exact h₀
| succ n =>
  refine' (ihn n.zero_lt_succ (fun k hk => hx _ _) fun k hk => hy _ _).le <;> exact hk.trans n.succ.lt_succ_self
[GOAL]
case succ.zero
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n : ℕ
hn✝ : 0 < n
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)
hy✝ : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
ihn :
  0 < Nat.zero →
    (∀ (k : ℕ), k < Nat.zero → x (k + 1) < f (x k)) →
      (∀ (k : ℕ), k < Nat.zero → f (y k) ≤ y (k + 1)) → x Nat.zero < y Nat.zero
hn : 0 < Nat.succ Nat.zero
hx : ∀ (k : ℕ), k < Nat.succ Nat.zero → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < Nat.succ Nat.zero → f (y k) ≤ y (k + 1)
⊢ x Nat.zero ≤ y Nat.zero
[PROOFSTEP]

| zero => exact h₀
[GOAL]
case succ.zero
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n : ℕ
hn✝ : 0 < n
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)
hy✝ : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
ihn :
  0 < Nat.zero →
    (∀ (k : ℕ), k < Nat.zero → x (k + 1) < f (x k)) →
      (∀ (k : ℕ), k < Nat.zero → f (y k) ≤ y (k + 1)) → x Nat.zero < y Nat.zero
hn : 0 < Nat.succ Nat.zero
hx : ∀ (k : ℕ), k < Nat.succ Nat.zero → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < Nat.succ Nat.zero → f (y k) ≤ y (k + 1)
⊢ x Nat.zero ≤ y Nat.zero
[PROOFSTEP]
exact h₀
[GOAL]
case succ.succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n✝ : ℕ
hn✝ : 0 < n✝
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n✝ → x (k + 1) < f (x k)
hy✝ : ∀ (k : ℕ), k < n✝ → f (y k) ≤ y (k + 1)
n : ℕ
ihn :
  0 < Nat.succ n →
    (∀ (k : ℕ), k < Nat.succ n → x (k + 1) < f (x k)) →
      (∀ (k : ℕ), k < Nat.succ n → f (y k) ≤ y (k + 1)) → x (Nat.succ n) < y (Nat.succ n)
hn : 0 < Nat.succ (Nat.succ n)
hx : ∀ (k : ℕ), k < Nat.succ (Nat.succ n) → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < Nat.succ (Nat.succ n) → f (y k) ≤ y (k + 1)
⊢ x (Nat.succ n) ≤ y (Nat.succ n)
[PROOFSTEP]

| succ n =>
  refine' (ihn n.zero_lt_succ (fun k hk => hx _ _) fun k hk => hy _ _).le <;> exact hk.trans n.succ.lt_succ_self
[GOAL]
case succ.succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n✝ : ℕ
hn✝ : 0 < n✝
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n✝ → x (k + 1) < f (x k)
hy✝ : ∀ (k : ℕ), k < n✝ → f (y k) ≤ y (k + 1)
n : ℕ
ihn :
  0 < Nat.succ n →
    (∀ (k : ℕ), k < Nat.succ n → x (k + 1) < f (x k)) →
      (∀ (k : ℕ), k < Nat.succ n → f (y k) ≤ y (k + 1)) → x (Nat.succ n) < y (Nat.succ n)
hn : 0 < Nat.succ (Nat.succ n)
hx : ∀ (k : ℕ), k < Nat.succ (Nat.succ n) → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < Nat.succ (Nat.succ n) → f (y k) ≤ y (k + 1)
⊢ x (Nat.succ n) ≤ y (Nat.succ n)
[PROOFSTEP]
refine' (ihn n.zero_lt_succ (fun k hk => hx _ _) fun k hk => hy _ _).le
[GOAL]
case succ.succ.refine'_1
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n✝ : ℕ
hn✝ : 0 < n✝
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n✝ → x (k + 1) < f (x k)
hy✝ : ∀ (k : ℕ), k < n✝ → f (y k) ≤ y (k + 1)
n : ℕ
ihn :
  0 < Nat.succ n →
    (∀ (k : ℕ), k < Nat.succ n → x (k + 1) < f (x k)) →
      (∀ (k : ℕ), k < Nat.succ n → f (y k) ≤ y (k + 1)) → x (Nat.succ n) < y (Nat.succ n)
hn : 0 < Nat.succ (Nat.succ n)
hx : ∀ (k : ℕ), k < Nat.succ (Nat.succ n) → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < Nat.succ (Nat.succ n) → f (y k) ≤ y (k + 1)
k : ℕ
hk : k < Nat.succ n
⊢ k < Nat.succ (Nat.succ n)
[PROOFSTEP]
exact hk.trans n.succ.lt_succ_self
[GOAL]
case succ.succ.refine'_2
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n✝ : ℕ
hn✝ : 0 < n✝
h₀ : x 0 ≤ y 0
hx✝ : ∀ (k : ℕ), k < n✝ → x (k + 1) < f (x k)
hy✝ : ∀ (k : ℕ), k < n✝ → f (y k) ≤ y (k + 1)
n : ℕ
ihn :
  0 < Nat.succ n →
    (∀ (k : ℕ), k < Nat.succ n → x (k + 1) < f (x k)) →
      (∀ (k : ℕ), k < Nat.succ n → f (y k) ≤ y (k + 1)) → x (Nat.succ n) < y (Nat.succ n)
hn : 0 < Nat.succ (Nat.succ n)
hx : ∀ (k : ℕ), k < Nat.succ (Nat.succ n) → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < Nat.succ (Nat.succ n) → f (y k) ≤ y (k + 1)
k : ℕ
hk : k < Nat.succ n
⊢ k < Nat.succ (Nat.succ n)
[PROOFSTEP]
exact hk.trans n.succ.lt_succ_self
[GOAL]
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n : ℕ
h₀ : x 0 < y 0
hx : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
⊢ x n < y n
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 < y 0
hx : ∀ (k : ℕ), k < Nat.zero → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < Nat.zero → f (y k) ≤ y (k + 1)
⊢ x Nat.zero < y Nat.zero
case succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 < y 0
n✝ : ℕ
hx : ∀ (k : ℕ), k < Nat.succ n✝ → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < Nat.succ n✝ → f (y k) ≤ y (k + 1)
⊢ x (Nat.succ n✝) < y (Nat.succ n✝)
[PROOFSTEP]
exacts [h₀, hf.seq_pos_lt_seq_of_lt_of_le (Nat.zero_lt_succ _) h₀.le hx hy]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : α → α
x✝ y : ℕ → α
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
⊢ (h ∘ g^[n]) x ≤ (f^[n] ∘ h) x
[PROOFSTEP]
apply hf.seq_le_seq n
[GOAL]
case h₀
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : α → α
x✝ y : ℕ → α
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
⊢ (h ∘ g^[0]) x ≤ (f^[0] ∘ h) x
[PROOFSTEP]
intros
[GOAL]
case hx
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : α → α
x✝ y : ℕ → α
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
⊢ ∀ (k : ℕ), k < n → (h ∘ g^[k + 1]) x ≤ f ((h ∘ g^[k]) x)
[PROOFSTEP]
intros
[GOAL]
case hy
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : α → α
x✝ y : ℕ → α
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
⊢ ∀ (k : ℕ), k < n → f ((f^[k] ∘ h) x) ≤ (f^[k + 1] ∘ h) x
[PROOFSTEP]
intros
[GOAL]
case h₀
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : α → α
x✝ y : ℕ → α
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
⊢ (h ∘ g^[0]) x ≤ (f^[0] ∘ h) x
[PROOFSTEP]
simp [iterate_succ', -iterate_succ, comp_apply, id_eq, le_refl]
[GOAL]
case hx
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : α → α
x✝ y : ℕ → α
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
k✝ : ℕ
a✝ : k✝ < n
⊢ (h ∘ g^[k✝ + 1]) x ≤ f ((h ∘ g^[k✝]) x)
[PROOFSTEP]
simp [iterate_succ', -iterate_succ, comp_apply, id_eq, le_refl]
[GOAL]
case hy
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : α → α
x✝ y : ℕ → α
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
k✝ : ℕ
a✝ : k✝ < n
⊢ f ((f^[k✝] ∘ h) x) ≤ (f^[k✝ + 1] ∘ h) x
[PROOFSTEP]
simp [iterate_succ', -iterate_succ, comp_apply, id_eq, le_refl]
[GOAL]
case hx
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : α → α
x✝ y : ℕ → α
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
k✝ : ℕ
a✝ : k✝ < n
⊢ h (g (g^[k✝] x)) ≤ f (h (g^[k✝] x))
[PROOFSTEP]
case hx => exact H _
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : α → α
x✝ y : ℕ → α
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
k✝ : ℕ
a✝ : k✝ < n
⊢ h (g (g^[k✝] x)) ≤ f (h (g^[k✝] x))
[PROOFSTEP]
case hx => exact H _
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : α → α
x✝ y : ℕ → α
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
k✝ : ℕ
a✝ : k✝ < n
⊢ h (g (g^[k✝] x)) ≤ f (h (g^[k✝] x))
[PROOFSTEP]
exact H _
[GOAL]
α : Type u_1
inst✝ : Preorder α
f : α → α
h : id ≤ f
n : ℕ
⊢ id ≤ f^[n]
[PROOFSTEP]
simpa only [iterate_id] using monotone_id.iterate_le_of_le h n
[GOAL]
α : Type u_1
inst✝ : Preorder α
f : α → α
h : id ≤ f
n : ℕ
x : α
⊢ f^[n] x ≤ f^[n + 1] x
[PROOFSTEP]
rw [iterate_succ_apply']
[GOAL]
α : Type u_1
inst✝ : Preorder α
f : α → α
h : id ≤ f
n : ℕ
x : α
⊢ f^[n] x ≤ f (f^[n] x)
[PROOFSTEP]
exact h _
[GOAL]
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ f^[n] x ≤ g^[n] x
[PROOFSTEP]
apply hf.seq_le_seq n
[GOAL]
case h₀
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ f^[0] x ≤ g^[0] x
[PROOFSTEP]
rfl
[GOAL]
case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ ∀ (k : ℕ), k < n → f^[k + 1] x ≤ f (f^[k] x)
[PROOFSTEP]
intros
[GOAL]
case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n k✝ : ℕ
a✝ : k✝ < n
⊢ f^[k✝ + 1] x ≤ f (f^[k✝] x)
[PROOFSTEP]
rw [iterate_succ_apply']
[GOAL]
case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ ∀ (k : ℕ), k < n → f (g^[k] x) ≤ g^[k + 1] x
[PROOFSTEP]
intros
[GOAL]
case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n k✝ : ℕ
a✝ : k✝ < n
⊢ f (g^[k✝] x) ≤ g^[k✝ + 1] x
[PROOFSTEP]
simp [h.iterate_right _ _, hg.iterate _ hx]
[GOAL]
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ f^[n] x < g^[n] x
[PROOFSTEP]
apply hf.seq_pos_lt_seq_of_le_of_lt hn
[GOAL]
case h₀
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ f^[0] x ≤ g^[0] x
[PROOFSTEP]
rfl
[GOAL]
case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ ∀ (k : ℕ), k < n → f^[k + 1] x ≤ f (f^[k] x)
[PROOFSTEP]
intros
[GOAL]
case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
k✝ : ℕ
a✝ : k✝ < n
⊢ f^[k✝ + 1] x ≤ f (f^[k✝] x)
[PROOFSTEP]
rw [iterate_succ_apply']
[GOAL]
case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ ∀ (k : ℕ), k < n → f (g^[k] x) < g^[k + 1] x
[PROOFSTEP]
intros
[GOAL]
case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
k✝ : ℕ
a✝ : k✝ < n
⊢ f (g^[k✝] x) < g^[k✝ + 1] x
[PROOFSTEP]
simp [h.iterate_right _ _, hg.iterate _ hx]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
⊢ f^[n] x < g^[n] x ↔ f x < g x
[PROOFSTEP]
rcases lt_trichotomy (f x) (g x) with (H | H | H)
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : f x < g x
⊢ f^[n] x < g^[n] x ↔ f x < g x
[PROOFSTEP]
simp only [*, iterate_pos_lt_of_map_lt]
[GOAL]
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : f x = g x
⊢ f^[n] x < g^[n] x ↔ f x < g x
[PROOFSTEP]
simp only [*, h.iterate_eq_of_map_eq, lt_irrefl]
[GOAL]
case inr.inr
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : g x < f x
⊢ f^[n] x < g^[n] x ↔ f x < g x
[PROOFSTEP]
simp only [lt_asymm H, lt_asymm (h.symm.iterate_pos_lt_of_map_lt' hg hf H hn)]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
⊢ f^[n] x ≤ g^[n] x ↔ f x ≤ g x
[PROOFSTEP]
simpa only [not_lt] using not_congr (h.symm.iterate_pos_lt_iff_map_lt' hg hf hn)
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : StrictMono f
hg : Monotone g
x : α
n : ℕ
hn : 0 < n
⊢ f^[n] x ≤ g^[n] x ↔ f x ≤ g x
[PROOFSTEP]
simpa only [not_lt] using not_congr (h.symm.iterate_pos_lt_iff_map_lt hg hf hn)
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
⊢ f^[n] x = g^[n] x ↔ f x = g x
[PROOFSTEP]
simp only [le_antisymm_iff, h.iterate_pos_le_iff_map_le hf hg hn, h.symm.iterate_pos_le_iff_map_le' hg hf hn]
[GOAL]
α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : Monotone f
hx : x ≤ f x
n : ℕ
⊢ f^[n] x ≤ f^[n + 1] x
[PROOFSTEP]
rw [iterate_succ_apply]
[GOAL]
α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : Monotone f
hx : x ≤ f x
n : ℕ
⊢ f^[n] x ≤ f^[n] (f x)
[PROOFSTEP]
exact hf.iterate n hx
[GOAL]
α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : StrictMono f
hx : x < f x
n : ℕ
⊢ f^[n] x < f^[n + 1] x
[PROOFSTEP]
rw [iterate_succ_apply]
[GOAL]
α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : StrictMono f
hx : x < f x
n : ℕ
⊢ f^[n] x < f^[n] (f x)
[PROOFSTEP]
exact hf.iterate n hx
