-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s_1 s : Seq α
H :
  match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop)
    match (motive := Option (α × Seq α × Seq α) → Option (α × Seq α))
      match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) destruct nil with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun (x : Seq α × Seq α) ↦
              match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
              | none =>
                match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.2))
            b),
    destruct nil with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_2 : Seq α),
        s =
            corec
              (fun (x : Seq α × Seq α) ↦
                match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
                | none =>
                  match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.2))
              (nil, s_2) ∧
          s' = s_2
  | x, x_1 => False
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop)
    match (motive := Option (α × Seq α × Seq α) → Option (α × Seq α))
      match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) s.destruct with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun (x : Seq α × Seq α) ↦
              match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
              | none =>
                match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.2))
            b),
    s.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_2 : Seq α),
        s =
            corec
              (fun (x : Seq α × Seq α) ↦
                match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
                | none =>
                  match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.2))
              (nil, s_2) ∧
          s' = s_2
  | x, x_1 => False
have H₁ : ∀ (x : α) (s : Seq α),
  match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop)
    match (motive := Option (α × Seq α × Seq α) → Option (α × Seq α))
      match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) (cons x s).destruct with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun (x : Seq α × Seq α) ↦
              match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
              | none =>
                match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.2))
            b),
    (cons x s).destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_2 : Seq α),
        s =
            corec
              (fun (x : Seq α × Seq α) ↦
                match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
                | none =>
                  match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.2))
              (nil, s_2) ∧
          s' = s_2
  | x, x_1 => False
Tactic: cases s
Cleared hypotheses: s