awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → LinearOrder (α i)
i : ι
a b : α i
inr :
  ∀ (hab : a ≤ b),
    mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) i b ∨
      mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a
inr₁ :
  ∀ (hba : b ≤ a),
    mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) i b ∨
      mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a
⊢ mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) i b ∨
    mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a

Tactic:
obtain hab | hba := le_total a b

Premises used: le_total
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → LinearOrder (α i)
i : ι
a b : α i
hab : a ≤ b
⊢ mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) i b ∨
    mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a

Tactic:
Or.inl (Lex.right _ hab)

Premises used: PSigma.Lex.right, Or.inl
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → LinearOrder (α i)
i : ι
a b : α i
hab : a ≤ b
⊢ mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) i b ∨
    mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a

Tactic:
exact Or.inl (Lex.right _ hab)

Premises used: PSigma.Lex.right, Or.inl
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → LinearOrder (α i)
i : ι
a b : α i
hba : b ≤ a
⊢ mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) i b ∨
    mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a

Tactic:
Or.inr (Lex.right _ hba)

Premises used: PSigma.Lex.right, Or.inr
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → LinearOrder (α i)
i : ι
a b : α i
hba : b ≤ a
⊢ mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) i b ∨
    mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a

Tactic:
exact Or.inr (Lex.right _ hba)

Premises used: PSigma.Lex.right, Or.inr
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → LinearOrder (α i)
i : ι
a : α i
j : ι
b : α j
hji : j < i
⊢ mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) j b ∨
    mk (β := fun (i : ι) ↦ α i) j b ≤ mk (β := fun (i : ι) ↦ α i) i a

Tactic:
Or.inr (Lex.left _ _ hji)

Premises used: PSigma.Lex.left, Or.inr
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → LinearOrder (α i)
i : ι
a : α i
j : ι
b : α j
hji : j < i
⊢ mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) j b ∨
    mk (β := fun (i : ι) ↦ α i) j b ≤ mk (β := fun (i : ι) ↦ α i) i a

Tactic:
exact Or.inr (Lex.left _ _ hji)

Premises used: PSigma.Lex.left, Or.inr
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : OrderBot ι
inst_2 : (i : ι) → Preorder (α i)
inst_3 : OrderBot (α ⊥)
x : Σₗ' (i : ι), α i
a : ι
b : α a
inl : ∀ (b : α ⊥), mk (β := fun (i : ι) ↦ α i) ⊥ ⊥ ≤ mk (β := fun (i : ι) ↦ α i) ⊥ b
inr : ∀ (ha : ⊥ < a), mk (β := fun (i : ι) ↦ α i) ⊥ ⊥ ≤ mk (β := fun (i : ι) ↦ α i) a b
⊢ mk (β := fun (i : ι) ↦ α i) ⊥ ⊥ ≤ mk (β := fun (i : ι) ↦ α i) a b

Tactic:
obtain rfl | ha := eq_bot_or_bot_lt a

Premises used: eq_bot_or_bot_lt, rfl
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : OrderBot ι
inst_2 : (i : ι) → Preorder (α i)
inst_3 : OrderBot (α ⊥)
x : Σₗ' (i : ι), α i
b : α ⊥
⊢ mk (β := fun (i : ι) ↦ α i) ⊥ ⊥ ≤ mk (β := fun (i : ι) ↦ α i) ⊥ b

Tactic:
Lex.right _ bot_le

Premises used: PSigma.Lex.right, bot_le
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : OrderBot ι
inst_2 : (i : ι) → Preorder (α i)
inst_3 : OrderBot (α ⊥)
x : Σₗ' (i : ι), α i
b : α ⊥
⊢ mk (β := fun (i : ι) ↦ α i) ⊥ ⊥ ≤ mk (β := fun (i : ι) ↦ α i) ⊥ b

Tactic:
exact Lex.right _ bot_le

