awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : Preorder β
f : α → β
⊢ Antitone f ↔ ∀ ⦃a b : α⦄, a < b → f b ≤ f a

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

Premises used: LE.le.eq_or_lt, Eq.ge, LT.lt.le, congr_arg, Antitone, forall₂_congr, Iff.intro, Or.elim
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : Preorder β
f : α → β
s : Set α
⊢ MonotoneOn f s ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f a ≤ f b

Tactic:
⟨fun hf _ ha _ hb h ↦ hf ha hb h.le,
   fun hf _ ha _ hb h ↦ h.eq_or_lt.elim (fun H ↦ (congr_arg _ H).le) (hf ha hb)⟩

Premises used: LE.le.eq_or_lt, LT.lt.le, Eq.le, congr_arg, Iff.intro, Or.elim
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : Preorder β
f : α → β
s : Set α
⊢ AntitoneOn f s ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f b ≤ f a

Tactic:
⟨fun hf _ ha _ hb h ↦ hf ha hb h.le,
   fun hf _ ha _ hb h ↦ h.eq_or_lt.elim (fun H ↦ (congr_arg _ H).ge) (hf ha hb)⟩

Premises used: LE.le.eq_or_lt, Eq.ge, LT.lt.le, congr_arg, Iff.intro, Or.elim
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
⊢ MonotoneOn f s

Tactic:
monotoneOn_iff_forall_lt.2 fun _ ha _ hb h ↦ (hf ha hb h).le

Premises used: Iff.mpr, monotoneOn_iff_forall_lt, LT.lt.le
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : StrictAntiOn f s
⊢ AntitoneOn f s

Tactic:
antitoneOn_iff_forall_lt.2 fun _ ha _ hb h ↦ (hf ha hb h).le

Premises used: Iff.mpr, LT.lt.le, antitoneOn_iff_forall_lt
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
⊢ Monotone f

Tactic:
monotone_iff_forall_lt.2 fun _ _ h ↦ (hf h).le

Premises used: Iff.mpr, LT.lt.le, monotone_iff_forall_lt
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : Preorder β
f : α → β
hf : StrictAnti f
⊢ Antitone f

Tactic:
antitone_iff_forall_lt.2 fun _ _ h ↦ (hf h).le

Premises used: Iff.mpr, LT.lt.le, antitone_iff_forall_lt
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : Subsingleton α
f : α → β
⊢ Monotone f

Tactic:
fun _ _ _ ↦ (congr_arg _ <| Subsingleton.elim _ _).le

Premises used: Monotone, Eq.le, congr_arg, Subsingleton.elim
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : Subsingleton α
f : α → β
⊢ Antitone f

Tactic:
fun _ _ _ ↦ (congr_arg _ <| Subsingleton.elim _ _).le

Premises used: Eq.le, congr_arg, Antitone, Subsingleton.elim
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : Subsingleton β
f : α → β
⊢ Monotone f

Tactic:
fun _ _ _ ↦ (Subsingleton.elim _ _).le

Premises used: Monotone, Eq.le, Subsingleton.elim
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : Subsingleton β
f : α → β
⊢ Antitone f

Tactic:
fun _ _ _ ↦ (Subsingleton.elim _ _).le

Premises used: Eq.le, Antitone, Subsingleton.elim
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : Subsingleton α
f : α → β
⊢ StrictMono f

Tactic:
fun _ _ h ↦ (h.ne <| Subsingleton.elim _ _).elim

Premises used: StrictMono, False.elim, Subsingleton.elim, LT.lt.ne
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : Subsingleton α
f : α → β
⊢ StrictAnti f

Tactic:
fun _ _ h ↦ (h.ne <| Subsingleton.elim _ _).elim

Premises used: False.elim, StrictAnti, Subsingleton.elim, LT.lt.ne
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
inst : Preorder α
⊢ Monotone.{u, u} (α := α) id

Tactic:
fun _ _ ↦ id

