awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Sort u_1
α : ι → Sort u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
a₁ : ι
a : α a₁
a₂ : ι
b : α a₂
hij : r₁ a₁ a₂
⊢ Lex (β := α) r₂ s₂ (mk (β := α) a₁ a) (mk (β := α) a₂ b)

Tactic:
exact Lex.left _ _ (hr _ _ hij)

Premises used: PSigma.Lex.left
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Sort u_1
α : ι → Sort u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
i : ι
b₁ b₂ : α i
hab : s₁ i b₁ b₂
⊢ Lex (β := α) r₂ s₂ (mk (β := α) i b₁) (mk (β := α) i b₂)

Tactic:
Lex.right _ (hs _ _ _ hab)

Premises used: PSigma.Lex.right
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Sort u_1
α : ι → Sort u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
i : ι
b₁ b₂ : α i
hab : s₁ i b₁ b₂
⊢ Lex (β := α) r₂ s₂ (mk (β := α) i b₁) (mk (β := α) i b₂)

Tactic:
exact Lex.right _ (hs _ _ _ hab)

Premises used: PSigma.Lex.right
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Sort u_1
α : ι → Sort u_2
r₁ r₂ : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
a b : (i : ι) ×' α i
h : Lex (β := α) r₁ s a b
⊢ Lex (β := α) r₂ s a b

Tactic:
h.mono hr fun _ _ _ => id

Premises used: PSigma.Lex.mono, id
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
a b : (i : ι) ×' α i
h : Lex (β := α) r s₁ a b
⊢ Lex (β := α) r s₂ a b

Tactic:
h.mono (fun _ _ => id) hs

Premises used: PSigma.Lex.mono, id
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → LE (α i)
i : ι
a b : α i
⊢ mk (β := α) i a ≤ mk (β := α) i b ↔ a ≤ b

Tactic:
⟨fun ⟨_, _, _, h⟩ => h, Sigma.LE.fiber _ _ _⟩

Premises used: _private.0.Sigma.mk_le_mk_iff.match_1, LE.le, Sigma.LE.fiber, Iff.intro
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → LT (α i)
i : ι
a b : α i
⊢ mk (β := α) i a < mk (β := α) i b ↔ a < b

Tactic:
⟨fun ⟨_, _, _, h⟩ => h, Sigma.LT.fiber _ _ _⟩

Premises used: _private.0.Sigma.mk_lt_mk_iff.match_1, LT.lt, Iff.intro, Sigma.LT.fiber
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → LE (α i)
a b : (i : ι) × α i
mp :
  a ≤ b →
    ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
      Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) (a.snd (β := fun (i : ι) ↦ α i))
          h ≤
        b.snd (β := fun (i : ι) ↦ α i)
mpr :
  (∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
      Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) (a.snd (β := fun (i : ι) ↦ α i))
          h ≤
        b.snd (β := fun (i : ι) ↦ α i)) →
    a ≤ b
⊢ a ≤ b ↔
    ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
      Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) (a.snd (β := fun (i : ι) ↦ α i))
          h ≤
        b.snd (β := fun (i : ι) ↦ α i)

Tactic:
constructor
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → LE (α i)
i : ι
a b : α i
h : a ≤ b
⊢ ∃ (h :
    (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) =
      (mk (β := fun (i : ι) ↦ α i) i b).fst (β := fun (i : ι) ↦ α i)),
    Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
        ((mk (β := fun (i : ι) ↦ α i) i a).snd (β := fun (i : ι) ↦ α i)) h ≤
      (mk (β := fun (i : ι) ↦ α i) i b).snd (β := fun (i : ι) ↦ α i)

Tactic:
⟨rfl, h⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → LE (α i)
i : ι
a b : α i
h : a ≤ b
⊢ ∃ (h :
    (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) =
      (mk (β := fun (i : ι) ↦ α i) i b).fst (β := fun (i : ι) ↦ α i)),
    Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
        ((mk (β := fun (i : ι) ↦ α i) i a).snd (β := fun (i : ι) ↦ α i)) h ≤
      (mk (β := fun (i : ι) ↦ α i) i b).snd (β := fun (i : ι) ↦ α i)

