awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℕ → α
k : ℕ
refine_1 :
  ∀ (h : Monotone.{0, u} (β := α) fun (n : ℕ) ↦ f (n + k)) (x : ℕ) (hx : Membership.mem (γ := Set ℕ) {x : ℕ | k ≤ x} x)
    (y : ℕ) (hy : Membership.mem (γ := Set ℕ) {x : ℕ | k ≤ x} y) (hle : x ≤ y), f x ≤ f y
refine_2 :
  ∀ (h : MonotoneOn f {x : ℕ | k ≤ x}) (x y : ℕ) (hle : x ≤ y),
    LE.le.{u} (α := α) ((fun (n : ℕ) ↦ f (n + k)) x) ((fun (n : ℕ) ↦ f (n + k)) y)
⊢ (Monotone.{0, u} (β := α) fun (n : ℕ) ↦ f (n + k)) ↔ MonotoneOn f {x : ℕ | k ≤ x}

Tactic:
refine ⟨fun h x hx y hy hle ↦ ?_, fun h x y hle ↦ ?_⟩
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℕ → α
k : ℕ
h : Monotone.{0, u} (β := α) fun (n : ℕ) ↦ f (n + k)
x : ℕ
hx : Membership.mem (γ := Set ℕ) {x : ℕ | k ≤ x} x
y : ℕ
hy : Membership.mem (γ := Set ℕ) {x : ℕ | k ≤ x} y
hle : x ≤ y
refine_1 : f (x - k + k) ≤ f (y - k + k)
⊢ f x ≤ f y

Tactic:
rw [← Nat.sub_add_cancel hx, ← Nat.sub_add_cancel hy]

Premises used: Nat.sub_add_cancel
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℕ → α
k : ℕ
h : Monotone.{0, u} (β := α) fun (n : ℕ) ↦ f (n + k)
x : ℕ
hx : Membership.mem (γ := Set ℕ) {x : ℕ | k ≤ x} x
y : ℕ
hy : Membership.mem (γ := Set ℕ) {x : ℕ | k ≤ x} y
hle : x ≤ y
⊢ x - k ≤ y - k

Tactic:
rw [← Nat.sub_le_sub_iff_right hy] at hle

Premises used: Nat.sub_le_sub_iff_right
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℕ → α
k : ℕ
h : Monotone.{0, u} (β := α) fun (n : ℕ) ↦ f (n + k)
x : ℕ
hx : Membership.mem (γ := Set ℕ) {x : ℕ | k ≤ x} x
y : ℕ
hy : Membership.mem (γ := Set ℕ) {x : ℕ | k ≤ x} y
hle : x - k ≤ y - k
⊢ f (x - k + k) ≤ f (y - k + k)

Tactic:
h hle
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℕ → α
k : ℕ
h : Monotone.{0, u} (β := α) fun (n : ℕ) ↦ f (n + k)
x : ℕ
hx : Membership.mem (γ := Set ℕ) {x : ℕ | k ≤ x} x
y : ℕ
hy : Membership.mem (γ := Set ℕ) {x : ℕ | k ≤ x} y
hle : x - k ≤ y - k
⊢ f (x - k + k) ≤ f (y - k + k)

Tactic:
exact h hle
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℕ → α
k : ℕ
h : MonotoneOn f {x : ℕ | k ≤ x}
x y : ℕ
hle : x ≤ y
refine_2 : ∀ (hle : x + k ≤ y + k), LE.le.{u} (α := α) ((fun (n : ℕ) ↦ f (n + k)) x) ((fun (n : ℕ) ↦ f (n + k)) y)
rw : ℕ
⊢ LE.le.{u} (α := α) ((fun (n : ℕ) ↦ f (n + k)) x) ((fun (n : ℕ) ↦ f (n + k)) y)

Tactic:
rw [← Nat.add_le_add_iff_right] at hle

Premises used: Nat.add_le_add_iff_right
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℕ → α
k : ℕ
h : MonotoneOn f {x : ℕ | k ≤ x}
x y : ℕ
hle_1 : x ≤ y
hle : x + k ≤ y + k
⊢ LE.le.{u} (α := α) ((fun (n : ℕ) ↦ f (n + k)) x) ((fun (n : ℕ) ↦ f (n + k)) y)

Tactic:
h (Nat.le_add_left k x) (Nat.le_add_left k y) hle