Premises used: Monotone, id
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
inst : Preorder α
s : Set α
⊢ MonotoneOn id s

Tactic:
fun _ _ _ _ ↦ id

Premises used: id, MonotoneOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
inst : Preorder α
⊢ StrictMono.{u, u} (α := α) id

Tactic:
fun _ _ ↦ id

Premises used: StrictMono, id
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
inst : Preorder α
s : Set α
⊢ StrictMonoOn id s

Tactic:
fun _ _ _ _ ↦ id

Premises used: id, StrictMonoOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
c : β
⊢ Monotone.{u, v} (β := β) fun (x : α) ↦ c

Tactic:
fun _ _ _ ↦ le_rfl

Premises used: le_rfl, Monotone
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
c : β
s : Set α
⊢ MonotoneOn.{u, v} (β := β) (fun (x : α) ↦ c) s

Tactic:
fun _ _ _ _ _ ↦ le_rfl

Premises used: le_rfl, MonotoneOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
c : β
⊢ Antitone.{u, v} (β := β) fun (x : α) ↦ c

Tactic:
fun _ _ _ ↦ le_refl c

Premises used: le_refl, Antitone
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
c : β
s : Set α
⊢ AntitoneOn.{u, v} (β := β) (fun (x : α) ↦ c) s

Tactic:
fun _ _ _ _ _ ↦ le_rfl

Premises used: le_rfl, AntitoneOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
h : ∀ (x y : α), x ≤ y ↔ f x ≤ f y
⊢ StrictMono f

