-- Mathlib/Data/Seq/Seq.lean
theorem join_append (S T : Seq (Seq1 α)) : join (append S T) = append (join S) (join T)

Proof state:
case cons.mk
α : Type u
S T✝ : Seq (Seq1 α)
s1 s2 : Seq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : Seq (Seq1 α)
a : α
s : Seq α
⊢ ∃ s_1 S T_1, s.append T.join = s_1.append (S.append T_1).join ∧ s.append T.join = s_1.append (S.join.append T_1.join)

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

Result:
no goals

Proof state:
α : Type u
S T : Seq (Seq1 α)
⊢ (S.append T).join = S.join.append T.join

Tactic:
apply
  eq_of_bisim fun s1 s2 =>
    ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))

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

case r
α : Type u
S T : Seq (Seq1 α)
⊢ ∃ s S_1 T_1,
    (S.append T).join = s.append (S_1.append T_1).join ∧ S.join.append T.join = s.append (S_1.join.append T_1.join)

Proof state:
α : Type u
S✝ T✝ : Seq (Seq1 α)
s1 s2 : Seq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
S T : Seq (Seq1 α)
x✝ : α
s : Seq α
⊢ ∃ s_1 S_1 T_1,
    s.append (S.append T).join = s_1.append (S_1.append T_1).join ∧
      s.append (S.join.append T.join) = s_1.append (S_1.join.append T_1.join)

Tactic:
exact ⟨s, S, T, rfl, rfl⟩

Result:
no goals

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

Tactic:
obtain ⟨a, s⟩ := s

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

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

Tactic:
cases T with
| nil => simp
| cons s T =>
  obtain ⟨a, s⟩ := s; simp only [join_cons, destruct_cons, true_and]
  refine ⟨s, nil, T, ?_, ?_⟩ <;> simp

Result:
no goals

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

Tactic:
simp

Result:
no goals

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

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

Tactic:
case nil =>
  cases T with
  | nil => simp
  | cons s T =>
    obtain ⟨a, s⟩ := s; simp only [join_cons, destruct_cons, true_and]
    refine ⟨s, nil, T, ?_, ?_⟩ <;> simp

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

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

Tactic:
simp only [join_cons, destruct_cons, true_and]

Result:
case cons.mk
α : Type u
S T✝ : Seq (Seq1 α)
s1 s2 : Seq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : Seq (Seq1 α)
a : α
s : Seq α
⊢ ∃ s_1 S T_1, s.append T.join = s_1.append (S.append T_1).join ∧ s.append T.join = s_1.append (S.join.append T_1.join)

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

Tactic:
obtain ⟨a, s⟩ := s

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

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

Tactic:
cases s <;> simp

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

case cons
α : Type u
S✝ T✝ : Seq (Seq1 α)
s1 s2 : Seq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
S T : Seq (Seq1 α)
x✝ : α
s✝ : Seq α
⊢ ∃ s S_1 T_1,
    s✝.append (S.append T).join = s.append (S_1.append T_1).join ∧
      s✝.append (S.join.append T.join) = s.append (S_1.join.append T_1.join)