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

case r
α : Type u
β : Type v
γ : Type w
f : α → β
S : Seq (Seq1 α)
⊢ ∃ s S_1,
    Seq.map f (Seq.join S) = append s (Seq.map f (Seq.join S_1)) ∧
      Seq.join (Seq.map (map f) S) = append s (Seq.join (Seq.map (map f) S_1))
α : Type u
β : Type v
γ : Type w
f : α → β
S : Seq (Seq1 α)
⊢ Seq.map f (Seq.join S) = Seq.join (Seq.map (map f) S)
apply
  Seq.eq_of_bisim fun s1 s2 =>
    ∃ s S,
      s1 = Seq.append s (Seq.map f (Seq.join S)) ∧ s2 = append s (Seq.join (Seq.map (map f) S))
case bisim
α : Type u
β : Type v
γ : Type w
f : α → β
S : Seq (Seq1 α)
s1 s2 : Seq β
h : ∃ s S, s1 = append s (Seq.map f (Seq.join S)) ∧ s2 = append s (Seq.join (Seq.map (map f) S))
⊢ BisimO (fun s1 s2 => ∃ s S, s1 = append s (Seq.map f (Seq.join S)) ∧ s2 = append s (Seq.join (Seq.map (map f) S)))
    (destruct s1) (destruct s2)
case bisim
α : Type u
β : Type v
γ : Type w
f : α → β
S : Seq (Seq1 α)
⊢ Seq.IsBisimulation fun s1 s2 =>
    ∃ s S, s1 = append s (Seq.map f (Seq.join S)) ∧ s2 = append s (Seq.join (Seq.map (map f) S))
intro s1 s2 h
case h1
α : Type u
β : Type v
γ : Type w
f : α → β
S✝ : Seq (Seq1 α)
s1 s2 : Seq β
h : ∃ s S, s1 = append s (Seq.map f (Seq.join S)) ∧ s2 = append s (Seq.join (Seq.map (map f) S))
s : Seq β
S : Seq (Seq1 α)
⊢ match destruct (Seq.map f (Seq.join S)), destruct (Seq.join (Seq.map (map f) S)) with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧ ∃ s_1 S, s = append s_1 (Seq.map f (Seq.join S)) ∧ s' = append s_1 (Seq.join (Seq.map (map f) S))
  | x, x_1 => False

case h2
α : Type u
β : Type v
γ : Type w
f : α → β
S✝ : Seq (Seq1 α)
s1 s2 : Seq β
h : ∃ s S, s1 = append s (Seq.map f (Seq.join S)) ∧ s2 = append s (Seq.join (Seq.map (map f) S))
s : Seq β
S : Seq (Seq1 α)
⊢ β →
    ∀ (s : Seq β),
      ∃ s_1 S_1,
        append s (Seq.map f (Seq.join S)) = append s_1 (Seq.map f (Seq.join S_1)) ∧
          append s (Seq.join (Seq.map (map f) S)) = append s_1 (Seq.join (Seq.map (map f) S_1))
α : Type u
β : Type v
γ : Type w
f : α → β
S✝ : Seq (Seq1 α)
s1 s2 : Seq β
h : ∃ s S, s1 = append s (Seq.map f (Seq.join S)) ∧ s2 = append s (Seq.join (Seq.map (map f) S))
s : Seq β
S : Seq (Seq1 α)
⊢ BisimO (fun s1 s2 => ∃ s S, s1 = append s (Seq.map f (Seq.join S)) ∧ s2 = append s (Seq.join (Seq.map (map f) S)))
    (destruct (append s (Seq.map f (Seq.join S)))) (destruct (append s (Seq.join (Seq.map (map f) S))))
apply recOn s <;> simp
case h1.h2
α : Type u
β : Type v
γ : Type w
f : α → β
S✝ : Seq (Seq1 α)
s1 s2 : Seq β
h : ∃ s S, s1 = append s (Seq.map f (Seq.join S)) ∧ s2 = append s (Seq.join (Seq.map (map f) S))
s : Seq β
S : Seq (Seq1 α)
⊢ ∀ (x : Seq1 α) (s : Seq (Seq1 α)),
    match destruct (Seq.map f (Seq.join (Seq.cons x s))),
      destruct (Seq.join (Seq.cons (map f x) (Seq.map (map f) s))) with
    | none, none => True
    | some (a, s), some (a', s') =>
      a = a' ∧ ∃ s_1 S, s = append s_1 (Seq.map f (Seq.join S)) ∧ s' = append s_1 (Seq.join (Seq.map (map f) S))
    | x, x_1 => False
