awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst_2 : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
pos :
  ∀ (hy : p y),
    LT.lt.{v} (α := β) ((fun (x : α) ↦ if p x then f x else g x) x) ((fun (x : α) ↦ if p x then f x else g x) y)
neg :
  ∀ (hy : ¬p y),
    LT.lt.{v} (α := β) ((fun (x : α) ↦ if p x then f x else g x) x) ((fun (x : α) ↦ if p x then f x else g x) y)
⊢ LT.lt.{v} (α := β) ((fun (x : α) ↦ if p x then f x else g x) x) ((fun (x : α) ↦ if p x then f x else g x) y)

Tactic:
by_cases hy : p y
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst_2 : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : p y
⊢ p x

Tactic:
have hx : p x := hp h hy
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst_2 : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : p y
hx : p x
⊢ LT.lt.{v} (α := β) ((fun (x : α) ↦ if p x then f x else g x) x) ((fun (x : α) ↦ if p x then f x else g x) y)

Tactic:
simpa [hx, hy] using hf h
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst_2 : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
pos :
  ∀ (hx : p x),
    LT.lt.{v} (α := β) ((fun (x : α) ↦ if p x then f x else g x) x) ((fun (x : α) ↦ if p x then f x else g x) y)
neg :
  ∀ (hx : ¬p x),
    LT.lt.{v} (α := β) ((fun (x : α) ↦ if p x then f x else g x) x) ((fun (x : α) ↦ if p x then f x else g x) y)
⊢ LT.lt.{v} (α := β) ((fun (x : α) ↦ if p x then f x else g x) x) ((fun (x : α) ↦ if p x then f x else g x) y)

Tactic:
by_cases hx : p x
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst_2 : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
hx : p x
⊢ LT.lt.{v} (α := β) ((fun (x : α) ↦ if p x then f x else g x) x) ((fun (x : α) ↦ if p x then f x else g x) y)

Tactic:
simpa [hx, hy] using hfg hx hy h
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst_2 : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
hx : ¬p x
⊢ LT.lt.{v} (α := β) ((fun (x : α) ↦ if p x then f x else g x) x) ((fun (x : α) ↦ if p x then f x else g x) y)

Tactic:
simpa [hx, hy] using hg h
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst_2 : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ (x : α), f x ≤ g x
⊢ StrictMono.{u, v} (β := β) fun (x : α) ↦ if p x then f x else g x

Tactic:
(hf.ite' hg hp) fun _ y _ _ h ↦ (hf h).trans_le (hfg y)

Premises used: StrictMono.ite', LT.lt.trans_le
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f g : α → β
hf : StrictAnti f
hg : StrictAnti g
p : α → Prop
inst_2 : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → g y < f x
⊢ StrictAnti.{u, v} (β := β) fun (x : α) ↦ if p x then f x else g x

Tactic:
StrictMono.ite' hf.dual_right hg.dual_right hp hfg

Premises used: StrictMono.ite', StrictAnti, StrictAnti.dual_right, OrderDual
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f g : α → β
hf : StrictAnti f
hg : StrictAnti g
p : α → Prop
inst_2 : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ (x : α), g x ≤ f x
⊢ StrictAnti.{u, v} (β := β) fun (x : α) ↦ if p x then f x else g x

Tactic:
(hf.ite' hg hp) fun _ y _ _ h ↦ (hfg y).trans_lt (hf h)

Premises used: LE.le.trans_lt, StrictAnti.ite'
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
f : α → β → α
H : ∀ (b : β), Monotone (β := α) fun (a : α) ↦ f a b
l : List β
⊢ Monotone (β := α) fun (a : α) ↦ foldl f a l

Tactic:
List.recOn l (fun _ _ ↦ id) fun _ _ hl _ _ h ↦ hl (H _ h)

Premises used: List.recOn
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β → β
H : ∀ (a : α), Monotone (f a)
l : List α
⊢ Monotone (β := β) fun (b : β) ↦ foldr f b l

Tactic:
fun _ _ h ↦ List.recOn l h fun i _ hl ↦ H i hl

Premises used: Monotone, List.recOn
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
f : α → β → α
H : ∀ (b : β), StrictMono (β := α) fun (a : α) ↦ f a b
l : List β
⊢ StrictMono (β := α) fun (a : α) ↦ foldl f a l

Tactic:
List.recOn l (fun _ _ ↦ id) fun _ _ hl _ _ h ↦ hl (H _ h)

Premises used: List.recOn
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β → β
H : ∀ (a : α), StrictMono (f a)
l : List α
⊢ StrictMono (β := β) fun (b : β) ↦ foldr f b l

Tactic:
fun _ _ h ↦ List.recOn l h fun i _ hl ↦ H i hl

Premises used: StrictMono, List.recOn
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ f a ≤ f b ↔ a ≤ b

Tactic:
⟨fun h ↦ le_of_not_gt fun h' ↦ (hf hb ha h').not_ge h, fun h ↦
    h.lt_or_eq_dec.elim (fun h' ↦ (hf ha hb h').le) fun h' ↦ h' ▸ le_rfl⟩

