awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
h₁ : min a b < max c d
h₂ : min c d < max a b
⊢ Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a a₁ b b₁ c d : α
h₁ : a ≤ a₁
h₂ : c < b
h₃ : b₁ ≤ d
⊢ Ioo a₁ b₁ ⊆ Ioo a b ∪ Ioo c d

Tactic:
fun x hx =>
  (lt_or_ge x b).elim (fun hxb => Or.inl ⟨lt_of_le_of_lt h₁ hx.1, hxb⟩)
    fun hxb => Or.inr ⟨lt_of_lt_of_le h₂ hxb, lt_of_lt_of_le hx.2 h₃⟩

Premises used: lt_of_le_of_lt, Set.Subset, And.right, And.left, And.intro, Or.inl, lt_or_ge, Or.elim, Or.inr, lt_of_lt_of_le
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ioi a ∩ Ioi b = Ioi (max a b)

Tactic:
ext fun _ => sup_lt_iff.symm

Premises used: Set.ext, sup_lt_iff, Iff.symm
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Ico a₁ b₁ ∩ Ico a₂ b₂ = Ico (max a₁ a₂) (min b₁ b₂)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Ioo a₁ b₁ ∩ Ioo a₂ b₂ = Ioo (max a₁ a₂) (min b₁ b₂)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ Ioo a b ∩ Iio c = Ioo a (min b c)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ Iio a ∩ Ioo b c = Ioo b (min a c)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
h : b₁ < b₂
⊢ Ioc a₁ b₁ ∩ Ioo a₂ b₂ = Ioc (max a₁ a₂) b₁

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
h : b₂ ≤ b₁
⊢ Ioc a₁ b₁ ∩ Ioo a₂ b₂ = Ioo (max a₁ a₂) b₂

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
h : b₁ ≤ b₂
⊢ Ioo a₁ b₁ ∩ Ioc a₂ b₂ = Ioo (max a₁ a₂) b₁

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
h : b₂ < b₁
⊢ Ioo a₁ b₁ ∩ Ioc a₂ b₂ = Ioc (max a₁ a₂) b₂

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ Ico a b \ Iio c = Ico (max a c) b

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ Ioc a b \ Ioi c = Ioc a (min b c)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ Ioc a b ∩ Ioi c = Ioc (max a c) b

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ Ico a b ∩ Iio c = Ico a (min b c)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ Ioc a b \ Iic c = Ioc (max a c) b

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ (Ioc a b)ᶜ = Iic a ∪ Ioi b

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Iic b \ Ioc a b = Iic (min a b)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ioi a \ Ioc a b = Ioi (max a b)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
hab : a ≤ b
⊢ Iic b \ Ioc a b = Iic a

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ Ioc a b ∪ Ioc a c = Ioc a (max b c)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ Ioc a c ∪ Ioc b c = Ioc (min a b) c

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ioc a b ∪ Ioc b a = Ioc (min a b) (max a b)

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc (min a (min b c)) (max a (max b c))

Tactic:
grind
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
inst : Preorder α
⊢ Antitone.{u_1, u_1} (α := α) Ici

Tactic:
fun _ _ => Ici_subset_Ici.2

Premises used: Iff.mpr, Set.Ici_subset_Ici, Antitone
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
inst : Preorder α
⊢ Monotone.{u_1, u_1} (α := α) Iic

Tactic:
fun _ _ => Iic_subset_Iic.2

Premises used: Iff.mpr, Set.Iic_subset_Iic, Monotone
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
inst : Preorder α
⊢ Antitone.{u_1, u_1} (α := α) Ioi

Tactic:
fun _ _ => Ioi_subset_Ioi

Premises used: Antitone, Set.Ioi_subset_Ioi
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
inst : Preorder α
⊢ Monotone.{u_1, u_1} (α := α) Iio

Tactic:
fun _ _ => Iio_subset_Iio

