awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
x : α
hx : x ∈ s
simp : f x = if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
⊢ f x = g x

Tactic:
simp only [g]
-- 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)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
x : α
hx : x ∈ s
⊢ IsGreatest (Iic x ∩ s) x

Tactic:
have : IsGreatest (Iic x ∩ s) x := ⟨⟨self_mem_Iic, hx⟩, fun y hy => hy.1⟩
-- 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)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
x : α
hx : x ∈ s
this : IsGreatest (Iic x ∩ s) x
rw : f x = sSup (f '' (Iic x ∩ s))
rw₁ rw₂ : f x = f x
⊢ f x = if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))

Tactic:
rw [if_neg this.nonempty.not_disjoint,
        ((h.mono inter_subset_right).map_isGreatest this).csSup_eq]

Premises used: MonotoneOn.map_isGreatest, IsGreatest.nonempty, IsGreatest.csSup_eq, if_neg, Set.inter_subset_right, MonotoneOn.mono, Set.Nonempty.not_disjoint
-- 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)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
⊢ EqOn f g s

Tactic:
have hgs : EqOn f g s := by
      intro x hx
      simp only [g]
      have : IsGreatest (Iic x ∩ s) x := ⟨⟨self_mem_Iic, hx⟩, fun y hy => hy.1⟩
      rw [if_neg this.nonempty.not_disjoint,
        ((h.mono inter_subset_right).map_isGreatest this).csSup_eq]
-- 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)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
⊢ ∃ (g : α → β), Monotone g ∧ EqOn f g s

Tactic:
⟨g, fun x y hxy => ?_, hgs⟩

Premises used: And.intro, Exists.intro
-- 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)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
refine : ∀ (x y : α) (hxy : x ≤ y), g x ≤ g y
⊢ ∃ (g : α → β), Monotone g ∧ EqOn f g s

Tactic:
refine ⟨g, fun x y hxy => ?_, hgs⟩
-- 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)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
pos : ∀ (hx : Disjoint (Iic x) s), g x ≤ g y
neg : ∀ (hx : ¬Disjoint (Iic x) s), g x ≤ g y
⊢ g x ≤ g y

Tactic:
by_cases hx : Disjoint (Iic x) s

Premises used: Disjoint, Set.Iic
-- 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)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : Disjoint (Iic x) s
pos : ∀ (hy : Disjoint (Iic y) s), g x ≤ g y
neg : ∀ (hy : ¬Disjoint (Iic y) s), g x ≤ g y
⊢ g x ≤ g y

Tactic:
by_cases hy : Disjoint (Iic y) s

Premises used: Disjoint, Set.Iic
-- 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)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : ¬Disjoint (Iic x) s
pos : ∀ (hy : Disjoint (Iic y) s), g x ≤ g y
neg : ∀ (hy : ¬Disjoint (Iic y) s), g x ≤ g y
⊢ g x ≤ g y

Tactic:
by_cases hy : Disjoint (Iic y) s

Premises used: Disjoint, Set.Iic
-- 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)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : Disjoint (Iic x) s
hy : Disjoint (Iic y) s
⊢ g x ≤ g y

Tactic:
simp only [g, if_pos, if_neg, not_false_iff, *, refl]

Premises used: if_pos, not_false_iff, refl, if_neg
-- 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)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : Disjoint (Iic x) s
hy : ¬Disjoint (Iic y) s
neg : a ≤ sSup (f '' (Iic y ∩ s))
⊢ g x ≤ g y

Tactic:
simp only [g, if_pos, if_neg, not_false_iff, *, refl]

Premises used: if_pos, not_false_iff, refl, if_neg
-- 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)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : ¬Disjoint (Iic x) s
hy : Disjoint (Iic y) s
pos : sSup (f '' (Iic x ∩ s)) ≤ a
⊢ g x ≤ g y

Tactic:
simp only [g, if_pos, if_neg, not_false_iff, *, refl]

