Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+βCtrl+βto navigate, Ctrl+π±οΈto focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Yury G. Kudryashov

! This file was ported from Lean 3 source module order.iterate
! leanprover-community/mathlib commit 2258b40dacd2942571c8ce136215350c702dc78f
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Logic.Function.Iterate
import Mathlib.Order.Monotone.Basic

/-!
# Inequalities on iterates

In this file we prove some inequalities comparing `f^[n] x` and `g^[n] x` where `f` and `g` are
two self-maps that commute with each other.

Current selection of inequalities is motivated by formalization of the rotation number of
a circle homeomorphism.
-/

open Function

namespace Monotone

variable [Preorder: Type ?u.2419 β Type ?u.2419Preorder Ξ±: ?m.24Ξ±] {f: Ξ± β Ξ±f : Ξ±: ?m.483Ξ± β Ξ±: ?m.2396Ξ±} {x: β β Ξ±x y: β β Ξ±y : β: Typeβ β Ξ±: ?m.4Ξ±}

/-!
### Comparison of two sequences

If \$f\$ is a monotone function, then \$β k, x_{k+1} β€ f(x_k)\$ implies that \$x_k\$ grows slower than
\$f^k(x_0)\$, and similarly for the reversed inequalities. If \$x_k\$ and \$y_k\$ are two sequences such
that \$x_{k+1} β€ f(x_k)\$ and \$y_{k+1} β₯ f(y_k)\$ for all \$k < n\$, then \$x_0 β€ y_0\$ implies
\$x_n β€ y_n\$, see `Monotone.seq_le_seq`.

If some of the inequalities in this lemma are strict, then we have \$x_n < y_n\$. The rest of the
lemmas in this section formalize this fact for different inequalities made strict.
-/