Tactic:
fun _ _ ↦ (lt_iff_lt_of_le_iff_le' (h _ _) (h _ _)).1

Premises used: StrictMono, lt_iff_lt_of_le_iff_le', Iff.mp
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
h : ∀ (x y : α), x ≤ y ↔ f y ≤ f x
⊢ StrictAnti f

Tactic:
fun _ _ ↦ (lt_iff_lt_of_le_iff_le' (h _ _) (h _ _)).1

Premises used: lt_iff_lt_of_le_iff_le', StrictAnti, Iff.mp
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
⊢ Injective f

Tactic:
grind [Injective]

Premises used: Function.Injective
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : PartialOrder α
f : α → β
h : ∀ {x y : α}, f x = f y → x ≤ y
⊢ Injective f

Tactic:
fun _ _ hxy ↦ h hxy |>.antisymm <| h hxy.symm

Premises used: LE.le.antisymm, Function.Injective, Eq.symm
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : Preorder β
f : α → β
h : ∀ {x y : α}, f x ≤ f y → x ≤ y
⊢ Injective f

Tactic:
.of_eq_imp_le (h ·.le)

Premises used: Eq.le, Function.Injective.of_eq_imp_le
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
hg : Monotone g
hf : Monotone f
⊢ Monotone (g ∘ f)

Tactic:
fun _ _ h ↦ hg (hf h)

Premises used: Monotone
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
hg : Monotone g
hf : Antitone f
⊢ Antitone (g ∘ f)

Tactic:
fun _ _ h ↦ hg (hf h)

Premises used: Antitone
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
hg : Antitone g
hf : Antitone f
⊢ Monotone (g ∘ f)

Tactic:
fun _ _ h ↦ hg (hf h)

Premises used: Monotone
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
hg : Antitone g
hf : Monotone f
⊢ Antitone (g ∘ f)

Tactic:
fun _ _ h ↦ hg (hf h)

Premises used: Antitone
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
inst : Preorder α
f : α → α
hf : Monotone f
n : ℕ
⊢ Monotone f^[n]

Tactic:
Nat.recOn n monotone_id fun _ h ↦ h.comp hf

Premises used: Nat.recOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
s : Set α
hg : Monotone g
hf : MonotoneOn f s
⊢ MonotoneOn (g ∘ f) s

Tactic:
fun _ ha _ hb h ↦ hg (hf ha hb h)

Premises used: MonotoneOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
s : Set α
hg : Monotone g
hf : AntitoneOn f s
⊢ AntitoneOn (g ∘ f) s

Tactic:
fun _ ha _ hb h ↦ hg (hf ha hb h)

Premises used: AntitoneOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
s : Set α
hg : Antitone g
hf : AntitoneOn f s
⊢ MonotoneOn (g ∘ f) s

Tactic:
fun _ ha _ hb h ↦ hg (hf ha hb h)

Premises used: MonotoneOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
s : Set α
hg : Antitone g
hf : MonotoneOn f s
⊢ AntitoneOn (g ∘ f) s

Tactic:
fun _ ha _ hb h ↦ hg (hf ha hb h)

Premises used: AntitoneOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
hg : StrictMono g
hf : StrictMono f
⊢ StrictMono (g ∘ f)

Tactic:
fun _ _ h ↦ hg (hf h)

Premises used: StrictMono
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
hg : StrictMono g
hf : StrictAnti f
⊢ StrictAnti (g ∘ f)

Tactic:
fun _ _ h ↦ hg (hf h)

Premises used: StrictAnti
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
hg : StrictAnti g
hf : StrictAnti f
⊢ StrictMono (g ∘ f)

Tactic:
fun _ _ h ↦ hg (hf h)

Premises used: StrictMono
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
hg : StrictAnti g
hf : StrictMono f
⊢ StrictAnti (g ∘ f)

Tactic:
fun _ _ h ↦ hg (hf h)

Premises used: StrictAnti
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
inst : Preorder α
f : α → α
hf : StrictMono f
n : ℕ
⊢ StrictMono f^[n]

Tactic:
Nat.recOn n strictMono_id fun _ h ↦ h.comp hf

Premises used: Nat.recOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
s : Set α
hg : StrictMono g
hf : StrictMonoOn f s
⊢ StrictMonoOn (g ∘ f) s

Tactic:
fun _ ha _ hb h ↦ hg (hf ha hb h)

Premises used: StrictMonoOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
s : Set α
hg : StrictMono g
hf : StrictAntiOn f s
⊢ StrictAntiOn (g ∘ f) s

Tactic:
fun _ ha _ hb h ↦ hg (hf ha hb h)

Premises used: StrictAntiOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
s : Set α
hg : StrictAnti g
hf : StrictAntiOn f s
⊢ StrictMonoOn (g ∘ f) s

Tactic:
fun _ ha _ hb h ↦ hg (hf ha hb h)

Premises used: StrictMonoOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
s : Set α
hg : StrictAnti g
hf : StrictMonoOn f s
⊢ StrictAntiOn (g ∘ f) s

Tactic:
fun _ ha _ hb h ↦ hg (hf ha hb h)

Premises used: StrictAntiOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
s : Set α
t : Set β
hg : MonotoneOn g t
hf : MonotoneOn f s
hs : Set.MapsTo f s t
⊢ MonotoneOn (g ∘ f) s

Tactic:
fun _x hx _y hy hxy ↦ hg (hs hx) (hs hy) <| hf hx hy hxy

Premises used: MonotoneOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
s : Set α
t : Set β
hg : MonotoneOn g t
hf : AntitoneOn f s
hs : Set.MapsTo f s t
⊢ AntitoneOn (g ∘ f) s

Tactic:
fun _x hx _y hy hxy ↦
  hg (hs hy) (hs hx) <| hf hx hy hxy

Premises used: AntitoneOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
s : Set α
t : Set β
hg : AntitoneOn g t
hf : AntitoneOn f s
hs : Set.MapsTo f s t
⊢ MonotoneOn (g ∘ f) s

Tactic:
fun _x hx _y hy hxy ↦ hg (hs hy) (hs hx) <| hf hx hy hxy

Premises used: MonotoneOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
s : Set α
t : Set β
hg : AntitoneOn g t
hf : MonotoneOn f s
hs : Set.MapsTo f s t
⊢ AntitoneOn (g ∘ f) s

Tactic:
fun _x hx _y hy hxy ↦
  hg (hs hx) (hs hy) <| hf hx hy hxy

Premises used: AntitoneOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
s : Set α
t : Set β
hg : StrictMonoOn g t
hf : StrictMonoOn f s
hs : Set.MapsTo f s t
⊢ StrictMonoOn (g ∘ f) s

Tactic:
fun _x hx _y hy hxy ↦ hg (hs hx) (hs hy) <| hf hx hy hxy

Premises used: StrictMonoOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
s : Set α
t : Set β
hg : StrictMonoOn g t
hf : StrictAntiOn f s
hs : Set.MapsTo f s t
⊢ StrictAntiOn (g ∘ f) s

Tactic:
fun _x hx _y hy hxy ↦
  hg (hs hy) (hs hx) <| hf hx hy hxy

Premises used: StrictAntiOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
s : Set α
t : Set β
hg : StrictAntiOn g t
hf : StrictAntiOn f s
hs : Set.MapsTo f s t
⊢ StrictMonoOn (g ∘ f) s

Tactic:
fun _x hx _y hy hxy ↦ hg (hs hy) (hs hx) <| hf hx hy hxy

Premises used: StrictMonoOn
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
s : Set α
t : Set β
hg : StrictAntiOn g t
hf : StrictMonoOn f s
hs : Set.MapsTo f s t
⊢ StrictAntiOn (g ∘ f) s

Tactic:
fun _x hx _y hy hxy ↦
  hg (hs hx) (hs hy) <| hf hx hy hxy

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

Tactic:
lt_of_not_ge fun h' ↦ h.not_ge (hf h')

Premises used: lt_of_not_ge, LT.lt.not_ge
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
hf : Antitone f
a b : α
h : f a < f b
⊢ b < a

Tactic:
lt_of_not_ge fun h' ↦ h.not_ge (hf h')

