awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ), k ≥ m → f k = f m
⊢ f n = f b

Tactic:
(key n (hmb.trans hbn)).trans (key b hmb).symm

Premises used: LE.le.trans, Eq.symm, Eq.trans
-- 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 : ℕ), k ≥ m → f k = f m
⊢ f n = f b

Tactic:
exact (key n (hmb.trans hbn)).trans (key b hmb).symm

Premises used: LE.le.trans, Eq.symm, Eq.trans
-- Module: Mathlib.Order.Monotone.Basic
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
neg : ∀ (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

Tactic:
by_cases heq : f 0 = f 1

Premises used: OfNat.ofNat
-- Module: Mathlib.Order.Monotone.Basic
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
⊢ f 0 = f (HAdd.hAdd (α := ℕ) 0 1)

Tactic:
grind
-- Module: Mathlib.Order.Monotone.Basic
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 : ℕ
h_1 : f n_1 = f (n_1 + 1)
⊢ f (n_1 + 1) = f (n_1 + 1 + 1)

Tactic:
grind
-- Module: Mathlib.Order.Monotone.Basic
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
j : ℕ
zero : f 0 = f (HAdd.hAdd (α := ℕ) 0 1)
succ : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 1 + 1)
⊢ f j = f (j + 1)

Tactic:
induction j with grind
-- Module: Mathlib.Order.Monotone.Basic
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
⊢ ∀ (j : ℕ), f j = f (j + 1)

Tactic:
have flat (j : ℕ) : f j = f (j + 1) := by induction j with grind
-- Module: Mathlib.Order.Monotone.Basic
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)
h_1 : LE.le (α := ℕ) 0 0
⊢ f 0 = f 0

Tactic:
grind
-- Module: Mathlib.Order.Monotone.Basic
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)
n_1 : ℕ
h_1 : 0 ≤ n_1 → f n_1 = f 0
h_2 : 0 ≤ n_1 + 1
⊢ f (n_1 + 1) = f 0

Tactic:
grind
-- Module: Mathlib.Order.Monotone.Basic
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
succ : ∀ (n : ℕ), (0 ≤ n → f n = f 0) → 0 ≤ n + 1 → f (n + 1) = f 0
⊢ f m = f 0

Tactic:
induction m with grind
-- Module: Mathlib.Order.Monotone.Basic
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)
⊢ ∃ (n_1 : ℕ), n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1

Tactic:
exact ⟨0, Nat.zero_le _, fun m _ => by induction m with grind⟩
-- Module: Mathlib.Order.Monotone.Basic
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
⊢ f 1 < f 0

Tactic:
have hlt : f 1 < f 0 := (hfmono (Nat.le_succ 0)).lt_of_ne' heq
-- Module: Mathlib.Order.Monotone.Basic
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)
⊢ Antitone g

Tactic:
grind [Antitone]

Premises used: Antitone
-- Module: Mathlib.Order.Monotone.Basic
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)
⊢ Antitone g

Tactic:
have hg_anti : Antitone g := by grind [Antitone]
-- Module: Mathlib.Order.Monotone.Basic
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
⊢ f 1 < n

Tactic:
grind
-- Module: Mathlib.Order.Monotone.Basic
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
⊢ ∀ (m : ℕ), g m = g (m + 1) → g (m + 1) = g (m + 2)

Tactic:
grind
-- Module: Mathlib.Order.Monotone.Basic
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
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
⊢ ∃ (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

Premises used: OfNat.ofNat, rfl
-- Module: Mathlib.Order.Monotone.Basic
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
⊢ p + 1 ≤ n

Tactic:
omega
-- Module: Mathlib.Order.Monotone.Basic
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
neg : ∀ (m : ℕ) (hm : p + 1 ≤ m), f m = f (p + 1)
⊢ ∃ (n_1 : ℕ), n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1

Tactic:
refine ⟨p + 1, by omega, fun m hm => ?_⟩
-- Module: Mathlib.Order.Monotone.Basic
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
⊢ p ≤ m - 1

Tactic:
lia
-- Module: Mathlib.Order.Monotone.Basic
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
⊢ g (m - 1) = g p

Tactic:
specialize hp' (m - 1) (by lia)

Premises used: HSub.hSub, OfNat.ofNat
-- Module: Mathlib.Order.Monotone.Basic
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
m : ℕ
hm : p + 1 ≤ m
hp' : g (m - 1) = g p
⊢ f m = f (p + 1)

Tactic:
grind
-- Module: Mathlib.Order.Monotone.Basic
Goal:
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
induction : ∀ (x : ℕ) (h : f 0 = x), ∃ (n : ℕ), n ≤ x ∧ ∀ (m : ℕ), n ≤ m → f m = f n
⊢ ∃ (n : ℕ), n ≤ f 0 ∧ ∀ (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

Premises used: OfNat.ofNat
-- Module: Mathlib.Order.Monotone.Basic
Goal:
f : ℕ → ℕ
mono_f : Monotone f
hc : ∀ (n : ℕ), f n ≤ 0
w w₁ : ℕ
h : ∀ (n : ℕ), n ≥ 0 → f n = 0
⊢ ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b

Tactic:
use 0, 0, fun n _ ↦ Nat.eq_zero_of_le_zero (hc n)

Premises used: Nat.eq_zero_of_le_zero
-- Module: Mathlib.Order.Monotone.Basic
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
neg : ∀ (h : ∃ (n : ℕ), c < f n), ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
⊢ ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b

Tactic:
by_cases! h : ∀ n, f n ≤ c
-- Module: Mathlib.Order.Monotone.Basic
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 : ℕ), f n ≤ c
⊢ ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b

Tactic:
ih h
-- Module: Mathlib.Order.Monotone.Basic
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 : ℕ), f n ≤ c
⊢ ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b

