awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : α × β
mp : x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2)
mpr : x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2) → x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2
mp₁ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2)
mp₂ : x.2 ≤ y.2 → x.1 ≤ y.1 → y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2)
mp₃ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2)
mp₄ : x.2 ≤ y.2 → x.1 ≤ y.1 → y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2)
mp₅ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1
mp₆ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2
mp₇ : x.2 ≤ y.2 → x.1 ≤ y.1 → y.1 ≤ x.1 → x.1 ≤ y.1
mp₈ : x.2 ≤ y.2 → x.1 ≤ y.1 → y.1 ≤ x.1 → x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2
mpr₁ mpr₂ :
  x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2) → x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2
mpr₃ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → x.1 ≤ y.1
mpr₄ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → y.1 ≤ x.1
mpr₅ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → x.2 ≤ y.2
mp₉ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2
mp₁₀ mp₁₁ mp₁₂ : x.2 ≤ y.2 → x.1 ≤ y.1 → y.1 ≤ x.1 → x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2
mpr₆ : x.1 ≤ y.1 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬x.1 ≤ y.1 → y.1 ≤ x.1
mpr₇ : x.1 ≤ y.1 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬¬y.1 ≤ x.1 → y.1 ≤ x.1
mpr₈ : x.1 ≤ y.1 → x.2 ≤ y.2 → ¬x.1 ≤ y.1 → y.1 ≤ x.1
mpr₉ : x.1 ≤ y.1 → x.2 ≤ y.2 → ¬¬y.1 ≤ x.1 → y.1 ≤ x.1
mpr₁₀ : x.1 ≤ y.1 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬¬y.1 ≤ x.1 → y.1 ≤ x.1
mpr₁₁ : x.1 ≤ y.1 → x.2 ≤ y.2 → ¬¬y.1 ≤ x.1 → y.1 ≤ x.1
mpr₁₂ : x.1 ≤ y.1 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬¬y.1 ≤ x.1 → y.1 ≤ x.1
mpr₁₃ : x.1 ≤ y.1 → x.2 ≤ y.2 → ¬¬y.1 ≤ x.1 → y.1 ≤ x.1
mpr₁₄ : x.1 ≤ y.1 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬x.1 ≤ y.1 → x.2 ≤ y.2
mpr₁₅ : x.1 ≤ y.1 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2
mpr₁₆ : x.1 ≤ y.1 → x.2 ≤ y.2 → ¬x.1 ≤ y.1 → x.2 ≤ y.2
mpr₁₇ : x.1 ≤ y.1 → x.2 ≤ y.2 → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2
mpr₁₈ : x.1 ≤ y.1 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2
mpr₁₉ : x.1 ≤ y.1 → x.2 ≤ y.2 → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2
mpr₂₀ : x.1 ≤ y.1 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2
mpr₂₁ : x.1 ≤ y.1 → x.2 ≤ y.2 → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2
mpr₂₂ : x.1 ≤ y.1 → y.1 ≤ x.1 → ¬x.1 ≤ y.1 → y.1 ≤ x.1
mpr₂₃ : x.1 ≤ y.1 → y.1 ≤ x.1 → ¬y.1 ≤ x.1 → y.1 ≤ x.1
mpr₂₄ mpr₂₅ mpr₂₆ : x.1 ≤ y.1 → x.2 ≤ y.2 → y.1 ≤ x.1 → y.1 ≤ x.1
mpr₂₇ : x.1 ≤ y.1 → y.1 ≤ x.1 → ¬x.1 ≤ y.1 → x.2 ≤ y.2
⊢ x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ↔ x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2)
have mpr₂₈ : x.1 ≤ y.1 → y.1 ≤ x.1 → ¬y.1 ≤ x.1 → x.2 ≤ y.2
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : α × β
⊢ LT.lt (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) x : Lex (α × β))
      ((toLex : (a : α × β) → Lex (α × β)) y : Lex (α × β)) ↔
    x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 < y.2)
have rw : x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2 ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 < y.2)
Tactic: rw [toLex_lt_toLex]
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : α × β
⊢ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2 ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 < y.2)
have simp : x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 ↔
  x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
Tactic: simp only [lt_iff_le_not_ge, le_antisymm_iff]
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : α × β
⊢ x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 ↔
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
have mp : x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 →
  x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : α × β
