Theorem: Free.free_bind (CoInd/QPF/FreeMonads.lean)

State before:
F : Type u → Type u
inst : QPF F
R S : Type u
f : F (Free F R)
k : R → Free F S
⊢ free f >>= k = free (flip bind k <$> f)
Tactic:
simp only [free, bind, flip]
State after:
F : Type u → Type u
inst : QPF F
R S : Type u
f : F (Free F R)
k : R → Free F S
⊢ corec (bind.automaton k) (Sum.inl (construct (FreeF.Free f))) =
    construct (FreeF.Free ((fun a => corec (bind.automaton k) (Sum.inl a)) <$> f))

State before:
F : Type u → Type u
inst : QPF F
R S : Type u
f : F (Free F R)
k : R → Free F S
⊢ corec (bind.automaton k) (Sum.inl (construct (FreeF.Free f))) =
    construct (FreeF.Free ((fun a => corec (bind.automaton k) (Sum.inl a)) <$> f))
Tactic:
conv =>
  lhs
  rw [←construct_destruct (corec (bind.automaton k) (.inl (construct <| .Free f)))]
  rw [destruct_corec]
  rhs
  rhs
  simp only [bind.automaton, destruct_construct]
State after:
F : Type u → Type u
inst : QPF F
R S : Type u
f : F (Free F R)
k : R → Free F S
⊢ construct (corec (bind.automaton k) <$> FreeF.Free (Sum.inl <$> f)) =
    construct (FreeF.Free ((fun a => corec (bind.automaton k) (Sum.inl a)) <$> f))

State before:
F : Type u → Type u
inst : QPF F
R S : Type u
f : F (Free F R)
k : R → Free F S
⊢ construct (corec (bind.automaton k) <$> FreeF.Free (Sum.inl <$> f)) =
    construct (FreeF.Free ((fun a => corec (bind.automaton k) (Sum.inl a)) <$> f))
Tactic:
apply congrArg
State after:
case h
F : Type u → Type u
inst : QPF F
R S : Type u
f : F (Free F R)
k : R → Free F S
⊢ corec (bind.automaton k) <$> FreeF.Free (Sum.inl <$> f) =
    FreeF.Free ((fun a => corec (bind.automaton k) (Sum.inl a)) <$> f)

State before:
case h
F : Type u → Type u
inst : QPF F
R S : Type u
f : F (Free F R)
k : R → Free F S
⊢ corec (bind.automaton k) <$> FreeF.Free (Sum.inl <$> f) =
    FreeF.Free ((fun a => corec (bind.automaton k) (Sum.inl a)) <$> f)
Tactic:
simp only [Functor.map, ←QPF.map_comp, Function.comp]
State after:
no goals