awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
_ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → ∀ ⦃a : α⦄, IsLUB s a → a ∈ range f
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → ∀ ⦃a : α⦄, IsLUB s a → a ∈ range f

Tactic:
_
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
obtain : ∀ (b : α) (hb : b ∈ s), (f ⁻¹' s).Nonempty
⊢ (f ⁻¹' s).Nonempty

Tactic:
obtain ⟨b, hb⟩ := hs₀
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
b : α
hb : b ∈ s
obtain : ∀ (c : α) (hb : f c ∈ s), (f ⁻¹' s).Nonempty
⊢ (f ⁻¹' s).Nonempty

Tactic:
obtain ⟨c, rfl⟩ := hs hb

Premises used: rfl
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
c : α
hb : f c ∈ s
⊢ (f ⁻¹' s).Nonempty

Tactic:
⟨c, hb⟩

Premises used: Set.Nonempty, Exists.intro
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
c : α
hb : f c ∈ s
⊢ (f ⁻¹' s).Nonempty

Tactic:
exact ⟨c, hb⟩
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
⊢ (f ⁻¹' s).Nonempty

Tactic:
have hf' : (f ⁻¹' s).Nonempty := by
    obtain ⟨b, hb⟩ := hs₀
    obtain ⟨c, rfl⟩ := hs hb
    exact ⟨c, hb⟩
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
hf' : (f ⁻¹' s).Nonempty
⊢ Nonempty α

Tactic:
have : Nonempty α := ⟨a⟩
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
hf' : (f ⁻¹' s).Nonempty
this_1 : Nonempty α
this_2 : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
⊢ IsLUB (f ⁻¹' s) (sSup (f ⁻¹' s))

Tactic:
have hfl : IsLUB (f ⁻¹' s) (sSup (f ⁻¹' s)) :=
    isLUB_csSup hf' ⟨a, fun b hb ↦ hf.strictMono.le_apply.trans (ha.1 hb)⟩
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
hf' : (f ⁻¹' s).Nonempty
this_1 : Nonempty α
this_2 : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
hfl : IsLUB (f ⁻¹' s) (sSup (f ⁻¹' s))
⊢ IsLUB (f '' f ⁻¹' s) (f (sSup (f ⁻¹' s)))

Tactic:
have ha' := hf.map_isLUB hfl hf'
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
hf' : (f ⁻¹' s).Nonempty
this_1 : Nonempty α
this_2 : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
hfl : IsLUB (f ⁻¹' s) (sSup (f ⁻¹' s))
ha' : IsLUB (f '' f ⁻¹' s) (f (sSup (f ⁻¹' s)))
⊢ IsLUB s (f (sSup (f ⁻¹' s)))

Tactic:
rw [image_preimage_eq_of_subset hs] at ha'

Premises used: Set.image_preimage_eq_of_subset
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
hf' : (f ⁻¹' s).Nonempty
this_1 : Nonempty α
this_2 : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
hfl : IsLUB (f ⁻¹' s) (sSup (f ⁻¹' s))
ha' : IsLUB s (f (sSup (f ⁻¹' s)))
obtain : ∀ (ha : IsLUB s (f (sSup (f ⁻¹' s)))), f (sSup (f ⁻¹' s)) ∈ range f
⊢ a ∈ range f

Tactic:
obtain rfl := ha.unique ha'

Premises used: IsLUB.unique, rfl
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hf' : (f ⁻¹' s).Nonempty
this_1 : Nonempty α
this_2 : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
hfl : IsLUB (f ⁻¹' s) (sSup (f ⁻¹' s))
ha' ha : IsLUB s (f (sSup (f ⁻¹' s)))
⊢ f (sSup (f ⁻¹' s)) ∈ range f

Tactic:
mem_range_self _

Premises used: Set.mem_range_self
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hf' : (f ⁻¹' s).Nonempty
this_1 : Nonempty α
this_2 : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
hfl : IsLUB (f ⁻¹' s) (sSup (f ⁻¹' s))
ha' ha : IsLUB s (f (sSup (f ⁻¹' s)))
⊢ f (sSup (f ⁻¹' s)) ∈ range f

Tactic:
exact mem_range_self _

Premises used: Set.mem_range_self
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
hx : ∀ (k : ℕ), k < 0 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)
⊢ x 0 ≤ y 0

Tactic:
h₀
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
hx : ∀ (k : ℕ), k < 0 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)
⊢ x 0 ≤ y 0