Premises used: lt_of_not_ge, LT.lt.not_ge
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : MonotoneOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
h : f a < f b
⊢ a < b

Tactic:
lt_of_not_ge fun h' ↦ h.not_ge <| hf hb ha h'

Premises used: lt_of_not_ge, LT.lt.not_ge
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : AntitoneOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
h : f a < f b
⊢ b < a

Tactic:
lt_of_not_ge fun h' ↦ h.not_ge <| hf ha hb h'

Premises used: lt_of_not_ge, LT.lt.not_ge
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
inst : Preorder α
p : α → Prop
⊢ Monotone.{u, u} (α := Subtype p) (val (p := p))

Tactic:
fun _ _ ↦ id

Premises used: Monotone, id
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
inst : Preorder α
p : α → Prop
⊢ StrictMono.{u, u} (α := Subtype p) (val (p := p))

Tactic:
fun _ _ ↦ id

Premises used: StrictMono, id
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
⊢ Monotone (α := α × β) Prod.fst

Tactic:
fun _ _ ↦ And.left

Premises used: Monotone, And.left
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
⊢ Monotone (α := α × β) Prod.snd

Tactic:
fun _ _ ↦ And.right

Premises used: Monotone, And.right
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : γ → α
g : γ → β
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
simp_rw₁ :
  (∀ ⦃a b : γ⦄, a ≤ b → f a ≤ f b ∧ g a ≤ g b) ↔ (∀ ⦃a b : γ⦄, a ≤ b → f a ≤ f b) ∧ ∀ ⦃a b : γ⦄, a ≤ b → g a ≤ g b
⊢ (Monotone (β := α × β) fun (x : γ) ↦ (f x, g x)) ↔ Monotone f ∧ Monotone g

Tactic:
simp_rw [Monotone, Prod.mk_le_mk, forall_and]

Premises used: Monotone, Prod.mk_le_mk, forall_and
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : γ → α
g : γ → β
hf : Monotone f
hg : Monotone g
⊢ Monotone (β := α × β) fun (x : γ) ↦ (f x, g x)

Tactic:
monotone_prodMk_iff.2 ⟨hf, hg⟩

