awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
a₁ a₂ : α
b₁ b₂ : β
⊢ (a₁, b₁) ≤ (a₂, b₂) ↔ a₁ ≤ a₂ ∧ b₁ ≤ b₂

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ (a₁, b₁) ≤ (a₂, b₂)

Tactic:
⟨ha, hb⟩

Premises used: And.intro
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
x y : α × β
⊢ x.swap ≤ y.swap ↔ x ≤ y

Tactic:
and_comm

Premises used: and_comm
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
x : α × β
a : α
b : β
⊢ x.swap ≤ (b, a) ↔ x ≤ (a, b)

Tactic:
and_comm

Premises used: and_comm
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
x y : α × β
⊢ x.swap < y.swap ↔ x < y

Tactic:
and_congr swap_le_swap (not_congr swap_le_swap)

Premises used: Prod.swap_le_swap, not_congr, and_congr
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
a : α
b : β
x : α × β
rw : x.swap.swap < (b, a).swap ↔ x < (a, b)
⊢ x.swap < (b, a) ↔ x < (a, b)

Tactic:
rw [← swap_lt_swap]

Premises used: Prod.swap_lt_swap
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
a : α
b : β
x : α × β
⊢ x.swap.swap < (b, a).swap ↔ x < (a, b)

Tactic:
simp
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
a₁ a₂ : α
b : β
⊢ (a₁, b) ≤ (a₂, b) ↔ a₁ ≤ a₂

Tactic:
and_iff_left le_rfl

Premises used: le_rfl, and_iff_left
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
a : α
b₁ b₂ : β
⊢ (a, b₁) ≤ (a, b₂) ↔ b₁ ≤ b₂

Tactic:
and_iff_right le_rfl

Premises used: le_rfl, and_iff_right
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
a₁ a₂ : α
b : β
⊢ (a₁, b) < (a₂, b) ↔ a₁ < a₂

Tactic:
lt_iff_lt_of_le_iff_le' mk_le_mk_iff_left mk_le_mk_iff_left

Premises used: lt_iff_lt_of_le_iff_le', Prod.mk_le_mk_iff_left
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
a : α
b₁ b₂ : β
⊢ (a, b₁) < (a, b₂) ↔ b₁ < b₂

Tactic:
lt_iff_lt_of_le_iff_le' mk_le_mk_iff_right mk_le_mk_iff_right

Premises used: lt_iff_lt_of_le_iff_le', Prod.mk_le_mk_iff_right
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
x y : α × β
⊢ x < y ↔ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

Tactic:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
x y : α × β
refine_1 : ∀ (h : x < y), x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
refine_2 : x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd → x < y
⊢ x < y ↔ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
x y : α × β
h : x < y
pos : ∀ (h₁ : y.fst ≤ x.fst), x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
neg : ∀ (h₁ : ¬y.fst ≤ x.fst), x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

Tactic:
by_cases h₁ : y.1 ≤ x.1

Premises used: Prod.fst
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
x y : α × β
h : x < y
h₁ : y.fst ≤ x.fst
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

Tactic:
Or.inr ⟨h.1.1, LE.le.lt_of_not_ge h.1.2 fun h₂ ↦ h.2 ⟨h₁, h₂⟩⟩

Premises used: LE.le.lt_of_not_ge, And.right, And.left, And.intro, Or.inr
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
x y : α × β
h : x < y
h₁ : y.fst ≤ x.fst
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

Tactic:
exact Or.inr ⟨h.1.1, LE.le.lt_of_not_ge h.1.2 fun h₂ ↦ h.2 ⟨h₁, h₂⟩⟩

Premises used: Or.inr
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
x y : α × β
h : x < y
h₁ : ¬y.fst ≤ x.fst
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

Tactic:
Or.inl ⟨LE.le.lt_of_not_ge h.1.1 h₁, h.1.2⟩

Premises used: LE.le.lt_of_not_ge, And.right, And.left, And.intro, Or.inl
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
x y : α × β
h : x < y
h₁ : ¬y.fst ≤ x.fst
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

Tactic:
exact Or.inl ⟨LE.le.lt_of_not_ge h.1.1 h₁, h.1.2⟩

Premises used: Or.inl
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
x y : α × β
h₁ : x.fst < y.fst
h₂ : x.snd ≤ y.snd
⊢ x < y

