awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β →o γ
f : α →o β
a : NonemptyInterval α
⊢ map g (map f a) = map (g.comp f) a

Tactic:
rfl

Premises used: OrderHom.comp, Prod.map, rfl, NonemptyInterval.map
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α →o β
a : NonemptyInterval α
⊢ Eq (α := NonemptyInterval βᵒᵈ)
    ((dual : (a : NonemptyInterval β) → NonemptyInterval βᵒᵈ) (map f a) : NonemptyInterval βᵒᵈ)
    (map.{u_1, u_2} (α := αᵒᵈ) ((OrderHom.dual : (a : α →o β) → αᵒᵈ →o βᵒᵈ) f)
        ((dual : (a : NonemptyInterval α) → NonemptyInterval αᵒᵈ) a) :
      NonemptyInterval βᵒᵈ)

Tactic:
rfl

Premises used: Prod.map, OrderDual, rfl, NonemptyInterval.map
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β → γ
h₀ : ∀ (b : β), Monotone.{u_1, u_3} (β := γ) fun (a : α) ↦ f a b
h₁ : ∀ (a : α), Monotone (f a)
a : α
b : β
⊢ map₂ f h₀ h₁ (pure a) (pure b) = pure (f a b)

Tactic:
rfl

Premises used: NonemptyInterval.pure, NonemptyInterval.map₂, rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β → γ
h₀ : ∀ (b : β), Monotone.{u_1, u_3} (β := γ) fun (a : α) ↦ f a b
h₁ : ∀ (a : α), Monotone (f a)
s : NonemptyInterval α
t : NonemptyInterval β
⊢ Eq (α := NonemptyInterval γᵒᵈ)
    ((dual : (a : NonemptyInterval γ) → NonemptyInterval γᵒᵈ) (map₂ f h₀ h₁ s t) : NonemptyInterval γᵒᵈ)
    (map₂
        (fun (a : αᵒᵈ) (b : βᵒᵈ) ↦
          (toDual : (a : γ) → γᵒᵈ) (f ((ofDual : (a : αᵒᵈ) → α) a) ((ofDual : (a : βᵒᵈ) → β) b)))
        ⋯ ⋯ ((dual : (a : NonemptyInterval α) → NonemptyInterval αᵒᵈ) s)
        ((dual : (a : NonemptyInterval β) → NonemptyInterval βᵒᵈ) t) :
      NonemptyInterval γᵒᵈ)

Tactic:
rfl

Premises used: NonemptyInterval.map₂, Prod.swap, OrderDual, rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : BoundedOrder α
⊢ Eq.{u_1 + 1} (α := NonemptyInterval αᵒᵈ) ((dual : (a : NonemptyInterval α) → NonemptyInterval αᵒᵈ) ⊤) ⊤

Tactic:
rfl

Premises used: Prod.swap, OrderDual, rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : PartialOrder α
s t : NonemptyInterval α
⊢ (↑s : Set α) ⊆ (↑t : Set α) ↔ s ≤ t

Tactic:
(@coeHom α _).le_iff_le

Premises used: NonemptyInterval.coeHom, setOf, Set.Icc, OrderEmbedding.le_iff_le
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : PartialOrder α
s t : NonemptyInterval α
⊢ (↑s : Set α) ⊂ (↑t : Set α) ↔ s < t

Tactic:
(@coeHom α _).lt_iff_lt

Premises used: NonemptyInterval.coeHom, setOf, Set.Icc, OrderEmbedding.lt_iff_lt
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : PartialOrder α
⊢ Eq (α := (a : NonemptyInterval α) → Set α) (⇑coeHom : (a : NonemptyInterval α) → Set α) SetLike.coe

Tactic:
rfl

Premises used: setOf, Set.Icc, rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : PartialOrder α
s : NonemptyInterval α
⊢ (↑s : Set α) = Icc s.toProd.1 s.toProd.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a : α
⊢ (↑(pure a) : Set α) = {a}

