-- Mathlib/Data/Seq/WSeq.lean
theorem tail_congr {s t : WSeq α} (h : s ~ʷ t) : tail s ~ʷ tail t

Proof state:
case a
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a b : Option (α × WSeq α)
h : BisimO (fun x1 x2 => x1 ~ʷ x2) a b
⊢ Computation.LiftRel Equiv ((Computation.pure ∘ fun o => Option.rec nil Prod.snd o) a)
    ((Computation.pure ∘ fun o => Option.rec nil Prod.snd o) b)

Tactic:
simp only [comp_apply, liftRel_pure]

Result:
case a
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a b : Option (α × WSeq α)
h : BisimO (fun x1 x2 => x1 ~ʷ x2) a b
⊢ Option.rec nil Prod.snd a ~ʷ Option.rec nil Prod.snd b

Proof state:
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ s.tail ~ʷ t.tail

Tactic:
apply flatten_congr

Result:
case a
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ Computation.LiftRel Equiv ((fun o => Option.recOn o nil Prod.snd) <$> s.destruct)
    ((fun o => Option.recOn o nil Prod.snd) <$> t.destruct)

Proof state:
case a.none.some
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
b : α × WSeq α
h : BisimO (fun x1 x2 => x1 ~ʷ x2) none (some b)
⊢ Option.rec nil Prod.snd none ~ʷ Option.rec nil Prod.snd (some b)

Tactic:
cases h

Result:
no goals

Proof state:
case a
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ Computation.LiftRel Equiv (Computation.map (fun o => Option.rec nil Prod.snd o) s.destruct)
    (Computation.map (fun o => Option.rec nil Prod.snd o) t.destruct)

Tactic:
rw [← Computation.bind_pure, ← Computation.bind_pure]

Result:
case a
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ Computation.LiftRel Equiv (s.destruct.bind (Computation.pure ∘ fun o => Option.rec nil Prod.snd o))
    (t.destruct.bind (Computation.pure ∘ fun o => Option.rec nil Prod.snd o))