Tactic:
⟨⟨h₁.le, h₂⟩, fun h ↦ h₁.not_ge h.1⟩

Premises used: LT.lt.le, And.left, And.intro, LT.lt.not_ge
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
x y : α × β
h₁ : x.fst < y.fst
h₂ : x.snd ≤ y.snd
⊢ x < y

Tactic:
exact ⟨⟨h₁.le, h₂⟩, fun h ↦ h₁.not_ge h.1⟩
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
x y : α × β
h₁ : x.fst ≤ y.fst
h₂ : x.snd < y.snd
⊢ x < y

Tactic:
⟨⟨h₁, h₂.le⟩, fun h ↦ h₂.not_ge h.2⟩

Premises used: LT.lt.le, And.right, And.intro, LT.lt.not_ge
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
x y : α × β
h₁ : x.fst ≤ y.fst
h₂ : x.snd < y.snd
⊢ x < y

Tactic:
exact ⟨⟨h₁, h₂.le⟩, fun h ↦ h₂.not_ge h.2⟩
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
a₁ a₂ : α
b₁ b₂ : β
⊢ (a₁, b₁) < (a₂, b₂) ↔ a₁ < a₂ ∧ b₁ ≤ b₂ ∨ a₁ ≤ a₂ ∧ b₁ < b₂

Tactic:
lt_iff

Premises used: Prod.lt_iff
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
x y : α × β
h₁ : x.fst < y.fst
h₂ : x.snd ≤ y.snd
⊢ x < y

Tactic:
simp [lt_iff, *]

Premises used: Prod.lt_iff
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
x y : α × β
h₁ : x.fst ≤ y.fst
h₂ : x.snd < y.snd
⊢ x < y

Tactic:
simp [lt_iff, *]

Premises used: Prod.lt_iff
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
a₁ a₂ : α
b₁ b₂ : β
h₁ : a₁ < a₂
h₂ : b₁ ≤ b₂
⊢ (a₁, b₁) < (a₂, b₂)

Tactic:
simp [lt_iff, *]

Premises used: Prod.lt_iff
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
a₁ a₂ : α
b₁ b₂ : β
h₁ : a₁ ≤ a₂
h₂ : b₁ < b₂
⊢ (a₁, b₁) < (a₂, b₂)

Tactic:
simp [lt_iff, *]

Premises used: Prod.lt_iff
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LT α
inst_1 : DenselyOrdered α
simp_rw : ∀ (a₁ a₂ : α), a₁ < a₂ → ∃ (a : α), a₁ < a ∧ a < a₂
⊢ ∀ (a₁ a₂ : α), a₁ < a₂ → ∃ (a : α), a < a₂ ∧ a₁ < a

Tactic:
simp_rw [and_comm]

Premises used: and_comm
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LT α
inst_1 : DenselyOrdered α
⊢ ∀ (a₁ a₂ : α), a₁ < a₂ → ∃ (a : α), a₁ < a ∧ a < a₂

Tactic:
dense

Premises used: DenselyOrdered.dense
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LT α
inst_1 : DenselyOrdered α
⊢ ∀ (a₁ a₂ : α), a₁ < a₂ → ∃ (a : α), a₁ < a ∧ a < a₂

Tactic:
exact dense

Premises used: DenselyOrdered.dense
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LT α
inst_1 : DenselyOrdered α
a₁ a₂ : α
⊢ a₁ < a₂ → ∃ (a : α), a₁ < a ∧ a < a₂

Tactic:
DenselyOrdered.dense _ _

Premises used: DenselyOrdered.dense
-- Module: Mathlib.Order.Basic
Goal:
X : Type u_5
inst : Subsingleton X
inst_1 : LT X
⊢ DenselyOrdered X

Tactic:
⟨fun _ _ h ↦ ⟨_, h.trans_eq (Subsingleton.elim _ _), h⟩⟩

Premises used: LT.lt.trans_eq, DenselyOrdered.mk, And.intro, Exists.intro, Subsingleton.elim
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : DenselyOrdered α
inst_3 : DenselyOrdered β
a b : α × β
simp_rw :
  a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
    ∃ (a_2 : α × β),
      (a.fst < a_2.fst ∧ a.snd ≤ a_2.snd ∨ a.fst ≤ a_2.fst ∧ a.snd < a_2.snd) ∧
        (a_2.fst < b.fst ∧ a_2.snd ≤ b.snd ∨ a_2.fst ≤ b.fst ∧ a_2.snd < b.snd)
