awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
refine_1 : ∀ (a b c : α) (h : f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c), a ≠ b
⊢ (∃ (a : α), ∃ (b : α), ∃ (c : α), (a ≤ b ∧ b ≤ c) ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)) ↔
    ∃ (a : α), ∃ (b : α), ∃ (c : α), (a < b ∧ b < c) ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
have refine_2 : ∀ (a b c : α) (h : f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c), b ≠ c
Tactic: refine exists₃_congr (fun a b c ↦ and_congr_left <|
    fun h ↦ (Ne.le_iff_lt ?_).and <| Ne.le_iff_lt ?_)
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
β : Type v
r : β → β → Prop
inst : IsTrans β r
f : ℕ → β
a : ℕ
h : ∀ (n : ℕ), a ≤ n → r (f n) (f (n + 1))
b c : ℕ
hab : a ≤ b
hbc : b < c
⊢ r (f b) (f c)
have refl : r (f b) (f b.succ)
Tactic: induction hbc with
  | refl => exact h _ hab
  | step b_lt_k r_b_k => exact _root_.trans r_b_k (h _ (hab.trans_lt b_lt_k).le)
Cleared hypotheses: hbc
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
β : Type v
r : β → β → Prop
inst : IsTrans β r
f : ℕ → β
a : ℕ
h : ∀ (n : ℕ), a ≤ n → r (f n) (f (n + 1))
b c : ℕ
hab : a ≤ b
hbc : b < c
refl : r (f b) (f b.succ)
⊢ r (f b) (f c)
have step : ∀ {m : ℕ} (b_lt_k : b.succ.le m) (r_b_k : r (f b) (f m)), r (f b) (f m.succ)
Tactic: induction hbc with
  | refl => exact h _ hab
  | step b_lt_k r_b_k => exact _root_.trans r_b_k (h _ (hab.trans_lt b_lt_k).le)
Cleared hypotheses: hbc
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
inst : Preorder α
f : ℕ → α
k : ℕ
⊢ (Monotone.{0, u} (β := α) fun (n : ℕ) ↦ f (n + k)) ↔ MonotoneOn f {x : ℕ | k ≤ x}
have 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
Tactic: refine ⟨fun h x hx y hy hle ↦ ?_, fun h x y hle ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
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
⊢ (Monotone.{0, u} (β := α) fun (n : ℕ) ↦ f (n + k)) ↔ MonotoneOn f {x : ℕ | k ≤ x}
have 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)
Tactic: refine ⟨fun h x hx y hy hle ↦ ?_, fun h x y hle ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
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
⊢ f x ≤ f y
have refine_1 : f (x - k + k) ≤ f (y - k + k)
Tactic: rw [← Nat.sub_add_cancel hx, ← Nat.sub_add_cancel hy]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (hypothesis)
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
⊢ f (x - k + k) ≤ f (y - k + k)
have hle₁ : x - k ≤ y - k
Tactic: rw [← Nat.sub_le_sub_iff_right hy] at hle
Cleared hypotheses: hle
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
inst : Preorder α
f : ℕ → α
k : ℕ
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)
have refine_2 : ∀ (hle : x + k ≤ y + k), 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
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
⊢ ∃ (f : ℕ → α), StrictMono f ∧ f 0 = a
have choose : ∀ (g : (x : α) → α) (hg : ∀ (x : α), x < g x), ∃ (f : ℕ → α), StrictMono f ∧ f 0 = a
Tactic: choose g hg using fun x : α ↦ exists_gt x
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (hypothesis)
Goal:
P : ℕ → Prop
h : ∀ (N : ℕ), ∃ (n : ℕ), n > N ∧ P n
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
have this : 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⟩
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
P : ℕ → Prop
h : ∀ (N : ℕ), ∃ (n : ℕ), n > N ∧ P n
this : NoMaxOrder { n : ℕ // P n }
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
have 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) sorry) sorry →
    ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
