-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem lex_eq_true_iff_exists [BEq α] (lt : α → α → Bool) :
    lex l₁ l₂ lt = true ↔
      (l₁.isEqv (l₂.take l₁.length) (· == ·) ∧ l₁.length < l₂.length) ∨
        (∃ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length),
          (∀ j, (hj : j < i) →
            l₁[j]'(Nat.lt_trans hj h₁) == l₂[j]'(Nat.lt_trans hj h₂)) ∧ lt l₁[i] l₂[i])

Proof state:
case cons.cons.mpr.inr.intro.intro.intro.intro.succ.h
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a : α
l₁ : List α
ih :
  ∀ {l₂ : List α},
    l₁.lex l₂ lt = true ↔
      (l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true ∧ l₁.length < l₂.length ∨
        ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₁[i] l₂[i] = true
b : α
l₂ : List α
i : Nat
h₁ : i + 1 < l₁.length + 1
h₂ : i + 1 < l₂.length + 1
w₁ : ∀ (j : Nat) (hj : j < i + 1), ((a :: l₁)[j] == (b :: l₂)[j]) = true
w₂ : lt (a :: l₁)[i + 1] (b :: l₂)[i + 1] = true
⊢ (l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true ∧ l₁.length < l₂.length ∨
    ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₁[i] l₂[i] = true

Tactic:
right

Result:
case cons.cons.mpr.inr.intro.intro.intro.intro.succ.h.h
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a : α
l₁ : List α
ih :
  ∀ {l₂ : List α},
    l₁.lex l₂ lt = true ↔
      (l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true ∧ l₁.length < l₂.length ∨
        ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₁[i] l₂[i] = true
b : α
l₂ : List α
i : Nat
h₁ : i + 1 < l₁.length + 1
h₂ : i + 1 < l₂.length + 1
w₁ : ∀ (j : Nat) (hj : j < i + 1), ((a :: l₁)[j] == (b :: l₂)[j]) = true
w₂ : lt (a :: l₁)[i + 1] (b :: l₂)[i + 1] = true
⊢ ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₁[i] l₂[i] = true

Proof state:
case cons.cons.mp
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a : α
l₁ : List α
ih :
  ∀ {l₂ : List α},
    l₁.lex l₂ lt = true ↔
      (l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true ∧ l₁.length < l₂.length ∨
        ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₁[i] l₂[i] = true
b : α
l₂ : List α
⊢ lt a b = true ∨
      (a == b) = true ∧
        ((l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true ∧ l₁.length < l₂.length ∨
          ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₁[i] l₂[i] = true) →
    ((a == b) = true ∧ (l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true) ∧ l₁.length < l₂.length ∨
      ∃ i h h₂, (∀ (j : Nat) (hj : j < i), ((a :: l₁)[j] == (b :: l₂)[j]) = true) ∧ lt (a :: l₁)[i] (b :: l₂)[i] = true

Tactic:
rintro (hab | ⟨hab, ⟨h₁, h₂⟩ | ⟨i, h₁, h₂, w₁, w₂⟩⟩)

Result:
case cons.cons.mp.inl
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a : α
l₁ : List α
ih :
  ∀ {l₂ : List α},
    l₁.lex l₂ lt = true ↔
      (l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true ∧ l₁.length < l₂.length ∨
        ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₁[i] l₂[i] = true
b : α
l₂ : List α
hab : lt a b = true
⊢ ((a == b) = true ∧ (l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true) ∧ l₁.length < l₂.length ∨
    ∃ i h h₂, (∀ (j : Nat) (hj : j < i), ((a :: l₁)[j] == (b :: l₂)[j]) = true) ∧ lt (a :: l₁)[i] (b :: l₂)[i] = true

case cons.cons.mp.inr.intro.inl.intro
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a : α
l₁ : List α
ih :
  ∀ {l₂ : List α},
    l₁.lex l₂ lt = true ↔
      (l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true ∧ l₁.length < l₂.length ∨
        ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₁[i] l₂[i] = true
b : α
l₂ : List α
hab : (a == b) = true
h₁ : (l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true
h₂ : l₁.length < l₂.length
⊢ ((a == b) = true ∧ (l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true) ∧ l₁.length < l₂.length ∨
    ∃ i h h₂, (∀ (j : Nat) (hj : j < i), ((a :: l₁)[j] == (b :: l₂)[j]) = true) ∧ lt (a :: l₁)[i] (b :: l₂)[i] = true

case cons.cons.mp.inr.intro.inr.intro.intro.intro.intro
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a : α
l₁ : List α
ih :
  ∀ {l₂ : List α},
    l₁.lex l₂ lt = true ↔
      (l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true ∧ l₁.length < l₂.length ∨
        ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₁[i] l₂[i] = true
b : α
l₂ : List α
hab : (a == b) = true
i : Nat
h₁ : i < l₁.length
h₂ : i < l₂.length
w₁ : ∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true
w₂ : lt l₁[i] l₂[i] = true
⊢ ((a == b) = true ∧ (l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true) ∧ l₁.length < l₂.length ∨
    ∃ i h h₂, (∀ (j : Nat) (hj : j < i), ((a :: l₁)[j] == (b :: l₂)[j]) = true) ∧ lt (a :: l₁)[i] (b :: l₂)[i] = true

Proof state:
case cons.cons.mp.inl
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a : α
l₁ : List α
ih :
  ∀ {l₂ : List α},
    l₁.lex l₂ lt = true ↔
      (l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true ∧ l₁.length < l₂.length ∨
        ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₁[i] l₂[i] = true
b : α
l₂ : List α
hab : lt a b = true
⊢ ((a == b) = true ∧ (l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true) ∧ l₁.length < l₂.length ∨
    ∃ i h h₂, (∀ (j : Nat) (hj : j < i), ((a :: l₁)[j] == (b :: l₂)[j]) = true) ∧ lt (a :: l₁)[i] (b :: l₂)[i] = true

Tactic:
exact .inr ⟨0, by simp [hab]⟩

Result:
no goals

Proof state:
case cons.cons.mp.inr.intro.inr.intro.intro.intro.intro.refine_1.zero
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a : α
l₁ : List α
ih :
  ∀ {l₂ : List α},
    l₁.lex l₂ lt = true ↔
      (l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true ∧ l₁.length < l₂.length ∨
        ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₁[i] l₂[i] = true
b : α
l₂ : List α
hab : (a == b) = true
i : Nat
h₁ : i < l₁.length
h₂ : i < l₂.length
w₁ : ∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true
w₂ : lt l₁[i] l₂[i] = true
hj : 0 < i + 1
⊢ ((a :: l₁)[0] == (b :: l₂)[0]) = true

Tactic:
simp [hab]

Result:
no goals

Proof state:
case cons.cons.mpr.inr.intro.intro.intro.intro.succ.h.h
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a : α
l₁ : List α
ih :
  ∀ {l₂ : List α},
    l₁.lex l₂ lt = true ↔
      (l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true ∧ l₁.length < l₂.length ∨
        ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₁[i] l₂[i] = true
b : α
l₂ : List α
i : Nat
h₁ : i + 1 < l₁.length + 1
h₂ : i + 1 < l₂.length + 1
w₁ : ∀ (j : Nat) (hj : j < i + 1), ((a :: l₁)[j] == (b :: l₂)[j]) = true
w₂ : lt (a :: l₁)[i + 1] (b :: l₂)[i + 1] = true
⊢ ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₁[i] l₂[i] = true

Tactic:
refine ⟨i, by simpa using h₁, by simpa using h₂, ?_, ?_⟩

Result:
case cons.cons.mpr.inr.intro.intro.intro.intro.succ.h.h.refine_1
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a : α
l₁ : List α
ih :
  ∀ {l₂ : List α},
    l₁.lex l₂ lt = true ↔
      (l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true ∧ l₁.length < l₂.length ∨
        ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₁[i] l₂[i] = true
b : α
l₂ : List α
i : Nat
h₁ : i + 1 < l₁.length + 1
h₂ : i + 1 < l₂.length + 1
w₁ : ∀ (j : Nat) (hj : j < i + 1), ((a :: l₁)[j] == (b :: l₂)[j]) = true
w₂ : lt (a :: l₁)[i + 1] (b :: l₂)[i + 1] = true
⊢ ∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true

case cons.cons.mpr.inr.intro.intro.intro.intro.succ.h.h.refine_2
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a : α
l₁ : List α
ih :
  ∀ {l₂ : List α},
    l₁.lex l₂ lt = true ↔
      (l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true ∧ l₁.length < l₂.length ∨
        ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₁[i] l₂[i] = true
b : α
l₂ : List α
i : Nat
h₁ : i + 1 < l₁.length + 1
h₂ : i + 1 < l₂.length + 1
w₁ : ∀ (j : Nat) (hj : j < i + 1), ((a :: l₁)[j] == (b :: l₂)[j]) = true
w₂ : lt (a :: l₁)[i + 1] (b :: l₂)[i + 1] = true
⊢ lt l₁[i] l₂[i] = true