awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Sigma.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.Sigma.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: Sigma.Lex.right, le_top
-- Module: Mathlib.Data.Sigma.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: Sigma.Lex.right
-- Module: Mathlib.Data.Sigma.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: Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.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: Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.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.Sigma.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.Sigma.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.Sigma.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: And.intro, Exists.intro, Sigma.mk, Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.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.Sigma.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.Sigma.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: Sigma.Lex.right, And.intro, Exists.intro, Sigma.mk
-- Module: Mathlib.Data.Sigma.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.Sigma.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.Sigma.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: Sigma.Lex.right, And.intro, Exists.intro, Sigma.mk, Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.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.Sigma.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.Sigma.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: Sigma.Lex.right, And.intro, Exists.intro, Sigma.mk
-- Module: Mathlib.Data.Sigma.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.Sigma.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.Sigma.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: Sigma.Lex.right, And.intro, Exists.intro, Sigma.mk, Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.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.Sigma.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.Sigma.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: Sigma.Lex.right, And.intro, Exists.intro, Sigma.mk
-- Module: Mathlib.Data.Sigma.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.Sigma.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.Sigma.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.Sigma.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.Sigma.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: Exists.intro, Sigma.mk, Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.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.Sigma.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.Sigma.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.Sigma.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.Sigma.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: Exists.intro, Sigma.mk, Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.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.Sigma.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.Sigma.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: Sigma.Lex.right, Exists.intro, Sigma.mk
-- Module: Mathlib.Data.Sigma.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.Sigma.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.Sigma.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: Sigma.Lex.right, Exists.intro, Sigma.mk
-- Module: Mathlib.Data.Sigma.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.Sign.Basic
Goal:
α : Type u_1
inst : AddGroupWithOne α
s : SignType
⊢ Eq.{u_1 + 1} (α := α) (↑(↑s : ℤ) : α) (↑s : α)

Tactic:
map_cast' _ Int.cast_one Int.cast_zero (@Int.cast_one α _ ▸ Int.cast_neg 1) _

Premises used: Int.cast_zero, SignType.map_cast', Int.cast_one
-- Module: Mathlib.Data.Sign.Basic
Goal:
s : SignType
n : ℕ
hn : Odd n
obtain : ∀ (k : ℕ), s ^ (2 * k + 1) = s
⊢ s ^ n = s

Tactic:
obtain ⟨k, rfl⟩ := hn

Premises used: rfl
-- Module: Mathlib.Data.Sign.Basic
Goal:
s : SignType
k : ℕ
rw : (s * s) ^ k * s = s
⊢ s ^ (2 * k + 1) = s

Tactic:
rw [pow_add, pow_one, pow_mul, sq]

Premises used: pow_add, sq, pow_mul, pow_one
-- Module: Mathlib.Data.Sign.Basic
Goal:
s : SignType
k : ℕ
zero : (SignType.zero * SignType.zero) ^ k * SignType.zero = SignType.zero
neg : (SignType.neg * SignType.neg) ^ k * SignType.neg = SignType.neg
pos : (SignType.pos * SignType.pos) ^ k * SignType.pos = SignType.pos
⊢ (s * s) ^ k * s = s

Tactic:
cases s
-- Module: Mathlib.Data.Sign.Basic
Goal:
k : ℕ
⊢ (zero * zero) ^ k * zero = zero

Tactic:
simp
-- Module: Mathlib.Data.Sign.Basic
Goal:
k : ℕ
⊢ (neg * neg) ^ k * neg = neg

Tactic:
simp
-- Module: Mathlib.Data.Sign.Basic
Goal:
k : ℕ
⊢ (pos * pos) ^ k * pos = pos

Tactic:
simp
-- Module: Mathlib.Data.Sign.Basic
Goal:
s : SignType
z : ℤ
hz : Odd z
inl : HPow.hPow (α := SignType) 0 z = 0
inr : ∀ (hs : s ≠ 0), s ^ z = s
⊢ s ^ z = s

Tactic:
obtain rfl | hs := eq_or_ne s 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Sign.Basic
Goal:
z : ℤ
hz : Odd z
inl : z ≠ 0
⊢ HPow.hPow (α := SignType) 0 z = 0

Tactic:
rw [zero_zpow]

Premises used: zero_zpow
-- Module: Mathlib.Data.Sign.Basic
Goal:
hz : Odd (α := ℤ) 0
⊢ False

Tactic:
simp at hz
-- Module: Mathlib.Data.Sign.Basic
Goal:
s : SignType
z : ℤ
hz : Odd z
hs : s ≠ 0
inr : ∀ (k : ℤ), s ^ (2 * k + 1) = s
⊢ s ^ z = s

Tactic:
obtain ⟨k, rfl⟩ := hz

Premises used: rfl
-- Module: Mathlib.Data.Sign.Basic
Goal:
s : SignType
hs : s ≠ 0
k : ℤ
inr : (s * s) ^ k * s = s
⊢ s ^ (2 * k + 1) = s

Tactic:
rw [zpow_add₀ hs, zpow_one, zpow_mul, zpow_two]

Premises used: zpow_mul, zpow_one, zpow_add₀, zpow_two
-- Module: Mathlib.Data.Sign.Basic
Goal:
s : SignType
hs : s ≠ 0
k : ℤ
inr : ∀ (hs : zero ≠ 0), (zero * zero) ^ k * zero = zero
inr₁ : ∀ (hs : neg ≠ 0), (neg * neg) ^ k * neg = neg
inr₂ : ∀ (hs : pos ≠ 0), (pos * pos) ^ k * pos = pos
⊢ (s * s) ^ k * s = s

Tactic:
cases s
-- Module: Mathlib.Data.Sign.Basic
Goal:
k : ℤ
hs : zero ≠ 0
⊢ (zero * zero) ^ k * zero = zero

