-- Mathlib/Data/Seq/Seq.lean
theorem append_assoc (s t u : Seq α) : append (append s t) u = append s (append t u)

Proof state:
α : Type u
s t u : Seq α
⊢ (s.append t).append u = s.append (t.append u)

Tactic:
apply eq_of_bisim fun s1 s2 => ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u)

Result:
case bisim
α : Type u
s t u : Seq α
⊢ IsBisimulation fun s1 s2 => ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)

case r
α : Type u
s t u : Seq α
⊢ ∃ s_1 t_1 u_1,
    (s.append t).append u = (s_1.append t_1).append u_1 ∧ s.append (t.append u) = s_1.append (t_1.append u_1)

Proof state:
case cons
α : Type u
s t✝ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
t u : Seq α
x✝ : α
s✝ : Seq α
⊢ ∃ s t_1 u_1, (s✝.append t).append u = (s.append t_1).append u_1 ∧ s✝.append (t.append u) = s.append (t_1.append u_1)

Tactic:
case cons _ s => exact ⟨s, t, u, rfl, rfl⟩

Result:
no goals

Proof state:
case bisim
α : Type u
s t u s1 s2 : Seq α
h : ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
⊢ BisimO (fun s1 s2 => ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)) s1.destruct s2.destruct

Tactic:
exact
  match s1, s2, h with
  | _, _, ⟨s, t, u, rfl, rfl⟩ => by
    cases s <;> simp
    case nil =>
      cases t <;> simp
      case nil =>
        cases u <;> simp
        case cons _ u => refine ⟨nil, nil, u, ?_, ?_⟩ <;> simp
      case cons _ t => refine ⟨nil, t, u, ?_, ?_⟩ <;> simp
    case cons _ s => exact ⟨s, t, u, rfl, rfl⟩

Result:
no goals

Proof state:
case nil
α : Type u
s t✝ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
t u : Seq α
⊢ match (t.append u).destruct, (t.append u).destruct with
  | none, none => True
  | some (a, s), some (a', s') => a = a' ∧ ∃ s_1 t u, s = (s_1.append t).append u ∧ s' = s_1.append (t.append u)
  | x, x_1 => False

case cons
α : Type u
s t✝ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
t u : Seq α
x✝ : α
s✝ : Seq α
⊢ ∃ s t_1 u_1, (s✝.append t).append u = (s.append t_1).append u_1 ∧ s✝.append (t.append u) = s.append (t_1.append u_1)

Tactic:
case nil =>
  cases t <;> simp
  case nil =>
    cases u <;> simp
    case cons _ u => refine ⟨nil, nil, u, ?_, ?_⟩ <;> simp
  case cons _ t => refine ⟨nil, t, u, ?_, ?_⟩ <;> simp

Result:
case cons
α : Type u
s t✝ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
t u : Seq α
x✝ : α
s✝ : Seq α
⊢ ∃ s t_1 u_1, (s✝.append t).append u = (s.append t_1).append u_1 ∧ s✝.append (t.append u) = s.append (t_1.append u_1)

Proof state:
α : Type u
s t u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
u : Seq α
⊢ match u.destruct, u.destruct with
  | none, none => True
  | some (a, s), some (a', s') => a = a' ∧ ∃ s_1 t u, s = (s_1.append t).append u ∧ s' = s_1.append (t.append u)
  | x, x_1 => False

Tactic:
cases u <;> simp

Result:
case cons
α : Type u
s t u s1 s2 : Seq α
h : ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
x✝ : α
s✝ : Seq α
⊢ ∃ s t u, s✝ = (s.append t).append u ∧ s✝ = s.append (t.append u)

Proof state:
case r
α : Type u
s t u : Seq α
⊢ ∃ s_1 t_1 u_1,
    (s.append t).append u = (s_1.append t_1).append u_1 ∧ s.append (t.append u) = s_1.append (t_1.append u_1)

Tactic:
exact ⟨s, t, u, rfl, rfl⟩

Result:
no goals

Proof state:
α : Type u
s✝ t✝ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
t u : Seq α
x✝ : α
s : Seq α
⊢ ∃ s_1 t_1 u_1,
    (s.append t).append u = (s_1.append t_1).append u_1 ∧ s.append (t.append u) = s_1.append (t_1.append u_1)