Premises used: le_rfl, le_of_not_gt, Eq.rec, LT.lt.le, Iff.intro, LE.le.lt_or_eq_dec, LT.lt.not_ge, Or.elim
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : StrictAntiOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ f a ≤ f b ↔ b ≤ a

Tactic:
hf.dual_right.le_iff_le hb ha

Premises used: StrictMonoOn.le_iff_le, StrictAntiOn.dual_right
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a : α
ha hb : a ∈ s
⊢ f a = f a

Tactic:
rfl
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : StrictAntiOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ f a = f b ↔ b = a

Tactic:
(hf.dual_right.eq_iff_eq ha hb).trans eq_comm

Premises used: StrictMonoOn.eq_iff_eq, eq_comm, Iff.trans, OrderDual, StrictAntiOn.dual_right
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
rw : f a ≤ f b ∧ ¬f b ≤ f a ↔ a < b
rw₁ : f a ≤ f b ∧ ¬f b ≤ f a ↔ a ≤ b ∧ ¬b ≤ a
rw₂ : a ≤ b ∧ ¬f b ≤ f a ↔ a ≤ b ∧ ¬b ≤ a
rw₃ rw₄ : a ≤ b ∧ ¬b ≤ a ↔ a ≤ b ∧ ¬b ≤ a
⊢ f a < f b ↔ a < b

Tactic:
rw [lt_iff_le_not_ge, lt_iff_le_not_ge, hf.le_iff_le ha hb, hf.le_iff_le hb ha]

Premises used: lt_iff_le_not_ge, StrictMonoOn.le_iff_le
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : StrictAntiOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ f a < f b ↔ b < a

Tactic:
hf.dual_right.lt_iff_lt hb ha

Premises used: StrictAntiOn.dual_right, StrictMonoOn.lt_iff_lt
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
a b : α
⊢ f a ≤ f b ↔ a ≤ b

Tactic:
(hf.strictMonoOn Set.univ).le_iff_le trivial trivial

Premises used: trivial, Set.univ, StrictMono.strictMonoOn, StrictMonoOn.le_iff_le
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
hf : StrictAnti f
a b : α
⊢ f a ≤ f b ↔ b ≤ a

Tactic:
(hf.strictAntiOn Set.univ).le_iff_ge trivial trivial

Premises used: trivial, Set.univ, StrictAntiOn.le_iff_ge, StrictAnti.strictAntiOn
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
a b : α
⊢ f a < f b ↔ a < b

Tactic:
(hf.strictMonoOn Set.univ).lt_iff_lt trivial trivial

Premises used: trivial, Set.univ, StrictMono.strictMonoOn, StrictMonoOn.lt_iff_lt
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
hf : StrictAnti f
a b : α
⊢ f a < f b ↔ b < a

Tactic:
(hf.strictAntiOn Set.univ).lt_iff_gt trivial trivial

Premises used: trivial, Set.univ, StrictAntiOn.lt_iff_gt, StrictAnti.strictAntiOn
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : StrictAntiOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
o : Ordering
⊢ o.Compares (f a) (f b) ↔ o.Compares b a

Tactic:
toDual_compares_toDual.trans <| hf.dual_right.compares hb ha

Premises used: toDual_compares_toDual, Iff.trans, OrderDual, StrictMonoOn.compares, StrictAntiOn.dual_right
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
a b : α
o : Ordering
⊢ o.Compares (f a) (f b) ↔ o.Compares a b

Tactic:
(hf.strictMonoOn Set.univ).compares trivial trivial

Premises used: trivial, Set.univ, StrictMono.strictMonoOn, StrictMonoOn.compares
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
hf : StrictAnti f
a b : α
o : Ordering
⊢ o.Compares (f a) (f b) ↔ o.Compares b a

Tactic:
(hf.strictAntiOn Set.univ).compares trivial trivial

Premises used: trivial, Set.univ, StrictAnti.strictAntiOn, StrictAntiOn.compares
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
⊢ Injective f

Tactic:
fun x y h ↦ show Compares eq x y from hf.compares.1 h

Premises used: Ordering.Compares, Iff.mp, Function.Injective, StrictMono.compares
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
hf : StrictAnti f
⊢ Injective f

Tactic:
fun x y h ↦ show Compares eq x y from hf.compares.1 h.symm

Premises used: StrictAnti.compares, Ordering.Compares, Iff.mp, Function.Injective, Eq.symm
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
⊢ Set.InjOn f s