Premises used: Nat.le_add_left
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℕ → α
hf : ∀ (n : ℕ), f (n + 1) ≤ f n
⊢ Antitone f

Tactic:
@monotone_nat_of_le_succ αᵒᵈ _ _ hf

Premises used: Antitone, monotone_nat_of_le_succ
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℕ → α
k : ℕ
hf : ∀ (n : ℕ), n ≥ k → f (n + 1) ≤ f n
⊢ Antitone.{0, u} (β := α) fun (n : ℕ) ↦ f (n + k)

Tactic:
@monotone_add_nat_of_le_succ αᵒᵈ _ f k hf

Premises used: monotone_add_nat_of_le_succ, Antitone
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℕ → α
k : ℕ
hf : ∀ (n : ℕ), n ≥ k → f (n + 1) ≤ f n
⊢ AntitoneOn f {x : ℕ | k ≤ x}

Tactic:
@monotoneOn_nat_Ici_of_le_succ αᵒᵈ _ f k hf

Premises used: monotoneOn_nat_Ici_of_le_succ, AntitoneOn
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℕ → α
k : ℕ
⊢ (Antitone.{0, u} (β := α) fun (n : ℕ) ↦ f (n + k)) ↔ AntitoneOn f {x : ℕ | k ≤ x}

Tactic:
@monotone_add_nat_iff_monotoneOn_nat_Ici αᵒᵈ _ f k

Premises used: monotone_add_nat_iff_monotoneOn_nat_Ici, Antitone, AntitoneOn
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℕ → α
hf : ∀ (n : ℕ), f n < f (n + 1)
⊢ StrictMono f

Tactic:
Nat.rel_of_forall_rel_succ_of_lt (· < ·) hf

Premises used: StrictMono, LT.lt, Nat.rel_of_forall_rel_succ_of_lt
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℕ → α
hf : ∀ (n : ℕ), f (n + 1) < f n
⊢ StrictAnti f

Tactic:
@strictMono_nat_of_lt_succ αᵒᵈ _ f hf

Premises used: strictMono_nat_of_lt_succ, StrictAnti
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
choose : ∀ (g : (x : α) → α) (hg : ∀ (x : α), x < g x), ∃ (f : ℕ → α), StrictMono f ∧ f 0 = a
⊢ ∃ (f : ℕ → α), StrictMono f ∧ f 0 = a

Tactic:
choose g hg using fun x : α ↦ exists_gt x

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
g : (x : α) → α
hg : ∀ (x : α), x < g x
⊢ ∃ (f : ℕ → α), StrictMono f ∧ f 0 = a

Tactic:
⟨fun n ↦ Nat.recOn n a fun _ ↦ g, strictMono_nat_of_lt_succ fun n ↦ hg _, rfl⟩

Premises used: strictMono_nat_of_lt_succ, And.intro, Exists.intro, Nat.recOn
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
g : (x : α) → α
hg : ∀ (x : α), x < g x
⊢ ∃ (f : ℕ → α), StrictMono f ∧ f 0 = a

Tactic:
exact ⟨fun n ↦ Nat.recOn n a fun _ ↦ g, strictMono_nat_of_lt_succ fun n ↦ hg _, rfl⟩
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : NoMinOrder α
a : α
⊢ ∃ (f : ℕ → α), StrictAnti f ∧ f 0 = a

Tactic:
exists_strictMono' (OrderDual.toDual a)