Tactic: obtain ⟨f, hf, _⟩ := Nat.exists_strictMono' (⟨(h 0).choose, (h 0).choose_spec.2⟩ : {n // P n})
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
⊢ Monotone (β := ℕ) fun (n : ℕ) ↦ n ^ n
have refine : ∀ (n : ℕ), n ^ n ≤ (n + 1) ^ (n + 1)
Tactic: refine monotone_nat_of_le_succ fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
n : ℕ
⊢ n ^ n ≤ (n + 1) ^ (n + 1)
have rw : n ^ n ≤ (n + 1) ^ n * (n + 1)
Tactic: rw [Nat.pow_succ]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
β : Type v
r : β → β → Prop
inst : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a b : ℤ
hab : a < b
⊢ r (f a) (f b)
have rcases : ∀ (n : ℕ) (hab : a < a + (↑n.succ : ℤ)), r (f a) (f (a + (↑n.succ : ℤ)))
Tactic: rcases lt.dest hab with ⟨n, rfl⟩
Cleared hypotheses: b, hab
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
β : Type v
r : β → β → Prop
inst : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
⊢ r (f a) (f (a + (↑(Nat.succ 0) : ℤ)))
have zero : r (f a) (f (a + 1))
Tactic: rw [Int.ofNat_one]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
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).succ : ℤ)))
have succ : r (f a) (f (a + (↑(n + 1) : ℤ) + 1))
Tactic: rw [Int.natCast_succ, ← Int.add_assoc]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
β : Type v
r : β → β → Prop
inst : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
⊢ r (f a) (f (a + (↑n.succ : ℤ)))
have zero : r (f a) (f (a + (↑(Nat.succ 0) : ℤ)))
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 _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
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) : ℤ)))
⊢ r (f a) (f (a + (↑n.succ : ℤ)))
have succ : ∀ (n : ℕ) (ihn : r (f a) (f (a + (↑n.succ : ℤ)))), r (f a) (f (a + (↑(n + 1).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 _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMinOrder α
inst_3 : NoMaxOrder α
⊢ ∃ (f : ℤ → α), StrictMono f
have inhabit : ∀ (inhabited_h : Inhabited α), ∃ (f : ℤ → α), StrictMono f
Tactic: inhabit α
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMinOrder α
inst_3 : NoMaxOrder α
inhabited_h : Inhabited α
⊢ ∃ (f : ℤ → α), StrictMono f
have rcases : ∀ (f : ℕ → α) (hf : StrictMono f) (hf₀ : f 0 = default), ∃ (f : ℤ → α), StrictMono f
Tactic: rcases Nat.exists_strictMono' (default : α) with ⟨f, hf, hf₀⟩
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
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
⊢ ∃ (f : ℤ → α), StrictMono f
have rcases : ∀ (g : ℕ → α) (hg : StrictAnti g) (hg₀ : g 0 = default), ∃ (f : ℤ → α), StrictMono f
Tactic: rcases Nat.exists_strictAnti' (default : α) with ⟨g, hg, hg₀⟩
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
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
have 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) : α)
Tactic: refine ⟨fun n ↦ Int.casesOn n f fun n ↦ g (n + 1), strictMono_int_of_lt_succ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
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
⊢ 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) : α)
have negSucc : g 1 < f 0
Tactic: change g 1 < f 0
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
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 < f 0
have negSucc : g 1 < g 0
Tactic: rw [hf₀, ← hg₀]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
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 : ℕ), m ≤ b ∧ f m = f (m + 1)
have contrapose! : ∀ (hfb : ∀ (m : ℕ) (_ : m ≤ b), f m ≠ f (m + 1)), ∃ (m : ℕ), b < f m
Tactic: contrapose! hfb
Cleared hypotheses: hfb
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
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
⊢ f n = f b
have obtain : ∀ (m : ℕ) (hmb : m ≤ b) (hm : f m = f (m + 1)), 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⟩
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (hypothesis)
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)
⊢ f n = f b
have key : ∀ (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
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (hypothesis)
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
⊢ f n = f b
have key₁ : ∀ (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
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ} (hfmono : Antitone f) (hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) (h : f 0 = m),
        ∃ (n : ℕ), n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
⊢ ∃ (n_1 : ℕ), n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1
have pos : ∀ (heq : f 0 = f 1), ∃ (n_1 : ℕ), n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1
Tactic: by_cases heq : f 0 = f 1
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ} (hfmono : Antitone f) (hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) (h : f 0 = m),
        ∃ (n : ℕ), n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