Premises used: Monotone, Set.Iio_subset_Iio
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : Monotone f
⊢ Antitone.{u_1, u_2} (β := Set β) fun (x : α) ↦ Ici (f x)

Tactic:
antitone_Ici.comp_monotone hf

Premises used: Set.Ici, setOf, Antitone.comp_monotone, antitone_Ici
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : MonotoneOn f s
⊢ AntitoneOn.{u_1, u_2} (β := Set β) (fun (x : α) ↦ Ici (f x)) s

Tactic:
antitone_Ici.comp_monotoneOn hf

Premises used: Set.Ici, setOf, antitone_Ici, Antitone.comp_monotoneOn
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : Antitone f
⊢ Monotone.{u_1, u_2} (β := Set β) fun (x : α) ↦ Ici (f x)

Tactic:
antitone_Ici.comp hf

Premises used: Set.Ici, setOf, Antitone.comp, antitone_Ici
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : AntitoneOn f s
⊢ MonotoneOn.{u_1, u_2} (β := Set β) (fun (x : α) ↦ Ici (f x)) s

Tactic:
antitone_Ici.comp_antitoneOn hf

Premises used: Antitone.comp_antitoneOn, Set.Ici, setOf, antitone_Ici
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : Monotone f
⊢ Monotone.{u_1, u_2} (β := Set β) fun (x : α) ↦ Iic (f x)

Tactic:
monotone_Iic.comp hf

Premises used: setOf, Monotone.comp, monotone_Iic, Set.Iic
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : MonotoneOn f s
⊢ MonotoneOn.{u_1, u_2} (β := Set β) (fun (x : α) ↦ Iic (f x)) s

Tactic:
monotone_Iic.comp_monotoneOn hf

Premises used: setOf, monotone_Iic, Set.Iic, Monotone.comp_monotoneOn
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : Antitone f
⊢ Antitone.{u_1, u_2} (β := Set β) fun (x : α) ↦ Iic (f x)

Tactic:
monotone_Iic.comp_antitone hf

Premises used: setOf, monotone_Iic, Set.Iic, Monotone.comp_antitone
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : AntitoneOn f s
⊢ AntitoneOn.{u_1, u_2} (β := Set β) (fun (x : α) ↦ Iic (f x)) s

Tactic:
monotone_Iic.comp_antitoneOn hf

Premises used: setOf, monotone_Iic, Set.Iic, Monotone.comp_antitoneOn
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : Monotone f
⊢ Antitone.{u_1, u_2} (β := Set β) fun (x : α) ↦ Ioi (f x)

Tactic:
antitone_Ioi.comp_monotone hf

Premises used: Set.Ioi, antitone_Ioi, setOf, Antitone.comp_monotone
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : MonotoneOn f s
⊢ AntitoneOn.{u_1, u_2} (β := Set β) (fun (x : α) ↦ Ioi (f x)) s

Tactic:
antitone_Ioi.comp_monotoneOn hf

Premises used: Set.Ioi, antitone_Ioi, setOf, Antitone.comp_monotoneOn
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : Antitone f
⊢ Monotone.{u_1, u_2} (β := Set β) fun (x : α) ↦ Ioi (f x)

Tactic:
antitone_Ioi.comp hf

Premises used: Set.Ioi, antitone_Ioi, setOf, Antitone.comp
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : AntitoneOn f s
⊢ MonotoneOn.{u_1, u_2} (β := Set β) (fun (x : α) ↦ Ioi (f x)) s

Tactic:
antitone_Ioi.comp_antitoneOn hf

Premises used: Antitone.comp_antitoneOn, Set.Ioi, antitone_Ioi, setOf
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : Monotone f
⊢ Monotone.{u_1, u_2} (β := Set β) fun (x : α) ↦ Iio (f x)

Tactic:
monotone_Iio.comp hf

Premises used: setOf, Monotone.comp, monotone_Iio, Set.Iio
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : MonotoneOn f s
⊢ MonotoneOn.{u_1, u_2} (β := Set β) (fun (x : α) ↦ Iio (f x)) s