case h1
α : Type u
β : Type v
γ : Type w
f : α → β
S✝ : Seq (Seq1 α)
s1 s2 : Seq β
h : ∃ s S, s1 = append s (Seq.map f (Seq.join S)) ∧ s2 = append s (Seq.join (Seq.map (map f) S))
s : Seq β
S : Seq (Seq1 α)
⊢ match destruct (Seq.map f (Seq.join S)), destruct (Seq.join (Seq.map (map f) S)) with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧ ∃ s_1 S, s = append s_1 (Seq.map f (Seq.join S)) ∧ s' = append s_1 (Seq.join (Seq.map (map f) S))
  | x, x_1 => False
apply recOn S <;> simp
case h1.h2
α : Type u
β : Type v
γ : Type w
f : α → β
S✝¹ : Seq (Seq1 α)
s1 s2 : Seq β
h : ∃ s S, s1 = append s (Seq.map f (Seq.join S)) ∧ s2 = append s (Seq.join (Seq.map (map f) S))
s : Seq β
S✝ : Seq (Seq1 α)
x : Seq1 α
S : Seq (Seq1 α)
⊢ match destruct (Seq.map f (Seq.join (Seq.cons x S))),
    destruct (Seq.join (Seq.cons (map f x) (Seq.map (map f) S))) with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧ ∃ s_1 S, s = append s_1 (Seq.map f (Seq.join S)) ∧ s' = append s_1 (Seq.join (Seq.map (map f) S))
  | x, x_1 => False
case h1.h2
α : Type u
β : Type v
γ : Type w
f : α → β
S✝ : Seq (Seq1 α)
s1 s2 : Seq β
h : ∃ s S, s1 = append s (Seq.map f (Seq.join S)) ∧ s2 = append s (Seq.join (Seq.map (map f) S))
s : Seq β
S : Seq (Seq1 α)
⊢ ∀ (x : Seq1 α) (s : Seq (Seq1 α)),
    match destruct (Seq.map f (Seq.join (Seq.cons x s))),
      destruct (Seq.join (Seq.cons (map f x) (Seq.map (map f) s))) with
    | none, none => True
    | some (a, s), some (a', s') =>
      a = a' ∧ ∃ s_1 S, s = append s_1 (Seq.map f (Seq.join S)) ∧ s' = append s_1 (Seq.join (Seq.map (map f) S))
    | x, x_1 => False
intro x S
case h1.h2.mk
α : Type u
β : Type v
γ : Type w
f : α → β
S✝¹ : Seq (Seq1 α)
s1 s2 : Seq β
h : ∃ s S, s1 = append s (Seq.map f (Seq.join S)) ∧ s2 = append s (Seq.join (Seq.map (map f) S))
s✝ : Seq β
S✝ S : Seq (Seq1 α)
a : α
s : Seq α
⊢ match destruct (Seq.map f (Seq.join (Seq.cons (a, s) S))),
    destruct (Seq.join (Seq.cons (map f (a, s)) (Seq.map (map f) S))) with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧ ∃ s_1 S, s = append s_1 (Seq.map f (Seq.join S)) ∧ s' = append s_1 (Seq.join (Seq.map (map f) S))
  | x, x_1 => False
case h1.h2
α : Type u
β : Type v
γ : Type w
f : α → β
S✝¹ : Seq (Seq1 α)
s1 s2 : Seq β
h : ∃ s S, s1 = append s (Seq.map f (Seq.join S)) ∧ s2 = append s (Seq.join (Seq.map (map f) S))
s : Seq β
S✝ : Seq (Seq1 α)
x : Seq1 α
S : Seq (Seq1 α)
⊢ match destruct (Seq.map f (Seq.join (Seq.cons x S))),
    destruct (Seq.join (Seq.cons (map f x) (Seq.map (map f) S))) with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧ ∃ s_1 S, s = append s_1 (Seq.map f (Seq.join S)) ∧ s' = append s_1 (Seq.join (Seq.map (map f) S))
  | x, x_1 => False
cases' x with a s
case h1.h2.mk
α : Type u
β : Type v
γ : Type w
f : α → β
S✝¹ : Seq (Seq1 α)
s1 s2 : Seq β
h : ∃ s S, s1 = append s (Seq.map f (Seq.join S)) ∧ s2 = append s (Seq.join (Seq.map (map f) S))
s✝ : Seq β
S✝ S : Seq (Seq1 α)
a : α
s : Seq α
⊢ ∃ s_1 S_1,
    append (Seq.map f s) (Seq.map f (Seq.join S)) = append s_1 (Seq.map f (Seq.join S_1)) ∧
      append (Seq.map f s)
          (Seq.join
            (Seq.map
              (fun x =>
                match x with
                | (a, s) => (f a, Seq.map f s))
              S)) =
        append s_1
          (Seq.join
            (Seq.map
              (fun x =>
                match x with
                | (a, s) => (f a, Seq.map f s))
              S_1))