pos : ∀ (heq : f 0 = f 1), ∃ (n_1 : ℕ), n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1
⊢ ∃ (n_1 : ℕ), n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1
have neg : ∀ (heq : ¬f 0 = f 1), ∃ (n_1 : ℕ), n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1
Tactic: by_cases heq : f 0 = f 1
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (hypothesis)
Goal:
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ} (hfmono : Antitone f) (hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) (h : f 0 = m),
        ∃ (n : ℕ), n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : f 0 = f 1
⊢ ∃ (n_1 : ℕ), n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1
have flat : ∀ (j : ℕ), f j = f (j + 1)
Tactic: have flat (j : ℕ) : f j = f (j + 1) := by induction j with grind
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ} (hfmono : Antitone f) (hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) (h : f 0 = m),
        ∃ (n : ℕ), n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : f 0 = f 1
flat : ∀ (j : ℕ), f j = f (j + 1)
m : ℕ
h_1 : 0 ≤ m
⊢ f m = f 0
have zero : LE.le (α := ℕ) 0 0 → f 0 = f 0
Tactic: induction m with grind
Cleared hypotheses: m, h_1
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ} (hfmono : Antitone f) (hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) (h : f 0 = m),
        ∃ (n : ℕ), n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : f 0 = f 1
flat : ∀ (j : ℕ), f j = f (j + 1)
m : ℕ
h_1 : 0 ≤ m
zero : LE.le (α := ℕ) 0 0 → f 0 = f 0
⊢ f m = f 0
have succ : ∀ (n : ℕ), (0 ≤ n → f n = f 0) → 0 ≤ n + 1 → f (n + 1) = f 0
Tactic: induction m with grind
Cleared hypotheses: m, h_1
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (hypothesis)
Goal:
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ} (hfmono : Antitone f) (hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) (h : f 0 = m),
        ∃ (n : ℕ), n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : ¬f 0 = f 1
⊢ ∃ (n_1 : ℕ), n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1
have hlt : f 1 < f 0
Tactic: have hlt : f 1 < f 0 := (hfmono (Nat.le_succ 0)).lt_of_ne' heq
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (hypothesis)
Goal:
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ} (hfmono : Antitone f) (hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) (h : f 0 = m),
        ∃ (n : ℕ), n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : ¬f 0 = f 1
hlt : f 1 < f 0
g : (i : ℕ) → ℕ := fun (i : ℕ) ↦ f (i + 1)
⊢ ∃ (n_1 : ℕ), n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1
have hg_anti : Antitone g
Tactic: have hg_anti : Antitone g := by grind [Antitone]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ} (hfmono : Antitone f) (hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) (h : f 0 = m),
        ∃ (n : ℕ), n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : ¬f 0 = f 1
hlt : f 1 < f 0
g : (i : ℕ) → ℕ := fun (i : ℕ) ↦ f (i + 1)
hg_anti : Antitone g
⊢ ∃ (n_1 : ℕ), n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1
have neg : ∀ (p : ℕ) (hp : p ≤ f 1) (hp' : ∀ (m : ℕ), p ≤ m → g m = g p), ∃ (n_1 : ℕ), n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1
Tactic: obtain ⟨p, hp, hp'⟩ := ih (f 1) (by grind) hg_anti (by grind) rfl
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ} (hfmono : Antitone f) (hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) (h : f 0 = m),
        ∃ (n : ℕ), n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : ¬f 0 = f 1