Premises used: Iff.mpr, monotone_prodMk_iff, And.intro
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
f : α → γ
g : β → δ
hf : Monotone f
hg : Monotone g
⊢ Monotone (Prod.map f g)

Tactic:
fun _ _ h ↦ ⟨hf h.1, hg h.2⟩

Premises used: Monotone, And.right, And.left, And.intro
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
f : α → γ
g : β → δ
hf : Antitone f
hg : Antitone g
⊢ Antitone (Prod.map f g)

Tactic:
fun _ _ h ↦ ⟨hf h.1, hg h.2⟩

Premises used: Antitone, And.right, And.left, And.intro
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : Preorder γ
inst_3 : Preorder δ
f : α → γ
g : β → δ
hf : StrictMono f
hg : StrictMono g
a b : α × β
simp :
  a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
    (Prod.map f g a).fst < (Prod.map f g b).fst ∧ (Prod.map f g a).snd ≤ (Prod.map f g b).snd ∨
      (Prod.map f g a).fst ≤ (Prod.map f g b).fst ∧ (Prod.map f g a).snd < (Prod.map f g b).snd
⊢ a < b → Prod.map f g a < Prod.map f g b

Tactic:
simp only [Prod.lt_iff]

Premises used: Prod.lt_iff
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : Preorder γ
inst_3 : Preorder δ
f : α → γ
g : β → δ
hf : StrictMono f
hg : StrictMono g
a b : α × β
⊢ a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
    (Prod.map f g a).fst < (Prod.map f g b).fst ∧ (Prod.map f g a).snd ≤ (Prod.map f g b).snd ∨
      (Prod.map f g a).fst ≤ (Prod.map f g b).fst ∧ (Prod.map f g a).snd < (Prod.map f g b).snd

Tactic:
Or.imp (And.imp hf.imp hg.monotone.imp) (And.imp hf.monotone.imp hg.imp)

Premises used: And.imp, StrictMono.monotone, StrictMono.imp, Monotone.imp, Or.imp
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : Preorder γ
inst_3 : Preorder δ
f : α → γ
g : β → δ
hf : StrictMono f
hg : StrictMono g
a b : α × β
⊢ a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
    (Prod.map f g a).fst < (Prod.map f g b).fst ∧ (Prod.map f g a).snd ≤ (Prod.map f g b).snd ∨
      (Prod.map f g a).fst ≤ (Prod.map f g b).fst ∧ (Prod.map f g a).snd < (Prod.map f g b).snd

Tactic:
exact Or.imp (And.imp hf.imp hg.monotone.imp) (And.imp hf.monotone.imp hg.imp)

Premises used: And.imp, StrictMono.monotone, StrictMono.imp, Monotone.imp, Or.imp
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : Preorder γ
inst_3 : Preorder δ
f : α → γ
g : β → δ
hf : StrictAnti f
hg : StrictAnti g
a b : α × β
simp :
  a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
    (Prod.map f g b).fst < (Prod.map f g a).fst ∧ (Prod.map f g b).snd ≤ (Prod.map f g a).snd ∨
      (Prod.map f g b).fst ≤ (Prod.map f g a).fst ∧ (Prod.map f g b).snd < (Prod.map f g a).snd
⊢ a < b → Prod.map f g b < Prod.map f g a

Tactic:
simp only [Prod.lt_iff]

Premises used: Prod.lt_iff
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : Preorder γ
inst_3 : Preorder δ
f : α → γ
g : β → δ
hf : StrictAnti f
hg : StrictAnti g
a b : α × β
⊢ a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
    (Prod.map f g b).fst < (Prod.map f g a).fst ∧ (Prod.map f g b).snd ≤ (Prod.map f g a).snd ∨
      (Prod.map f g b).fst ≤ (Prod.map f g a).fst ∧ (Prod.map f g b).snd < (Prod.map f g a).snd

Tactic:
Or.imp (And.imp hf.imp hg.antitone.imp) (And.imp hf.antitone.imp hg.imp)

