-- Mathlib/Data/Seq/WSeq.lean
theorem flatten_pure (s : WSeq α) : flatten (Computation.pure s) = s

Proof state:
α : Type u
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
⊢ Seq.BisimO (fun s1 s2 => flatten (Computation.pure s2) = s1) (Seq.destruct (flatten (Computation.pure s))) s.destruct

Tactic:
simp only [Seq.BisimO, flatten, Seq.omap, pure_def, Seq.corec_eq, destruct_pure]

Result:
α : Type u
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
⊢ match
    match
      match s.destruct with
      | none => none
      | some (a, b) => some (a, Computation.pure b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          Seq.corec
            (fun c =>
              match c.destruct with
              | Sum.inl s =>
                match Seq.destruct s with
                | none => none
                | some (a, b) => some (a, Computation.pure b)
              | Sum.inr c' => some (none, c'))
            b),
    s.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      Seq.corec
          (fun c =>
            match c.destruct with
            | Sum.inl s =>
              match Seq.destruct s with
              | none => none
              | some (a, b) => some (a, Computation.pure b)
            | Sum.inr c' => some (none, c'))
          (Computation.pure s') =
        s
  | x, x_1 => False

Proof state:
α : Type u
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
⊢ match
    match
      match s.destruct with
      | none => none
      | some (a, b) => some (a, Computation.pure b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          Seq.corec
            (fun c =>
              match c.destruct with
              | Sum.inl s =>
                match Seq.destruct s with
                | none => none
                | some (a, b) => some (a, Computation.pure b)
              | Sum.inr c' => some (none, c'))
            b),
    s.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      Seq.corec
          (fun c =>
            match c.destruct with
            | Sum.inl s =>
              match Seq.destruct s with
              | none => none
              | some (a, b) => some (a, Computation.pure b)
            | Sum.inr c' => some (none, c'))
          (Computation.pure s') =
        s
  | x, x_1 => False

Tactic:
cases Seq.destruct s with
| none => simp
| some val =>
  obtain ⟨o, s'⟩ := val
  simp

Result:
no goals

Proof state:
case none
α : Type u
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
⊢ match
    match
      match none with
      | none => none
      | some (a, b) => some (a, Computation.pure b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          Seq.corec
            (fun c =>
              match c.destruct with
              | Sum.inl s =>
                match Seq.destruct s with
                | none => none
                | some (a, b) => some (a, Computation.pure b)
              | Sum.inr c' => some (none, c'))
            b),
    none with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      Seq.corec
          (fun c =>
            match c.destruct with
            | Sum.inl s =>
              match Seq.destruct s with
              | none => none
              | some (a, b) => some (a, Computation.pure b)
            | Sum.inr c' => some (none, c'))
          (Computation.pure s') =
        s
  | x, x_1 => False

Tactic:
simp

Result:
no goals

Proof state:
case some.mk
α : Type u
s✝ : WSeq α
s'✝ s : Seq (Option α)
h : flatten (Computation.pure s) = s'✝
o : Option α
s' : Seq (Option α)
⊢ match
    match
      match some (o, s') with
      | none => none
      | some (a, b) => some (a, Computation.pure b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          Seq.corec
            (fun c =>
              match c.destruct with
              | Sum.inl s =>
                match Seq.destruct s with
                | none => none
                | some (a, b) => some (a, Computation.pure b)
              | Sum.inr c' => some (none, c'))
            b),
    some (o, s') with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      Seq.corec
          (fun c =>
            match c.destruct with
            | Sum.inl s =>
              match Seq.destruct s with
              | none => none
              | some (a, b) => some (a, Computation.pure b)
            | Sum.inr c' => some (none, c'))
          (Computation.pure s') =
        s
  | x, x_1 => False

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
⊢ Seq.BisimO (fun s1 s2 => flatten (Computation.pure s2) = s1) s'.destruct s.destruct

Tactic:
rw [← h]

Result:
α : Type u
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
⊢ Seq.BisimO (fun s1 s2 => flatten (Computation.pure s2) = s1) (Seq.destruct (flatten (Computation.pure s))) s.destruct

Proof state:
case some
α : Type u
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
val : Seq1 (Option α)
⊢ match
    match
      match some val with
      | none => none
      | some (a, b) => some (a, Computation.pure b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          Seq.corec
            (fun c =>
              match c.destruct with
              | Sum.inl s =>
                match Seq.destruct s with
                | none => none
                | some (a, b) => some (a, Computation.pure b)
              | Sum.inr c' => some (none, c'))
            b),
    some val with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      Seq.corec
          (fun c =>
            match c.destruct with
            | Sum.inl s =>
              match Seq.destruct s with
              | none => none
              | some (a, b) => some (a, Computation.pure b)
            | Sum.inr c' => some (none, c'))
          (Computation.pure s') =
        s
  | x, x_1 => False

Tactic:
obtain ⟨o, s'⟩ := val

Result:
case some.mk
α : Type u
s✝ : WSeq α
s'✝ s : Seq (Option α)
h : flatten (Computation.pure s) = s'✝
o : Option α
s' : Seq (Option α)
⊢ match
    match
      match some (o, s') with
      | none => none
      | some (a, b) => some (a, Computation.pure b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          Seq.corec
            (fun c =>
              match c.destruct with
              | Sum.inl s =>
                match Seq.destruct s with
                | none => none
                | some (a, b) => some (a, Computation.pure b)
              | Sum.inr c' => some (none, c'))
            b),
    some (o, s') with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      Seq.corec
          (fun c =>
            match c.destruct with
            | Sum.inl s =>
              match Seq.destruct s with
              | none => none
              | some (a, b) => some (a, Computation.pure b)
            | Sum.inr c' => some (none, c'))
          (Computation.pure s') =
        s
  | x, x_1 => False

Proof state:
α : Type u
s : WSeq α
⊢ flatten (Computation.pure s) = s

Tactic:
refine Seq.eq_of_bisim (fun s1 s2 => flatten (Computation.pure s2) = s1) ?_ rfl

Result:
α : Type u
s : WSeq α
⊢ Seq.IsBisimulation fun s1 s2 => flatten (Computation.pure s2) = s1

Proof state:
α : Type u
s : WSeq α
⊢ Seq.IsBisimulation fun s1 s2 => flatten (Computation.pure s2) = s1

Tactic:
intro s' s h

Result:
α : Type u
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
⊢ Seq.BisimO (fun s1 s2 => flatten (Computation.pure s2) = s1) s'.destruct s.destruct