Tactic:
fun x hx y hy hxy ↦
  show Ordering.eq.Compares x y from (hf.compares hx hy).1 hxy

Premises used: Ordering.Compares, Iff.mp, Set.InjOn, StrictMonoOn.compares
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : StrictAntiOn f s
⊢ Set.InjOn f s

Tactic:
hf.dual_left.injOn

Premises used: StrictMonoOn.injOn, StrictAntiOn.dual_left, OrderDual
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
a : α
hmax : ∀ (p : β), p ≤ f a
x : α
⊢ x ≤ a

Tactic:
hf.le_iff_le.mp (hmax (f x))

Premises used: Iff.mp, StrictMono.le_iff_le
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
hf : StrictAnti f
a : α
hmax : ∀ (p : β), p ≤ f a
x : α
⊢ a ≤ x

Tactic:
hf.le_iff_ge.mp (hmax (f x))

Premises used: StrictAnti.le_iff_ge, Iff.mp
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
hf : Monotone f
⊢ StrictMono f ↔ Injective f

Tactic:
⟨fun h ↦ h.injective, hf.strictMono_of_injective⟩

Premises used: StrictMono.injective, Monotone.strictMono_of_injective, Iff.intro
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
hf : Antitone f
⊢ StrictAnti f ↔ Injective f

Tactic:
⟨fun h ↦ h.injective, hf.strictAnti_of_injective⟩

Premises used: Iff.intro, Antitone.strictAnti_of_injective, StrictAnti.injective
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
s : Set α
hf : MonotoneOn f s
⊢ StrictMonoOn f s ↔ Set.InjOn f s

Tactic:
⟨StrictMonoOn.injOn, hf.strictMonoOn_of_injOn⟩

Premises used: StrictMonoOn.injOn, MonotoneOn.strictMonoOn_of_injOn, Iff.intro
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
s : Set α
hf : AntitoneOn f s
⊢ StrictAntiOn f s ↔ Set.InjOn f s

Tactic:
⟨StrictAntiOn.injOn, hf.strictAntiOn_of_injOn⟩

Premises used: StrictAntiOn.injOn, Iff.intro, AntitoneOn.strictAntiOn_of_injOn
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
a : f i ≤ f a₁
a₃ : f a₁ ≤ f i
⊢ f i = f a₁

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
a : f i ≤ f a₂
⊢ f i ≤ f a₁

Tactic:
rw [h_fa]
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i ≤ f a₂

Tactic:
h_mon h₂
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i ≤ f a₂

Tactic:
exact h_mon h₂
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₁ ≤ f i

Tactic:
h_mon h₁
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₁ ≤ f i

Tactic:
exact h_mon h₁
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
a : f i ≤ f a₁
a₃ : f a₁ ≤ f i
⊢ f i = f a₁

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i ≤ f a₁

Tactic:
h_anti h₁
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i ≤ f a₁

Tactic:
exact h_anti h₁
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
a : f a₂ ≤ f i
⊢ f a₁ ≤ f i

Tactic:
rw [h_fa]
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₂ ≤ f i

Tactic:
h_anti h₂
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₂ ≤ f i

Tactic:
exact h_anti h₂
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
⊢ ((¬∀ ⦃a b : α⦄, a ≤ b → f a ≤ f b) ∧ ¬∀ ⦃a b : α⦄, a ≤ b → f b ≤ f a) ↔
    ∃ (a : α), ∃ (b : α), ∃ (c : α), a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
grind [not_le]

