-- Mathlib/Data/Seq/Seq.lean
theorem join_join (SS : Seq (Seq1 (Seq1 α))) :
    Seq.join (Seq.join SS) = Seq.join (Seq.map join SS)

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

Tactic:
obtain ⟨x, s⟩ := s

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

Proof state:
α : Type u
SS : Seq (Seq1 (Seq1 α))
⊢ SS.join.join = (Seq.map join SS).join

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

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

case r
α : Type u
SS : Seq (Seq1 (Seq1 α))
⊢ ∃ s SS_1, SS.join.join = s.append SS_1.join.join ∧ (Seq.map join SS).join = s.append (Seq.map join SS_1).join

Proof state:
α : Type u
SS✝ : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ s SS, s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x✝ x : α
s : Seq α
⊢ ∃ s_1 SS_1,
    Seq.cons x (s.append (S.join.append SS.join.join)) = s_1.append SS_1.join.join ∧
      Seq.cons x (s.append (S.join.append (Seq.map join SS).join)) = s_1.append (Seq.map join SS_1).join

Tactic:
refine ⟨Seq.cons x (append s (Seq.join S)), SS, ?_, ?_⟩ <;> simp

Result:
no goals

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

Tactic:
cases SS <;> simp

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

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

Tactic:
obtain ⟨s, S⟩ := S

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

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

Tactic:
cases s <;> simp

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

case cons
α : Type u
SS✝ : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ s SS, s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
x✝ : α
s✝ : Seq α
⊢ ∃ s SS_1,
    s✝.append SS.join.join = s.append SS_1.join.join ∧
      s✝.append (Seq.map join SS).join = s.append (Seq.map join SS_1).join

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

Tactic:
cases s <;> simp

Result:
case mk.mk.nil
α : Type u
SS✝ : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ s SS, s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x : α
⊢ ∃ s SS_1,
    S.join.append SS.join.join = s.append SS_1.join.join ∧
      S.join.append (Seq.map join SS).join = s.append (Seq.map join SS_1).join

case mk.mk.cons
α : Type u
SS✝ : Seq (Seq1 (Seq1 α))
s1 s2 : Seq α
h : ∃ s SS, s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x x✝ : α
s✝ : Seq α
⊢ ∃ s SS_1,
    Seq.cons x✝ (s✝.append (S.join.append SS.join.join)) = s.append SS_1.join.join ∧
      Seq.cons x✝ (s✝.append (S.join.append (Seq.map join SS).join)) = s.append (Seq.map join SS_1).join