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

Proof state:
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)

Tactic:
intro s1 s2 h

Result:
case bisim
α : 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)
⊢ BisimO (fun s1 s2 => ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)) s1.destruct
    s2.destruct

Proof state:
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)

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

Result:
no goals

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 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)

Tactic:
case cons _ s => exact ⟨s, S, T, rfl, rfl⟩

Result:
no goals

Proof state:
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

Tactic:
simpa using ⟨s, S, T, rfl, rfl⟩

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)
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)

Tactic:
case nil =>
  cases S <;> simp
  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
  case cons s S =>
    obtain ⟨a, s⟩ := s
    simpa using ⟨s, S, T, rfl, rfl⟩

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)
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)

Proof state:
case bisim
α : 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)
⊢ BisimO (fun s1 s2 => ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)) s1.destruct
    s2.destruct

Tactic:
exact
  match s1, s2, h with
  | _, _, ⟨s, S, T, rfl, rfl⟩ => by
    cases s <;> simp
    case nil =>
      cases S <;> simp
      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
      case cons s S =>
        obtain ⟨a, s⟩ := s
        simpa using ⟨s, S, T, rfl, rfl⟩
    case cons _ s => 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)
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

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)
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

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)
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 cons s S =>
  obtain ⟨a, s⟩ := s
  simpa using ⟨s, S, T, rfl, rfl⟩

Result:
no goals