theorem seq_le_seq: β {Ξ± : Type u_1} [inst : Preorder Ξ±] {f : Ξ± β Ξ±} {x y : β β Ξ±},
Monotone f β
β (n : β),
x 0 β€ y 0 β (β (k : β), k < n β x (k + 1) β€ f (x k)) β (β (k : β), k < n β f (y k) β€ y (k + 1)) β x n β€ y nseq_le_seq (hf: Monotone fhf : Monotone: {Ξ± : Type ?u.43} β {Ξ² : Type ?u.42} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropMonotone f: Ξ± β Ξ±f) (n: βn : β: Typeβ) (hβ: x 0 β€ y 0hβ : x: β β Ξ±x 0: ?m.780 β€ y: β β Ξ±y 0: ?m.890) (hx: β (k : β), k < n β x (k + 1) β€ f (x k)hx : β k: ?m.104k < n: βn, x: β β Ξ±x (k: ?m.104k + 1: ?m.1201) β€ f: Ξ± β Ξ±f (x: β β Ξ±x k: ?m.104k))
(hy: β (k : β), k < n β f (y k) β€ y (k + 1)hy : β k: ?m.181k < n: βn, f: Ξ± β Ξ±f (y: β β Ξ±y k: ?m.181k) β€ y: β β Ξ±y (k: ?m.181k + 1: ?m.1941)) : x: β β Ξ±x n: βn β€ y: β β Ξ±y n: βn := byGoals accomplished! π
Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fn: βhβ: x 0 β€ y 0hx: β (k : β), k < n β x (k + 1) β€ f (x k)hy: β (k : β), k < n β f (y k) β€ y (k + 1)x n β€ y ninduction' n: βn with n: βn ihn: ?m.268 nihnΞ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fn: βhβ: x 0 β€ y 0hxβ: β (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)zerox Nat.zero β€ y Nat.zeroΞ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fnβ: βhβ: x 0 β€ y 0hxβ: β (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 nhx: β (k : β), k < Nat.succ n β x (k + 1) β€ f (x k)hy: β (k : β), k < Nat.succ n β f (y k) β€ y (k + 1)succx (Nat.succ n) β€ y (Nat.succ n)
Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fn: βhβ: x 0 β€ y 0hx: β (k : β), k < n β x (k + 1) β€ f (x k)hy: β (k : β), k < n β f (y k) β€ y (k + 1)x n β€ y nΒ·Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fn: βhβ: x 0 β€ y 0hxβ: β (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)zerox Nat.zero β€ y Nat.zero Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fn: βhβ: x 0 β€ y 0hxβ: β (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)zerox Nat.zero β€ y Nat.zeroΞ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fnβ: βhβ: x 0 β€ y 0hxβ: β (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 nhx: β (k : β), k < Nat.succ n β x (k + 1) β€ f (x k)hy: β (k : β), k < Nat.succ n β f (y k) β€ y (k + 1)succx (Nat.succ n) β€ y (Nat.succ n)exact hβ: x 0 β€ y 0hβGoals accomplished! π
Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fn: βhβ: x 0 β€ y 0hx: β (k : β), k < n β x (k + 1) β€ f (x k)hy: β (k : β), k < n β f (y k) β€ y (k + 1)x n β€ y nΒ·Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fnβ: βhβ: x 0 β€ y 0hxβ: β (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 nhx: β (k : β), k < Nat.succ n β x (k + 1) β€ f (x k)hy: β (k : β), k < Nat.succ n β f (y k) β€ y (k + 1)succx (Nat.succ n) β€ y (Nat.succ n) Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fnβ: βhβ: x 0 β€ y 0hxβ: β (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 nhx: β (k : β), k < Nat.succ n β x (k + 1) β€ f (x k)hy: β (k : β), k < Nat.succ n β f (y k) β€ y (k + 1)succx (Nat.succ n) β€ y (Nat.succ n)refine' (hx: β (k : β), k < Nat.succ n β x (k + 1) β€ f (x k)hx _: β_ n: βn.lt_succ_self: β (n : β), n < Nat.succ nlt_succ_self).trans: β {Ξ± : Type ?u.313} [inst : Preorder Ξ±] {a b c : Ξ±}, a β€ b β b β€ c β a β€ ctrans ((hf: Monotone fhf \$ ihn: ?m.268 nihn _: β (k : β), k < n β x (k + 1) β€ f (x k)_ _: β (k : β), k < n β f (y k) β€ y (k + 1)_).trans: β {Ξ± : Type ?u.336} [inst : Preorder Ξ±] {a b c : Ξ±}, a β€ b β b β€ c β a β€ ctrans (hy: β (k : β), k < Nat.succ n β f (y k) β€ y (k + 1)hy _: β_ n: βn.lt_succ_self: β (n : β), n < Nat.succ nlt_succ_self))Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fnβ: βhβ: x 0 β€ y 0hxβ: β (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 nhx: β (k : β), k < Nat.succ n β x (k + 1) β€ f (x k)hy: β (k : β), k < Nat.succ n β f (y k) β€ y (k + 1)succ.refine'_1β (k : β), k < n β x (k + 1) β€ f (x k)Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fnβ: βhβ: x 0 β€ y 0hxβ: β (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 nhx: β (k : β), k < Nat.succ n β x (k + 1) β€ f (x k)hy: β (k : β), k < Nat.succ n β f (y k) β€ y (k + 1)succ.refine'_2β (k : β), k < n β f (y k) β€ y (k + 1)
Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fnβ: βhβ: x 0 β€ y 0hxβ: β (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 nhx: β (k : β), k < Nat.succ n β x (k + 1) β€ f (x k)hy: β (k : β), k < Nat.succ n β f (y k) β€ y (k + 1)succx (Nat.succ n) β€ y (Nat.succ n)exact fun k: ?m.353k hk: ?m.356hk => hx: β (k : β), k < Nat.succ n β x (k + 1) β€ f (x k)hx _: β_ (hk: ?m.356hk.trans: β {Ξ± : Type ?u.359} [inst : Preorder Ξ±] {a b c : Ξ±}, a < b β b < c β a < ctrans n: βn.lt_succ_self: β (n : β), n < Nat.succ nlt_succ_self)Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fnβ: βhβ: x 0 β€ y 0hxβ: β (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 nhx: β (k : β), k < Nat.succ n β x (k + 1) β€ f (x k)hy: β (k : β), k < Nat.succ n β f (y k) β€ y (k + 1)succ.refine'_2β (k : β), k < n β f (y k) β€ y (k + 1)
Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fnβ: βhβ: x 0 β€ y 0hxβ: β (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 nhx: β (k : β), k < Nat.succ n β x (k + 1) β€ f (x k)hy: β (k : β), k < Nat.succ n β f (y k) β€ y (k + 1)succx (Nat.succ n) β€ y (Nat.succ n)exact fun k: ?m.388k hk: ?m.391hk => hy: β (k : β), k < Nat.succ n β f (y k) β€ y (k + 1)hy _: β_ (hk: ?m.391hk.trans: β {Ξ± : Type ?u.394} [inst : Preorder Ξ±] {a b c : Ξ±}, a < b β b < c β a < ctrans n: βn.lt_succ_self: β (n : β), n < Nat.succ nlt_succ_self)Goals accomplished! π
#align monotone.seq_le_seq Monotone.seq_le_seq: β {Ξ± : Type u_1} [inst : Preorder Ξ±] {f : Ξ± β Ξ±} {x y : β β Ξ±},
Monotone f β
β (n : β),
x 0 β€ y 0 β (β (k : β), k < n β x (k + 1) β€ f (x k)) β (β (k : β), k < n β f (y k) β€ y (k + 1)) β x n β€ y nMonotone.seq_le_seq

theorem seq_pos_lt_seq_of_lt_of_le: β {Ξ± : Type u_1} [inst : Preorder Ξ±] {f : Ξ± β Ξ±} {x y : β β Ξ±},
Monotone f β
β {n : β},
0 < n β
x 0 β€ y 0 β (β (k : β), k < n β x (k + 1) < f (x k)) β (β (k : β), k < n β f (y k) β€ y (k + 1)) β x n < y nseq_pos_lt_seq_of_lt_of_le (hf: Monotone fhf : Monotone: {Ξ± : Type ?u.502} β {Ξ² : Type ?u.501} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropMonotone f: Ξ± β Ξ±f) {n: βn : β: Typeβ} (hn: 0 < nhn : 0: ?m.5370 < n: βn) (hβ: x 0 β€ y 0hβ : x: β β Ξ±x 0: ?m.5740 β€ y: β β Ξ±y 0: ?m.5770)
(hx: β (k : β), k < n β x (k + 1) < f (x k)hx : β k: ?m.592k < n: βn, x: β β Ξ±x (k: ?m.592k + 1: ?m.6051) < f: Ξ± β Ξ±f (x: β β Ξ±x k: ?m.592k)) (hy: β (k : β), k < n β f (y k) β€ y (k + 1)hy : β k: ?m.673k < n: βn, f: Ξ± β Ξ±f (y: β β Ξ±y k: ?m.673k) β€ y: β β Ξ±y (k: ?m.673k + 1: ?m.6861)) : x: β β Ξ±x n: βn < y: β β Ξ±y n: βn := byGoals accomplished! π
Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fn: βhn: 0 < nhβ: x 0 β€ y 0hx: β (k : β), k < n β x (k + 1) < f (x k)hy: β (k : β), k < n β f (y k) β€ y (k + 1)x n < y ninduction' n: βn with n: βn ihn: ?m.762 nihnΞ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fn: βhnβ: 0 < nhβ: x 0 β€ y 0hxβ: β (k : β), k < n β x (k + 1) < f (x k)hyβ: β (k : β), k < n β f (y k) β€ y (k + 1)hn: 0 < Nat.zerohx: β (k : β), k < Nat.zero β x (k + 1) < f (x k)hy: β (k : β), k < Nat.zero β f (y k) β€ y (k + 1)zerox Nat.zero < y Nat.zeroΞ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fnβ: βhnβ: 0 < nβhβ: x 0 β€ y 0hxβ: β (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 nhn: 0 < Nat.succ nhx: β (k : β), k < Nat.succ n β x (k + 1) < f (x k)hy: β (k : β), k < Nat.succ n β f (y k) β€ y (k + 1)succx (Nat.succ n) < y (Nat.succ n)
Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fn: βhn: 0 < nhβ: x 0 β€ y 0hx: β (k : β), k < n β x (k + 1) < f (x k)hy: β (k : β), k < n β f (y k) β€ y (k + 1)x n < y nΒ·Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fn: βhnβ: 0 < nhβ: x 0 β€ y 0hxβ: β (k : β), k < n β x (k + 1) < f (x k)hyβ: β (k : β), k < n β f (y k) β€ y (k + 1)hn: 0 < Nat.zerohx: β (k : β), k < Nat.zero β x (k + 1) < f (x k)hy: β (k : β), k < Nat.zero β f (y k) β€ y (k + 1)zerox Nat.zero < y Nat.zero Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fn: βhnβ: 0 < nhβ: x 0 β€ y 0hxβ: β (k : β), k < n β x (k + 1) < f (x k)hyβ: β (k : β), k < n β f (y k) β€ y (k + 1)hn: 0 < Nat.zerohx: β (k : β), k < Nat.zero β x (k + 1) < f (x k)hy: β (k : β), k < Nat.zero β f (y k) β€ y (k + 1)zerox Nat.zero < y Nat.zeroΞ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fnβ: βhnβ: 0 < nβhβ: x 0 β€ y 0hxβ: β (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 nhn: 0 < Nat.succ nhx: β (k : β), k < Nat.succ n β x (k + 1) < f (x k)hy: β (k : β), k < Nat.succ n β f (y k) β€ y (k + 1)succx (Nat.succ n) < y (Nat.succ n)exact hn: 0 < Nat.zerohn.false: β {Ξ± : Type ?u.800} [inst : Preorder Ξ±] {x : Ξ±}, x < x β Falsefalse.elim: β {C : Sort ?u.820}, False β CelimGoals accomplished! π
Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fn: βhn: 0 < nhβ: x 0 β€ y 0hx: β (k : β), k < n β x (k + 1) < f (x k)hy: β (k : β), k < n β f (y k) β€ y (k + 1)x n < y nsuffices x: β β Ξ±x n: βn β€ y: β β Ξ±y n: βn from (hx: β (k : β), k < Nat.succ n β x (k + 1) < f (x k)hx n: βn n: βn.lt_succ_self: β (n : β), n < Nat.succ nlt_succ_self).trans_le: β {Ξ± : Type ?u.840} [inst : Preorder Ξ±] {a b c : Ξ±}, a < b β b β€ c β a < ctrans_le ((hf: Monotone fhf this: x n β€ y nthis).trans: β {Ξ± : Type ?u.866} [inst : Preorder Ξ±] {a b c : Ξ±}, a β€ b β b β€ c β a β€ ctrans \$ hy: β (k : β), k < Nat.succ n β f (y k) β€ y (k + 1)hy n: βn n: βn.lt_succ_self: β (n : β), n < Nat.succ nlt_succ_self)Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fnβ: βhnβ: 0 < nβhβ: x 0 β€ y 0hxβ: β (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 nhn: 0 < Nat.succ nhx: β (k : β), k < Nat.succ n β x (k + 1) < f (x k)hy: β (k : β), k < Nat.succ n β f (y k) β€ y (k + 1)succx n β€ y n
Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fn: βhn: 0 < nhβ: x 0 β€ y 0hx: β (k : β), k < n β x (k + 1) < f (x k)hy: β (k : β), k < n β f (y k) β€ y (k + 1)x n < y ncases n: βn with
Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fnβ: βhnβ: 0 < nβhβ: x 0 β€ y 0hxβ: β (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 nhn: 0 < Nat.succ nhx: β (k : β), k < Nat.succ n β x (k + 1) < f (x k)hy: β (k : β), k < Nat.succ n β f (y k) β€ y (k + 1)succx n β€ y n| zero: βzero => Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fn: βhnβ: 0 < nhβ: x 0 β€ y 0hxβ: β (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.zerohn: 0 < Nat.succ Nat.zerohx: β (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)succ.zerox Nat.zero β€ y Nat.zeroexact hβ: x 0 β€ y 0hβGoals accomplished! π
Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fnβ: βhnβ: 0 < nβhβ: x 0 β€ y 0hxβ: β (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 nhn: 0 < Nat.succ nhx: β (k : β), k < Nat.succ n β x (k + 1) < f (x k)hy: β (k : β), k < Nat.succ n β f (y k) β€ y (k + 1)succx n β€ y n| succ: β β βsucc n: βn =>
Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fnβ: βhnβ: 0 < nβhβ: x 0 β€ y 0hxβ: β (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)succ.succx (Nat.succ n) β€ y (Nat.succ n)refine' (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)ihn n: βn.zero_lt_succ: β (n : β), 0 < Nat.succ nzero_lt_succ (fun k: ?m.990k hk: ?m.993hk => hx: β (k : β), k < Nat.succ (Nat.succ n) β x (k + 1) < f (x k)hx _: β_ _: ?m.995 < Nat.succ (Nat.succ n)_) fun k: ?m.1002k hk: ?m.1005hk => hy: β (k : β), k < Nat.succ (Nat.succ n) β f (y k) β€ y (k + 1)hy _: β_ _: ?m.1007 < Nat.succ (Nat.succ n)_).le: β {Ξ± : Type ?u.1012} [inst : Preorder Ξ±] {a b : Ξ±}, a < b β a β€ bleΞ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fnβ: βhnβ: 0 < nβhβ: x 0 β€ y 0hxβ: β (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 nsucc.succ.refine'_1k < Nat.succ (Nat.succ n)Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fnβ: βhnβ: 0 < nβhβ: x 0 β€ y 0hxβ: β (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 nsucc.succ.refine'_2k < Nat.succ (Nat.succ n) Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fnβ: βhnβ: 0 < nβhβ: x 0 β€ y 0hxβ: β (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)succ.succx (Nat.succ n) β€ y (Nat.succ n)<;>Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fnβ: βhnβ: 0 < nβhβ: x 0 β€ y 0hxβ: β (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 nsucc.succ.refine'_1k < Nat.succ (Nat.succ n)Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fnβ: βhnβ: 0 < nβhβ: x 0 β€ y 0hxβ: β (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 nsucc.succ.refine'_2k < Nat.succ (Nat.succ n)
Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fnβ: βhnβ: 0 < nβhβ: x 0 β€ y 0hxβ: β (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)succ.succx (Nat.succ n) β€ y (Nat.succ n)exact hk: ?m.993hk.trans: β {Ξ± : Type ?u.1022} [inst : Preorder Ξ±] {a b c : Ξ±}, a < b β b < c β a < ctrans n: βn.succ: β β βsucc.lt_succ_self: β (n : β), n < Nat.succ nlt_succ_selfGoals accomplished! π
#align monotone.seq_pos_lt_seq_of_lt_of_le Monotone.seq_pos_lt_seq_of_lt_of_le: β {Ξ± : Type u_1} [inst : Preorder Ξ±] {f : Ξ± β Ξ±} {x y : β β Ξ±},
Monotone f β
β {n : β},
0 < n β
x 0 β€ y 0 β (β (k : β), k < n β x (k + 1) < f (x k)) β (β (k : β), k < n β f (y k) β€ y (k + 1)) β x n < y nMonotone.seq_pos_lt_seq_of_lt_of_le

theorem seq_pos_lt_seq_of_le_of_lt: Monotone f β
β {n : β},
0 < n β x 0 β€ y 0 β (β (k : β), k < n β x (k + 1) β€ f (x k)) β (β (k : β), k < n β f (y k) < y (k + 1)) β x n < y nseq_pos_lt_seq_of_le_of_lt (hf: Monotone fhf : Monotone: {Ξ± : Type ?u.1229} β {Ξ² : Type ?u.1228} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropMonotone f: Ξ± β Ξ±f) {n: βn : β: Typeβ} (hn: 0 < nhn : 0: ?m.12640 < n: βn) (hβ: x 0 β€ y 0hβ : x: β β Ξ±x 0: ?m.13010 β€ y: β β Ξ±y 0: ?m.13040)
(hx: β (k : β), k < n β x (k + 1) β€ f (x k)hx : β k: ?m.1319k < n: βn, x: β β Ξ±x (k: ?m.1319k + 1: ?m.13321) β€ f: Ξ± β Ξ±f (x: β β Ξ±x k: ?m.1319k)) (hy: β (k : β), k < n β f (y k) < y (k + 1)hy : β k: ?m.1393k < n: βn, f: Ξ± β Ξ±f (y: β β Ξ±y k: ?m.1393k) < y: β β Ξ±y (k: ?m.1393k + 1: ?m.14061)) : x: β β Ξ±x n: βn < y: β β Ξ±y n: βn :=
hf: Monotone fhf.dual: β {Ξ± : Type ?u.1475} {Ξ² : Type ?u.1474} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {f : Ξ± β Ξ²},
Monotone f β Monotone (βOrderDual.toDual β f β βOrderDual.ofDual)dual.seq_pos_lt_seq_of_lt_of_le: β {Ξ± : Type ?u.1492} [inst : Preorder Ξ±] {f : Ξ± β Ξ±} {x y : β β Ξ±},
Monotone f β
β {n : β},
0 < n β
x 0 β€ y 0 β (β (k : β), k < n β x (k + 1) < f (x k)) β (β (k : β), k < n β f (y k) β€ y (k + 1)) β x n < y nseq_pos_lt_seq_of_lt_of_le hn: 0 < nhn hβ: x 0 β€ y 0hβ hy: β (k : β), k < n β f (y k) < y (k + 1)hy hx: β (k : β), k < n β x (k + 1) β€ f (x k)hx
#align monotone.seq_pos_lt_seq_of_le_of_lt Monotone.seq_pos_lt_seq_of_le_of_lt: β {Ξ± : Type u_1} [inst : Preorder Ξ±] {f : Ξ± β Ξ±} {x y : β β Ξ±},
Monotone f β
β {n : β},
0 < n β
x 0 β€ y 0 β (β (k : β), k < n β x (k + 1) β€ f (x k)) β (β (k : β), k < n β f (y k) < y (k + 1)) β x n < y nMonotone.seq_pos_lt_seq_of_le_of_lt

theorem seq_lt_seq_of_lt_of_le: Monotone f β
β (n : β), x 0 < y 0 β (β (k : β), k < n β x (k + 1) < f (x k)) β (β (k : β), k < n β f (y k) β€ y (k + 1)) β x n < y nseq_lt_seq_of_lt_of_le (hf: Monotone fhf : Monotone: {Ξ± : Type ?u.1600} β {Ξ² : Type ?u.1599} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropMonotone f: Ξ± β Ξ±f) (n: βn : β: Typeβ) (hβ: x 0 < y 0hβ : x: β β Ξ±x 0: ?m.16350 < y: β β Ξ±y 0: ?m.16460)
(hx: β (k : β), k < n β x (k + 1) < f (x k)hx : β k: ?m.1661k < n: βn, x: β β Ξ±x (k: ?m.1661k + 1: ?m.16771) < f: Ξ± β Ξ±f (x: β β Ξ±x k: ?m.1661k)) (hy: β (k : β), k < n β f (y k) β€ y (k + 1)hy : β k: ?m.1738k < n: βn, f: Ξ± β Ξ±f (y: β β Ξ±y k: ?m.1738k) β€ y: β β Ξ±y (k: ?m.1738k + 1: ?m.17511)) : x: β β Ξ±x n: βn < y: β β Ξ±y n: βn := byGoals accomplished! π
Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fn: βhβ: x 0 < y 0hx: β (k : β), k < n β x (k + 1) < f (x k)hy: β (k : β), k < n β f (y k) β€ y (k + 1)x n < y ncases n: βnΞ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fhβ: x 0 < y 0hx: β (k : β), k < Nat.zero β x (k + 1) < f (x k)hy: β (k : β), k < Nat.zero β f (y k) β€ y (k + 1)zerox Nat.zero < y Nat.zeroΞ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fhβ: x 0 < y 0nβ: βhx: β (k : β), k < Nat.succ nβ β x (k + 1) < f (x k)hy: β (k : β), k < Nat.succ nβ β f (y k) β€ y (k + 1)succx (Nat.succ nβ) < y (Nat.succ nβ)
Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±x, y: β β Ξ±hf: Monotone fn: βhβ: x 0 < y 0hx: β (k : β), k < n β x (k + 1) < f (x k)hy: β (k : β), k < n β f (y k) β€ y (k + 1)x n < y nexacts[hβ: x 0 < y 0hβ, hf: Monotone fhf.seq_pos_lt_seq_of_lt_of_le: β {Ξ± : Type ?u.1898} [inst : Preorder Ξ±] {f : Ξ± β Ξ±} {x y : β β Ξ±},
Monotone f β
β {n : β},
0 < n β
x 0 β€ y 0 β (β (k : β), k < n β x (k + 1) < f (x k)) β (β (k : β), k < n β f (y k) β€ y (k + 1)) β x n < y nseq_pos_lt_seq_of_lt_of_le (Nat.zero_lt_succ: β (n : β), 0 < Nat.succ nNat.zero_lt_succ _: β_) hβ: x 0 < y 0hβ.le: β {Ξ± : Type ?u.1941} [inst : Preorder Ξ±] {a b : Ξ±}, a < b β a β€ ble hx: β (k : β), k < Nat.succ nβ β x (k + 1) < f (x k)hx hy: β (k : β), k < Nat.succ nβ β f (y k) β€ y (k + 1)hy]Goals accomplished! π
#align monotone.seq_lt_seq_of_lt_of_le Monotone.seq_lt_seq_of_lt_of_le: β {Ξ± : Type u_1} [inst : Preorder Ξ±] {f : Ξ± β Ξ±} {x y : β β Ξ±},
Monotone f β
β (n : β),
x 0 < y 0 β (β (k : β), k < n β x (k + 1) < f (x k)) β (β (k : β), k < n β f (y k) β€ y (k + 1)) β x n < y nMonotone.seq_lt_seq_of_lt_of_le

theorem seq_lt_seq_of_le_of_lt: Monotone f β
β (n : β), x 0 < y 0 β (β (k : β), k < n β x (k + 1) β€ f (x k)) β (β (k : β), k < n β f (y k) < y (k + 1)) β x n < y nseq_lt_seq_of_le_of_lt (hf: Monotone fhf : Monotone: {Ξ± : Type ?u.2042} β {Ξ² : Type ?u.2041} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropMonotone f: Ξ± β Ξ±f) (n: βn : β: Typeβ) (hβ: x 0 < y 0hβ : x: β β Ξ±x 0: ?m.20770 < y: β β Ξ±y 0: ?m.20880)
(hx: β (k : β), k < n β x (k + 1) β€ f (x k)hx : β k: ?m.2103k < n: βn, x: β β Ξ±x (k: ?m.2103k + 1: ?m.21191) β€ f: Ξ± β Ξ±f (x: β β Ξ±x k: ?m.2103k)) (hy: β (k : β), k < n β f (y k) < y (k + 1)hy : β k: ?m.2187k < n: βn, f: Ξ± β Ξ±f (y: β β Ξ±y k: ?m.2187k) < y: β β Ξ±y (k: ?m.2187k + 1: ?m.22001)) : x: β β Ξ±x n: βn < y: β β Ξ±y n: βn :=
hf: Monotone fhf.dual: β {Ξ± : Type ?u.2260} {Ξ² : Type ?u.2259} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {f : Ξ± β Ξ²},
Monotone f β Monotone (βOrderDual.toDual β f β βOrderDual.ofDual)dual.seq_lt_seq_of_lt_of_le: β {Ξ± : Type ?u.2277} [inst : Preorder Ξ±] {f : Ξ± β Ξ±} {x y : β β Ξ±},
Monotone f β
β (n : β),
x 0 < y 0 β (β (k : β), k < n β x (k + 1) < f (x k)) β (β (k : β), k < n β f (y k) β€ y (k + 1)) β x n < y nseq_lt_seq_of_lt_of_le n: βn hβ: x 0 < y 0hβ hy: β (k : β), k < n β f (y k) < y (k + 1)hy hx: β (k : β), k < n β x (k + 1) β€ f (x k)hx
#align monotone.seq_lt_seq_of_le_of_lt Monotone.seq_lt_seq_of_le_of_lt: β {Ξ± : Type u_1} [inst : Preorder Ξ±] {f : Ξ± β Ξ±} {x y : β β Ξ±},
Monotone f β
β (n : β),
x 0 < y 0 β (β (k : β), k < n β x (k + 1) β€ f (x k)) β (β (k : β), k < n β f (y k) < y (k + 1)) β x n < y nMonotone.seq_lt_seq_of_le_of_lt

/-!
### Iterates of two functions

In this section we compare the iterates of a monotone function `f : Ξ± β Ξ±` to iterates of any
function `g : Ξ² β Ξ²`. If `h : Ξ² β Ξ±` satisfies `h β g β€ f β h`, then `h (g^[n] x)` grows slower
than `f^[n] (h x)`, and similarly for the reversed inequality.

Then we specialize these two lemmas to the case `Ξ² = Ξ±`, `h = id`.
-/

variable {g: Ξ² β Ξ²g : Ξ²: ?m.2383Ξ² β Ξ²: ?m.2383Ξ²} {h: Ξ² β Ξ±h : Ξ²: ?m.2383Ξ² β Ξ±: ?m.2363Ξ±}

open Function

theorem le_iterate_comp_of_le: β {Ξ± : Type u_1} {Ξ² : Type u_2} [inst : Preorder Ξ±] {f : Ξ± β Ξ±} {g : Ξ² β Ξ²} {h : Ξ² β Ξ±},
Monotone f β h β g β€ f β h β β (n : β), h β g^[n] β€ f^[n] β hle_iterate_comp_of_le (hf: Monotone fhf : Monotone: {Ξ± : Type ?u.2443} β {Ξ² : Type ?u.2442} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropMonotone f: Ξ± β Ξ±f) (H: h β g β€ f β hH : h: Ξ² β Ξ±h β g: Ξ² β Ξ²g β€ f: Ξ± β Ξ±f β h: Ξ² β Ξ±h) (n: βn : β: Typeβ) :
h: Ξ² β Ξ±h β g: Ξ² β Ξ²g^[n: βn] β€ f: Ξ± β Ξ±f^[n: βn] β h: Ξ² β Ξ±h := fun x: ?m.2625x => byGoals accomplished! π
Ξ±: Type u_1Ξ²: Type u_2instβ: Preorder Ξ±f: Ξ± β Ξ±xβ, y: β β Ξ±g: Ξ² β Ξ²h: Ξ² β Ξ±hf: Monotone fH: h β g β€ f β hn: βx: Ξ²(h β g^[n]) x β€ (f^[n] β h) xapply hf: Monotone fhf.seq_le_seq: β {Ξ± : Type ?u.2631} [inst : Preorder Ξ±] {f : Ξ± β Ξ±} {x y : β β Ξ±},
Monotone f β
β (n : β),
x 0 β€ y 0 β (β (k : β), k < n β x (k + 1) β€ f (x k)) β (β (k : β), k < n β f (y k) β€ y (k + 1)) β x n β€ y nseq_le_seq n: βnΞ±: Type u_1Ξ²: Type u_2instβ: Preorder Ξ±f: Ξ± β Ξ±xβ, y: β β Ξ±g: Ξ² β Ξ²h: Ξ² β Ξ±hf: Monotone fH: h β g β€ f β hn: βx: Ξ²hβ(h β g^[0]) x β€ (f^[0] β h) xΞ±: Type u_1Ξ²: Type u_2instβ: Preorder Ξ±f: Ξ± β Ξ±xβ, y: β β Ξ±g: Ξ² β Ξ²h: Ξ² β Ξ±hf: Monotone fH: h β g β€ f β hn: βx: Ξ²hxβ (k : β), k < n β (h β g^[k + 1]) x β€ f ((h β g^[k]) x)Ξ±: Type u_1Ξ²: Type u_2instβ: Preorder Ξ±f: Ξ± β Ξ±xβ, y: β β Ξ±g: Ξ² β Ξ²h: Ξ² β Ξ±hf: Monotone fH: h β g β€ f β hn: βx: Ξ²hyβ (k : β), k < n β f ((f^[k] β h) x) β€ (f^[k + 1] β h) x Ξ±: Type u_1Ξ²: Type u_2instβ: Preorder Ξ±f: Ξ± β Ξ±xβ, y: β β Ξ±g: Ξ² β Ξ²h: Ξ² β Ξ±hf: Monotone fH: h β g β€ f β hn: βx: Ξ²(h β g^[n]) x β€ (f^[n] β h) x<;>Ξ±: Type u_1Ξ²: Type u_2instβ: Preorder Ξ±f: Ξ± β Ξ±xβ, y: β β Ξ±g: Ξ² β Ξ²h: Ξ² β Ξ±hf: Monotone fH: h β g β€ f β hn: βx: Ξ²hβ(h β g^[0]) x β€ (f^[0] β h) xΞ±: Type u_1Ξ²: Type u_2instβ: Preorder Ξ±f: Ξ± β Ξ±xβ, y: β β Ξ±g: Ξ² β Ξ²h: Ξ² β Ξ±hf: Monotone fH: h β g β€ f β hn: βx: Ξ²hxβ (k : β), k < n β (h β g^[k + 1]) x β€ f ((h β g^[k]) x)Ξ±: Type u_1Ξ²: Type u_2instβ: Preorder Ξ±f: Ξ± β Ξ±xβ, y: β β Ξ±g: Ξ² β Ξ²h: Ξ² β Ξ±hf: Monotone fH: h β g β€ f β hn: βx: Ξ²hyβ (k : β), k < n β f ((f^[k] β h) x) β€ (f^[k + 1] β h) x Ξ±: Type u_1Ξ²: Type u_2instβ: Preorder Ξ±f: Ξ± β Ξ±xβ, y: β β Ξ±g: Ξ² β Ξ²h: Ξ² β Ξ±hf: Monotone fH: h β g β€ f β hn: βx: Ξ²(h β g^[n]) x β€ (f^[n] β h) xintrosΞ±: Type u_1Ξ²: Type u_2instβ: Preorder Ξ±f: Ξ± β Ξ±xβ, y: β β Ξ±g: Ξ² β Ξ²h: Ξ² β Ξ±hf: Monotone fH: h β g β€ f β hn: βx: Ξ²kβ: βaβ: kβ < nhyf ((f^[kβ] β h) x) β€ (f^[kβ + 1] β h) x Ξ±: Type u_1Ξ²: Type u_2instβ: Preorder Ξ±f: Ξ± β Ξ±xβ, y: β β Ξ±g: Ξ² β Ξ²h: Ξ² β Ξ±hf: Monotone fH: h β g β€ f β hn: βx: Ξ²(h β g^[n]) x β€ (f^[n] β h) x<;>Ξ±: Type u_1Ξ²: Type u_2instβ: Preorder Ξ±f: Ξ± β Ξ±xβ, y: β β Ξ±g: Ξ² β Ξ²h: Ξ² β Ξ±hf: Monotone fH: h β g β€ f β hn: βx: Ξ²hβ(h β g^[0]) x β€ (f^[0] β h) xΞ±: Type u_1Ξ²: Type u_2instβ: Preorder Ξ±f: Ξ± β Ξ±xβ, y: β β Ξ±g: Ξ² β Ξ²h: Ξ² β Ξ±hf: Monotone fH: h β g β€ f β hn: βx: Ξ²kβ: βaβ: kβ < nhx(h β g^[kβ + 1]) x β€ f ((h β g^[kβ]) x)Ξ±: Type u_1Ξ²: Type u_2instβ: Preorder Ξ±f: Ξ± β Ξ±xβ, y: β β Ξ±g: Ξ² β Ξ²h: Ξ² β Ξ±hf: Monotone fH: h β g β€ f β hn: βx: Ξ²kβ: βaβ: kβ < nhyf ((f^[kβ] β h) x) β€ (f^[kβ + 1] β h) x
Ξ±: Type u_1Ξ²: Type u_2instβ: Preorder Ξ±f: Ξ± β Ξ±xβ, y: β β Ξ±g: Ξ² β Ξ²h: Ξ² β Ξ±hf: Monotone fH: h β g β€ f β hn: βx: Ξ²(h β g^[n]) x β€ (f^[n] β h) xsimp [iterate_succ': β {Ξ± : Type ?u.3311} (f : Ξ± β Ξ±) (n : β), f^[Nat.succ n] = f β f^[n]iterate_succ', -iterate_succ: β {Ξ± : Type u} (f : Ξ± β Ξ±) (n : β), f^[Nat.succ n] = f^[n] β fiterate_succ, comp_apply: β {Ξ² : Sort ?u.2974} {Ξ΄ : Sort ?u.2975} {Ξ± : Sort ?u.2976} {f : Ξ² β Ξ΄} {g : Ξ± β Ξ²} {x : Ξ±}, (f β g) x = f (g x)comp_apply, id_eq: β {Ξ± : Sort ?u.3335} (a : Ξ±), id a = aid_eq, le_refl: β {Ξ± : Type ?u.3341} [inst : Preorder Ξ±] (a : Ξ±), a β€ ale_refl]Ξ±: Type u_1Ξ²: Type u_2instβ: Preorder Ξ±f: Ξ± β Ξ±xβ, y: β β Ξ±g: Ξ² β Ξ²h: Ξ² β Ξ±hf: Monotone fH: h β g β€ f β hn: βx: Ξ²kβ: βaβ: kβ < nhxh (g ((g^[kβ]) x)) β€ f (h ((g^[kβ]) x))
Ξ±: Type u_1Ξ²: Type u_2instβ: Preorder Ξ±f: Ξ± β Ξ±xβ, y: β β Ξ±g: Ξ² β Ξ²h: Ξ² β Ξ±hf: Monotone fH: h β g β€ f β hn: βx: Ξ²(h β g^[n]) x β€ (f^[n] β h) xcase hx => Ξ±: Type u_1Ξ²: Type u_2instβ: Preorder Ξ±f: Ξ± β Ξ±xβ, y: β β Ξ±g: Ξ² β Ξ²h: Ξ² β Ξ±hf: Monotone fH: h β g β€ f β hn: βx: Ξ²kβ: βaβ: kβ < nh (g ((g^[kβ]) x)) β€ f (h ((g^[kβ]) x))exact H: h β g β€ f β hH _: Ξ²_Goals accomplished! π
#align monotone.le_iterate_comp_of_le Monotone.le_iterate_comp_of_le: β {Ξ± : Type u_1} {Ξ² : Type u_2} [inst : Preorder Ξ±] {f : Ξ± β Ξ±} {g : Ξ² β Ξ²} {h : Ξ² β Ξ±},
Monotone f β h β g β€ f β h β β (n : β), h β g^[n] β€ f^[n] β hMonotone.le_iterate_comp_of_le

theorem iterate_comp_le_of_le: β {Ξ± : Type u_1} {Ξ² : Type u_2} [inst : Preorder Ξ±] {f : Ξ± β Ξ±} {g : Ξ² β Ξ²} {h : Ξ² β Ξ±},
Monotone f β f β h β€ h β g β β (n : β), f^[n] β h β€ h β g^[n]iterate_comp_le_of_le (hf: Monotone fhf : Monotone: {Ξ± : Type ?u.3598} β {Ξ² : Type ?u.3597} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropMonotone f: Ξ± β Ξ±f) (H: f β h β€ h β gH : f: Ξ± β Ξ±f β h: Ξ² β Ξ±h β€ h: Ξ² β Ξ±h β g: Ξ² β Ξ²g) (n: βn : β: Typeβ) :
f: Ξ± β Ξ±f^[n: βn] β h: Ξ² β Ξ±h β€ h: Ξ² β Ξ±h β g: Ξ² β Ξ²g^[n: βn] :=
hf: Monotone fhf.dual: β {Ξ± : Type ?u.3780} {Ξ² : Type ?u.3779} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {f : Ξ± β Ξ²},
Monotone f β Monotone (βOrderDual.toDual β f β βOrderDual.ofDual)dual.le_iterate_comp_of_le: β {Ξ± : Type ?u.3797} {Ξ² : Type ?u.3798} [inst : Preorder Ξ±] {f : Ξ± β Ξ±} {g : Ξ² β Ξ²} {h : Ξ² β Ξ±},
Monotone f β h β g β€ f β h β β (n : β), h β g^[n] β€ f^[n] β hle_iterate_comp_of_le H: f β h β€ h β gH n: βn
#align monotone.iterate_comp_le_of_le Monotone.iterate_comp_le_of_le: β {Ξ± : Type u_1} {Ξ² : Type u_2} [inst : Preorder Ξ±] {f : Ξ± β Ξ±} {g : Ξ² β Ξ²} {h : Ξ² β Ξ±},
Monotone f β f β h β€ h β g β β (n : β), f^[n] β h β€ h β g^[n]Monotone.iterate_comp_le_of_le

/-- If `f β€ g` and `f` is monotone, then `f^[n] β€ g^[n]`. -/
theorem iterate_le_of_le: β {g : Ξ± β Ξ±}, Monotone f β f β€ g β β (n : β), f^[n] β€ g^[n]iterate_le_of_le {g: Ξ± β Ξ±g : Ξ±: ?m.3913Ξ± β Ξ±: ?m.3913Ξ±} (hf: Monotone fhf : Monotone: {Ξ± : Type ?u.3964} β {Ξ² : Type ?u.3963} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropMonotone f: Ξ± β Ξ±f) (h: f β€ gh : f: Ξ± β Ξ±f β€ g: Ξ± β Ξ±g) (n: βn : β: Typeβ) : f: Ξ± β Ξ±f^[n: βn] β€ g: Ξ± β Ξ±g^[n: βn] :=
hf: Monotone fhf.iterate_comp_le_of_le: β {Ξ± : Type ?u.4061} {Ξ² : Type ?u.4062} [inst : Preorder Ξ±] {f : Ξ± β Ξ±} {g : Ξ² β Ξ²} {h : Ξ² β Ξ±},
Monotone f β f β h β€ h β g β β (n : β), f^[n] β h β€ h β g^[n]iterate_comp_le_of_le h: f β€ gh n: βn
#align monotone.iterate_le_of_le Monotone.iterate_le_of_le: β {Ξ± : Type u_1} [inst : Preorder Ξ±] {f g : Ξ± β Ξ±}, Monotone f β f β€ g β β (n : β), f^[n] β€ g^[n]Monotone.iterate_le_of_le

/-- If `f β€ g` and `g` is monotone, then `f^[n] β€ g^[n]`. -/
theorem le_iterate_of_le: β {g : Ξ± β Ξ±}, Monotone g β f β€ g β β (n : β), f^[n] β€ g^[n]le_iterate_of_le {g: Ξ± β Ξ±g : Ξ±: ?m.4158Ξ± β Ξ±: ?m.4158Ξ±} (hg: Monotone ghg : Monotone: {Ξ± : Type ?u.4209} β {Ξ² : Type ?u.4208} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropMonotone g: Ξ± β Ξ±g) (h: f β€ gh : f: Ξ± β Ξ±f β€ g: Ξ± β Ξ±g) (n: βn : β: Typeβ) : f: Ξ± β Ξ±f^[n: βn] β€ g: Ξ± β Ξ±g^[n: βn] :=
hg: Monotone ghg.dual: β {Ξ± : Type ?u.4307} {Ξ² : Type ?u.4306} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {f : Ξ± β Ξ²},
Monotone f β Monotone (βOrderDual.toDual β f β βOrderDual.ofDual)dual.iterate_le_of_le: β {Ξ± : Type ?u.4324} [inst : Preorder Ξ±] {f g : Ξ± β Ξ±}, Monotone f β f β€ g β β (n : β), f^[n] β€ g^[n]iterate_le_of_le h: f β€ gh n: βn
#align monotone.le_iterate_of_le Monotone.le_iterate_of_le: β {Ξ± : Type u_1} [inst : Preorder Ξ±] {f g : Ξ± β Ξ±}, Monotone g β f β€ g β β (n : β), f^[n] β€ g^[n]Monotone.le_iterate_of_le

end Monotone

/-!
### Comparison of iterations and the identity function

If \$f(x) β€ x\$ for all \$x\$ (we express this as `f β€ id` in the code), then the same is true for
any iterate of \$f\$, and similarly for the reversed inequality.
-/

namespace Function

section Preorder

variable [Preorder: Type ?u.4730 β Type ?u.4730Preorder Ξ±: ?m.4727Ξ±] {f: Ξ± β Ξ±f : Ξ±: ?m.4409Ξ± β Ξ±: ?m.4727Ξ±}

/-- If \$x β€ f x\$ for all \$x\$ (we write this as `id β€ f`), then the same is true for any iterate
`f^[n]` of `f`. -/
theorem id_le_iterate_of_id_le: id β€ f β β (n : β), id β€ f^[n]id_le_iterate_of_id_le (h: id β€ fh : id: {Ξ± : Sort ?u.4420} β Ξ± β Ξ±id β€ f: Ξ± β Ξ±f) (n: βn : β: Typeβ) : id: {Ξ± : Sort ?u.4497} β Ξ± β Ξ±id β€ f: Ξ± β Ξ±f^[n: βn] := byGoals accomplished! π
Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±h: id β€ fn: βid β€ f^[n]simpa only [iterate_id: β {Ξ± : Type ?u.4562} (n : β), id^[n] = iditerate_id] using monotone_id: β {Ξ± : Type ?u.4628} [inst : Preorder Ξ±], Monotone idmonotone_id.iterate_le_of_le: β {Ξ± : Type ?u.4640} [inst : Preorder Ξ±] {f g : Ξ± β Ξ±}, Monotone f β f β€ g β β (n : β), f^[n] β€ g^[n]iterate_le_of_le h: id β€ fh n: βnGoals accomplished! π
#align function.id_le_iterate_of_id_le Function.id_le_iterate_of_id_le: β {Ξ± : Type u_1} [inst : Preorder Ξ±] {f : Ξ± β Ξ±}, id β€ f β β (n : β), id β€ f^[n]Function.id_le_iterate_of_id_le

theorem iterate_le_id_of_le_id: f β€ id β β (n : β), f^[n] β€ iditerate_le_id_of_le_id (h: f β€ idh : f: Ξ± β Ξ±f β€ id: {Ξ± : Sort ?u.4739} β Ξ± β Ξ±id) (n: βn : β: Typeβ) : f: Ξ± β Ξ±f^[n: βn] β€ id: {Ξ± : Sort ?u.4822} β Ξ± β Ξ±id :=
@id_le_iterate_of_id_le: β {Ξ± : Type ?u.4868} [inst : Preorder Ξ±] {f : Ξ± β Ξ±}, id β€ f β β (n : β), id β€ f^[n]id_le_iterate_of_id_le Ξ±: ?m.4727Ξ±α΅α΅ _ f: Ξ± β Ξ±f h: f β€ idh n: βn
#align function.iterate_le_id_of_le_id Function.iterate_le_id_of_le_id: β {Ξ± : Type u_1} [inst : Preorder Ξ±] {f : Ξ± β Ξ±}, f β€ id β β (n : β), f^[n] β€ idFunction.iterate_le_id_of_le_id

theorem monotone_iterate_of_id_le: id β€ f β Monotone fun m => f^[m]monotone_iterate_of_id_le (h: id β€ fh : id: {Ξ± : Sort ?u.4939} β Ξ± β Ξ±id β€ f: Ξ± β Ξ±f) : Monotone: {Ξ± : Type ?u.5014} β {Ξ² : Type ?u.5013} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropMonotone fun m: ?m.5038m => f: Ξ± β Ξ±f^[m: ?m.5038m] :=
monotone_nat_of_le_succ: β {Ξ± : Type ?u.5093} [inst : Preorder Ξ±] {f : β β Ξ±}, (β (n : β), f n β€ f (n + 1)) β Monotone fmonotone_nat_of_le_succ \$ fun n: ?m.5120n x: ?m.5123x => byGoals accomplished! π
Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±h: id β€ fn: βx: Ξ±(f^[n]) x β€ (f^[n + 1]) xrw [Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±h: id β€ fn: βx: Ξ±(f^[n]) x β€ (f^[n + 1]) xiterate_succ_apply': β {Ξ± : Type ?u.5157} (f : Ξ± β Ξ±) (n : β) (x : Ξ±), (f^[Nat.succ n]) x = f ((f^[n]) x)iterate_succ_apply'Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±h: id β€ fn: βx: Ξ±(f^[n]) x β€ f ((f^[n]) x)]Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±h: id β€ fn: βx: Ξ±(f^[n]) x β€ f ((f^[n]) x)
Ξ±: Type u_1instβ: Preorder Ξ±f: Ξ± β Ξ±h: id β€ fn: βx: Ξ±(f^[n]) x β€ (f^[n + 1]) xexact h: id β€ fh _: Ξ±_Goals accomplished! π
#align function.monotone_iterate_of_id_le Function.monotone_iterate_of_id_le: β {Ξ± : Type u_1} [inst : Preorder Ξ±] {f : Ξ± β Ξ±}, id β€ f β Monotone fun m => f^[m]Function.monotone_iterate_of_id_le

theorem antitone_iterate_of_le_id: f β€ id β Antitone fun m => f^[m]antitone_iterate_of_le_id (h: f β€ idh : f: Ξ± β Ξ±f β€ id: {Ξ± : Sort ?u.5272} β Ξ± β Ξ±id) : Antitone: {Ξ± : Type ?u.5347} β {Ξ² : Type ?u.5346} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropAntitone fun m: ?m.5371m => f: Ξ± β Ξ±f^[m: ?m.5371m] := fun m: ?m.5427m n: ?m.5430n hmn: ?m.5433hmn =>
@monotone_iterate_of_id_le: β {Ξ± : Type ?u.5435} [inst : Preorder Ξ±] {f : Ξ± β Ξ±}, id β€ f β Monotone fun m => f^[m]monotone_iterate_of_id_le Ξ±: ?m.5260Ξ±α΅α΅ _ f: Ξ± β Ξ±f h: f β€ idh m: ?m.5427m n: ?m.5430n hmn: ?m.5433hmn
#align function.antitone_iterate_of_le_id Function.antitone_iterate_of_le_id: β {Ξ± : Type u_1} [inst : Preorder Ξ±] {f : Ξ± β Ξ±}, f β€ id β Antitone fun m => f^[m]Function.antitone_iterate_of_le_id

end Preorder

/-!
### Iterates of commuting functions

If `f` and `g` are monotone and commute, then `f x β€ g x` implies `f^[n] x β€ g^[n] x`, see
`Function.Commute.iterate_le_of_map_le`. We also prove two strict inequality versions of this lemma,
as well as `iff` versions.
-/

namespace Commute

section Preorder

variable [Preorder: Type ?u.6079 β Type ?u.6079Preorder Ξ±: ?m.5515Ξ±] {f: Ξ± β Ξ±f g: Ξ± β Ξ±g : Ξ±: ?m.5515Ξ± β Ξ±: ?m.5515Ξ±}

theorem iterate_le_of_map_le: β {Ξ± : Type u_1} [inst : Preorder Ξ±] {f g : Ξ± β Ξ±},
Commute f g β Monotone f β Monotone g β β {x : Ξ±}, f x β€ g x β β (n : β), (f^[n]) x β€ (g^[n]) xiterate_le_of_map_le (h: Commute f gh : Commute: {Ξ± : Type ?u.5545} β (Ξ± β Ξ±) β (Ξ± β Ξ±) β PropCommute f: Ξ± β Ξ±f g: Ξ± β Ξ±g) (hf: Monotone fhf : Monotone: {Ξ± : Type ?u.5556} β {Ξ² : Type ?u.5555} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropMonotone f: Ξ± β Ξ±f) (hg: Monotone ghg : Monotone: {Ξ± : Type ?u.5588} β {Ξ² : Type ?u.5587} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropMonotone g: Ξ± β Ξ±g) {x: ?m.5616x}
(hx: f x β€ g xhx : f: Ξ± β Ξ±f x: ?m.5616x β€ g: Ξ± β Ξ±g x: ?m.5616x) (n: βn : β: Typeβ) : (f: Ξ± β Ξ±f^[n: βn]) x: ?m.5616x β€ (g: Ξ± β Ξ±g^[n: βn]) x: ?m.5616x := byGoals accomplished! π
Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: Monotone gx: Ξ±hx: f x β€ g xn: β(f^[n]) x β€ (g^[n]) xapply hf: Monotone fhf.seq_le_seq: β {Ξ± : Type ?u.5664} [inst : Preorder Ξ±] {f : Ξ± β Ξ±} {x y : β β Ξ±},
Monotone f β
β (n : β),
x 0 β€ y 0 β (β (k : β), k < n β x (k + 1) β€ f (x k)) β (β (k : β), k < n β f (y k) β€ y (k + 1)) β x n β€ y nseq_le_seq n: βnΞ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: Monotone gx: Ξ±hx: f x β€ g xn: βhβ(f^[0]) x β€ (g^[0]) xΞ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: Monotone gx: Ξ±hx: f x β€ g xn: βhxβ (k : β), k < n β (f^[k + 1]) x β€ f ((f^[k]) x)Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: Monotone gx: Ξ±hx: f x β€ g xn: βhyβ (k : β), k < n β f ((g^[k]) x) β€ (g^[k + 1]) x
Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: Monotone gx: Ξ±hx: f x β€ g xn: β(f^[n]) x β€ (g^[n]) xΒ·Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: Monotone gx: Ξ±hx: f x β€ g xn: βhβ(f^[0]) x β€ (g^[0]) x Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: Monotone gx: Ξ±hx: f x β€ g xn: βhβ(f^[0]) x β€ (g^[0]) xΞ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: Monotone gx: Ξ±hx: f x β€ g xn: βhxβ (k : β), k < n β (f^[k + 1]) x β€ f ((f^[k]) x)Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: Monotone gx: Ξ±hx: f x β€ g xn: βhyβ (k : β), k < n β f ((g^[k]) x) β€ (g^[k + 1]) xrflGoals accomplished! π
Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: Monotone gx: Ξ±hx: f x β€ g xn: β(f^[n]) x β€ (g^[n]) xΒ·Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: Monotone gx: Ξ±hx: f x β€ g xn: βhxβ (k : β), k < n β (f^[k + 1]) x β€ f ((f^[k]) x) Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: Monotone gx: Ξ±hx: f x β€ g xn: βhxβ (k : β), k < n β (f^[k + 1]) x β€ f ((f^[k]) x)Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: Monotone gx: Ξ±hx: f x β€ g xn: βhyβ (k : β), k < n β f ((g^[k]) x) β€ (g^[k + 1]) xintrosΞ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: Monotone gx: Ξ±hx: f x β€ g xn, kβ: βaβ: kβ < nhx(f^[kβ + 1]) x β€ f ((f^[kβ]) x);Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: Monotone gx: Ξ±hx: f x β€ g xn, kβ: βaβ: kβ < nhx(f^[kβ + 1]) x β€ f ((f^[kβ]) x) Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: Monotone gx: Ξ±hx: f x β€ g xn: βhxβ (k : β), k < n β (f^[k + 1]) x β€ f ((f^[k]) x)rw [Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: Monotone gx: Ξ±hx: f x β€ g xn, kβ: βaβ: kβ < nhx(f^[kβ + 1]) x β€ f ((f^[kβ]) x)iterate_succ_apply': β {Ξ± : Type ?u.5758} (f : Ξ± β Ξ±) (n : β) (x : Ξ±), (f^[Nat.succ n]) x = f ((f^[n]) x)iterate_succ_apply'Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: Monotone gx: Ξ±hx: f x β€ g xn, kβ: βaβ: kβ < nhxf ((f^[kβ]) x) β€ f ((f^[kβ]) x)]Goals accomplished! π
Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: Monotone gx: Ξ±hx: f x β€ g xn: β(f^[n]) x β€ (g^[n]) xΒ·Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: Monotone gx: Ξ±hx: f x β€ g xn: βhyβ (k : β), k < n β f ((g^[k]) x) β€ (g^[k + 1]) x Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: Monotone gx: Ξ±hx: f x β€ g xn: βhyβ (k : β), k < n β f ((g^[k]) x) β€ (g^[k + 1]) xintrosΞ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: Monotone gx: Ξ±hx: f x β€ g xn, kβ: βaβ: kβ < nhyf ((g^[kβ]) x) β€ (g^[kβ + 1]) x;Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: Monotone gx: Ξ±hx: f x β€ g xn, kβ: βaβ: kβ < nhyf ((g^[kβ]) x) β€ (g^[kβ + 1]) x Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: Monotone gx: Ξ±hx: f x β€ g xn: βhyβ (k : β), k < n β f ((g^[k]) x) β€ (g^[k + 1]) xsimp [h: Commute f gh.iterate_right: β {Ξ± : Type ?u.5795} {f g : Ξ± β Ξ±}, Commute f g β β (n : β), Commute f (g^[n])iterate_right _: β_ _: ?m.5802_, hg: Monotone ghg.iterate: β {Ξ± : Type ?u.5826} [inst : Preorder Ξ±] {f : Ξ± β Ξ±}, Monotone f β β (n : β), Monotone (f^[n])iterate _: β_ hx: f x β€ g xhx]Goals accomplished! π;Goals accomplished! π
#align function.commute.iterate_le_of_map_le Function.Commute.iterate_le_of_map_le: β {Ξ± : Type u_1} [inst : Preorder Ξ±] {f g : Ξ± β Ξ±},
Commute f g β Monotone f β Monotone g β β {x : Ξ±}, f x β€ g x β β (n : β), (f^[n]) x β€ (g^[n]) xFunction.Commute.iterate_le_of_map_le

theorem iterate_pos_lt_of_map_lt: Commute f g β Monotone f β StrictMono g β β {x : Ξ±}, f x < g x β β {n : β}, 0 < n β (f^[n]) x < (g^[n]) xiterate_pos_lt_of_map_lt (h: Commute f gh : Commute: {Ξ± : Type ?u.6090} β (Ξ± β Ξ±) β (Ξ± β Ξ±) β PropCommute f: Ξ± β Ξ±f g: Ξ± β Ξ±g) (hf: Monotone fhf : Monotone: {Ξ± : Type ?u.6101} β {Ξ² : Type ?u.6100} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropMonotone f: Ξ± β Ξ±f) (hg: StrictMono ghg : StrictMono: {Ξ± : Type ?u.6133} β {Ξ² : Type ?u.6132} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropStrictMono g: Ξ± β Ξ±g) {x: Ξ±x}
(hx: f x < g xhx : f: Ξ± β Ξ±f x: ?m.6161x < g: Ξ± β Ξ±g x: ?m.6161x) {n: βn} (hn: 0 < nhn : 0: ?m.61820 < n: ?m.6177n) : (f: Ξ± β Ξ±f^[n: ?m.6177n]) x: ?m.6161x < (g: Ξ± β Ξ±g^[n: ?m.6177n]) x: ?m.6161x := byGoals accomplished! π
Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±hx: f x < g xn: βhn: 0 < n(f^[n]) x < (g^[n]) xapply hf: Monotone fhf.seq_pos_lt_seq_of_le_of_lt: β {Ξ± : Type ?u.6283} [inst : Preorder Ξ±] {f : Ξ± β Ξ±} {x y : β β Ξ±},
Monotone f β
β {n : β},
0 < n β
x 0 β€ y 0 β (β (k : β), k < n β x (k + 1) β€ f (x k)) β (β (k : β), k < n β f (y k) < y (k + 1)) β x n < y nseq_pos_lt_seq_of_le_of_lt hn: 0 < nhnΞ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±hx: f x < g xn: βhn: 0 < nhβ(f^[0]) x β€ (g^[0]) xΞ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±hx: f x < g xn: βhn: 0 < nhxβ (k : β), k < n β (f^[k + 1]) x β€ f ((f^[k]) x)Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±hx: f x < g xn: βhn: 0 < nhyβ (k : β), k < n β f ((g^[k]) x) < (g^[k + 1]) x
Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±hx: f x < g xn: βhn: 0 < n(f^[n]) x < (g^[n]) xΒ·Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±hx: f x < g xn: βhn: 0 < nhβ(f^[0]) x β€ (g^[0]) x Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±hx: f x < g xn: βhn: 0 < nhβ(f^[0]) x β€ (g^[0]) xΞ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±hx: f x < g xn: βhn: 0 < nhxβ (k : β), k < n β (f^[k + 1]) x β€ f ((f^[k]) x)Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±hx: f x < g xn: βhn: 0 < nhyβ (k : β), k < n β f ((g^[k]) x) < (g^[k + 1]) xrflGoals accomplished! π
Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±hx: f x < g xn: βhn: 0 < n(f^[n]) x < (g^[n]) xΒ·Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±hx: f x < g xn: βhn: 0 < nhxβ (k : β), k < n β (f^[k + 1]) x β€ f ((f^[k]) x) Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±hx: f x < g xn: βhn: 0 < nhxβ (k : β), k < n β (f^[k + 1]) x β€ f ((f^[k]) x)Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±hx: f x < g xn: βhn: 0 < nhyβ (k : β), k < n β f ((g^[k]) x) < (g^[k + 1]) xintrosΞ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±hx: f x < g xn: βhn: 0 < nkβ: βaβ: kβ < nhx(f^[kβ + 1]) x β€ f ((f^[kβ]) x);Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±hx: f x < g xn: βhn: 0 < nkβ: βaβ: kβ < nhx(f^[kβ + 1]) x β€ f ((f^[kβ]) x) Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±hx: f x < g xn: βhn: 0 < nhxβ (k : β), k < n β (f^[k + 1]) x β€ f ((f^[k]) x)rw [Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±hx: f x < g xn: βhn: 0 < nkβ: βaβ: kβ < nhx(f^[kβ + 1]) x β€ f ((f^[kβ]) x)iterate_succ_apply': β {Ξ± : Type ?u.6383} (f : Ξ± β Ξ±) (n : β) (x : Ξ±), (f^[Nat.succ n]) x = f ((f^[n]) x)iterate_succ_apply'Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±hx: f x < g xn: βhn: 0 < nkβ: βaβ: kβ < nhxf ((f^[kβ]) x) β€ f ((f^[kβ]) x)]Goals accomplished! π
Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±hx: f x < g xn: βhn: 0 < n(f^[n]) x < (g^[n]) xΒ·Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±hx: f x < g xn: βhn: 0 < nhyβ (k : β), k < n β f ((g^[k]) x) < (g^[k + 1]) x Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±hx: f x < g xn: βhn: 0 < nhyβ (k : β), k < n β f ((g^[k]) x) < (g^[k + 1]) xintrosΞ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±hx: f x < g xn: βhn: 0 < nkβ: βaβ: kβ < nhyf ((g^[kβ]) x) < (g^[kβ + 1]) x;Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±hx: f x < g xn: βhn: 0 < nkβ: βaβ: kβ < nhyf ((g^[kβ]) x) < (g^[kβ + 1]) x Ξ±: Type u_1instβ: Preorder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±hx: f x < g xn: βhn: 0 < nhyβ (k : β), k < n β f ((g^[k]) x) < (g^[k + 1]) xsimp [h: Commute f gh.iterate_right: β {Ξ± : Type ?u.6420} {f g : Ξ± β Ξ±}, Commute f g β β (n : β), Commute f (g^[n])iterate_right _: β_ _: ?m.6427_, hg: StrictMono ghg.iterate: β {Ξ± : Type ?u.6451} [inst : Preorder Ξ±] {f : Ξ± β Ξ±}, StrictMono f β β (n : β), StrictMono (f^[n])iterate _: β_ hx: f x < g xhx]Goals accomplished! π
#align function.commute.iterate_pos_lt_of_map_lt Function.Commute.iterate_pos_lt_of_map_lt: β {Ξ± : Type u_1} [inst : Preorder Ξ±] {f g : Ξ± β Ξ±},
Commute f g β Monotone f β StrictMono g β β {x : Ξ±}, f x < g x β β {n : β}, 0 < n β (f^[n]) x < (g^[n]) xFunction.Commute.iterate_pos_lt_of_map_lt

theorem iterate_pos_lt_of_map_lt': β {Ξ± : Type u_1} [inst : Preorder Ξ±] {f g : Ξ± β Ξ±},
Commute f g β StrictMono f β Monotone g β β {x : Ξ±}, f x < g x β β {n : β}, 0 < n β (f^[n]) x < (g^[n]) xiterate_pos_lt_of_map_lt' (h: Commute f gh : Commute: {Ξ± : Type ?u.6722} β (Ξ± β Ξ±) β (Ξ± β Ξ±) β PropCommute f: Ξ± β Ξ±f g: Ξ± β Ξ±g) (hf: StrictMono fhf : StrictMono: {Ξ± : Type ?u.6733} β {Ξ² : Type ?u.6732} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropStrictMono f: Ξ± β Ξ±f) (hg: Monotone ghg : Monotone: {Ξ± : Type ?u.6765} β {Ξ² : Type ?u.6764} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropMonotone g: Ξ± β Ξ±g) {x: Ξ±x}
(hx: f x < g xhx : f: Ξ± β Ξ±f x: ?m.6793x < g: Ξ± β Ξ±g x: ?m.6793x) {n: βn} (hn: 0 < nhn : 0: ?m.68140 < n: ?m.6809n) : (f: Ξ± β Ξ±f^[n: ?m.6809n]) x: ?m.6793x < (g: Ξ± β Ξ±g^[n: ?m.6809n]) x: ?m.6793x :=
@iterate_pos_lt_of_map_lt: β {Ξ± : Type ?u.6913} [inst : Preorder Ξ±] {f g : Ξ± β Ξ±},
Commute f g β Monotone f β StrictMono g β β {x : Ξ±}, f x < g x β β {n : β}, 0 < n β (f^[n]) x < (g^[n]) xiterate_pos_lt_of_map_lt Ξ±: ?m.6708Ξ±α΅α΅ _ g: Ξ± β Ξ±g f: Ξ± β Ξ±f h: Commute f gh.symm: β {Ξ± : Type ?u.6922} {f g : Ξ± β Ξ±}, Commute f g β Commute g fsymm hg: Monotone ghg.dual: β {Ξ± : Type ?u.6940} {Ξ² : Type ?u.6939} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {f : Ξ± β Ξ²},
Monotone f β Monotone (βOrderDual.toDual β f β βOrderDual.ofDual)dual hf: StrictMono fhf.dual: β {Ξ± : Type ?u.6973} {Ξ² : Type ?u.6972} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {f : Ξ± β Ξ²},
StrictMono f β StrictMono (βOrderDual.toDual β f β βOrderDual.ofDual)dual x: Ξ±x hx: f x < g xhx n: βn hn: 0 < nhn
#align function.commute.iterate_pos_lt_of_map_lt' Function.Commute.iterate_pos_lt_of_map_lt': β {Ξ± : Type u_1} [inst : Preorder Ξ±] {f g : Ξ± β Ξ±},
Commute f g β StrictMono f β Monotone g β β {x : Ξ±}, f x < g x β β {n : β}, 0 < n β (f^[n]) x < (g^[n]) xFunction.Commute.iterate_pos_lt_of_map_lt'

end Preorder

variable [LinearOrder: Type ?u.7034 β Type ?u.7034LinearOrder Ξ±: ?m.7047Ξ±] {f: Ξ± β Ξ±f g: Ξ± β Ξ±g : Ξ±: ?m.7031Ξ± β Ξ±: ?m.7031Ξ±}

theorem iterate_pos_lt_iff_map_lt: Commute f g β Monotone f β StrictMono g β β {x : Ξ±} {n : β}, 0 < n β ((f^[n]) x < (g^[n]) x β f x < g x)iterate_pos_lt_iff_map_lt (h: Commute f gh : Commute: {Ξ± : Type ?u.7061} β (Ξ± β Ξ±) β (Ξ± β Ξ±) β PropCommute f: Ξ± β Ξ±f g: Ξ± β Ξ±g) (hf: Monotone fhf : Monotone: {Ξ± : Type ?u.7072} β {Ξ² : Type ?u.7071} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropMonotone f: Ξ± β Ξ±f) (hg: StrictMono ghg : StrictMono: {Ξ± : Type ?u.7122} β {Ξ² : Type ?u.7121} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropStrictMono g: Ξ± β Ξ±g) {x: Ξ±x n: ?m.7161n}
(hn: 0 < nhn : 0: ?m.71660 < n: ?m.7161n) : (f: Ξ± β Ξ±f^[n: ?m.7161n]) x: ?m.7158x < (g: Ξ± β Ξ±g^[n: ?m.7161n]) x: ?m.7158x β f: Ξ± β Ξ±f x: ?m.7158x < g: Ξ± β Ξ±g x: ?m.7158x := byGoals accomplished! π
Ξ±: Type u_1instβ: LinearOrder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±n: βhn: 0 < n(f^[n]) x < (g^[n]) x β f x < g xrcases lt_trichotomy: β {Ξ± : Type ?u.7274} [inst : LinearOrder Ξ±] (a b : Ξ±), a < b β¨ a = b β¨ b < alt_trichotomy (f: Ξ± β Ξ±f x: Ξ±x) (g: Ξ± β Ξ±g x: Ξ±x) with (H | H | H): f x < g x β¨ f x = g x β¨ g x < f x(H: f x < g xHH | H | H: f x = g x β¨ g x < f x | H: f x = g xHH | H | H: f x = g x β¨ g x < f x | H: g x < f xH(H | H | H): f x < g x β¨ f x = g x β¨ g x < f x)Ξ±: Type u_1instβ: LinearOrder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±n: βhn: 0 < nH: f x < g xinl(f^[n]) x < (g^[n]) x β f x < g xΞ±: Type u_1instβ: LinearOrder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±n: βhn: 0 < nH: f x = g xinr.inl(f^[n]) x < (g^[n]) x β f x < g xΞ±: Type u_1instβ: LinearOrder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±n: βhn: 0 < nH: g x < f xinr.inr(f^[n]) x < (g^[n]) x β f x < g x
Ξ±: Type u_1instβ: LinearOrder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±n: βhn: 0 < n(f^[n]) x < (g^[n]) x β f x < g xΒ·Ξ±: Type u_1instβ: LinearOrder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±n: βhn: 0 < nH: f x < g xinl(f^[n]) x < (g^[n]) x β f x < g x Ξ±: Type u_1instβ: LinearOrder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±n: βhn: 0 < nH: f x < g xinl(f^[n]) x < (g^[n]) x β f x < g xΞ±: Type u_1instβ: LinearOrder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±n: βhn: 0 < nH: f x = g xinr.inl(f^[n]) x < (g^[n]) x β f x < g xΞ±: Type u_1instβ: LinearOrder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±n: βhn: 0 < nH: g x < f xinr.inr(f^[n]) x < (g^[n]) x β f x < g xsimp only [*, iterate_pos_lt_of_map_lt: β {Ξ± : Type ?u.7347} [inst : Preorder Ξ±] {f g : Ξ± β Ξ±},
Commute f g β Monotone f β StrictMono g β β {x : Ξ±}, f x < g x β β {n : β}, 0 < n β (f^[n]) x < (g^[n]) xiterate_pos_lt_of_map_lt]Goals accomplished! π
Ξ±: Type u_1instβ: LinearOrder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±n: βhn: 0 < n(f^[n]) x < (g^[n]) x β f x < g xΒ·Ξ±: Type u_1instβ: LinearOrder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±n: βhn: 0 < nH: f x = g xinr.inl(f^[n]) x < (g^[n]) x β f x < g x Ξ±: Type u_1instβ: LinearOrder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±n: βhn: 0 < nH: f x = g xinr.inl(f^[n]) x < (g^[n]) x β f x < g xΞ±: Type u_1instβ: LinearOrder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±n: βhn: 0 < nH: g x < f xinr.inr(f^[n]) x < (g^[n]) x β f x < g xsimp only [*, h: Commute f gh.iterate_eq_of_map_eq: β {Ξ± : Type ?u.7588} {f g : Ξ± β Ξ±}, Commute f g β β (n : β) {x : Ξ±}, f x = g x β (f^[n]) x = (g^[n]) xiterate_eq_of_map_eq, lt_irrefl: β {Ξ± : Type ?u.7613} [inst : Preorder Ξ±] (a : Ξ±), Β¬a < alt_irrefl]Goals accomplished! π
Ξ±: Type u_1instβ: LinearOrder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±n: βhn: 0 < n(f^[n]) x < (g^[n]) x β f x < g xΒ·Ξ±: Type u_1instβ: LinearOrder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±n: βhn: 0 < nH: g x < f xinr.inr(f^[n]) x < (g^[n]) x β f x < g x Ξ±: Type u_1instβ: LinearOrder Ξ±f, g: Ξ± β Ξ±h: Commute f ghf: Monotone fhg: StrictMono gx: Ξ±n: βhn: 0 < nH: g x < f xinr.inr(f^[n]) x < (g^[n]) x β f x < g xsimp only [lt_asymm: β {Ξ± : Type ?u.7789} [inst : Preorder Ξ±] {a b : Ξ±}, a < b β Β¬b < alt_asymm H: g x < f xH, lt_asymm: β {Ξ± : Type ?u.7802} [inst : Preorder Ξ±] {a b : Ξ±}, a < b β Β¬b < alt_asymm (h: Commute f gh.symm: β {Ξ± : Type ?u.7807} {f g : Ξ± β Ξ±}, Commute f g β Commute g fsymm.iterate_pos_lt_of_map_lt': β {Ξ± : Type ?u.7819} [inst : Preorder Ξ±] {f g : Ξ± β Ξ±},
Commute f g β StrictMono f β Monotone g β β {x : Ξ±}, f x < g x β β {n : β}, 0 < n β (f^[n]) x < (g^[n]) xiterate_pos_lt_of_map_lt' hg: StrictMono ghg hf: Monotone fhf H: g x < f xH hn: 0 < nhn)]Goals accomplished! π
#align function.commute.iterate_pos_lt_iff_map_lt Function.Commute.iterate_pos_lt_iff_map_lt: β {Ξ± : Type u_1} [inst : LinearOrder Ξ±] {f g : Ξ± β Ξ±},
Commute f g β Monotone f β StrictMono g β β {x : Ξ±} {n : β}, 0 < n β ((f^[n]) x < (g^[n]) x β f x < g x)Function.Commute.iterate_pos_lt_iff_map_lt

theorem iterate_pos_lt_iff_map_lt': β {Ξ± : Type u_1} [inst : LinearOrder Ξ±] {f g : Ξ± β Ξ±},
Commute f g β StrictMono f β Monotone g β β {x : Ξ±} {n : β}, 0 < n β ((f^[n]) x < (g^[n]) x β f x < g x)iterate_pos_lt_iff_map_lt' (h: Commute f gh : Commute: {Ξ± : Type ?u.7913} β (Ξ± β Ξ±) β (Ξ± β Ξ±) β PropCommute f: Ξ± β Ξ±f g: Ξ± β Ξ±g) (hf: StrictMono fhf : StrictMono: {Ξ± : Type ?u.7924} β {Ξ² : Type ?u.7923} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropStrictMono f: Ξ± β Ξ±f) (hg: Monotone ghg : Monotone: {Ξ± : Type ?u.7974} β {Ξ² : Type ?u.7973} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropMonotone g: Ξ± β Ξ±g) {x: ?m.8010x n: ?m.8013n}
(hn: 0 < nhn : 0: ?m.80180 < n: ?m.8013n) : (f: Ξ± β Ξ±f^[n: ?m.8013n]) x: ?m.8010x < (g: Ξ± β Ξ±g^[n: ?m.8013n]) x: ?m.8010x β f: Ξ± β Ξ±f x: ?m.8010x < g: Ξ± β Ξ±g x: ?m.8010x :=
@iterate_pos_lt_iff_map_lt: β {Ξ± : Type ?u.8124} [inst : LinearOrder Ξ±] {f g : Ξ± β Ξ±},
Commute f g β Monotone f β StrictMono g β β {x : Ξ±} {n : β}, 0 < n β ((f^[n]) x < (g^[n]) x β f x < g x)iterate_pos_lt_iff_map_lt Ξ±: ?m.7899Ξ±α΅α΅ _ _: Ξ±α΅α΅ β Ξ±α΅α΅_ _: Ξ±α΅α΅ β Ξ±α΅α΅_ h: Commute f gh.symm: β {Ξ± : Type ?u.8129} {f g : Ξ± β Ξ±}, Commute f g β Commute g fsymm hg: Monotone ghg.dual: β {Ξ± : Type ?u.8149} {Ξ² : Type ?u.8148} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {f : Ξ± β Ξ²},
Monotone f β Monotone (βOrderDual.toDual β f β βOrderDual.ofDual)dual hf: StrictMono fhf.dual: β {Ξ± : Type ?u.8223} {Ξ² : Type ?u.8222} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {f : Ξ± β Ξ²},
StrictMono f β StrictMono (βOrderDual.toDual β f β βOrderDual.ofDual)dual x: Ξ±x n: βn hn: 0 < nhn
#align function.commute.iterate_pos_lt_iff_map_lt' Function.Commute.iterate_pos_lt_iff_map_lt': β {Ξ± : Type u_1} [inst : LinearOrder Ξ±] {f g : Ξ± β Ξ±},
Commute f g β StrictMono f β Monotone g β β {x : Ξ±} {n : β}, 0 < n β ((f^[n]) x < (g^[n]) x β f x < g x)Function.Commute.iterate_pos_lt_iff_map_lt'

theorem iterate_pos_le_iff_map_le: ```