Premises used: And.imp, Antitone.imp, Or.imp, StrictAnti.antitone, StrictAnti.imp
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : Preorder γ
inst_3 : Preorder δ
f : α → γ
g : β → δ
hf : StrictAnti f
hg : StrictAnti g
a b : α × β
⊢ a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
    (Prod.map f g b).fst < (Prod.map f g a).fst ∧ (Prod.map f g b).snd ≤ (Prod.map f g a).snd ∨
      (Prod.map f g b).fst ≤ (Prod.map f g a).fst ∧ (Prod.map f g b).snd < (Prod.map f g a).snd

Tactic:
exact Or.imp (And.imp hf.imp hg.antitone.imp) (And.imp hf.antitone.imp hg.imp)

Premises used: And.imp, Antitone.imp, Or.imp, StrictAnti.antitone, StrictAnti.imp
-- Module: Mathlib.Order.Monotone.Defs
Goal:
ι : Type u_1
π : ι → Type u_3
inst : DecidableEq ι
inst_1 : (i : ι) → Preorder (π i)
f : (i : ι) → π i
i : ι
⊢ Monotone (update (β := π) f i)

Tactic:
fun _ _ => update_le_update_iff'.2

Premises used: Iff.mpr, update_le_update_iff', Monotone
-- Module: Mathlib.Order.Monotone.Defs
Goal:
ι : Type u_1
π : ι → Type u_3
inst : DecidableEq ι
inst_1 : (i : ι) → Preorder (π i)
f : (i : ι) → π i
i : ι
⊢ StrictMono (update (β := π) f i)

Tactic:
fun _ _ => update_lt_update_iff.2

Premises used: update_lt_update_iff, Iff.mpr, StrictMono
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
⊢ Monotone (α := α) (const β)

Tactic:
fun _ _ h _ ↦ h

Premises used: Monotone
-- Module: Mathlib.Order.Monotone.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Nonempty β
⊢ StrictMono (α := α) (const β)

Tactic:
fun _ _ ↦ const_lt_const.2

Premises used: Iff.mpr, StrictMono, Function.const_lt_const
-- Module: Mathlib.Order.Monotone.Defs
Goal:
ι : Type u_1
α : Type u
β : ι → Type u_4
inst : (i : ι) → Preorder (β i)
inst_1 : Preorder α
f : α → (i : ι) → β i
⊢ Monotone f ↔ ∀ (i : ι), Monotone.{u, u_4} (β := β i) fun (x : α) ↦ f x i

Tactic:
simp [Monotone, Pi.le_def, @forall_comm ι]

Premises used: Monotone, forall_comm, Pi.le_def
-- Module: Mathlib.Order.Monotone.Defs
Goal:
ι : Type u_1
α : Type u
β : ι → Type u_4
inst : (i : ι) → Preorder (β i)
inst_1 : Preorder α
f : α → (i : ι) → β i
⊢ Antitone f ↔ ∀ (i : ι), Antitone.{u, u_4} (β := β i) fun (x : α) ↦ f x i

Tactic:
simp [Antitone, Pi.le_def, @forall_comm ι]

Premises used: forall_comm, Antitone, Pi.le_def
-- Module: Mathlib.Order.Monotone.Extension
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hl : BddBelow (f '' s)
hu : BddAbove (f '' s)
rcases : ∀ (a : β) (ha : a ∈ lowerBounds (f '' s)), ∃ (g : α → β), Monotone g ∧ EqOn f g s
⊢ ∃ (g : α → β), Monotone g ∧ EqOn f g s

Tactic:
rcases hl with ⟨a, ha⟩
-- Module: Mathlib.Order.Monotone.Extension
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
⊢ ∀ (x : α), BddAbove (f '' (Iic x ∩ s))

Tactic:
have hu' : ∀ x, BddAbove (f '' (Iic x ∩ s)) := fun x =>
      hu.mono (image_mono inter_subset_right)