hlt : f 1 < f 0
g : (i : ℕ) → ℕ := fun (i : ℕ) ↦ f (i + 1)
hg_anti : Antitone g
p : ℕ
hp : p ≤ f 1
hp' : ∀ (m : ℕ), p ≤ m → g m = g p
⊢ ∃ (n_1 : ℕ), n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1
have neg : ∀ (m : ℕ) (hm : p + 1 ≤ m), f m = f (p + 1)
Tactic: refine ⟨p + 1, by omega, fun m hm => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (hypothesis)
Goal:
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ} (hfmono : Antitone f) (hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) (h : f 0 = m),
        ∃ (n : ℕ), n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
heq : ¬f 0 = f 1
hlt : f 1 < f 0
g : (i : ℕ) → ℕ := fun (i : ℕ) ↦ f (i + 1)
hg_anti : Antitone g
p : ℕ
hp : p ≤ f 1
hp' : ∀ (m : ℕ), p ≤ m → g m = g p
m : ℕ
hm : p + 1 ≤ m
⊢ f m = f (p + 1)
have hp'₁ : g (m - 1) = g p
Tactic: specialize hp' (m - 1) (by lia)
Cleared hypotheses: hp'
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
⊢ ∃ (n : ℕ), n ≤ f 0 ∧ ∀ (m : ℕ), n ≤ m → f m = f n
have induction : ∀ (x : ℕ) (h : f 0 = x), ∃ (n : ℕ), n ≤ x ∧ ∀ (m : ℕ), n ≤ m → f m = f n
Tactic: induction h : f 0 using Nat.strongRecOn generalizing f with
  | ind n ih =>
    by_cases heq : f 0 = f 1
    · have flat (j : ℕ) : f j = f (j + 1) := by induction j with grind
      exact ⟨0, Nat.zero_le _, fun m _ => by induction m with grind⟩
    · have hlt : f 1 < f 0 := (hfmono (Nat.le_succ 0)).lt_of_ne' heq
      let g (i : ℕ) := f (i + 1)
      have hg_anti : Antitone g := by grind [Antitone]
      obtain ⟨p, hp, hp'⟩ := ih (f 1) (by grind) hg_anti (by grind) rfl
      refine ⟨p + 1, by omega, fun m hm => ?_⟩
      specialize hp' (m - 1) (by lia)
      grind
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
f : ℕ → ℕ
mono_f : Monotone f
hc : ∀ (n : ℕ), f n ≤ 0
⊢ ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
have w : ℕ
Tactic: use 0, 0, fun n _ ↦ Nat.eq_zero_of_le_zero (hc n)
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
f : ℕ → ℕ
mono_f : Monotone f
hc : ∀ (n : ℕ), f n ≤ 0
w w₁ : ℕ
⊢ ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
have h : ∀ (n : ℕ), n ≥ 0 → f n = 0
Tactic: use 0, 0, fun n _ ↦ Nat.eq_zero_of_le_zero (hc n)
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : ∀ (hc : ∀ (n : ℕ), f n ≤ c), ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
hc : ∀ (n : ℕ), f n ≤ c + 1
pos : ∀ (h : ∀ (n : ℕ), f n ≤ c), ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
⊢ ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
have neg : ∀ (h : ∃ (n : ℕ), c < f n), ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
Tactic: by_cases! h : ∀ n, f n ≤ c
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : ∀ (hc : ∀ (n : ℕ), f n ≤ c), ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
hc : ∀ (n : ℕ), f n ≤ c + 1
h : ∃ (n : ℕ), c < f n
⊢ ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
have neg : ∀ (N : ℕ) (hN : c < f N), ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
Tactic: obtain ⟨N, hN⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (hypothesis)
Goal:
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : ∀ (hc : ∀ (n : ℕ), f n ≤ c), ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
hc : ∀ (n : ℕ), f n ≤ c + 1
N : ℕ
hN : c < f N
⊢ f N = c + 1
have hc₁ : f N ≤ c + 1
Tactic: specialize hc N
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (hypothesis)
Goal:
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : ∀ (hc : ∀ (n : ℕ), f n ≤ c), ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
hc : ∀ (n : ℕ), f n ≤ c + 1
N : ℕ
hN : c < f N
⊢ ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
have hN₁ : f N = c + 1
Tactic: replace hN : f N = c + 1 := by specialize hc N; lia
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : ∀ (hc : ∀ (n : ℕ), f n ≤ c), ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
hc : ∀ (n : ℕ), f n ≤ c + 1
N : ℕ
hN : f N = c + 1
⊢ ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
have h : ∀ (n : ℕ), n ≥ N → f n = c + 1
Tactic: use c + 1, N
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (hypothesis)
Goal:
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : ∀ (hc : ∀ (n : ℕ), f n ≤ c), ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
hc : ∀ (n : ℕ), f n ≤ c + 1
N : ℕ
hN : f N = c + 1
n : ℕ
hn : n ≥ N
⊢ f n = c + 1
have mono_f₁ : f N ≤ f n
Tactic: specialize mono_f hn
Cleared hypotheses: mono_f
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (hypothesis)
Goal:
f : ℕ → ℕ
c : ℕ
ih : ∀ (hc : ∀ (n : ℕ), f n ≤ c), ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
hc : ∀ (n : ℕ), f n ≤ c + 1
N : ℕ
hN : f N = c + 1
n : ℕ
hn : n ≥ N
mono_f : f N ≤ f n
⊢ f n = c + 1
have hc₁ : f n ≤ c + 1
Tactic: specialize hc n
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
hc : ∀ (n : ℕ), f n ≤ c
⊢ ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
have zero : ∀ (hc : ∀ (n : ℕ), f n ≤ 0), ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
Tactic: induction c with
  | zero => use 0, 0, fun n _ ↦ Nat.eq_zero_of_le_zero (hc n)
  | succ c ih =>
    by_cases! h : ∀ n, f n ≤ c
    · exact ih h
    · obtain ⟨N, hN⟩ := h
      replace hN : f N = c + 1 := by specialize hc N; lia
      use c + 1, N; intro n hn
      specialize mono_f hn; specialize hc n; lia
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
hc : ∀ (n : ℕ), f n ≤ c
zero : ∀ (hc : ∀ (n : ℕ), f n ≤ 0), ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
⊢ ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
have succ : ∀ (c : ℕ) (ih : ∀ (hc : ∀ (n : ℕ), f n ≤ c), ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b)
  (hc : ∀ (n : ℕ), f n ≤ c + 1), ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
Tactic: induction c with
  | zero => use 0, 0, fun n _ ↦ Nat.eq_zero_of_le_zero (hc n)
  | succ c ih =>
    by_cases! h : ∀ n, f n ≤ c
    · exact ih h
    · obtain ⟨N, hN⟩ := h
      replace hN : f N = c + 1 := by specialize hc N; lia
      use c + 1, N; intro n hn
      specialize mono_f hn; specialize hc n; lia
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Order.Monotone.Defs (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : γ → α
g : γ → β
⊢ (Monotone (β := α × β) fun (x : γ) ↦ (f x, g x)) ↔ Monotone f ∧ Monotone g
have simp_rw : (∀ ⦃a b : γ⦄, a ≤ b → (f a, g a) ≤ (f b, g b)) ↔ (∀ ⦃a b : γ⦄, a ≤ b → f a ≤ f b) ∧ ∀ ⦃a b : γ⦄, a ≤ b → g a ≤ g b
Tactic: simp_rw [Monotone, Prod.mk_le_mk, forall_and]