Premises used: OrderDual.toDual, Nat.exists_strictMono', StrictAnti, OrderDual, DFunLike.coe
-- Module: Mathlib.Order.Monotone.Basic
Goal:
P : ℕ → Prop
h : ∀ (N : ℕ), ∃ (n : ℕ), n > N ∧ P n
⊢ NoMaxOrder { n : ℕ // P n }

Tactic:
have : NoMaxOrder {n // P n} :=
    ⟨fun n ↦ Exists.intro ⟨(h n.1).choose, (h n.1).choose_spec.2⟩ (h n.1).choose_spec.1⟩
-- Module: Mathlib.Order.Monotone.Basic
Goal:
P : ℕ → Prop
h : ∀ (N : ℕ), ∃ (n : ℕ), n > N ∧ P n
this : NoMaxOrder { n : ℕ // P n }
obtain :
  ∀ (f : ℕ → { n : ℕ // P n }) (hf : StrictMono f),
    f 0 = Subtype.mk (p := fun (n : ℕ) ↦ P n) (Exists.choose (p := fun (n : ℕ) ↦ n > 0 ∧ P n) ⋯) ⋯ →
      ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

Tactic:
obtain ⟨f, hf, _⟩ := Nat.exists_strictMono' (⟨(h 0).choose, (h 0).choose_spec.2⟩ : {n // P n})

Premises used: Nat.exists_strictMono', Exists.choose_spec, Subtype.mk, And.right, Exists.choose, OfNat.ofNat
-- Module: Mathlib.Order.Monotone.Basic
Goal:
P : ℕ → Prop
h : ∀ (N : ℕ), ∃ (n : ℕ), n > N ∧ P n
this : NoMaxOrder { n : ℕ // P n }
f : ℕ → { n : ℕ // P n }
hf : StrictMono f
right : f 0 = Subtype.mk (p := fun (n : ℕ) ↦ P n) (Exists.choose (p := fun (n : ℕ) ↦ n > 0 ∧ P n) ⋯) ⋯
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

Tactic:
Exists.intro (fun n ↦ (f n).1) ⟨hf, fun n ↦ (f n).2⟩

Premises used: And.intro, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.Order.Monotone.Basic
Goal:
P : ℕ → Prop
h : ∀ (N : ℕ), ∃ (n : ℕ), n > N ∧ P n
this : NoMaxOrder { n : ℕ // P n }
f : ℕ → { n : ℕ // P n }
hf : StrictMono f
right : f 0 = Subtype.mk (p := fun (n : ℕ) ↦ P n) (Exists.choose (p := fun (n : ℕ) ↦ n > 0 ∧ P n) ⋯) ⋯
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

Tactic:
exact Exists.intro (fun n ↦ (f n).1) ⟨hf, fun n ↦ (f n).2⟩

Premises used: Exists.intro, Subtype.val
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMaxOrder α
⊢ ∃ (f : ℕ → α), StrictMono f

Tactic:
let ⟨a⟩ := ‹Nonempty α›
  let ⟨f, hf, _⟩ := exists_strictMono' a
  ⟨f, hf⟩

Premises used: Nat.exists_strictMono', StrictMono, Exists, _private.0.Nat.exists_strictMono.match_2, Exists.intro, _private.0.Nat.exists_strictMono.match_1
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMinOrder α
⊢ ∃ (f : ℕ → α), StrictAnti f

Tactic:
exists_strictMono αᵒᵈ

Premises used: Nat.exists_strictMono, StrictAnti, OrderDual
-- Module: Mathlib.Order.Monotone.Basic
Goal:
⊢ Monotone (β := ℕ) fun (n : ℕ) ↦ n ^ n

Tactic:
monotone_nat_of_le_succ fun n ↦ ?_

Premises used: monotone_nat_of_le_succ
-- Module: Mathlib.Order.Monotone.Basic
Goal:
refine : ∀ (n : ℕ), n ^ n ≤ (n + 1) ^ (n + 1)
⊢ Monotone (β := ℕ) fun (n : ℕ) ↦ n ^ n

Tactic:
refine monotone_nat_of_le_succ fun n ↦ ?_

Premises used: monotone_nat_of_le_succ
-- Module: Mathlib.Order.Monotone.Basic
Goal:
n : ℕ
rw : n ^ n ≤ (n + 1) ^ n * (n + 1)
⊢ n ^ n ≤ (n + 1) ^ (n + 1)

Tactic:
rw [Nat.pow_succ]

Premises used: Nat.pow_succ
-- Module: Mathlib.Order.Monotone.Basic
Goal:
n : ℕ
⊢ n ^ n ≤ (n + 1) ^ n * (n + 1)

Tactic:
(Nat.pow_le_pow_left n.le_succ _).trans (Nat.le_mul_of_pos_right _ n.succ_pos)

Premises used: Nat.le_mul_of_pos_right, Nat.le_succ, Nat.succ_pos, LE.le.trans, Nat.pow_le_pow_left
-- Module: Mathlib.Order.Monotone.Basic
Goal:
n : ℕ
⊢ n ^ n ≤ (n + 1) ^ n * (n + 1)

Tactic:
exact (Nat.pow_le_pow_left n.le_succ _).trans (Nat.le_mul_of_pos_right _ n.succ_pos)

Premises used: Nat.le_mul_of_pos_right, Nat.le_succ, Nat.succ_pos, LE.le.trans, Nat.pow_le_pow_left
-- Module: Mathlib.Order.Monotone.Basic
Goal:
⊢ MonotoneOn (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.fst ^ p.snd) {p : ℕ × ℕ | p.fst ≠ 0}

Tactic:
fun _p _ _q hq hpq ↦
  (Nat.pow_le_pow_left hpq.1 _).trans (Nat.pow_le_pow_right (Nat.pos_iff_ne_zero.2 hq) hpq.2)

Premises used: Iff.mpr, Nat.pos_iff_ne_zero, Nat.pow_le_pow_right, MonotoneOn, And.right, And.left, LE.le.trans, Prod.snd, Nat.pow_le_pow_left
-- Module: Mathlib.Order.Monotone.Basic
Goal:
⊢ StrictMonoOn (β := ℕ) (fun (n : ℕ) ↦ n ^ n) {n : ℕ | n ≠ 0}

Tactic:
fun _m hm _n hn hmn ↦
    (Nat.pow_lt_pow_left hmn hm).trans_le (Nat.pow_le_pow_right (Nat.pos_iff_ne_zero.2 hn) hmn.le)

Premises used: Iff.mpr, Nat.pos_iff_ne_zero, LT.lt.le, Nat.pow_le_pow_right, LT.lt.trans_le, Nat.pow_lt_pow_left, StrictMonoOn
-- Module: Mathlib.Order.Monotone.Basic
Goal:
β : Type v
r : β → β → Prop
inst : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a b : ℤ
hab : a < b
rcases : ∀ (n : ℕ) (hab : a < a + (↑n.succ : ℤ)), r (f a) (f (a + (↑n.succ : ℤ)))
⊢ r (f a) (f b)

Tactic:
rcases lt.dest hab with ⟨n, rfl⟩

Premises used: Int.lt.dest, rfl
-- Module: Mathlib.Order.Monotone.Basic
Goal:
β : Type v
r : β → β → Prop
inst : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
zero : r (f a) (f (a + 1))
⊢ r (f a) (f (a + (↑(Nat.succ 0) : ℤ)))

Tactic:
rw [Int.ofNat_one]

Premises used: Int.ofNat_one
-- Module: Mathlib.Order.Monotone.Basic
Goal:
β : Type v
r : β → β → Prop
inst : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
⊢ r (f a) (f (a + 1))

Tactic:
apply h
-- Module: Mathlib.Order.Monotone.Basic
Goal:
β : Type v
r : β → β → Prop
inst : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
ihn : r (f a) (f (a + (↑n.succ : ℤ)))
succ : r (f a) (f (a + (↑(n + 1) : ℤ) + 1))
⊢ r (f a) (f (a + (↑(n + 1).succ : ℤ)))

Tactic:
rw [Int.natCast_succ, ← Int.add_assoc]

Premises used: Int.add_assoc, Int.natCast_succ
-- Module: Mathlib.Order.Monotone.Basic
Goal:
β : Type v
r : β → β → Prop
inst : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
ihn : r (f a) (f (a + (↑n.succ : ℤ)))
⊢ r (f a) (f (a + (↑(n + 1) : ℤ) + 1))

Tactic:
_root_.trans ihn (h _)

Premises used: trans
-- Module: Mathlib.Order.Monotone.Basic
Goal:
β : Type v
r : β → β → Prop
inst : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
ihn : r (f a) (f (a + (↑n.succ : ℤ)))
⊢ r (f a) (f (a + (↑(n + 1) : ℤ) + 1))

Tactic:
exact _root_.trans ihn (h _)

Premises used: trans
-- Module: Mathlib.Order.Monotone.Basic
Goal:
β : Type v
r : β → β → Prop
inst : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
zero : r (f a) (f (a + (↑(Nat.succ 0) : ℤ)))
succ : ∀ (n : ℕ) (ihn : r (f a) (f (a + (↑n.succ : ℤ)))), r (f a) (f (a + (↑(n + 1).succ : ℤ)))
⊢ r (f a) (f (a + (↑n.succ : ℤ)))

Tactic:
induction n with
  | zero => rw [Int.ofNat_one]; apply h
  | succ n ihn => rw [Int.natCast_succ, ← Int.add_assoc]; exact _root_.trans ihn (h _)

Premises used: Int.add_assoc, Int.natCast_succ, Int.ofNat_one
-- Module: Mathlib.Order.Monotone.Basic
Goal:
β : Type v
r : β → β → Prop
inst : Std.Refl r
inst_1 : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a b : ℤ
hab : a ≤ b
⊢ r (f a) (f b)

Tactic:
hab.eq_or_lt.elim (fun h ↦ h ▸ refl _) fun h' ↦ Int.rel_of_forall_rel_succ_of_lt r h h'

Premises used: Int.rel_of_forall_rel_succ_of_lt, LE.le.eq_or_lt, Eq.rec, Or.elim, refl
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℤ → α
hf : ∀ (n : ℤ), f n ≤ f (n + 1)
⊢ Monotone f

Tactic:
Int.rel_of_forall_rel_succ_of_le (· ≤ ·) hf

Premises used: Monotone, LE.le, Int.rel_of_forall_rel_succ_of_le
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℤ → α
hf : ∀ (n : ℤ), f (n + 1) ≤ f n
⊢ Antitone f

Tactic:
Int.rel_of_forall_rel_succ_of_le (· ≥ ·) hf

Premises used: GE.ge, Antitone, Int.rel_of_forall_rel_succ_of_le
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℤ → α
hf : ∀ (n : ℤ), f n < f (n + 1)
⊢ StrictMono f

Tactic:
Int.rel_of_forall_rel_succ_of_lt (· < ·) hf

Premises used: Int.rel_of_forall_rel_succ_of_lt, StrictMono, LT.lt
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℤ → α
hf : ∀ (n : ℤ), f (n + 1) < f n
⊢ StrictAnti f

Tactic:
Int.rel_of_forall_rel_succ_of_lt (· > ·) hf

Premises used: Int.rel_of_forall_rel_succ_of_lt, GT.gt, StrictAnti
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMinOrder α
inst_3 : NoMaxOrder α
inhabit : ∀ (inhabited_h : Inhabited α), ∃ (f : ℤ → α), StrictMono f
⊢ ∃ (f : ℤ → α), StrictMono f

Tactic:
inhabit α
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMinOrder α
inst_3 : NoMaxOrder α
inhabited_h : Inhabited α
rcases : ∀ (f : ℕ → α) (hf : StrictMono f) (hf₀ : f 0 = default), ∃ (f : ℤ → α), StrictMono f
⊢ ∃ (f : ℤ → α), StrictMono f

Tactic:
rcases Nat.exists_strictMono' (default : α) with ⟨f, hf, hf₀⟩

Premises used: Inhabited.default, Nat.exists_strictMono'
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMinOrder α
inst_3 : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
rcases : ∀ (g : ℕ → α) (hg : StrictAnti g) (hg₀ : g 0 = default), ∃ (f : ℤ → α), StrictMono f
⊢ ∃ (f : ℤ → α), StrictMono f

Tactic:
rcases Nat.exists_strictAnti' (default : α) with ⟨g, hg, hg₀⟩

Premises used: Nat.exists_strictAnti', Inhabited.default
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMinOrder α
inst_3 : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ ∃ (f : ℤ → α), StrictMono f

Tactic:
⟨fun n ↦ Int.casesOn n f fun n ↦ g (n + 1), strictMono_int_of_lt_succ ?_⟩

Premises used: Int.casesOn, strictMono_int_of_lt_succ, Exists.intro
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMinOrder α
inst_3 : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
refine :
  ∀ (n : ℤ),
    LT.lt.{u} (α := α) (casesOn (motive := fun (x : ℤ) ↦ α) n f fun (n : ℕ) ↦ g (n + 1) : α)
      (casesOn (motive := fun (x : ℤ) ↦ α) (n + 1) f fun (n : ℕ) ↦ g (n + 1) : α)
⊢ ∃ (f : ℤ → α), StrictMono f

Tactic:
refine ⟨fun n ↦ Int.casesOn n f fun n ↦ g (n + 1), strictMono_int_of_lt_succ ?_⟩
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMinOrder α
inst_3 : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
n : ℕ
⊢ LT.lt.{u} (α := α) (casesOn (motive := fun (x : ℤ) ↦ α) (ofNat n) f fun (n : ℕ) ↦ g (n + 1) : α)
    (casesOn (motive := fun (x : ℤ) ↦ α) (ofNat n + 1) f fun (n : ℕ) ↦ g (n + 1) : α)

Tactic:
hf n.lt_succ_self

Premises used: Nat.lt_succ_self
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMinOrder α
inst_3 : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
n : ℕ
⊢ LT.lt.{u} (α := α) (casesOn (motive := fun (x : ℤ) ↦ α) (ofNat n) f fun (n : ℕ) ↦ g (n + 1) : α)
    (casesOn (motive := fun (x : ℤ) ↦ α) (ofNat n + 1) f fun (n : ℕ) ↦ g (n + 1) : α)

Tactic:
exact hf n.lt_succ_self

Premises used: Nat.lt_succ_self
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMinOrder α
inst_3 : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
negSucc : g 1 < f 0
⊢ LT.lt.{u} (α := α) (casesOn (motive := fun (x : ℤ) ↦ α) -[0+1] f fun (n : ℕ) ↦ g (n + 1) : α)
    (casesOn (motive := fun (x : ℤ) ↦ α) (-[0+1] + 1) f fun (n : ℕ) ↦ g (n + 1) : α)

Tactic:
change g 1 < f 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMinOrder α
inst_3 : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
negSucc : g 1 < g 0
⊢ g 1 < f 0

Tactic:
rw [hf₀, ← hg₀]
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMinOrder α
inst_3 : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ g 1 < g 0

Tactic:
hg Nat.zero_lt_one

Premises used: Nat.zero_lt_one
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMinOrder α
inst_3 : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ g 1 < g 0

Tactic:
exact hg Nat.zero_lt_one

Premises used: Nat.zero_lt_one
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMinOrder α
inst_3 : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
n : ℕ
⊢ LT.lt.{u} (α := α) (casesOn (motive := fun (x : ℤ) ↦ α) -[n + 1+1] f fun (n : ℕ) ↦ g (n + 1) : α)
    (casesOn (motive := fun (x : ℤ) ↦ α) (-[n + 1+1] + 1) f fun (n : ℕ) ↦ g (n + 1) : α)

Tactic:
hg (Nat.lt_succ_self _)

Premises used: Nat.lt_succ_self
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMinOrder α
inst_3 : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
n : ℕ
⊢ LT.lt.{u} (α := α) (casesOn (motive := fun (x : ℤ) ↦ α) -[n + 1+1] f fun (n : ℕ) ↦ g (n + 1) : α)
    (casesOn (motive := fun (x : ℤ) ↦ α) (-[n + 1+1] + 1) f fun (n : ℕ) ↦ g (n + 1) : α)

Tactic:
exact hg (Nat.lt_succ_self _)

Premises used: Nat.lt_succ_self
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMinOrder α
inst_3 : NoMaxOrder α
⊢ ∃ (f : ℤ → α), StrictAnti f

Tactic:
exists_strictMono αᵒᵈ

Premises used: StrictAnti, Int.exists_strictMono, OrderDual
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℕ → α
hf : Monotone f
n a : ℕ
h1 : f n < f a
h2 : f a < f (n + 1)
⊢ False

Tactic:
(hf.reflect_lt h1).not_ge (Nat.le_of_lt_succ <| hf.reflect_lt h2)

Premises used: Monotone.reflect_lt, Nat.le_of_lt_succ, LT.lt.not_ge
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℕ → α
hf : Monotone f
n a : ℕ
h1 : f n < f a
h2 : f a < f (n + 1)
⊢ False

Tactic:
exact (hf.reflect_lt h1).not_ge (Nat.le_of_lt_succ <| hf.reflect_lt h2)

Premises used: Monotone.reflect_lt, Nat.le_of_lt_succ, LT.lt.not_ge
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℕ → α
hf : Antitone f
n a : ℕ
h1 : f (n + 1) < f a
h2 : f a < f n
⊢ False

Tactic:
(hf.reflect_lt h2).not_ge (Nat.le_of_lt_succ <| hf.reflect_lt h1)

Premises used: Antitone.reflect_lt, Nat.le_of_lt_succ, LT.lt.not_ge
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℕ → α
hf : Antitone f
n a : ℕ
h1 : f (n + 1) < f a
h2 : f a < f n
⊢ False

Tactic:
exact (hf.reflect_lt h2).not_ge (Nat.le_of_lt_succ <| hf.reflect_lt h1)

Premises used: Antitone.reflect_lt, Nat.le_of_lt_succ, LT.lt.not_ge
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℤ → α
hf : Monotone f
n a : ℤ
h1 : f n < f a
h2 : f a < f (n + 1)
⊢ False

Tactic:
(hf.reflect_lt h1).not_ge (Int.le_of_lt_add_one <| hf.reflect_lt h2)

Premises used: Int.le_of_lt_add_one, Monotone.reflect_lt, LT.lt.not_ge
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℤ → α
hf : Monotone f
n a : ℤ
h1 : f n < f a
h2 : f a < f (n + 1)
⊢ False

Tactic:
exact (hf.reflect_lt h1).not_ge (Int.le_of_lt_add_one <| hf.reflect_lt h2)

Premises used: Int.le_of_lt_add_one, Monotone.reflect_lt, LT.lt.not_ge
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℤ → α
hf : Antitone f
n a : ℤ
h1 : f (n + 1) < f a
h2 : f a < f n
⊢ False

Tactic:
(hf.reflect_lt h2).not_ge (Int.le_of_lt_add_one <| hf.reflect_lt h1)

Premises used: Antitone.reflect_lt, Int.le_of_lt_add_one, LT.lt.not_ge
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℤ → α
hf : Antitone f
n a : ℤ
h1 : f (n + 1) < f a
h2 : f a < f n
⊢ False

Tactic:
exact (hf.reflect_lt h2).not_ge (Int.le_of_lt_add_one <| hf.reflect_lt h1)

Premises used: Antitone.reflect_lt, Int.le_of_lt_add_one, LT.lt.not_ge
-- Module: Mathlib.Order.Monotone.Basic
Goal:
f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfb : ∀ (m : ℕ), f m ≤ b
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
contrapose! : ∀ (hfb : ∀ (m : ℕ) (_ : m ≤ b), f m ≠ f (m + 1)), ∃ (m : ℕ), b < f m
⊢ ∃ (m : ℕ), m ≤ b ∧ f m = f (m + 1)

Tactic:
contrapose! hfb
-- Module: Mathlib.Order.Monotone.Basic
Goal:
f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
hfb : ∀ (m : ℕ) (_ : m ≤ b), f m ≠ f (m + 1)
⊢ ∃ (m : ℕ), b < f m

Tactic:
⟨b + 1, strictMono _ le_rfl⟩

Premises used: le_rfl, HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Order.Monotone.Basic
Goal:
f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
hfb : ∀ (m : ℕ) (_ : m ≤ b), f m ≠ f (m + 1)
⊢ ∃ (m : ℕ), b < f m

Tactic:
exact ⟨b + 1, strictMono _ le_rfl⟩
-- Module: Mathlib.Order.Monotone.Basic
Goal:
f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfb : ∀ (m : ℕ), f m ≤ b
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
obtain : ∀ (m : ℕ) (hmb : m ≤ b) (hm : f m = f (m + 1)), f n = f b
⊢ f n = f b

Tactic:
obtain ⟨m, hmb, hm⟩ : ∃ m ≤ b, f m = f (m + 1) := by
    contrapose! hfb
    let rec strictMono : ∀ m ≤ b + 1, m ≤ f m
    | 0, _ => Nat.zero_le _
    | m + 1, hmb => (strictMono _ <| m.le_succ.trans hmb).trans_lt <| (hfmono m.le_succ).lt_of_ne <|
        hfb _ <| Nat.le_of_succ_le_succ hmb
    exact ⟨b + 1, strictMono _ le_rfl⟩
-- Module: Mathlib.Order.Monotone.Basic
Goal:
f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfb : ∀ (m : ℕ), f m ≤ b
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
m : ℕ
hmb : m ≤ b
hm : f m = f (m + 1)
⊢ ∀ (k : ℕ), f (m + k) = f (m + k + 1) ∧ f (m + k) = f m

Tactic:
replace key : ∀ k : ℕ, f (m + k) = f (m + k + 1) ∧ f (m + k) = f m := fun k =>
    Nat.rec ⟨hm, rfl⟩ (fun k ih => ⟨hfstab _ ih.1, ih.1.symm.trans ih.2⟩) k
-- Module: Mathlib.Order.Monotone.Basic
Goal:
f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfb : ∀ (m : ℕ), f m ≤ b
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
m : ℕ
hmb : m ≤ b
hm : f m = f (m + 1)
key : ∀ (k : ℕ), f (m + k) = f (m + k + 1) ∧ f (m + k) = f m
⊢ ∀ (k : ℕ), k ≥ m → f k = f m

Tactic:
replace key : ∀ k ≥ m, f k = f m := fun k hk =>
    (congr_arg f (Nat.add_sub_of_le hk)).symm.trans (key (k - m)).2