Tactic:
Icc_self _

Premises used: Set.Icc_self
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
rw : b ∈ (↑(pure a) : Set α) ↔ b = a
rw₁ : Membership.mem (γ := Set α) {a} b ↔ b = a
rw₂ rw₃ : b = a ↔ b = a
⊢ Membership.mem (γ := NonemptyInterval α) (pure a) b ↔ b = a

Tactic:
rw [← SetLike.mem_coe, coe_pure, mem_singleton_iff]

Premises used: Set.mem_singleton_iff, SetLike.mem_coe, NonemptyInterval.coe_pure
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
⊢ (↑⊤ : Set α) = univ

Tactic:
Icc_bot_top

Premises used: Set.Icc_bot_top
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : PartialOrder α
s : NonemptyInterval α
⊢ (↑((dual : (a : NonemptyInterval α) → NonemptyInterval αᵒᵈ) s : NonemptyInterval αᵒᵈ) : Set αᵒᵈ) =
    (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (↑s : Set α)

Tactic:
Icc_toDual

Premises used: Set.Icc_toDual
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f : α →o β
s : NonemptyInterval α
⊢ (⇑f : (a : α) → β) '' (↑s : Set α) ⊆ (↑(map f s) : Set β)

Tactic:
image_subset_iff.2 fun _ ha => ⟨f.mono ha.1, f.mono ha.2⟩

Premises used: Iff.mpr, OrderHom.mono, And.right, And.left, And.intro, Set.image_subset_iff
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Lattice α
s t : NonemptyInterval α
⊢ (s ⊔ t).toProd.1 = s.toProd.1 ⊓ t.toProd.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Lattice α
s t : NonemptyInterval α
⊢ (s ⊔ t).toProd.2 = s.toProd.2 ⊔ t.toProd.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : LE α
⊢ CanLift.{u_1 + 1, u_1 + 1} (Interval α) (NonemptyInterval α) coe fun (r : Interval α) ↦ r ≠ ⊥

Tactic:
WithBot.canLift

Premises used: Interval, Interval.coe, WithBot.canLift
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : LE α
⊢ Injective.{u_1 + 1, u_1 + 1} (α := NonemptyInterval α) coe

Tactic:
WithBot.coe_injective

Premises used: WithBot.coe_injective, Interval, Interval.coe
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : LE α
s t : NonemptyInterval α
⊢ (↑s : Interval α) = (↑t : Interval α) ↔ s = t

Tactic:
WithBot.coe_inj

Premises used: Interval, Interval.coe, WithBot.coe_inj
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : LE α
p : Interval α → Prop
⊢ (∀ (s : Interval α), p s) ↔ p ⊥ ∧ ∀ (s : NonemptyInterval α), p (↑s : Interval α)

Tactic:
Option.forall

Premises used: WithBot.some, WithBot, Option.forall, Interval, Interval.coe
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : LE α
p : Interval α → Prop
⊢ (∃ (s : Interval α), p s) ↔ p ⊥ ∨ ∃ (s : NonemptyInterval α), p (↑s : Interval α)

Tactic:
Option.exists

Premises used: WithBot.some, WithBot, Interval, Interval.coe, Option.exists
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Preorder α
⊢ Injective.{u_1 + 1, u_1 + 1} (α := α) (β := Interval α) pure

Tactic:
coe_injective.comp NonemptyInterval.pure_injective

Premises used: WithBot.some, Interval.pure, Interval.coe_injective, NonemptyInterval.pure_injective, Interval.coe, Function.Injective.comp
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Eq (α := Interval αᵒᵈ) ((dual : (a : Interval α) → Interval αᵒᵈ) (pure a) : Interval αᵒᵈ)
    (pure ((toDual : (a : α) → αᵒᵈ) a) : Interval αᵒᵈ)

Tactic:
rfl

Premises used: WithBot.some, Interval.pure, NonemptyInterval.pure, Interval.coe, Prod.swap, OrderDual, WithBot.map, rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Preorder α
⊢ Eq.{u_1 + 1} (α := Interval αᵒᵈ) ((dual : (a : Interval α) → Interval αᵒᵈ) ⊥) ⊥

Tactic:
rfl

Premises used: WithBot.map, rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Ne (α := Interval α) (pure a) ⊥

Tactic:
WithBot.coe_ne_bot

Premises used: Interval.pure, Interval, Interval.coe, WithBot.coe_ne_bot
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Ne (α := Interval α) ⊥ (pure a)

Tactic:
WithBot.bot_ne_coe

Premises used: Interval.pure, Interval, Interval.coe, WithBot.bot_ne_coe
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Nonempty α
⊢ Nontrivial.{u_1} (Interval α)

Tactic:
Option.nontrivial

Premises used: WithBot, Interval, Option.nontrivial
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α →o β
a : α
⊢ map f (pure a) = pure ((f : (a : α) → β) a)

Tactic:
rfl

Premises used: WithBot.some, Interval.pure, NonemptyInterval.pure, Prod.map, Interval.coe, rfl, NonemptyInterval.map
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β →o γ
f : α →o β
s : Interval α
⊢ map g (map f s) = map (g.comp f) s

Tactic:
Option.map_map _ _ _

Premises used: WithBot, Prod.map, Interval, Interval.map, Option.map_map, WithBot.map, NonemptyInterval.map
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α →o β
s : Interval α
bot :
  Eq (α := Interval βᵒᵈ) ((dual : (a : Interval β) → Interval βᵒᵈ) (map f ⊥) : Interval βᵒᵈ)
    (map.{u_1, u_2} (α := αᵒᵈ) ((OrderHom.dual : (a : α →o β) → αᵒᵈ →o βᵒᵈ) f)
        ((dual : (a : Interval α) → Interval αᵒᵈ) ⊥) :
      Interval βᵒᵈ)
coe :
  ∀ (a : NonemptyInterval α),
    Eq (α := Interval βᵒᵈ) ((dual : (a : Interval β) → Interval βᵒᵈ) (map f (↑a : Interval α)) : Interval βᵒᵈ)
      (map.{u_1, u_2} (α := αᵒᵈ) ((OrderHom.dual : (a : α →o β) → αᵒᵈ →o βᵒᵈ) f)
          ((dual : (a : Interval α) → Interval αᵒᵈ) (↑a : Interval α)) :
        Interval βᵒᵈ)
⊢ Eq (α := Interval βᵒᵈ) ((dual : (a : Interval β) → Interval βᵒᵈ) (map f s) : Interval βᵒᵈ)
    (map.{u_1, u_2} (α := αᵒᵈ) ((OrderHom.dual : (a : α →o β) → αᵒᵈ →o βᵒᵈ) f)
        ((dual : (a : Interval α) → Interval αᵒᵈ) s) :
      Interval βᵒᵈ)

Tactic:
cases s
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α →o β
⊢ Eq (α := Interval βᵒᵈ) ((dual : (a : Interval β) → Interval βᵒᵈ) (map f ⊥) : Interval βᵒᵈ)
    (map.{u_1, u_2} (α := αᵒᵈ) ((OrderHom.dual : (a : α →o β) → αᵒᵈ →o βᵒᵈ) f)
        ((dual : (a : Interval α) → Interval αᵒᵈ) ⊥) :
      Interval βᵒᵈ)

Tactic:
rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α →o β
a : NonemptyInterval α
⊢ Eq (α := Interval βᵒᵈ) ((dual : (a : Interval β) → Interval βᵒᵈ) (map f (↑a : Interval α)) : Interval βᵒᵈ)
    (map.{u_1, u_2} (α := αᵒᵈ) ((OrderHom.dual : (a : α →o β) → αᵒᵈ →o βᵒᵈ) f)
        ((dual : (a : Interval α) → Interval αᵒᵈ) (↑a : Interval α)) :
      Interval βᵒᵈ)

Tactic:
WithBot.map_comm rfl _

Premises used: WithBot.map_comm, Prod.map, Interval, Interval.map, OrderDual, WithBot.map, rfl, NonemptyInterval.map
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α →o β
a : NonemptyInterval α
⊢ Eq (α := Interval βᵒᵈ) ((dual : (a : Interval β) → Interval βᵒᵈ) (map f (↑a : Interval α)) : Interval βᵒᵈ)
    (map.{u_1, u_2} (α := αᵒᵈ) ((OrderHom.dual : (a : α →o β) → αᵒᵈ →o βᵒᵈ) f)
        ((dual : (a : Interval α) → Interval αᵒᵈ) (↑a : Interval α)) :
      Interval βᵒᵈ)

Tactic:
exact WithBot.map_comm rfl _

Premises used: WithBot.map_comm, rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : NonemptyInterval α
⊢ (↑s : Interval α) ≤ (↑t : Interval α) ↔ s ≤ t

Tactic:
WithBot.coe_le_coe

Premises used: WithBot.coe_le_coe, Interval.coe
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : BoundedOrder α
⊢ Eq.{u_1 + 1} (α := Interval αᵒᵈ) ((dual : (a : Interval α) → Interval αᵒᵈ) ⊤) ⊤

Tactic:
rfl

Premises used: WithBot.some, Prod.swap, OrderDual, WithBot.map, rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : PartialOrder α
s t : Interval α
⊢ (↑s : Set α) ⊆ (↑t : Set α) ↔ s ≤ t

Tactic:
(@coeHom α _).le_iff_le

Premises used: Interval.coeHom, OrderEmbedding.le_iff_le
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : PartialOrder α
s t : Interval α
⊢ (↑s : Set α) ⊂ (↑t : Set α) ↔ s < t

Tactic:
(@coeHom α _).lt_iff_lt

Premises used: Interval.coeHom, OrderEmbedding.lt_iff_lt
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a : α
⊢ (↑(pure a) : Set α) = {a}

Tactic:
Icc_self _

Premises used: Set.Icc_self, setOf, Set.Icc
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : PartialOrder α
s : NonemptyInterval α
⊢ (↑(↑s : Interval α) : Set α) = (↑s : Set α)

Tactic:
rfl

Premises used: setOf, Set.Icc, rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : PartialOrder α
⊢ (↑⊥ : Set α) = ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
⊢ (↑⊤ : Set α) = univ

Tactic:
Icc_bot_top

Premises used: setOf, Set.Icc_bot_top, Set.Icc
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : PartialOrder α
⊢ (↑((dual : (a : Interval α) → Interval αᵒᵈ) ⊥) : Set αᵒᵈ) = (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (↑⊥ : Set α)

Tactic:
rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : PartialOrder α
s₀ : NonemptyInterval α
⊢ (↑((dual : (a : Interval α) → Interval αᵒᵈ) (↑s₀ : Interval α) : Interval αᵒᵈ) : Set αᵒᵈ) =
    (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (↑(↑s₀ : Interval α) : Set α)

Tactic:
NonemptyInterval.coe_dual s₀

Premises used: NonemptyInterval.coe_dual, setOf, Set.Icc
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : PartialOrder α
s₀ : NonemptyInterval α
⊢ (↑((dual : (a : Interval α) → Interval αᵒᵈ) (↑s₀ : Interval α) : Interval αᵒᵈ) : Set αᵒᵈ) =
    (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (↑(↑s₀ : Interval α) : Set α)

Tactic:
exact NonemptyInterval.coe_dual s₀

Premises used: NonemptyInterval.coe_dual
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : PartialOrder α
s : Interval α
bot : (↑((dual : (a : Interval α) → Interval αᵒᵈ) ⊥) : Set αᵒᵈ) = (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (↑⊥ : Set α)
coe :
  ∀ (s₀ : NonemptyInterval α),
    (↑((dual : (a : Interval α) → Interval αᵒᵈ) (↑s₀ : Interval α) : Interval αᵒᵈ) : Set αᵒᵈ) =
      (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (↑(↑s₀ : Interval α) : Set α)
⊢ (↑((dual : (a : Interval α) → Interval αᵒᵈ) s : Interval αᵒᵈ) : Set αᵒᵈ) = (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (↑s : Set α)

Tactic:
cases s with
  | bot => rfl
  | coe s₀ => exact NonemptyInterval.coe_dual s₀

Premises used: Interval.coe
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f : α →o β
⊢ (⇑f : (a : α) → β) '' (↑⊥ : Set α) ⊆ (↑(map f ⊥) : Set β)

Tactic:
simp
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
rw : b ∈ (↑(pure a) : Set α) ↔ b = a
rw₁ : Membership.mem (γ := Set α) {a} b ↔ b = a
rw₂ rw₃ : b = a ↔ b = a
⊢ Membership.mem (γ := Interval α) (pure a) b ↔ b = a

Tactic:
rw [← SetLike.mem_coe, coe_pure, mem_singleton_iff]

Premises used: Set.mem_singleton_iff, SetLike.mem_coe, Interval.coe_pure
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
inst : PartialOrder α
a : α
⊢ Membership.mem (γ := Interval α) (pure a) a

Tactic:
mem_pure.2 rfl

Premises used: Iff.mpr, Interval.mem_pure, rfl
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 : Interval α
s t : NonemptyInterval α
pos :
  ∀ (h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2),
    (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ : NonemptyInterval α } :
        Interval α) ≤
      some s
neg : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2) → ⊥ ≤ some s
⊢ (if h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2 then
      (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ } : Interval α)
    else ⊥) ≤
    some s

Tactic:
split_ifs
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 : Interval α
s t : NonemptyInterval α
h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2
⊢ (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ : NonemptyInterval α } :
      Interval α) ≤
    some s

Tactic:
WithBot.coe_le_coe.2 ⟨le_sup_left, inf_le_left⟩

Premises used: Iff.mpr, WithBot.some, le_sup_left, WithBot.coe_le_coe, Interval.coe, And.intro, inf_le_left
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 : Interval α
s t : NonemptyInterval α
h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2
⊢ (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ : NonemptyInterval α } :
      Interval α) ≤
    some s

Tactic:
exact WithBot.coe_le_coe.2 ⟨le_sup_left, inf_le_left⟩
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 : Interval α
s t : NonemptyInterval α
h : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2)
⊢ ⊥ ≤ some s

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 : Interval α
s t : NonemptyInterval α
h : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2)
⊢ ⊥ ≤ some s

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 : Interval α
s t : NonemptyInterval α
pos :
  ∀ (h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2),
    (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ : NonemptyInterval α } :
        Interval α) ≤
      some t