Tactic:
exact ⟨rfl, h⟩
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → LE (α i)
a b : (i : ι) × α i
mpr :
  ∀ (i : ι) (a : α i),
    (∃ (h : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
        Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            ((mk (β := fun (i : ι) ↦ α i) i a).snd (β := fun (i : ι) ↦ α i)) h ≤
          b.snd (β := fun (i : ι) ↦ α i)) →
      mk (β := fun (i : ι) ↦ α i) i a ≤ b
⊢ (∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
      Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) (a.snd (β := fun (i : ι) ↦ α i))
          h ≤
        b.snd (β := fun (i : ι) ↦ α i)) →
    a ≤ b

Tactic:
obtain ⟨i, a⟩ := a
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → LE (α i)
b : (i : ι) × α i
i : ι
a : α i
mpr :
  ∀ (j : ι) (b : α j),
    (∃ (h :
        (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) =
          (mk (β := fun (i : ι) ↦ α i) j b).fst (β := fun (i : ι) ↦ α i)),
        Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            ((mk (β := fun (i : ι) ↦ α i) i a).snd (β := fun (i : ι) ↦ α i)) h ≤
          (mk (β := fun (i : ι) ↦ α i) j b).snd (β := fun (i : ι) ↦ α i)) →
      mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) j b
⊢ (∃ (h : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
      Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
          ((mk (β := fun (i : ι) ↦ α i) i a).snd (β := fun (i : ι) ↦ α i)) h ≤
        b.snd (β := fun (i : ι) ↦ α i)) →
    mk (β := fun (i : ι) ↦ α i) i a ≤ b

Tactic:
obtain ⟨j, b⟩ := b
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → LE (α i)
i : ι
a b : α i
h :
  Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
      ((mk (β := fun (i : ι) ↦ α i) i a).snd (β := fun (i : ι) ↦ α i)) ⋯ ≤
    (mk (β := fun (i : ι) ↦ α i) i b).snd (β := fun (i : ι) ↦ α i)
⊢ mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) i b

Tactic:
LE.fiber _ _ _ h

Premises used: Sigma.LE.fiber
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → LE (α i)
i : ι
a b : α i
h :
  Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
      ((mk (β := fun (i : ι) ↦ α i) i a).snd (β := fun (i : ι) ↦ α i)) ⋯ ≤
    (mk (β := fun (i : ι) ↦ α i) i b).snd (β := fun (i : ι) ↦ α i)
⊢ mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) i b

Tactic:
exact LE.fiber _ _ _ h

Premises used: Sigma.LE.fiber
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → LT (α i)
a b : (i : ι) × α i
mp :
  a < b →
    ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
      Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) (a.snd (β := fun (i : ι) ↦ α i))
          h <
        b.snd (β := fun (i : ι) ↦ α i)
mpr :
  (∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
      Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) (a.snd (β := fun (i : ι) ↦ α i))
          h <
        b.snd (β := fun (i : ι) ↦ α i)) →
    a < b
⊢ a < b ↔
    ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
      Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) (a.snd (β := fun (i : ι) ↦ α i))
          h <
        b.snd (β := fun (i : ι) ↦ α i)