⊢ a < b → ∃ (a_2 : α × β), a < a_2 ∧ a_2 < b

Tactic:
simp_rw [Prod.lt_iff]

Premises used: Prod.lt_iff
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : DenselyOrdered α
inst_3 : DenselyOrdered β
a b : α × β
h₁ : a.fst < b.fst
h₂ : a.snd ≤ b.snd
inl :
  ∀ (c : α) (ha : a.fst < c) (hb : c < b.fst),
    ∃ (a_1 : α × β),
      (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
        (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)
⊢ ∃ (a_1 : α × β),
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)

Tactic:
obtain ⟨c, ha, hb⟩ := exists_between h₁

Premises used: exists_between
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : DenselyOrdered α
inst_3 : DenselyOrdered β
a b : α × β
h₁ : a.fst < b.fst
h₂ : a.snd ≤ b.snd
c : α
ha : a.fst < c
hb : c < b.fst
⊢ ∃ (a_1 : α × β),
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)

Tactic:
⟨(c, _), Or.inl ⟨ha, h₂⟩, Or.inl ⟨hb, le_rfl⟩⟩

Premises used: le_rfl, Prod.mk, And.intro, Exists.intro, Or.inl
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : DenselyOrdered α
inst_3 : DenselyOrdered β
a b : α × β
h₁ : a.fst < b.fst
h₂ : a.snd ≤ b.snd
c : α
ha : a.fst < c
hb : c < b.fst
⊢ ∃ (a_1 : α × β),
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)

Tactic:
exact ⟨(c, _), Or.inl ⟨ha, h₂⟩, Or.inl ⟨hb, le_rfl⟩⟩
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : DenselyOrdered α
inst_3 : DenselyOrdered β
a b : α × β
h₁ : a.fst ≤ b.fst
h₂ : a.snd < b.snd
inr :
  ∀ (c : β) (ha : a.snd < c) (hb : c < b.snd),
    ∃ (a_1 : α × β),
      (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
        (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)
⊢ ∃ (a_1 : α × β),
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)

Tactic:
obtain ⟨c, ha, hb⟩ := exists_between h₂

Premises used: exists_between
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : DenselyOrdered α
inst_3 : DenselyOrdered β
a b : α × β
h₁ : a.fst ≤ b.fst
h₂ : a.snd < b.snd
c : β
ha : a.snd < c
hb : c < b.snd
⊢ ∃ (a_1 : α × β),
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)

Tactic:
⟨(_, c), Or.inr ⟨h₁, ha⟩, Or.inr ⟨le_rfl, hb⟩⟩

Premises used: le_rfl, Prod.mk, And.intro, Exists.intro, Or.inr
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : DenselyOrdered α
inst_3 : DenselyOrdered β
a b : α × β
h₁ : a.fst ≤ b.fst
h₂ : a.snd < b.snd
c : β
ha : a.snd < c
hb : c < b.snd
⊢ ∃ (a_1 : α × β),
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)

Tactic:
exact ⟨(_, c), Or.inr ⟨h₁, ha⟩, Or.inr ⟨le_rfl, hb⟩⟩
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : (i : ι) → Preorder (π i)
inst_1 : ∀ (i : ι), DenselyOrdered.{u_4} (π i)
a b : (i : ι) → π i
simp_rw :
  (a ≤ b ∧ ∃ (i : ι), a i < b i) →
    ∃ (a_2 : (i : ι) → π i), (a ≤ a_2 ∧ ∃ (i : ι), a i < a_2 i) ∧ a_2 ≤ b ∧ ∃ (i : ι), a_2 i < b i
⊢ a < b → ∃ (a_2 : (i : ι) → π i), a < a_2 ∧ a_2 < b

Tactic:
simp_rw [Pi.lt_def]

Premises used: Pi.lt_def
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : (i : ι) → Preorder (π i)
inst_1 : ∀ (i : ι), DenselyOrdered.{u_4} (π i)
a b : (i : ι) → π i
hab : a ≤ b
i : ι
hi : a i < b i
obtain :
  ∀ (c : π i) (ha : a i < c) (hb : c < b i),
    ∃ (a_1 : (i : ι) → π i), (a ≤ a_1 ∧ ∃ (i : ι), a i < a_1 i) ∧ a_1 ≤ b ∧ ∃ (i : ι), a_1 i < b i