Tactic:
simp
-- Module: Mathlib.Data.Sign.Basic
Goal:
k : ℤ
hs : neg ≠ 0
⊢ (neg * neg) ^ k * neg = neg

Tactic:
simp
-- Module: Mathlib.Data.Sign.Basic
Goal:
k : ℤ
hs : pos ≠ 0
⊢ (pos * pos) ^ k * pos = pos

Tactic:
simp
-- Module: Mathlib.Data.Sign.Basic
Goal:
s : SignType
n : ℕ
hn : Even n
hs : s ≠ 0
zero : ∀ (hs : SignType.zero ≠ 0), SignType.zero ^ n = 1
neg : ∀ (hs : SignType.neg ≠ 0), SignType.neg ^ n = 1
pos : ∀ (hs : SignType.pos ≠ 0), SignType.pos ^ n = 1
⊢ s ^ n = 1

Tactic:
cases s
-- Module: Mathlib.Data.Sign.Basic
Goal:
n : ℕ
hn : Even n
hs : zero ≠ 0
⊢ zero ^ n = 1

Tactic:
simp_all
-- Module: Mathlib.Data.Sign.Basic
Goal:
n : ℕ
hn : Even n
hs : neg ≠ 0
⊢ neg ^ n = 1

Tactic:
simp_all
-- Module: Mathlib.Data.Sign.Basic
Goal:
n : ℕ
hn : Even n
hs : pos ≠ 0
⊢ pos ^ n = 1

Tactic:
simp_all
-- Module: Mathlib.Data.Sign.Basic
Goal:
s : SignType
z : ℤ
hz : Even z
hs : s ≠ 0
zero : ∀ (hs : SignType.zero ≠ 0), SignType.zero ^ z = 1
neg : ∀ (hs : SignType.neg ≠ 0), SignType.neg ^ z = 1
pos : ∀ (hs : SignType.pos ≠ 0), SignType.pos ^ z = 1
⊢ s ^ z = 1

Tactic:
cases s
-- Module: Mathlib.Data.Sign.Basic
Goal:
z : ℤ
hz : Even z
hs : zero ≠ 0
⊢ zero ^ z = 1

Tactic:
simp_all [Even.neg_one_zpow]

Premises used: Even.neg_one_zpow
-- Module: Mathlib.Data.Sign.Basic
Goal:
z : ℤ
hz : Even z
hs : neg ≠ 0
⊢ neg ^ z = 1

Tactic:
simp_all [Even.neg_one_zpow]

Premises used: Even.neg_one_zpow
-- Module: Mathlib.Data.Sign.Basic
Goal:
z : ℤ
hz : Even z
hs : pos ≠ 0
⊢ pos ^ z = 1

Tactic:
simp_all [Even.neg_one_zpow]

Premises used: Even.neg_one_zpow
-- Module: Mathlib.Data.Sign.Basic
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
x y : SignType
zero : (↑(SignType.zero * y) : α) = HMul.hMul (α := α) (↑SignType.zero : α) (↑y : α)
neg : (↑(SignType.neg * y) : α) = HMul.hMul (α := α) (↑SignType.neg : α) (↑y : α)
pos : (↑(SignType.pos * y) : α) = HMul.hMul (α := α) (↑SignType.pos : α) (↑y : α)
⊢ (↑(x * y) : α) = HMul.hMul (α := α) (↑x : α) (↑y : α)

Tactic:
cases x
-- Module: Mathlib.Data.Sign.Basic
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
y : SignType
zero : (↑(SignType.zero * SignType.zero) : α) = HMul.hMul (α := α) (↑SignType.zero : α) (↑SignType.zero : α)
zero₁ : (↑(SignType.zero * neg) : α) = HMul.hMul (α := α) (↑SignType.zero : α) (↑neg : α)
zero₂ : (↑(SignType.zero * pos) : α) = HMul.hMul (α := α) (↑SignType.zero : α) (↑pos : α)
⊢ (↑(SignType.zero * y) : α) = HMul.hMul (α := α) (↑SignType.zero : α) (↑y : α)

Tactic:
cases y
-- Module: Mathlib.Data.Sign.Basic
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
y : SignType
neg : (↑(SignType.neg * zero) : α) = HMul.hMul (α := α) (↑SignType.neg : α) (↑zero : α)
neg₁ : (↑(SignType.neg * SignType.neg) : α) = HMul.hMul (α := α) (↑SignType.neg : α) (↑SignType.neg : α)
neg₂ : (↑(SignType.neg * pos) : α) = HMul.hMul (α := α) (↑SignType.neg : α) (↑pos : α)
⊢ (↑(SignType.neg * y) : α) = HMul.hMul (α := α) (↑SignType.neg : α) (↑y : α)

Tactic:
cases y
-- Module: Mathlib.Data.Sign.Basic
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
y : SignType
pos : (↑(SignType.pos * zero) : α) = HMul.hMul (α := α) (↑SignType.pos : α) (↑zero : α)
pos₁ : (↑(SignType.pos * neg) : α) = HMul.hMul (α := α) (↑SignType.pos : α) (↑neg : α)
pos₂ : (↑(SignType.pos * SignType.pos) : α) = HMul.hMul (α := α) (↑SignType.pos : α) (↑SignType.pos : α)
⊢ (↑(SignType.pos * y) : α) = HMul.hMul (α := α) (↑SignType.pos : α) (↑y : α)

Tactic:
cases y
-- Module: Mathlib.Data.Sign.Basic
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
⊢ (↑(zero * zero) : α) = HMul.hMul (α := α) (↑zero : α) (↑zero : α)

Tactic:
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]

Premises used: SignType.neg_eq_neg_one, SignType.zero_eq_zero, SignType.pos_eq_one