-- Mathlib/Data/Seq/WSeq.lean
theorem head_congr : ∀ {s t : WSeq α}, s ~ʷ t → head s ~ head t

Proof state:
case intro.intro.intro.intro.intro.some.some.mk
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b, b ∈ t.destruct ∧ BisimO (fun x1 x2 => x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a, a ∈ s.destruct ∧ BisimO (fun x1 x2 => x1 ~ʷ x2) a b
b : α × WSeq α
dtm : some b ∈ t.destruct
a : α
s' : WSeq α
dsm : some (a, s') ∈ s.destruct
dse : Prod.fst <$> some (a, s') = o
dst : BisimO (fun x1 x2 => x1 ~ʷ x2) (some (a, s')) (some b)
⊢ Prod.fst <$> some (a, s') ∈ t.head

Tactic:
obtain ⟨b, t'⟩ := b

Result:
case intro.intro.intro.intro.intro.some.some.mk.mk
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b, b ∈ t.destruct ∧ BisimO (fun x1 x2 => x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a, a ∈ s.destruct ∧ BisimO (fun x1 x2 => x1 ~ʷ x2) a b
a : α
s' : WSeq α
dsm : some (a, s') ∈ s.destruct
dse : Prod.fst <$> some (a, s') = o
b : α
t' : WSeq α
dtm : some (b, t') ∈ t.destruct
dst : BisimO (fun x1 x2 => x1 ~ʷ x2) (some (a, s')) (some (b, t'))
⊢ Prod.fst <$> some (a, s') ∈ t.head

Proof state:
case intro.intro.intro.intro.intro.some.none
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b, b ∈ t.destruct ∧ BisimO (fun x1 x2 => x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a, a ∈ s.destruct ∧ BisimO (fun x1 x2 => x1 ~ʷ x2) a b
a : α × WSeq α
dsm : some a ∈ s.destruct
dse : Prod.fst <$> some a = o
dtm : none ∈ t.destruct
dst : BisimO (fun x1 x2 => x1 ~ʷ x2) (some a) none
⊢ Prod.fst <$> some a ∈ t.head

Tactic:
cases a

Result:
case intro.intro.intro.intro.intro.some.none.mk
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b, b ∈ t.destruct ∧ BisimO (fun x1 x2 => x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a, a ∈ s.destruct ∧ BisimO (fun x1 x2 => x1 ~ʷ x2) a b
dtm : none ∈ t.destruct
fst✝ : α
snd✝ : WSeq α
dsm : some (fst✝, snd✝) ∈ s.destruct
dse : Prod.fst <$> some (fst✝, snd✝) = o
dst : BisimO (fun x1 x2 => x1 ~ʷ x2) (some (fst✝, snd✝)) none
⊢ Prod.fst <$> some (fst✝, snd✝) ∈ t.head

Proof state:
case intro.intro.intro.intro.intro.none.none
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b, b ∈ t.destruct ∧ BisimO (fun x1 x2 => x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a, a ∈ s.destruct ∧ BisimO (fun x1 x2 => x1 ~ʷ x2) a b
dsm : none ∈ s.destruct
dse : Prod.fst <$> none = o
dtm : none ∈ t.destruct
dst : BisimO (fun x1 x2 => x1 ~ʷ x2) none none
⊢ Prod.fst <$> none ∈ t.head

Tactic:
apply Computation.mem_map _ dtm

Result:
no goals

Proof state:
α : Type u
⊢ ∀ {s t : WSeq α}, s ~ʷ t → ∀ {o : Option α}, o ∈ s.head → o ∈ t.head

Tactic:
intro s t h o ho

Result:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
⊢ o ∈ t.head

Proof state:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
⊢ o ∈ t.head

Tactic:
rcases @Computation.exists_of_mem_map _ _ _ _ (destruct s) ho with ⟨ds, dsm, dse⟩

Result:
case intro.intro
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
ds : Option (α × WSeq α)
dsm : ds ∈ s.destruct
dse : Prod.fst <$> ds = o
⊢ o ∈ t.head

Proof state:
case intro.intro.intro
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
ds : Option (α × WSeq α)
dsm : ds ∈ s.destruct
dse : Prod.fst <$> ds = o
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b, b ∈ t.destruct ∧ BisimO (fun x1 x2 => x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a, a ∈ s.destruct ∧ BisimO (fun x1 x2 => x1 ~ʷ x2) a b
⊢ Prod.fst <$> ds ∈ t.head

Tactic:
rcases l dsm with ⟨dt, dtm, dst⟩

Result:
case intro.intro.intro.intro.intro
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
ds : Option (α × WSeq α)
dsm : ds ∈ s.destruct
dse : Prod.fst <$> ds = o
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b, b ∈ t.destruct ∧ BisimO (fun x1 x2 => x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a, a ∈ s.destruct ∧ BisimO (fun x1 x2 => x1 ~ʷ x2) a b
dt : Option (α × WSeq α)
dtm : dt ∈ t.destruct
dst : BisimO (fun x1 x2 => x1 ~ʷ x2) ds dt
⊢ Prod.fst <$> ds ∈ t.head

Proof state:
case intro.intro.intro.intro.intro.some.none.mk
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b, b ∈ t.destruct ∧ BisimO (fun x1 x2 => x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a, a ∈ s.destruct ∧ BisimO (fun x1 x2 => x1 ~ʷ x2) a b
dtm : none ∈ t.destruct
fst✝ : α
snd✝ : WSeq α
dsm : some (fst✝, snd✝) ∈ s.destruct
dse : Prod.fst <$> some (fst✝, snd✝) = o
dst : BisimO (fun x1 x2 => x1 ~ʷ x2) (some (fst✝, snd✝)) none
⊢ Prod.fst <$> some (fst✝, snd✝) ∈ t.head

Tactic:
cases dst

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.none.some
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b, b ∈ t.destruct ∧ BisimO (fun x1 x2 => x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a, a ∈ s.destruct ∧ BisimO (fun x1 x2 => x1 ~ʷ x2) a b
dsm : none ∈ s.destruct
dse : Prod.fst <$> none = o
b : α × WSeq α
dtm : some b ∈ t.destruct
dst : BisimO (fun x1 x2 => x1 ~ʷ x2) none (some b)
⊢ Prod.fst <$> none ∈ t.head

Tactic:
cases b

Result:
case intro.intro.intro.intro.intro.none.some.mk
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b, b ∈ t.destruct ∧ BisimO (fun x1 x2 => x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a, a ∈ s.destruct ∧ BisimO (fun x1 x2 => x1 ~ʷ x2) a b
dsm : none ∈ s.destruct
dse : Prod.fst <$> none = o
fst✝ : α
snd✝ : WSeq α
dtm : some (fst✝, snd✝) ∈ t.destruct
dst : BisimO (fun x1 x2 => x1 ~ʷ x2) none (some (fst✝, snd✝))
⊢ Prod.fst <$> none ∈ t.head

Proof state:
case intro.intro.intro.intro.intro.none.some.mk
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b, b ∈ t.destruct ∧ BisimO (fun x1 x2 => x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a, a ∈ s.destruct ∧ BisimO (fun x1 x2 => x1 ~ʷ x2) a b
dsm : none ∈ s.destruct
dse : Prod.fst <$> none = o
fst✝ : α
snd✝ : WSeq α
dtm : some (fst✝, snd✝) ∈ t.destruct
dst : BisimO (fun x1 x2 => x1 ~ʷ x2) none (some (fst✝, snd✝))
⊢ Prod.fst <$> none ∈ t.head

Tactic:
cases dst

Result:
no goals