Premises used: PSigma.Lex.right
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : OrderBot ι
inst_2 : (i : ι) → Preorder (α i)
inst_3 : OrderBot (α ⊥)
x : Σₗ' (i : ι), α i
a : ι
b : α a
ha : ⊥ < a
⊢ mk (β := fun (i : ι) ↦ α i) ⊥ ⊥ ≤ mk (β := fun (i : ι) ↦ α i) a b

Tactic:
Lex.left _ _ ha

Premises used: PSigma.Lex.left
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : OrderBot ι
inst_2 : (i : ι) → Preorder (α i)
inst_3 : OrderBot (α ⊥)
x : Σₗ' (i : ι), α i
a : ι
b : α a
ha : ⊥ < a
⊢ mk (β := fun (i : ι) ↦ α i) ⊥ ⊥ ≤ mk (β := fun (i : ι) ↦ α i) a b

Tactic:
exact Lex.left _ _ ha

Premises used: PSigma.Lex.left
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : OrderTop ι
inst_2 : (i : ι) → Preorder (α i)
inst_3 : OrderTop (α ⊤)
x : Σₗ' (i : ι), α i
a : ι
b : α a
inl : ∀ (b : α ⊤), mk (β := fun (i : ι) ↦ α i) ⊤ b ≤ mk (β := fun (i : ι) ↦ α i) ⊤ ⊤
inr : ∀ (ha : a < ⊤), mk (β := fun (i : ι) ↦ α i) a b ≤ mk (β := fun (i : ι) ↦ α i) ⊤ ⊤
⊢ mk (β := fun (i : ι) ↦ α i) a b ≤ mk (β := fun (i : ι) ↦ α i) ⊤ ⊤

Tactic:
obtain rfl | ha := eq_top_or_lt_top a

Premises used: eq_top_or_lt_top, rfl
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : OrderTop ι
inst_2 : (i : ι) → Preorder (α i)
inst_3 : OrderTop (α ⊤)
x : Σₗ' (i : ι), α i
b : α ⊤
⊢ mk (β := fun (i : ι) ↦ α i) ⊤ b ≤ mk (β := fun (i : ι) ↦ α i) ⊤ ⊤

Tactic:
Lex.right _ le_top

Premises used: PSigma.Lex.right, le_top
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : OrderTop ι
inst_2 : (i : ι) → Preorder (α i)
inst_3 : OrderTop (α ⊤)
x : Σₗ' (i : ι), α i
b : α ⊤
⊢ mk (β := fun (i : ι) ↦ α i) ⊤ b ≤ mk (β := fun (i : ι) ↦ α i) ⊤ ⊤

Tactic:
exact Lex.right _ le_top

Premises used: PSigma.Lex.right
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : OrderTop ι
inst_2 : (i : ι) → Preorder (α i)
inst_3 : OrderTop (α ⊤)
x : Σₗ' (i : ι), α i
a : ι
b : α a
ha : a < ⊤
⊢ mk (β := fun (i : ι) ↦ α i) a b ≤ mk (β := fun (i : ι) ↦ α i) ⊤ ⊤

Tactic:
Lex.left _ _ ha

Premises used: PSigma.Lex.left
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : OrderTop ι
inst_2 : (i : ι) → Preorder (α i)
inst_3 : OrderTop (α ⊤)
x : Σₗ' (i : ι), α i
a : ι
b : α a
ha : a < ⊤
⊢ mk (β := fun (i : ι) ↦ α i) a b ≤ mk (β := fun (i : ι) ↦ α i) ⊤ ⊤

Tactic:
exact Lex.left _ _ ha

Premises used: PSigma.Lex.left
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : DenselyOrdered ι
inst_2 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
inst_3 : (i : ι) → Preorder (α i)
inst_4 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
left :
  ∀ (k : ι) (hi : i < k) (hj : k < j),
    ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b

Tactic:
obtain ⟨k, hi, hj⟩ := exists_between h

