awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
mp :
  Lex (α := α) r s a b →
    r (a.fst (β := fun (i : ι) ↦ α i)) (b.fst (β := fun (i : ι) ↦ α i)) ∨
      ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
        s (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 :
  (r (a.fst (β := fun (i : ι) ↦ α i)) (b.fst (β := fun (i : ι) ↦ α i)) ∨
      ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
        s (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))) →
    Lex (α := α) r s a b
⊢ Lex (α := α) r s a b ↔
    r (a.fst (β := fun (i : ι) ↦ α i)) (b.fst (β := fun (i : ι) ↦ α i)) ∨
      ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
        s (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.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i j : ι
a : α i
b : α j
hij : r i j
⊢ r ((mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i))
      ((mk (β := fun (i : ι) ↦ α i) j b).fst (β := fun (i : ι) ↦ α i)) ∨
    ∃ (h :
      (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) =
        (mk (β := fun (i : ι) ↦ α i) j b).fst (β := fun (i : ι) ↦ α i)),
      s ((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))

Tactic:
Or.inl hij

Premises used: Or.inl
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i j : ι
a : α i
b : α j
hij : r i j
⊢ r ((mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i))
      ((mk (β := fun (i : ι) ↦ α i) j b).fst (β := fun (i : ι) ↦ α i)) ∨
    ∃ (h :
      (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) =
        (mk (β := fun (i : ι) ↦ α i) j b).fst (β := fun (i : ι) ↦ α i)),
      s ((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))

Tactic:
exact Or.inl hij

Premises used: Or.inl
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i : ι
a b : α i
hab : s i a b
⊢ r ((mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i))
      ((mk (β := fun (i : ι) ↦ α i) i b).fst (β := fun (i : ι) ↦ α i)) ∨
    ∃ (h :
      (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) =
        (mk (β := fun (i : ι) ↦ α i) i b).fst (β := fun (i : ι) ↦ α i)),
      s ((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:
Or.inr ⟨rfl, hab⟩

Premises used: Exists.intro, Or.inr, rfl
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i : ι
a b : α i
hab : s i a b
⊢ r ((mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i))
      ((mk (β := fun (i : ι) ↦ α i) i b).fst (β := fun (i : ι) ↦ α i)) ∨
    ∃ (h :
      (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) =
        (mk (β := fun (i : ι) ↦ α i) i b).fst (β := fun (i : ι) ↦ α i)),
      s ((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 Or.inr ⟨rfl, hab⟩

Premises used: Or.inr
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
mpr :
  ∀ (i : ι) (a : α i),
    (r ((mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i)) (b.fst (β := fun (i : ι) ↦ α i)) ∨
        ∃ (h : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
          s (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))) →
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) b
⊢ (r (a.fst (β := fun (i : ι) ↦ α i)) (b.fst (β := fun (i : ι) ↦ α i)) ∨
      ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
        s (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))) →
    Lex (α := α) r s a b

Tactic:
obtain ⟨i, a⟩ := a
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
b : (i : ι) × α i
i : ι
a : α i
mpr :
  (r i (b.fst (β := fun (i : ι) ↦ α i)) ∨
      ∃ (h : i = b.fst (β := fun (i : ι) ↦ α i)),
        s (b.fst (β := fun (i : ι) ↦ α i)) (Eq.rec (motive := fun (x : ι) (x_1 : i = x) ↦ α x) a h)
          (b.snd (β := fun (i : ι) ↦ α i))) →
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) b
⊢ (r ((mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i)) (b.fst (β := fun (i : ι) ↦ α i)) ∨
      ∃ (h : (mk (β := fun (i : ι) ↦ α i) i a).fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i)),
        s (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))) →
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) b

Tactic:
dsimp only
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
b : (i : ι) × α i
i : ι
a : α i
h : r i (b.fst (β := fun (i : ι) ↦ α i))
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) b

Tactic:
Lex.left _ _ h

Premises used: Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
b : (i : ι) × α i
i : ι
a : α i
h : r i (b.fst (β := fun (i : ι) ↦ α i))
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) b

Tactic:
exact Lex.left _ _ h

Premises used: Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
b : (i : ι) × α i
a : α (b.fst (β := fun (i : ι) ↦ α i))
h :
  s (b.fst (β := fun (i : ι) ↦ α i))
    (Eq.rec (motive := fun (x : ι) (x_1 : b.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) a ⋯)
    (b.snd (β := fun (i : ι) ↦ α i))
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) (b.fst (β := fun (i : ι) ↦ α i)) a) b

