-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lex/Lemmas.lean
theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs ys : Array α} :
     (#[a] ++ xs).lex (#[b] ++ ys) lt =
       (lt a b || a == b && xs.lex ys lt)

Proof state:
case false
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a b : α
xs ys : Array α
⊢ (match
      (match
          if false = true then ForInStep.done ⟨some true, PUnit.unit⟩
          else
            if (!a == b) = true then ForInStep.done ⟨some false, PUnit.unit⟩
            else ForInStep.yield ⟨none, PUnit.unit⟩ with
        | ForInStep.done b => b
        | ForInStep.yield b_1 =>
          forIn' (List.range' 0 (min xs.size ys.size) 1) b_1 fun a_1 m b_2 =>
            if lt xs[a_1] ys[a_1] = true then ForInStep.done ⟨some true, PUnit.unit⟩
            else
              if (xs[a_1] != ys[a_1]) = true then ForInStep.done ⟨some false, PUnit.unit⟩
              else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
    | none => decide (xs.size < ys.size)
    | some a => a) =
    (false ||
      a == b &&
        match
          (forIn' (List.range' 0 (min xs.size ys.size) 1) ⟨none, PUnit.unit⟩ fun a m b =>
              if lt xs[a] ys[a] = true then ForInStep.done ⟨some true, PUnit.unit⟩
              else
                if (xs[a] != ys[a]) = true then ForInStep.done ⟨some false, PUnit.unit⟩
                else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
        | none => decide (xs.size < ys.size)
        | some a => a)

Tactic:
cases a == b <;> simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a b : α
xs ys : Array α
⊢ (match
      (match
          if lt a b = true then ForInStep.done ⟨some true, PUnit.unit⟩
          else
            if (a != b) = true then ForInStep.done ⟨some false, PUnit.unit⟩ else ForInStep.yield ⟨none, PUnit.unit⟩ with
        | ForInStep.done b => b
        | ForInStep.yield b_1 =>
          forIn' (List.range' 0 (min xs.size ys.size) 1) b_1 fun a_1 m b_2 =>
            if lt xs[a_1] ys[a_1] = true then ForInStep.done ⟨some true, PUnit.unit⟩
            else
              if (xs[a_1] != ys[a_1]) = true then ForInStep.done ⟨some false, PUnit.unit⟩
              else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
    | none => decide (xs.size < ys.size)
    | some a => a) =
    (lt a b ||
      a == b &&
        match
          (forIn' (List.range' 0 (min xs.size ys.size) 1) ⟨none, PUnit.unit⟩ fun a m b =>
              if lt xs[a] ys[a] = true then ForInStep.done ⟨some true, PUnit.unit⟩
              else
                if (xs[a] != ys[a]) = true then ForInStep.done ⟨some false, PUnit.unit⟩
                else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
        | none => decide (xs.size < ys.size)
        | some a => a)

Tactic:
cases lt a b

Result:
case false
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a b : α
xs ys : Array α
⊢ (match
      (match
          if false = true then ForInStep.done ⟨some true, PUnit.unit⟩
          else
            if (a != b) = true then ForInStep.done ⟨some false, PUnit.unit⟩ else ForInStep.yield ⟨none, PUnit.unit⟩ with
        | ForInStep.done b => b
        | ForInStep.yield b_1 =>
          forIn' (List.range' 0 (min xs.size ys.size) 1) b_1 fun a_1 m b_2 =>
            if lt xs[a_1] ys[a_1] = true then ForInStep.done ⟨some true, PUnit.unit⟩
            else
              if (xs[a_1] != ys[a_1]) = true then ForInStep.done ⟨some false, PUnit.unit⟩
              else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
    | none => decide (xs.size < ys.size)
    | some a => a) =
    (false ||
      a == b &&
        match
          (forIn' (List.range' 0 (min xs.size ys.size) 1) ⟨none, PUnit.unit⟩ fun a m b =>
              if lt xs[a] ys[a] = true then ForInStep.done ⟨some true, PUnit.unit⟩
              else
                if (xs[a] != ys[a]) = true then ForInStep.done ⟨some false, PUnit.unit⟩
                else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
        | none => decide (xs.size < ys.size)
        | some a => a)

case true
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a b : α
xs ys : Array α
⊢ (match
      (match
          if true = true then ForInStep.done ⟨some true, PUnit.unit⟩
          else
            if (a != b) = true then ForInStep.done ⟨some false, PUnit.unit⟩ else ForInStep.yield ⟨none, PUnit.unit⟩ with
        | ForInStep.done b => b
        | ForInStep.yield b_1 =>
          forIn' (List.range' 0 (min xs.size ys.size) 1) b_1 fun a_1 m b_2 =>
            if lt xs[a_1] ys[a_1] = true then ForInStep.done ⟨some true, PUnit.unit⟩
            else
              if (xs[a_1] != ys[a_1]) = true then ForInStep.done ⟨some false, PUnit.unit⟩
              else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
    | none => decide (xs.size < ys.size)
    | some a => a) =
    (true ||
      a == b &&
        match
          (forIn' (List.range' 0 (min xs.size ys.size) 1) ⟨none, PUnit.unit⟩ fun a m b =>
              if lt xs[a] ys[a] = true then ForInStep.done ⟨some true, PUnit.unit⟩
              else
                if (xs[a] != ys[a]) = true then ForInStep.done ⟨some false, PUnit.unit⟩
                else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
        | none => decide (xs.size < ys.size)
        | some a => a)

Proof state:
case false
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a b : α
xs ys : Array α
⊢ (match
      (match
          if false = true then ForInStep.done ⟨some true, PUnit.unit⟩
          else
            if (a != b) = true then ForInStep.done ⟨some false, PUnit.unit⟩ else ForInStep.yield ⟨none, PUnit.unit⟩ with
        | ForInStep.done b => b
        | ForInStep.yield b_1 =>
          forIn' (List.range' 0 (min xs.size ys.size) 1) b_1 fun a_1 m b_2 =>
            if lt xs[a_1] ys[a_1] = true then ForInStep.done ⟨some true, PUnit.unit⟩
            else
              if (xs[a_1] != ys[a_1]) = true then ForInStep.done ⟨some false, PUnit.unit⟩
              else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
    | none => decide (xs.size < ys.size)
    | some a => a) =
    (false ||
      a == b &&
        match
          (forIn' (List.range' 0 (min xs.size ys.size) 1) ⟨none, PUnit.unit⟩ fun a m b =>
              if lt xs[a] ys[a] = true then ForInStep.done ⟨some true, PUnit.unit⟩
              else
                if (xs[a] != ys[a]) = true then ForInStep.done ⟨some false, PUnit.unit⟩
                else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
        | none => decide (xs.size < ys.size)
        | some a => a)

Tactic:
rw [bne]

Result:
case false
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a b : α
xs ys : Array α
⊢ (match
      (match
          if false = true then ForInStep.done ⟨some true, PUnit.unit⟩
          else
            if (!a == b) = true then ForInStep.done ⟨some false, PUnit.unit⟩
            else ForInStep.yield ⟨none, PUnit.unit⟩ with
        | ForInStep.done b => b
        | ForInStep.yield b_1 =>
          forIn' (List.range' 0 (min xs.size ys.size) 1) b_1 fun a_1 m b_2 =>
            if lt xs[a_1] ys[a_1] = true then ForInStep.done ⟨some true, PUnit.unit⟩
            else
              if (xs[a_1] != ys[a_1]) = true then ForInStep.done ⟨some false, PUnit.unit⟩
              else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
    | none => decide (xs.size < ys.size)
    | some a => a) =
    (false ||
      a == b &&
        match
          (forIn' (List.range' 0 (min xs.size ys.size) 1) ⟨none, PUnit.unit⟩ fun a m b =>
              if lt xs[a] ys[a] = true then ForInStep.done ⟨some true, PUnit.unit⟩
              else
                if (xs[a] != ys[a]) = true then ForInStep.done ⟨some false, PUnit.unit⟩
                else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
        | none => decide (xs.size < ys.size)
        | some a => a)