neg : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2) → ⊥ ≤ some t
⊢ (if h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2 then
      (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ } : Interval α)
    else ⊥) ≤
    some t

Tactic:
split_ifs
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 : Interval α
s t : NonemptyInterval α
h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2
⊢ (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ : NonemptyInterval α } :
      Interval α) ≤
    some t

Tactic:
WithBot.coe_le_coe.2 ⟨le_sup_right, inf_le_right⟩

Premises used: Iff.mpr, WithBot.some, inf_le_right, le_sup_right, WithBot.coe_le_coe, Interval.coe, And.intro
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 : Interval α
s t : NonemptyInterval α
h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2
⊢ (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ : NonemptyInterval α } :
      Interval α) ≤
    some t

Tactic:
exact WithBot.coe_le_coe.2 ⟨le_sup_right, inf_le_right⟩
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 : Interval α
s t : NonemptyInterval α
h : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2)
⊢ ⊥ ≤ some t

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 : Interval α
s t : NonemptyInterval α
h : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2)
⊢ ⊥ ≤ some t

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s : NonemptyInterval α
t c : Interval α
hb : (↑s : Interval α) ≤ t
hc : (↑s : Interval α) ≤ c
⊢ t ≠ ⊥

Tactic:
ne_bot_of_le_ne_bot WithBot.coe_ne_bot hb