Tactic:
Lex.right _ _ h

Premises used: Sigma.Lex.right
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
b : (i : ι) × α i
a : α (b.fst (β := fun (i : ι) ↦ α i))
h :
  s (b.fst (β := fun (i : ι) ↦ α i))
    (Eq.rec (motive := fun (x : ι) (x_1 : b.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) a ⋯)
    (b.snd (β := fun (i : ι) ↦ α i))
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) (b.fst (β := fun (i : ι) ↦ α i)) a) b

Tactic:
exact Lex.right _ _ h

Premises used: Sigma.Lex.right
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type 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 b : (i : ι) × α i
h : Lex (α := α) r₁ s₁ a b
left :
  ∀ {i j : ι} (a : α i) (b : α j) (hij : r₁ i j),
    Lex (α := α) r₂ s₂ (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b)
right :
  ∀ {i : ι} (a b : α i) (hab : s₁ i a b),
    Lex (α := α) r₂ s₂ (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b)
⊢ Lex (α := α) r₂ s₂ a b

Tactic:
obtain ⟨a, b, hij⟩ | ⟨a, b, hab⟩ := h
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type 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 j : ι
a : α i
b : α j
hij : r₁ i j
⊢ Lex (α := α) r₂ s₂ (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b)

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

Premises used: Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type 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 j : ι
a : α i
b : α j
hij : r₁ i j
⊢ Lex (α := α) r₂ s₂ (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b)

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

Premises used: Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type 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 : ι
a b : α i
hab : s₁ i a b
⊢ Lex (α := α) r₂ s₂ (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b)

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

Premises used: Sigma.Lex.right
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type 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 : ι
a b : α i
hab : s₁ i a b
⊢ Lex (α := α) r₂ s₂ (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b)

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

Premises used: Sigma.Lex.right
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type 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: id, Sigma.Lex.mono
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type 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: id, Sigma.Lex.mono
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
mp :
  Lex (α := α) (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) r) s a b →
    Lex (α := α) r (fun (i : ι) ↦ Function.swap (φ := fun (a a_2 : α i) ↦ Prop) (s i)) b a
mpr :
  Lex (α := α) r (fun (i : ι) ↦ Function.swap (φ := fun (a a_1 : α i) ↦ Prop) (s i)) b a →
    Lex (α := α) (Function.swap (φ := fun (a a_2 : ι) ↦ Prop) r) s a b
⊢ Lex (α := α) (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) r) s a b ↔
    Lex (α := α) r (fun (i : ι) ↦ Function.swap (φ := fun (a a_1 : α i) ↦ Prop) (s i)) b a

Tactic:
constructor
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i j : ι
a : α i
b : α j
h : Function.swap (φ := fun (a a_1 : ι) ↦ Prop) r i j
⊢ Lex (α := α) r (fun (i : ι) ↦ Function.swap (φ := fun (a a_1 : α i) ↦ Prop) (s i)) (mk (β := fun (i : ι) ↦ α i) j b)
    (mk (β := fun (i : ι) ↦ α i) i a)

Tactic:
Lex.left _ _ h

Premises used: Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i j : ι
a : α i
b : α j
h : Function.swap (φ := fun (a a_1 : ι) ↦ Prop) r i j
⊢ Lex (α := α) r (fun (i : ι) ↦ Function.swap (φ := fun (a a_1 : α i) ↦ Prop) (s i)) (mk (β := fun (i : ι) ↦ α i) j b)
    (mk (β := fun (i : ι) ↦ α i) i a)

Tactic:
exact Lex.left _ _ h

Premises used: Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i : ι
a b : α i
h : s i a b
⊢ Lex (α := α) r (fun (i : ι) ↦ Function.swap (φ := fun (a a_1 : α i) ↦ Prop) (s i)) (mk (β := fun (i : ι) ↦ α i) i b)
    (mk (β := fun (i : ι) ↦ α i) i a)

Tactic:
Lex.right _ _ h

Premises used: Sigma.Lex.right
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i : ι
a b : α i
h : s i a b
⊢ Lex (α := α) r (fun (i : ι) ↦ Function.swap (φ := fun (a a_1 : α i) ↦ Prop) (s i)) (mk (β := fun (i : ι) ↦ α i) i b)
    (mk (β := fun (i : ι) ↦ α i) i a)

Tactic:
exact Lex.right _ _ h

