-- Mathlib/Data/Seq/WSeq.lean
theorem map_join (f : α → β) (S) : map f (join S) = join (map (map f) S)

Proof state:
case h1.h3
α : Type u
β : Type v
f : α → β
S✝ : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
S : WSeq (WSeq α)
⊢ ∃ s S_1, map f S.join = s.append (map f S_1.join) ∧ (map (map f) S).join = s.append (map (map f) S_1).join

Tactic:
refine ⟨nil, S, ?_, ?_⟩ <;> simp

Result:
no goals

Proof state:
case h2
α : Type u
β : Type v
f : α → β
S✝ : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
S : WSeq (WSeq α)
a : β
s : WSeq β
⊢ ∃ s_1 S_1,
    s.append (map f S.join) = s_1.append (map f S_1.join) ∧
      s.append (map (map f) S).join = s_1.append (map (map f) S_1).join

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

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
S✝ : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
s : WSeq β
S : WSeq (WSeq α)
⊢ Seq.BisimO (fun s1 s2 => ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct (s.append (map f S.join))) (Seq.destruct (s.append (map (map f) S).join))

Tactic:
induction' s using WSeq.recOn with a s s <;> simp

Result:
case h1
α : Type u
β : Type v
f : α → β
S✝ : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
S : WSeq (WSeq α)
⊢ match Seq.destruct (map f S.join), Seq.destruct (map (map f) S).join with
  | none, none => True
  | some (a, s), some (a', s') => a = a' ∧ ∃ s_1 S, s = s_1.append (map f S.join) ∧ s' = s_1.append (map (map f) S).join
  | x, x_1 => False

case h2
α : Type u
β : Type v
f : α → β
S✝ : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
S : WSeq (WSeq α)
a : β
s : WSeq β
⊢ ∃ s_1 S_1,
    s.append (map f S.join) = s_1.append (map f S_1.join) ∧
      s.append (map (map f) S).join = s_1.append (map (map f) S_1).join

case h3
α : Type u
β : Type v
f : α → β
S✝ : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
S : WSeq (WSeq α)
s : WSeq β
⊢ ∃ s_1 S_1,
    s.append (map f S.join) = s_1.append (map f S_1.join) ∧
      s.append (map (map f) S).join = s_1.append (map (map f) S_1).join

Proof state:
case h1.h2
α : Type u
β : Type v
f : α → β
S✝ : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
s : WSeq α
S : WSeq (WSeq α)
⊢ ∃ s_1 S_1,
    (map f s).append (map f S.join) = s_1.append (map f S_1.join) ∧
      (map f s).append (map (map f) S).join = s_1.append (map (map f) S_1).join

Tactic:
exact ⟨map f s, S, rfl, rfl⟩

Result:
no goals

Proof state:
case bisim
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ Seq.IsBisimulation fun s1 s2 => ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join

Tactic:
intro s1 s2 h

Result:
case bisim
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
⊢ Seq.BisimO (fun s1 s2 => ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join) s1.destruct
    s2.destruct

Proof state:
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ map f S.join = (map (map f) S).join

Tactic:
apply
  Seq.eq_of_bisim fun s1 s2 =>
    ∃ s S, s1 = append s (map f (join S)) ∧ s2 = append s (join (map (map f) S))

Result:
case bisim
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ Seq.IsBisimulation fun s1 s2 => ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join

case r
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ ∃ s S_1, map f S.join = s.append (map f S_1.join) ∧ (map (map f) S).join = s.append (map (map f) S_1).join

Proof state:
case h1
α : Type u
β : Type v
f : α → β
S✝ : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
S : WSeq (WSeq α)
⊢ match Seq.destruct (map f S.join), Seq.destruct (map (map f) S).join with
  | none, none => True
  | some (a, s), some (a', s') => a = a' ∧ ∃ s_1 S, s = s_1.append (map f S.join) ∧ s' = s_1.append (map (map f) S).join
  | x, x_1 => False

Tactic:
induction' S using WSeq.recOn with s S S <;> simp

Result:
case h1.h2
α : Type u
β : Type v
f : α → β
S✝ : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
s : WSeq α
S : WSeq (WSeq α)
⊢ ∃ s_1 S_1,
    (map f s).append (map f S.join) = s_1.append (map f S_1.join) ∧
      (map f s).append (map (map f) S).join = s_1.append (map (map f) S_1).join

case h1.h3
α : Type u
β : Type v
f : α → β
S✝ : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
S : WSeq (WSeq α)
⊢ ∃ s S_1, map f S.join = s.append (map f S_1.join) ∧ (map (map f) S).join = s.append (map (map f) S_1).join

Proof state:
case h3
α : Type u
β : Type v
f : α → β
S✝ : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
S : WSeq (WSeq α)
s : WSeq β
⊢ ∃ s_1 S_1,
    s.append (map f S.join) = s_1.append (map f S_1.join) ∧
      s.append (map (map f) S).join = s_1.append (map (map f) S_1).join

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

Result:
no goals

Proof state:
case r
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ ∃ s S_1, map f S.join = s.append (map f S_1.join) ∧ (map (map f) S).join = s.append (map (map f) S_1).join

Tactic:
refine ⟨nil, S, ?_, ?_⟩ <;> simp

Result:
no goals