Premises used: ne_bot_of_le_ne_bot, WithBot.coe_ne_bot
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s : NonemptyInterval α
t c : Interval α
hb : (↑s : Interval α) ≤ t
hc : (↑s : Interval α) ≤ c
lift :
  ∀ (t : NonemptyInterval α) (hb : (↑s : Interval α) ≤ (↑t : Interval α)),
    (↑s : Interval α) ≤
      match (motive := Interval α → Interval α → Interval α) (↑t : Interval α), c with
      | none, x => ⊥
      | x, none => ⊥
      | some s, some t =>
        if h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2 then
          (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ } : Interval α)
        else ⊥
⊢ (↑s : Interval α) ≤
    match (motive := Interval α → Interval α → Interval α) t, c with
    | none, x => ⊥
    | x, none => ⊥
    | some s, some t =>
      if h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2 then
        (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ } : Interval α)
      else ⊥

Tactic:
lift t to NonemptyInterval α using ne_bot_of_le_ne_bot WithBot.coe_ne_bot hb

Premises used: ne_bot_of_le_ne_bot, NonemptyInterval
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s : NonemptyInterval α
c : Interval α
hc : (↑s : Interval α) ≤ c
t : NonemptyInterval α
hb : (↑s : Interval α) ≤ (↑t : Interval α)
⊢ c ≠ ⊥