Tactic:
monotone_Iio.comp_monotoneOn hf

Premises used: setOf, monotone_Iio, Set.Iio, Monotone.comp_monotoneOn
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : Antitone f
⊢ Antitone.{u_1, u_2} (β := Set β) fun (x : α) ↦ Iio (f x)

Tactic:
monotone_Iio.comp_antitone hf

Premises used: setOf, monotone_Iio, Set.Iio, Monotone.comp_antitone
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : AntitoneOn f s
⊢ AntitoneOn.{u_1, u_2} (β := Set β) (fun (x : α) ↦ Iio (f x)) s

Tactic:
monotone_Iio.comp_antitoneOn hf

Premises used: setOf, monotone_Iio, Monotone.comp_antitoneOn, Set.Iio
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f g : α → β
hf : Monotone f
hg : Antitone g
⊢ Antitone.{u_1, u_2} (β := Set β) fun (x : α) ↦ Icc (f x) (g x)

Tactic:
hf.Ici.inter hg.Iic

Premises used: Monotone.Ici, Set.Ici, Set.Mem, setOf, Set.inter, Set.Icc, Antitone.inter, Antitone.Iic
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f g : α → β
s : Set α
hf : MonotoneOn f s
hg : AntitoneOn g s
⊢ AntitoneOn.{u_1, u_2} (β := Set β) (fun (x : α) ↦ Icc (f x) (g x)) s

Tactic:
hf.Ici.inter hg.Iic

Premises used: Set.Ici, Set.Mem, setOf, AntitoneOn.inter, MonotoneOn.Ici, Set.inter, AntitoneOn.Iic, Set.Icc
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f g : α → β
hf : Antitone f
hg : Monotone g
⊢ Monotone.{u_1, u_2} (β := Set β) fun (x : α) ↦ Icc (f x) (g x)

Tactic:
hf.Ici.inter hg.Iic

Premises used: Set.Ici, Set.Mem, setOf, Monotone.inter, Set.inter, Antitone.Ici, Set.Icc, Monotone.Iic
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f g : α → β
s : Set α
hf : AntitoneOn f s
hg : MonotoneOn g s
⊢ MonotoneOn.{u_1, u_2} (β := Set β) (fun (x : α) ↦ Icc (f x) (g x)) s

Tactic:
hf.Ici.inter hg.Iic

Premises used: AntitoneOn.Ici, Set.Ici, Set.Mem, setOf, Set.inter, MonotoneOn.Iic, MonotoneOn.inter, Set.Icc
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f g : α → β
hf : Monotone f
hg : Antitone g
⊢ Antitone.{u_1, u_2} (β := Set β) fun (x : α) ↦ Ico (f x) (g x)

Tactic:
hf.Ici.inter hg.Iio

Premises used: Monotone.Ici, Set.Ici, Set.Mem, setOf, Antitone.Iio, Set.inter, Set.Ico, Antitone.inter
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f g : α → β
s : Set α
hf : MonotoneOn f s
hg : AntitoneOn g s
⊢ AntitoneOn.{u_1, u_2} (β := Set β) (fun (x : α) ↦ Ico (f x) (g x)) s

Tactic:
hf.Ici.inter hg.Iio

Premises used: Set.Ici, Set.Mem, setOf, AntitoneOn.inter, MonotoneOn.Ici, Set.inter, Set.Ico, AntitoneOn.Iio
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f g : α → β
hf : Antitone f
hg : Monotone g
⊢ Monotone.{u_1, u_2} (β := Set β) fun (x : α) ↦ Ico (f x) (g x)

Tactic:
hf.Ici.inter hg.Iio

Premises used: Set.Ici, Set.Mem, setOf, Monotone.Iio, Monotone.inter, Set.inter, Antitone.Ici, Set.Ico
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f g : α → β
s : Set α
hf : AntitoneOn f s
hg : MonotoneOn g s
⊢ MonotoneOn.{u_1, u_2} (β := Set β) (fun (x : α) ↦ Ico (f x) (g x)) s