case h1.h2.mk
α : Type u
β : Type v
γ : Type w
f : α → β
S✝¹ : Seq (Seq1 α)
s1 s2 : Seq β
h : ∃ s S, s1 = append s (Seq.map f (Seq.join S)) ∧ s2 = append s (Seq.join (Seq.map (map f) S))
s✝ : Seq β
S✝ S : Seq (Seq1 α)
a : α
s : Seq α
⊢ match destruct (Seq.map f (Seq.join (Seq.cons (a, s) S))),
    destruct (Seq.join (Seq.cons (map f (a, s)) (Seq.map (map f) S))) with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧ ∃ s_1 S, s = append s_1 (Seq.map f (Seq.join S)) ∧ s' = append s_1 (Seq.join (Seq.map (map f) S))
  | x, x_1 => False
simp [map]
no goals
case h1.h2.mk
α : Type u
β : Type v
γ : Type w
f : α → β
S✝¹ : Seq (Seq1 α)
s1 s2 : Seq β
h : ∃ s S, s1 = append s (Seq.map f (Seq.join S)) ∧ s2 = append s (Seq.join (Seq.map (map f) S))
s✝ : Seq β
S✝ S : Seq (Seq1 α)
a : α
s : Seq α
⊢ ∃ s_1 S_1,
    append (Seq.map f s) (Seq.map f (Seq.join S)) = append s_1 (Seq.map f (Seq.join S_1)) ∧
      append (Seq.map f s)
          (Seq.join
            (Seq.map
              (fun x =>
                match x with
                | (a, s) => (f a, Seq.map f s))
              S)) =
        append s_1
          (Seq.join
            (Seq.map
              (fun x =>
                match x with
                | (a, s) => (f a, Seq.map f s))
              S_1))
exact ⟨_, _, rfl, rfl⟩
case h2
α : Type u
β : Type v
γ : Type w
f : α → β
S✝ : Seq (Seq1 α)
s1 s2 : Seq β
h : ∃ s S, s1 = append s (Seq.map f (Seq.join S)) ∧ s2 = append s (Seq.join (Seq.map (map f) S))
s✝ : Seq β
S : Seq (Seq1 α)
x✝ : β
s : Seq β
⊢ ∃ s_1 S_1,
    append s (Seq.map f (Seq.join S)) = append s_1 (Seq.map f (Seq.join S_1)) ∧
      append s (Seq.join (Seq.map (map f) S)) = append s_1 (Seq.join (Seq.map (map f) S_1))
case h2
α : Type u
β : Type v
γ : Type w
f : α → β
S✝ : Seq (Seq1 α)
s1 s2 : Seq β
h : ∃ s S, s1 = append s (Seq.map f (Seq.join S)) ∧ s2 = append s (Seq.join (Seq.map (map f) S))
s : Seq β
S : Seq (Seq1 α)
⊢ β →
    ∀ (s : Seq β),
      ∃ s_1 S_1,
        append s (Seq.map f (Seq.join S)) = append s_1 (Seq.map f (Seq.join S_1)) ∧
          append s (Seq.join (Seq.map (map f) S)) = append s_1 (Seq.join (Seq.map (map f) S_1))
intro _ s
no goals
case h2
α : Type u
β : Type v
γ : Type w
f : α → β
S✝ : Seq (Seq1 α)
s1 s2 : Seq β
h : ∃ s S, s1 = append s (Seq.map f (Seq.join S)) ∧ s2 = append s (Seq.join (Seq.map (map f) S))
s✝ : Seq β
S : Seq (Seq1 α)
x✝ : β
s : Seq β
⊢ ∃ s_1 S_1,
    append s (Seq.map f (Seq.join S)) = append s_1 (Seq.map f (Seq.join S_1)) ∧
      append s (Seq.join (Seq.map (map f) S)) = append s_1 (Seq.join (Seq.map (map f) S_1))
refine' ⟨s, S, rfl, rfl⟩
no goals
case r
α : Type u
β : Type v
γ : Type w
f : α → β
S : Seq (Seq1 α)
⊢ ∃ s S_1,
    Seq.map f (Seq.join S) = append s (Seq.map f (Seq.join S_1)) ∧
      Seq.join (Seq.map (map f) S) = append s (Seq.join (Seq.map (map f) S_1))
refine' ⟨nil, S, _, _⟩ <;> simp