case mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ bind (bind (a, s) f) g = bind (a, s) fun x => bind (f x) g
α : Type u
β : Type v
γ : Type w
s : Seq1 α
f : α → Seq1 β
g : β → Seq1 γ
⊢ bind (bind s f) g = bind s fun x => bind (f x) g
cases' s with a s
case mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ join (join (map g (f a), Seq.map (map g) (Seq.map f s))) =
    join (join (map g (f a)), Seq.map (fun x => join (map g (f x))) s)
case mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ bind (bind (a, s) f) g = bind (a, s) fun x => bind (f x) g
simp only [bind, map_pair, map_join]
case mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ join (join (map g (f a), Seq.map (map g ∘ f) s)) = join (join (map g (f a)), Seq.map (fun x => join (map g (f x))) s)
case mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ join (join (map g (f a), Seq.map (map g) (Seq.map f s))) =
    join (join (map g (f a)), Seq.map (fun x => join (map g (f x))) s)
rw [← map_comp]
case mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ join (join (map g (f a), Seq.map (map g ∘ f) s)) = join (join (map g (f a)), Seq.map (join ∘ map g ∘ f) s)
case mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ join (join (map g (f a), Seq.map (map g ∘ f) s)) = join (join (map g (f a)), Seq.map (fun x => join (map g (f x))) s)
simp only [show (fun x => join (map g (f x))) = join ∘ (map g ∘ f) from rfl]
case mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ join (join (map g (f a), Seq.map (map g ∘ f) s)) = join (join (map g (f a)), Seq.map join (Seq.map (map g ∘ f) s))
case mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ join (join (map g (f a), Seq.map (map g ∘ f) s)) = join (join (map g (f a)), Seq.map (join ∘ map g ∘ f) s)
rw [map_comp _ join]
case mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
⊢ join (join (map g (f a), SS)) = join (join (map g (f a)), Seq.map join SS)
case mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ join (join (map g (f a), Seq.map (map g ∘ f) s)) = join (join (map g (f a)), Seq.map join (Seq.map (map g ∘ f) s))
generalize Seq.map (map g ∘ f) s = SS
case mk.mk.mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s✝ : Seq α
SS : Seq (Seq1 (Seq1 γ))
S : Seq (Seq1 γ)
a : γ
s : Seq γ
⊢ join (join (((a, s), S), SS)) = join (join ((a, s), S), Seq.map join SS)
case mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
⊢ join (join (map g (f a), SS)) = join (join (map g (f a)), Seq.map join SS)
rcases map g (f a) with ⟨⟨a, s⟩, S⟩
case mk.mk.mk.h1.h2
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a : γ
x_1 : Seq1 γ
s_2 : Seq (Seq1 γ)
⊢ (a, Seq.join (Seq.cons x_1 (append s_2 (Seq.join SS)))) = join ((a, Seq.join (Seq.cons x_1 s_2)), Seq.map join SS)

case mk.mk.mk.h2.h2
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a x : γ
s_1 : Seq γ
x_1 : Seq1 γ
s_2 : Seq (Seq1 γ)
⊢ (a, Seq.cons x (append s_1 (Seq.join (Seq.cons x_1 (append s_2 (Seq.join SS)))))) =
    (a, Seq.cons x (append s_1 (append (Seq.join (Seq.cons x_1 s_2)) (Seq.join (Seq.map join SS)))))
case mk.mk.mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s✝ : Seq α
SS : Seq (Seq1 (Seq1 γ))
S : Seq (Seq1 γ)
a : γ
s : Seq γ
⊢ join (join (((a, s), S), SS)) = join (join ((a, s), S), Seq.map join SS)
induction' s using recOn with x s_1 <;> induction' S using recOn with x_1 s_2 <;> simp
case mk.mk.mk.h1.h2.mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a : γ
s_2 : Seq (Seq1 γ)
x : γ
t : Seq γ
⊢ (a, Seq.join (Seq.cons (x, t) (append s_2 (Seq.join SS)))) =
    join ((a, Seq.join (Seq.cons (x, t) s_2)), Seq.map join SS)
case mk.mk.mk.h1.h2
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a : γ
x_1 : Seq1 γ
s_2 : Seq (Seq1 γ)
⊢ (a, Seq.join (Seq.cons x_1 (append s_2 (Seq.join SS)))) = join ((a, Seq.join (Seq.cons x_1 s_2)), Seq.map join SS)
cases' x_1 with x t
no goals
case mk.mk.mk.h1.h2.mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a : γ
s_2 : Seq (Seq1 γ)
x : γ
t : Seq γ
⊢ (a, Seq.join (Seq.cons (x, t) (append s_2 (Seq.join SS)))) =
    join ((a, Seq.join (Seq.cons (x, t) s_2)), Seq.map join SS)
apply recOn t <;> intros <;> simp
case mk.mk.mk.h2.h2.mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a x : γ
s_1 : Seq γ
s_2 : Seq (Seq1 γ)
y : γ
t : Seq γ
⊢ (a, Seq.cons x (append s_1 (Seq.join (Seq.cons (y, t) (append s_2 (Seq.join SS)))))) =
    (a, Seq.cons x (append s_1 (append (Seq.join (Seq.cons (y, t) s_2)) (Seq.join (Seq.map join SS)))))
case mk.mk.mk.h2.h2
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a x : γ
s_1 : Seq γ
x_1 : Seq1 γ
s_2 : Seq (Seq1 γ)
⊢ (a, Seq.cons x (append s_1 (Seq.join (Seq.cons x_1 (append s_2 (Seq.join SS)))))) =
    (a, Seq.cons x (append s_1 (append (Seq.join (Seq.cons x_1 s_2)) (Seq.join (Seq.map join SS)))))
cases' x_1 with y t
no goals
case mk.mk.mk.h2.h2.mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a x : γ
s_1 : Seq γ
s_2 : Seq (Seq1 γ)
y : γ
t : Seq γ
⊢ (a, Seq.cons x (append s_1 (Seq.join (Seq.cons (y, t) (append s_2 (Seq.join SS)))))) =
    (a, Seq.cons x (append s_1 (append (Seq.join (Seq.cons (y, t) s_2)) (Seq.join (Seq.map join SS)))))
simp