Tactic:
exact h₀
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : ∀ (hx : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) (hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)), x n ≤ y n
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ x (n + 1) ≤ y (n + 1)

Tactic:
(hx _ n.lt_succ_self).trans ((hf <| ihn ?_ ?_).trans (hy _ n.lt_succ_self))

Premises used: Nat.lt_succ_self, LE.le.trans
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : ∀ (hx : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) (hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)), x n ≤ y n
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
succ : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)
succ₁ : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
⊢ x (n + 1) ≤ y (n + 1)

Tactic:
refine (hx _ n.lt_succ_self).trans ((hf <| ihn ?_ ?_).trans (hy _ n.lt_succ_self))

Premises used: Nat.lt_succ_self, LE.le.trans
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : ∀ (hx : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) (hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)), x n ≤ y n
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)

Tactic:
fun k hk => hx _ (hk.trans n.lt_succ_self)

Premises used: Nat.lt_succ_self, LT.lt.trans
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : ∀ (hx : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) (hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)), x n ≤ y n
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)

Tactic:
exact fun k hk => hx _ (hk.trans n.lt_succ_self)
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : ∀ (hx : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) (hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)), x n ≤ y n
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)

Tactic:
fun k hk => hy _ (hk.trans n.lt_succ_self)

Premises used: Nat.lt_succ_self, LT.lt.trans
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : ∀ (hx : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) (hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)), x n ≤ y n
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)

Tactic:
exact fun k hk => hy _ (hk.trans n.lt_succ_self)
-- Module: Mathlib.Order.Iterate
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)
zero : ∀ (hx : ∀ (k : ℕ), k < 0 → x (k + 1) ≤ f (x k)) (hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)), x 0 ≤ y 0
succ :
  ∀ (n : ℕ)
    (ihn : ∀ (hx : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) (hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)), x n ≤ y n)
    (hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) ≤ f (x k)) (hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)),
    x (n + 1) ≤ y (n + 1)
⊢ x n ≤ y n

Tactic:
induction n with
  | zero => exact h₀
  | succ n ihn =>
    refine (hx _ n.lt_succ_self).trans ((hf <| ihn ?_ ?_).trans (hy _ n.lt_succ_self))
    · exact fun k hk => hx _ (hk.trans n.lt_succ_self)
    · exact fun k hk => hy _ (hk.trans n.lt_succ_self)
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
hn : LT.lt (α := ℕ) 0 0
hx : ∀ (k : ℕ), k < 0 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)
⊢ x 0 < y 0

Tactic:
hn.false.elim

Premises used: False.elim, LT.lt.false
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
hn : LT.lt (α := ℕ) 0 0
hx : ∀ (k : ℕ), k < 0 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)
⊢ x 0 < y 0

Tactic:
exact hn.false.elim

Premises used: False.elim, LT.lt.false
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn :
  ∀ (hn : 0 < n) (hx : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)) (hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)), x n < y n
hn : 0 < n + 1
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
succ : x n ≤ y n
⊢ x (n + 1) < y (n + 1)

Tactic:
suffices x n ≤ y n from (hx n n.lt_succ_self).trans_le ((hf this).trans <| hy n n.lt_succ_self)
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
ihn :
  ∀ (hn : LT.lt (α := ℕ) 0 0) (hx : ∀ (k : ℕ), k < 0 → x (k + 1) < f (x k))
    (hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)), x 0 < y 0
hn : 0 < HAdd.hAdd (α := ℕ) 0 1
hx : ∀ (k : ℕ), k < HAdd.hAdd (α := ℕ) 0 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < HAdd.hAdd (α := ℕ) 0 1 → f (y k) ≤ y (k + 1)
⊢ x 0 ≤ y 0