⊢ ∃ (a_1 : (i : ι) → π i), (a ≤ a_1 ∧ ∃ (i : ι), a i < a_1 i) ∧ a_1 ≤ b ∧ ∃ (i : ι), a_1 i < b i

Tactic:
obtain ⟨c, ha, hb⟩ := exists_between hi

Premises used: exists_between
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : (i : ι) → Preorder (π i)
inst_1 : ∀ (i : ι), DenselyOrdered.{u_4} (π i)
a b : (i : ι) → π i
hab : a ≤ b
i : ι
hi : a i < b i
c : π i
ha : a i < c
hb : c < b i
rwa rwa₁ rwa₂ rwa₃ : a i < c
⊢ a i < update (β := π) a i c i

Tactic:
rwa [update_self]

Premises used: Function.update_self
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : (i : ι) → Preorder (π i)
inst_1 : ∀ (i : ι), DenselyOrdered.{u_4} (π i)
a b : (i : ι) → π i
hab : a ≤ b
i : ι
hi : a i < b i
c : π i
ha : a i < c
hb rwa rwa₁ rwa₂ rwa₃ : c < b i
⊢ update (β := π) a i c i < b i

Tactic:
rwa [update_self]

Premises used: Function.update_self
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : (i : ι) → Preorder (π i)
inst_1 : ∀ (i : ι), DenselyOrdered.{u_4} (π i)
a b : (i : ι) → π i
hab : a ≤ b
i : ι
hi : a i < b i
c : π i
ha : a i < c
hb : c < b i
⊢ ∃ (a_1 : (i : ι) → π i), (a ≤ a_1 ∧ ∃ (i : ι), a i < a_1 i) ∧ a_1 ≤ b ∧ ∃ (i : ι), a_1 i < b i

Tactic:
exact
        ⟨Function.update a i c,
          ⟨le_update_iff.2 ⟨ha.le, fun _ _ ↦ le_rfl⟩, i, by rwa [update_self]⟩,
          update_le_iff.2 ⟨hb.le, fun _ _ ↦ hab _⟩, i, by rwa [update_self]⟩
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : (i : ι) → Preorder (π i)
inst_1 : ∀ (i : ι), DenselyOrdered.{u_4} (π i)
a b : (i : ι) → π i
simp_rw :
  (a ≤ b ∧ ∃ (i : ι), a i < b i) →
    ∃ (a_2 : (i : ι) → π i), (a ≤ a_2 ∧ ∃ (i : ι), a i < a_2 i) ∧ a_2 ≤ b ∧ ∃ (i : ι), a_2 i < b i
simp_rw₁ :
  ∀ (hab : a ≤ b) (i : ι) (hi : a i < b i),
    ∃ (a_1 : (i : ι) → π i), (a ≤ a_1 ∧ ∃ (i : ι), a i < a_1 i) ∧ a_1 ≤ b ∧ ∃ (i : ι), a_1 i < b i
simp_rw₂ :
  ∀ (hab : a ≤ b) (i : ι) (hi : a i < b i) (c : π i) (ha : a i < c) (hb : c < b i),
    ∃ (a_1 : (i : ι) → π i), (a ≤ a_1 ∧ ∃ (i : ι), a i < a_1 i) ∧ a_1 ≤ b ∧ ∃ (i : ι), a_1 i < b i
⊢ a < b → ∃ (a_2 : (i : ι) → π i), a < a_2 ∧ a_2 < b

Tactic:
classical
      simp_rw [Pi.lt_def]
      rintro ⟨hab, i, hi⟩
      obtain ⟨c, ha, hb⟩ := exists_between hi
      exact
        ⟨Function.update a i c,
          ⟨le_update_iff.2 ⟨ha.le, fun _ _ ↦ le_rfl⟩, i, by rwa [update_self]⟩,
          update_le_iff.2 ⟨hb.le, fun _ _ ↦ hab _⟩, i, by rwa [update_self]⟩

Premises used: Pi.lt_def
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : DenselyOrdered α
a₁ a₂ : α
h : ∀ (a : α), a₂ < a → a₁ ≤ a
⊢ a₁ ≤ a₂

Tactic:
le_of_not_gt fun ha ↦
    let ⟨a, ha₁, ha₂⟩ := exists_between ha
    lt_irrefl a <| lt_of_lt_of_le ‹a < a₁› (h _ ‹a₂ < a›)

