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 ∧ ¬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
mp₁₀ 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 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
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
mp₁₀ 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
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
⊢ 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 → ¬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
mp₁₀ 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
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
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 → ¬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.1 ≤ y.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
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
mp₁₀ 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
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
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 → ¬y.2 ≤ x.2
mpr₇ : x.1 ≤ y.1 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬x.1 ≤ y.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) → ¬¬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
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
mp₁₀ 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
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
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 → ¬y.2 ≤ x.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
⊢ 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 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → 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
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
mp₁₀ 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
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
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 → ¬y.2 ≤ x.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.1 ≤ y.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → 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 → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → 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
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
mp₁₀ 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
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
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 → ¬y.2 ≤ x.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.1 ≤ y.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → y.1 ≤ x.1
mpr₁₀ : x.1 ≤ y.1 → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → 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 → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → 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 → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → 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.1 ≤ y.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
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
mp₁₀ 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
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
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 → ¬y.2 ≤ x.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.1 ≤ y.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → y.1 ≤ x.1
mpr₁₀ : x.1 ≤ y.1 → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → 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 → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → 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 → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → 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
⊢ 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) → ¬¬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
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
mp₁₀ 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
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
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 → ¬y.2 ≤ x.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.1 ≤ y.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → y.1 ≤ x.1
mpr₁₀ : x.1 ≤ y.1 → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → 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 → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → 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 → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → 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
⊢ 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 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.2 ≤ y.2
Tactic: tauto