Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case none.none
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ 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

pp: case none.some
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ 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

pp: case some.none
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ 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

pp: case some.some
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ 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:
· apply Computation.mem_map _ dtm

Goal state after:
case none.some
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ 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 some.none
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ 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 some.some
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ 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