-- Mathlib/Data/Seq/WSeq.lean
theorem join_map_ret (s : WSeq α) : join (map ret s) ~ʷ s

Proof state:
α : Type u
s✝¹ s' s✝ : WSeq α
h : (map ret s✝).join = s'
c1 c2 : Computation (Option (α × WSeq α))
s : WSeq α
this :
  ∀ (s : WSeq α),
    ∃ s',
      (map (fun a => cons a nil) s).join.destruct = (map (fun a => cons a nil) s').join.destruct ∧
        s.destruct = s'.destruct
⊢ LiftRelAux (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 => (map ret s2).join = s1)
    (fun c1 c2 => ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct) (map ret s).join.destruct.destruct
    s.destruct.destruct

Tactic:
induction' s using WSeq.recOn with a s s <;>
  simp (config := { unfoldPartialApp := true }) [ret, ret_mem, this, Option.exists]

Result:
no goals

Proof state:
α : Type u
s✝ s' s : WSeq α
h : (map ret s).join = s'
⊢ Computation.LiftRel (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 => (map ret s2).join = s1) s'.destruct s.destruct

Tactic:
rw [← h]

Result:
α : Type u
s✝ s' s : WSeq α
h : (map ret s).join = s'
⊢ Computation.LiftRel (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 => (map ret s2).join = s1) (map ret s).join.destruct
    s.destruct

Proof state:
α : Type u
s✝¹ s' s✝ : WSeq α
h : (map ret s✝).join = s'
c1 c2 : Computation (Option (α × WSeq α))
s : WSeq α
⊢ LiftRelAux (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 => (map ret s2).join = s1)
    (fun c1 c2 => ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct) (map ret s).join.destruct.destruct
    s.destruct.destruct

Tactic:
have : ∀ s, ∃ s' : WSeq α,
    (map (fun a => cons a nil) s).join.destruct =
      (map (fun a => cons a nil) s').join.destruct ∧ destruct s = s'.destruct :=
  fun s => ⟨s, rfl, rfl⟩

Result:
α : Type u
s✝¹ s' s✝ : WSeq α
h : (map ret s✝).join = s'
c1 c2 : Computation (Option (α × WSeq α))
s : WSeq α
this :
  ∀ (s : WSeq α),
    ∃ s',
      (map (fun a => cons a nil) s).join.destruct = (map (fun a => cons a nil) s').join.destruct ∧
        s.destruct = s'.destruct
⊢ LiftRelAux (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 => (map ret s2).join = s1)
    (fun c1 c2 => ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct) (map ret s).join.destruct.destruct
    s.destruct.destruct

Proof state:
α : Type u
s : WSeq α
⊢ (map ret s).join ~ʷ s

Tactic:
refine ⟨fun s1 s2 => join (map ret s2) = s1, rfl, ?_⟩

Result:
α : Type u
s : WSeq α
⊢ ∀ {s t : WSeq α},
    (fun s1 s2 => (map ret s2).join = s1) s t →
      Computation.LiftRel (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 => (map ret s2).join = s1) s.destruct t.destruct

Proof state:
case Hc
α : Type u
s✝ s' s : WSeq α
h : (map ret s).join = s'
⊢ ∃ s_1, (map ret s).join.destruct = (map ret s_1).join.destruct ∧ s.destruct = s_1.destruct

Tactic:
exact ⟨s, rfl, rfl⟩

Result:
no goals

Proof state:
α : Type u
s✝ s' s : WSeq α
h : (map ret s).join = s'
⊢ Computation.LiftRel (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 => (map ret s2).join = s1) (map ret s).join.destruct
    s.destruct

Tactic:
apply liftRel_rec fun c1 c2 => ∃ s, c1 = destruct (join (map ret s)) ∧ c2 = destruct s

Result:
case H
α : Type u
s✝ s' s : WSeq α
h : (map ret s).join = s'
⊢ ∀ {ca cb : Computation (Option (α × WSeq α))},
    (∃ s, ca = (map ret s).join.destruct ∧ cb = s.destruct) →
      LiftRelAux (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 => (map ret s2).join = s1)
        (fun c1 c2 => ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct) ca.destruct cb.destruct

case Hc
α : Type u
s✝ s' s : WSeq α
h : (map ret s).join = s'
⊢ ∃ s_1, (map ret s).join.destruct = (map ret s_1).join.destruct ∧ s.destruct = s_1.destruct

Proof state:
case H
α : Type u
s✝ s' s : WSeq α
h : (map ret s).join = s'
⊢ ∀ {ca cb : Computation (Option (α × WSeq α))},
    (∃ s, ca = (map ret s).join.destruct ∧ cb = s.destruct) →
      LiftRelAux (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 => (map ret s2).join = s1)
        (fun c1 c2 => ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct) ca.destruct cb.destruct

Tactic:
exact fun {c1 c2} h =>
  match c1, c2, h with
  | _, _, ⟨s, rfl, rfl⟩ => by
    clear h
    have : ∀ s, ∃ s' : WSeq α,
        (map (fun a => cons a nil) s).join.destruct =
          (map (fun a => cons a nil) s').join.destruct ∧ destruct s = s'.destruct :=
      fun s => ⟨s, rfl, rfl⟩
    induction' s using WSeq.recOn with a s s <;>
      simp (config := { unfoldPartialApp := true }) [ret, ret_mem, this, Option.exists]

Result:
no goals

Proof state:
α : Type u
s : WSeq α
⊢ ∀ {s t : WSeq α},
    (fun s1 s2 => (map ret s2).join = s1) s t →
      Computation.LiftRel (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 => (map ret s2).join = s1) s.destruct t.destruct

Tactic:
intro s' s h

Result:
α : Type u
s✝ s' s : WSeq α
h : (map ret s).join = s'
⊢ Computation.LiftRel (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 => (map ret s2).join = s1) s'.destruct s.destruct

Proof state:
α : Type u
s✝¹ s' s✝ : WSeq α
h✝ : (map ret s✝).join = s'
c1 c2 : Computation (Option (α × WSeq α))
h : ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct
s : WSeq α
⊢ LiftRelAux (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 => (map ret s2).join = s1)
    (fun c1 c2 => ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct) (map ret s).join.destruct.destruct
    s.destruct.destruct

Tactic:
clear h

Result:
α : Type u
s✝¹ s' s✝ : WSeq α
h : (map ret s✝).join = s'
c1 c2 : Computation (Option (α × WSeq α))
s : WSeq α
⊢ LiftRelAux (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 => (map ret s2).join = s1)
    (fun c1 c2 => ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct) (map ret s).join.destruct.destruct
    s.destruct.destruct