Tactic:
hf.Ici.inter hg.Iio

Premises used: AntitoneOn.Ici, Set.Ici, Set.Mem, MonotoneOn.Iio, setOf, Set.inter, MonotoneOn.inter, Set.Ico
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f g : α → β
hf : Monotone f
hg : Antitone g
⊢ Antitone.{u_1, u_2} (β := Set β) fun (x : α) ↦ Ioc (f x) (g x)

Tactic:
hf.Ioi.inter hg.Iic

Premises used: Set.Ioc, Set.Ioi, Set.Mem, setOf, Set.inter, Monotone.Ioi, Antitone.inter, Antitone.Iic
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f g : α → β
s : Set α
hf : MonotoneOn f s
hg : AntitoneOn g s
⊢ AntitoneOn.{u_1, u_2} (β := Set β) (fun (x : α) ↦ Ioc (f x) (g x)) s

Tactic:
hf.Ioi.inter hg.Iic

Premises used: Set.Ioc, Set.Ioi, Set.Mem, setOf, AntitoneOn.inter, Set.inter, AntitoneOn.Iic, MonotoneOn.Ioi
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f g : α → β
hf : Antitone f
hg : Monotone g
⊢ Monotone.{u_1, u_2} (β := Set β) fun (x : α) ↦ Ioc (f x) (g x)

Tactic:
hf.Ioi.inter hg.Iic

Premises used: Set.Ioc, Set.Ioi, Set.Mem, setOf, Monotone.inter, Set.inter, Antitone.Ioi, Monotone.Iic
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f g : α → β
s : Set α
hf : AntitoneOn f s
hg : MonotoneOn g s
⊢ MonotoneOn.{u_1, u_2} (β := Set β) (fun (x : α) ↦ Ioc (f x) (g x)) s

Tactic:
hf.Ioi.inter hg.Iic

Premises used: Set.Ioc, Set.Ioi, Set.Mem, setOf, Set.inter, MonotoneOn.Iic, AntitoneOn.Ioi, MonotoneOn.inter
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f g : α → β
hf : Monotone f
hg : Antitone g
⊢ Antitone.{u_1, u_2} (β := Set β) fun (x : α) ↦ Ioo (f x) (g x)

Tactic:
hf.Ioi.inter hg.Iio

Premises used: Set.Ioi, Set.Mem, setOf, Antitone.Iio, Set.inter, Monotone.Ioi, Antitone.inter, Set.Ioo
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f g : α → β
s : Set α
hf : MonotoneOn f s
hg : AntitoneOn g s
⊢ AntitoneOn.{u_1, u_2} (β := Set β) (fun (x : α) ↦ Ioo (f x) (g x)) s

Tactic:
hf.Ioi.inter hg.Iio

Premises used: Set.Ioi, Set.Mem, setOf, AntitoneOn.inter, Set.inter, AntitoneOn.Iio, MonotoneOn.Ioi, Set.Ioo
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f g : α → β
hf : Antitone f
hg : Monotone g
⊢ Monotone.{u_1, u_2} (β := Set β) fun (x : α) ↦ Ioo (f x) (g x)

Tactic:
hf.Ioi.inter hg.Iio

Premises used: Set.Ioi, Set.Mem, setOf, Monotone.Iio, Monotone.inter, Set.inter, Antitone.Ioi, Set.Ioo
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f g : α → β
s : Set α
hf : AntitoneOn f s
hg : MonotoneOn g s
⊢ MonotoneOn.{u_1, u_2} (β := Set β) (fun (x : α) ↦ Ioo (f x) (g x)) s

Tactic:
hf.Ioi.inter hg.Iio

