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

Tactic:
intro s1 s2 h

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

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

Tactic:
exact
  match s1, s2, h with
  | _, _, ⟨s, SS, rfl, rfl⟩ => by
    cases s <;> simp
    case nil =>
      cases SS <;> simp
      case cons S SS =>
        obtain ⟨s, S⟩ := S; obtain ⟨x, s⟩ := s
        simp only [Seq.join_cons, join_append, destruct_cons]
        cases s <;> simp
        case nil => exact ⟨_, _, rfl, rfl⟩
        case cons x s => refine ⟨Seq.cons x (append s (Seq.join S)), SS, ?_, ?_⟩ <;> simp
    case cons _ s => exact ⟨s, SS, rfl, rfl⟩

Result:
no goals

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

Tactic:
simp only [Seq.join_cons, join_append, destruct_cons]

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

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

Tactic:
refine ⟨nil, 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 α))
x✝ : α
s : Seq α
⊢ ∃ s_1 SS_1,
    s.append SS.join.join = s_1.append SS_1.join.join ∧
      s.append (Seq.map join SS).join = s_1.append (Seq.map join SS_1).join

Tactic:
exact ⟨s, SS, rfl, rfl⟩

Result:
no goals

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

Tactic:
case nil => exact ⟨_, _, rfl, rfl⟩

Result:
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

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

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

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

Tactic:
exact ⟨_, _, rfl, rfl⟩

Result:
no goals

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

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

Result:
no goals

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

Tactic:
case nil =>
  cases SS <;> simp
  case cons S SS =>
    obtain ⟨s, S⟩ := S; obtain ⟨x, s⟩ := s
    simp only [Seq.join_cons, join_append, destruct_cons]
    cases s <;> simp
    case nil => exact ⟨_, _, rfl, rfl⟩
    case cons x s => refine ⟨Seq.cons x (append s (Seq.join S)), 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
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 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

Tactic:
case cons S SS =>
  obtain ⟨s, S⟩ := S; obtain ⟨x, s⟩ := s
  simp only [Seq.join_cons, join_append, destruct_cons]
  cases s <;> simp
  case nil => exact ⟨_, _, rfl, rfl⟩
  case cons x s => refine ⟨Seq.cons x (append s (Seq.join S)), SS, ?_, ?_⟩ <;> simp

Result:
no goals