Tactic:
h₀
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
ihn :
  ∀ (hn : LT.lt (α := ℕ) 0 0) (hx : ∀ (k : ℕ), k < 0 → x (k + 1) < f (x k))
    (hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)), x 0 < y 0
hn : 0 < HAdd.hAdd (α := ℕ) 0 1
hx : ∀ (k : ℕ), k < HAdd.hAdd (α := ℕ) 0 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < HAdd.hAdd (α := ℕ) 0 1 → f (y k) ≤ y (k + 1)
⊢ x 0 ≤ y 0

Tactic:
exact h₀
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn :
  ∀ (hn : 0 < n + 1) (hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k))
    (hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)), x (n + 1) < y (n + 1)
hn : 0 < n + 1 + 1
hx : ∀ (k : ℕ), k < n + 1 + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n + 1 + 1 → f (y k) ≤ y (k + 1)
⊢ x (n + 1) ≤ y (n + 1)

Tactic:
(ihn n.zero_lt_succ (fun k hk => hx _ ?_) fun k hk => hy _ ?_).le

Premises used: Nat.zero_lt_succ, LT.lt.le
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn :
  ∀ (hn : 0 < n + 1) (hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k))
    (hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)), x (n + 1) < y (n + 1)
hn : 0 < n + 1 + 1
hx : ∀ (k : ℕ), k < n + 1 + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n + 1 + 1 → f (y k) ≤ y (k + 1)
succ succ₁ : ∀ (k : ℕ) (hk : k < n + 1), k < n + 1 + 1
⊢ x (n + 1) ≤ y (n + 1)

Tactic:
refine (ihn n.zero_lt_succ (fun k hk => hx _ ?_) fun k hk => hy _ ?_).le

Premises used: Nat.zero_lt_succ, LT.lt.le
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn :
  ∀ (hn : 0 < n + 1) (hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k))
    (hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)), x (n + 1) < y (n + 1)
hn : 0 < n + 1 + 1
hx : ∀ (k : ℕ), k < n + 1 + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n + 1 + 1 → f (y k) ≤ y (k + 1)
k : ℕ
hk : k < n + 1
⊢ k < n + 1 + 1

Tactic:
hk.trans n.succ.lt_succ_self

Premises used: Nat.lt_succ_self, LT.lt.trans, Nat.succ
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn :
  ∀ (hn : 0 < n + 1) (hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k))
    (hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)), x (n + 1) < y (n + 1)
hn : 0 < n + 1 + 1
hx : ∀ (k : ℕ), k < n + 1 + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n + 1 + 1 → f (y k) ≤ y (k + 1)
k : ℕ
hk : k < n + 1
⊢ k < n + 1 + 1

Tactic:
exact hk.trans n.succ.lt_succ_self

Premises used: Nat.lt_succ_self, LT.lt.trans, Nat.succ
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn :
  ∀ (hn : 0 < n) (hx : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)) (hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)), x n < y n
hn : 0 < n + 1
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
succ :
  ∀
    (ihn :
      ∀ (hn : LT.lt (α := ℕ) 0 0) (hx : ∀ (k : ℕ), k < 0 → x (k + 1) < f (x k))
        (hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)), x 0 < y 0)
    (hn : 0 < HAdd.hAdd (α := ℕ) 0 1) (hx : ∀ (k : ℕ), k < HAdd.hAdd (α := ℕ) 0 1 → x (k + 1) < f (x k))
    (hy : ∀ (k : ℕ), k < HAdd.hAdd (α := ℕ) 0 1 → f (y k) ≤ y (k + 1)), x 0 ≤ y 0
succ₁ :
  ∀ (n : ℕ)
    (ihn :
      ∀ (hn : 0 < n + 1) (hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k))
        (hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)), x (n + 1) < y (n + 1))
    (hn : 0 < n + 1 + 1) (hx : ∀ (k : ℕ), k < n + 1 + 1 → x (k + 1) < f (x k))
    (hy : ∀ (k : ℕ), k < n + 1 + 1 → f (y k) ≤ y (k + 1)), x (n + 1) ≤ y (n + 1)