Premises used: False, lt_irrefl, _private.0.le_of_forall_gt_imp_ge_of_dense.match_1, le_of_not_gt, exists_between, lt_of_lt_of_le
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : DenselyOrdered α
a₁ a₂ : α
⊢ (∀ (a : α), a₂ < a → a₁ ≤ a) ↔ a₁ ≤ a₂

Tactic:
⟨le_of_forall_gt_imp_ge_of_dense, fun ha _a ha₂ ↦ ha.trans ha₂.le⟩

Premises used: LT.lt.le, Iff.intro, le_of_forall_gt_imp_ge_of_dense, LE.le.trans
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : DenselyOrdered α
a₁ a₂ : α
h₁ : a₂ ≤ a₁
h₂ : ∀ (a : α), a₂ < a → a₁ ≤ a
⊢ a₁ = a₂

Tactic:
le_antisymm (le_of_forall_gt_imp_ge_of_dense h₂) h₁

Premises used: le_antisymm, le_of_forall_gt_imp_ge_of_dense
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a₁ a₂ : α
⊢ (∃ (a : α), a₁ < a ∧ a < a₂) ∨ (∀ (a : α), a₁ < a → a₂ ≤ a) ∧ ∀ (a : α), a < a₂ → a ≤ a₁

Tactic:
or_iff_not_imp_left.2 fun h ↦
    ⟨fun a ha₁ ↦ le_of_not_gt fun ha₂ ↦ h ⟨a, ha₁, ha₂⟩,
     fun a ha₂ ↦ le_of_not_gt fun ha₁ ↦ h ⟨a, ha₁, ha₂⟩⟩

Premises used: Iff.mpr, le_of_not_gt, Classical.or_iff_not_imp_left, And.intro, Exists.intro
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
by_contra : ∀ (hne : ¬(x = y ∨ y = z ∨ x = z)), False
⊢ x = y ∨ y = z ∨ x = z

Tactic:
by_contra hne
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : ¬(x = y ∨ y = z ∨ x = z)
⊢ x ≠ y ∧ y ≠ z ∧ x ≠ z

Tactic:
simp only [not_or, ← Ne.eq_def] at hne

Premises used: Ne.eq_def, not_or
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
inl : ∀ (h₁ : x < y), False
inr : ∀ (h₁ : y < x), False
⊢ False

Tactic:
rcases hne.1.lt_or_gt with h₁ | h₁

Premises used: And.left, Ne.lt_or_gt
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
inl : ∀ (h₂ : y < z), False
inl₁ : ∀ (h₂ : z < y), False
⊢ False

Tactic:
rcases hne.2.1.lt_or_gt with h₂ | h₂

Premises used: And.right, And.left, Ne.lt_or_gt
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
inr : ∀ (h₂ : y < z), False
inr₁ : ∀ (h₂ : z < y), False
⊢ False

Tactic:
rcases hne.2.1.lt_or_gt with h₂ | h₂

Premises used: And.right, And.left, Ne.lt_or_gt
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : y < z
inl : ∀ (h₃ : x < z), False
inl₁ : ∀ (h₃ : z < x), False
⊢ False

Tactic:
rcases hne.2.2.lt_or_gt with h₃ | h₃

Premises used: And.right, Ne.lt_or_gt
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : z < y
inl : ∀ (h₃ : x < z), False
inl₁ : ∀ (h₃ : z < x), False
⊢ False

Tactic:
rcases hne.2.2.lt_or_gt with h₃ | h₃

Premises used: And.right, Ne.lt_or_gt
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : y < z
inr : ∀ (h₃ : x < z), False
inr₁ : ∀ (h₃ : z < x), False
⊢ False

Tactic:
rcases hne.2.2.lt_or_gt with h₃ | h₃

Premises used: And.right, Ne.lt_or_gt
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : z < y
inr : ∀ (h₃ : x < z), False
inr₁ : ∀ (h₃ : z < x), False
⊢ False

Tactic:
rcases hne.2.2.lt_or_gt with h₃ | h₃

Premises used: And.right, Ne.lt_or_gt
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : y < z
h₃ : x < z
⊢ False

Tactic:
h h₁ h₂
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : y < z
h₃ : z < x
⊢ False

Tactic:
h h₂ h₃
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : z < y
h₃ : x < z
⊢ False