Premises used: Set.Ioi, Set.Mem, MonotoneOn.Iio, setOf, Set.inter, AntitoneOn.Ioi, MonotoneOn.inter, Set.Ioo
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
inst_1 : LinearOrder β
f g : α → β
a b : β
hf : Antitone f
hg : Monotone g
ha : IsGLB (range f) a
hb : IsLUB (range g) b
⊢ ⋃ (x : α), Ioo (f x) (g x) = Ioo a b

Tactic:
calc
    ⋃ x, Ioo (f x) (g x) = (⋃ x, Ioi (f x)) ∩ ⋃ x, Iio (g x) :=
      iUnion_inter_of_monotone hf.Ioi hg.Iio
    _ = Ioi a ∩ Iio b := congr_arg₂ (· ∩ ·) ha.iUnion_Ioi_eq hb.iUnion_Iio_eq

Premises used: Set.Ioi, Trans.trans, Set.Mem, setOf, Monotone.Iio, IsLUB.iUnion_Iio_eq, Set.inter, Antitone.Ioi, Inter.inter, Set.iUnion_inter_of_monotone, Set.Iio, Set.Ioo, IsGLB.iUnion_Ioi_eq, congr_arg₂
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
ψ : α → β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
n : α
hψ : ∀ m < n, ψ m < ψ (succ m)
⊢ StrictMonoOn ψ (Iic n)