Proof state:
case a.some.some.mk
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
b : α × WSeq α
a : α
s' : WSeq α
h : BisimO (fun x1 x2 => x1 ~ʷ x2) (some (a, s')) (some b)
⊢ Option.rec nil Prod.snd (some (a, s')) ~ʷ Option.rec nil Prod.snd (some b)

Tactic:
obtain ⟨b, t'⟩ := b

Result:
case a.some.some.mk.mk
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a : α
s' : WSeq α
b : α
t' : WSeq α
h : BisimO (fun x1 x2 => x1 ~ʷ x2) (some (a, s')) (some (b, t'))
⊢ Option.rec nil Prod.snd (some (a, s')) ~ʷ Option.rec nil Prod.snd (some (b, t'))

Proof state:
case a.none.none
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
h : BisimO (fun x1 x2 => x1 ~ʷ x2) none none
⊢ Option.rec nil Prod.snd none ~ʷ Option.rec nil Prod.snd none

Tactic:
trivial

Result:
no goals

Proof state:
case a.some.none.mk
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
fst✝ : α
snd✝ : WSeq α
h : BisimO (fun x1 x2 => x1 ~ʷ x2) (some (fst✝, snd✝)) none
⊢ Option.rec nil Prod.snd (some (fst✝, snd✝)) ~ʷ Option.rec nil Prod.snd none

Tactic:
cases h

Result:
no goals

Proof state:
case a
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a b : Option (α × WSeq α)
h : BisimO (fun x1 x2 => x1 ~ʷ x2) a b
⊢ Option.rec nil Prod.snd a ~ʷ Option.rec nil Prod.snd b

Tactic:
rcases a with - | a <;> rcases b with - | b

Result:
case a.none.none
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
h : BisimO (fun x1 x2 => x1 ~ʷ x2) none none
⊢ Option.rec nil Prod.snd none ~ʷ Option.rec nil Prod.snd none

case a.none.some
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
b : α × WSeq α
h : BisimO (fun x1 x2 => x1 ~ʷ x2) none (some b)
⊢ Option.rec nil Prod.snd none ~ʷ Option.rec nil Prod.snd (some b)

case a.some.none
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a : α × WSeq α
h : BisimO (fun x1 x2 => x1 ~ʷ x2) (some a) none
⊢ Option.rec nil Prod.snd (some a) ~ʷ Option.rec nil Prod.snd none

case a.some.some
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a b : α × WSeq α
h : BisimO (fun x1 x2 => x1 ~ʷ x2) (some a) (some b)
⊢ Option.rec nil Prod.snd (some a) ~ʷ Option.rec nil Prod.snd (some b)

Proof state:
case a.some.none
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a : α × WSeq α
h : BisimO (fun x1 x2 => x1 ~ʷ x2) (some a) none
⊢ Option.rec nil Prod.snd (some a) ~ʷ Option.rec nil Prod.snd none

Tactic:
cases a

Result:
case a.some.none.mk
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
fst✝ : α
snd✝ : WSeq α
h : BisimO (fun x1 x2 => x1 ~ʷ x2) (some (fst✝, snd✝)) none
⊢ Option.rec nil Prod.snd (some (fst✝, snd✝)) ~ʷ Option.rec nil Prod.snd none

Proof state:
case a.some.some
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a b : α × WSeq α
h : BisimO (fun x1 x2 => x1 ~ʷ x2) (some a) (some b)
⊢ Option.rec nil Prod.snd (some a) ~ʷ Option.rec nil Prod.snd (some b)

Tactic:
obtain ⟨a, s'⟩ := a

Result:
case a.some.some.mk
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
b : α × WSeq α
a : α
s' : WSeq α
h : BisimO (fun x1 x2 => x1 ~ʷ x2) (some (a, s')) (some b)
⊢ Option.rec nil Prod.snd (some (a, s')) ~ʷ Option.rec nil Prod.snd (some b)

Proof state:
case a
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ Computation.LiftRel Equiv (s.destruct.bind (Computation.pure ∘ fun o => Option.rec nil Prod.snd o))
    (t.destruct.bind (Computation.pure ∘ fun o => Option.rec nil Prod.snd o))

Tactic:
apply liftRel_bind _ _ (destruct_congr h)

Result:
case a
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ ∀ {a b : Option (α × WSeq α)},
    BisimO (fun x1 x2 => x1 ~ʷ x2) a b →
      Computation.LiftRel Equiv ((Computation.pure ∘ fun o => Option.rec nil Prod.snd o) a)
        ((Computation.pure ∘ fun o => Option.rec nil Prod.snd o) b)

Proof state:
case a.some.some.mk.mk
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a : α
s' : WSeq α
b : α
t' : WSeq α
h : BisimO (fun x1 x2 => x1 ~ʷ x2) (some (a, s')) (some (b, t'))
⊢ Option.rec nil Prod.snd (some (a, s')) ~ʷ Option.rec nil Prod.snd (some (b, t'))

Tactic:
exact h.right

Result:
no goals

Proof state:
case a
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ ∀ {a b : Option (α × WSeq α)},
    BisimO (fun x1 x2 => x1 ~ʷ x2) a b →
      Computation.LiftRel Equiv ((Computation.pure ∘ fun o => Option.rec nil Prod.snd o) a)
        ((Computation.pure ∘ fun o => Option.rec nil Prod.snd o) b)

Tactic:
intro a b h

Result:
case a
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a b : Option (α × WSeq α)
h : BisimO (fun x1 x2 => x1 ~ʷ x2) a b
⊢ Computation.LiftRel Equiv ((Computation.pure ∘ fun o => Option.rec nil Prod.snd o) a)
    ((Computation.pure ∘ fun o => Option.rec nil Prod.snd o) b)