Tactic:
h h₃ h₂
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : z < y
h₃ : z < x
⊢ False

Tactic:
h h₃ h₁
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : y < z
h₃ : x < z
⊢ False

Tactic:
h h₁ h₃
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : y < z
h₃ : z < x
⊢ False

Tactic:
h h₂ h₃
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : z < y
h₃ : x < z
⊢ False

Tactic:
h h₁ h₃
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : z < y
h₃ : z < x
⊢ False

Tactic:
h h₂ h₁
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : y < z
h₃ : x < z
⊢ False

Tactic:
exacts [h h₁ h₂, h h₂ h₃, h h₃ h₂, h h₃ h₁, h h₁ h₃, h h₂ h₃, h h₁ h₃, h h₂ h₁]
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
β : Type u_3
π : ι → Type u_4
α : Type u_5
inst : Subsingleton α
x x_1 : α
⊢ False ↔ True ∧ ¬True

Tactic:
simp
-- Module: Mathlib.Order.Basic
Goal:
a b : PUnit
⊢ max a b = unit

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Order.Basic
Goal:
a b : PUnit
⊢ a ≤ b

Tactic:
trivial

Premises used: trivial
-- Module: Mathlib.Order.Basic
Goal:
a b : PUnit
⊢ ¬a < b

Tactic:
not_false

Premises used: not_false
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
a : PUnit
b : PUnit
⊢ DenselyOrdered PUnit

Tactic:
⟨fun _ _ ↦ False.elim⟩

Premises used: False.elim, DenselyOrdered.mk
-- Module: Mathlib.Order.Basic
Goal:
⊢ Eq (α := Prop → Prop → Prop) (fun (x1 x2 : Prop) ↦ x1 ≤ x2) fun (x1 x2 : Prop) ↦ x1 → x2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
r s : α → α → Prop
⊢ Subrelation r s ↔ r ≤ s

Tactic:
Iff.rfl

Premises used: Iff.rfl, Subrelation
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
a : α
⊢ InfIrred (α := UpperSet α) (Ici a)

Tactic:
⟨fun h ↦ Ici_ne_top h.eq_top, fun s t hst ↦ ?_⟩

Premises used: UpperSet.Ici_ne_top, InfIrred, IsMax.eq_top, And.intro
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
a : α
refine : ∀ (s t : UpperSet α) (hst : s ⊓ t = Ici a), s = Ici a ∨ t = Ici a
⊢ InfIrred (α := UpperSet α) (Ici a)

Tactic:
refine ⟨fun h ↦ Ici_ne_top h.eq_top, fun s t hst ↦ ?_⟩
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
a : α
s t : UpperSet α
hst : s ⊓ t = Ici a
⊢ Membership.mem (γ := UpperSet α) (Ici a) a

Tactic:
have := mem_Ici_iff.2 (le_refl a)
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
a : α
s t : UpperSet α
hst : s ⊓ t = Ici a
this : Membership.mem (γ := UpperSet α) (Ici a) a
⊢ a ∈ s ⊓ t

Tactic:
rw [← hst] at this
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
a : α
s t : UpperSet α
hst : s ⊓ t = Ici a
this : a ∈ s ⊓ t
⊢ s = Ici a ∨ t = Ici a

Tactic:
this.imp (fun ha ↦ le_antisymm (le_Ici.2 ha) <| hst.ge.trans inf_le_left) fun ha ↦
      le_antisymm (le_Ici.2 ha) <| hst.ge.trans inf_le_right

Premises used: Iff.mpr, Eq.ge, inf_le_right, UpperSet.le_Ici, le_antisymm, inf_le_left, LE.le.trans, Or.imp
-- Module: Mathlib.Order.Birkhoff
Goal:
α : Type u_1
inst : PartialOrder α
a : α
s t : UpperSet α
hst : s ⊓ t = Ici a
this : a ∈ s ⊓ t
⊢ s = Ici a ∨ t = Ici a

Tactic:
exact this.imp (fun ha ↦ le_antisymm (le_Ici.2 ha) <| hst.ge.trans inf_le_left) fun ha ↦
      le_antisymm (le_Ici.2 ha) <| hst.ge.trans inf_le_right

Premises used: Iff.mpr, Eq.ge, inf_le_right, UpperSet.le_Ici, le_antisymm, inf_le_left, LE.le.trans, Or.imp