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

Proof state:
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
⊢ Prod.fst <$> ds ∈ t.head

Tactic:
obtain ⟨l, r⟩ := destruct_congr h

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

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

Tactic:
rcases ds with - | a <;> rcases dt with - | b

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

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

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

case intro.intro.intro.intro.intro.some.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
a : α × WSeq α
dsm : some a ∈ s.destruct
dse : Prod.fst <$> some a = o
b : α × WSeq α
dtm : some b ∈ t.destruct
dst : BisimO (fun x1 x2 => x1 ~ʷ x2) (some a) (some b)
⊢ Prod.fst <$> some a ∈ t.head

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

Tactic:
suffices ∀ {s t : WSeq α}, s ~ʷ t → ∀ {o}, o ∈ head s → o ∈ head t from fun s t h o =>
  ⟨this h, this h.symm⟩

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

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

Tactic:
rw [dst.left]

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 (b, s') ∈ t.head

Proof state:
case intro.intro.intro.intro.intro.some.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
a : α × WSeq α
dsm : some a ∈ s.destruct
dse : Prod.fst <$> some a = o
b : α × WSeq α
dtm : some b ∈ t.destruct
dst : BisimO (fun x1 x2 => x1 ~ʷ x2) (some a) (some b)
⊢ Prod.fst <$> some a ∈ t.head

Tactic:
obtain ⟨a, s'⟩ := a

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

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

Tactic:
rw [← 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
⊢ Prod.fst <$> ds ∈ t.head

Proof state:
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 (b, s') ∈ t.head

Tactic:
exact @Computation.mem_map _ _ (@Functor.map _ _ (α × WSeq α) _ Prod.fst)
  (some (b, t')) (destruct t) dtm

Result:
no goals