Premises used: if_pos, not_false_iff, refl, if_neg
-- 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)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : ¬Disjoint (Iic x) s
hy : ¬Disjoint (Iic y) s
neg : sSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))
⊢ g x ≤ g y

Tactic:
simp only [g, if_pos, if_neg, not_false_iff, *, refl]

Premises used: if_pos, not_false_iff, refl, if_neg
-- 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)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : Disjoint (Iic x) s
hy : ¬Disjoint (Iic y) s
neg : ∀ (z : α) (hz : z ∈ Iic y ∩ s), a ≤ sSup (f '' (Iic y ∩ s))
⊢ a ≤ sSup (f '' (Iic y ∩ s))

Tactic:
rcases not_disjoint_iff_nonempty_inter.1 hy with ⟨z, hz⟩

Premises used: Set.not_disjoint_iff_nonempty_inter, Iff.mp
-- 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)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : Disjoint (Iic x) s
hy : ¬Disjoint (Iic y) s
z : α
hz : z ∈ Iic y ∩ s
⊢ a ≤ sSup (f '' (Iic y ∩ s))

Tactic:
le_csSup_of_le (hu' _) (mem_image_of_mem _ hz) (ha <| mem_image_of_mem _ hz.2)

Premises used: le_csSup_of_le, And.right, Set.mem_image_of_mem
-- 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)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : Disjoint (Iic x) s
hy : ¬Disjoint (Iic y) s
z : α
hz : z ∈ Iic y ∩ s
⊢ a ≤ sSup (f '' (Iic y ∩ s))

Tactic:
exact le_csSup_of_le (hu' _) (mem_image_of_mem _ hz) (ha <| mem_image_of_mem _ hz.2)

Premises used: le_csSup_of_le, And.right, Set.mem_image_of_mem
-- 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)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : ¬Disjoint (Iic x) s
hy : Disjoint (Iic y) s
⊢ sSup (f '' (Iic x ∩ s)) ≤ a

Tactic:
(hx <| hy.mono_left <| Iic_subset_Iic.2 hxy).elim

Premises used: Iff.mpr, Set.Iic_subset_Iic, False.elim, Disjoint.mono_left
-- 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)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : ¬Disjoint (Iic x) s
hy : Disjoint (Iic y) s
⊢ sSup (f '' (Iic x ∩ s)) ≤ a

Tactic:
exact (hx <| hy.mono_left <| Iic_subset_Iic.2 hxy).elim

Premises used: Iff.mpr, Set.Iic_subset_Iic, False.elim, Disjoint.mono_left
-- 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)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : ¬Disjoint (Iic x) s
hy : ¬Disjoint (Iic y) s
⊢ (Iic x ∩ s).Nonempty

Tactic:
rw [not_disjoint_iff_nonempty_inter] at hx

Premises used: Set.not_disjoint_iff_nonempty_inter
-- 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)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : ¬Disjoint (Iic x) s
hy : ¬Disjoint (Iic y) s
hx₁ : (Iic x ∩ s).Nonempty
⊢ ¬Disjoint (Iic y) s

Tactic:
rw [not_disjoint_iff_nonempty_inter] at hx

Premises used: Set.not_disjoint_iff_nonempty_inter
-- 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)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : (Iic x ∩ s).Nonempty
hy : ¬Disjoint (Iic y) s
neg : BddAbove (f '' (Iic y ∩ s))
neg₁ : (f '' (Iic x ∩ s)).Nonempty
⊢ sSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))

Tactic:
gcongr
-- 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)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : (Iic x ∩ s).Nonempty
hy : ¬Disjoint (Iic y) s
⊢ BddAbove (f '' (Iic y ∩ s))

Tactic:
hu' _
-- 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)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : (Iic x ∩ s).Nonempty
hy : ¬Disjoint (Iic y) s
⊢ (f '' (Iic x ∩ s)).Nonempty