Premises used: Sigma.Lex.right
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i j : ι
a : α i
b : α j
h : r i j
⊢ Lex (α := α) (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) r) s (mk (β := fun (i : ι) ↦ α i) j b)
    (mk (β := fun (i : ι) ↦ α i) i a)

Tactic:
Lex.left _ _ h

Premises used: Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i j : ι
a : α i
b : α j
h : r i j
⊢ Lex (α := α) (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) r) s (mk (β := fun (i : ι) ↦ α i) j b)
    (mk (β := fun (i : ι) ↦ α i) i a)

Tactic:
exact Lex.left _ _ h

Premises used: Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i : ι
a b : α i
h : Function.swap (φ := fun (a a_1 : α i) ↦ Prop) (s i) a b
⊢ Lex (α := α) (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) r) s (mk (β := fun (i : ι) ↦ α i) i b)
    (mk (β := fun (i : ι) ↦ α i) i a)

Tactic:
Lex.right _ _ h

Premises used: Sigma.Lex.right
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i : ι
a b : α i
h : Function.swap (φ := fun (a a_1 : α i) ↦ Prop) (s i) a b
⊢ Lex (α := α) (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) r) s (mk (β := fun (i : ι) ↦ α i) i b)
    (mk (β := fun (i : ι) ↦ α i) i a)

Tactic:
exact Lex.right _ _ h

Premises used: Sigma.Lex.right
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
inst : ∀ (i : ι), Std.Refl (s i)
⊢ Std.Refl (Lex (α := α) r s)

Tactic:
⟨fun ⟨_, _⟩ => Lex.right _ _ <| refl _⟩

Premises used: Sigma.Lex, _private.0.Sigma.instReflLex.match_1, Std.Refl.mk, Sigma.Lex.right, refl
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b : (i : ι) × α i
inst : Std.Irrefl r
inst_1 : ∀ (i : ι), Std.Irrefl (s i)
i : ι
a : α i
hi : r i i
⊢ False

Tactic:
irrefl _ hi

Premises used: irrefl
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b : (i : ι) × α i
inst : Std.Irrefl r
inst_1 : ∀ (i : ι), Std.Irrefl (s i)
i : ι
a : α i
hi : r i i
⊢ False

Tactic:
exact irrefl _ hi

Premises used: irrefl
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b : (i : ι) × α i
inst : Std.Irrefl r
inst_1 : ∀ (i : ι), Std.Irrefl (s i)
i : ι
a : α i
ha : s i a a
⊢ False

Tactic:
irrefl _ ha

Premises used: irrefl
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b : (i : ι) × α i
inst : Std.Irrefl r
inst_1 : ∀ (i : ι), Std.Irrefl (s i)
i : ι
a : α i
ha : s i a a
⊢ False

Tactic:
exact irrefl _ ha

Premises used: irrefl
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b_1 : (i : ι) × α i
inst : IsTrans ι r
inst_1 : ∀ (i : ι), IsTrans (α i) (s i)
i j : ι
a : α i
b : α j
hij : r i j
j_1 : ι
c : α j_1
hk : r j j_1
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j_1 c)

Tactic:
Lex.left _ _ (_root_.trans hij hk)

Premises used: trans, Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b_1 : (i : ι) × α i
inst : IsTrans ι r
inst_1 : ∀ (i : ι), IsTrans (α i) (s i)
i j : ι
a : α i
b : α j
hij : r i j
j_1 : ι
c : α j_1
hk : r j j_1
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j_1 c)

Tactic:
exact Lex.left _ _ (_root_.trans hij hk)

Premises used: trans, Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b_1 : (i : ι) × α i
inst : IsTrans ι r
inst_1 : ∀ (i : ι), IsTrans (α i) (s i)
i j : ι
a : α i
b : α j
hij : r i j
c : α j
hc : s j b c
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j c)

Tactic:
Lex.left _ _ hij

Premises used: Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b_1 : (i : ι) × α i
inst : IsTrans ι r
inst_1 : ∀ (i : ι), IsTrans (α i) (s i)
i j : ι
a : α i
b : α j
hij : r i j
c : α j
hc : s j b c
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j c)

Tactic:
exact Lex.left _ _ hij

Premises used: Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b_1 : (i : ι) × α i
inst : IsTrans ι r
inst_1 : ∀ (i : ι), IsTrans (α i) (s i)
i : ι
a b : α i
hab : s i a b
j : ι
c : α j
hk : r i j
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j c)

Tactic:
Lex.left _ _ hk

