-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem lex_eq_false_iff_exists [BEq α] [PartialEquivBEq α] (lt : α → α → Bool)
    (lt_irrefl : ∀ x y, x == y → lt x y = false)
    (lt_asymm : ∀ x y, lt x y = true → lt y x = false)
    (lt_antisymm : ∀ x y, lt x y = false → lt y x = false → x == y) :
    lex l₁ l₂ lt = false ↔
      (l₂.isEqv (l₁.take 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.zero
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
lt : α → α → Bool
lt_irrefl : ∀ (x y : α), (x == y) = true → lt x y = false
lt_asymm : ∀ (x y : α), lt x y = true → lt y x = false
lt_antisymm : ∀ (x y : α), lt x y = false → lt y x = false → (x == y) = true
a : α
l₁ : List α
ih :
  ∀ {l₂ : List α},
    l₁.lex l₂ lt = false ↔
      (l₂.isEqv (take l₂.length l₁) fun x1 x2 => x1 == x2) = true ∨
        ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₂[i] l₁[i] = true
b : α
l₂ : List α
h₁ : 0 < l₁.length + 1
h₂ : 0 < l₂.length + 1
w₁ : ∀ (j : Nat) (hj : j < 0), ((a :: l₁)[j] == (b :: l₂)[j]) = true
w₂ : lt b a = true
⊢ lt a b = false ∧
    ((a == b) = true →
      (l₂.isEqv (take l₂.length l₁) fun x1 x2 => x1 == x2) = true ∨
        ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₂[i] l₁[i] = true)

Tactic:
refine ⟨lt_asymm _ _ w₂, ?_⟩

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

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
lt : α → α → Bool
lt_irrefl : ∀ (x y : α), (x == y) = true → lt x y = false
lt_asymm : ∀ (x y : α), lt x y = true → lt y x = false
lt_antisymm : ∀ (x y : α), lt x y = false → lt y x = false → (x == y) = true
a : α
l₁ : List α
ih :
  ∀ {l₂ : List α},
    l₁.lex l₂ lt = false ↔
      (l₂.isEqv (take l₂.length l₁) fun x1 x2 => x1 == x2) = true ∨
        ∃ 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 = false
h :
  (a == b) = true →
    (l₂.isEqv (take l₂.length l₁) fun x1 x2 => x1 == x2) = true ∨
      ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₂[i] l₁[i] = true
eq : (b == a) = true
⊢ (b == a) = true ∧ (l₂.isEqv (take l₂.length l₁) fun x1 x2 => x1 == x2) = true ∨
    ∃ i h h₂, (∀ (j : Nat) (hj : j < i), ((a :: l₁)[j] == (b :: l₂)[j]) = true) ∧ lt (b :: l₂)[i] (a :: l₁)[i] = true

Tactic:
specialize h (BEq.symm eq)

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
lt : α → α → Bool
lt_irrefl : ∀ (x y : α), (x == y) = true → lt x y = false
lt_asymm : ∀ (x y : α), lt x y = true → lt y x = false
lt_antisymm : ∀ (x y : α), lt x y = false → lt y x = false → (x == y) = true
a : α
l₁ : List α
ih :
  ∀ {l₂ : List α},
    l₁.lex l₂ lt = false ↔
      (l₂.isEqv (take l₂.length l₁) fun x1 x2 => x1 == x2) = true ∨
        ∃ 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 = false
eq : (b == a) = true
h :
  (l₂.isEqv (take l₂.length l₁) fun x1 x2 => x1 == x2) = true ∨
    ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₂[i] l₁[i] = true
⊢ (b == a) = true ∧ (l₂.isEqv (take l₂.length l₁) fun x1 x2 => x1 == x2) = true ∨
    ∃ i h h₂, (∀ (j : Nat) (hj : j < i), ((a :: l₁)[j] == (b :: l₂)[j]) = true) ∧ lt (b :: l₂)[i] (a :: l₁)[i] = true

Proof state:
case cons.cons.mp
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
lt : α → α → Bool
lt_irrefl : ∀ (x y : α), (x == y) = true → lt x y = false
lt_asymm : ∀ (x y : α), lt x y = true → lt y x = false
lt_antisymm : ∀ (x y : α), lt x y = false → lt y x = false → (x == y) = true
a : α
l₁ : List α
ih :
  ∀ {l₂ : List α},
    l₁.lex l₂ lt = false ↔
      (l₂.isEqv (take l₂.length l₁) fun x1 x2 => x1 == x2) = true ∨
        ∃ 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 = false ∧
      ((a == b) = true →
        (l₂.isEqv (take l₂.length l₁) fun x1 x2 => x1 == x2) = true ∨
          ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₂[i] l₁[i] = true) →
    (b == a) = true ∧ (l₂.isEqv (take l₂.length l₁) fun x1 x2 => x1 == x2) = true ∨
      ∃ i h h₂, (∀ (j : Nat) (hj : j < i), ((a :: l₁)[j] == (b :: l₂)[j]) = true) ∧ lt (b :: l₂)[i] (a :: l₁)[i] = true

Tactic:
rintro ⟨hab, h⟩

Result:
case cons.cons.mp.intro
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
lt : α → α → Bool
lt_irrefl : ∀ (x y : α), (x == y) = true → lt x y = false
lt_asymm : ∀ (x y : α), lt x y = true → lt y x = false
lt_antisymm : ∀ (x y : α), lt x y = false → lt y x = false → (x == y) = true
a : α
l₁ : List α
ih :
  ∀ {l₂ : List α},
    l₁.lex l₂ lt = false ↔
      (l₂.isEqv (take l₂.length l₁) fun x1 x2 => x1 == x2) = true ∨
        ∃ 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 = false
h :
  (a == b) = true →
    (l₂.isEqv (take l₂.length l₁) fun x1 x2 => x1 == x2) = true ∨
      ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₂[i] l₁[i] = true
⊢ (b == a) = true ∧ (l₂.isEqv (take l₂.length l₁) fun x1 x2 => x1 == x2) = true ∨
    ∃ i h h₂, (∀ (j : Nat) (hj : j < i), ((a :: l₁)[j] == (b :: l₂)[j]) = true) ∧ lt (b :: l₂)[i] (a :: l₁)[i] = true

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
lt : α → α → Bool
lt_irrefl : ∀ (x y : α), (x == y) = true → lt x y = false
lt_asymm : ∀ (x y : α), lt x y = true → lt y x = false
lt_antisymm : ∀ (x y : α), lt x y = false → lt y x = false → (x == y) = true
a : α
l₁ : List α
ih :
  ∀ {l₂ : List α},
    l₁.lex l₂ lt = false ↔
      (l₂.isEqv (take l₂.length l₁) fun x1 x2 => x1 == x2) = true ∨
        ∃ 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 (b :: l₂)[i + 1] (a :: l₁)[i + 1] = true
x✝ : (a == b) = true
⊢ i < l₁.length

Tactic:
simpa using h₁

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
lt : α → α → Bool
lt_irrefl : ∀ (x y : α), (x == y) = true → lt x y = false
lt_asymm : ∀ (x y : α), lt x y = true → lt y x = false
lt_antisymm : ∀ (x y : α), lt x y = false → lt y x = false → (x == y) = true
a : α
l₁ : List α
ih :
  ∀ {l₂ : List α},
    l₁.lex l₂ lt = false ↔
      (l₂.isEqv (take l₂.length l₁) fun x1 x2 => x1 == x2) = true ∨
        ∃ 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 = false
eq : (b == a) = true
h : (l₂.isEqv (take l₂.length l₁) fun x1 x2 => x1 == x2) = true
⊢ (b == a) = true ∧ (l₂.isEqv (take l₂.length l₁) fun x1 x2 => x1 == x2) = true ∨
    ∃ i h h₂, (∀ (j : Nat) (hj : j < i), ((a :: l₁)[j] == (b :: l₂)[j]) = true) ∧ lt (b :: l₂)[i] (a :: l₁)[i] = true

Tactic:
exact .inl ⟨eq, h⟩

Result:
no goals