mp :
  x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 →
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
⊢ x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 ↔
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
have mpr : x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) →
  x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : α × β
mp :
  x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 →
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mpr :
  x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) →
    x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
⊢ x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 ↔
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
have mp₁ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : α × β
mp :
  x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 →
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mpr :
  x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) →
    x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mp₁ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
⊢ x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 ↔
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
have mp₂ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : α × β
mp :
  x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 →
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mpr :
  x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) →
    x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mp₁ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₂ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₃ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₄ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
⊢ x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 ↔
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
have mp₅ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : α × β
mp :
  x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 →
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mpr :
  x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) →
    x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mp₁ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₂ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₃ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₄ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₅ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1
⊢ x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 ↔
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
have mp₆ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : α × β
mp :
  x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 →
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mpr :
  x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) →
    x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mp₁ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₂ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₃ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₄ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₅ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1
mp₆ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
⊢ x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 ↔
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
have mp₇ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : α × β
mp :
  x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 →
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mpr :
  x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) →
    x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mp₁ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₂ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₃ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₄ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₅ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1
mp₆ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mp₇ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1
⊢ x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 ↔
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
have mp₈ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : α × β
mp :
  x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 →
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mpr :
  x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) →
    x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mp₁ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₂ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₃ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₄ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₅ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1
mp₆ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mp₇ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1
mp₈ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
⊢ x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 ↔
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
have mpr₁ : x.1 ≤ y.1 →
  (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) →
    x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : α × β
mp :
  x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 →
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mpr :
  x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) →
    x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mp₁ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₂ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₃ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₄ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₅ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1
mp₆ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mp₇ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1
mp₈ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mpr₁ mpr₂ :
  x.1 ≤ y.1 →
    (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) →
      x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
⊢ x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 ↔
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
have mpr₃ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → x.1 ≤ y.1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : α × β
mp :
  x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 →
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mpr :
  x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) →
    x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mp₁ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₂ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₃ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₄ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₅ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1
mp₆ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mp₇ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1
mp₈ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mpr₁ mpr₂ :
  x.1 ≤ y.1 →
    (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) →
      x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mpr₃ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → x.1 ≤ y.1
⊢ x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 ↔
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
have mpr₄ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → y.1 ≤ x.1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : α × β
mp :
  x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 →
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mpr :
  x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) →
    x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mp₁ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₂ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₃ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₄ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₅ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1
mp₆ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mp₇ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1
mp₈ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mpr₁ mpr₂ :
  x.1 ≤ y.1 →
    (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) →
      x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mpr₃ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → x.1 ≤ y.1
mpr₄ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → y.1 ≤ x.1
⊢ x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 ↔
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
have mpr₅ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → x.2 ≤ y.2
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : α × β
mp :
  x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 →
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mpr :
  x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) →
    x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mp₁ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₂ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₃ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₄ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₅ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1
mp₆ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mp₇ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1
mp₈ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mpr₁ mpr₂ :
  x.1 ≤ y.1 →
    (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) →
      x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mpr₃ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → x.1 ≤ y.1
mpr₄ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → y.1 ≤ x.1
mpr₅ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → x.2 ≤ y.2
⊢ x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 ↔
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
have mpr₆ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → ¬y.2 ≤ x.2
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : α × β
mp :
  x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 →
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mpr :
  x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) →
    x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mp₁ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₂ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₃ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₄ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₅ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1
mp₆ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mp₇ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1
mp₈ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mpr₁ mpr₂ :
  x.1 ≤ y.1 →
    (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) →
      x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mpr₃ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → x.1 ≤ y.1
mpr₄ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → y.1 ≤ x.1
mpr₅ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → x.2 ≤ y.2
mpr₆ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → ¬y.2 ≤ x.2
⊢ x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 ↔
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
have mp₉ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Prod.Lex (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : α × β
mp :
  x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 →
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mpr :
  x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) →
    x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mp₁ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₂ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₃ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₄ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
mp₅ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1
mp₆ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mp₇ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1
mp₈ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mpr₁ mpr₂ :
  x.1 ≤ y.1 →
    (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) →
      x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
mpr₃ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → x.1 ≤ y.1
mpr₄ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → y.1 ≤ x.1
mpr₅ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → x.2 ≤ y.2
mpr₆ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → ¬y.2 ≤ x.2
mp₉ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
⊢ x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 ↔
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
have mp₁₀ : x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2
Tactic: tauto