ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>min (min a b) c = min a (min b c)
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>min a (min b c) = min b (min a c)
<VAR>α : Type u<VAR>LinearOrder α<VAR>a : α<GOAL>min a a = a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>min a b = a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<VAR>h : b ≤ a<GOAL>min a b = b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<VAR>h₁ : a ≤ c<VAR>h₂ : b ≤ c<VAR>h₃ : ∀ {d : α}, a ≤ d → b ≤ d → c ≤ d<GOAL>c = max a b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>max a b = max b a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>max (max a b) c = max a (max b c)
<VAR>α : Type u<VAR>LinearOrder α<VAR>a : α<GOAL>max a a = a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<VAR>h : b ≤ a<GOAL>max a b = a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>max a b = b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<VAR>h : a < b<GOAL>min a b = a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<VAR>h : b < a<GOAL>min a b = b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<VAR>h : b < a<GOAL>max a b = a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<VAR>h : a < b<GOAL>max a b = b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<VAR>h₁ : a < b<VAR>h₂ : a < c<GOAL>a < min b c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<VAR>h₁ : a < c<VAR>h₂ : b < c<GOAL>max a b < c
<VAR>α : Type u<VAR>Preorder α<VAR>k j : α<VAR>hkj : k ≤ j<GOAL>Monotone fun x => match x with | ⟨i, hi⟩ => ⟨i, ⋯⟩
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>Monotone (f ∘ ⇑OrderDual.ofDual) ↔ Antitone f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>Antitone (f ∘ ⇑OrderDual.ofDual) ↔ Monotone f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>Monotone (⇑OrderDual.toDual ∘ f) ↔ Antitone f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>Antitone (⇑OrderDual.toDual ∘ f) ↔ Monotone f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<GOAL>MonotoneOn (f ∘ ⇑OrderDual.ofDual) s ↔ AntitoneOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<GOAL>AntitoneOn (f ∘ ⇑OrderDual.ofDual) s ↔ MonotoneOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<GOAL>MonotoneOn (⇑OrderDual.toDual ∘ f) s ↔ AntitoneOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<GOAL>AntitoneOn (⇑OrderDual.toDual ∘ f) s ↔ MonotoneOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>StrictMono (f ∘ ⇑OrderDual.ofDual) ↔ StrictAnti f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>StrictAnti (f ∘ ⇑OrderDual.ofDual) ↔ StrictMono f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>StrictMono (⇑OrderDual.toDual ∘ f) ↔ StrictAnti f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>StrictAnti (⇑OrderDual.toDual ∘ f) ↔ StrictMono f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<GOAL>StrictMonoOn (f ∘ ⇑OrderDual.ofDual) s ↔ StrictAntiOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<GOAL>StrictAntiOn (f ∘ ⇑OrderDual.ofDual) s ↔ StrictMonoOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<GOAL>StrictMonoOn (⇑OrderDual.toDual ∘ f) s ↔ StrictAntiOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<GOAL>StrictAntiOn (⇑OrderDual.toDual ∘ f) s ↔ StrictMonoOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>Monotone (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) ↔ Monotone f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>Antitone (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) ↔ Antitone f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<GOAL>MonotoneOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s ↔ MonotoneOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<GOAL>AntitoneOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s ↔ AntitoneOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>StrictMono (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) ↔ StrictMono f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>StrictAnti (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) ↔ StrictAnti f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<GOAL>StrictMonoOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s ↔ StrictMonoOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<GOAL>StrictAntiOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s ↔ StrictAntiOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>f : β → α<VAR>g h : γ → β<VAR>hf : Monotone f<VAR>le_gh : g ≤ h<GOAL>f ∘ g ≤ f ∘ h
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder γ<VAR>f : α → β → γ<VAR>hf : ∀ (b : β), Monotone fun a => f a b<GOAL>Monotone f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder γ<VAR>f : β → α → γ<VAR>b : β<VAR>hf : Monotone fun a b => f b a<GOAL>Monotone (f b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder γ<VAR>f : α → β → γ<VAR>hf : ∀ (b : β), Antitone fun a => f a b<GOAL>Antitone f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder γ<VAR>f : β → α → γ<VAR>b : β<VAR>hf : Antitone fun a b => f b a<GOAL>Antitone (f b)
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>(i : ι) → Preorder (α i)<VAR>i : ι<GOAL>Monotone (Function.eval i)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>a b : α<VAR>hf : Monotone f<VAR>h : a ≤ b<GOAL>f a ≤ f b
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>a b : α<VAR>hf : Antitone f<VAR>h : a ≤ b<GOAL>f b ≤ f a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>a b : α<VAR>hf : StrictMono f<VAR>h : a < b<GOAL>f a < f b
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>a b : α<VAR>hf : StrictAnti f<VAR>h : a < b<GOAL>f b < f a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Monotone f<VAR>s : Set α<GOAL>MonotoneOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<VAR>s : Set α<GOAL>AntitoneOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>MonotoneOn f Set.univ ↔ Monotone f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>AntitoneOn f Set.univ ↔ Antitone f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : StrictMono f<VAR>s : Set α<GOAL>StrictMonoOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : StrictAnti f<VAR>s : Set α<GOAL>StrictAntiOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>StrictMonoOn f Set.univ ↔ StrictMono f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>StrictAntiOn f Set.univ ↔ StrictAnti f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>PartialOrder β<VAR>f : α → β<VAR>h₁ : Monotone f<VAR>h₂ : Function.Injective f<GOAL>StrictMono f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>PartialOrder β<VAR>f : α → β<VAR>h₁ : Antitone f<VAR>h₂ : Function.Injective f<GOAL>StrictAnti f
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder α<VAR>Preorder β<VAR>f : α → β<GOAL>Monotone f ↔ ∀ ⦃a b : α⦄, a < b → f a ≤ f b
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder α<VAR>Preorder β<VAR>f : α → β<GOAL>Antitone f ↔ ∀ ⦃a b : α⦄, a < b → f b ≤ f a
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<GOAL>MonotoneOn f s ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f a ≤ f b
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<GOAL>AntitoneOn f s ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f b ≤ f a
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : StrictMonoOn f s<GOAL>MonotoneOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : StrictAntiOn f s<GOAL>AntitoneOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : StrictMono f<GOAL>Monotone f
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : StrictAnti f<GOAL>Antitone f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>Subsingleton α<VAR>f : α → β<GOAL>Monotone f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>Subsingleton α<VAR>f : α → β<GOAL>Antitone f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>Subsingleton β<VAR>f : α → β<GOAL>Monotone f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>Subsingleton β<VAR>f : α → β<GOAL>Antitone f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>Subsingleton α<VAR>f : α → β<GOAL>StrictMono f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>Subsingleton α<VAR>f : α → β<GOAL>StrictAnti f
<VAR>α : Type u<VAR>Preorder α<GOAL>Monotone id
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<GOAL>MonotoneOn id s
<VAR>α : Type u<VAR>Preorder α<GOAL>StrictMono id
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<GOAL>StrictMonoOn id s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>c : β<GOAL>Monotone fun x => c
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>c : β<VAR>s : Set α<GOAL>MonotoneOn (fun x => c) s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>c : β<GOAL>Antitone fun x => c
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>c : β<VAR>s : Set α<GOAL>AntitoneOn (fun x => c) s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>h : ∀ (x y : α), x ≤ y ↔ f x ≤ f y<GOAL>StrictMono f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>h : ∀ (x y : α), x ≤ y ↔ f y ≤ f x<GOAL>StrictAnti f
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>f : α → β<VAR>h : ∀ (x y : α), x < y → f x ≠ f y<GOAL>Function.Injective f
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder α<VAR>Preorder β<VAR>f : α → β<VAR>h : ∀ {x y : α}, f x ≤ f y → x ≤ y<GOAL>Function.Injective f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>a : α<VAR>hf : StrictMono f<VAR>ha : IsMax (f a)<GOAL>IsMax a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>a : α<VAR>hf : StrictMono f<VAR>ha : IsMin (f a)<GOAL>IsMin a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>a : α<VAR>hf : StrictAnti f<VAR>ha : IsMin (f a)<GOAL>IsMax a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>a : α<VAR>hf : StrictAnti f<VAR>ha : IsMax (f a)<GOAL>IsMin a
<VAR>f : ℕ → ℕ<VAR>hf : StrictMono f<VAR>m n : ℕ<GOAL>m + f n ≤ f (m + n)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f g : α → β<VAR>hf : StrictMono f<VAR>hg : StrictMono g<VAR>p : α → Prop<VAR>DecidablePred p<VAR>hp : ∀ ⦃x y : α⦄, x < y → p y → p x<VAR>hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y<GOAL>StrictMono fun x => if p x then f x else g x
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f g : α → β<VAR>hf : StrictMono f<VAR>hg : StrictMono g<VAR>p : α → Prop<VAR>DecidablePred p<VAR>hp : ∀ ⦃x y : α⦄, x < y → p y → p x<VAR>hfg : ∀ (x : α), f x ≤ g x<GOAL>StrictMono fun x => if p x then f x else g x
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f g : α → β<VAR>hf : StrictAnti f<VAR>hg : StrictAnti g<VAR>p : α → Prop<VAR>DecidablePred p<VAR>hp : ∀ ⦃x y : α⦄, x < y → p y → p x<VAR>hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → g y < f x<GOAL>StrictAnti fun x => if p x then f x else g x
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f g : α → β<VAR>hf : StrictAnti f<VAR>hg : StrictAnti g<VAR>p : α → Prop<VAR>DecidablePred p<VAR>hp : ∀ ⦃x y : α⦄, x < y → p y → p x<VAR>hfg : ∀ (x : α), g x ≤ f x<GOAL>StrictAnti fun x => if p x then f x else g x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : Monotone g<VAR>hf : Monotone f<GOAL>Monotone (g ∘ f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : Monotone g<VAR>hf : Antitone f<GOAL>Antitone (g ∘ f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : Antitone g<VAR>hf : Antitone f<GOAL>Monotone (g ∘ f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : Antitone g<VAR>hf : Monotone f<GOAL>Antitone (g ∘ f)
<VAR>α : Type u<VAR>Preorder α<VAR>f : α → α<VAR>hf : Monotone f<VAR>n : ℕ<GOAL>Monotone f^[n]
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set α<VAR>hg : Monotone g<VAR>hf : MonotoneOn f s<GOAL>MonotoneOn (g ∘ f) s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set α<VAR>hg : Monotone g<VAR>hf : AntitoneOn f s<GOAL>AntitoneOn (g ∘ f) s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set α<VAR>hg : Antitone g<VAR>hf : AntitoneOn f s<GOAL>MonotoneOn (g ∘ f) s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set α<VAR>hg : Antitone g<VAR>hf : MonotoneOn f s<GOAL>AntitoneOn (g ∘ f) s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : StrictMono g<VAR>hf : StrictMono f<GOAL>StrictMono (g ∘ f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : StrictMono g<VAR>hf : StrictAnti f<GOAL>StrictAnti (g ∘ f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : StrictAnti g<VAR>hf : StrictAnti f<GOAL>StrictMono (g ∘ f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : StrictAnti g<VAR>hf : StrictMono f<GOAL>StrictAnti (g ∘ f)
<VAR>α : Type u<VAR>Preorder α<VAR>f : α → α<VAR>hf : StrictMono f<VAR>n : ℕ<GOAL>StrictMono f^[n]
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set α<VAR>hg : StrictMono g<VAR>hf : StrictMonoOn f s<GOAL>StrictMonoOn (g ∘ f) s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set α<VAR>hg : StrictMono g<VAR>hf : StrictAntiOn f s<GOAL>StrictAntiOn (g ∘ f) s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set α<VAR>hg : StrictAnti g<VAR>hf : StrictAntiOn f s<GOAL>StrictMonoOn (g ∘ f) s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set α<VAR>hg : StrictAnti g<VAR>hf : StrictMonoOn f s<GOAL>StrictAntiOn (g ∘ f) s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>f : α → β → α<VAR>H : ∀ (b : β), Monotone fun a => f a b<VAR>l : List β<GOAL>Monotone fun a => List.foldl f a l
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β → β<VAR>H : ∀ (a : α), Monotone (f a)<VAR>l : List α<GOAL>Monotone fun b => List.foldr f b l
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>f : α → β → α<VAR>H : ∀ (b : β), StrictMono fun a => f a b<VAR>l : List β<GOAL>StrictMono fun a => List.foldl f a l
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>f : α → β → β<VAR>H : ∀ (a : α), StrictMono (f a)<VAR>l : List α<GOAL>StrictMono fun b => List.foldr f b l
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Monotone f<VAR>a b : α<VAR>h : f a < f b<GOAL>a < b
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<VAR>a b : α<VAR>h : f a < f b<GOAL>b < a
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : MonotoneOn f s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>h : f a < f b<GOAL>a < b
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : AntitoneOn f s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>h : f a < f b<GOAL>b < a
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : StrictMonoOn f s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>f a ≤ f b ↔ a ≤ b
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : StrictAntiOn f s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>f a ≤ f b ↔ b ≤ a
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : StrictMonoOn f s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>f a = f b ↔ a = b
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : StrictAntiOn f s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>f a = f b ↔ b = a
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : StrictMonoOn f s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>f a < f b ↔ a < b
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : StrictAntiOn f s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>f a < f b ↔ b < a
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : StrictMono f<VAR>a b : α<GOAL>f a ≤ f b ↔ a ≤ b
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : StrictAnti f<VAR>a b : α<GOAL>f a ≤ f b ↔ b ≤ a
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : StrictMono f<VAR>a b : α<GOAL>f a < f b ↔ a < b
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : StrictAnti f<VAR>a b : α<GOAL>f a < f b ↔ b < a
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : StrictMonoOn f s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>o : Ordering<GOAL>o.Compares (f a) (f b) ↔ o.Compares a b
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : StrictAntiOn f s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>o : Ordering<GOAL>o.Compares (f a) (f b) ↔ o.Compares b a
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : StrictMono f<VAR>a b : α<VAR>o : Ordering<GOAL>o.Compares (f a) (f b) ↔ o.Compares a b
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : StrictAnti f<VAR>a b : α<VAR>o : Ordering<GOAL>o.Compares (f a) (f b) ↔ o.Compares b a
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : StrictMono f<GOAL>Function.Injective f
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : StrictAnti f<GOAL>Function.Injective f
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : StrictMono f<VAR>a : α<VAR>hmax : ∀ (p : β), p ≤ f a<VAR>x : α<GOAL>x ≤ a
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : StrictMono f<VAR>a : α<VAR>hmin : ∀ (p : β), f a ≤ p<VAR>x : α<GOAL>a ≤ x
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : StrictAnti f<VAR>a : α<VAR>hmax : ∀ (p : β), p ≤ f a<VAR>x : α<GOAL>a ≤ x
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : StrictAnti f<VAR>a : α<VAR>hmin : ∀ (p : β), f a ≤ p<VAR>x : α<GOAL>x ≤ a
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>PartialOrder β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>StrictMono f ↔ Function.Injective f
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>PartialOrder β<VAR>f : α → β<VAR>hf : Antitone f<GOAL>StrictAnti f ↔ Function.Injective f
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>PartialOrder β<VAR>f : α → β<VAR>a₁ a₂ : α<VAR>h_mon : Monotone f<VAR>h_fa : f a₁ = f a₂<VAR>i : α<VAR>h₁ : a₁ ≤ i<VAR>h₂ : i ≤ a₂<GOAL>f i = f a₁
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>PartialOrder β<VAR>f : α → β<VAR>a₁ a₂ : α<VAR>h_anti : Antitone f<VAR>h_fa : f a₁ = f a₂<VAR>i : α<VAR>h₁ : a₁ ≤ i<VAR>h₂ : i ≤ a₂<GOAL>f i = f a₁
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<GOAL>¬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)
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<GOAL>¬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)
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>x y : α<VAR>hf : StrictMonoOn f s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>cmp (f x) (f y) = cmp x y
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<VAR>hf : StrictMono f<VAR>x y : α<GOAL>cmp (f x) (f y) = cmp x y
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>x y : α<VAR>hf : StrictAntiOn f s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>cmp (f x) (f y) = cmp y x
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<VAR>hf : StrictAnti f<VAR>x y : α<GOAL>cmp (f x) (f y) = cmp y x
<VAR>β : Type v<VAR>r : β → β → Prop<VAR>IsTrans β r<VAR>f : ℕ → β<VAR>a : ℕ<VAR>h : ∀ (n : ℕ), a ≤ n → r (f n) (f (n + 1))<VAR>b c : ℕ<VAR>hab : a ≤ b<VAR>hbc : b < c<GOAL>r (f b) (f c)
<VAR>β : Type v<VAR>r : β → β → Prop<VAR>IsRefl β r<VAR>IsTrans β r<VAR>f : ℕ → β<VAR>a : ℕ<VAR>h : ∀ (n : ℕ), a ≤ n → r (f n) (f (n + 1))<VAR>b c : ℕ<VAR>hab : a ≤ b<VAR>hbc : b ≤ c<GOAL>r (f b) (f c)
<VAR>β : Type v<VAR>r : β → β → Prop<VAR>IsTrans β r<VAR>f : ℕ → β<VAR>h : ∀ (n : ℕ), r (f n) (f (n + 1))<VAR>a b : ℕ<VAR>hab : a < b<GOAL>r (f a) (f b)
<VAR>β : Type v<VAR>r : β → β → Prop<VAR>IsRefl β r<VAR>IsTrans β r<VAR>f : ℕ → β<VAR>h : ∀ (n : ℕ), r (f n) (f (n + 1))<VAR>a b : ℕ<VAR>hab : a ≤ b<GOAL>r (f a) (f b)
<VAR>α : Type u<VAR>Preorder α<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), f n ≤ f (n + 1)<GOAL>Monotone f
<VAR>α : Type u<VAR>Preorder α<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), f (n + 1) ≤ f n<GOAL>Antitone f
<VAR>α : Type u<VAR>Preorder α<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), f n < f (n + 1)<GOAL>StrictMono f
<VAR>α : Type u<VAR>Preorder α<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), f (n + 1) < f n<GOAL>StrictAnti f
<VAR>α : Type u<VAR>Preorder α<VAR>NoMaxOrder α<VAR>a : α<GOAL>∃ f, StrictMono f ∧ f 0 = a
<VAR>α : Type u<VAR>Preorder α<VAR>NoMinOrder α<VAR>a : α<GOAL>∃ f, StrictAnti f ∧ f 0 = a
<VAR>α : Type u<VAR>Preorder α<VAR>Nonempty α<VAR>NoMaxOrder α<GOAL>∃ f, StrictMono f
<VAR>α : Type u<VAR>Preorder α<VAR>Nonempty α<VAR>NoMinOrder α<GOAL>∃ f, StrictAnti f
<VAR>β : Type v<VAR>r : β → β → Prop<VAR>IsTrans β r<VAR>f : ℤ → β<VAR>h : ∀ (n : ℤ), r (f n) (f (n + 1))<VAR>a b : ℤ<VAR>hab : a < b<GOAL>r (f a) (f b)
<VAR>β : Type v<VAR>r : β → β → Prop<VAR>IsRefl β r<VAR>IsTrans β r<VAR>f : ℤ → β<VAR>h : ∀ (n : ℤ), r (f n) (f (n + 1))<VAR>a b : ℤ<VAR>hab : a ≤ b<GOAL>r (f a) (f b)
<VAR>α : Type u<VAR>Preorder α<VAR>f : ℤ → α<VAR>hf : ∀ (n : ℤ), f n ≤ f (n + 1)<GOAL>Monotone f
<VAR>α : Type u<VAR>Preorder α<VAR>f : ℤ → α<VAR>hf : ∀ (n : ℤ), f (n + 1) ≤ f n<GOAL>Antitone f
<VAR>α : Type u<VAR>Preorder α<VAR>f : ℤ → α<VAR>hf : ∀ (n : ℤ), f n < f (n + 1)<GOAL>StrictMono f
<VAR>α : Type u<VAR>Preorder α<VAR>f : ℤ → α<VAR>hf : ∀ (n : ℤ), f (n + 1) < f n<GOAL>StrictAnti f
<VAR>α : Type u<VAR>Preorder α<VAR>Nonempty α<VAR>NoMinOrder α<VAR>NoMaxOrder α<GOAL>∃ f, StrictMono f