-- Mathlib/Data/Seq/Seq.lean
theorem map_append (f : α → β) (s t) : map f (append s t) = append (map f s) (map f t)

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

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

Result:
no goals

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

Tactic:
cases t <;> simp

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

Proof state:
α : Type u
β : Type v
f : α → β
s t : Seq α
⊢ map f (s.append t) = (map f s).append (map f t)

Tactic:
apply
  eq_of_bisim (fun s1 s2 => ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)) _
    ⟨s, t, rfl, rfl⟩

Result:
α : Type u
β : Type v
f : α → β
s t : Seq α
⊢ IsBisimulation fun s1 s2 => ∃ s t, s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)

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

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

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

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

Proof state:
α : Type u
β : Type v
f : α → β
s t : Seq α
⊢ IsBisimulation fun s1 s2 => ∃ s t, s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)

Tactic:
intro s1 s2 h

Result:
α : Type u
β : Type v
f : α → β
s t : Seq α
s1 s2 : Seq β
h : ∃ s t, s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)
⊢ BisimO (fun s1 s2 => ∃ s t, s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)) s1.destruct s2.destruct

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

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

Result:
no goals

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

Tactic:
cases s <;> simp

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

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

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

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

Result:
no goals

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

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

Result:
no goals

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

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

Result:
no goals