awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact congr_arg (Sigma.mk _ ·) <| antisymm hab hba

Premises used: congr_arg, antisymm, Sigma.mk
-- 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.Trichotomous r
inst_1 : ∀ (i : ι), Std.Total (s i)
i : ι
a : α i
j : ι
b : α j
inl :
  ∀ (hij : r i j),
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b) ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) j b) (mk (β := fun (i : ι) ↦ α i) i a)
inr :
  ∀ (b : α i),
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b) ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)
inr₁ :
  ∀ (hji : r j i),
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b) ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) j b) (mk (β := fun (i : ι) ↦ α i) i a)
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b) ∨
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) j b) (mk (β := fun (i : ι) ↦ α i) i a)

Tactic:
obtain hij | rfl | hji := trichotomous_of r i j

Premises used: trichotomous_of, rfl
-- 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.Trichotomous r
inst_1 : ∀ (i : ι), Std.Total (s i)
i : ι
a : α i
j : ι
b : α j
hij : r i j
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b) ∨
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) j b) (mk (β := fun (i : ι) ↦ α i) i a)

Tactic:
Or.inl (Lex.left _ _ hij)

Premises used: Or.inl, 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.Trichotomous r
inst_1 : ∀ (i : ι), Std.Total (s i)
i : ι
a : α i
j : ι
b : α j
hij : r i j
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b) ∨
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) j b) (mk (β := fun (i : ι) ↦ α i) i a)

Tactic:
exact Or.inl (Lex.left _ _ hij)

Premises used: Or.inl, 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.Trichotomous r
inst_1 : ∀ (i : ι), Std.Total (s i)
i : ι
a b : α i
inr :
  ∀ (hab : s i a b),
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b) ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)
inr₁ :
  ∀ (hba : s i b a),
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b) ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b) ∨
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)

Tactic:
obtain hab | hba := total_of (s i) a b

Premises used: total_of
-- 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.Trichotomous r
inst_1 : ∀ (i : ι), Std.Total (s i)
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 (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)

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

Premises used: Sigma.Lex.right, Or.inl
-- 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.Trichotomous r
inst_1 : ∀ (i : ι), Std.Total (s i)
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 (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)

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

Premises used: Sigma.Lex.right, Or.inl
-- 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.Trichotomous r
inst_1 : ∀ (i : ι), Std.Total (s i)
i : ι
a b : α i
hba : s i b a
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b) ∨
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)

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

Premises used: Sigma.Lex.right, Or.inr
-- 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.Trichotomous r
inst_1 : ∀ (i : ι), Std.Total (s i)
i : ι
a b : α i
hba : s i b a
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b) ∨
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)

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

Premises used: Sigma.Lex.right, Or.inr
-- 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.Trichotomous r
inst_1 : ∀ (i : ι), Std.Total (s i)
i : ι
a : α i
j : ι
b : α j
hji : r j i
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b) ∨
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) j b) (mk (β := fun (i : ι) ↦ α i) i a)

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

Premises used: Or.inr, 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.Trichotomous r
inst_1 : ∀ (i : ι), Std.Total (s i)
i : ι
a : α i
j : ι
b : α j
hji : r j i
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b) ∨
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) j b) (mk (β := fun (i : ι) ↦ α i) i a)

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

Premises used: Or.inr, 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.Trichotomous r
inst_1 : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a : α i
j : ι
b : α j
inl :
  ∀ (hij : r i j),
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b) ∨
      mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) j b ∨
        Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) j b) (mk (β := fun (i : ι) ↦ α i) i a)
inr :
  ∀ (b : α i),
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b) ∨
      mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i b ∨
        Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)
inr₁ :
  ∀ (hji : r j i),
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b) ∨
      mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) j b ∨
        Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) j b) (mk (β := fun (i : ι) ↦ α i) i a)
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b) ∨
    mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) j b ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) j b) (mk (β := fun (i : ι) ↦ α i) i a)

Tactic:
obtain hij | rfl | hji := trichotomous_of r i j

Premises used: trichotomous_of, rfl
-- 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.Trichotomous r
inst_1 : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a : α i
j : ι
b : α j
hij : r i j
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b) ∨
    mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) j b ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) j b) (mk (β := fun (i : ι) ↦ α i) i a)

Tactic:
Or.inl (Lex.left _ _ hij)

Premises used: Or.inl, 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.Trichotomous r
inst_1 : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a : α i
j : ι
b : α j
hij : r i j
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b) ∨
    mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) j b ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) j b) (mk (β := fun (i : ι) ↦ α i) i a)

Tactic:
exact Or.inl (Lex.left _ _ hij)

Premises used: Or.inl, 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.Trichotomous r
inst_1 : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a b : α i
inr :
  ∀ (hab : s i a b),
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b) ∨
      mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i b ∨
        Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)
inr₁ :
  Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i a) ∨
    mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i a ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i a)
inr₂ :
  ∀ (hba : s i b a),
    Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b) ∨
      mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i b ∨
        Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b) ∨
    mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i b ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)

Tactic:
obtain hab | rfl | hba := trichotomous_of (s i) a b

Premises used: trichotomous_of, rfl
-- 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.Trichotomous r
inst_1 : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a b : α i
hab : s i a b
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b) ∨
    mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i b ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)

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

Premises used: Sigma.Lex.right, Or.inl
-- 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.Trichotomous r
inst_1 : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a b : α i
hab : s i a b
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b) ∨
    mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i b ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)

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

Premises used: Sigma.Lex.right, Or.inl
-- 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.Trichotomous r
inst_1 : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a : α i
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i a) ∨
    mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i a ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i a)