Premises used: Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b_1 : (i : ι) × α i
inst : IsTrans ι r
inst_1 : ∀ (i : ι), IsTrans (α i) (s i)
i : ι
a b : α i
hab : s i a b
j : ι
c : α j
hk : r i j
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j c)

Tactic:
exact Lex.left _ _ hk

Premises used: Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b_1 : (i : ι) × α i
inst : IsTrans ι r
inst_1 : ∀ (i : ι), IsTrans (α i) (s i)
i : ι
a b : α i
hab : s i a b
c : α i
hc : s i b c
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i c)

Tactic:
Lex.right _ _ (_root_.trans hab hc)

Premises used: trans, Sigma.Lex.right
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b_1 : (i : ι) × α i
inst : IsTrans ι r
inst_1 : ∀ (i : ι), IsTrans (α i) (s i)
i : ι
a b : α i
hab : s i a b
c : α i
hc : s i b c
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i c)

Tactic:
exact Lex.right _ _ (_root_.trans hab hc)

Premises used: trans, Sigma.Lex.right
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b_1 : (i : ι) × α i
inst : Std.Symm r
inst_1 : ∀ (i : ι), Std.Symm (s i)
i j : ι
a : α i
b : α j
hij : r i j
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) j b) (mk (β := fun (i : ι) ↦ α i) i a)

Tactic:
Lex.left _ _ (symm hij)

Premises used: symm, Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b_1 : (i : ι) × α i
inst : Std.Symm r
inst_1 : ∀ (i : ι), Std.Symm (s i)
i j : ι
a : α i
b : α j
hij : r i j
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) j b) (mk (β := fun (i : ι) ↦ α i) i a)

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

Premises used: symm, Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b_1 : (i : ι) × α i
inst : Std.Symm r
inst_1 : ∀ (i : ι), Std.Symm (s i)
i : ι
a b : α i
hab : s i a b
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)

Tactic:
Lex.right _ _ (symm hab)

Premises used: Sigma.Lex.right, symm
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b_1 : (i : ι) × α i
inst : Std.Symm r
inst_1 : ∀ (i : ι), Std.Symm (s i)
i : ι
a b : α i
hab : s i a b
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)

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

Premises used: Sigma.Lex.right, symm
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b_1 : (i : ι) × α i
inst : Std.Asymm r
inst_1 : ∀ (i : ι), Std.Antisymm (s i)
i j : ι
a : α i
b : α j
hij : r i j
hji : r j i
⊢ mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) j b

Tactic:
(asymm hij hji).elim

Premises used: asymm, False.elim
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b_1 : (i : ι) × α i
inst : Std.Asymm r
inst_1 : ∀ (i : ι), Std.Antisymm (s i)
i j : ι
a : α i
b : α j
hij : r i j
hji : r j i
⊢ mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) j b

Tactic:
exact (asymm hij hji).elim

Premises used: asymm, False.elim
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b_1 : (i : ι) × α i
inst : Std.Asymm r
inst_1 : ∀ (i : ι), Std.Antisymm (s i)
i : ι
a b : α i
hij : r i i
hba : s i b a
⊢ mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i b

Tactic:
(irrefl _ hij).elim

Premises used: irrefl, False.elim
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b_1 : (i : ι) × α i
inst : Std.Asymm r
inst_1 : ∀ (i : ι), Std.Antisymm (s i)
i : ι
a b : α i
hij : r i i
hba : s i b a
⊢ mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i b

Tactic:
exact (irrefl _ hij).elim

Premises used: irrefl, False.elim
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b_1 : (i : ι) × α i
inst : Std.Asymm r
inst_1 : ∀ (i : ι), Std.Antisymm (s i)
i : ι
a b : α i
hab : s i a b
hji : r i i
⊢ mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i b

Tactic:
(irrefl _ hji).elim

Premises used: irrefl, False.elim
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b_1 : (i : ι) × α i
inst : Std.Asymm r
inst_1 : ∀ (i : ι), Std.Antisymm (s i)
i : ι
a b : α i
hab : s i a b
hji : r i i
⊢ mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i b

Tactic:
exact (irrefl _ hji).elim

Premises used: irrefl, False.elim
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a_1 b_1 : (i : ι) × α i
inst : Std.Asymm r
inst_1 : ∀ (i : ι), Std.Antisymm (s i)
i : ι
a b : α i
hab : s i a b
hba : s i b a
⊢ mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i b

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

Premises used: congr_arg, antisymm, Sigma.mk