-- 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
mpr₁₇ : x.1 ≤ y.1 → ¬x.1 ≤ y.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.2 ≤ y.2
mpr₁₈ : x.1 ≤ y.1 → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → 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 → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → 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 → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → x.2 ≤ y.2
mpr₂₃ : x.1 ≤ y.1 → y.2 ≤ x.2 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬x.1 ≤ y.1 → False
mpr₂₄ : x.1 ≤ y.1 → y.2 ≤ x.2 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬¬y.1 ≤ x.1 → False
mpr₂₅ : x.1 ≤ y.1 → y.2 ≤ x.2 → ¬x.1 ≤ y.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → False
mpr₂₆ : x.1 ≤ y.1 → y.2 ≤ x.2 → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2 → ¬y.2 ≤ x.2 → False
mpr₂₇ mpr₂₈ : x.1 ≤ y.1 → y.2 ≤ x.2 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬¬y.1 ≤ x.1 → False
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 → 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 → y.1 ≤ x.1 → ¬x.1 ≤ y.1 → x.2 ≤ y.2
Tactic: tauto