awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : ι → α
f' : α → γ
g : ι → β
s : Set ι
h : MonovaryOn f g s
hf : Antitone f'
⊢ AntivaryOn (f' ∘ f) g s

Tactic:
fun _ hi _ hj hij => hf <| h hi hj hij

Premises used: AntivaryOn
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : ι → α
f' : α → γ
g : ι → β
s : Set ι
h : AntivaryOn f g s
hf : Monotone f'
⊢ AntivaryOn (f' ∘ f) g s

Tactic:
fun _ hi _ hj hij => hf <| h hi hj hij

Premises used: AntivaryOn
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : ι → α
f' : α → γ
g : ι → β
s : Set ι
h : AntivaryOn f g s
hf : Antitone f'
⊢ MonovaryOn (f' ∘ f) g s

Tactic:
fun _ hi _ hj hij => hf <| h hi hj hij

Premises used: MonovaryOn
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
⊢ Monovary f g → Monovary (α := αᵒᵈ) (β := βᵒᵈ) ((⇑toDual : (a : α) → αᵒᵈ) ∘ f) ((⇑toDual : (a : β) → βᵒᵈ) ∘ g)

Tactic:
swap

Premises used: Monovary, Function.swap
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
⊢ Antivary f g → Antivary (α := αᵒᵈ) (β := βᵒᵈ) ((⇑toDual : (a : α) → αᵒᵈ) ∘ f) ((⇑toDual : (a : β) → βᵒᵈ) ∘ g)

Tactic:
swap

Premises used: Antivary, Function.swap
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
⊢ Monovary f g → Antivary (α := αᵒᵈ) ((⇑toDual : (a : α) → αᵒᵈ) ∘ f) g

Tactic:
id

Premises used: Antivary, id
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
⊢ Antivary f g → Monovary (α := αᵒᵈ) ((⇑toDual : (a : α) → αᵒᵈ) ∘ f) g

Tactic:
id

Premises used: Monovary, id
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
⊢ Monovary f g → Antivary (β := βᵒᵈ) f ((⇑toDual : (a : β) → βᵒᵈ) ∘ g)

Tactic:
swap

Premises used: Monovary, Antivary, Function.swap
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
⊢ Antivary f g → Monovary (β := βᵒᵈ) f ((⇑toDual : (a : β) → βᵒᵈ) ∘ g)

Tactic:
swap

Premises used: Monovary, Antivary, Function.swap
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn f g s → MonovaryOn (α := αᵒᵈ) (β := βᵒᵈ) ((⇑toDual : (a : α) → αᵒᵈ) ∘ f) ((⇑toDual : (a : β) → βᵒᵈ) ∘ g) s

Tactic:
swap₂

Premises used: MonovaryOn, Function.swap₂
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
s : Set ι
⊢ AntivaryOn f g s → AntivaryOn (α := αᵒᵈ) (β := βᵒᵈ) ((⇑toDual : (a : α) → αᵒᵈ) ∘ f) ((⇑toDual : (a : β) → βᵒᵈ) ∘ g) s

Tactic:
swap₂

Premises used: AntivaryOn, Function.swap₂
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn f g s → AntivaryOn (α := αᵒᵈ) ((⇑toDual : (a : α) → αᵒᵈ) ∘ f) g s

Tactic:
id

Premises used: id, AntivaryOn
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
s : Set ι
⊢ AntivaryOn f g s → MonovaryOn (α := αᵒᵈ) ((⇑toDual : (a : α) → αᵒᵈ) ∘ f) g s

Tactic:
id

Premises used: id, MonovaryOn
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn f g s → AntivaryOn (β := βᵒᵈ) f ((⇑toDual : (a : β) → βᵒᵈ) ∘ g) s

Tactic:
swap₂

Premises used: MonovaryOn, AntivaryOn, Function.swap₂
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
s : Set ι
⊢ AntivaryOn f g s → MonovaryOn (β := βᵒᵈ) f ((⇑toDual : (a : β) → βᵒᵈ) ∘ g) s

Tactic:
swap₂

Premises used: MonovaryOn, AntivaryOn, Function.swap₂
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
⊢ Monovary (α := αᵒᵈ) ((⇑toDual : (a : α) → αᵒᵈ) ∘ f) g ↔ Antivary f g

Tactic:
Iff.rfl

Premises used: Antivary, Iff.rfl
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
⊢ Monovary (β := βᵒᵈ) f ((⇑toDual : (a : β) → βᵒᵈ) ∘ g) ↔ Antivary f g

Tactic:
forall_comm

Premises used: Monovary, Antivary, forall_comm
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
⊢ Antivary (α := αᵒᵈ) ((⇑toDual : (a : α) → αᵒᵈ) ∘ f) g ↔ Monovary f g

Tactic:
Iff.rfl

Premises used: Monovary, Iff.rfl
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
⊢ Antivary (β := βᵒᵈ) f ((⇑toDual : (a : β) → βᵒᵈ) ∘ g) ↔ Monovary f g

Tactic:
forall_comm

Premises used: Monovary, Antivary, forall_comm
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn (α := αᵒᵈ) ((⇑toDual : (a : α) → αᵒᵈ) ∘ f) g s ↔ AntivaryOn f g s

Tactic:
Iff.rfl

Premises used: Iff.rfl, AntivaryOn
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn (β := βᵒᵈ) f ((⇑toDual : (a : β) → βᵒᵈ) ∘ g) s ↔ AntivaryOn f g s

Tactic:
forall₂_comm

Premises used: MonovaryOn, AntivaryOn, forall₂_comm
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
s : Set ι
⊢ AntivaryOn (α := αᵒᵈ) ((⇑toDual : (a : α) → αᵒᵈ) ∘ f) g s ↔ MonovaryOn f g s

Tactic:
Iff.rfl

Premises used: Iff.rfl, MonovaryOn
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
s : Set ι
⊢ AntivaryOn (β := βᵒᵈ) f ((⇑toDual : (a : β) → βᵒᵈ) ∘ g) s ↔ MonovaryOn f g s

Tactic:
forall₂_comm

Premises used: MonovaryOn, AntivaryOn, forall₂_comm
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
inst : Preorder α
f : ι → α
inst_1 : PartialOrder ι
⊢ Monovary f id ↔ Monotone f

Tactic:
monotone_iff_forall_lt.symm

Premises used: Monovary, monotone_iff_forall_lt, Iff.symm
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
inst : Preorder α
f : ι → α
inst_1 : PartialOrder ι
⊢ Antivary f id ↔ Antitone f

Tactic:
antitone_iff_forall_lt.symm

Premises used: Antivary, antitone_iff_forall_lt, Iff.symm
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
inst : Preorder α
f : ι → α
s : Set ι
inst_1 : PartialOrder ι
⊢ MonovaryOn f id s ↔ MonotoneOn f s

Tactic:
monotoneOn_iff_forall_lt.symm

Premises used: monotoneOn_iff_forall_lt, MonovaryOn, Iff.symm
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
inst : Preorder α
f : ι → α
s : Set ι
inst_1 : PartialOrder ι
⊢ AntivaryOn f id s ↔ AntitoneOn f s

Tactic:
antitoneOn_iff_forall_lt.symm

Premises used: AntivaryOn, Iff.symm, antitoneOn_iff_forall_lt
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
inst_2 : PartialOrder ι
hf : StrictMono f
h : Monovary g f
⊢ Monotone g

Tactic:
monotone_iff_forall_lt.2 fun _a _b hab ↦ h <| hf hab

Premises used: Iff.mpr, monotone_iff_forall_lt
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
inst_2 : PartialOrder ι
hf : StrictMono f
h : Antivary g f
⊢ Antitone g

Tactic:
antitone_iff_forall_lt.2 fun _a _b hab ↦ h <| hf hab

Premises used: Iff.mpr, antitone_iff_forall_lt
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
inst_2 : PartialOrder ι
hf : StrictAnti f
h : Monovary g f
⊢ Antitone g

Tactic:
antitone_iff_forall_lt.2 fun _a _b hab ↦ h <| hf hab

Premises used: Iff.mpr, antitone_iff_forall_lt
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
inst_2 : PartialOrder ι
hf : StrictAnti f
h : Antivary g f
⊢ Monotone g

Tactic:
monotone_iff_forall_lt.2 fun _a _b hab ↦ h <| hf hab

Premises used: Iff.mpr, monotone_iff_forall_lt
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
s : Set ι
inst_2 : PartialOrder ι
hf : StrictMonoOn f s
h : MonovaryOn g f s
⊢ MonotoneOn g s

Tactic:
monotoneOn_iff_forall_lt.2 fun _a ha _b hb hab ↦ h ha hb <| hf ha hb hab

Premises used: Iff.mpr, monotoneOn_iff_forall_lt
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
s : Set ι
inst_2 : PartialOrder ι
hf : StrictMonoOn f s
h : AntivaryOn g f s
⊢ AntitoneOn g s

Tactic:
antitoneOn_iff_forall_lt.2 fun _a ha _b hb hab ↦ h ha hb <| hf ha hb hab

Premises used: Iff.mpr, antitoneOn_iff_forall_lt
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
s : Set ι
inst_2 : PartialOrder ι
hf : StrictAntiOn f s
h : MonovaryOn g f s
⊢ AntitoneOn g s

Tactic:
antitoneOn_iff_forall_lt.2 fun _a ha _b hb hab ↦ h hb ha <| hf ha hb hab

Premises used: Iff.mpr, antitoneOn_iff_forall_lt
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
s : Set ι
inst_2 : PartialOrder ι
hf : StrictAntiOn f s
h : AntivaryOn g f s
⊢ MonotoneOn g s

Tactic:
monotoneOn_iff_forall_lt.2 fun _a ha _b hb hab ↦ h hb ha <| hf ha hb hab

Premises used: Iff.mpr, monotoneOn_iff_forall_lt
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
inst_2 : LinearOrder ι
hf : Monotone f
hg : Monotone g
⊢ Monovary f g

Tactic:
fun _ _ hij => hf (hg.reflect_lt hij).le

Premises used: Monovary, Monotone.reflect_lt, LT.lt.le
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
inst_2 : LinearOrder ι
hf : Monotone f
hg : Antitone g
⊢ Antivary f g

Tactic:
(hf.monovary hg.dual_right).dual_right

Premises used: Antitone.dual_right, Monovary.dual_right, Monotone.monovary, OrderDual
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
inst_2 : LinearOrder ι
hf : Antitone f
hg : Antitone g
⊢ Monovary f g

Tactic:
(hf.dual_right.antivary hg).dual_left

Premises used: Monotone.antivary, Antitone.dual_right, Antivary.dual_left, OrderDual
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
inst_2 : LinearOrder ι
hf : Antitone f
hg : Monotone g
⊢ Antivary f g

Tactic:
(hf.monovary hg.dual_right).dual_right

Premises used: Monotone.dual_right, Monovary.dual_right, Antitone.monovary, OrderDual
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
s : Set ι
inst_2 : LinearOrder ι
hf : MonotoneOn f s
hg : MonotoneOn g s
⊢ MonovaryOn f g s

Tactic:
fun _ hi _ hj hij => hf hi hj (hg.reflect_lt hi hj hij).le

Premises used: MonotoneOn.reflect_lt, LT.lt.le, MonovaryOn
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
s : Set ι
inst_2 : LinearOrder ι
hf : MonotoneOn f s
hg : AntitoneOn g s
⊢ AntivaryOn f g s

Tactic:
(hf.monovaryOn hg.dual_right).dual_right

Premises used: AntitoneOn.dual_right, MonovaryOn.dual_right, MonotoneOn.monovaryOn, OrderDual
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
s : Set ι
inst_2 : LinearOrder ι
hf : AntitoneOn f s
hg : AntitoneOn g s
⊢ MonovaryOn f g s

Tactic:
(hf.dual_right.antivaryOn hg).dual_left

Premises used: AntitoneOn.dual_right, MonotoneOn.antivaryOn, AntivaryOn.dual_left, OrderDual
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
s : Set ι
inst_2 : LinearOrder ι
hf : AntitoneOn f s
hg : MonotoneOn g s
⊢ AntivaryOn f g s

Tactic:
(hf.monovaryOn hg.dual_right).dual_right

Premises used: AntitoneOn.monovaryOn, MonovaryOn.dual_right, MonotoneOn.dual_right, OrderDual
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder α
inst_1 : LinearOrder β
inst_2 : Preorder γ
f : ι → α
g : ι → β
g' : β → γ
s : Set ι
h : MonovaryOn f g s
hg : MonotoneOn g' (g '' s)
⊢ MonovaryOn f (g' ∘ g) s

Tactic:
fun _ hi _ hj hij =>
  h hi hj <| hg.reflect_lt (mem_image_of_mem _ hi) (mem_image_of_mem _ hj) hij

Premises used: MonotoneOn.reflect_lt, MonovaryOn, Set.mem_image_of_mem
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder α
inst_1 : LinearOrder β
inst_2 : Preorder γ
f : ι → α
g : ι → β
g' : β → γ
s : Set ι
h : MonovaryOn f g s
hg : AntitoneOn g' (g '' s)
⊢ AntivaryOn f (g' ∘ g) s

Tactic:
fun _ hi _ hj hij =>
  h hj hi <| hg.reflect_lt (mem_image_of_mem _ hi) (mem_image_of_mem _ hj) hij

Premises used: AntitoneOn.reflect_lt, AntivaryOn, Set.mem_image_of_mem
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder α
inst_1 : LinearOrder β
inst_2 : Preorder γ
f : ι → α
g : ι → β
g' : β → γ
s : Set ι
h : AntivaryOn f g s
hg : MonotoneOn g' (g '' s)
⊢ AntivaryOn f (g' ∘ g) s

Tactic:
fun _ hi _ hj hij =>
  h hi hj <| hg.reflect_lt (mem_image_of_mem _ hi) (mem_image_of_mem _ hj) hij

Premises used: MonotoneOn.reflect_lt, AntivaryOn, Set.mem_image_of_mem
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder α
inst_1 : LinearOrder β
inst_2 : Preorder γ
f : ι → α
g : ι → β
g' : β → γ
s : Set ι
h : AntivaryOn f g s
hg : AntitoneOn g' (g '' s)
⊢ MonovaryOn f (g' ∘ g) s

Tactic:
fun _ hi _ hj hij =>
  h hj hi <| hg.reflect_lt (mem_image_of_mem _ hi) (mem_image_of_mem _ hj) hij

Premises used: AntitoneOn.reflect_lt, MonovaryOn, Set.mem_image_of_mem
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
h : Monovary f g
⊢ Monovary g f

Tactic:
fun _ _ hf =>
  le_of_not_gt fun hg => hf.not_ge <| h hg

Premises used: Monovary, le_of_not_gt, LT.lt.not_ge
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
h : Antivary f g
⊢ Antivary g f

Tactic:
fun _ _ hf =>
  le_of_not_gt fun hg => hf.not_ge <| h hg

Premises used: Antivary, le_of_not_gt, LT.lt.not_ge
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
h : MonovaryOn f g s
⊢ MonovaryOn g f s

Tactic:
fun _ hi _ hj hf =>
  le_of_not_gt fun hg => hf.not_ge <| h hj hi hg

Premises used: le_of_not_gt, MonovaryOn, LT.lt.not_ge
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
h : AntivaryOn f g s
⊢ AntivaryOn g f s

Tactic:
fun _ hi _ hj hf =>
  le_of_not_gt fun hg => hf.not_ge <| h hi hj hg

Premises used: le_of_not_gt, AntivaryOn, LT.lt.not_ge
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
⊢ Monovary f g ↔ Monovary g f

Tactic:
⟨Monovary.symm, Monovary.symm⟩

Premises used: Iff.intro, Monovary.symm
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
⊢ Antivary f g ↔ Antivary g f

Tactic:
⟨Antivary.symm, Antivary.symm⟩

Premises used: Iff.intro, Antivary.symm
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn f g s ↔ MonovaryOn g f s

Tactic:
⟨MonovaryOn.symm, MonovaryOn.symm⟩

Premises used: MonovaryOn.symm, Iff.intro
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
⊢ AntivaryOn f g s ↔ AntivaryOn g f s

Tactic:
⟨AntivaryOn.symm, AntivaryOn.symm⟩

Premises used: Iff.intro, AntivaryOn.symm
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
a b : ι
⊢ Prod.Lex (fun (x1 x2 : α) ↦ x1 < x2) (Prod.Lex (fun (x1 x2 : β) ↦ x1 < x2) WellOrderingRel) (f a, g a, a)
      (f b, g b, b) ∨
    (f a, g a, a) = (f b, g b, b) ∨
      Prod.Lex (fun (x1 x2 : α) ↦ x1 < x2) (Prod.Lex (fun (x1 x2 : β) ↦ x1 < x2) WellOrderingRel) (f b, g b, b)
        (f a, g a, a)

Tactic:
trichotomous_of (Prod.Lex (· < ·) <| Prod.Lex (· < ·) WellOrderingRel) _ _

Premises used: Prod.Lex, LT.lt, trichotomous_of, WellOrderingRel
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
a b : ι
h : a = b ↔ (f a, g a, a) = (f b, g b, b)
convert_6 :
  Std.Trichotomous (α := α × β × ι)
    (Prod.Lex (fun (x1 x2 : α) ↦ x1 < x2) (Prod.Lex (fun (x1 x2 : β) ↦ x1 < x2) WellOrderingRel))
⊢ MonovaryOrder f g a b ∨ a = b ∨ MonovaryOrder f g b a

Tactic:
convert! trichotomous_of (Prod.Lex (· < ·) <| Prod.Lex (· < ·) WellOrderingRel) _ _

Premises used: Prod.Lex, LT.lt, trichotomous_of, WellOrderingRel
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
a b : ι
h : (a = b → f a = f b) ∧ (a = b → g a = g b)
⊢ a = b ↔ (f a, g a, a) = (f b, g b, b)

Tactic:
simp only [Prod.ext_iff, ← and_assoc, imp_and, iff_and_self]

Premises used: imp_and, Prod.ext_iff, and_assoc, iff_and_self
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
a b : ι
⊢ (a = b → f a = f b) ∧ (a = b → g a = g b)

Tactic:
⟨congr_arg _, congr_arg _⟩

Premises used: congr_arg, And.intro
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
a b : ι
⊢ (a = b → f a = f b) ∧ (a = b → g a = g b)

Tactic:
exact ⟨congr_arg _, congr_arg _⟩
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
a b : ι
⊢ Std.Trichotomous (α := α × β × ι)
    (Prod.Lex (fun (x1 x2 : α) ↦ x1 < x2) (Prod.Lex (fun (x1 x2 : β) ↦ x1 < x2) WellOrderingRel))

Tactic:
infer_instance
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
i : ι
⊢ ¬Prod.Lex (fun (x1 x2 : α) ↦ x1 < x2) (Prod.Lex (fun (x1 x2 : β) ↦ x1 < x2) WellOrderingRel) (f i, g i, i)
      (f i, g i, i)

Tactic:
irrefl _

Premises used: irrefl
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
i : ι
⊢ ¬Prod.Lex (fun (x1 x2 : α) ↦ x1 < x2) (Prod.Lex (fun (x1 x2 : β) ↦ x1 < x2) WellOrderingRel) (f i, g i, i)
      (f i, g i, i)

Tactic:
exact irrefl _

Premises used: irrefl
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
i j k : ι
⊢ Prod.Lex (fun (x1 x2 : α) ↦ x1 < x2) (Prod.Lex (fun (x1 x2 : β) ↦ x1 < x2) WellOrderingRel) (f i, g i, i)
      (f j, g j, j) →
    MonovaryOrder f g j k → MonovaryOrder f g i k

Tactic:
_root_.trans

Premises used: trans, MonovaryOrder
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
i j k : ι
⊢ Prod.Lex (fun (x1 x2 : α) ↦ x1 < x2) (Prod.Lex (fun (x1 x2 : β) ↦ x1 < x2) WellOrderingRel) (f i, g i, i)
      (f j, g j, j) →
    MonovaryOrder f g j k → MonovaryOrder f g i k

Tactic:
exact _root_.trans

Premises used: trans
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
⊢ MonovaryOn f g s ↔ ∃ (x : LinearOrder ι), MonotoneOn f s ∧ MonotoneOn g s

Tactic:
⟨fun hfg => ⟨‹_›, monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_,
    monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_⟩, ?_⟩

Premises used: Iff.mpr, monotoneOn_iff_forall_lt, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
refine_1 : ∀ (hfg : MonovaryOn f g s) (i : ι) (hi : i ∈ s) (j : ι) (hj : j ∈ s) (hij : i < j), f i ≤ f j
refine_2 : ∀ (hfg : MonovaryOn f g s) (i : ι) (hi : i ∈ s) (j : ι) (hj : j ∈ s) (hij : i < j), g i ≤ g j
refine_3 : (∃ (x : LinearOrder ι), MonotoneOn f s ∧ MonotoneOn g s) → MonovaryOn f g s
⊢ MonovaryOn f g s ↔ ∃ (x : LinearOrder ι), MonotoneOn f s ∧ MonotoneOn g s

Tactic:
refine ⟨fun hfg => ⟨‹_›, monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_,
    monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_⟩, ?_⟩
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
refine_1 : ∀ (h : (f i, g i, i).1 < (f j, g j, j).1), f i ≤ f j
refine_1₁ : ∀ (h : (f i, g i, i).1 = (f j, g j, j).1), f i ≤ f j
⊢ f i ≤ f j

Tactic:
obtain h | ⟨h, -⟩ := Prod.lex_iff.1 hij

Premises used: Prod.lex_iff, Iff.mp
-- Module: Mathlib.Order.Monotone.MonovaryOrder
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
h : (f i, g i, i).1 < (f j, g j, j).1
⊢ f i ≤ f j

Tactic:
h.le

Premises used: LT.lt.le