-- 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:
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a b : α
xs ys : Array α
⊢ (do
      let r ←
        forIn' { start := 0, stop := min (#[a] ++ xs).size (#[b] ++ ys).size, step := 1, step_pos := Nat.zero_lt_one }
            ⟨none, PUnit.unit⟩ fun i h r =>
            if lt (#[a] ++ xs)[i] (#[b] ++ ys)[i] = true then pure (ForInStep.done ⟨some true, PUnit.unit⟩)
            else
              if ((#[a] ++ xs)[i] != (#[b] ++ ys)[i]) = true then pure (ForInStep.done ⟨some false, PUnit.unit⟩)
              else do
                pure PUnit.unit
                pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => do
          pure PUnit.unit
          pure (decide ((#[a] ++ xs).size < (#[b] ++ ys).size))
        | some a => pure a) =
    (lt a b ||
      a == b && do
        let r ←
          forIn' { start := 0, stop := min xs.size ys.size, step := 1, step_pos := Nat.zero_lt_one } ⟨none, PUnit.unit⟩
              fun i h r =>
              if lt xs[i] ys[i] = true then pure (ForInStep.done ⟨some true, PUnit.unit⟩)
              else
                if (xs[i] != ys[i]) = true then pure (ForInStep.done ⟨some false, PUnit.unit⟩)
                else do
                  pure PUnit.unit
                  pure (ForInStep.yield ⟨none, PUnit.unit⟩)
        match r.fst with
          | none => do
            pure PUnit.unit
            pure (decide (xs.size < ys.size))
          | some a => pure a)

Tactic:
simp only [Std.Range.forIn'_eq_forIn'_range', size_append, size_toArray, List.length_singleton,
  Nat.add_comm 1]

Result:
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a b : α
xs ys : Array α
⊢ (do
      let r ←
        forIn'
            (List.range' 0
              { start := 0, stop := min (xs.size + 1) (ys.size + 1), step := 1, step_pos := Nat.zero_lt_one }.size 1)
            ⟨none, PUnit.unit⟩ fun a_1 m b_1 =>
            if lt (#[a] ++ xs)[a_1] (#[b] ++ ys)[a_1] = true then pure (ForInStep.done ⟨some true, PUnit.unit⟩)
            else
              if ((#[a] ++ xs)[a_1] != (#[b] ++ ys)[a_1]) = true then pure (ForInStep.done ⟨some false, PUnit.unit⟩)
              else do
                pure PUnit.unit
                pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => do
          pure PUnit.unit
          pure (decide (xs.size + 1 < ys.size + 1))
        | some a => pure a) =
    (lt a b ||
      a == b && do
        let r ←
          forIn'
              (List.range' 0 { start := 0, stop := min xs.size ys.size, step := 1, step_pos := Nat.zero_lt_one }.size 1)
              ⟨none, PUnit.unit⟩ fun a h r =>
              if lt xs[a] ys[a] = true then pure (ForInStep.done ⟨some true, PUnit.unit⟩)
              else
                if (xs[a] != ys[a]) = true then pure (ForInStep.done ⟨some false, PUnit.unit⟩)
                else do
                  pure PUnit.unit
                  pure (ForInStep.yield ⟨none, PUnit.unit⟩)
        match r.fst with
          | none => do
            pure PUnit.unit
            pure (decide (xs.size < ys.size))
          | some a => pure a)

Proof state:
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a b : α
xs ys : Array α
⊢ (#[a] ++ xs).lex (#[b] ++ ys) lt = (lt a b || a == b && xs.lex ys lt)

Tactic:
simp only [lex, Id.run]

Result:
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a b : α
xs ys : Array α
⊢ (do
      let r ←
        forIn' { start := 0, stop := min (#[a] ++ xs).size (#[b] ++ ys).size, step := 1, step_pos := Nat.zero_lt_one }
            ⟨none, PUnit.unit⟩ fun i h r =>
            if lt (#[a] ++ xs)[i] (#[b] ++ ys)[i] = true then pure (ForInStep.done ⟨some true, PUnit.unit⟩)
            else
              if ((#[a] ++ xs)[i] != (#[b] ++ ys)[i]) = true then pure (ForInStep.done ⟨some false, PUnit.unit⟩)
              else do
                pure PUnit.unit
                pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => do
          pure PUnit.unit
          pure (decide ((#[a] ++ xs).size < (#[b] ++ ys).size))
        | some a => pure a) =
    (lt a b ||
      a == b && do
        let r ←
          forIn' { start := 0, stop := min xs.size ys.size, step := 1, step_pos := Nat.zero_lt_one } ⟨none, PUnit.unit⟩
              fun i h r =>
              if lt xs[i] ys[i] = true then pure (ForInStep.done ⟨some true, PUnit.unit⟩)
              else
                if (xs[i] != ys[i]) = true then pure (ForInStep.done ⟨some false, PUnit.unit⟩)
                else do
                  pure PUnit.unit
                  pure (ForInStep.yield ⟨none, PUnit.unit⟩)
        match r.fst with
          | none => do
            pure PUnit.unit
            pure (decide (xs.size < ys.size))
          | some a => pure a)

Proof state:
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a b : α
xs ys : Array α
⊢ (do
      let r ←
        forIn'
            (List.range' 0
              { start := 0, stop := min (xs.size + 1) (ys.size + 1), step := 1, step_pos := Nat.zero_lt_one }.size 1)
            ⟨none, PUnit.unit⟩ fun a_1 m b_1 =>
            if lt (#[a] ++ xs)[a_1] (#[b] ++ ys)[a_1] = true then pure (ForInStep.done ⟨some true, PUnit.unit⟩)
            else
              if ((#[a] ++ xs)[a_1] != (#[b] ++ ys)[a_1]) = true then pure (ForInStep.done ⟨some false, PUnit.unit⟩)
              else do
                pure PUnit.unit
                pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => do
          pure PUnit.unit
          pure (decide (xs.size + 1 < ys.size + 1))
        | some a => pure a) =
    (lt a b ||
      a == b && do
        let r ←
          forIn'
              (List.range' 0 { start := 0, stop := min xs.size ys.size, step := 1, step_pos := Nat.zero_lt_one }.size 1)
              ⟨none, PUnit.unit⟩ fun a h r =>
              if lt xs[a] ys[a] = true then pure (ForInStep.done ⟨some true, PUnit.unit⟩)
              else
                if (xs[a] != ys[a]) = true then pure (ForInStep.done ⟨some false, PUnit.unit⟩)
                else do
                  pure PUnit.unit
                  pure (ForInStep.yield ⟨none, PUnit.unit⟩)
        match r.fst with
          | none => do
            pure PUnit.unit
            pure (decide (xs.size < ys.size))
          | some a => pure a)

Tactic:
simp [Nat.add_min_add_right, List.range'_succ, getElem_append_left, List.range'_succ_left,
  getElem_append_right]

Result:
α : 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)