Tactic:
constructor
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → LT (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ (h :
    (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) =
      (mk (β := fun (i : ι) ↦ α i) i b).fst (β := fun (i : ι) ↦ α i)),
    Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
        ((mk (β := fun (i : ι) ↦ α i) i a).snd (β := fun (i : ι) ↦ α i)) h <
      (mk (β := fun (i : ι) ↦ α i) i b).snd (β := fun (i : ι) ↦ α i)

Tactic:
⟨rfl, h⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → LT (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ (h :
    (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) =
      (mk (β := fun (i : ι) ↦ α i) i b).fst (β := fun (i : ι) ↦ α i)),
    Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
        ((mk (β := fun (i : ι) ↦ α i) i a).snd (β := fun (i : ι) ↦ α i)) h <
      (mk (β := fun (i : ι) ↦ α i) i b).snd (β := fun (i : ι) ↦ α i)

Tactic:
exact ⟨rfl, h⟩
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → LT (α i)
a b : (i : ι) × α i
mpr :
  ∀ (i : ι) (a : α i),
    (∃ (h : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
        Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            ((mk (β := fun (i : ι) ↦ α i) i a).snd (β := fun (i : ι) ↦ α i)) h <
          b.snd (β := fun (i : ι) ↦ α i)) →
      mk (β := fun (i : ι) ↦ α i) i a < b
⊢ (∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
      Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) (a.snd (β := fun (i : ι) ↦ α i))
          h <
        b.snd (β := fun (i : ι) ↦ α i)) →
    a < b

Tactic:
obtain ⟨i, a⟩ := a
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → LT (α i)
b : (i : ι) × α i
i : ι
a : α i
mpr :
  ∀ (j : ι) (b : α j),
    (∃ (h :
        (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) =
          (mk (β := fun (i : ι) ↦ α i) j b).fst (β := fun (i : ι) ↦ α i)),
        Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            ((mk (β := fun (i : ι) ↦ α i) i a).snd (β := fun (i : ι) ↦ α i)) h <
          (mk (β := fun (i : ι) ↦ α i) j b).snd (β := fun (i : ι) ↦ α i)) →
      mk (β := fun (i : ι) ↦ α i) i a < mk (β := fun (i : ι) ↦ α i) j b
⊢ (∃ (h : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
      Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
          ((mk (β := fun (i : ι) ↦ α i) i a).snd (β := fun (i : ι) ↦ α i)) h <
        b.snd (β := fun (i : ι) ↦ α i)) →
    mk (β := fun (i : ι) ↦ α i) i a < b

Tactic:
obtain ⟨j, b⟩ := b
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → LT (α i)
i : ι
a b : α i
h :
  Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
      ((mk (β := fun (i : ι) ↦ α i) i a).snd (β := fun (i : ι) ↦ α i)) ⋯ <
    (mk (β := fun (i : ι) ↦ α i) i b).snd (β := fun (i : ι) ↦ α i)
⊢ mk (β := fun (i : ι) ↦ α i) i a < mk (β := fun (i : ι) ↦ α i) i b

Tactic:
LT.fiber _ _ _ h

Premises used: Sigma.LT.fiber
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → LT (α i)
i : ι
a b : α i
h :
  Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
      ((mk (β := fun (i : ι) ↦ α i) i a).snd (β := fun (i : ι) ↦ α i)) ⋯ <
    (mk (β := fun (i : ι) ↦ α i) i b).snd (β := fun (i : ι) ↦ α i)
⊢ mk (β := fun (i : ι) ↦ α i) i a < mk (β := fun (i : ι) ↦ α i) i b

Tactic:
exact LT.fiber _ _ _ h

Premises used: Sigma.LT.fiber
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
i : ι
a b : α i
hab : a ≤ b
c : α i
hbc : b ≤ c
⊢ mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) i c

Tactic:
LE.fiber i a c (hab.trans hbc)

Premises used: Sigma.LE.fiber, LE.le.trans
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
i : ι
a b : α i
hab : a ≤ b
c : α i
hbc : b ≤ c
⊢ mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) i c

Tactic:
exact LE.fiber i a c (hab.trans hbc)

Premises used: Sigma.LE.fiber, LE.le.trans
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
x x_1 : (i : ι) × α i
mp : x < x_1 → x ≤ x_1 ∧ ¬x_1 ≤ x
mpr : x ≤ x_1 ∧ ¬x_1 ≤ x → x < x_1
⊢ x < x_1 ↔ x ≤ x_1 ∧ ¬x_1 ≤ x

Tactic:
constructor
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
i : ι
a b : α i
hab : a < b
mp : a ≤ b ∧ ¬mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a
mp₁ : a ≤ b ∧ ¬b ≤ a
mp₂ mp₃ mp₄ mp₅ : 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:
rwa [mk_le_mk_iff, mk_le_mk_iff, ← lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge, Sigma.mk_le_mk_iff
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
i : ι
a b : α i
hab : a ≤ b
h : ¬mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a
⊢ ¬b ≤ a

Tactic:
rw [mk_le_mk_iff] at h

Premises used: Sigma.mk_le_mk_iff
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
i : ι
a b : α i
hab : a ≤ b
h : ¬b ≤ a
⊢ mk (β := fun (i : ι) ↦ α i) i a < mk (β := fun (i : ι) ↦ α i) i b

Tactic:
mk_lt_mk_iff.2 (hab.lt_of_not_ge h)

Premises used: Iff.mpr, LE.le.lt_of_not_ge, Sigma.mk_lt_mk_iff
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
i : ι
a b : α i
hab : a ≤ b
h : ¬b ≤ a
⊢ mk (β := fun (i : ι) ↦ α i) i a < mk (β := fun (i : ι) ↦ α i) i b

Tactic:
exact mk_lt_mk_iff.2 (hab.lt_of_not_ge h)

Premises used: Iff.mpr, LE.le.lt_of_not_ge, Sigma.mk_lt_mk_iff
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → PartialOrder (α i)
i : ι
a b : α i
hab : a ≤ b
hba : b ≤ a
⊢ mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i b

Tactic:
congr_arg (Sigma.mk _ ·) <| hab.antisymm hba

Premises used: LE.le.antisymm, congr_arg, Sigma.mk
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → PartialOrder (α i)
i : ι
a b : α i
hab : a ≤ b
hba : b ≤ a
⊢ mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i b

Tactic:
exact congr_arg (Sigma.mk _ ·) <| hab.antisymm hba

Premises used: LE.le.antisymm, congr_arg, Sigma.mk
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
i : ι
a b : α i
h : a < b
obtain :
  ∀ (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 : (i : ι) → Preorder (α i)
inst_1 : ∀ (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⟩, LT.fiber i a c ha, LT.fiber i c b hb⟩

Premises used: And.intro, Exists.intro, Sigma.LT.fiber, Sigma.mk
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : ∀ (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⟩, LT.fiber i a c ha, LT.fiber i c b hb⟩
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LT ι
inst_1 : (i : ι) → LE (α i)
a b : Σₗ (i : ι), α i
⊢ a ≤ b ↔
    a.fst (β := fun (i : ι) ↦ α i) < b.fst (β := fun (i : ι) ↦ α i) ∨
      ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
        Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) (a.snd (β := fun (i : ι) ↦ α i))
            h ≤
          b.snd (β := fun (i : ι) ↦ α i)

Tactic:
Sigma.lex_iff

Premises used: Sigma.lex_iff
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LT ι
inst_1 : (i : ι) → LT (α i)
a b : Σₗ (i : ι), α i
⊢ a < b ↔
    a.fst (β := fun (i : ι) ↦ α i) < b.fst (β := fun (i : ι) ↦ α i) ∨
      ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
        Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) (a.snd (β := fun (i : ι) ↦ α i))
            h <
          b.snd (β := fun (i : ι) ↦ α i)

Tactic:
Sigma.lex_iff

Premises used: Sigma.lex_iff
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
⊢ ∀ (a b : Σₗ (i : ι), α i), a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
fun a b => ⟨fun hab => ⟨hab.mono_right fun i a b => le_of_lt, ?_⟩, ?_⟩

Premises used: le_of_lt, And.intro, Iff.intro, Sigma.Lex.mono_right
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
refine_1 : ∀ (a b : Σₗ (i : ι), α i) (hab : a < b), ¬b ≤ a
refine_2 : ∀ (a b : Σₗ (i : ι), α i), a ≤ b ∧ ¬b ≤ a → a < b
⊢ ∀ (a b : Σₗ (i : ι), α i), a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
refine fun a b => ⟨fun hab => ⟨hab.mono_right fun i a b => le_of_lt, ?_⟩, ?_⟩
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i j : ι
b : α i
a : α j
hji : i < j
hab : mk (β := fun (i : ι) ↦ α i) j a < mk (β := fun (i : ι) ↦ α i) i b
refine_1 : ∀ (hij : j < i), False
refine_1₁ : ∀ (a : α i) (hji : i < i) (hab : a < b), False
⊢ False

Tactic:
obtain ⟨_, _, hij⟩ | ⟨_, _, hab⟩ := hab
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i : ι
b a : α i
hba : b ≤ a
hab : mk (β := fun (i : ι) ↦ α i) i a < mk (β := fun (i : ι) ↦ α i) i b
refine_1 : ∀ (hij : i < i), False
refine_1₁ : ∀ (hab : a < b), False
⊢ False

Tactic:
obtain ⟨_, _, hij⟩ | ⟨_, _, hab⟩ := hab
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i j : ι
b : α i
a : α j
hji : i < j
hij : j < i
⊢ False

Tactic:
hij.not_gt hji

Premises used: LT.lt.not_gt
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i j : ι
b : α i
a : α j
hji : i < j
hij : j < i
⊢ False

Tactic:
exact hij.not_gt hji

Premises used: LT.lt.not_gt
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i : ι
b a : α i
hji : i < i
hab : a < b
⊢ False

Tactic:
lt_irrefl _ hji

Premises used: lt_irrefl
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i : ι
b a : α i
hji : i < i
hab : a < b
⊢ False

Tactic:
exact lt_irrefl _ hji

Premises used: lt_irrefl
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i : ι
b a : α i
hba : b ≤ a
hij : i < i
⊢ False

Tactic:
lt_irrefl _ hij

Premises used: lt_irrefl
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i : ι
b a : α i
hba : b ≤ a
hij : i < i
⊢ False

Tactic:
exact lt_irrefl _ hij

Premises used: lt_irrefl
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i : ι
b a : α i
hba : b ≤ a
hab : a < b
⊢ False

Tactic:
hab.not_ge hba

Premises used: LT.lt.not_ge
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i : ι
b a : α i
hba : b ≤ a
hab : a < b
⊢ False

Tactic:
exact hab.not_ge hba

Premises used: LT.lt.not_ge
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i j : ι
a : α i
b : α j
hij : i < j
hba : ¬mk (β := fun (i : ι) ↦ α i) j b ≤ mk (β := fun (i : ι) ↦ α i) i a
⊢ mk (β := fun (i : ι) ↦ α i) i a < mk (β := fun (i : ι) ↦ α i) j b

Tactic:
Sigma.Lex.left _ _ hij

Premises used: Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i j : ι
a : α i
b : α j
hij : i < j
hba : ¬mk (β := fun (i : ι) ↦ α i) j b ≤ mk (β := fun (i : ι) ↦ α i) i a
⊢ mk (β := fun (i : ι) ↦ α i) i a < mk (β := fun (i : ι) ↦ α i) j b

Tactic:
exact Sigma.Lex.left _ _ hij

Premises used: Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i : ι
a b : α i
hab : a ≤ b
hba : ¬mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a
⊢ mk (β := fun (i : ι) ↦ α i) i a < mk (β := fun (i : ι) ↦ α i) i b

Tactic:
Sigma.Lex.right _ _ (hab.lt_of_not_ge fun h => hba <| Sigma.Lex.right _ _ h)

Premises used: LE.le.lt_of_not_ge, Sigma.Lex.right
-- Module: Mathlib.Data.Sigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i : ι
a b : α i
hab : a ≤ b
hba : ¬mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a
⊢ mk (β := fun (i : ι) ↦ α i) i a < mk (β := fun (i : ι) ↦ α i) i b

Tactic:
exact Sigma.Lex.right _ _ (hab.lt_of_not_ge fun h => hba <| Sigma.Lex.right _ _ h)

Premises used: Sigma.Lex.right
-- Module: Mathlib.Data.Sigma.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.Sigma.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: Sigma.Lex.right, bot_le
-- Module: Mathlib.Data.Sigma.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: Sigma.Lex.right
-- Module: Mathlib.Data.Sigma.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: Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.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: Sigma.Lex.left