-- Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean
theorem le_iff {x y : DegLex (α →₀ ℕ)} :
    x ≤ y ↔ (ofDegLex x).degree < (ofDegLex y).degree ∨
      (ofDegLex x).degree = (ofDegLex y).degree ∧ toLex (ofDegLex x) ≤ toLex (ofDegLex y)

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
h : ¬x = y
k : ¬(ofDegLex x).degree < (ofDegLex y).degree
⊢ x = y ∨
      (ofDegLex x).degree < (ofDegLex y).degree ∨
        (ofDegLex x).degree = (ofDegLex y).degree ∧ toLex (ofDegLex x) < toLex (ofDegLex y) ↔
    (ofDegLex x).degree < (ofDegLex y).degree ∨
      (ofDegLex x).degree = (ofDegLex y).degree ∧ (x = y ∨ toLex (ofDegLex x) < toLex (ofDegLex y))

Tactic:
simp only [h, k, false_or]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
⊢ x ≤ y ↔
    (ofDegLex x).degree < (ofDegLex y).degree ∨
      (ofDegLex x).degree = (ofDegLex y).degree ∧ toLex (ofDegLex x) ≤ toLex (ofDegLex y)

Tactic:
simp only [le_iff_eq_or_lt, lt_iff, EmbeddingLike.apply_eq_iff_eq]

Result:
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
⊢ x = y ∨
      (ofDegLex x).degree < (ofDegLex y).degree ∨
        (ofDegLex x).degree = (ofDegLex y).degree ∧ toLex (ofDegLex x) < toLex (ofDegLex y) ↔
    (ofDegLex x).degree < (ofDegLex y).degree ∨
      (ofDegLex x).degree = (ofDegLex y).degree ∧ (x = y ∨ toLex (ofDegLex x) < toLex (ofDegLex y))

Proof state:
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
⊢ x = y ∨
      (ofDegLex x).degree < (ofDegLex y).degree ∨
        (ofDegLex x).degree = (ofDegLex y).degree ∧ toLex (ofDegLex x) < toLex (ofDegLex y) ↔
    (ofDegLex x).degree < (ofDegLex y).degree ∨
      (ofDegLex x).degree = (ofDegLex y).degree ∧ (x = y ∨ toLex (ofDegLex x) < toLex (ofDegLex y))

Tactic:
by_cases h : x = y

Result:
case pos
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
h : x = y
⊢ x = y ∨
      (ofDegLex x).degree < (ofDegLex y).degree ∨
        (ofDegLex x).degree = (ofDegLex y).degree ∧ toLex (ofDegLex x) < toLex (ofDegLex y) ↔
    (ofDegLex x).degree < (ofDegLex y).degree ∨
      (ofDegLex x).degree = (ofDegLex y).degree ∧ (x = y ∨ toLex (ofDegLex x) < toLex (ofDegLex y))

case neg
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
h : ¬x = y
⊢ x = y ∨
      (ofDegLex x).degree < (ofDegLex y).degree ∨
        (ofDegLex x).degree = (ofDegLex y).degree ∧ toLex (ofDegLex x) < toLex (ofDegLex y) ↔
    (ofDegLex x).degree < (ofDegLex y).degree ∨
      (ofDegLex x).degree = (ofDegLex y).degree ∧ (x = y ∨ toLex (ofDegLex x) < toLex (ofDegLex y))

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
h : ¬x = y
⊢ x = y ∨
      (ofDegLex x).degree < (ofDegLex y).degree ∨
        (ofDegLex x).degree = (ofDegLex y).degree ∧ toLex (ofDegLex x) < toLex (ofDegLex y) ↔
    (ofDegLex x).degree < (ofDegLex y).degree ∨
      (ofDegLex x).degree = (ofDegLex y).degree ∧ (x = y ∨ toLex (ofDegLex x) < toLex (ofDegLex y))

Tactic:
by_cases k : (ofDegLex x).degree < (ofDegLex y).degree

Result:
case pos
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
h : ¬x = y
k : (ofDegLex x).degree < (ofDegLex y).degree
⊢ x = y ∨
      (ofDegLex x).degree < (ofDegLex y).degree ∨
        (ofDegLex x).degree = (ofDegLex y).degree ∧ toLex (ofDegLex x) < toLex (ofDegLex y) ↔
    (ofDegLex x).degree < (ofDegLex y).degree ∨
      (ofDegLex x).degree = (ofDegLex y).degree ∧ (x = y ∨ toLex (ofDegLex x) < toLex (ofDegLex y))

case neg
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
h : ¬x = y
k : ¬(ofDegLex x).degree < (ofDegLex y).degree
⊢ x = y ∨
      (ofDegLex x).degree < (ofDegLex y).degree ∨
        (ofDegLex x).degree = (ofDegLex y).degree ∧ toLex (ofDegLex x) < toLex (ofDegLex y) ↔
    (ofDegLex x).degree < (ofDegLex y).degree ∨
      (ofDegLex x).degree = (ofDegLex y).degree ∧ (x = y ∨ toLex (ofDegLex x) < toLex (ofDegLex y))

Proof state:
case pos
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
h : x = y
⊢ x = y ∨
      (ofDegLex x).degree < (ofDegLex y).degree ∨
        (ofDegLex x).degree = (ofDegLex y).degree ∧ toLex (ofDegLex x) < toLex (ofDegLex y) ↔
    (ofDegLex x).degree < (ofDegLex y).degree ∨
      (ofDegLex x).degree = (ofDegLex y).degree ∧ (x = y ∨ toLex (ofDegLex x) < toLex (ofDegLex y))

Tactic:
simp [h]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
h : ¬x = y
k : (ofDegLex x).degree < (ofDegLex y).degree
⊢ x = y ∨
      (ofDegLex x).degree < (ofDegLex y).degree ∨
        (ofDegLex x).degree = (ofDegLex y).degree ∧ toLex (ofDegLex x) < toLex (ofDegLex y) ↔
    (ofDegLex x).degree < (ofDegLex y).degree ∨
      (ofDegLex x).degree = (ofDegLex y).degree ∧ (x = y ∨ toLex (ofDegLex x) < toLex (ofDegLex y))

Tactic:
simp [k]

Result:
no goals