Tactic:
strictMonoOn_of_lt_succ ordConnected_Iic fun _a ha' _ ha ↦
    hψ _ <| (succ_le_iff_of_not_isMax ha').1 ha

Premises used: Set.ordConnected_Iic, Order.succ_le_iff_of_not_isMax, Iff.mp, strictMonoOn_of_lt_succ
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
ψ : α → β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
n : α
hψ : ∀ m < n, ψ (succ m) < ψ m
⊢ StrictAntiOn ψ (Iic n)

Tactic:
fun i hi j hj hij =>
  @strictMonoOn_Iic_of_lt_succ α βᵒᵈ _ _ ψ _ _ n hψ i hi j hj hij

Premises used: StrictAntiOn, strictMonoOn_Iic_of_lt_succ
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
ψ : α → β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
n : α
hψ : ∀ (m : α), n < m → ψ (pred m) < ψ m
⊢ StrictMonoOn ψ (Ici n)

Tactic:
fun i hi j hj hij =>
  @strictMonoOn_Iic_of_lt_succ αᵒᵈ βᵒᵈ _ _ ψ _ _ n hψ j hj i hi hij

Premises used: StrictMonoOn, strictMonoOn_Iic_of_lt_succ
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
ψ : α → β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
n : α
hψ : ∀ (m : α), n < m → ψ m < ψ (pred m)
⊢ StrictAntiOn ψ (Ici n)

Tactic:
fun i hi j hj hij =>
  @strictAntiOn_Iic_of_succ_lt αᵒᵈ βᵒᵈ _ _ ψ _ _ n hψ j hj i hi hij

Premises used: StrictAntiOn, strictAntiOn_Iic_of_succ_lt
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
hφ : StrictMonoOn φ (Iic n)
revert : ∀ (hφ : StrictMonoOn φ (Iic n)), ∀ m ≤ n, m ≤ φ m
⊢ ∀ m ≤ n, m ≤ φ m

Tactic:
revert hφ
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
⊢ ∀ (hφ : StrictMonoOn φ (Iic n)), ∀ m ≤ n, m ≤ φ m

Tactic:
Succ.rec_bot (fun n => StrictMonoOn φ (Set.Iic n) → ∀ m ≤ n, m ≤ φ m)
      (fun _ _ hm => hm.trans bot_le) ?_ _

Premises used: LE.le.trans, bot_le, Succ.rec_bot
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
n₁ :
  ∀ (a : α),
    (fun (n : α) ↦ StrictMonoOn φ (Iic n) → ∀ m ≤ n, m ≤ φ m) a →
      (fun (n : α) ↦ StrictMonoOn φ (Iic n) → ∀ m ≤ n, m ≤ φ m) (succ a)
⊢ ∀ (hφ : StrictMonoOn φ (Iic n)), ∀ m ≤ n, m ≤ φ m

Tactic:
refine
    Succ.rec_bot (fun n => StrictMonoOn φ (Set.Iic n) → ∀ m ≤ n, m ≤ φ m)
      (fun _ _ hm => hm.trans bot_le) ?_ _

Premises used: LE.le.trans, bot_le, Succ.rec_bot
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ succ k
pos : ∀ (hk : IsMax k), m ≤ φ m
neg : ∀ (hk : ¬IsMax k), m ≤ φ m
⊢ m ≤ φ m

Tactic:
by_cases hk : IsMax k

Premises used: IsMax
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ succ k
hk : IsMax k
⊢ m ≤ k

Tactic:
rw [succ_eq_iff_isMax.2 hk] at hm

Premises used: Iff.mpr, Order.succ_eq_iff_isMax
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ succ k
hk : IsMax k
hm₁ : m ≤ k
⊢ IsMax k

Tactic:
rw [succ_eq_iff_isMax.2 hk] at hm

Premises used: Iff.mpr, Order.succ_eq_iff_isMax
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ k
hk : IsMax k
⊢ m ≤ φ m

Tactic:
ih (hφ.mono <| Iic_subset_Iic.2 (le_succ _)) _ hm

Premises used: Iff.mpr, Set.Iic_subset_Iic, StrictMonoOn.mono, Order.le_succ
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ k
hk : IsMax k
⊢ m ≤ φ m

Tactic:
exact ih (hφ.mono <| Iic_subset_Iic.2 (le_succ _)) _ hm

Premises used: Iff.mpr, Set.Iic_subset_Iic, StrictMonoOn.mono, Order.le_succ
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ succ k
hk : ¬IsMax k
neg : ∀ (hm : succ k ≤ succ k), succ k ≤ φ (succ k)
neg₁ : ∀ (h : m ≤ k), m ≤ φ m
⊢ m ≤ φ m

Tactic:
obtain rfl | h := le_succ_iff_eq_or_le.1 hm

Premises used: Iff.mp, rfl, Order.le_succ_iff_eq_or_le
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
hk : ¬IsMax k
hm : succ k ≤ succ k
⊢ k ≤ φ k

Tactic:
specialize ih (StrictMonoOn.mono hφ fun x hx => le_trans hx (le_succ _)) k le_rfl

Premises used: le_rfl, StrictMonoOn.mono, Order.le_succ, le_trans
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
k : α
hφ : StrictMonoOn φ (Iic (succ k))
hk : ¬IsMax k
hm : succ k ≤ succ k
ih : k ≤ φ k
neg : succ (φ k) ≤ φ (succ k)
⊢ succ k ≤ φ (succ k)

Tactic:
nth_grw 1 [ih]
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
k : α
hφ : StrictMonoOn φ (Iic (succ k))
hk : ¬IsMax k
hm : succ k ≤ succ k
ih : k ≤ φ k
⊢ succ (φ k) ≤ φ (succ k)

Tactic:
succ_le_of_lt (hφ (le_succ _) le_rfl ?_)

Premises used: le_rfl, Order.succ_le_of_lt, Order.le_succ
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
k : α
hφ : StrictMonoOn φ (Iic (succ k))
hk : ¬IsMax k
hm : succ k ≤ succ k
ih : k ≤ φ k
neg : k < succ k
⊢ succ (φ k) ≤ φ (succ k)

Tactic:
refine succ_le_of_lt (hφ (le_succ _) le_rfl ?_)

Premises used: le_rfl, Order.succ_le_of_lt, Order.le_succ
-- Module: Mathlib.Order.Interval.Set.Monotone
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
k : α
hφ : StrictMonoOn φ (Iic (succ k))
hk : ¬IsMax k
hm : succ k ≤ succ k
ih : k ≤ φ k
⊢ k < succ k

Tactic:
lt_succ_of_not_isMax hk

Premises used: Order.lt_succ_of_not_isMax