Tactic:
exact ⟨s, t, u, rfl, rfl⟩

Result:
no goals

Proof state:
α : Type u
s t✝ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
t u : Seq α
⊢ match (t.append u).destruct, (t.append u).destruct with
  | none, none => True
  | some (a, s), some (a', s') => a = a' ∧ ∃ s_1 t u, s = (s_1.append t).append u ∧ s' = s_1.append (t.append u)
  | x, x_1 => False

Tactic:
cases t <;> simp

Result:
case nil
α : Type u
s t u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
u : Seq α
⊢ match u.destruct, u.destruct with
  | none, none => True
  | some (a, s), some (a', s') => a = a' ∧ ∃ s_1 t u, s = (s_1.append t).append u ∧ s' = s_1.append (t.append u)
  | x, x_1 => False

case cons
α : Type u
s t u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
u : Seq α
x✝ : α
s✝ : Seq α
⊢ ∃ s t u_1, s✝.append u = (s.append t).append u_1 ∧ s✝.append u = s.append (t.append u_1)

Proof state:
case cons
α : Type u
s t u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
u : Seq α
x✝ : α
s✝ : Seq α
⊢ ∃ s t u_1, s✝.append u = (s.append t).append u_1 ∧ s✝.append u = s.append (t.append u_1)

Tactic:
case cons _ t => refine ⟨nil, t, u, ?_, ?_⟩ <;> simp

Result:
no goals

Proof state:
case nil
α : Type u
s t u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
u : Seq α
⊢ match u.destruct, u.destruct with
  | none, none => True
  | some (a, s), some (a', s') => a = a' ∧ ∃ s_1 t u, s = (s_1.append t).append u ∧ s' = s_1.append (t.append u)
  | x, x_1 => False

case cons
α : Type u
s t u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
u : Seq α
x✝ : α
s✝ : Seq α
⊢ ∃ s t u_1, s✝.append u = (s.append t).append u_1 ∧ s✝.append u = s.append (t.append u_1)

Tactic:
case nil =>
  cases u <;> simp
  case cons _ u => refine ⟨nil, nil, u, ?_, ?_⟩ <;> simp

Result:
case cons
α : Type u
s t u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
u : Seq α
x✝ : α
s✝ : Seq α
⊢ ∃ s t u_1, s✝.append u = (s.append t).append u_1 ∧ s✝.append u = s.append (t.append u_1)

Proof state:
α : Type u
s t✝ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
u : Seq α
x✝ : α
t : Seq α
⊢ ∃ s t_1 u_1, t.append u = (s.append t_1).append u_1 ∧ t.append u = s.append (t_1.append u_1)

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

Result:
no goals

Proof state:
α : Type u
s✝ t✝ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
s t u : Seq α
⊢ BisimO (fun s1 s2 => ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u))
    ((s.append t).append u).destruct (s.append (t.append u)).destruct

Tactic:
cases s <;> simp

Result:
case nil
α : Type u
s t✝ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
t u : Seq α
⊢ match (t.append u).destruct, (t.append u).destruct with
  | none, none => True
  | some (a, s), some (a', s') => a = a' ∧ ∃ s_1 t u, s = (s_1.append t).append u ∧ s' = s_1.append (t.append u)
  | x, x_1 => False

case cons
α : Type u
s t✝ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
t u : Seq α
x✝ : α
s✝ : Seq α
⊢ ∃ s t_1 u_1, (s✝.append t).append u = (s.append t_1).append u_1 ∧ s✝.append (t.append u) = s.append (t_1.append u_1)

Proof state:
case bisim
α : Type u
s t u : Seq α
⊢ IsBisimulation fun s1 s2 => ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)

Tactic:
intro s1 s2 h

Result:
case bisim
α : Type u
s t u s1 s2 : Seq α
h : ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
⊢ BisimO (fun s1 s2 => ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)) s1.destruct s2.destruct

Proof state:
α : Type u
s t u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
x✝ : α
u : Seq α
⊢ ∃ s t u_1, u = (s.append t).append u_1 ∧ u = s.append (t.append u_1)

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

Result:
no goals