Premises used: exists_between
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : DenselyOrdered ι
inst_2 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
inst_3 : (i : ι) → Preorder (α i)
inst_4 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
k : ι
hi : i < k
hj : k < j
⊢ Nonempty.{u_2 + 1} (α k)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : DenselyOrdered ι
inst_2 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
inst_3 : (i : ι) → Preorder (α i)
inst_4 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
k : ι
hi : i < k
hj : k < j
left :
  ∀ (c : α k), ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b

Tactic:
obtain ⟨c⟩ : Nonempty (α k) := inferInstance

Premises used: Nonempty
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : DenselyOrdered ι
inst_2 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
inst_3 : (i : ι) → Preorder (α i)
inst_4 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
k : ι
hi : i < k
hj : k < j
c : α k
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b

Tactic:
⟨⟨k, c⟩, left _ _ hi, left _ _ hj⟩

Premises used: PSigma.Lex.left, And.intro, Exists.intro, PSigma.mk
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : DenselyOrdered ι
inst_2 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
inst_3 : (i : ι) → Preorder (α i)
inst_4 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
k : ι
hi : i < k
hj : k < j
c : α k
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b

Tactic:
exact ⟨⟨k, c⟩, left _ _ hi, left _ _ hj⟩
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : DenselyOrdered ι
inst_2 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
inst_3 : (i : ι) → Preorder (α i)
inst_4 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
i : ι
a b : α i
h : a < b
right :
  ∀ (c : α i) (ha : a < c) (hb : c < b),
    ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b

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

Premises used: exists_between
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : DenselyOrdered ι
inst_2 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
inst_3 : (i : ι) → Preorder (α i)
inst_4 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
i : ι
a b : α i
h : a < b
c : α i
ha : a < c
hb : c < b
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b

Tactic:
⟨⟨i, c⟩, right _ ha, right _ hb⟩

Premises used: PSigma.Lex.right, And.intro, Exists.intro, PSigma.mk
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : DenselyOrdered ι
inst_2 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
inst_3 : (i : ι) → Preorder (α i)
inst_4 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
i : ι
a b : α i
h : a < b
c : α i
ha : a < c
hb : c < b
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b