Premises used: not_le
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
simp_rw :
  (∃ (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)
⊢ ¬Monotone f ∧ ¬Antitone f ↔
    ∃ (a : α), ∃ (b : α), ∃ (c : α), a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
simp_rw [not_monotone_not_antitone_iff_exists_le_le, ← and_assoc]

Premises used: not_monotone_not_antitone_iff_exists_le_le, and_assoc
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
⊢ (∃ (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)

Tactic:
exists₃_congr (fun a b c ↦ and_congr_left <|
    fun h ↦ (Ne.le_iff_lt ?_).and <| Ne.le_iff_lt ?_)

Premises used: Ne.le_iff_lt, and_congr_left, Iff.and, exists₃_congr
-- Module: Mathlib.Order.Monotone.Basic
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
refine_2 : ∀ (a b c : α) (h : f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c), b ≠ c
⊢ (∃ (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)

Tactic:
refine exists₃_congr (fun a b c ↦ and_congr_left <|
    fun h ↦ (Ne.le_iff_lt ?_).and <| Ne.le_iff_lt ?_)

Premises used: Ne.le_iff_lt, and_congr_left, Iff.and, exists₃_congr
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
a c : α
h : f a < f a ∧ f c < f a ∨ f a < f a ∧ f a < f c
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
a b : α
h : f a < f b ∧ f b < f b ∨ f b < f a ∧ f b < f b
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
s : Set α
x y : α
hf : StrictMonoOn f s
hx : x ∈ s
hy : y ∈ s
⊢ cmp (f x) (f y) = cmp x y

Tactic:
((hf.compares hx hy).2 (cmp_compares x y)).cmp_eq

Premises used: Iff.mpr, Ordering.Compares.cmp_eq, cmp_compares, StrictMonoOn.compares
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
x y : α
⊢ cmp (f x) (f y) = cmp x y

Tactic:
(hf.strictMonoOn Set.univ).cmp_map_eq trivial trivial

Premises used: trivial, Set.univ, StrictMonoOn.cmp_map_eq, StrictMono.strictMonoOn
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
s : Set α
x y : α
hf : StrictAntiOn f s
hx : x ∈ s
hy : y ∈ s
⊢ cmp (f x) (f y) = cmp y x

Tactic:
hf.dual_right.cmp_map_eq hy hx

Premises used: cmpUsing, cmp, StrictMonoOn.cmp_map_eq, OrderDual, StrictAntiOn.dual_right
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictAnti f
x y : α
⊢ cmp (f x) (f y) = cmp y x

Tactic:
(hf.strictAntiOn Set.univ).cmp_map_eq trivial trivial

Premises used: trivial, Set.univ, StrictAntiOn.cmp_map_eq, StrictAnti.strictAntiOn
-- Module: Mathlib.Order.Monotone.Basic
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
⊢ r (f b) (f b.succ)

Tactic:
h _ hab
-- Module: Mathlib.Order.Monotone.Basic
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
⊢ r (f b) (f b.succ)

Tactic:
exact h _ hab
-- Module: Mathlib.Order.Monotone.Basic
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
m : ℕ
b_lt_k : b.succ.le m
r_b_k : r (f b) (f m)
⊢ r (f b) (f m.succ)

Tactic:
_root_.trans r_b_k (h _ (hab.trans_lt b_lt_k).le)

Premises used: trans, LT.lt.le, LE.le.trans_lt
-- Module: Mathlib.Order.Monotone.Basic
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
m : ℕ
b_lt_k : b.succ.le m
r_b_k : r (f b) (f m)
⊢ r (f b) (f m.succ)

Tactic:
exact _root_.trans r_b_k (h _ (hab.trans_lt b_lt_k).le)

Premises used: trans, LT.lt.le, LE.le.trans_lt
-- Module: Mathlib.Order.Monotone.Basic
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)
step : ∀ {m : ℕ} (b_lt_k : b.succ.le m) (r_b_k : r (f b) (f m)), r (f b) (f m.succ)
⊢ r (f b) (f c)

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)

Premises used: refl
-- Module: Mathlib.Order.Monotone.Basic
Goal:
β : Type v
r : β → β → Prop
inst : Std.Refl r
inst_1 : 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)

Tactic:
hbc.eq_or_lt.elim (fun h ↦ h ▸ refl _) (Nat.rel_of_forall_rel_succ_of_le_of_lt r h hab)

Premises used: LE.le.eq_or_lt, Eq.rec, Nat.rel_of_forall_rel_succ_of_le_of_lt, Or.elim, refl
-- 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
⊢ r (f a) (f b)

Tactic:
Nat.rel_of_forall_rel_succ_of_le_of_lt r (fun n _ ↦ h n) le_rfl hab

Premises used: le_rfl, Nat.rel_of_forall_rel_succ_of_le_of_lt
-- 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:
Nat.rel_of_forall_rel_succ_of_le_of_le r (fun n _ ↦ h n) le_rfl hab

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

Tactic:
Nat.rel_of_forall_rel_succ_of_le (· ≤ ·) hf

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

Tactic:
fun _ _ hle ↦ Nat.rel_of_forall_rel_succ_of_le_of_le (· ≤ ·) hf
    (Nat.le_add_left k _) (Nat.add_le_add_iff_right.mpr hle)

Premises used: Iff.mpr, Nat.add_le_add_iff_right, Nat.rel_of_forall_rel_succ_of_le_of_le, Monotone, Nat.le_add_left, LE.le
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
inst : Preorder α
f : ℕ → α
k : ℕ
hf : ∀ (n : ℕ), n ≥ k → f n ≤ f (n + 1)
⊢ MonotoneOn f {x : ℕ | k ≤ x}

Tactic:
fun _ hab _ _ hle ↦ Nat.rel_of_forall_rel_succ_of_le_of_le (· ≤ ·) hf hab hle

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

Tactic:
⟨fun h x hx y hy hle ↦ ?_, fun h x y hle ↦ ?_⟩

Premises used: Iff.intro