⊢ x n ≤ y n

Tactic:
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
-- Module: Mathlib.Order.Iterate
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)
zero :
  ∀ (hn : LT.lt (α := ℕ) 0 0) (hx : ∀ (k : ℕ), k < 0 → x (k + 1) < f (x k))
    (hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)), x 0 < y 0
succ :
  ∀ (n : ℕ)
    (ihn :
      ∀ (hn : 0 < n) (hx : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)) (hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)),
        x n < y n)
    (hn : 0 < n + 1) (hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k))
    (hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)), x (n + 1) < y (n + 1)
⊢ x n < y n

Tactic:
induction n with
  | zero => exact hn.false.elim
  | succ n ihn =>
  suffices x n ≤ y n from (hx n n.lt_succ_self).trans_le ((hf this).trans <| hy n n.lt_succ_self)
  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

Premises used: False.elim, LT.lt.false
-- Module: Mathlib.Order.Iterate
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

Tactic:
hf.dual.seq_pos_lt_seq_of_lt_of_le hn h₀ hy hx

Premises used: Monotone.dual, Monotone.seq_pos_lt_seq_of_lt_of_le
-- Module: Mathlib.Order.Iterate
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)
zero : ∀ (hx : ∀ (k : ℕ), k < 0 → x (k + 1) < f (x k)) (hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)), x 0 < y 0
succ :
  ∀ (n : ℕ) (hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k)) (hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)),
    x (n + 1) < y (n + 1)
⊢ x n < y n

Tactic:
cases n
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 < y 0
hx : ∀ (k : ℕ), k < 0 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)
⊢ x 0 < y 0

Tactic:
h₀
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 < y 0
n : ℕ
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ x (n + 1) < y (n + 1)

Tactic:
hf.seq_pos_lt_seq_of_lt_of_le (Nat.zero_lt_succ _) h₀.le hx hy

Premises used: Nat.zero_lt_succ, LT.lt.le, Monotone.seq_pos_lt_seq_of_lt_of_le
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 < y 0
hx : ∀ (k : ℕ), k < 0 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)
⊢ x 0 < y 0

Tactic:
exacts [h₀, hf.seq_pos_lt_seq_of_lt_of_le (Nat.zero_lt_succ _) h₀.le hx hy]
-- Module: Mathlib.Order.Iterate
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

Tactic:
hf.dual.seq_lt_seq_of_lt_of_le n h₀ hy hx

Premises used: Monotone.seq_lt_seq_of_lt_of_le, Monotone.dual
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
β : Type u_2
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
h₀ : (h ∘ g^[0]) x ≤ (f^[0] ∘ h) x
hx : ∀ (k : ℕ), k < n → (h ∘ g^[k + 1]) x ≤ f ((h ∘ g^[k]) x)
hy : ∀ (k : ℕ), k < n → f ((f^[k] ∘ h) x) ≤ (f^[k + 1] ∘ h) x
⊢ (h ∘ g^[n]) x ≤ (f^[n] ∘ h) x

Tactic:
apply hf.seq_le_seq n

Premises used: Monotone.seq_le_seq
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
β : Type u_2
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
⊢ (h ∘ g^[0]) x ≤ (f^[0] ∘ h) x