Tactic:
exact ⟨⟨i, c⟩, right _ ha, right _ hb⟩
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
inst_3 : ∀ (i : ι), NoMaxOrder.{u_2} (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
left :
  ∀ (c : α i) (ha : a < c),
    ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b

Tactic:
obtain ⟨c, ha⟩ := exists_gt a

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
inst_3 : ∀ (i : ι), NoMaxOrder.{u_2} (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
c : α i
ha : a < c
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b

Tactic:
⟨⟨i, c⟩, right _ ha, left _ _ h⟩

Premises used: PSigma.Lex.left, PSigma.Lex.right, And.intro, Exists.intro, PSigma.mk
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
inst_3 : ∀ (i : ι), NoMaxOrder.{u_2} (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
c : α i
ha : a < c
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b

Tactic:
exact ⟨⟨i, c⟩, right _ ha, left _ _ h⟩
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
inst_3 : ∀ (i : ι), NoMaxOrder.{u_2} (α i)
i : ι
a b : α i
h : a < b
right :
  ∀ (c : α i) (ha : a < c) (hb : c < b),
    ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b

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

Premises used: exists_between
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
inst_3 : ∀ (i : ι), NoMaxOrder.{u_2} (α i)
i : ι
a b : α i
h : a < b
c : α i
ha : a < c
hb : c < b
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b

Tactic:
⟨⟨i, c⟩, right _ ha, right _ hb⟩

Premises used: PSigma.Lex.right, And.intro, Exists.intro, PSigma.mk
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
inst_3 : ∀ (i : ι), NoMaxOrder.{u_2} (α i)
i : ι
a b : α i
h : a < b
c : α i
ha : a < c
hb : c < b
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b

Tactic:
exact ⟨⟨i, c⟩, right _ ha, right _ hb⟩
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
inst_3 : ∀ (i : ι), NoMinOrder.{u_2} (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
left :
  ∀ (c : α j) (hb : c < b),
    ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b

Tactic:
obtain ⟨c, hb⟩ := exists_lt b

Premises used: NoMinOrder.exists_lt
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
inst_3 : ∀ (i : ι), NoMinOrder.{u_2} (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
c : α j
hb : c < b
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b

Tactic:
⟨⟨j, c⟩, left _ _ h, right _ hb⟩

Premises used: PSigma.Lex.left, PSigma.Lex.right, And.intro, Exists.intro, PSigma.mk
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
inst_3 : ∀ (i : ι), NoMinOrder.{u_2} (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
c : α j
hb : c < b
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b

Tactic:
exact ⟨⟨j, c⟩, left _ _ h, right _ hb⟩
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
inst_3 : ∀ (i : ι), NoMinOrder.{u_2} (α i)
i : ι
a b : α i
h : a < b
right :
  ∀ (c : α i) (ha : a < c) (hb : c < b),
    ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b

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

Premises used: exists_between
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
inst_3 : ∀ (i : ι), NoMinOrder.{u_2} (α i)
i : ι
a b : α i
h : a < b
c : α i
ha : a < c
hb : c < b
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b

Tactic:
⟨⟨i, c⟩, right _ ha, right _ hb⟩

Premises used: PSigma.Lex.right, And.intro, Exists.intro, PSigma.mk
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
inst_3 : ∀ (i : ι), NoMinOrder.{u_2} (α i)
i : ι
a b : α i
h : a < b
c : α i
ha : a < c
hb : c < b
⊢ ∃ (a_1 : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b

Tactic:
exact ⟨⟨i, c⟩, right _ ha, right _ hb⟩
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : NoMaxOrder ι
inst_3 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
i : ι
a : α i
obtain : ∀ (j : ι) (h : i < j), ∃ (b : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < b
⊢ ∃ (b : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < b

Tactic:
obtain ⟨j, h⟩ := exists_gt i

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : NoMaxOrder ι
inst_3 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
i : ι
a : α i
j : ι
h : i < j
⊢ Nonempty.{u_2 + 1} (α j)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : NoMaxOrder ι
inst_3 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
i : ι
a : α i
j : ι
h : i < j
obtain : ∀ (b : α j), ∃ (b : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < b
⊢ ∃ (b : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < b

Tactic:
obtain ⟨b⟩ : Nonempty (α j) := inferInstance

Premises used: Nonempty
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : NoMaxOrder ι
inst_3 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
i : ι
a : α i
j : ι
h : i < j
b : α j
⊢ ∃ (b : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < b

Tactic:
⟨⟨j, b⟩, left _ _ h⟩

Premises used: PSigma.Lex.left, Exists.intro, PSigma.mk
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : NoMaxOrder ι
inst_3 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
i : ι
a : α i
j : ι
h : i < j
b : α j
⊢ ∃ (b : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < b

Tactic:
exact ⟨⟨j, b⟩, left _ _ h⟩
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : NoMinOrder ι
inst_3 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
i : ι
a : α i
obtain : ∀ (j : ι) (h : j < i), ∃ (b : Σₗ' (i : ι), α i), b < mk (β := fun (i : ι) ↦ α i) i a
⊢ ∃ (b : Σₗ' (i : ι), α i), b < mk (β := fun (i : ι) ↦ α i) i a

Tactic:
obtain ⟨j, h⟩ := exists_lt i

Premises used: NoMinOrder.exists_lt
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : NoMinOrder ι
inst_3 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
i : ι
a : α i
j : ι
h : j < i
⊢ Nonempty.{u_2 + 1} (α j)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : NoMinOrder ι
inst_3 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
i : ι
a : α i
j : ι
h : j < i
obtain : ∀ (b : α j), ∃ (b : Σₗ' (i : ι), α i), b < mk (β := fun (i : ι) ↦ α i) i a
⊢ ∃ (b : Σₗ' (i : ι), α i), b < mk (β := fun (i : ι) ↦ α i) i a

Tactic:
obtain ⟨b⟩ : Nonempty (α j) := inferInstance

Premises used: Nonempty
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : NoMinOrder ι
inst_3 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
i : ι
a : α i
j : ι
h : j < i
b : α j
⊢ ∃ (b : Σₗ' (i : ι), α i), b < mk (β := fun (i : ι) ↦ α i) i a

Tactic:
⟨⟨j, b⟩, left _ _ h⟩

Premises used: PSigma.Lex.left, Exists.intro, PSigma.mk
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : NoMinOrder ι
inst_3 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
i : ι
a : α i
j : ι
h : j < i
b : α j
⊢ ∃ (b : Σₗ' (i : ι), α i), b < mk (β := fun (i : ι) ↦ α i) i a

Tactic:
exact ⟨⟨j, b⟩, left _ _ h⟩
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), NoMaxOrder.{u_2} (α i)
i : ι
a : α i
obtain : ∀ (b : α i) (h : a < b), ∃ (b : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < b
⊢ ∃ (b : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < b

Tactic:
obtain ⟨b, h⟩ := exists_gt a

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), NoMaxOrder.{u_2} (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ (b : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < b

Tactic:
⟨⟨i, b⟩, right _ h⟩

Premises used: PSigma.Lex.right, Exists.intro, PSigma.mk
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), NoMaxOrder.{u_2} (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ (b : Σₗ' (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < b

Tactic:
exact ⟨⟨i, b⟩, right _ h⟩
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), NoMinOrder.{u_2} (α i)
i : ι
a : α i
obtain : ∀ (b : α i) (h : b < a), ∃ (b : Σₗ' (i : ι), α i), b < mk (β := fun (i : ι) ↦ α i) i a
⊢ ∃ (b : Σₗ' (i : ι), α i), b < mk (β := fun (i : ι) ↦ α i) i a

Tactic:
obtain ⟨b, h⟩ := exists_lt a

Premises used: NoMinOrder.exists_lt
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), NoMinOrder.{u_2} (α i)
i : ι
a b : α i
h : b < a
⊢ ∃ (b : Σₗ' (i : ι), α i), b < mk (β := fun (i : ι) ↦ α i) i a

Tactic:
⟨⟨i, b⟩, right _ h⟩

Premises used: PSigma.Lex.right, Exists.intro, PSigma.mk
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), NoMinOrder.{u_2} (α i)
i : ι
a b : α i
h : b < a
⊢ ∃ (b : Σₗ' (i : ι), α i), b < mk (β := fun (i : ι) ↦ α i) i a

Tactic:
exact ⟨⟨i, b⟩, right _ h⟩
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
pos : ∀ (h : o.Dom), o.toOption.isSome = true ↔ o.Dom
neg : ∀ (h : ¬o.Dom), o.toOption.isSome = true ↔ o.Dom
⊢ o.toOption.isSome = true ↔ o.Dom

Tactic:
by_cases h : o.Dom

Premises used: Part.Dom
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
h : o.Dom
⊢ o.toOption.isSome = true ↔ o.Dom

Tactic:
simp [h, toOption]

Premises used: Part.toOption
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
h : ¬o.Dom
⊢ o.toOption.isSome = true ↔ o.Dom

Tactic:
simp [h, toOption]

Premises used: Part.toOption
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
pos : ∀ (h : o.Dom), o.toOption = none ↔ ¬o.Dom
neg : ∀ (h : ¬o.Dom), o.toOption = none ↔ ¬o.Dom
⊢ o.toOption = none ↔ ¬o.Dom

Tactic:
by_cases h : o.Dom

Premises used: Part.Dom
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
h : o.Dom
⊢ o.toOption = none ↔ ¬o.Dom

Tactic:
simp [h, toOption]

Premises used: Part.toOption
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
h : ¬o.Dom
⊢ o.toOption = none ↔ ¬o.Dom

Tactic:
simp [h, toOption]

Premises used: Part.toOption