Tactic:
Or.inr (Or.inl rfl)

Premises used: Or.inl, Or.inr, rfl
-- 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.Trichotomous r
inst_1 : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a : α i
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i a) ∨
    mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i a ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i a)

Tactic:
exact Or.inr (Or.inl rfl)

Premises used: Or.inl, Or.inr, rfl
-- 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.Trichotomous r
inst_1 : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a b : α i
hba : s i b a
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b) ∨
    mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i b ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)

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

Premises used: Sigma.Lex.right, Or.inr
-- 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.Trichotomous r
inst_1 : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a b : α i
hba : s i b a
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) i b) ∨
    mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) i b ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i b) (mk (β := fun (i : ι) ↦ α i) i a)

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

Premises used: Sigma.Lex.right, Or.inr
-- 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.Trichotomous r
inst_1 : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a : α i
j : ι
b : α j
hji : r j i
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b) ∨
    mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) j b ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) j b) (mk (β := fun (i : ι) ↦ α i) i a)

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

Premises used: Or.inr, 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.Trichotomous r
inst_1 : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a : α i
j : ι
b : α j
hji : r j i
⊢ Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b) ∨
    mk (β := fun (i : ι) ↦ α i) i a = mk (β := fun (i : ι) ↦ α i) j b ∨
      Lex (α := α) r s (mk (β := fun (i : ι) ↦ α i) j b) (mk (β := fun (i : ι) ↦ α i) i a)

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

Premises used: Or.inr, Sigma.Lex.left
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Sort u_1
α : ι → Sort 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:
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a₁ : ι
a : α a₁
a₂ : ι
b : α a₂
hij : r a₁ a₂
⊢ r ((mk (β := α) a₁ a).fst (β := fun (i : ι) ↦ α i)) ((mk (β := α) a₂ b).fst (β := fun (i : ι) ↦ α i)) ∨
    ∃ (h : (mk (β := α) a₁ a).fst (β := fun (i : ι) ↦ α i) = (mk (β := α) a₂ b).fst (β := fun (i : ι) ↦ α i)),
      s ((mk (β := α) a₂ b).fst (β := fun (i : ι) ↦ α i))
        (Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := α) a₁ a).fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
          ((mk (β := α) a₁ a).snd (β := fun (i : ι) ↦ α i)) h)
        ((mk (β := α) a₂ b).snd (β := fun (i : ι) ↦ α i))

Tactic:
Or.inl hij

Premises used: Or.inl
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a₁ : ι
a : α a₁
a₂ : ι
b : α a₂
hij : r a₁ a₂
⊢ r ((mk (β := α) a₁ a).fst (β := fun (i : ι) ↦ α i)) ((mk (β := α) a₂ b).fst (β := fun (i : ι) ↦ α i)) ∨
    ∃ (h : (mk (β := α) a₁ a).fst (β := fun (i : ι) ↦ α i) = (mk (β := α) a₂ b).fst (β := fun (i : ι) ↦ α i)),
      s ((mk (β := α) a₂ b).fst (β := fun (i : ι) ↦ α i))
        (Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := α) a₁ a).fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
          ((mk (β := α) a₁ a).snd (β := fun (i : ι) ↦ α i)) h)
        ((mk (β := α) a₂ b).snd (β := fun (i : ι) ↦ α i))

Tactic:
exact Or.inl hij

Premises used: Or.inl
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i : ι
b₁ b₂ : α i
hab : s i b₁ b₂
⊢ r ((mk (β := α) i b₁).fst (β := fun (i : ι) ↦ α i)) ((mk (β := α) i b₂).fst (β := fun (i : ι) ↦ α i)) ∨
    ∃ (h : (mk (β := α) i b₁).fst (β := fun (i : ι) ↦ α i) = (mk (β := α) i b₂).fst (β := fun (i : ι) ↦ α i)),
      s ((mk (β := α) i b₂).fst (β := fun (i : ι) ↦ α i))
        (Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := α) i b₁).fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
          ((mk (β := α) i b₁).snd (β := fun (i : ι) ↦ α i)) h)
        ((mk (β := α) i b₂).snd (β := fun (i : ι) ↦ α i))

Tactic:
Or.inr ⟨rfl, hab⟩

Premises used: Exists.intro, Or.inr, rfl
-- Module: Mathlib.Data.Sigma.Lex
Goal:
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i : ι
b₁ b₂ : α i
hab : s i b₁ b₂
⊢ r ((mk (β := α) i b₁).fst (β := fun (i : ι) ↦ α i)) ((mk (β := α) i b₂).fst (β := fun (i : ι) ↦ α i)) ∨
    ∃ (h : (mk (β := α) i b₁).fst (β := fun (i : ι) ↦ α i) = (mk (β := α) i b₂).fst (β := fun (i : ι) ↦ α i)),
      s ((mk (β := α) i b₂).fst (β := fun (i : ι) ↦ α i))
        (Eq.rec (motive := fun (x : ι) (x_1 : (mk (β := α) i b₁).fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
          ((mk (β := α) i b₁).snd (β := fun (i : ι) ↦ α i)) h)
        ((mk (β := α) i b₂).snd (β := fun (i : ι) ↦ α i))

Tactic:
exact Or.inr ⟨rfl, hab⟩

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

Tactic:
obtain ⟨a, b, hij⟩ | ⟨i, hab⟩ := h
-- 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:
Lex.left _ _ (hr _ _ hij)

Premises used: PSigma.Lex.left