-- Mathlib/Data/Seq/Seq.lean
theorem bind_assoc (s : Seq1 α) (f : α → Seq1 β) (g : β → Seq1 γ) :
    bind (bind s f) g = bind s fun x : α => bind (f x) g

Proof state:
case mk.mk.mk.cons.cons.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 (s_1.append (Seq.cons (y, t) (s_2.append SS.join)).join)) =
    (a, Seq.cons x (s_1.append ((Seq.cons (y, t) s_2).join.append (Seq.map join SS).join)))

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ (join (map g (f a), Seq.map (map g ∘ f) s)).join = join ((map g (f a)).join, Seq.map join (Seq.map (map g ∘ f) s))

Tactic:
generalize Seq.map (map g ∘ f) s = SS

Result:
case mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
⊢ (join (map g (f a), SS)).join = join ((map g (f a)).join, Seq.map join SS)

Proof state:
case mk.mk.mk.nil.cons.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.cons (x, t) (s_2.append SS.join)).join) = join ((a, (Seq.cons (x, t) s_2).join), Seq.map join SS)

Tactic:
cases t <;> simp

Result:
no goals

Proof state:
case mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ (join (map g (f a), Seq.map (map g ∘ f) s)).join = join ((map g (f a)).join, Seq.map (fun x => (map g (f x)).join) s)

Tactic:
simp only [show (fun x => join (map g (f x))) = join ∘ (map g ∘ f) from rfl]

Result:
case mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ (join (map g (f a), Seq.map (map g ∘ f) s)).join = join ((map g (f a)).join, Seq.map (join ∘ map g ∘ f) s)

Proof state:
case mk.mk.mk.cons.cons
α : 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 (s_1.append (Seq.cons x_1 (s_2.append SS.join)).join)) =
    (a, Seq.cons x (s_1.append ((Seq.cons x_1 s_2).join.append (Seq.map join SS).join)))

Tactic:
obtain ⟨y, t⟩ := x_1

Result:
case mk.mk.mk.cons.cons.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 (s_1.append (Seq.cons (y, t) (s_2.append SS.join)).join)) =
    (a, Seq.cons x (s_1.append ((Seq.cons (y, t) s_2).join.append (Seq.map join SS).join)))

Proof state:
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 (((a, s), S), SS)).join = join (join ((a, s), S), Seq.map join SS)

Tactic:
induction' s using recOn with x s_1 <;> induction' S using recOn with x_1 s_2 <;> simp

Result:
case mk.mk.mk.nil.cons
α : 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.cons x_1 (s_2.append SS.join)).join) = join ((a, (Seq.cons x_1 s_2).join), Seq.map join SS)

case mk.mk.mk.cons.cons
α : 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 (s_1.append (Seq.cons x_1 (s_2.append SS.join)).join)) =
    (a, Seq.cons x (s_1.append ((Seq.cons x_1 s_2).join.append (Seq.map join SS).join)))

Proof state:
case mk.mk.mk.nil.cons
α : 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.cons x_1 (s_2.append SS.join)).join) = join ((a, (Seq.cons x_1 s_2).join), Seq.map join SS)

Tactic:
obtain ⟨x, t⟩ := x_1

Result:
case mk.mk.mk.nil.cons.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.cons (x, t) (s_2.append SS.join)).join) = join ((a, (Seq.cons (x, t) s_2).join), Seq.map join SS)

Proof state:
case mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ (bind (a, s) f).bind g = bind (a, s) fun x => (f x).bind g

Tactic:
simp only [bind, map_pair, map_join]

Result:
case mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ (join (map g (f a), Seq.map (map g) (Seq.map f s))).join =
    join ((map g (f a)).join, Seq.map (fun x => (map g (f x)).join) s)

Proof state:
α : Type u
β : Type v
γ : Type w
s : Seq1 α
f : α → Seq1 β
g : β → Seq1 γ
⊢ (s.bind f).bind g = s.bind fun x => (f x).bind g

Tactic:
obtain ⟨a, s⟩ := s

Result:
case mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ (bind (a, s) f).bind g = bind (a, s) fun x => (f x).bind g

Proof state:
case mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
⊢ (join (map g (f a), SS)).join = join ((map g (f a)).join, Seq.map join SS)

Tactic:
rcases map g (f a) with ⟨⟨a, s⟩, S⟩

Result:
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 (((a, s), S), SS)).join = join (join ((a, s), S), Seq.map join SS)

Proof state:
case mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ (join (map g (f a), Seq.map (map g) (Seq.map f s))).join =
    join ((map g (f a)).join, Seq.map (fun x => (map g (f x)).join) s)

Tactic:
rw [← map_comp]

Result:
case mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ (join (map g (f a), Seq.map (map g ∘ f) s)).join = join ((map g (f a)).join, Seq.map (fun x => (map g (f x)).join) s)

Proof state:
case mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ (join (map g (f a), Seq.map (map g ∘ f) s)).join = join ((map g (f a)).join, Seq.map (join ∘ map g ∘ f) s)

Tactic:
rw [map_comp _ join]

Result:
case mk
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ (join (map g (f a), Seq.map (map g ∘ f) s)).join = join ((map g (f a)).join, Seq.map join (Seq.map (map g ∘ f) s))