-- Mathlib/Data/Seq/Seq.lean
theorem nil_append (s : Seq α) : append nil s = s

Proof state:
case H
α : Type u
s✝ s : Seq α
⊢ match
    match
      match s.destruct with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x =>
              match x.fst.destruct with
              | none =>
                match x.snd.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.snd))
            b),
    s.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x =>
                match x.fst.destruct with
                | none =>
                  match x.snd.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.snd))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False

Tactic:
cases s

Result:
case H.nil
α : Type u
s : Seq α
⊢ match
    match
      match nil.destruct with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x =>
              match x.fst.destruct with
              | none =>
                match x.snd.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.snd))
            b),
    nil.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x =>
                match x.fst.destruct with
                | none =>
                  match x.snd.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.snd))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False

case H.cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ match
    match
      match (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 =>
              match x.fst.destruct with
              | none =>
                match x.snd.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.snd))
            b),
    (cons x✝ s✝).destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x =>
                match x.fst.destruct with
                | none =>
                  match x.snd.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.snd))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False

Proof state:
α : Type u
s : Seq α
⊢ nil.append s = s

Tactic:
apply coinduction2

Result:
case H
α : Type u
s : Seq α
⊢ ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = nil.append s ∧ s2 = s) (nil.append s).destruct s.destruct

Proof state:
case H.cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ match
    match
      match some (x✝, s✝) with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x =>
              match x.fst.destruct with
              | none =>
                match x.snd.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.snd))
            b),
    some (x✝, s✝) with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x =>
                match x.fst.destruct with
                | none =>
                  match x.snd.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.snd))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False

Tactic:
dsimp

Result:
case H.cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ x✝ = x✝ ∧
    ∃ s,
      corec
            (fun x =>
              match x.fst.destruct with
              | none =>
                match x.snd.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.snd))
            (nil, s✝) =
          corec
            (fun x =>
              match x.fst.destruct with
              | none =>
                match x.snd.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.snd))
            (nil, s) ∧
        s✝ = s

Proof state:
case H.cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ x✝ = x✝ ∧
    ∃ s,
      corec
            (fun x =>
              match x.fst.destruct with
              | none =>
                match x.snd.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.snd))
            (nil, s✝) =
          corec
            (fun x =>
              match x.fst.destruct with
              | none =>
                match x.snd.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.snd))
            (nil, s) ∧
        s✝ = s

Tactic:
exact ⟨rfl, _, rfl, rfl⟩

Result:
no goals

Proof state:
case H
α : Type u
s✝ s : Seq α
⊢ BisimO (fun s1 s2 => ∃ s, s1 = nil.append s ∧ s2 = s) (nil.append s).destruct s.destruct

Tactic:
dsimp [append]

Result:
case H
α : Type u
s✝ s : Seq α
⊢ match
    (corec
        (fun x =>
          match x.fst.destruct with
          | none =>
            match x.snd.destruct with
            | none => none
            | some (a, b) => some (a, nil, b)
          | some (a, s₁') => some (a, s₁', x.snd))
        (nil, s)).destruct,
    s.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x =>
                match x.fst.destruct with
                | none =>
                  match x.snd.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.snd))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False

Proof state:
case H.nil
α : Type u
s : Seq α
⊢ match
    match
      match nil.destruct with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x =>
              match x.fst.destruct with
              | none =>
                match x.snd.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.snd))
            b),
    nil.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x =>
                match x.fst.destruct with
                | none =>
                  match x.snd.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.snd))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False

Tactic:
trivial

Result:
no goals