Tactic:
aesop (add simp [iterate_succ']) (erase simp [iterate_succ])

Premises used: Function.iterate_succ, Function.iterate_succ'
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
β : Type u_2
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)

Tactic:
aesop (add simp [iterate_succ']) (erase simp [iterate_succ])

Premises used: Function.iterate_succ, Function.iterate_succ'
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
β : Type u_2
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

Tactic:
aesop (add simp [iterate_succ']) (erase simp [iterate_succ])

Premises used: Function.iterate_succ, Function.iterate_succ'
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f g : α → α
hf : Monotone f
h : f ≤ g
n : ℕ
⊢ f^[n] ≤ g^[n]

Tactic:
hf.iterate_comp_le_of_le h n

Premises used: Monotone.iterate_comp_le_of_le
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
h : id ≤ f
n : ℕ
⊢ id ≤ f^[n]

Tactic:
simpa only [iterate_id] using monotone_id.iterate_le_of_le h n

Premises used: Function.iterate_id, Monotone.iterate_le_of_le, monotone_id
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
h : id ≤ f
n : ℕ
x : α
rw : f^[n] x ≤ f (f^[n] x)
⊢ f^[n] x ≤ f^[n + 1] x

Tactic:
rw [iterate_succ_apply']

Premises used: Function.iterate_succ_apply'
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
h : id ≤ f
n : ℕ
x : α
⊢ f^[n] x ≤ f (f^[n] x)

Tactic:
h _
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
h : id ≤ f
n : ℕ
x : α
⊢ f^[n] x ≤ f (f^[n] x)

Tactic:
exact h _
-- Module: Mathlib.Order.Iterate
Goal:
α : Type u_1
inst : Preorder α
f : α → α
h : f ≤ id
⊢ Antitone.{0, u_1} (β := α → α) fun (m : ℕ) ↦ f^[m]

Tactic:
fun m n hmn =>
  @monotone_iterate_of_id_le αᵒᵈ _ f h m n hmn

Premises used: Antitone, OrderDual, Function.monotone_iterate_of_id_le
-- Module: Mathlib.Order.Iterate
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 : ℕ
h₀ : f^[0] x ≤ f^[0] x
hx₁ : ∀ (k : ℕ), k < n → f^[k + 1] x ≤ f (f^[k] x)
hy : ∀ (k : ℕ), k < n → f (g^[k] x) ≤ g^[k + 1] x
⊢ f^[n] x ≤ g^[n] x

Tactic:
apply hf.seq_le_seq n

Premises used: Monotone.seq_le_seq
-- Module: Mathlib.Order.Iterate
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^[0] x ≤ f^[0] x

Tactic:
rfl
-- Module: Mathlib.Order.Iterate
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 k : ℕ
h_1 : k < n
hx₁ hx₂ : f (f^[k] x) ≤ f (f^[k] x)
⊢ f^[k + 1] x ≤ f (f^[k] x)

Tactic:
rw [iterate_succ_apply']

Premises used: Function.iterate_succ_apply'
-- Module: Mathlib.Order.Iterate
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 : ℕ
⊢ ∀ (k : ℕ), k < n → f (g^[k] x) ≤ g^[k + 1] x

Tactic:
simp [h.iterate_right _ _, hg.iterate _ hx]

Premises used: Monotone.iterate, Function.Commute.iterate_right
-- Module: Mathlib.Order.Iterate
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
h₀ : f^[0] x ≤ f^[0] x
hx₁ : ∀ (k : ℕ), k < n → f^[k + 1] x ≤ f (f^[k] x)
hy : ∀ (k : ℕ), k < n → f (g^[k] x) < g^[k + 1] x
⊢ f^[n] x < g^[n] x

Tactic:
apply hf.seq_pos_lt_seq_of_le_of_lt hn

Premises used: Monotone.seq_pos_lt_seq_of_le_of_lt
-- Module: Mathlib.Order.Iterate
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^[0] x ≤ f^[0] x

Tactic:
rfl
-- Module: Mathlib.Order.Iterate
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
k : ℕ
h_1 : k < n
hx₁ hx₂ : f (f^[k] x) ≤ f (f^[k] x)
⊢ f^[k + 1] x ≤ f (f^[k] x)

Tactic:
rw [iterate_succ_apply']

Premises used: Function.iterate_succ_apply'
-- Module: Mathlib.Order.Iterate
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
⊢ ∀ (k : ℕ), k < n → f (g^[k] x) < g^[k + 1] x

Tactic:
simp [h.iterate_right _ _, hg.iterate _ hx]

Premises used: Function.Commute.iterate_right, StrictMono.iterate