Tactic:
ne_bot_of_le_ne_bot WithBot.coe_ne_bot hc

Premises used: ne_bot_of_le_ne_bot, WithBot.coe_ne_bot
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s : NonemptyInterval α
c : Interval α
hc : (↑s : Interval α) ≤ c
t : NonemptyInterval α
hb : (↑s : Interval α) ≤ (↑t : Interval α)
lift :
  ∀ (c : NonemptyInterval α) (hc : (↑s : Interval α) ≤ (↑c : Interval α)),
    (↑s : Interval α) ≤
      match (motive := Interval α → Interval α → Interval α) (↑t : Interval α), (↑c : Interval α) with
      | none, x => ⊥
      | x, none => ⊥
      | some s, some t =>
        if h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2 then
          (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ } : Interval α)
        else ⊥
⊢ (↑s : Interval α) ≤
    match (motive := Interval α → Interval α → Interval α) (↑t : Interval α), c with
    | none, x => ⊥
    | x, none => ⊥
    | some s, some t =>
      if h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2 then
        (↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ } : Interval α)
      else ⊥

Tactic:
lift c to NonemptyInterval α using ne_bot_of_le_ne_bot WithBot.coe_ne_bot hc

Premises used: ne_bot_of_le_ne_bot, NonemptyInterval
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s t : NonemptyInterval α
hb : (↑s : Interval α) ≤ (↑t : Interval α)
c : NonemptyInterval α
hc : (↑s : Interval α) ≤ (↑c : Interval α)
⊢ s ≤ t

Tactic:
simp only [Interval.coe_le_coe] at hb hc ⊢

Premises used: Interval.coe_le_coe
-- Module: Mathlib.Order.Interval.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : Lattice α
inst_1 : DecidableLE α
s_1 t_1 c_1 : Interval α
s t : NonemptyInterval α
hb : (↑s : Interval α) ≤ (↑t : Interval α)
c : NonemptyInterval α
hc : (↑s : Interval α) ≤ (↑c : Interval α)
hb₁ : s ≤ t
⊢ s ≤ c

Tactic:
simp only [Interval.coe_le_coe] at hb hc ⊢

Premises used: Interval.coe_le_coe