Tactic:
exact ih h
-- Module: Mathlib.Order.Monotone.Basic
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
neg : ∀ (N : ℕ) (hN : c < f N), ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
⊢ ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b

Tactic:
obtain ⟨N, hN⟩ := h
-- Module: Mathlib.Order.Monotone.Basic
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

Tactic:
specialize hc N
-- Module: Mathlib.Order.Monotone.Basic
Goal:
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : ∀ (hc : ∀ (n : ℕ), f n ≤ c), ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
N : ℕ
hN : c < f N
hc : f N ≤ c + 1
⊢ f N = c + 1

Tactic:
lia
-- Module: Mathlib.Order.Monotone.Basic
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

Tactic:
replace hN : f N = c + 1 := by specialize hc N; lia
-- Module: Mathlib.Order.Monotone.Basic
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
h : ∀ (n : ℕ), n ≥ N → f n = c + 1
⊢ ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b

Tactic:
use c + 1, N
-- Module: Mathlib.Order.Monotone.Basic
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 ≤ f n

Tactic:
specialize mono_f hn
-- Module: Mathlib.Order.Monotone.Basic
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

Tactic:
specialize hc n
-- Module: Mathlib.Order.Monotone.Basic
Goal:
f : ℕ → ℕ
c : ℕ
ih : ∀ (hc : ∀ (n : ℕ), f n ≤ c), ∃ (b : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → f n = b
N : ℕ
hN : f N = c + 1
n : ℕ
hn : n ≥ N
mono_f : f N ≤ f n
hc : f n ≤ c + 1
⊢ f n = c + 1

Tactic:
lia
-- Module: Mathlib.Order.Monotone.Basic
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
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
⊢ ∃ (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

Premises used: Nat.eq_zero_of_le_zero
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ Eq (α := Prop) (∀ ⦃a b : α⦄, a ≤ b → f a ≤ f b) (∀ ⦃a b : α⦄, b ≤ a → f b ≤ f a)

Tactic:
forall_comm.eq

Premises used: forall_comm, Iff.eq
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ Eq (α := Prop) (∀ ⦃a b : α⦄, a ≤ b → f b ≤ f a) (∀ ⦃a b : α⦄, b ≤ a → f a ≤ f b)

Tactic:
forall_comm.eq

Premises used: forall_comm, Iff.eq
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
⊢ Eq (α := Prop) (∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a ≤ b → f a ≤ f b)
    (∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → b ≤ a → f b ≤ f a)

Tactic:
grind only
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
⊢ Eq (α := Prop) (∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a ≤ b → f b ≤ f a)
    (∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → b ≤ a → f a ≤ f b)

Tactic:
grind only
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ Eq (α := Prop) (∀ ⦃a b : α⦄, a < b → f a < f b) (∀ ⦃a b : α⦄, b < a → f b < f a)

Tactic:
forall_comm.eq

Premises used: forall_comm, Iff.eq
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ Eq (α := Prop) (∀ ⦃a b : α⦄, a < b → f b < f a) (∀ ⦃a b : α⦄, b < a → f a < f b)

Tactic:
forall_comm.eq

Premises used: forall_comm, Iff.eq
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
⊢ Eq (α := Prop) (∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f a < f b)
    (∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → b < a → f b < f a)

Tactic:
grind only
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
⊢ Eq (α := Prop) (∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f b < f a)
    (∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → b < a → f a < f b)

Tactic:
grind only
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
f : β → α
g h : γ → β
hf : Monotone f
le_gh : g ≤ h
⊢ f ∘ g ≤ f ∘ h

Tactic:
fun x ↦ hf (le_gh x)
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder γ
f : α → β → γ
hf : ∀ (b : β), Monotone.{u, w} (β := γ) fun (a : α) ↦ f a b
⊢ Monotone f

Tactic:
fun _ _ h b ↦ hf b h

Premises used: Monotone
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder γ
f : β → α → γ
b : β
hf : Monotone (β := (b : β) → γ) fun (a : α) (b : β) ↦ f b a
⊢ Monotone (f b)

Tactic:
fun _ _ h ↦ hf h b

Premises used: Monotone
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder γ
f : α → β → γ
hf : ∀ (b : β), Antitone.{u, w} (β := γ) fun (a : α) ↦ f a b
⊢ Antitone f

Tactic:
fun _ _ h b ↦ hf b h

Premises used: Antitone
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder γ
f : β → α → γ
b : β
hf : Antitone (β := (b : β) → γ) fun (a : α) (b : β) ↦ f b a
⊢ Antitone (f b)

Tactic:
fun _ _ h ↦ hf h b

Premises used: Antitone
-- Module: Mathlib.Order.Monotone.Defs
Goal:
ι : Type u
α : ι → Type v
inst : (i : ι) → Preorder (α i)
i : ι
⊢ Monotone (α := (x : ι) → α x) (eval (β := α) i)

Tactic:
fun _ _ H ↦ H i

Premises used: Monotone
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
a b : α
hf : Monotone f
h : a ≤ b
⊢ f a ≤ f b

Tactic:
hf h
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
a b : α
hf : Antitone f
h : a ≤ b
⊢ f b ≤ f a

Tactic:
hf h
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
a b : α
hf : StrictMono f
h : a < b
⊢ f a < f b

Tactic:
hf h
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
a b : α
hf : StrictAnti f
h : a < b
⊢ f b < f a

Tactic:
hf h
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : Monotone f
s : Set α
⊢ MonotoneOn f s

Tactic:
fun _ _ _ _ ↦ hf.imp

Premises used: Monotone.imp, MonotoneOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : Antitone f
s : Set α
⊢ AntitoneOn f s

Tactic:
fun _ _ _ _ ↦ hf.imp

Premises used: Antitone.imp, AntitoneOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ MonotoneOn f Set.univ ↔ Monotone f

Tactic:
⟨fun h _ _ ↦ h trivial trivial, fun h ↦ h.monotoneOn _⟩

Premises used: trivial, Set.univ, Iff.intro, Monotone.monotoneOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ AntitoneOn f Set.univ ↔ Antitone f

Tactic:
⟨fun h _ _ ↦ h trivial trivial, fun h ↦ h.antitoneOn _⟩

Premises used: trivial, Antitone.antitoneOn, Set.univ, Iff.intro
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
s : Set α
⊢ StrictMonoOn f s

Tactic:
fun _ _ _ _ ↦ hf.imp

Premises used: StrictMono.imp, StrictMonoOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : StrictAnti f
s : Set α
⊢ StrictAntiOn f s

Tactic:
fun _ _ _ _ ↦ hf.imp

Premises used: StrictAntiOn, StrictAnti.imp
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ StrictMonoOn f Set.univ ↔ StrictMono f

Tactic:
⟨fun h _ _ ↦ h trivial trivial, fun h ↦ h.strictMonoOn _⟩

Premises used: trivial, Set.univ, StrictMono.strictMonoOn, Iff.intro
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ StrictAntiOn f Set.univ ↔ StrictAnti f

Tactic:
⟨fun h _ _ ↦ h trivial trivial, fun h ↦ h.strictAntiOn _⟩

Premises used: trivial, Set.univ, StrictAnti.strictAntiOn, Iff.intro
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : PartialOrder β
f : α → β
h₁ : Monotone f
h₂ : Injective f
⊢ StrictMono f

Tactic:
fun _ _ h ↦ (h₁ h.le).lt_of_ne fun H ↦ h.ne <| h₂ H

Premises used: StrictMono, LT.lt.le, LE.le.lt_of_ne, LT.lt.ne
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : PartialOrder β
f : α → β
h₁ : Antitone f
h₂ : Injective f
⊢ StrictAnti f

Tactic:
fun _ _ h ↦ (h₁ h.le).lt_of_ne fun H ↦ h.ne <| h₂ H.symm

Premises used: LT.lt.le, LE.le.lt_of_ne, StrictAnti, Eq.symm, LT.lt.ne
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : Preorder β
f : α → β
⊢ Monotone f ↔ ∀ ⦃a b : α⦄, a < b → f a ≤ f b

Tactic:
forall₂_congr fun _ _ ↦
    ⟨fun hf h ↦ hf h.le, fun hf h ↦ h.eq_or_lt.elim (fun H ↦ (congr_arg _ H).le) hf⟩

Premises used: LE.le.eq_or_lt, Monotone, LT.lt.le, Eq.le, congr_arg, forall₂_congr, Iff.intro, Or.elim