Tactic:
hx.image _

Premises used: Set.Nonempty.image
-- 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)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun (x : α) ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : (Iic x ∩ s).Nonempty
hy : ¬Disjoint (Iic y) s
⊢ BddAbove (f '' (Iic y ∩ s))

Tactic:
exacts [hu' _, hx.image _]

Premises used: Set.Nonempty.image
-- Module: Mathlib.Order.Monotone.Extension
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : AntitoneOn f s
hl : BddBelow (f '' s)
hu : BddAbove (f '' s)
⊢ ∃ (g : α → β), Antitone g ∧ EqOn f g s

Tactic:
h.dual_right.exists_monotone_extension hu hl

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

Tactic:
fun _ _ _ _ hij => h 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 : ι → β
h : Antivary f g
s : Set ι
⊢ AntivaryOn f g s

Tactic:
fun _ _ _ _ hij => h hij

Premises used: AntivaryOn
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
⊢ MonovaryOn f g ∅

Tactic:
fun _ => False.elim

Premises used: Set.Mem, False.elim, MonovaryOn
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
⊢ AntivaryOn f g ∅

Tactic:
fun _ => False.elim

Premises used: Set.Mem, False.elim, AntivaryOn
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
⊢ MonovaryOn f g univ ↔ Monovary f g

Tactic:
⟨fun h _ _ => h trivial trivial, fun h _ _ _ _ hij => h hij⟩

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

Tactic:
⟨fun h _ _ => h trivial trivial, fun h _ _ _ _ hij => h hij⟩

Premises used: trivial, Iff.intro
-- 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 ↔
    Monovary.{u_1, u_3, u_4} (α := α) (β := β) (fun (i : (↑s : Type u_1)) ↦ f (↑i : ι)) fun (i : (↑s : Type u_1)) ↦
      g (↑i : ι)

Tactic:
simp [Monovary, MonovaryOn]

Premises used: Monovary, 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 g s ↔
    Antivary.{u_1, u_3, u_4} (α := α) (β := β) (fun (i : (↑s : Type u_1)) ↦ f (↑i : ι)) fun (i : (↑s : Type u_1)) ↦
      g (↑i : ι)

Tactic:
simp [Antivary, AntivaryOn]

Premises used: Antivary, AntivaryOn
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
s t : Set ι
hst : s ⊆ t
h : MonovaryOn f g t
⊢ MonovaryOn f g s

Tactic:
fun _ hi _ hj => h (hst hi) (hst hj)

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 : ι → β
s t : Set ι
hst : s ⊆ t
h : AntivaryOn f g t
⊢ AntivaryOn f g s

Tactic:
fun _ hi _ hj => h (hst hi) (hst hj)

Premises used: AntivaryOn
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
g : ι → β
a : α
⊢ Monovary (const ι a) g

Tactic:
fun _ _ _ => le_rfl

Premises used: le_rfl, Monovary
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
g : ι → β
a : α
⊢ Antivary (const ι a) g

Tactic:
fun _ _ _ => le_rfl

Premises used: le_rfl, Antivary
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
b : β
⊢ Monovary f (const ι b)

Tactic:
fun _ _ h =>
  (h.ne rfl).elim

Premises used: Monovary, False.elim, rfl, LT.lt.ne
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
b : β
⊢ Antivary f (const ι b)

Tactic:
fun _ _ h =>
  (h.ne rfl).elim

Premises used: Antivary, False.elim, rfl, LT.lt.ne
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
inst : Preorder α
f : ι → α
⊢ Monovary f f

Tactic:
fun _ _ => le_of_lt

Premises used: Monovary, le_of_lt
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
inst : Preorder α
f : ι → α
s : Set ι
⊢ MonovaryOn f f s

Tactic:
fun _ _ _ _ => le_of_lt

Premises used: le_of_lt, MonovaryOn
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Subsingleton ι
f : ι → α
g : ι → β
⊢ Monovary f g

Tactic:
fun _ _ h => (ne_of_apply_ne _ h.ne <| Subsingleton.elim _ _).elim

Premises used: Monovary, False.elim, ne_of_apply_ne, Subsingleton.elim, LT.lt.ne
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Subsingleton ι
f : ι → α
g : ι → β
⊢ Antivary f g

Tactic:
fun _ _ h => (ne_of_apply_ne _ h.ne <| Subsingleton.elim _ _).elim

Premises used: Antivary, False.elim, ne_of_apply_ne, Subsingleton.elim, LT.lt.ne
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Subsingleton ι
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn f g s

Tactic:
fun _ _ _ _ h => (ne_of_apply_ne _ h.ne <| Subsingleton.elim _ _).elim

Premises used: False.elim, MonovaryOn, ne_of_apply_ne, Subsingleton.elim, LT.lt.ne
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Subsingleton ι
f : ι → α
g : ι → β
s : Set ι
⊢ AntivaryOn f g s

Tactic:
fun _ _ _ _ h => (ne_of_apply_ne _ h.ne <| Subsingleton.elim _ _).elim

Premises used: False.elim, AntivaryOn, ne_of_apply_ne, Subsingleton.elim, LT.lt.ne
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
g : ι → β
a : α
s : Set ι
⊢ MonovaryOn (const ι a) g s

Tactic:
fun _ _ _ _ _ => le_rfl

Premises used: le_rfl, MonovaryOn
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
g : ι → β
a : α
s : Set ι
⊢ AntivaryOn (const ι a) g s

Tactic:
fun _ _ _ _ _ => le_rfl

Premises used: le_rfl, AntivaryOn
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
b : β
s : Set ι
⊢ MonovaryOn f (const ι b) s

Tactic:
fun _ _ _ _ h => (h.ne rfl).elim

Premises used: False.elim, MonovaryOn, rfl, LT.lt.ne
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
b : β
s : Set ι
⊢ AntivaryOn f (const ι b) s

Tactic:
fun _ _ _ _ h => (h.ne rfl).elim

Premises used: False.elim, AntivaryOn, rfl, LT.lt.ne
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
h : Monovary f g
k : ι' → ι
⊢ Monovary (f ∘ k) (g ∘ k)

Tactic:
fun _ _ hij => h hij

Premises used: Monovary
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
h : Antivary f g
k : ι' → ι
⊢ Antivary (f ∘ k) (g ∘ k)

Tactic:
fun _ _ hij => h hij

Premises used: Antivary
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
s : Set ι
h : MonovaryOn f g s
k : ι' → ι
⊢ MonovaryOn (f ∘ k) (g ∘ k) (k ⁻¹' s)

Tactic:
fun _ hi _ hj => h hi hj

Premises used: MonovaryOn
-- Module: Mathlib.Order.Monotone.Monovary
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : ι → α
g : ι → β
s : Set ι
h : AntivaryOn f g s
k : ι' → ι
⊢ AntivaryOn (f ∘ k) (g ∘ k) (k ⁻¹' s)

Tactic:
fun _ hi _ hj => h hi hj

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 : ι → β
h : Monovary f g
hf : Monotone f'
⊢ Monovary (f' ∘ f) g

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

Premises used: Monovary
-- 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 : ι → β
h : Monovary f g
hf : Antitone f'
⊢ Antivary (f' ∘ f) g

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

Premises used: Antivary
-- 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 : ι → β
h : Antivary f g
hf : Monotone f'
⊢ Antivary (f' ∘ f) g

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

Premises used: Antivary
-- 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 : ι → β
h : Antivary f g
hf : Antitone f'
⊢ Monovary (f' ∘ f) g

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

Premises used: Monovary
-- 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 : Monotone f'
⊢ MonovaryOn (f' ∘ f) g s

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

Premises used: MonovaryOn